Warren SmithIndependent checks of technical results Ask for a check
Menu

Cases / Logic software

A logic-solving program changed its answer when a statement that is always true was added

It said
This logic problem has a solution.
Actually
It doesn’t. A harmless change, adding a statement that is always true, had flipped the answer.
Then
Another user found the wrong answer. I found the cause and wrote the fix, which is now released.

cvc5 is an open-source program that solves logic puzzles for other software, including tools that check whether software is correct. Another user showed it gave a wrong answer to a small puzzle. I found the cause and wrote the fix.

The technical record

What it reported

sat

What the check found

Wrong. Adding a statement that holds for every input flipped the answer.

cvc5 is one of the main open-source SMT solvers; verification tools use answers like this one to decide whether a program is correct. Another user reported that on a small separation-logic problem it answered sat when the answer is unsat. I traced the cause to a cache keyed without polarity, wrote the fix, and it shipped in cvc5 1.4.2.

Add a line that should change nothing

The highlighted line is true of every heap, so adding it cannot change the answer. Switch it on and off, and choose the solver version. Every output here was produced by running the solver on 8 October 2026.

(set-logic QF_ALL)
(declare-heap (Int Int))
(assert (not (and sep.emp (pto 1 1))))   ; true of every heap
(assert (or sep.emp (pto 3 3)))
(assert (sep (pto 1 1) (pto 2 2)))
(check-sat)
Solver answersatWrong. Without the line the same solver says unsat.

How the finding was reached

  1. Claim

    cvc5’s answer to this separation-logic problem is correct.

  2. Test

    I reproduced the report, then followed the reduction of each assertion through the solver to find where the wrong answer entered.

  3. What happened

    Two assertions alone: unsat. Add a third that holds for every heap: sat. Re-run on 8 October 2026 against cvc5 1.3.4.

  4. Trying to break the finding

    The reporter had already shown it is a bug, not a question of interpretation: the added assertion is valid, the returned heap breaks the formula, and an option that removes sep.emp early gives the right answer. My question was why. Could the cache be wrong for the other operators too? No: their cached conclusions don’t depend on polarity, so only sep.emp is affected, and the fix changes nothing else.

  5. Evidence

    TheorySep::reduceFact cached reduced conclusions keyed without polarity. That is valid for the other separation-logic operators, but sep.emp emits a polarity-specific lemma and leaves a null conclusion that was still cached. The fix changes the cache key and adds regression tests.

  6. What survives

    A caching bug in one reduction path let cvc5 return a wrong sat. The fix was merged on 1 October 2026 and is in the cvc5 1.4.2 release.

What this does not show

One theory and one class of formula. I did not audit the rest of cvc5. The failing input was found by someone else; my part was the root cause and the fix.

If this had been your system

If a tool you depend on gave you an answer like this, you would have received the minimal input, the location of the fault, a fix or workaround, and a regression test.

Ask for a checkSample report