1
65%
master: 65%

Ran 28 Feb 2026 10:10AM UTC

Files 486

Run time 11s

Badge

Embed ▾

Committed 28 Feb 2026 10:01AM UTC coverage: 65.307% (+0.001%) from 65.306%

Job # 22518557096.1

Build Type

push

github

Committed by

web-flow

Commit Message

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.

Run Details

81263 of 124433 relevant lines covered (65.31%)

1710211.43 hits per line

SRI-CSL / yices2 / 22518557096 / 1
65%
master: 65%

README BADGES
x

Markdown

Textile

RDoc

HTML

Rst

Source Files on job 22518557096.1

SRI-CSL / yices2 / 22518557096 / 1 65% master: 65%

README BADGES x

Markdown

Textile

RDoc

HTML

Rst

Source Files on job 22518557096.1

SRI-CSL / yices2 / 22518557096 / 1
65%
master: 65%

README BADGES
x