diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-11-26 17:40:31 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-11-26 17:40:31 +0000 |
commit | 78f459b303ed292a297a36cd0c435fdd025b0865 (patch) | |
tree | 80be491bc4525d70d599fbd72869dd592f70d56a /test/regress/regress0/push-pop/boolean/fuzz_31.smt2 | |
parent | c3ca3d8c58cc9954f8ad190e1e2dedbcbb5372f0 (diff) |
fixup for incremental solving
Diffstat (limited to 'test/regress/regress0/push-pop/boolean/fuzz_31.smt2')
-rw-r--r-- | test/regress/regress0/push-pop/boolean/fuzz_31.smt2 | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_31.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_31.smt2 new file mode 100644 index 000000000..3df801225 --- /dev/null +++ b/test/regress/regress0/push-pop/boolean/fuzz_31.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LIA) +(declare-fun x0 () Bool) +(declare-fun x1 () Bool) +(assert (not (and (and (or (and (and (or (and (and x1 x1) (and x0 x0)) (or (and x1 x0) (or x1 x0))) (or (not (and x0 x0)) (or (or x0 x1) (or x0 x1)))) (not (and (not (and x1 x1)) (or (not x0) (not x0))))) (and (or (not (not (not x0))) (and (and (or x0 x1) (and x1 x0)) (not (and x1 x1)))) (or (not (not (not x1))) (or (or (and x1 x0) (not x1)) (not (and x0 x0)))))) (not (not (or (and (and (or x1 x0) (not x0)) (not (and x1 x0))) (and (or (not x0) (and x0 x0)) (and (or x0 x0) (or x1 x1))))))) (or (or (or (or (or (or (not x0) (and x1 x0)) (not (or x0 x0))) (and (not (or x0 x1)) (or (not x1) (not x0)))) (or (and (or (or x1 x0) (and x1 x0)) (not (and x1 x0))) (and (and (not x1) (or x1 x1)) (and (not x0) (and x0 x1))))) (or (and (or (or (not x0) (not x0)) (and (not x1) (and x1 x1))) (or (or (and x1 x1) (not x1)) (and (or x0 x1) (and x0 x1)))) (and (and (and (not x1) (not x0)) (or (or x0 x1) (or x1 x0))) (and (or (and x0 x0) (or x0 x1)) (or (or x1 x0) (and x1 x1)))))) (and (not (and (or (not (and x1 x1)) (or (and x0 x1) (not x1))) (not (and (not x1) (or x0 x0))))) (and (not (not (and (not x1) (not x0)))) (not (and (or (not x0) (and x1 x1)) (not (and x1 x0)))))))))) +(check-sat) +(push 1) +(assert (not (or (not (and (and (not (not (not (or (or x0 x1) (not x1))))) (and (and (and (and (not x0) (not x1)) (or (not x1) (not x1))) (and (and (not x1) (or x1 x0)) (and (and x0 x0) (or x0 x1)))) (or (and (not (and x0 x0)) (and (and x1 x1) (and x0 x0))) (and (not (and x0 x1)) (or (and x0 x0) (or x1 x1)))))) (not (and (or (and (not (or x0 x1)) (or (or x0 x0) (and x1 x1))) (and (not (or x0 x1)) (or (not x1) (and x1 x0)))) (and (and (not (or x1 x0)) (and (or x0 x1) (and x0 x1))) (not (not (not x1)))))))) (and (or (not (and (not (not (and (or x1 x1) (or x0 x0)))) (or (not (and (or x1 x1) (not x1))) (not (and (and x0 x0) (not x1)))))) (not (not (not (not (not (and x1 x0))))))) (and (not (not (or (or (or (and x0 x1) (and x0 x0)) (and (not x0) (or x1 x0))) (and (or (or x1 x1) (and x0 x0)) (or (not x0) (and x1 x1)))))) (or (not (and (and (or (not x0) (not x0)) (not (or x1 x0))) (or (and (and x1 x0) (not x0)) (or (or x1 x1) (and x1 x0))))) (and (not (not (and (or x1 x0) (and x0 x1)))) (and (and (not (and x1 x1)) (or (or x0 x1) (not x0))) (and (and (not x0) (not x0)) (or (and x0 x0) (or x0 x1))))))))))) +(assert (not (not (and (or (or (not x1) (or x0 x0)) (and (and x0 x1) (or x0 x0))) (not (not (and x0 x1))))))) +(assert (or (and (or x0 x1) (and x1 x0)) (or (and x1 x0) (not x0)))) +(assert (not (or x0 x0))) +(check-sat) +(pop 1) +(check-sat) +(push 1) +(check-sat) +(push 1) +(assert (or (or (and x0 x0) (and x0 x0)) (and (or x1 x0) (and x1 x0)))) +(assert (and x1 x1)) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(check-sat) +(pop 1) +(check-sat) |