projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 494bf99) | patch
Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 21 Apr 2015 14:34:56 +0000 (16:34 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 21 Apr 2015 14:35:53 +0000 (16:35 +0200)
commit82f4d5bd67f70a561b0f6357f6d6b80c2fcd7b64
treec55a17ef87f4a68a9a0de115fde101452d771dc7tree
parent494bf99194fa4c9eb55eaffa0d090777a34e6359commit | diff
Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.
src/theory/quantifiers/full_model_check.cpp diff | blob | history
test/regress/regress0/datatypes/Makefile.am diff | blob | history
test/regress/regress0/datatypes/bug625.smt2 [new file with mode: 0644] blob
test/regress/regress0/datatypes/manos-model.smt2 [new file with mode: 0644] blob