projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1ddacac) | patch
Fix bug 421, again, and add a second, independent test case for the same
authorMorgan Deters <mdeters@gmail.com>
Thu, 11 Oct 2012 21:17:12 +0000 (21:17 +0000)
committerMorgan Deters <mdeters@gmail.com>
Thu, 11 Oct 2012 21:17:12 +0000 (21:17 +0000)
commit22c270963b48dae4e306972026c8accf7c9a6765
treebdea5da5abc889ff9c053efa6a508a7ca77f6c4dtree
parent1ddacacb1a002fa38292f523f30df50b9e3d70fecommit | diff
Fix bug 421, again, and add a second, independent test case for the same
with --check-models (which caused the same bug, for a different reason,
due to some unintended interaction between the checkModel() function and
the UserContext, which rolled back the Model object.  (Groan...)

(this commit was certified error- and warning-free by the test-and-commit script.)
src/smt/smt_engine.cpp diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/bug421b.smt2 [new file with mode: 0644] blob