diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-26 13:58:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-26 13:58:53 -0500 |
| commit | 2bf51317486cfbfc8c19e32256ca9727bfb2e42a (patch) | |
| tree | a05f035ff50ec261eaf4ae890af8a246c550e386 /src/smt/update_ostream.h | |
| parent | 7e85adc022bc10e2a2b95bd42e216ddddd51e03e (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.
Diffstat (limited to 'src/smt/update_ostream.h')
0 files changed, 0 insertions, 0 deletions