projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7e85adc) | patch
Fix theoryOf for Boolean equalities (#6444)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 26 Apr 2021 18:58:53 +0000 (13:58 -0500)
committerGitHub <noreply@github.com>
Mon, 26 Apr 2021 18:58:53 +0000 (13:58 -0500)
commit2bf51317486cfbfc8c19e32256ca9727bfb2e42a
treea05f035ff50ec261eaf4ae890af8a246c550e386tree
parent7e85adc022bc10e2a2b95bd42e216ddddd51e03ecommit | diff
Fix theoryOf for Boolean equalities (#6444)

Required for fixing a bug in CNF stream's ensureLiteral, which was crashing when combined with unsat-cores-mode=assumptions.

With this PR, we assign a formula like (= (= x y) (= z w)) to have theoryOf THEORY_BOOL. Previously, it mistaken was assigned THEORY_UF if e.g. x,y z, w were terms whose type was an uninterpreted sort.

We should retest unsat-cores-mode=assumptions after this PR is merged.
src/theory/theory.cpp diff | blob | history