diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-12 14:25:25 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-12 14:25:25 -0500 |
| commit | 8b41e8d8128752eba75f32f751ec9c095a6b1d87 (patch) | |
| tree | 68559af9be49966dedfa877b124f76d3af152b7b /test/regress/regress0/push-pop | |
| parent | 15d36d99363b4ee20754498b566bd315150953fc (diff) | |
Work on array pf signature, add working example. Add quantifiers proof signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
Diffstat (limited to 'test/regress/regress0/push-pop')
| -rw-r--r-- | test/regress/regress0/push-pop/bug326.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2 index 51d60e920..8fe88e9f5 100644 --- a/test/regress/regress0/push-pop/bug326.smt2 +++ b/test/regress/regress0/push-pop/bug326.smt2 @@ -31,7 +31,7 @@ (check-sat) (pop) -; EXPECT: unknown +; EXPECT: sat (push);;sat (assert (and (not (R e1 e3)) (R e4 e1))) (check-sat) |