projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7443276) | patch
Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and string...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 9 Apr 2015 13:51:26 +0000 (15:51 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 9 Apr 2015 13:51:26 +0000 (15:51 +0200)
commit3f59801357808a538934b04ce7bf0894dec1b0dd
tree9a32729a077f25fbd7ef2e84825d1e177d29bafdtree
parent7443276e61db276e5ba48d605cb6b08a35c5a100commit | diff
Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and strings preprocessing.  Minor fix for conjecture generation for finite types.
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/first_order_reasoning.cpp diff | blob | history
src/theory/quantifiers/fun_def_process.cpp diff | blob | history
src/theory/quantifiers/macros.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.h diff | blob | history
src/util/sort_inference.cpp diff | blob | history