projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2c18128) | patch
Make conflict-based instantiation abort if a ground conflict is found in the master...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 15 May 2017 14:07:21 +0000 (09:07 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 15 May 2017 14:07:21 +0000 (09:07 -0500)
commit0369b8325e9f631c77d479e5e9103cdb450bf650
tree243626b1ab7a9b5b14ced6d45438c7847ac566abtree
parent2c1812877269667643bdc5e3dc7cf6fcc7ed1630commit | diff
Make conflict-based instantiation abort if a ground conflict is found in the master equality engine during term indexing, fixes bug 801.
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history