projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2150eb2) | patch
Fix term database for non-equal, congruent terms in master equality engine. Disable...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 23 Feb 2016 17:33:09 +0000 (11:33 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 23 Feb 2016 17:33:09 +0000 (11:33 -0600)
commitad3036f0bcaf634489b7e745dcf87bd2102d92aa
treefaaa7ce5f9f5a8ab8ead7f2de16c81a7347c63b8tree
parent2150eb22aaff94f9d0d9f0ee0854ea44675fd854commit | diff
Fix term database for non-equal, congruent terms in master equality engine. Disable ITE terms in quant conflict find.
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
test/regress/regress0/fmf/ForElimination-scala-9.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/Makefile.am diff | blob | history