projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bbcf8cc) | patch
Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant values...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 20 Jan 2016 22:55:02 +0000 (16:55 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 20 Jan 2016 22:55:02 +0000 (16:55 -0600)
commit7006d5ba2f68c01638a2ab2c98a86b41dcf4467c
treeecb2f69f3cbe1a2cabde21a9e9e4e08691c2b734tree
parentbbcf8ccc012caf6ad54b7ec2b91a9886fb6021e6commit | diff
Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant values. Add regression.
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
test/regress/regress0/fmf/fmc_unsound_model.smt2 [new file with mode: 0644] blob