SRI-CSL / yices2 / 22518557096

65%

push

github

Fix issue #536 bool equality evaluation dependencies (#601)

This PR fixes issue #536 in MCSAT bool evaluation explanation for equality terms.

When trying to explain the evaluation of an equality literal, the bool plugin now records both equality argument variables as dependencies before returning the explanation result.
Root cause

For EQ_TERM fallback evaluation, dependency tracking was incomplete: the evaluated equality could be explained without adding the two operand variables to vars.
This could lead to missing dependency information in downstream reasoning/explanations.
Changes

    src/mcsat/bool/bool_plugin.c
        Use eq_term_desc(..., t_unsigned) in the equality fallback path (not necessary, but more readable).
        Add both operand variables (t1_var, t2_var) to vars when both are assigned and used for equality evaluation.

Tests

Added 3 regressions under MCSAT regressions (all expected sat):

    tests/regress/mcsat/iss536a.smt2
    tests/regress/mcsat/iss536b.smt2
    tests/regress/mcsat/iss536c.smt2

Each test exercises bool/array expressions that trigger the equality-evaluation fallback path covered by this fix.

3 of 3 new or added lines in 1 file covered. (100.0%)

81263 of 124433 relevant lines covered (65.31%)

1710211.43 hits per line