projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c76d9cd) | patch
Minor fix for term database + central equality engine (#6928)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 27 Jul 2021 14:24:20 +0000 (09:24 -0500)
committerGitHub <noreply@github.com>
Tue, 27 Jul 2021 14:24:20 +0000 (14:24 +0000)
commit2bb47a96e61babeedfd717104a9ec80b559017a9
treed649c1821504c287cb7b17bbc337d143c31ce686tree
parentc76d9cde04270156030d0a3fa8f1bf8483bfe2ebcommit | diff
Minor fix for term database + central equality engine (#6928)

Previously we provided a bogus (self) explanation in a rare case of setting up the term database for higher order. This is incompatible with cases where central equality engine = master equality engine.
src/theory/quantifiers/term_database.cpp diff | blob | history