diff options
Diffstat (limited to 'test/regress/regress1/push-pop/fuzz_51.smt2')
| -rw-r--r-- | test/regress/regress1/push-pop/fuzz_51.smt2 | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/test/regress/regress1/push-pop/fuzz_51.smt2 b/test/regress/regress1/push-pop/fuzz_51.smt2 new file mode 100644 index 000000000..f9bdb084f --- /dev/null +++ b/test/regress/regress1/push-pop/fuzz_51.smt2 @@ -0,0 +1,36 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +(set-logic QF_LIA) +(declare-fun x0 () Bool) +(check-sat) +(push 1) +(assert (not (and (or (and (and (or x0 x0) (or x0 x0)) (or (not x0) (and x0 x0))) (and (or (or x0 x0) (not x0)) (not (and x0 x0)))) (or (or (or (not x0) (or x0 x0)) (and (or x0 x0) (and x0 x0))) (or (or (not x0) (or x0 x0)) (not (or x0 x0))))))) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(check-sat) +(pop 1) +(assert (or (and (and (not (and (or (or (or (not (not x0)) (not (and x0 x0))) (or (not (and x0 x0)) (and (and x0 x0) (and x0 x0)))) (not (not (or (or x0 x0) (or x0 x0))))) (or (not (or (or (not x0) (not x0)) (not (or x0 x0)))) (not (not (and (and x0 x0) (and x0 x0))))))) (or (or (not (or (and (or (and x0 x0) (and x0 x0)) (not (or x0 x0))) (not (and (or x0 x0) (or x0 x0))))) (or (not (not (and (and x0 x0) (and x0 x0)))) (not (not (and (or x0 x0) (not x0)))))) (not (not (and (and (or (and x0 x0) (or x0 x0)) (and (or x0 x0) (not x0))) (not (not (or x0 x0)))))))) (and (or (or (or (and (and (not (and x0 x0)) (and (and x0 x0) (or x0 x0))) (or (and (not x0) (and x0 x0)) (and (not x0) (or x0 x0)))) (and (or (and (and x0 x0) (or x0 x0)) (or (or x0 x0) (and x0 x0))) (or (and (or x0 x0) (and x0 x0)) (or (and x0 x0) (not x0))))) (or (and (and (or (not x0) (not x0)) (and (not x0) (not x0))) (or (or (not x0) (and x0 x0)) (or (or x0 x0) (and x0 x0)))) (not (and (not (or x0 x0)) (not (not x0)))))) (or (not (not (or (not (or x0 x0)) (and (and x0 x0) (or x0 x0))))) (and (or (not (or (not x0) (or x0 x0))) (or (or (not x0) (or x0 x0)) (or (not x0) (or x0 x0)))) (and (not (or (not x0) (not x0))) (not (and (not x0) (or x0 x0))))))) (or (or (and (or (and (and (not x0) (and x0 x0)) (not (and x0 x0))) (not (not (not x0)))) (and (and (or (and x0 x0) (not x0)) (and (or x0 x0) (not x0))) (or (not (and x0 x0)) (not (and x0 x0))))) (and (or (or (not (not x0)) (and (not x0) (and x0 x0))) (not (or (and x0 x0) (or x0 x0)))) (not (and (not (not x0)) (not (and x0 x0)))))) (not (and (not (not (not (not x0)))) (or (not (not (or x0 x0))) (not (or (and x0 x0) (or x0 x0))))))))) (not (and (or (not (and (and (not (not (not x0))) (and (and (and x0 x0) (and x0 x0)) (and (not x0) (or x0 x0)))) (and (or (or (and x0 x0) (not x0)) (and (not x0) (not x0))) (or (not (or x0 x0)) (and (or x0 x0) (or x0 x0)))))) (not (and (or (or (and (and x0 x0) (not x0)) (and (not x0) (and x0 x0))) (or (not (and x0 x0)) (not (or x0 x0)))) (and (and (or (not x0) (and x0 x0)) (and (and x0 x0) (and x0 x0))) (and (or (or x0 x0) (or x0 x0)) (or (and x0 x0) (or x0 x0))))))) (and (or (and (and (or (and (and x0 x0) (not x0)) (or (and x0 x0) (not x0))) (and (and (not x0) (and x0 x0)) (not (or x0 x0)))) (or (and (or (and x0 x0) (and x0 x0)) (not (or x0 x0))) (not (or (and x0 x0) (or x0 x0))))) (and (or (or (and (or x0 x0) (or x0 x0)) (not (not x0))) (and (not (and x0 x0)) (not (not x0)))) (and (not (and (not x0) (not x0))) (and (or (and x0 x0) (and x0 x0)) (or (or x0 x0) (and x0 x0)))))) (and (and (or (not (not (and x0 x0))) (or (or (and x0 x0) (not x0)) (or (not x0) (or x0 x0)))) (not (or (and (not x0) (and x0 x0)) (or (and x0 x0) (or x0 x0))))) (not (or (or (not (not x0)) (or (not x0) (not x0))) (not (not (and x0 x0))))))))))) +(check-sat) +(push 1) +(assert (and (not (and (not (not (not x0))) (or (not (not x0)) (and (not x0) (or x0 x0))))) (or (not (not (or (not x0) (or x0 x0)))) (and (and (or (or x0 x0) (not x0)) (not (and x0 x0))) (not (or (not x0) (not x0))))))) +(check-sat) +(push 1) +(check-sat) +(push 1) +(assert (not (or (not (or (and (and (not (or (not (not x0)) (not (not x0)))) (and (not (not (or x0 x0))) (or (and (or x0 x0) (and x0 x0)) (and (or x0 x0) (and x0 x0))))) (or (not (or (and (not x0) (not x0)) (or (not x0) (not x0)))) (and (and (or (not x0) (and x0 x0)) (or (or x0 x0) (and x0 x0))) (not (not (and x0 x0)))))) (not (not (and (or (not (and x0 x0)) (or (or x0 x0) (and x0 x0))) (not (not (and x0 x0)))))))) (not (or (and (or (and (not (or (not x0) (and x0 x0))) (and (or (and x0 x0) (and x0 x0)) (not (or x0 x0)))) (or (and (or (not x0) (not x0)) (not (and x0 x0))) (or (and (and x0 x0) (not x0)) (and (or x0 x0) (and x0 x0))))) (and (or (and (and (or x0 x0) (not x0)) (or (or x0 x0) (and x0 x0))) (not (or (and x0 x0) (and x0 x0)))) (not (or (not (not x0)) (or (not x0) (not x0)))))) (or (or (or (and (or (and x0 x0) (not x0)) (not (not x0))) (and (not (or x0 x0)) (and (not x0) (not x0)))) (or (not (and (and x0 x0) (and x0 x0))) (and (not (not x0)) (and (or x0 x0) (not x0))))) (or (and (not (not (not x0))) (and (and (and x0 x0) (not x0)) (or (and x0 x0) (and x0 x0)))) (or (and (not (or x0 x0)) (and (and x0 x0) (not x0))) (or (not (not x0)) (and (or x0 x0) (or x0 x0))))))))))) +(check-sat) +(push 1) +(assert (and (or (not (not (and (and (not (not (not (and x0 x0)))) (not (not (and (or x0 x0) (not x0))))) (and (or (or (and (or x0 x0) (or x0 x0)) (or (not x0) (or x0 x0))) (and (and (and x0 x0) (not x0)) (or (not x0) (or x0 x0)))) (or (not (and (and x0 x0) (not x0))) (not (not (not x0)))))))) (or (and (and (and (or (or (not (not x0)) (and (or x0 x0) (or x0 x0))) (and (and (and x0 x0) (or x0 x0)) (and (not x0) (or x0 x0)))) (or (or (not (not x0)) (or (or x0 x0) (and x0 x0))) (or (or (and x0 x0) (or x0 x0)) (not (and x0 x0))))) (not (or (not (or (and x0 x0) (not x0))) (and (and (not x0) (not x0)) (or (not x0) (or x0 x0)))))) (not (and (and (not (and (or x0 x0) (not x0))) (and (or (or x0 x0) (or x0 x0)) (or (and x0 x0) (or x0 x0)))) (or (or (not (not x0)) (and (not x0) (and x0 x0))) (and (and (or x0 x0) (or x0 x0)) (and (and x0 x0) (not x0))))))) (not (or (or (and (not (and (and x0 x0) (and x0 x0))) (or (or (or x0 x0) (or x0 x0)) (and (and x0 x0) (not x0)))) (not (not (or (or x0 x0) (or x0 x0))))) (not (or (or (or (and x0 x0) (not x0)) (not (or x0 x0))) (or (not (or x0 x0)) (and (and x0 x0) (or x0 x0))))))))) (or (or (and (not (not (not (and (or (or x0 x0) (not x0)) (and (not x0) (not x0)))))) (or (or (not (and (not (and x0 x0)) (not (and x0 x0)))) (not (not (not (or x0 x0))))) (or (and (or (or (or x0 x0) (not x0)) (or (and x0 x0) (not x0))) (or (and (not x0) (and x0 x0)) (not (not x0)))) (not (or (and (not x0) (and x0 x0)) (and (not x0) (and x0 x0))))))) (or (not (and (and (or (or (or x0 x0) (or x0 x0)) (not (not x0))) (or (and (not x0) (and x0 x0)) (not (and x0 x0)))) (or (or (not (not x0)) (or (and x0 x0) (and x0 x0))) (not (and (not x0) (and x0 x0)))))) (or (and (or (not (and (and x0 x0) (and x0 x0))) (not (or (not x0) (or x0 x0)))) (and (not (and (or x0 x0) (or x0 x0))) (or (or (not x0) (or x0 x0)) (or (and x0 x0) (or x0 x0))))) (not (or (and (or (not x0) (and x0 x0)) (and (and x0 x0) (or x0 x0))) (not (and (or x0 x0) (and x0 x0)))))))) (not (or (and (or (or (or (and (or x0 x0) (and x0 x0)) (and (not x0) (or x0 x0))) (and (or (or x0 x0) (not x0)) (or (or x0 x0) (and x0 x0)))) (not (or (and (or x0 x0) (or x0 x0)) (or (or x0 x0) (or x0 x0))))) (or (not (and (and (or x0 x0) (or x0 x0)) (or (and x0 x0) (not x0)))) (and (not (and (or x0 x0) (not x0))) (and (and (or x0 x0) (and x0 x0)) (and (not x0) (not x0)))))) (and (not (or (or (or (and x0 x0) (not x0)) (or (not x0) (or x0 x0))) (and (and (not x0) (not x0)) (not (not x0))))) (not (or (not (and (not x0) (or x0 x0))) (or (or (not x0) (and x0 x0)) (not (and x0 x0))))))))))) +(assert (or (not (and (or x0 x0) (or x0 x0))) (or (not (or x0 x0)) (not (not x0))))) +(assert (not (and (not (and (or (and (or x0 x0) (and x0 x0)) (not (and x0 x0))) (not (not (or x0 x0))))) (and (and (not (or (not x0) (not x0))) (and (or (and x0 x0) (or x0 x0)) (and (not x0) (not x0)))) (or (and (and (and x0 x0) (and x0 x0)) (or (not x0) (not x0))) (and (and (or x0 x0) (or x0 x0)) (or (not x0) (not x0)))))))) +(check-sat) |