diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-25 15:16:41 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-25 15:16:41 +0000 |
commit | 89bcd4deee07a2c61d30a9dfca64e58e8c2d701b (patch) | |
tree | d60e9264731c73a88a3947a06dea6ff294ff0f80 /test/regress/regress0/push-pop/bug326.smt2 | |
parent | 86df00c36c6cbabac53001082219c3fc8c0fa297 (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.)
Diffstat (limited to 'test/regress/regress0/push-pop/bug326.smt2')
-rw-r--r-- | test/regress/regress0/push-pop/bug326.smt2 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2 index 3797cb105..04b417e17 100644 --- a/test/regress/regress0/push-pop/bug326.smt2 +++ b/test/regress/regress0/push-pop/bug326.smt2 @@ -1,3 +1,6 @@ +; COMMAND-LINE: --incremental +; EXIT: 10 + (set-logic AUFLIA) (declare-fun R (Int Int) Bool) |