projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 86df00c) | patch
some buggy examples for incrementality, and make bug326 run as part of make regress...
authorMorgan Deters <mdeters@gmail.com>
Tue, 25 Sep 2012 15:16:41 +0000 (15:16 +0000)
committerMorgan Deters <mdeters@gmail.com>
Tue, 25 Sep 2012 15:16:41 +0000 (15:16 +0000)
commit89bcd4deee07a2c61d30a9dfca64e58e8c2d701b
treed60e9264731c73a88a3947a06dea6ff294ff0f80tree
parent86df00c36c6cbabac53001082219c3fc8c0fa297commit | diff
some buggy examples for incrementality, and make bug326 run as part of make regress, because the bug was fixed.

Also make QuantifiersModule's destructor virtual (it has virtual members).

(this commit was certified error- and warning-free by the test-and-commit script.)
src/theory/quantifiers_engine.h diff | blob | history
test/regress/regress0/push-pop/Makefile.am diff | blob | history
test/regress/regress0/push-pop/bug326.smt2 diff | blob | history
test/regress/regress0/push-pop/bug394.smt2 [new file with mode: 0644] blob
test/regress/regress0/push-pop/bug396.smt2 [new file with mode: 0644] blob