projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b71bbbb) | patch
Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). Improve...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 14 Apr 2014 20:36:28 +0000 (15:36 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 14 Apr 2014 20:36:28 +0000 (15:36 -0500)
commit1138911e0af7c15a7b41a5d02ff3edab2c837449
tree6b7a70bd32d461cff687f11def74bab0447aad82tree
parentb71bbbbc607b5ca0c2bec8b8cf6c7af596d21997commit | diff
Fix bug in mbqi=fmc handling theory symbols.  Fix mbqi=fmc models (Bug 557).  Improve datatypes rewrite, make option for previous dt semantics.
src/theory/datatypes/datatypes_rewriter.h diff | blob | history
src/theory/datatypes/options diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers/first_order_model.cpp diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history