From 55037e0bcef45c795f28ff3fcf6c1055af465c70 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 15 Feb 2018 15:31:48 -0600 Subject: Refactor regressions (#1581) --- test/regress/regress1/push-pop/fuzz_41.smt2 | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 test/regress/regress1/push-pop/fuzz_41.smt2 (limited to 'test/regress/regress1/push-pop/fuzz_41.smt2') diff --git a/test/regress/regress1/push-pop/fuzz_41.smt2 b/test/regress/regress1/push-pop/fuzz_41.smt2 new file mode 100644 index 000000000..b6d2e884f --- /dev/null +++ b/test/regress/regress1/push-pop/fuzz_41.smt2 @@ -0,0 +1,25 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +(set-logic QF_LIA) +(declare-fun x0 () Bool) +(declare-fun x1 () Bool) +(declare-fun x2 () Bool) +(check-sat) +(push 1) +(assert (or (or (or (and (and (not (and (or x0 x0) (not x0))) (not (or (or x2 x2) (not x0)))) (or (or (not (or x0 x0)) (or (and x0 x2) (or x0 x2))) (and (and (and x1 x1) (and x2 x1)) (not (not x2))))) (and (not (not (and (not x2) (and x0 x2)))) (not (not (and (not x2) (not x1)))))) (not (or (and (not (and (not x2) (not x0))) (and (not (not x0)) (and (not x1) (and x2 x2)))) (and (not (and (not x2) (or x1 x0))) (or (or (or x1 x0) (or x0 x0)) (or (or x0 x0) (not x1))))))) (not (not (not (and (not (or (or x2 x0) (not x2))) (not (and (not x0) (or x0 x1))))))))) +(assert (or (not (or (and (or (or x0 x0) (or x2 x2)) (and (not x1) (or x2 x2))) (and (not (not x1)) (and (or x0 x0) (or x0 x1))))) (not (and (or (and (and x1 x2) (not x1)) (not (not x2))) (not (and (and x2 x0) (not x1))))))) +(assert (or (not (not x2)) (not (not x0)))) +(assert (not (or (not (or (and (and (and x0 x0) (or x1 x1)) (or (or x0 x2) (not x1))) (not (or (or x0 x1) (or x0 x0))))) (not (not (not (or (or x1 x1) (not x2)))))))) +(check-sat) +(pop 1) +(assert (not (and (not (and (and (or (and (and (or (not x0) (not x1)) (and (or x1 x1) (not x2))) (and (and (or x1 x0) (and x1 x2)) (and (not x0) (not x2)))) (not (or (or (or x1 x0) (not x1)) (or (or x0 x1) (not x2))))) (or (or (and (not (not x0)) (or (or x0 x1) (not x0))) (or (not (or x0 x2)) (not (or x0 x0)))) (not (and (or (and x1 x1) (not x0)) (or (and x1 x1) (or x1 x0)))))) (or (and (not (or (not (and x0 x0)) (and (and x0 x2) (and x2 x0)))) (not (and (and (or x0 x2) (and x0 x2)) (and (not x0) (and x0 x1))))) (and (or (not (and (and x2 x1) (not x2))) (or (and (and x2 x2) (and x2 x2)) (or (or x0 x1) (or x1 x2)))) (or (and (and (and x2 x1) (or x1 x0)) (and (or x2 x0) (not x1))) (and (not (or x2 x2)) (or (and x2 x0) (and x0 x0)))))))) (or (and (or (not (and (not (not (or x2 x0))) (and (or (and x0 x1) (or x0 x1)) (not (not x1))))) (not (and (and (or (or x0 x1) (not x1)) (not (not x2))) (not (or (not x2) (not x2)))))) (and (or (and (or (not (and x2 x2)) (or (and x1 x2) (or x2 x2))) (and (or (not x2) (and x2 x2)) (not (not x2)))) (not (not (and (not x2) (not x1))))) (not (and (and (and (or x1 x1) (and x0 x0)) (or (or x0 x0) (not x1))) (or (and (or x2 x1) (not x2)) (and (or x2 x2) (not x1))))))) (not (or (and (and (or (or (not x2) (not x0)) (not (and x1 x0))) (and (not (not x0)) (or (and x1 x0) (or x1 x0)))) (and (and (or (and x0 x2) (not x2)) (and (or x2 x2) (not x1))) (not (or (and x0 x1) (and x1 x0))))) (or (not (or (not (and x1 x0)) (not (not x2)))) (not (not (and (or x2 x0) (not x1))))))))))) +(check-sat) +(push 1) +(assert (or (and (and (or (or (and (not (and (or (or x2 x0) (or x0 x1)) (not (or x2 x1)))) (or (not (not (not x2))) (not (not (or x1 x1))))) (or (or (and (or (and x2 x0) (not x1)) (or (or x2 x2) (and x1 x2))) (or (or (and x0 x0) (and x2 x0)) (or (not x2) (or x0 x1)))) (and (or (and (or x0 x0) (or x2 x0)) (not (not x1))) (not (and (or x1 x2) (or x1 x1)))))) (and (not (not (and (or (or x1 x0) (and x1 x1)) (not (or x1 x0))))) (and (and (and (or (or x0 x2) (and x0 x2)) (and (and x2 x2) (and x0 x1))) (or (or (or x1 x1) (not x2)) (not (not x1)))) (not (not (or (or x1 x0) (and x2 x0))))))) (not (not (and (or (not (or (and x1 x2) (not x2))) (and (and (or x2 x0) (and x1 x0)) (and (or x1 x0) (or x2 x1)))) (not (or (not (not x0)) (not (and x2 x2)))))))) (and (or (and (or (not (not (and (and x1 x1) (and x1 x1)))) (or (and (not (and x0 x1)) (or (or x2 x2) (or x0 x1))) (and (not (not x0)) (not (and x0 x0))))) (not (and (or (and (not x1) (not x2)) (not (or x2 x1))) (and (and (not x0) (and x0 x2)) (or (and x2 x2) (not x2)))))) (or (and (and (not (and (or x1 x0) (or x0 x1))) (not (or (or x2 x1) (or x1 x0)))) (and (and (or (and x1 x1) (not x2)) (or (not x0) (and x0 x1))) (not (not (or x0 x2))))) (not (and (not (or (and x2 x0) (or x2 x0))) (not (not (not x0))))))) (or (or (not (and (and (not (not x0)) (or (and x1 x2) (not x0))) (and (not (not x0)) (and (or x0 x2) (not x1))))) (and (not (and (or (not x1) (and x0 x0)) (and (not x1) (and x2 x2)))) (not (and (or (and x0 x0) (not x0)) (and (not x2) (and x0 x2)))))) (and (and (or (not (or (not x1) (or x1 x2))) (or (or (and x1 x1) (and x0 x0)) (not (and x0 x0)))) (not (or (and (or x0 x0) (not x1)) (or (and x0 x2) (or x1 x1))))) (not (and (not (not (and x2 x1))) (or (and (not x1) (not x0)) (not (or x0 x2))))))))) (or (and (or (and (not (or (or (or (not x1) (or x0 x0)) (and (or x2 x1) (not x1))) (and (or (not x2) (or x1 x2)) (or (and x2 x1) (and x1 x0))))) (and (not (and (and (or x2 x0) (not x2)) (and (or x1 x1) (or x2 x0)))) (not (or (and (and x0 x2) (and x0 x2)) (not (or x1 x1)))))) (not (or (not (or (and (and x0 x1) (not x1)) (or (and x2 x1) (not x2)))) (and (and (and (not x2) (and x2 x1)) (not (or x2 x2))) (and (and (or x1 x1) (not x1)) (or (and x0 x1) (not x1))))))) (not (and (or (and (or (or (not x2) (not x1)) (not (and x1 x1))) (or (not (or x0 x0)) (not (and x2 x1)))) (not (and (not (and x1 x1)) (or (not x1) (and x0 x2))))) (or (or (or (not (or x2 x2)) (and (and x1 x0) (and x1 x1))) (not (and (or x1 x0) (or x0 x2)))) (and (not (or (or x2 x2) (and x2 x0))) (not (and (and x2 x2) (or x1 x1)))))))) (not (or (not (or (not (and (not (and x2 x2)) (and (or x0 x1) (and x2 x0)))) (and (not (not (and x2 x0))) (or (and (and x0 x0) (not x0)) (and (and x0 x1) (not x0)))))) (or (not (or (or (and (and x0 x2) (and x2 x0)) (and (and x2 x1) (or x2 x2))) (and (or (or x0 x0) (or x1 x0)) (and (and x2 x1) (or x0 x1))))) (and (or (or (not (or x0 x1)) (not (or x0 x1))) (or (not (not x0)) (not (and x0 x2)))) (not (not (or (or x2 x2) (not x2))))))))))) +(check-sat) +(pop 1) +(check-sat) -- cgit v1.2.3