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/arith | |
| parent | c3ca3d8c58cc9954f8ad190e1e2dedbcbb5372f0 (diff) | |
fixup for incremental solving
Diffstat (limited to 'test/regress/regress0/push-pop/arith')
23 files changed, 1071 insertions, 0 deletions
diff --git a/test/regress/regress0/push-pop/arith/Makefile b/test/regress/regress0/push-pop/arith/Makefile new file mode 100644 index 000000000..d0abd99f5 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../../.. +srcdir = test/regress/regress0/push-pop/arith + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/push-pop/arith/Makefile.am b/test/regress/regress0/push-pop/arith/Makefile.am new file mode 100644 index 000000000..37a6e6c42 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/Makefile.am @@ -0,0 +1,58 @@ +SUBDIRS = . + +BINARY = cvc4 +LOG_COMPILER = @srcdir@/../../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" + +# Regression tests for SMT inputs +CVC_TESTS = + +SMT2_TESTS = \ + fuzz_3_10.smt2 \ + fuzz_3_11.smt2 \ + fuzz_3_12.smt2 \ + fuzz_3_13.smt2 \ + fuzz_3_14.smt2 \ + fuzz_3_15.smt2 \ + fuzz_3_1.smt2 \ + fuzz_3_2.smt2 \ + fuzz_3_3.smt2 \ + fuzz_3_4.smt2 \ + fuzz_3_5.smt2 \ + fuzz_3_6.smt2 \ + fuzz_3_7.smt2 \ + fuzz_3_8.smt2 \ + fuzz_3_9.smt2 \ + fuzz_5_1.smt2 \ + fuzz_5_2.smt2 \ + fuzz_5_3.smt2 \ + fuzz_5_4.smt2 \ + fuzz_5_5.smt2 \ + fuzz_5_6.smt2 + +BUG_TESTS = + +TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) + +EXTRA_DIST = $(TESTS) + +# synonyms for "check" in this directory +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2 new file mode 100644 index 000000000..73399358a --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2 @@ -0,0 +1,32 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (or (not (<= (+ (* (- 24) x0 ) (* (- 15) x2 ) (* (- 18) x2 ) ) 2)) (not (< (+ (* (- 21) x2 ) (* 6 x2 ) ) (- 11))) (> (+ (* (- 3) x0 ) (* 8 x1 ) ) 11) )) +(assert (not (> (+ (* (- 4) x2 ) (* (- 23) x2 ) ) (- 26))) ) +(assert (or (not (< (+ (* 35 x2 ) (* 40 x0 ) (* 38 x0 ) ) (- 4))) (not (<= (+ (* 46 x0 ) (* (- 16) x1 ) ) (- 44))) (> (+ (* 33 x2 ) (* (- 47) x2 ) (* (- 38) x0 ) ) 32) )) +(assert (or (<= (+ (* 49 x2 ) (* 42 x0 ) (* 36 x0 ) (* (- 15) x0 ) ) 41) (not (= (+ (* 5 x2 ) (* (- 2) x0 ) ) (- 23))) )) +(assert (or (< (+ (* 9 x1 ) (* (- 16) x1 ) (* 47 x2 ) (* 2 x0 ) ) (- 18)) (not (>= (+ (* 43 x0 ) (* (- 24) x1 ) ) (- 22))) (not (< (+ (* (- 37) x1 ) (* (- 27) x2 ) (* (- 40) x0 ) (* (- 34) x0 ) ) (- 42))) )) +(assert (or (not (<= (+ (* (- 26) x1 ) (* (- 20) x0 ) ) 26)) (<= (+ (* 24 x0 ) (* (- 40) x2 ) ) (- 50)) )) +(check-sat) +(push 1) +(assert (or (< (+ (* (- 23) x0 ) (* 25 x2 ) ) 47) (not (>= (+ (* (- 3) x0 ) (* 20 x1 ) (* (- 22) x0 ) ) 4)) (<= (+ (* (- 14) x0 ) (* 32 x2 ) (* 2 x0 ) (* 13 x1 ) ) (- 3)) )) +(assert (or (>= (+ (* (- 6) x0 ) (* (- 22) x2 ) ) (- 41)) (not (< (+ (* 26 x0 ) (* 15 x1 ) ) 6)) )) +(assert (<= (+ (* (- 14) x2 ) (* (- 39) x0 ) (* (- 31) x1 ) ) 24) ) +(assert (or (> (+ (* (- 27) x2 ) (* (- 35) x1 ) ) (- 46)) (< (+ (* (- 41) x0 ) (* 46 x1 ) (* 16 x2 ) (* (- 31) x2 ) ) 29) (not (<= (+ (* (- 44) x2 ) (* 46 x0 ) (* (- 33) x1 ) ) (- 14))) )) +(check-sat) +(assert (not (>= (+ (* 23 x2 ) (* 5 x1 ) ) (- 16))) ) +(assert (or (>= (+ (* (- 3) x0 ) (* 3 x1 ) (* 44 x0 ) ) (- 39)) (> (+ (* 28 x1 ) (* 26 x1 ) (* (- 22) x2 ) (* (- 36) x2 ) ) 27) (not (= (+ (* 16 x0 ) (* 41 x2 ) (* 16 x2 ) ) (- 47))) )) +(check-sat) +(pop 1) +(assert (not (<= (+ (* (- 28) x1 ) (* (- 11) x0 ) (* 9 x0 ) (* (- 4) x0 ) ) 23)) ) +(assert (not (< (+ (* 16 x1 ) (* (- 18) x2 ) ) 34)) ) +(assert (or (> (+ (* (- 41) x0 ) (* (- 12) x2 ) ) 11) (>= (+ (* 11 x1 ) (* 26 x0 ) (* 11 x1 ) (* 43 x1 ) ) 8) )) +(assert (or (> (+ (* 17 x2 ) (* (- 35) x2 ) ) 49) (not (= (+ (* 2 x0 ) (* 32 x1 ) (* 40 x1 ) (* 1 x0 ) ) (- 6))) (> (+ (* (- 18) x1 ) (* (- 40) x0 ) (* (- 40) x0 ) ) (- 36)) )) +(check-sat) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2 new file mode 100644 index 000000000..cdd6a6b18 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (or (not (<= (+ (* 30 x2 ) (* 34 x2 ) (* 16 x2 ) ) 30)) (not (>= (+ (* (- 7) x1 ) (* 5 x1 ) ) (- 36))) )) +(assert (= (+ (* (- 33) x2 ) (* (- 46) x0 ) (* (- 32) x1 ) ) (- 30)) ) +(assert (or (>= (+ (* (- 35) x1 ) (* (- 29) x1 ) (* 30 x1 ) (* 20 x1 ) ) 27) (> (+ (* 30 x1 ) (* 33 x0 ) ) 16) (= (+ (* (- 28) x2 ) (* 7 x1 ) (* 8 x0 ) ) 37) )) +(assert (or (< (+ (* 6 x2 ) (* (- 12) x1 ) ) (- 14)) (not (<= (+ (* (- 23) x1 ) (* 44 x1 ) ) 9)) (not (<= (+ (* (- 18) x2 ) (* 16 x0 ) (* 47 x0 ) ) 25)) )) +(assert (or (< (+ (* (- 8) x1 ) (* 12 x2 ) (* 23 x1 ) ) (- 50)) (not (> (+ (* 37 x1 ) (* (- 30) x2 ) (* 1 x0 ) (* 13 x1 ) ) (- 22))) )) +(check-sat) +(push 1) +(assert (or (not (= (+ (* (- 3) x0 ) (* (- 49) x1 ) ) 25)) (<= (+ (* 47 x2 ) (* 9 x0 ) ) (- 5)) )) +(assert (or (not (< (+ (* 34 x0 ) (* 28 x0 ) (* 36 x0 ) (* 1 x0 ) ) (- 9))) (>= (+ (* (- 4) x2 ) (* 15 x1 ) (* (- 35) x0 ) (* (- 2) x1 ) ) (- 20)) )) +(assert (not (<= (+ (* (- 4) x1 ) (* 22 x1 ) (* 22 x2 ) (* (- 33) x0 ) ) 12)) ) +(check-sat) +(pop 1) +(assert (<= (+ (* 36 x0 ) (* (- 25) x2 ) (* 48 x2 ) (* (- 14) x1 ) ) (- 9)) ) +(check-sat) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2 new file mode 100644 index 000000000..9078acf46 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2 @@ -0,0 +1,41 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (or (= (+ (* 25 x1 ) (* (- 35) x1 ) ) 3) (> (+ (* 31 x1 ) (* (- 25) x2 ) (* 24 x1 ) (* (- 37) x2 ) ) 37) )) +(assert (or (= (+ (* (- 18) x1 ) (* (- 42) x0 ) (* (- 41) x2 ) ) 18) (= (+ (* (- 34) x2 ) (* 14 x0 ) (* 33 x0 ) (* (- 40) x2 ) ) (- 34)) )) +(assert (or (>= (+ (* (- 45) x1 ) (* (- 21) x1 ) ) 30) (>= (+ (* 6 x2 ) (* (- 32) x0 ) (* (- 38) x0 ) ) 4) )) +(assert (or (not (< (+ (* (- 39) x2 ) (* (- 47) x2 ) ) 23)) (>= (+ (* 12 x2 ) (* 32 x1 ) (* (- 46) x2 ) ) 13) (not (= (+ (* 48 x2 ) (* 26 x1 ) (* 45 x2 ) ) (- 10))) )) +(check-sat) +(push 1) +(assert (or (not (<= (+ (* (- 34) x2 ) (* (- 24) x1 ) ) 39)) (<= (+ (* 34 x1 ) (* (- 35) x0 ) (* (- 13) x1 ) (* 2 x2 ) ) (- 2)) )) +(check-sat) +(push 1) +(assert (or (not (<= (+ (* (- 12) x0 ) (* 37 x1 ) (* (- 30) x0 ) ) (- 43))) (> (+ (* 28 x0 ) (* (- 49) x1 ) ) (- 22)) )) +(check-sat) +(pop 1) +(assert (or (not (>= (+ (* 49 x1 ) (* (- 19) x2 ) ) (- 4))) (not (< (+ (* (- 50) x2 ) (* (- 18) x1 ) ) (- 11))) (not (< (+ (* 43 x0 ) (* 11 x1 ) (* 26 x0 ) (* (- 46) x2 ) ) (- 11))) )) +(assert (or (< (+ (* 38 x0 ) (* (- 19) x1 ) ) (- 31)) (= (+ (* (- 15) x0 ) (* 28 x2 ) (* 9 x2 ) ) (- 43)) )) +(assert (or (>= (+ (* (- 4) x0 ) (* 20 x1 ) (* (- 30) x1 ) (* 17 x0 ) ) (- 13)) (< (+ (* 6 x0 ) (* (- 22) x2 ) (* (- 37) x1 ) (* (- 1) x2 ) ) (- 50)) )) +(assert (or (not (< (+ (* 33 x1 ) (* (- 30) x2 ) (* (- 18) x1 ) ) (- 32))) (> (+ (* 26 x0 ) (* (- 21) x1 ) ) 46) )) +(assert (or (not (<= (+ (* 3 x0 ) (* (- 19) x2 ) (* (- 50) x1 ) (* 31 x2 ) ) 23)) (= (+ (* 46 x0 ) (* 47 x1 ) (* (- 38) x2 ) (* 32 x0 ) ) 30) (<= (+ (* (- 44) x1 ) (* 32 x0 ) (* 29 x1 ) ) 19) )) +(assert (not (= (+ (* (- 21) x1 ) (* (- 4) x0 ) (* 38 x1 ) (* 17 x1 ) ) 35)) ) +(assert (or (<= (+ (* (- 42) x1 ) (* 8 x0 ) (* 37 x1 ) ) (- 33)) (not (> (+ (* 40 x0 ) (* 41 x0 ) (* 4 x1 ) (* (- 17) x2 ) ) 33)) )) +(assert (or (not (<= (+ (* (- 26) x2 ) (* 25 x0 ) (* 42 x0 ) (* 40 x2 ) ) 2)) (> (+ (* (- 33) x2 ) (* 18 x2 ) ) 47) )) +(check-sat) +(push 1) +(assert (or (not (>= (+ (* 13 x2 ) (* (- 16) x2 ) (* (- 18) x0 ) ) (- 15))) (not (< (+ (* 1 x0 ) (* 0 x2 ) (* (- 3) x2 ) (* 43 x0 ) ) 30)) (not (> (+ (* 10 x2 ) (* 36 x1 ) ) (- 17))) )) +(assert (or (not (< (+ (* (- 34) x0 ) (* (- 19) x1 ) (* 31 x0 ) (* 11 x1 ) ) 34)) (= (+ (* (- 45) x2 ) (* 48 x2 ) (* (- 43) x1 ) ) (- 44)) (>= (+ (* 16 x2 ) (* 10 x2 ) (* (- 21) x1 ) ) 23) )) +(check-sat) +(pop 1) +(assert (or (< (+ (* 27 x1 ) (* 6 x2 ) ) 13) (not (<= (+ (* 11 x1 ) (* 19 x0 ) (* (- 41) x0 ) (* (- 29) x1 ) ) (- 6))) (not (= (+ (* (- 16) x2 ) (* (- 8) x1 ) ) 2)) )) +(assert (or (= (+ (* (- 48) x1 ) (* (- 26) x1 ) (* (- 30) x0 ) ) 39) (>= (+ (* 21 x1 ) (* 25 x2 ) (* (- 35) x1 ) ) (- 2)) (= (+ (* (- 4) x1 ) (* 46 x0 ) (* 23 x2 ) ) 38) )) +(check-sat) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2 new file mode 100644 index 000000000..f3d6d95de --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2 @@ -0,0 +1,50 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (or (not (> (+ (* (- 45) x0 ) (* 2 x2 ) (* (- 18) x1 ) (* 12 x2 ) ) (- 39))) (not (< (+ (* 12 x1 ) (* (- 34) x2 ) (* (- 6) x2 ) (* (- 11) x1 ) ) 14)) )) +(assert (or (<= (+ (* (- 4) x0 ) (* (- 42) x2 ) (* (- 22) x0 ) ) 15) (not (= (+ (* (- 24) x0 ) (* (- 4) x2 ) ) (- 18))) (>= (+ (* 43 x2 ) (* (- 47) x1 ) (* 22 x0 ) (* 4 x1 ) ) (- 33)) )) +(assert (or (not (<= (+ (* (- 10) x0 ) (* (- 4) x0 ) (* 40 x0 ) ) 47)) (not (= (+ (* 8 x0 ) (* (- 35) x0 ) ) 6)) (not (< (+ (* 13 x1 ) (* (- 1) x2 ) (* 16 x2 ) (* 6 x1 ) ) (- 43))) )) +(assert (or (<= (+ (* 35 x2 ) (* 39 x0 ) (* 25 x1 ) (* 46 x0 ) ) 9) (= (+ (* (- 40) x2 ) (* (- 2) x2 ) (* 17 x2 ) (* (- 48) x1 ) ) 18) )) +(assert (or (> (+ (* (- 47) x2 ) (* (- 24) x2 ) (* (- 25) x0 ) ) 13) (= (+ (* (- 41) x2 ) (* (- 3) x0 ) (* (- 6) x2 ) ) (- 13)) )) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (= (+ (* (- 7) x2 ) (* 6 x0 ) ) (- 1)) ) +(assert (or (> (+ (* 21 x0 ) (* (- 48) x0 ) (* (- 39) x0 ) (* (- 3) x2 ) ) (- 48)) (< (+ (* 12 x2 ) (* 26 x1 ) (* 40 x2 ) ) (- 10)) )) +(check-sat) +(push 1) +(assert (or (= (+ (* (- 23) x2 ) (* 31 x2 ) ) 23) (< (+ (* 26 x0 ) (* 45 x0 ) (* (- 17) x1 ) (* (- 38) x2 ) ) (- 31)) (not (>= (+ (* 21 x1 ) (* (- 12) x2 ) ) (- 38))) )) +(check-sat) +(push 1) +(assert (not (<= (+ (* 26 x1 ) (* (- 40) x1 ) (* 22 x0 ) ) 8)) ) +(assert (or (not (>= (+ (* 20 x0 ) (* 0 x0 ) (* 29 x1 ) ) (- 14))) (< (+ (* 12 x1 ) (* (- 25) x2 ) ) (- 50)) )) +(check-sat) +(pop 1) +(assert (or (= (+ (* 37 x1 ) (* (- 10) x1 ) (* (- 50) x1 ) (* (- 15) x1 ) ) 21) (not (< (+ (* (- 27) x0 ) (* 4 x0 ) ) (- 8))) )) +(assert (or (= (+ (* 0 x1 ) (* (- 43) x0 ) (* 32 x1 ) (* 16 x0 ) ) 11) (not (> (+ (* 20 x2 ) (* (- 11) x2 ) (* (- 14) x0 ) ) (- 43))) (= (+ (* 30 x1 ) (* (- 18) x2 ) (* 0 x1 ) (* (- 32) x0 ) ) (- 5)) )) +(assert (> (+ (* 43 x2 ) (* (- 3) x0 ) ) 4) ) +(assert (> (+ (* 44 x0 ) (* 4 x2 ) ) (- 41)) ) +(check-sat) +(pop 1) +(assert (or (< (+ (* 17 x0 ) (* 11 x0 ) (* 45 x1 ) ) (- 38)) (> (+ (* 49 x1 ) (* (- 9) x2 ) (* 7 x2 ) (* 3 x2 ) ) (- 20)) (not (< (+ (* 10 x2 ) (* 31 x0 ) ) (- 38))) )) +(assert (not (>= (+ (* (- 43) x2 ) (* (- 8) x1 ) (* (- 8) x0 ) ) 34)) ) +(assert (not (>= (+ (* (- 42) x1 ) (* (- 40) x0 ) (* (- 22) x0 ) (* (- 37) x2 ) ) 21)) ) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2 new file mode 100644 index 000000000..ff78a7d39 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2 @@ -0,0 +1,49 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (or (<= (+ (* 49 x2 ) (* 24 x0 ) (* (- 41) x0 ) ) 40) (not (>= (+ (* 9 x2 ) (* 2 x1 ) (* 48 x1 ) (* 6 x2 ) ) 48)) )) +(assert (or (not (= (+ (* (- 2) x0 ) (* 22 x0 ) (* (- 37) x0 ) ) 29)) (not (= (+ (* (- 27) x1 ) (* (- 47) x0 ) ) 39)) )) +(assert (or (not (>= (+ (* (- 5) x2 ) (* (- 39) x0 ) (* (- 28) x2 ) ) 47)) (not (= (+ (* (- 25) x2 ) (* (- 1) x0 ) (* (- 26) x2 ) ) (- 35))) (not (<= (+ (* (- 26) x1 ) (* (- 31) x0 ) ) (- 22))) )) +(assert (or (> (+ (* 27 x1 ) (* (- 38) x0 ) (* 43 x2 ) (* (- 13) x0 ) ) 41) (>= (+ (* 34 x2 ) (* 1 x2 ) (* (- 20) x1 ) (* 21 x1 ) ) (- 40)) )) +(assert (> (+ (* (- 28) x1 ) (* 48 x1 ) (* (- 24) x1 ) (* 7 x1 ) ) 41) ) +(check-sat) +(push 1) +(assert (<= (+ (* (- 42) x1 ) (* 25 x0 ) (* (- 47) x2 ) (* 4 x0 ) ) (- 15)) ) +(check-sat) +(push 1) +(assert (or (not (= (+ (* (- 15) x0 ) (* (- 4) x1 ) (* (- 4) x1 ) ) 24)) (not (< (+ (* (- 35) x0 ) (* (- 45) x1 ) (* (- 8) x2 ) (* 19 x2 ) ) 19)) )) +(assert (or (not (< (+ (* (- 39) x1 ) (* 15 x0 ) (* 37 x0 ) ) (- 7))) (<= (+ (* 24 x0 ) (* 20 x0 ) (* 43 x1 ) ) 13) )) +(assert (or (< (+ (* 19 x1 ) (* (- 25) x1 ) ) 8) (> (+ (* 44 x0 ) (* (- 41) x0 ) ) 9) (>= (+ (* 20 x0 ) (* 10 x2 ) (* 23 x0 ) ) 32) )) +(assert (or (>= (+ (* (- 12) x0 ) (* 17 x2 ) ) (- 43)) (not (> (+ (* 25 x1 ) (* (- 38) x2 ) (* (- 10) x0 ) ) 24)) )) +(assert (or (not (< (+ (* (- 50) x2 ) (* 43 x0 ) (* (- 37) x2 ) (* (- 5) x0 ) ) (- 40))) (= (+ (* (- 16) x2 ) (* 6 x2 ) ) (- 11)) (> (+ (* 48 x0 ) (* 29 x1 ) ) 40) )) +(check-sat) +(push 1) +(assert (or (< (+ (* 1 x1 ) (* (- 24) x0 ) (* (- 2) x1 ) ) 21) (not (> (+ (* (- 42) x0 ) (* 40 x0 ) ) (- 33))) )) +(assert (or (not (> (+ (* 23 x0 ) (* (- 14) x2 ) (* (- 23) x0 ) (* (- 37) x0 ) ) 25)) (not (<= (+ (* 12 x2 ) (* 24 x1 ) (* (- 25) x0 ) ) 3)) )) +(check-sat) +(pop 1) +(assert (<= (+ (* 19 x0 ) (* 23 x0 ) (* (- 9) x1 ) (* (- 31) x1 ) ) 27) ) +(assert (or (> (+ (* 33 x1 ) (* (- 24) x1 ) (* (- 48) x2 ) (* (- 42) x1 ) ) 30) (not (<= (+ (* (- 36) x1 ) (* 5 x1 ) ) (- 36))) )) +(assert (or (not (>= (+ (* 20 x1 ) (* 29 x1 ) (* 48 x2 ) ) 40)) (not (> (+ (* (- 26) x2 ) (* 23 x1 ) (* (- 14) x0 ) ) 32)) )) +(assert (>= (+ (* 31 x2 ) (* 43 x1 ) ) 28) ) +(assert (or (= (+ (* 21 x2 ) (* (- 30) x1 ) (* 28 x1 ) (* 43 x0 ) ) 39) (not (<= (+ (* (- 3) x0 ) (* (- 49) x0 ) (* 9 x0 ) (* 24 x2 ) ) 14)) (not (> (+ (* 35 x1 ) (* (- 6) x2 ) (* 37 x0 ) ) 3)) )) +(assert (or (not (<= (+ (* 46 x0 ) (* 11 x1 ) ) 40)) (not (= (+ (* 3 x1 ) (* 49 x1 ) ) (- 38))) )) +(assert (not (<= (+ (* (- 39) x2 ) (* 23 x1 ) ) 5)) ) +(assert (or (not (< (+ (* 44 x1 ) (* (- 23) x1 ) (* 26 x1 ) ) 39)) (> (+ (* 14 x2 ) (* 2 x2 ) (* (- 5) x2 ) ) (- 22)) )) +(assert (not (<= (+ (* (- 15) x2 ) (* 17 x2 ) (* 19 x1 ) ) 30)) ) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2 new file mode 100644 index 000000000..01191c4da --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (or (> (+ (* (- 34) x2 ) (* 33 x1 ) (* (- 6) x1 ) (* (- 44) x1 ) ) (- 40)) (not (= (+ (* 7 x0 ) (* (- 27) x2 ) (* 10 x0 ) (* (- 42) x1 ) ) 7)) )) +(assert (or (< (+ (* (- 39) x1 ) (* 32 x1 ) (* 42 x1 ) (* 18 x1 ) ) 26) (not (= (+ (* (- 23) x2 ) (* 17 x1 ) ) (- 39))) )) +(assert (or (>= (+ (* (- 45) x0 ) (* (- 40) x1 ) (* (- 29) x0 ) (* (- 2) x0 ) ) 22) (not (>= (+ (* 11 x1 ) (* (- 42) x1 ) (* (- 21) x0 ) ) 41)) (not (= (+ (* 30 x2 ) (* (- 13) x2 ) (* 21 x1 ) (* (- 16) x2 ) ) 36)) )) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (or (= (+ (* 20 x2 ) (* 13 x2 ) (* (- 10) x0 ) ) (- 34)) (> (+ (* 23 x1 ) (* 10 x1 ) ) 49) (not (< (+ (* 28 x0 ) (* 22 x2 ) (* 6 x2 ) ) 13)) )) +(assert (or (not (< (+ (* (- 37) x2 ) (* (- 22) x1 ) (* 6 x1 ) ) 18)) (= (+ (* (- 20) x1 ) (* 32 x2 ) (* 16 x1 ) ) (- 49)) )) +(assert (or (>= (+ (* (- 2) x2 ) (* (- 23) x1 ) (* 39 x2 ) (* 35 x2 ) ) (- 8)) (not (<= (+ (* (- 19) x2 ) (* (- 43) x2 ) (* 22 x1 ) (* (- 27) x1 ) ) (- 48))) (not (= (+ (* (- 44) x1 ) (* 39 x1 ) (* 28 x2 ) ) (- 35))) )) +(assert (or (not (<= (+ (* (- 47) x1 ) (* (- 22) x2 ) (* 43 x2 ) ) (- 5))) (not (>= (+ (* (- 45) x2 ) (* (- 35) x2 ) (* 44 x0 ) ) (- 14))) )) +(assert (or (not (>= (+ (* (- 7) x1 ) (* (- 24) x2 ) (* 49 x1 ) ) (- 27))) (< (+ (* 48 x1 ) (* 19 x0 ) ) (- 6)) (not (< (+ (* 39 x0 ) (* 48 x1 ) ) 7)) )) +(assert (or (<= (+ (* (- 11) x2 ) (* 29 x0 ) ) (- 16)) (not (< (+ (* 31 x1 ) (* 5 x2 ) ) 44)) (>= (+ (* 0 x1 ) (* 42 x2 ) (* 27 x1 ) ) (- 17)) )) +(assert (not (< (+ (* 49 x1 ) (* 1 x0 ) ) 40)) ) +(check-sat) +(push 1) +(check-sat) +(push 1) +(assert (or (not (<= (+ (* 40 x2 ) (* (- 42) x1 ) (* 1 x0 ) (* 0 x0 ) ) 24)) (not (> (+ (* (- 27) x0 ) (* 46 x1 ) (* (- 48) x0 ) (* 29 x0 ) ) 11)) )) +(check-sat) +(pop 1) +(assert (not (< (+ (* 16 x1 ) (* (- 26) x0 ) (* (- 6) x0 ) ) 34)) ) +(check-sat) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2 new file mode 100644 index 000000000..e4b824dcc --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2 @@ -0,0 +1,36 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (not (<= (+ (* (- 3) x0 ) (* 38 x0 ) (* 34 x1 ) ) (- 5))) ) +(assert (or (not (> (+ (* (- 27) x0 ) (* 26 x1 ) ) (- 50))) (not (>= (+ (* 32 x0 ) (* 10 x0 ) (* (- 43) x1 ) (* (- 39) x0 ) ) (- 36))) )) +(check-sat) +(push 1) +(assert (> (+ (* (- 23) x2 ) (* 49 x2 ) ) 14) ) +(assert (not (= (+ (* 20 x1 ) (* (- 38) x2 ) ) 33)) ) +(assert (not (<= (+ (* 30 x0 ) (* (- 13) x1 ) (* 21 x1 ) ) 20)) ) +(assert (or (<= (+ (* 48 x0 ) (* (- 42) x0 ) (* 34 x1 ) (* 47 x1 ) ) 12) (not (>= (+ (* 0 x1 ) (* (- 1) x1 ) (* (- 19) x1 ) ) 40)) (not (>= (+ (* (- 40) x2 ) (* 3 x2 ) (* 4 x0 ) (* 19 x2 ) ) 34)) )) +(assert (or (= (+ (* (- 7) x1 ) (* 15 x0 ) (* (- 12) x0 ) ) 6) (not (<= (+ (* (- 41) x2 ) (* 10 x0 ) (* 12 x2 ) ) 49)) )) +(assert (or (<= (+ (* 12 x2 ) (* (- 50) x1 ) ) (- 25)) (= (+ (* (- 29) x2 ) (* (- 11) x2 ) (* (- 8) x2 ) (* (- 3) x2 ) ) (- 39)) )) +(assert (or (= (+ (* 33 x2 ) (* 44 x0 ) (* (- 4) x1 ) ) 5) (not (< (+ (* 27 x2 ) (* (- 45) x0 ) (* 43 x2 ) (* 40 x0 ) ) 17)) (not (<= (+ (* (- 40) x2 ) (* 3 x0 ) (* 16 x2 ) (* (- 37) x1 ) ) 29)) )) +(check-sat) +(push 1) +(check-sat) +(push 1) +(check-sat) +(push 1) +(assert (or (= (+ (* (- 21) x0 ) (* 5 x2 ) ) (- 27)) (not (<= (+ (* (- 20) x0 ) (* 19 x0 ) (* (- 50) x1 ) (* (- 24) x0 ) ) (- 32))) )) +(check-sat) +(pop 1) +(assert (not (<= (+ (* 9 x2 ) (* 0 x0 ) (* (- 40) x0 ) (* 49 x2 ) ) (- 11))) ) +(assert (or (not (< (+ (* (- 2) x0 ) (* 2 x2 ) ) 19)) (= (+ (* (- 28) x1 ) (* (- 1) x2 ) (* (- 4) x1 ) ) 38) )) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2 new file mode 100644 index 000000000..3003fa52b --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (or (not (>= (+ (* 47 x0 ) (* (- 1) x2 ) (* 13 x2 ) ) (- 9))) (not (< (+ (* 23 x1 ) (* (- 50) x0 ) (* 35 x1 ) (* 12 x2 ) ) 14)) )) +(assert (or (not (<= (+ (* 3 x0 ) (* (- 15) x2 ) (* 34 x0 ) ) (- 39))) (not (> (+ (* (- 35) x0 ) (* 36 x2 ) (* (- 3) x1 ) ) 22)) (not (> (+ (* 46 x2 ) (* 2 x2 ) (* (- 33) x1 ) (* (- 24) x0 ) ) (- 39))) )) +(assert (or (<= (+ (* 27 x1 ) (* 18 x2 ) (* (- 3) x2 ) ) (- 2)) (= (+ (* 27 x0 ) (* (- 26) x2 ) (* 15 x2 ) (* 23 x0 ) ) 11) )) +(assert (or (= (+ (* 23 x1 ) (* (- 1) x1 ) (* (- 3) x2 ) (* 49 x1 ) ) (- 26)) (not (> (+ (* (- 30) x0 ) (* (- 1) x0 ) (* 15 x1 ) ) (- 23))) )) +(check-sat) +(push 1) +(assert (or (not (= (+ (* 24 x1 ) (* 5 x2 ) (* (- 18) x1 ) (* (- 40) x2 ) ) (- 6))) (not (< (+ (* 6 x0 ) (* (- 29) x0 ) (* 16 x2 ) ) (- 42))) )) +(assert (or (= (+ (* (- 33) x0 ) (* 40 x0 ) (* (- 28) x1 ) (* (- 29) x0 ) ) (- 1)) (<= (+ (* (- 17) x1 ) (* 0 x0 ) (* 2 x1 ) ) (- 8)) (not (= (+ (* 39 x2 ) (* 4 x0 ) (* 12 x1 ) (* (- 1) x2 ) ) (- 40))) )) +(check-sat) +(push 1) +(assert (not (<= (+ (* 24 x2 ) (* 9 x2 ) (* 38 x0 ) (* 9 x2 ) ) (- 12))) ) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(check-sat) +(push 1) +(assert (not (> (+ (* (- 33) x1 ) (* 1 x0 ) (* (- 27) x1 ) (* (- 39) x1 ) ) 30)) ) +(check-sat) +(pop 1) +(assert (not (>= (+ (* (- 36) x1 ) (* 34 x0 ) (* 39 x0 ) (* 2 x2 ) ) 16)) ) +(check-sat) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2 new file mode 100644 index 000000000..c437a5fb8 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2 @@ -0,0 +1,28 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (or (= (+ (* (- 47) x1 ) (* 42 x2 ) ) (- 13)) (< (+ (* 5 x2 ) (* 8 x2 ) ) 41) (not (= (+ (* (- 20) x2 ) (* (- 3) x2 ) (* 38 x1 ) (* (- 38) x0 ) ) (- 30))) )) +(assert (or (= (+ (* (- 23) x2 ) (* 29 x2 ) ) (- 30)) (not (>= (+ (* 46 x1 ) (* (- 49) x0 ) (* (- 17) x0 ) (* 17 x0 ) ) 2)) (not (<= (+ (* (- 32) x0 ) (* 23 x0 ) (* (- 5) x1 ) (* (- 50) x2 ) ) (- 46))) )) +(check-sat) +(push 1) +(assert (or (not (<= (+ (* 36 x2 ) (* 21 x2 ) ) (- 31))) (not (= (+ (* 48 x2 ) (* (- 2) x1 ) (* 32 x0 ) ) 48)) (> (+ (* (- 43) x0 ) (* 7 x2 ) (* 1 x1 ) (* 2 x1 ) ) 15) )) +(assert (or (not (<= (+ (* (- 27) x1 ) (* 4 x0 ) (* 43 x2 ) ) (- 23))) (not (> (+ (* (- 4) x1 ) (* 31 x2 ) (* 22 x2 ) ) 0)) )) +(assert (or (not (<= (+ (* 19 x0 ) (* (- 29) x0 ) (* 18 x2 ) (* 6 x0 ) ) 24)) (>= (+ (* 32 x2 ) (* 36 x1 ) (* 41 x1 ) ) 44) )) +(assert (> (+ (* 30 x0 ) (* (- 9) x2 ) (* (- 22) x0 ) ) 38) ) +(assert (or (>= (+ (* (- 19) x0 ) (* 32 x2 ) (* (- 48) x2 ) ) (- 14)) (>= (+ (* (- 49) x2 ) (* 29 x2 ) (* 15 x1 ) ) (- 34)) )) +(assert (or (not (< (+ (* (- 6) x0 ) (* (- 43) x1 ) ) 35)) (= (+ (* (- 48) x2 ) (* (- 31) x0 ) ) 34) (not (< (+ (* (- 41) x0 ) (* 45 x2 ) (* (- 17) x1 ) (* (- 38) x2 ) ) 1)) )) +(assert (or (not (<= (+ (* (- 10) x2 ) (* 45 x1 ) ) 49)) (not (<= (+ (* 38 x2 ) (* 17 x2 ) (* (- 18) x1 ) (* (- 17) x1 ) ) 3)) )) +(assert (not (= (+ (* 20 x1 ) (* (- 3) x2 ) (* 15 x1 ) ) (- 11))) ) +(check-sat) +(push 1) +(assert (not (<= (+ (* (- 24) x1 ) (* 47 x2 ) (* (- 32) x2 ) ) (- 34))) ) +(check-sat) +(pop 1) +(check-sat) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2 new file mode 100644 index 000000000..4d42615f4 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2 @@ -0,0 +1,36 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (or (< (+ (* (- 15) x0 ) (* (- 4) x0 ) (* (- 33) x2 ) ) (- 21)) (<= (+ (* (- 2) x1 ) (* 12 x1 ) (* 48 x1 ) ) (- 21)) (> (+ (* 43 x2 ) (* (- 6) x2 ) ) (- 26)) )) +(assert (not (<= (+ (* (- 9) x2 ) (* 28 x0 ) (* (- 26) x0 ) ) (- 2))) ) +(assert (or (= (+ (* (- 43) x0 ) (* 49 x1 ) (* (- 49) x0 ) ) 25) (not (= (+ (* 39 x0 ) (* (- 23) x2 ) ) (- 12))) )) +(assert (or (not (<= (+ (* 13 x1 ) (* (- 17) x1 ) (* (- 27) x0 ) (* (- 24) x0 ) ) (- 47))) (not (<= (+ (* 5 x1 ) (* (- 31) x1 ) (* (- 40) x2 ) ) 28)) )) +(assert (or (not (< (+ (* (- 7) x2 ) (* (- 24) x0 ) (* 42 x0 ) ) (- 27))) (not (< (+ (* (- 4) x2 ) (* (- 16) x0 ) (* (- 20) x2 ) ) (- 14))) (not (<= (+ (* 2 x2 ) (* 26 x1 ) ) 12)) )) +(assert (< (+ (* (- 9) x0 ) (* 45 x1 ) (* (- 12) x2 ) ) 37) ) +(assert (or (= (+ (* 23 x2 ) (* 15 x1 ) (* 32 x1 ) (* (- 30) x2 ) ) 30) (>= (+ (* 36 x1 ) (* (- 36) x0 ) (* (- 22) x2 ) (* 36 x1 ) ) 20) )) +(assert (or (not (< (+ (* (- 22) x2 ) (* 34 x0 ) ) (- 10))) (not (>= (+ (* (- 38) x2 ) (* (- 46) x2 ) ) 34)) (not (>= (+ (* 24 x0 ) (* (- 48) x1 ) (* 7 x0 ) ) (- 19))) )) +(assert (<= (+ (* (- 49) x2 ) (* (- 18) x0 ) (* 17 x0 ) ) 18) ) +(assert (or (not (<= (+ (* (- 16) x2 ) (* 24 x1 ) (* (- 38) x2 ) ) 33)) (<= (+ (* 29 x2 ) (* (- 22) x1 ) ) (- 19)) )) +(assert (or (< (+ (* 19 x1 ) (* (- 30) x0 ) ) 39) (= (+ (* (- 47) x0 ) (* 46 x1 ) (* 37 x0 ) ) (- 28)) (not (= (+ (* (- 12) x0 ) (* 19 x0 ) ) 19)) )) +(assert (or (not (> (+ (* 35 x1 ) (* 35 x0 ) (* 17 x1 ) (* 46 x2 ) ) 46)) (not (>= (+ (* (- 8) x0 ) (* 43 x1 ) (* (- 26) x2 ) ) 21)) (not (< (+ (* (- 29) x1 ) (* (- 10) x2 ) (* (- 35) x1 ) ) 42)) )) +(check-sat) +(push 1) +(assert (or (>= (+ (* 21 x2 ) (* (- 38) x1 ) (* (- 21) x2 ) ) 28) (= (+ (* 28 x1 ) (* 2 x1 ) (* (- 16) x2 ) (* 47 x0 ) ) (- 45)) )) +(assert (not (= (+ (* 33 x0 ) (* 26 x0 ) (* 33 x1 ) (* (- 41) x2 ) ) 4)) ) +(assert (or (= (+ (* 40 x1 ) (* (- 23) x1 ) (* 27 x0 ) ) (- 19)) (>= (+ (* (- 29) x0 ) (* (- 12) x0 ) (* 42 x0 ) ) (- 30)) )) +(assert (or (not (<= (+ (* 35 x0 ) (* 40 x2 ) (* (- 46) x0 ) ) (- 35))) (>= (+ (* 34 x0 ) (* 33 x0 ) (* 27 x0 ) (* (- 21) x1 ) ) (- 4)) )) +(assert (not (<= (+ (* 42 x1 ) (* (- 4) x1 ) (* (- 30) x0 ) (* (- 23) x0 ) ) (- 44))) ) +(check-sat) +(pop 1) +(check-sat) +(push 1) +(assert (not (>= (+ (* 3 x1 ) (* 41 x2 ) (* (- 28) x1 ) ) (- 49))) ) +(assert (or (not (<= (+ (* (- 29) x1 ) (* (- 5) x2 ) (* 15 x2 ) (* (- 26) x1 ) ) (- 14))) (>= (+ (* (- 47) x1 ) (* (- 31) x1 ) ) 46) )) +(check-sat) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2 new file mode 100644 index 000000000..a566eb1f3 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2 @@ -0,0 +1,38 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (< (+ (* 23 x1 ) (* (- 27) x1 ) (* 22 x0 ) ) (- 22)) ) +(assert (>= (+ (* (- 4) x0 ) (* (- 9) x1 ) (* (- 40) x0 ) (* 40 x2 ) ) (- 27)) ) +(assert (or (not (>= (+ (* (- 34) x0 ) (* (- 36) x1 ) ) (- 26))) (not (>= (+ (* 6 x2 ) (* (- 6) x1 ) ) (- 43))) )) +(assert (or (>= (+ (* 20 x2 ) (* 12 x0 ) (* (- 50) x1 ) ) (- 46)) (not (> (+ (* 11 x1 ) (* (- 30) x0 ) ) (- 21))) )) +(check-sat) +(push 1) +(assert (or (not (>= (+ (* (- 17) x2 ) (* 25 x1 ) (* 43 x0 ) (* (- 9) x0 ) ) (- 19))) (> (+ (* 4 x1 ) (* (- 22) x1 ) ) 8) (> (+ (* 19 x1 ) (* (- 1) x1 ) (* (- 22) x1 ) (* (- 47) x2 ) ) 46) )) +(assert (or (> (+ (* (- 12) x1 ) (* 25 x1 ) ) (- 18)) (not (= (+ (* (- 47) x0 ) (* (- 13) x2 ) (* (- 13) x1 ) (* (- 10) x0 ) ) (- 27))) )) +(check-sat) +(pop 1) +(check-sat) +(push 1) +(assert (or (not (>= (+ (* 9 x2 ) (* (- 18) x1 ) (* (- 7) x0 ) (* (- 2) x2 ) ) (- 40))) (< (+ (* 2 x1 ) (* (- 4) x1 ) (* (- 48) x2 ) ) 32) )) +(check-sat) +(push 1) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (not (<= (+ (* (- 10) x2 ) (* (- 20) x1 ) (* 9 x2 ) ) 23)) ) +(check-sat) +(pop 1) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2 new file mode 100644 index 000000000..7fcd67745 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2 @@ -0,0 +1,37 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (or (= (+ (* 40 x1 ) (* (- 35) x0 ) (* 10 x1 ) ) 4) (not (= (+ (* 38 x1 ) (* 40 x1 ) (* (- 28) x2 ) ) 44)) (< (+ (* (- 46) x1 ) (* (- 18) x0 ) ) 37) )) +(assert (or (<= (+ (* (- 4) x2 ) (* (- 29) x1 ) ) (- 37)) (not (> (+ (* (- 10) x2 ) (* 13 x0 ) ) (- 21))) )) +(check-sat) +(push 1) +(assert (or (> (+ (* 21 x0 ) (* 13 x2 ) ) 49) (>= (+ (* 19 x2 ) (* 45 x2 ) (* 9 x1 ) ) (- 45)) )) +(assert (or (= (+ (* (- 17) x0 ) (* 22 x0 ) ) 12) (<= (+ (* 28 x1 ) (* 27 x0 ) (* 39 x0 ) (* (- 49) x2 ) ) (- 9)) )) +(assert (or (not (<= (+ (* (- 49) x2 ) (* (- 28) x1 ) (* 24 x2 ) ) 47)) (>= (+ (* 13 x2 ) (* 49 x0 ) (* (- 45) x0 ) (* (- 44) x1 ) ) (- 14)) )) +(assert (or (> (+ (* 9 x1 ) (* 18 x2 ) ) 31) (not (<= (+ (* 10 x2 ) (* 49 x1 ) (* (- 29) x2 ) (* (- 45) x2 ) ) (- 22))) )) +(assert (not (<= (+ (* 49 x0 ) (* (- 50) x0 ) (* 0 x1 ) ) 40)) ) +(assert (or (> (+ (* 37 x1 ) (* (- 37) x2 ) ) (- 13)) (not (< (+ (* (- 38) x2 ) (* (- 15) x2 ) (* (- 39) x2 ) (* (- 13) x1 ) ) 20)) (>= (+ (* 8 x2 ) (* 47 x1 ) (* (- 21) x2 ) (* 41 x0 ) ) 13) )) +(assert (or (> (+ (* (- 26) x2 ) (* 9 x0 ) (* (- 47) x1 ) (* (- 30) x0 ) ) (- 12)) (not (>= (+ (* 3 x0 ) (* 24 x0 ) ) (- 10))) )) +(check-sat) +(push 1) +(assert (or (= (+ (* (- 27) x1 ) (* 34 x2 ) (* (- 14) x2 ) (* (- 24) x1 ) ) (- 38)) (<= (+ (* (- 41) x2 ) (* 36 x1 ) (* (- 44) x2 ) (* (- 19) x2 ) ) 9) )) +(assert (or (not (<= (+ (* (- 2) x1 ) (* (- 7) x1 ) ) 45)) (<= (+ (* (- 39) x0 ) (* (- 18) x2 ) ) (- 13)) )) +(assert (or (= (+ (* (- 32) x2 ) (* 37 x2 ) ) (- 26)) (< (+ (* 26 x0 ) (* 4 x1 ) ) (- 32)) )) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (or (< (+ (* (- 23) x2 ) (* (- 14) x2 ) (* 3 x1 ) ) (- 39)) (not (> (+ (* 48 x1 ) (* 14 x0 ) ) (- 32))) (>= (+ (* (- 10) x0 ) (* (- 46) x0 ) ) 12) )) +(check-sat) +(pop 1) +(assert (< (+ (* (- 41) x1 ) (* (- 42) x1 ) (* 41 x1 ) ) (- 36)) ) +(check-sat) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2 new file mode 100644 index 000000000..88fd866de --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2 @@ -0,0 +1,37 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(check-sat) +(push 1) +(assert (or (not (>= (+ (* 25 x1 ) (* (- 37) x2 ) (* (- 48) x1 ) ) (- 37))) (not (<= (+ (* (- 6) x1 ) (* 0 x2 ) (* 22 x1 ) ) (- 25))) )) +(assert (or (not (> (+ (* 25 x2 ) (* (- 14) x1 ) ) (- 40))) (not (> (+ (* (- 44) x1 ) (* (- 5) x0 ) ) (- 31))) )) +(assert (or (< (+ (* (- 31) x2 ) (* (- 42) x1 ) (* (- 7) x0 ) (* (- 4) x2 ) ) 18) (<= (+ (* 8 x1 ) (* (- 46) x2 ) ) (- 4)) )) +(check-sat) +(push 1) +(assert (or (> (+ (* (- 45) x1 ) (* 45 x0 ) (* (- 12) x0 ) (* (- 24) x2 ) ) (- 41)) (< (+ (* 17 x2 ) (* 38 x0 ) (* 16 x2 ) ) 40) )) +(assert (or (< (+ (* 14 x2 ) (* 45 x0 ) (* (- 13) x0 ) (* (- 40) x0 ) ) 44) (= (+ (* (- 28) x1 ) (* (- 34) x1 ) (* (- 1) x0 ) ) 49) )) +(assert (or (>= (+ (* 2 x0 ) (* 21 x2 ) ) 21) (< (+ (* (- 5) x2 ) (* 41 x1 ) (* (- 16) x1 ) ) 3) )) +(assert (= (+ (* (- 17) x2 ) (* 34 x1 ) (* (- 20) x0 ) (* (- 47) x2 ) ) (- 39)) ) +(check-sat) +(push 1) +(assert (or (< (+ (* 26 x2 ) (* (- 29) x2 ) (* 3 x2 ) (* (- 42) x0 ) ) (- 10)) (not (<= (+ (* 9 x0 ) (* (- 31) x1 ) ) (- 6))) )) +(assert (or (not (< (+ (* (- 15) x0 ) (* (- 44) x1 ) (* (- 5) x2 ) (* 25 x2 ) ) 38)) (= (+ (* (- 24) x1 ) (* 20 x0 ) (* 8 x0 ) ) (- 10)) (not (> (+ (* (- 35) x1 ) (* (- 14) x2 ) ) 6)) )) +(assert (or (> (+ (* (- 13) x0 ) (* 10 x2 ) ) (- 16)) (= (+ (* 38 x0 ) (* 38 x2 ) (* 3 x0 ) ) 8) (not (<= (+ (* 18 x1 ) (* (- 26) x0 ) ) (- 14))) )) +(check-sat) +(push 1) +(assert (or (< (+ (* (- 11) x1 ) (* 42 x1 ) ) (- 50)) (not (> (+ (* (- 24) x0 ) (* 8 x1 ) (* 44 x2 ) (* 27 x0 ) ) 48)) (< (+ (* 2 x0 ) (* 32 x2 ) ) (- 30)) )) +(assert (>= (+ (* 28 x2 ) (* 29 x1 ) (* (- 7) x2 ) (* 16 x0 ) ) (- 19)) ) +(check-sat) +(pop 1) +(assert (or (not (> (+ (* 1 x1 ) (* (- 33) x1 ) (* (- 2) x1 ) ) (- 29))) (>= (+ (* 7 x2 ) (* 4 x0 ) (* 49 x2 ) ) (- 17)) )) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2 new file mode 100644 index 000000000..329be0391 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2 @@ -0,0 +1,48 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (or (not (> (+ (* (- 25) x0 ) (* 16 x2 ) ) 21)) (>= (+ (* 18 x1 ) (* (- 35) x0 ) (* 18 x0 ) (* 24 x0 ) ) (- 50)) )) +(assert (> (+ (* (- 40) x0 ) (* 29 x2 ) ) 9) ) +(check-sat) +(push 1) +(assert (or (not (> (+ (* 32 x1 ) (* (- 23) x0 ) (* 46 x2 ) ) 11)) (not (< (+ (* (- 12) x0 ) (* (- 40) x0 ) (* 43 x2 ) (* (- 13) x1 ) ) 49)) )) +(assert (not (>= (+ (* (- 47) x0 ) (* 24 x1 ) ) 32)) ) +(check-sat) +(pop 1) +(assert (or (= (+ (* 8 x0 ) (* 31 x1 ) (* 38 x1 ) ) (- 31)) (<= (+ (* (- 16) x1 ) (* (- 22) x2 ) (* 27 x2 ) (* (- 23) x0 ) ) (- 12)) )) +(assert (or (not (>= (+ (* 43 x1 ) (* (- 29) x1 ) (* 32 x0 ) (* (- 29) x1 ) ) (- 10))) (>= (+ (* 24 x0 ) (* (- 31) x1 ) ) 34) )) +(assert (or (not (>= (+ (* (- 39) x2 ) (* (- 48) x2 ) (* (- 46) x0 ) (* 2 x1 ) ) 19)) (not (<= (+ (* (- 44) x0 ) (* (- 36) x2 ) ) (- 23))) )) +(check-sat) +(push 1) +(assert (not (<= (+ (* 37 x1 ) (* 19 x2 ) (* 24 x1 ) (* (- 15) x0 ) ) (- 12))) ) +(assert (or (>= (+ (* (- 24) x0 ) (* (- 29) x0 ) (* 40 x2 ) ) (- 39)) (not (<= (+ (* (- 41) x0 ) (* 40 x2 ) (* 41 x1 ) (* (- 3) x0 ) ) 28)) )) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (or (not (> (+ (* 38 x0 ) (* (- 47) x0 ) (* 19 x0 ) (* 40 x2 ) ) (- 39))) (not (< (+ (* 30 x2 ) (* 39 x1 ) ) (- 28))) )) +(assert (or (>= (+ (* (- 12) x0 ) (* (- 26) x1 ) (* (- 13) x1 ) ) 28) (> (+ (* (- 10) x0 ) (* (- 32) x1 ) ) 12) )) +(check-sat) +(push 1) +(assert (< (+ (* (- 33) x2 ) (* (- 13) x0 ) ) 42) ) +(assert (or (not (= (+ (* 17 x2 ) (* 4 x2 ) ) 7)) (<= (+ (* 19 x1 ) (* 22 x1 ) (* 19 x1 ) ) 26) (not (<= (+ (* 9 x2 ) (* 0 x0 ) (* 24 x2 ) ) (- 10))) )) +(assert (< (+ (* 45 x1 ) (* (- 38) x0 ) (* 19 x2 ) (* 17 x1 ) ) (- 14)) ) +(check-sat) +(pop 1) +(assert (not (< (+ (* 10 x0 ) (* (- 31) x2 ) (* (- 21) x0 ) ) (- 29))) ) +(check-sat) +(pop 1) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2 new file mode 100644 index 000000000..db180f3f4 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2 @@ -0,0 +1,53 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(assert (or (not (>= (+ (* (- 32) x2 ) (* (- 10) x0 ) (* (- 33) x0 ) (* 16 x1 ) ) (- 35))) (< (+ (* (- 46) x1 ) (* 44 x1 ) (* (- 15) x1 ) (* (- 22) x2 ) ) (- 20)) )) +(check-sat) +(push 1) +(assert (or (not (< (+ (* (- 1) x2 ) (* (- 26) x0 ) ) 32)) (> (+ (* 39 x1 ) (* 31 x1 ) (* (- 16) x0 ) ) 27) )) +(check-sat) +(pop 1) +(assert (or (> (+ (* 46 x1 ) (* 48 x1 ) (* 26 x0 ) ) 12) (= (+ (* 30 x1 ) (* 1 x0 ) (* 8 x2 ) (* 11 x2 ) ) (- 3)) )) +(assert (<= (+ (* (- 11) x1 ) (* (- 27) x2 ) (* (- 29) x2 ) (* 23 x1 ) ) 19) ) +(assert (not (> (+ (* 15 x0 ) (* 25 x1 ) ) 47)) ) +(assert (<= (+ (* (- 3) x2 ) (* 1 x1 ) (* 36 x1 ) ) (- 27)) ) +(check-sat) +(push 1) +(assert (not (<= (+ (* (- 3) x0 ) (* (- 33) x2 ) (* 7 x2 ) (* (- 37) x0 ) ) 13)) ) +(check-sat) +(pop 1) +(assert (or (not (> (+ (* 24 x2 ) (* (- 48) x0 ) (* 18 x1 ) ) (- 46))) (not (< (+ (* (- 31) x1 ) (* 18 x0 ) (* (- 32) x0 ) (* (- 9) x0 ) ) 37)) )) +(assert (or (not (< (+ (* (- 30) x2 ) (* (- 32) x0 ) (* 27 x0 ) ) 28)) (not (= (+ (* (- 20) x2 ) (* (- 10) x2 ) ) (- 3))) (<= (+ (* 42 x0 ) (* 49 x0 ) (* 28 x0 ) (* 0 x2 ) ) (- 30)) )) +(assert (or (not (<= (+ (* 15 x2 ) (* 22 x2 ) ) (- 7))) (< (+ (* (- 7) x1 ) (* (- 42) x0 ) (* (- 27) x2 ) (* 19 x2 ) ) 15) (< (+ (* (- 25) x1 ) (* 39 x2 ) (* (- 24) x1 ) (* 17 x1 ) ) (- 48)) )) +(assert (or (= (+ (* (- 49) x0 ) (* 27 x1 ) (* 16 x0 ) (* (- 26) x2 ) ) (- 24)) (<= (+ (* (- 33) x0 ) (* (- 7) x1 ) (* (- 7) x2 ) (* 1 x0 ) ) 34) )) +(assert (not (<= (+ (* 30 x0 ) (* 17 x0 ) (* (- 48) x0 ) ) 19)) ) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (or (not (= (+ (* 24 x2 ) (* 13 x2 ) (* (- 13) x0 ) (* 14 x2 ) ) 8)) (> (+ (* (- 30) x2 ) (* (- 32) x1 ) (* (- 45) x0 ) (* (- 2) x2 ) ) 15) )) +(assert (or (> (+ (* (- 9) x0 ) (* (- 21) x1 ) ) 3) (not (= (+ (* (- 26) x2 ) (* 3 x0 ) ) (- 10))) )) +(assert (or (not (> (+ (* (- 20) x0 ) (* 43 x0 ) ) (- 14))) (> (+ (* 13 x1 ) (* (- 38) x1 ) (* 4 x1 ) (* (- 12) x2 ) ) (- 15)) (not (< (+ (* (- 38) x2 ) (* (- 3) x0 ) ) 15)) )) +(assert (or (>= (+ (* (- 33) x0 ) (* 8 x1 ) (* 16 x0 ) ) 32) (not (<= (+ (* 23 x0 ) (* (- 28) x0 ) (* 30 x1 ) (* 17 x2 ) ) 41)) (>= (+ (* 28 x1 ) (* (- 42) x0 ) ) (- 12)) )) +(assert (or (not (<= (+ (* 23 x1 ) (* 20 x2 ) (* (- 34) x0 ) (* (- 40) x2 ) ) 28)) (not (= (+ (* 17 x2 ) (* 30 x2 ) ) (- 15))) (<= (+ (* (- 47) x1 ) (* (- 24) x0 ) (* (- 37) x0 ) ) 19) )) +(assert (or (= (+ (* 14 x0 ) (* (- 22) x1 ) ) 30) (<= (+ (* 28 x1 ) (* 33 x2 ) (* 49 x2 ) ) (- 35)) (<= (+ (* (- 47) x0 ) (* (- 45) x2 ) (* (- 7) x1 ) (* (- 47) x1 ) ) 47) )) +(check-sat) +(push 1) +(assert (or (not (> (+ (* 35 x2 ) (* (- 46) x0 ) ) 26)) (>= (+ (* 3 x1 ) (* 1 x2 ) (* (- 14) x0 ) ) 27) (> (+ (* (- 27) x2 ) (* 20 x2 ) (* 19 x1 ) (* 23 x2 ) ) 39) )) +(assert (or (not (> (+ (* 20 x0 ) (* 9 x2 ) ) 6)) (not (< (+ (* 19 x1 ) (* (- 45) x1 ) ) (- 45))) )) +(check-sat) +(pop 1) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2 new file mode 100644 index 000000000..9e61f7c4d --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2 @@ -0,0 +1,84 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(declare-fun x3 () Real) +(declare-fun x4 () Real) +(assert (<= (+ (* 27 x2 ) (* 30 x4 ) ) (- 46)) ) +(assert (or (not (>= (+ (* (- 16) x0 ) (* (- 10) x4 ) (* 21 x3 ) (* (- 46) x0 ) (* 29 x0 ) (* 41 x4 ) (* 32 x0 ) (* 33 x2 ) (* (- 37) x1 ) (* 36 x3 ) (* 18 x3 ) ) (- 34))) (<= (+ (* (- 40) x2 ) (* (- 3) x1 ) (* (- 44) x4 ) (* (- 45) x1 ) (* 20 x1 ) (* 48 x1 ) (* 28 x1 ) (* (- 27) x3 ) (* 35 x4 ) ) (- 45)) )) +(assert (or (not (= (+ (* (- 41) x2 ) (* 28 x2 ) (* (- 8) x3 ) (* 27 x0 ) (* (- 19) x2 ) (* (- 7) x4 ) ) (- 13))) (< (+ (* (- 26) x3 ) (* (- 44) x4 ) (* 14 x2 ) (* (- 27) x4 ) (* 37 x0 ) (* (- 32) x3 ) (* (- 46) x1 ) (* 23 x2 ) ) 15) )) +(assert (not (>= (+ (* 31 x1 ) (* (- 15) x1 ) (* 25 x2 ) (* 27 x3 ) (* 23 x1 ) ) (- 48))) ) +(assert (or (< (+ (* (- 38) x2 ) (* 15 x3 ) (* 9 x3 ) (* 25 x0 ) (* 37 x0 ) (* 39 x2 ) (* 41 x1 ) (* (- 18) x3 ) ) (- 26)) (not (> (+ (* 15 x2 ) (* 18 x1 ) (* 35 x3 ) (* 20 x1 ) (* 31 x1 ) (* (- 25) x2 ) (* 30 x3 ) (* 26 x1 ) (* (- 37) x2 ) (* 27 x4 ) (* (- 32) x0 ) ) 16)) )) +(assert (or (not (= (+ (* 27 x3 ) (* (- 50) x1 ) (* (- 28) x2 ) ) (- 30))) (not (>= (+ (* (- 50) x3 ) (* (- 15) x0 ) (* 15 x3 ) (* 19 x2 ) ) (- 8))) )) +(assert (or (>= (+ (* 4 x1 ) (* 27 x3 ) (* 15 x3 ) (* (- 39) x4 ) (* (- 45) x4 ) (* 38 x3 ) (* 33 x4 ) (* 40 x1 ) (* (- 26) x2 ) (* 44 x1 ) ) (- 39)) (> (+ (* 4 x0 ) (* (- 26) x3 ) (* (- 24) x2 ) ) (- 40)) )) +(assert (not (> (+ (* (- 39) x1 ) (* 32 x4 ) ) 19)) ) +(assert (or (= (+ (* (- 13) x1 ) (* (- 16) x3 ) ) 33) (not (> (+ (* 47 x4 ) (* (- 3) x4 ) (* (- 49) x3 ) (* (- 15) x1 ) (* (- 39) x1 ) (* 20 x1 ) (* 44 x4 ) (* 30 x4 ) (* 5 x1 ) (* 49 x4 ) (* 23 x0 ) ) 41)) )) +(assert (or (< (+ (* 41 x0 ) (* (- 50) x1 ) (* 41 x3 ) (* (- 37) x4 ) (* 27 x4 ) (* (- 32) x4 ) (* (- 43) x3 ) (* (- 46) x3 ) (* (- 28) x3 ) (* 31 x4 ) (* 45 x2 ) ) 31) (not (= (+ (* (- 19) x0 ) (* (- 30) x4 ) (* (- 24) x4 ) (* (- 27) x1 ) (* 2 x1 ) (* 28 x4 ) (* (- 40) x2 ) ) 5)) (>= (+ (* 19 x2 ) (* (- 20) x0 ) (* 35 x1 ) (* (- 29) x2 ) (* (- 5) x0 ) (* (- 49) x1 ) (* (- 9) x4 ) (* 3 x0 ) (* (- 36) x3 ) (* 27 x0 ) ) (- 13)) )) +(assert (or (> (+ (* 42 x4 ) (* 44 x4 ) (* (- 4) x3 ) (* 38 x3 ) (* (- 43) x2 ) ) (- 25)) (> (+ (* (- 16) x1 ) (* 5 x4 ) (* (- 6) x2 ) ) 11) )) +(assert (or (> (+ (* 1 x3 ) (* (- 10) x4 ) (* 20 x1 ) (* 20 x4 ) (* (- 26) x4 ) ) (- 33)) (< (+ (* 40 x2 ) (* (- 35) x2 ) ) (- 2)) )) +(assert (or (<= (+ (* (- 5) x4 ) (* (- 35) x3 ) (* 45 x3 ) (* 44 x0 ) (* (- 31) x1 ) (* (- 50) x4 ) (* 20 x1 ) (* 8 x0 ) (* (- 11) x1 ) (* (- 40) x3 ) (* 27 x0 ) ) 2) (= (+ (* (- 5) x1 ) (* (- 16) x2 ) (* (- 34) x2 ) (* (- 47) x4 ) (* 20 x3 ) (* 48 x3 ) ) 14) )) +(assert (or (not (< (+ (* 17 x2 ) (* (- 32) x4 ) ) (- 43))) (= (+ (* (- 17) x1 ) (* 30 x4 ) (* 20 x2 ) (* (- 1) x2 ) (* 5 x1 ) (* (- 14) x2 ) (* 2 x3 ) (* 6 x3 ) (* 24 x1 ) (* 23 x3 ) (* 0 x4 ) ) (- 14)) (< (+ (* 27 x1 ) (* 48 x2 ) (* 4 x1 ) (* 40 x3 ) (* (- 29) x4 ) (* 14 x3 ) (* 19 x2 ) (* (- 10) x4 ) (* (- 21) x0 ) (* (- 35) x4 ) ) (- 13)) )) +(assert (or (<= (+ (* 7 x3 ) (* 13 x3 ) (* (- 19) x0 ) ) (- 10)) (= (+ (* (- 37) x3 ) (* (- 25) x2 ) (* (- 33) x1 ) (* (- 41) x4 ) (* 10 x2 ) (* (- 6) x1 ) ) (- 9)) (> (+ (* (- 1) x3 ) (* 15 x1 ) (* (- 35) x2 ) (* 30 x4 ) (* (- 9) x3 ) (* 21 x2 ) (* 44 x1 ) ) (- 17)) )) +(check-sat) +(push 1) +(assert (<= (+ (* 5 x2 ) (* 44 x2 ) (* 36 x3 ) (* 3 x0 ) (* 16 x3 ) ) 48) ) +(check-sat) +(pop 1) +(check-sat) +(push 1) +(assert (not (<= (+ (* (- 39) x4 ) (* (- 40) x1 ) ) (- 45))) ) +(assert (= (+ (* 35 x3 ) (* 20 x1 ) (* (- 49) x4 ) (* (- 32) x3 ) (* 33 x3 ) (* 4 x1 ) (* (- 34) x4 ) (* 0 x4 ) (* (- 50) x3 ) ) 42) ) +(assert (or (> (+ (* 2 x3 ) (* (- 33) x4 ) (* 15 x1 ) (* 34 x4 ) (* (- 3) x2 ) (* (- 16) x1 ) (* (- 14) x3 ) (* 39 x2 ) ) 21) (not (<= (+ (* 39 x2 ) (* 22 x2 ) (* (- 50) x0 ) (* (- 23) x0 ) (* (- 48) x3 ) (* (- 31) x3 ) (* 9 x1 ) (* (- 23) x1 ) (* 27 x1 ) (* 29 x3 ) ) (- 26))) (not (<= (+ (* 15 x0 ) (* 26 x1 ) (* 11 x0 ) (* 24 x4 ) (* (- 9) x3 ) (* (- 5) x2 ) (* 4 x3 ) (* 24 x2 ) (* (- 5) x3 ) (* 16 x3 ) (* 31 x2 ) ) 43)) )) +(assert (or (>= (+ (* 27 x4 ) (* 36 x1 ) (* 27 x4 ) (* (- 18) x0 ) (* (- 1) x4 ) (* 44 x1 ) (* (- 45) x2 ) (* 38 x4 ) (* (- 39) x2 ) (* (- 30) x2 ) ) (- 41)) (not (< (+ (* (- 18) x3 ) (* 48 x1 ) (* 14 x3 ) (* (- 28) x2 ) (* 46 x1 ) (* 38 x4 ) (* (- 26) x0 ) ) (- 30))) )) +(assert (or (= (+ (* (- 1) x4 ) (* 46 x0 ) (* 19 x3 ) (* 24 x3 ) (* (- 43) x1 ) (* 14 x2 ) (* (- 7) x2 ) (* 35 x2 ) ) 9) (not (< (+ (* (- 34) x3 ) (* 18 x1 ) (* 11 x2 ) (* (- 33) x0 ) (* 45 x4 ) (* (- 27) x0 ) (* 42 x2 ) (* (- 40) x1 ) (* (- 10) x2 ) ) 34)) )) +(assert (or (not (>= (+ (* 15 x1 ) (* (- 19) x1 ) (* 34 x4 ) (* 9 x4 ) (* (- 25) x2 ) (* (- 5) x3 ) (* 15 x1 ) (* 27 x4 ) (* 49 x2 ) (* (- 41) x1 ) ) 42)) (not (< (+ (* (- 43) x4 ) (* (- 38) x4 ) (* (- 3) x0 ) (* (- 43) x3 ) ) 15)) )) +(assert (or (>= (+ (* 18 x4 ) (* 19 x4 ) (* (- 13) x0 ) (* 30 x1 ) (* 48 x4 ) (* 17 x1 ) (* 25 x0 ) (* 33 x2 ) (* 6 x1 ) (* (- 24) x1 ) (* (- 24) x0 ) ) (- 25)) (not (<= (+ (* 25 x1 ) (* (- 26) x2 ) (* (- 37) x1 ) (* 2 x4 ) (* (- 40) x2 ) (* (- 30) x1 ) (* 6 x2 ) (* (- 25) x0 ) ) 25)) )) +(assert (or (>= (+ (* 7 x1 ) (* 46 x2 ) (* 40 x0 ) (* (- 29) x2 ) (* 30 x0 ) (* (- 46) x3 ) (* 0 x4 ) (* (- 1) x2 ) (* 1 x4 ) ) (- 39)) (not (<= (+ (* (- 8) x2 ) (* 29 x0 ) (* (- 15) x4 ) (* 40 x4 ) (* 25 x0 ) (* (- 16) x2 ) (* (- 15) x3 ) (* (- 2) x4 ) ) (- 42))) )) +(assert (or (not (<= (+ (* (- 19) x3 ) (* (- 37) x4 ) (* 47 x4 ) (* 8 x4 ) (* (- 37) x2 ) (* 34 x0 ) (* 26 x4 ) (* (- 7) x0 ) ) (- 31))) (> (+ (* 44 x3 ) (* (- 45) x3 ) (* 11 x2 ) (* (- 28) x2 ) ) 20) (not (> (+ (* 43 x3 ) (* (- 5) x3 ) (* 4 x0 ) (* (- 6) x3 ) (* 5 x2 ) (* 14 x1 ) (* (- 49) x3 ) ) (- 43))) )) +(check-sat) +(pop 1) +(assert (or (>= (+ (* 16 x3 ) (* (- 8) x1 ) (* 8 x3 ) (* (- 2) x0 ) (* 30 x3 ) ) (- 9)) (not (>= (+ (* 30 x1 ) (* (- 44) x0 ) (* 11 x2 ) (* 21 x0 ) ) (- 36))) (not (< (+ (* 44 x2 ) (* 33 x2 ) (* 15 x1 ) (* (- 41) x4 ) (* 40 x0 ) (* 32 x2 ) (* (- 45) x3 ) (* (- 19) x2 ) (* (- 10) x2 ) (* 26 x2 ) (* (- 2) x0 ) ) (- 16))) )) +(assert (or (not (< (+ (* 6 x0 ) (* (- 5) x2 ) (* 24 x1 ) (* (- 26) x3 ) (* 28 x2 ) (* 2 x3 ) ) (- 30))) (<= (+ (* (- 2) x2 ) (* (- 3) x1 ) ) (- 10)) (not (> (+ (* (- 41) x4 ) (* 20 x3 ) (* (- 46) x0 ) ) (- 4))) )) +(assert (not (> (+ (* (- 26) x0 ) (* 4 x2 ) (* 22 x4 ) (* (- 24) x3 ) (* (- 6) x4 ) (* 32 x1 ) (* (- 21) x0 ) (* 35 x4 ) ) 40)) ) +(check-sat) +(push 1) +(assert (or (not (= (+ (* (- 23) x0 ) (* 30 x0 ) (* 6 x0 ) (* (- 47) x3 ) (* (- 46) x4 ) (* 23 x3 ) (* 17 x0 ) ) (- 18))) (< (+ (* 24 x4 ) (* (- 45) x1 ) (* 9 x0 ) (* (- 39) x3 ) (* 49 x2 ) (* (- 21) x1 ) (* 8 x3 ) (* 44 x3 ) (* (- 2) x0 ) (* (- 32) x2 ) ) (- 46)) )) +(assert (or (not (< (+ (* 29 x1 ) (* 8 x4 ) (* (- 50) x2 ) (* 31 x4 ) (* (- 11) x1 ) (* (- 44) x0 ) (* 47 x2 ) (* 28 x0 ) (* (- 19) x3 ) ) (- 14))) (not (>= (+ (* (- 23) x2 ) (* 41 x2 ) (* (- 26) x1 ) (* (- 2) x0 ) (* 7 x0 ) (* (- 13) x2 ) (* 36 x0 ) (* (- 50) x2 ) (* 45 x2 ) ) 41)) )) +(check-sat) +(pop 1) +(assert (or (= (+ (* (- 37) x0 ) (* 17 x4 ) (* 12 x2 ) (* (- 9) x4 ) (* (- 3) x0 ) (* 46 x0 ) (* 28 x0 ) (* 24 x0 ) (* (- 30) x0 ) (* (- 46) x1 ) (* (- 22) x2 ) ) (- 50)) (> (+ (* 47 x0 ) (* (- 16) x2 ) (* 4 x4 ) (* (- 39) x2 ) (* (- 11) x1 ) (* 18 x0 ) ) 31) (not (> (+ (* (- 39) x3 ) (* 33 x3 ) ) 35)) )) +(assert (or (> (+ (* (- 50) x2 ) (* 17 x2 ) (* (- 48) x0 ) (* (- 32) x4 ) (* (- 2) x2 ) (* (- 14) x2 ) (* 44 x4 ) (* 34 x1 ) ) 12) (not (>= (+ (* (- 5) x4 ) (* 38 x0 ) (* (- 24) x4 ) (* 35 x3 ) (* 33 x4 ) (* (- 47) x3 ) (* 8 x0 ) (* (- 9) x0 ) (* (- 16) x2 ) (* (- 1) x1 ) (* (- 15) x0 ) ) (- 12))) (not (< (+ (* 45 x1 ) (* 0 x0 ) (* 36 x0 ) (* 15 x0 ) (* 26 x4 ) (* (- 40) x3 ) ) 11)) )) +(assert (not (> (+ (* (- 4) x0 ) (* 47 x1 ) (* (- 13) x0 ) (* 17 x4 ) (* (- 13) x4 ) (* (- 44) x4 ) (* (- 5) x3 ) (* (- 20) x3 ) (* 28 x2 ) ) 18)) ) +(assert (or (not (< (+ (* (- 18) x0 ) (* (- 48) x1 ) (* 37 x4 ) (* 46 x0 ) (* 11 x0 ) (* (- 33) x4 ) (* (- 5) x0 ) ) 35)) (>= (+ (* (- 13) x3 ) (* 36 x1 ) (* (- 7) x4 ) (* 37 x0 ) (* (- 37) x2 ) (* (- 42) x2 ) (* (- 11) x4 ) ) (- 9)) (= (+ (* 27 x2 ) (* 42 x1 ) (* (- 3) x1 ) (* (- 9) x4 ) (* 44 x2 ) (* (- 24) x3 ) (* (- 49) x3 ) (* 39 x0 ) (* 36 x0 ) (* 7 x4 ) ) (- 25)) )) +(assert (or (< (+ (* (- 27) x4 ) (* 43 x4 ) ) (- 22)) (not (>= (+ (* (- 36) x3 ) (* (- 47) x1 ) (* (- 30) x2 ) ) (- 1))) (> (+ (* (- 37) x1 ) (* (- 29) x4 ) (* 19 x1 ) (* 26 x3 ) (* (- 50) x3 ) (* 23 x1 ) (* 38 x2 ) (* 23 x4 ) (* 27 x3 ) (* 6 x0 ) ) 8) )) +(assert (or (not (<= (+ (* (- 25) x1 ) (* (- 46) x3 ) (* (- 11) x0 ) (* 6 x4 ) (* (- 30) x3 ) (* (- 7) x2 ) (* (- 30) x1 ) (* 35 x4 ) ) (- 4))) (not (<= (+ (* 8 x1 ) (* (- 27) x2 ) (* 32 x2 ) (* 39 x1 ) (* 21 x3 ) ) 21)) (< (+ (* (- 30) x0 ) (* 1 x3 ) (* (- 12) x2 ) (* 4 x1 ) (* (- 31) x1 ) (* 27 x2 ) (* 23 x1 ) (* 31 x2 ) ) 18) )) +(assert (or (< (+ (* (- 30) x1 ) (* 44 x2 ) (* (- 26) x2 ) (* 42 x0 ) ) 7) (not (= (+ (* (- 8) x3 ) (* (- 26) x0 ) (* 4 x1 ) (* 25 x0 ) ) 33)) )) +(assert (not (> (+ (* 27 x2 ) (* 11 x2 ) (* (- 12) x3 ) (* (- 9) x4 ) (* 28 x4 ) (* (- 46) x2 ) (* (- 24) x0 ) (* (- 15) x3 ) ) (- 41))) ) +(check-sat) +(push 1) +(assert (or (= (+ (* (- 49) x3 ) (* (- 15) x1 ) (* (- 43) x0 ) (* 20 x0 ) (* 48 x1 ) (* (- 41) x3 ) (* 23 x3 ) (* 29 x3 ) (* (- 29) x3 ) ) 46) (> (+ (* 29 x3 ) (* 34 x4 ) (* (- 33) x2 ) (* 33 x4 ) (* 9 x0 ) (* 26 x4 ) ) (- 4)) )) +(assert (not (< (+ (* (- 6) x1 ) (* 5 x2 ) (* (- 14) x2 ) (* (- 23) x1 ) (* (- 15) x4 ) (* 3 x2 ) (* (- 35) x0 ) (* 44 x0 ) ) 1)) ) +(assert (or (not (> (+ (* (- 37) x1 ) (* (- 18) x4 ) (* (- 19) x2 ) (* (- 37) x1 ) (* 17 x4 ) (* (- 43) x2 ) (* (- 24) x4 ) ) (- 7))) (>= (+ (* 46 x3 ) (* 8 x0 ) (* 45 x3 ) ) (- 46)) (not (<= (+ (* (- 32) x4 ) (* 30 x4 ) (* 30 x3 ) (* (- 15) x3 ) (* 14 x2 ) (* 28 x0 ) (* 7 x3 ) (* 8 x0 ) ) (- 14))) )) +(assert (or (not (>= (+ (* 45 x3 ) (* 3 x4 ) ) (- 8))) (not (< (+ (* (- 37) x0 ) (* (- 14) x1 ) (* 34 x4 ) (* 9 x4 ) (* (- 17) x2 ) ) (- 27))) )) +(assert (or (>= (+ (* (- 32) x1 ) (* (- 11) x4 ) (* 16 x0 ) (* 0 x0 ) (* 41 x1 ) (* 5 x3 ) (* (- 28) x4 ) (* 27 x3 ) (* (- 11) x3 ) (* (- 16) x3 ) ) (- 26)) (not (> (+ (* 18 x2 ) (* (- 19) x0 ) (* 4 x1 ) (* 45 x0 ) (* (- 41) x2 ) (* (- 18) x4 ) ) 26)) (>= (+ (* (- 13) x3 ) (* 15 x0 ) (* 33 x2 ) (* (- 50) x2 ) (* (- 43) x0 ) (* 1 x1 ) (* 29 x2 ) (* 11 x4 ) (* 21 x4 ) ) 42) )) +(assert (<= (+ (* 9 x4 ) (* (- 40) x3 ) (* (- 33) x1 ) (* 46 x1 ) ) (- 43)) ) +(assert (or (<= (+ (* 9 x1 ) (* 7 x3 ) (* 7 x0 ) (* 11 x3 ) (* 37 x0 ) (* 13 x4 ) (* (- 40) x4 ) (* (- 13) x2 ) (* (- 29) x3 ) (* 46 x1 ) (* 2 x1 ) ) 15) (= (+ (* 12 x3 ) (* 17 x1 ) (* (- 36) x4 ) (* (- 18) x1 ) (* 38 x1 ) (* 9 x1 ) (* (- 38) x1 ) ) (- 4)) (not (< (+ (* (- 36) x3 ) (* 11 x0 ) (* 46 x1 ) (* (- 31) x4 ) (* 25 x0 ) (* (- 50) x4 ) (* 40 x4 ) (* 41 x4 ) ) 7)) )) +(assert (>= (+ (* 12 x4 ) (* (- 24) x0 ) (* (- 11) x4 ) (* 3 x2 ) (* (- 38) x2 ) (* (- 48) x2 ) (* 5 x4 ) (* 33 x3 ) ) (- 23)) ) +(assert (> (+ (* 15 x3 ) (* 31 x1 ) (* 8 x1 ) ) (- 33)) ) +(assert (not (<= (+ (* (- 41) x4 ) (* 33 x4 ) (* (- 29) x2 ) (* (- 20) x1 ) (* (- 28) x0 ) ) (- 13))) ) +(assert (or (not (< (+ (* 23 x3 ) (* (- 29) x1 ) (* (- 23) x0 ) (* (- 7) x4 ) (* 21 x2 ) (* (- 21) x0 ) ) (- 33))) (not (< (+ (* 30 x3 ) (* (- 30) x2 ) (* (- 30) x3 ) (* 30 x2 ) (* (- 10) x2 ) (* (- 3) x3 ) (* (- 22) x4 ) (* (- 48) x0 ) (* (- 9) x3 ) (* (- 6) x4 ) ) (- 30))) (not (<= (+ (* 2 x2 ) (* (- 31) x4 ) ) 3)) )) +(check-sat) +(pop 1) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2 new file mode 100644 index 000000000..cfcd80a44 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2 @@ -0,0 +1,92 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(declare-fun x3 () Real) +(declare-fun x4 () Real) +(assert (> (+ (* (- 32) x4 ) (* 46 x3 ) ) 21) ) +(assert (< (+ (* 12 x3 ) (* (- 7) x2 ) (* (- 7) x0 ) (* (- 49) x1 ) (* (- 32) x3 ) ) (- 17)) ) +(assert (or (not (>= (+ (* (- 10) x2 ) (* 37 x1 ) (* 33 x0 ) (* 33 x0 ) ) 29)) (not (<= (+ (* 25 x3 ) (* 32 x4 ) (* (- 27) x3 ) (* 13 x2 ) (* (- 22) x1 ) (* (- 8) x4 ) (* (- 1) x4 ) (* 9 x4 ) (* 1 x1 ) (* 40 x1 ) ) 41)) )) +(assert (not (= (+ (* (- 12) x1 ) (* 5 x3 ) (* 36 x4 ) (* (- 35) x0 ) (* 18 x0 ) ) (- 12))) ) +(assert (>= (+ (* (- 25) x4 ) (* (- 20) x4 ) (* 12 x2 ) (* 3 x1 ) (* (- 26) x3 ) (* (- 20) x2 ) (* (- 13) x2 ) (* 35 x0 ) (* 30 x0 ) ) (- 10)) ) +(assert (or (not (= (+ (* (- 48) x1 ) (* 25 x0 ) (* 13 x4 ) ) 24)) (not (> (+ (* (- 24) x0 ) (* 24 x1 ) ) (- 19))) )) +(assert (not (< (+ (* (- 12) x2 ) (* (- 25) x3 ) ) (- 32))) ) +(assert (not (<= (+ (* 28 x4 ) (* 11 x4 ) (* 0 x3 ) (* (- 22) x4 ) (* (- 37) x0 ) (* 2 x3 ) (* 39 x1 ) ) (- 24))) ) +(assert (or (not (>= (+ (* 34 x3 ) (* 36 x2 ) (* (- 39) x4 ) (* 33 x2 ) (* 39 x1 ) (* 22 x3 ) (* 9 x3 ) ) (- 17))) (not (= (+ (* 19 x1 ) (* (- 45) x3 ) (* 16 x1 ) (* (- 50) x1 ) (* (- 23) x1 ) ) (- 25))) )) +(assert (or (<= (+ (* 24 x3 ) (* (- 17) x1 ) ) 7) (= (+ (* (- 8) x1 ) (* 39 x1 ) (* (- 5) x1 ) (* 19 x4 ) (* (- 28) x1 ) (* (- 11) x4 ) ) 38) )) +(assert (< (+ (* 35 x4 ) (* (- 28) x3 ) (* (- 11) x0 ) (* 49 x3 ) (* 7 x2 ) (* 44 x3 ) (* (- 10) x4 ) (* (- 28) x4 ) (* (- 45) x1 ) (* 30 x4 ) (* (- 13) x1 ) ) (- 48)) ) +(assert (or (> (+ (* 28 x4 ) (* (- 16) x1 ) (* 47 x0 ) (* (- 25) x3 ) (* 6 x1 ) ) 26) (not (<= (+ (* 49 x4 ) (* (- 7) x2 ) (* (- 17) x3 ) (* 42 x0 ) (* (- 23) x1 ) (* (- 30) x4 ) (* 7 x0 ) (* (- 44) x3 ) (* 38 x2 ) (* (- 36) x1 ) ) (- 28))) )) +(assert (or (>= (+ (* (- 45) x3 ) (* (- 47) x2 ) (* (- 37) x2 ) (* 19 x2 ) ) 7) (= (+ (* (- 30) x4 ) (* (- 2) x1 ) (* (- 34) x1 ) (* 6 x2 ) (* (- 15) x2 ) (* (- 40) x4 ) (* (- 32) x1 ) ) (- 37)) )) +(assert (not (<= (+ (* 24 x1 ) (* 18 x0 ) (* (- 3) x2 ) (* 46 x2 ) (* (- 7) x4 ) (* (- 5) x4 ) ) 14)) ) +(assert (or (not (> (+ (* (- 17) x3 ) (* (- 40) x0 ) (* 41 x4 ) (* (- 41) x0 ) (* (- 17) x2 ) (* (- 28) x3 ) (* 4 x3 ) (* 19 x3 ) (* (- 15) x2 ) ) 18)) (<= (+ (* (- 12) x0 ) (* 21 x0 ) (* (- 12) x0 ) ) (- 22)) )) +(assert (or (not (> (+ (* (- 29) x3 ) (* (- 14) x4 ) (* (- 17) x0 ) (* 36 x4 ) (* 42 x2 ) ) (- 10))) (not (<= (+ (* (- 16) x2 ) (* (- 24) x1 ) (* (- 17) x1 ) (* (- 29) x4 ) (* 47 x1 ) (* 34 x4 ) (* 2 x3 ) ) (- 20))) )) +(assert (or (< (+ (* 19 x1 ) (* 40 x1 ) (* 3 x0 ) (* (- 3) x0 ) (* (- 50) x0 ) (* 5 x2 ) (* (- 9) x4 ) ) 31) (> (+ (* 33 x4 ) (* (- 50) x2 ) (* (- 15) x4 ) (* (- 1) x3 ) (* (- 10) x3 ) (* 41 x0 ) (* (- 42) x4 ) ) (- 38)) )) +(check-sat) +(push 1) +(assert (or (= (+ (* 36 x1 ) (* 23 x1 ) (* 24 x1 ) (* 38 x0 ) (* 3 x1 ) (* (- 14) x2 ) (* 28 x0 ) (* 37 x0 ) ) 33) (<= (+ (* 34 x4 ) (* 2 x4 ) (* (- 20) x1 ) (* 18 x3 ) (* 39 x3 ) (* (- 44) x0 ) (* 18 x1 ) (* (- 1) x0 ) (* (- 15) x3 ) ) (- 13)) (<= (+ (* (- 10) x2 ) (* (- 11) x0 ) (* 30 x4 ) (* 22 x3 ) (* (- 6) x0 ) (* 35 x3 ) (* 6 x4 ) (* 2 x2 ) ) (- 26)) )) +(assert (or (not (<= (+ (* (- 9) x0 ) (* (- 27) x4 ) (* 6 x3 ) ) 21)) (not (> (+ (* 18 x0 ) (* 42 x4 ) (* (- 7) x0 ) (* 6 x1 ) (* 26 x4 ) (* 38 x3 ) (* 10 x2 ) (* (- 41) x3 ) (* 37 x2 ) (* 30 x0 ) ) (- 41))) )) +(assert (or (not (= (+ (* 48 x1 ) (* (- 38) x3 ) (* (- 15) x3 ) (* (- 2) x2 ) (* (- 17) x2 ) (* 45 x3 ) (* 32 x4 ) (* 32 x1 ) (* (- 46) x3 ) (* (- 34) x4 ) ) 15)) (not (<= (+ (* 14 x1 ) (* 17 x0 ) (* (- 33) x2 ) ) 20)) (<= (+ (* 19 x2 ) (* (- 25) x0 ) ) 19) )) +(assert (or (not (>= (+ (* 29 x4 ) (* (- 28) x1 ) (* (- 23) x3 ) (* (- 50) x3 ) (* 43 x3 ) (* 31 x0 ) ) 7)) (not (< (+ (* 21 x0 ) (* 11 x3 ) (* (- 24) x1 ) (* (- 2) x2 ) (* 2 x3 ) (* (- 37) x3 ) (* (- 34) x3 ) ) (- 38))) )) +(assert (not (<= (+ (* 29 x2 ) (* (- 38) x0 ) (* 17 x4 ) (* 31 x0 ) (* 44 x0 ) (* (- 10) x4 ) (* 18 x0 ) ) (- 49))) ) +(assert (< (+ (* 44 x4 ) (* (- 42) x4 ) (* 28 x0 ) (* 7 x0 ) (* (- 33) x0 ) (* 49 x4 ) (* 19 x1 ) ) (- 39)) ) +(assert (or (>= (+ (* 39 x3 ) (* (- 30) x4 ) (* 27 x4 ) (* 5 x4 ) (* (- 10) x2 ) (* 2 x1 ) (* (- 28) x4 ) (* (- 5) x2 ) ) 2) (= (+ (* 44 x1 ) (* (- 45) x1 ) (* 39 x3 ) (* (- 46) x1 ) (* (- 18) x0 ) (* (- 50) x3 ) (* (- 38) x3 ) (* 32 x1 ) (* (- 23) x1 ) (* 4 x4 ) (* 47 x2 ) ) 8) (not (= (+ (* (- 27) x3 ) (* 3 x1 ) (* (- 32) x2 ) ) (- 3))) )) +(assert (or (not (> (+ (* 17 x2 ) (* (- 43) x0 ) (* (- 39) x2 ) (* 38 x0 ) ) 43)) (not (<= (+ (* (- 16) x4 ) (* (- 21) x4 ) (* (- 42) x3 ) (* 36 x1 ) (* (- 37) x1 ) ) 41)) )) +(assert (or (> (+ (* 34 x3 ) (* 22 x1 ) ) 1) (not (<= (+ (* 1 x4 ) (* (- 45) x1 ) (* 28 x0 ) (* 34 x2 ) (* 26 x0 ) (* 3 x1 ) (* (- 33) x4 ) (* 18 x1 ) (* 33 x2 ) (* 15 x4 ) ) (- 25))) )) +(assert (or (> (+ (* (- 43) x2 ) (* (- 16) x4 ) (* 48 x0 ) (* (- 9) x0 ) (* (- 48) x0 ) (* (- 3) x1 ) (* (- 14) x4 ) (* (- 45) x1 ) (* (- 38) x1 ) (* 35 x2 ) ) (- 18)) (< (+ (* (- 5) x2 ) (* 0 x2 ) (* 13 x1 ) (* 28 x0 ) (* 29 x3 ) (* (- 45) x2 ) (* 0 x0 ) (* 35 x1 ) (* (- 33) x2 ) ) 35) (< (+ (* (- 3) x0 ) (* (- 27) x0 ) (* 8 x2 ) (* 2 x0 ) (* 4 x4 ) ) 48) )) +(check-sat) +(push 1) +(assert (= (+ (* (- 33) x3 ) (* 8 x2 ) (* (- 5) x4 ) (* (- 27) x1 ) (* 31 x4 ) (* (- 30) x2 ) (* 17 x2 ) (* (- 31) x3 ) (* 2 x2 ) ) 27) ) +(assert (not (= (+ (* 39 x2 ) (* 46 x3 ) (* (- 13) x1 ) (* 17 x0 ) (* 39 x1 ) (* (- 25) x0 ) ) 36)) ) +(assert (or (> (+ (* (- 2) x1 ) (* (- 9) x2 ) (* (- 20) x3 ) ) (- 4)) (> (+ (* (- 13) x4 ) (* (- 1) x2 ) (* 45 x2 ) (* 15 x2 ) (* (- 10) x4 ) (* 41 x2 ) (* (- 40) x1 ) ) 18) )) +(assert (or (not (<= (+ (* (- 8) x4 ) (* (- 21) x3 ) (* (- 44) x1 ) ) 9)) (= (+ (* (- 27) x2 ) (* 49 x2 ) (* (- 14) x4 ) (* (- 28) x1 ) ) (- 49)) (< (+ (* (- 7) x3 ) (* 44 x3 ) ) 13) )) +(assert (or (not (<= (+ (* (- 38) x2 ) (* 13 x1 ) (* (- 5) x0 ) (* 24 x2 ) (* (- 16) x4 ) (* (- 29) x0 ) ) 35)) (not (< (+ (* (- 39) x1 ) (* (- 40) x1 ) (* 37 x4 ) (* 47 x1 ) (* 19 x1 ) (* 46 x2 ) ) (- 44))) )) +(check-sat) +(pop 1) +(assert (<= (+ (* 47 x1 ) (* (- 49) x2 ) (* (- 33) x3 ) (* 18 x4 ) (* (- 18) x1 ) (* (- 10) x4 ) (* (- 38) x0 ) (* (- 6) x2 ) (* 10 x4 ) (* (- 18) x3 ) (* (- 25) x0 ) ) (- 21)) ) +(assert (or (not (<= (+ (* (- 29) x1 ) (* 12 x3 ) (* 15 x3 ) (* (- 49) x0 ) (* 40 x2 ) (* (- 25) x4 ) ) 24)) (not (>= (+ (* 18 x4 ) (* (- 14) x0 ) ) (- 22))) (<= (+ (* (- 1) x0 ) (* (- 31) x3 ) (* 21 x1 ) (* 12 x4 ) (* (- 28) x2 ) (* 12 x1 ) (* 42 x4 ) (* (- 29) x3 ) (* 34 x4 ) (* 10 x2 ) ) 6) )) +(assert (>= (+ (* 15 x1 ) (* (- 1) x4 ) (* (- 11) x0 ) (* (- 24) x1 ) (* 37 x3 ) ) (- 1)) ) +(assert (or (not (= (+ (* (- 1) x1 ) (* 22 x4 ) (* 5 x2 ) (* (- 29) x1 ) (* 15 x0 ) (* 46 x1 ) ) (- 40))) (< (+ (* (- 4) x0 ) (* 13 x2 ) ) 36) )) +(assert (or (<= (+ (* 33 x3 ) (* 43 x4 ) (* (- 9) x1 ) (* 32 x4 ) (* 18 x3 ) (* (- 29) x3 ) (* (- 45) x0 ) (* 26 x3 ) ) (- 48)) (>= (+ (* 36 x4 ) (* (- 18) x1 ) (* 27 x4 ) (* (- 8) x2 ) (* 12 x0 ) (* (- 41) x2 ) (* 19 x0 ) (* 8 x4 ) (* (- 2) x0 ) (* 25 x3 ) ) (- 34)) )) +(assert (or (>= (+ (* 40 x1 ) (* 35 x4 ) (* 29 x0 ) (* 28 x1 ) (* 22 x3 ) (* (- 8) x0 ) (* (- 18) x4 ) (* 48 x4 ) (* (- 48) x1 ) (* 45 x2 ) ) 10) (not (<= (+ (* 14 x1 ) (* (- 45) x3 ) (* 27 x2 ) (* (- 41) x1 ) (* (- 15) x4 ) (* 4 x1 ) (* (- 33) x1 ) (* 31 x2 ) (* (- 11) x1 ) (* 5 x4 ) (* (- 22) x2 ) ) (- 45))) (> (+ (* (- 7) x3 ) (* (- 42) x2 ) (* 9 x3 ) (* 39 x4 ) (* (- 3) x1 ) (* (- 38) x1 ) (* 35 x3 ) ) 49) )) +(assert (or (not (< (+ (* 14 x2 ) (* 21 x1 ) (* (- 10) x1 ) (* 26 x2 ) (* (- 16) x0 ) (* 20 x1 ) (* (- 46) x4 ) (* (- 20) x4 ) ) (- 35))) (not (> (+ (* 35 x2 ) (* (- 40) x2 ) (* (- 4) x2 ) (* (- 36) x1 ) (* (- 11) x2 ) ) 41)) )) +(check-sat) +(pop 1) +(assert (or (not (= (+ (* (- 42) x2 ) (* (- 42) x4 ) (* 5 x4 ) (* (- 40) x4 ) (* (- 19) x0 ) (* (- 46) x3 ) (* 18 x4 ) (* 11 x1 ) (* (- 34) x3 ) (* (- 3) x0 ) ) (- 20))) (> (+ (* 44 x1 ) (* 22 x4 ) (* (- 15) x4 ) (* 33 x1 ) (* (- 13) x4 ) (* 25 x2 ) ) 43) (not (> (+ (* 48 x2 ) (* (- 44) x0 ) (* 26 x3 ) (* (- 1) x0 ) (* (- 18) x2 ) (* 25 x1 ) (* (- 16) x1 ) (* 43 x0 ) (* 35 x0 ) (* 7 x2 ) ) 22)) )) +(assert (or (>= (+ (* (- 39) x3 ) (* (- 22) x0 ) (* (- 13) x4 ) (* (- 26) x4 ) (* 47 x0 ) (* (- 35) x3 ) (* 47 x1 ) (* 44 x2 ) (* 6 x2 ) (* (- 25) x4 ) ) (- 49)) (> (+ (* (- 16) x3 ) (* 9 x3 ) (* (- 34) x3 ) ) 45) )) +(assert (or (not (>= (+ (* (- 44) x2 ) (* 23 x3 ) ) (- 47))) (= (+ (* (- 10) x1 ) (* (- 30) x1 ) (* 27 x1 ) (* 47 x0 ) (* (- 43) x1 ) (* (- 41) x2 ) (* 15 x2 ) (* 47 x0 ) (* (- 34) x4 ) (* 11 x3 ) ) (- 42)) )) +(assert (or (< (+ (* (- 18) x1 ) (* 1 x4 ) (* 20 x1 ) (* (- 16) x3 ) (* (- 11) x3 ) (* 38 x2 ) (* (- 47) x3 ) (* 5 x3 ) ) 14) (not (= (+ (* (- 43) x2 ) (* 32 x0 ) ) (- 30))) (not (> (+ (* (- 17) x4 ) (* (- 40) x4 ) (* (- 45) x2 ) (* (- 47) x4 ) (* 7 x3 ) ) 40)) )) +(assert (not (= (+ (* 9 x2 ) (* 23 x0 ) (* (- 32) x4 ) (* 38 x0 ) ) 27)) ) +(check-sat) +(push 1) +(assert (or (= (+ (* 11 x0 ) (* (- 7) x3 ) (* 39 x4 ) ) 7) (not (< (+ (* 38 x4 ) (* 28 x0 ) (* (- 45) x4 ) (* 9 x2 ) (* 11 x0 ) (* (- 30) x0 ) ) (- 27))) (not (< (+ (* 48 x4 ) (* 2 x2 ) (* (- 46) x3 ) ) (- 37))) )) +(assert (not (< (+ (* (- 6) x4 ) (* (- 47) x0 ) (* 40 x4 ) (* (- 14) x4 ) (* (- 29) x0 ) (* 47 x2 ) ) (- 16))) ) +(check-sat) +(pop 1) +(assert (not (>= (+ (* 23 x2 ) (* (- 30) x1 ) (* (- 48) x4 ) (* 27 x1 ) (* (- 16) x1 ) (* 27 x0 ) (* 10 x3 ) (* 13 x3 ) ) (- 47))) ) +(assert (or (< (+ (* 25 x3 ) (* 15 x0 ) ) (- 17)) (< (+ (* 3 x0 ) (* (- 11) x1 ) (* (- 10) x3 ) (* (- 19) x3 ) (* (- 11) x4 ) (* 5 x0 ) (* 46 x2 ) (* (- 48) x2 ) ) (- 39)) )) +(assert (or (not (>= (+ (* 19 x3 ) (* 15 x4 ) (* 19 x1 ) (* (- 28) x3 ) ) 5)) (not (< (+ (* 2 x0 ) (* (- 32) x4 ) (* (- 22) x4 ) (* (- 49) x4 ) (* 28 x3 ) (* (- 47) x4 ) ) 30)) )) +(assert (or (< (+ (* 32 x4 ) (* 45 x2 ) (* (- 44) x3 ) (* (- 19) x0 ) (* (- 30) x0 ) (* (- 42) x2 ) (* 44 x4 ) (* 48 x0 ) (* 46 x2 ) (* 24 x1 ) (* 12 x0 ) ) 2) (not (> (+ (* (- 8) x0 ) (* (- 16) x4 ) (* (- 5) x1 ) (* (- 42) x2 ) (* (- 33) x1 ) (* (- 44) x1 ) (* 49 x0 ) (* (- 32) x3 ) (* (- 33) x4 ) (* (- 31) x4 ) (* 27 x2 ) ) 18)) (not (> (+ (* 5 x0 ) (* 27 x2 ) (* (- 21) x0 ) (* 25 x4 ) (* 10 x1 ) (* (- 17) x2 ) (* (- 37) x1 ) (* (- 11) x2 ) ) 21)) )) +(check-sat) +(push 1) +(assert (not (>= (+ (* 19 x2 ) (* 16 x2 ) (* (- 17) x4 ) (* (- 43) x4 ) ) 43)) ) +(assert (not (> (+ (* (- 6) x1 ) (* 4 x4 ) (* 9 x1 ) (* 32 x0 ) ) 11)) ) +(assert (or (not (> (+ (* 4 x1 ) (* (- 25) x3 ) (* 12 x0 ) (* 14 x1 ) (* 10 x2 ) ) (- 27))) (<= (+ (* 3 x4 ) (* (- 43) x0 ) (* 34 x4 ) (* 16 x1 ) ) (- 7)) )) +(assert (not (> (+ (* (- 38) x1 ) (* (- 43) x2 ) (* (- 18) x3 ) (* (- 4) x2 ) (* 25 x1 ) (* 43 x0 ) (* (- 16) x0 ) (* 22 x2 ) ) 36)) ) +(assert (= (+ (* 22 x2 ) (* (- 23) x0 ) (* 47 x2 ) (* (- 31) x3 ) (* 4 x0 ) (* 9 x3 ) (* (- 48) x4 ) (* 48 x1 ) ) (- 2)) ) +(assert (or (>= (+ (* (- 31) x1 ) (* (- 16) x3 ) ) (- 28)) (<= (+ (* (- 36) x2 ) (* (- 11) x4 ) (* (- 29) x1 ) (* 26 x1 ) (* 36 x1 ) ) (- 19)) (<= (+ (* 39 x3 ) (* 28 x0 ) (* 19 x4 ) (* (- 37) x1 ) (* 39 x1 ) (* 14 x3 ) (* (- 43) x4 ) (* 8 x4 ) ) 42) )) +(assert (< (+ (* 46 x0 ) (* 18 x3 ) (* (- 24) x3 ) (* 31 x4 ) (* 25 x3 ) ) 20) ) +(check-sat) +(pop 1) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2 new file mode 100644 index 000000000..f79d3ee69 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2 @@ -0,0 +1,67 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(declare-fun x3 () Real) +(declare-fun x4 () Real) +(assert (or (<= (+ (* 30 x0 ) (* 33 x1 ) (* 40 x1 ) (* 27 x3 ) (* 17 x3 ) (* (- 18) x0 ) (* (- 30) x0 ) ) (- 46)) (> (+ (* 48 x3 ) (* 16 x1 ) (* (- 20) x4 ) (* (- 22) x1 ) (* (- 11) x3 ) (* (- 27) x0 ) (* 8 x2 ) (* (- 17) x1 ) (* (- 21) x1 ) (* 19 x0 ) ) 8) (not (> (+ (* 24 x4 ) (* (- 7) x0 ) (* 11 x4 ) (* (- 17) x1 ) (* 3 x1 ) (* 36 x1 ) (* (- 16) x0 ) ) 16)) )) +(assert (or (> (+ (* (- 30) x1 ) (* (- 6) x3 ) (* 33 x4 ) (* 9 x4 ) (* (- 47) x0 ) ) 30) (not (<= (+ (* 44 x3 ) (* (- 34) x1 ) (* (- 5) x2 ) (* (- 20) x1 ) (* 6 x1 ) (* (- 1) x4 ) (* 40 x2 ) (* 11 x4 ) (* 48 x3 ) (* 23 x3 ) (* (- 16) x2 ) ) 6)) )) +(assert (or (not (> (+ (* (- 9) x3 ) (* (- 49) x4 ) (* (- 23) x2 ) (* (- 36) x2 ) (* (- 11) x2 ) (* 5 x1 ) (* 10 x2 ) (* (- 6) x1 ) (* 1 x1 ) (* (- 34) x0 ) ) (- 1))) (> (+ (* 48 x4 ) (* 20 x0 ) ) 47) (not (<= (+ (* 39 x1 ) (* (- 7) x3 ) (* (- 3) x4 ) (* 43 x4 ) (* (- 45) x1 ) ) (- 49))) )) +(assert (>= (+ (* 38 x0 ) (* 11 x0 ) (* (- 23) x3 ) (* 5 x0 ) (* 7 x1 ) (* 25 x0 ) (* (- 30) x0 ) (* (- 21) x2 ) (* (- 20) x0 ) ) (- 26)) ) +(assert (or (> (+ (* (- 25) x1 ) (* (- 41) x4 ) (* 34 x3 ) (* 45 x3 ) (* (- 34) x2 ) (* (- 47) x2 ) ) (- 7)) (< (+ (* 33 x1 ) (* (- 7) x1 ) (* (- 50) x3 ) (* 15 x2 ) ) 32) (= (+ (* 23 x3 ) (* 24 x0 ) (* (- 16) x3 ) (* (- 17) x4 ) (* 12 x0 ) (* (- 7) x4 ) (* (- 12) x0 ) (* 24 x3 ) (* 6 x2 ) ) (- 3)) )) +(assert (< (+ (* (- 11) x1 ) (* 29 x2 ) (* 10 x3 ) (* 21 x3 ) (* (- 27) x3 ) (* (- 18) x2 ) (* 31 x4 ) (* 29 x2 ) ) 46) ) +(assert (= (+ (* 38 x2 ) (* 2 x0 ) (* 21 x1 ) (* (- 20) x3 ) (* 46 x3 ) (* (- 20) x1 ) (* (- 41) x2 ) (* 20 x2 ) ) (- 18)) ) +(assert (or (= (+ (* 27 x3 ) (* 9 x4 ) (* (- 42) x4 ) (* (- 38) x2 ) (* (- 8) x3 ) (* (- 37) x1 ) (* 14 x4 ) (* 44 x0 ) (* 5 x4 ) (* (- 35) x0 ) (* (- 32) x2 ) ) 26) (> (+ (* (- 16) x0 ) (* (- 35) x0 ) (* 3 x3 ) (* (- 28) x3 ) (* 19 x4 ) (* (- 49) x3 ) (* (- 34) x1 ) (* (- 16) x0 ) (* 39 x4 ) (* 16 x4 ) (* 43 x3 ) ) (- 29)) (not (<= (+ (* (- 13) x4 ) (* 34 x0 ) (* (- 5) x1 ) (* 38 x3 ) (* 9 x3 ) (* 8 x1 ) (* (- 45) x1 ) (* (- 34) x4 ) ) 8)) )) +(check-sat) +(push 1) +(assert (or (<= (+ (* (- 18) x3 ) (* 41 x1 ) (* 7 x1 ) (* (- 34) x2 ) (* (- 8) x3 ) (* (- 13) x3 ) (* 6 x0 ) (* (- 22) x1 ) (* 17 x4 ) ) 19) (< (+ (* (- 33) x3 ) (* 20 x1 ) (* (- 8) x1 ) (* 17 x4 ) (* 17 x0 ) (* 23 x2 ) (* (- 40) x1 ) (* (- 35) x2 ) (* (- 15) x3 ) (* (- 13) x2 ) (* 47 x2 ) ) 43) )) +(assert (or (not (< (+ (* (- 2) x3 ) (* 1 x2 ) (* 11 x0 ) (* (- 32) x3 ) (* (- 7) x3 ) (* (- 5) x3 ) ) (- 40))) (< (+ (* (- 50) x2 ) (* (- 20) x2 ) ) 37) )) +(assert (or (= (+ (* 19 x2 ) (* (- 10) x1 ) ) (- 34)) (<= (+ (* 7 x0 ) (* 46 x1 ) (* 7 x0 ) (* (- 37) x4 ) (* (- 1) x2 ) (* 23 x0 ) (* 9 x3 ) (* 10 x0 ) (* (- 37) x0 ) (* (- 41) x1 ) (* 0 x0 ) ) 24) )) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (= (+ (* (- 20) x1 ) (* 32 x3 ) (* (- 21) x2 ) (* (- 9) x2 ) (* 5 x1 ) (* 4 x4 ) (* 42 x4 ) (* 6 x4 ) (* 22 x2 ) (* 32 x3 ) (* 42 x3 ) ) 1) ) +(assert (or (not (>= (+ (* (- 39) x0 ) (* 19 x4 ) (* (- 1) x3 ) ) (- 47))) (not (<= (+ (* (- 40) x4 ) (* (- 10) x2 ) (* 22 x4 ) (* (- 20) x4 ) ) 30)) )) +(assert (not (= (+ (* (- 23) x0 ) (* 33 x4 ) (* (- 43) x0 ) (* (- 48) x4 ) (* 8 x1 ) (* (- 34) x1 ) (* 24 x3 ) (* 37 x4 ) (* (- 27) x2 ) (* (- 16) x4 ) ) (- 35))) ) +(assert (not (>= (+ (* (- 1) x3 ) (* 19 x4 ) ) 29)) ) +(assert (or (not (> (+ (* (- 36) x3 ) (* (- 16) x0 ) (* 12 x3 ) (* (- 17) x2 ) (* 1 x3 ) ) 22)) (< (+ (* (- 8) x2 ) (* (- 40) x1 ) (* (- 17) x4 ) (* 37 x1 ) (* 41 x2 ) (* (- 37) x1 ) (* (- 46) x3 ) ) (- 33)) )) +(assert (<= (+ (* 27 x1 ) (* 18 x4 ) ) 12) ) +(assert (or (not (> (+ (* (- 43) x0 ) (* 43 x0 ) (* 36 x2 ) (* 21 x1 ) (* 11 x1 ) (* 32 x4 ) ) 24)) (not (< (+ (* 33 x0 ) (* 29 x3 ) (* 39 x3 ) (* 17 x4 ) (* 21 x0 ) (* 32 x2 ) (* (- 38) x1 ) (* (- 37) x0 ) (* 23 x4 ) ) (- 43))) (not (<= (+ (* 35 x4 ) (* 23 x1 ) (* 23 x0 ) (* (- 39) x0 ) (* (- 13) x4 ) (* (- 10) x1 ) (* (- 33) x2 ) (* 28 x1 ) (* 41 x4 ) (* 43 x4 ) ) 23)) )) +(check-sat) +(pop 1) +(assert (or (not (= (+ (* (- 12) x0 ) (* (- 26) x2 ) (* (- 34) x1 ) (* 46 x0 ) (* (- 38) x4 ) (* (- 45) x4 ) ) 0)) (not (>= (+ (* (- 23) x2 ) (* 9 x2 ) (* 48 x0 ) (* (- 6) x2 ) (* (- 40) x1 ) (* (- 19) x0 ) (* (- 21) x4 ) ) 13)) (not (<= (+ (* 45 x1 ) (* 28 x3 ) (* (- 13) x1 ) ) 40)) )) +(check-sat) +(push 1) +(assert (or (>= (+ (* (- 31) x0 ) (* 39 x3 ) (* (- 43) x2 ) (* (- 12) x4 ) (* (- 46) x0 ) (* 46 x3 ) (* 19 x0 ) (* (- 8) x4 ) (* 41 x3 ) (* 34 x0 ) ) (- 10)) (not (>= (+ (* (- 20) x3 ) (* (- 19) x4 ) (* (- 33) x3 ) (* 18 x2 ) (* (- 47) x1 ) (* 28 x0 ) (* 6 x0 ) (* (- 23) x1 ) (* 6 x0 ) (* 0 x0 ) ) (- 25))) )) +(assert (or (not (>= (+ (* 19 x0 ) (* 27 x4 ) (* (- 45) x4 ) (* (- 27) x2 ) (* (- 5) x3 ) (* (- 20) x0 ) ) 16)) (not (> (+ (* 45 x4 ) (* (- 22) x4 ) (* 46 x4 ) (* (- 1) x1 ) (* 12 x3 ) (* (- 7) x0 ) (* 15 x3 ) (* 28 x4 ) (* 26 x4 ) (* 35 x2 ) (* (- 35) x1 ) ) 11)) )) +(assert (or (not (<= (+ (* 35 x2 ) (* 44 x3 ) (* 44 x2 ) ) (- 28))) (> (+ (* 39 x3 ) (* (- 6) x2 ) (* 2 x4 ) (* (- 5) x4 ) (* 45 x2 ) (* 40 x1 ) (* 4 x1 ) (* (- 8) x0 ) (* (- 33) x3 ) ) 45) )) +(assert (or (> (+ (* 46 x4 ) (* (- 4) x0 ) ) 5) (>= (+ (* (- 21) x1 ) (* 22 x0 ) (* 19 x3 ) (* (- 34) x3 ) (* 41 x1 ) (* (- 1) x1 ) (* (- 39) x1 ) ) 41) )) +(assert (<= (+ (* (- 38) x4 ) (* 43 x1 ) (* 46 x4 ) (* 14 x1 ) (* 49 x3 ) (* (- 18) x3 ) (* 38 x0 ) (* (- 36) x4 ) (* 24 x4 ) (* 28 x0 ) (* (- 14) x3 ) ) (- 23)) ) +(assert (not (< (+ (* 36 x0 ) (* (- 19) x4 ) (* 5 x3 ) ) 26)) ) +(assert (or (> (+ (* (- 46) x3 ) (* 1 x0 ) (* 37 x0 ) (* (- 44) x0 ) (* 45 x3 ) (* (- 19) x1 ) (* 14 x3 ) (* (- 16) x2 ) (* 35 x2 ) (* 47 x0 ) (* (- 21) x3 ) ) 30) (< (+ (* (- 11) x3 ) (* 7 x2 ) (* (- 5) x3 ) ) (- 37)) )) +(assert (not (> (+ (* 23 x4 ) (* (- 45) x0 ) ) 6)) ) +(assert (or (not (> (+ (* 45 x4 ) (* (- 38) x2 ) (* (- 13) x4 ) (* 11 x0 ) (* (- 32) x0 ) (* 22 x2 ) ) (- 23))) (> (+ (* (- 32) x0 ) (* 24 x3 ) (* (- 26) x4 ) (* (- 6) x2 ) ) (- 20)) )) +(check-sat) +(push 1) +(assert (or (>= (+ (* 19 x4 ) (* 39 x3 ) (* 0 x2 ) (* (- 46) x2 ) (* (- 44) x4 ) (* (- 2) x4 ) (* 1 x4 ) (* 14 x1 ) (* 47 x4 ) (* 3 x3 ) (* (- 12) x1 ) ) 0) (<= (+ (* 4 x0 ) (* 17 x4 ) (* (- 26) x0 ) (* (- 30) x1 ) (* 45 x0 ) ) 20) )) +(assert (or (not (< (+ (* 24 x2 ) (* (- 17) x2 ) (* 3 x0 ) ) 32)) (not (< (+ (* (- 41) x4 ) (* 15 x4 ) (* 16 x4 ) ) (- 31))) (not (< (+ (* 24 x4 ) (* 1 x1 ) ) 19)) )) +(assert (or (< (+ (* 2 x1 ) (* (- 12) x0 ) (* (- 37) x2 ) (* 22 x4 ) (* (- 47) x4 ) ) (- 22)) (>= (+ (* 13 x0 ) (* (- 49) x1 ) (* 41 x3 ) (* 10 x4 ) (* (- 25) x0 ) (* 37 x1 ) (* 32 x3 ) ) 10) (= (+ (* (- 50) x4 ) (* 49 x2 ) (* (- 49) x3 ) (* 9 x1 ) (* 1 x1 ) (* (- 30) x4 ) (* (- 44) x0 ) ) 33) )) +(assert (or (< (+ (* (- 45) x1 ) (* 34 x3 ) (* (- 41) x4 ) (* 7 x3 ) (* (- 2) x1 ) (* 26 x4 ) (* (- 17) x1 ) (* (- 36) x2 ) (* 48 x2 ) (* (- 7) x1 ) (* 0 x4 ) ) (- 34)) (not (< (+ (* (- 34) x3 ) (* (- 22) x0 ) (* (- 17) x0 ) ) 35)) )) +(assert (or (not (> (+ (* 48 x2 ) (* 13 x2 ) ) (- 24))) (> (+ (* (- 15) x4 ) (* 32 x3 ) ) (- 19)) (not (= (+ (* (- 8) x0 ) (* (- 15) x3 ) (* (- 39) x3 ) (* 15 x0 ) (* (- 49) x1 ) (* 16 x1 ) ) 33)) )) +(assert (not (>= (+ (* 41 x2 ) (* 35 x4 ) (* 40 x4 ) (* 49 x3 ) ) 23)) ) +(assert (or (not (>= (+ (* (- 45) x0 ) (* (- 40) x4 ) (* 0 x1 ) (* 15 x1 ) (* (- 38) x3 ) (* 36 x1 ) (* (- 12) x1 ) (* 47 x0 ) (* 47 x2 ) (* (- 34) x3 ) ) (- 16))) (not (>= (+ (* (- 18) x4 ) (* (- 10) x0 ) (* 20 x2 ) (* (- 8) x4 ) (* (- 25) x1 ) (* (- 6) x2 ) (* 30 x2 ) ) (- 41))) (> (+ (* 26 x3 ) (* (- 22) x1 ) ) 23) )) +(check-sat) +(pop 1) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2 new file mode 100644 index 000000000..95a64c578 --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2 @@ -0,0 +1,55 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(declare-fun x3 () Real) +(declare-fun x4 () Real) +(check-sat) +(push 1) +(assert (or (not (< (+ (* 22 x2 ) (* (- 45) x4 ) (* (- 27) x4 ) (* (- 23) x1 ) (* (- 38) x4 ) (* 12 x0 ) (* 11 x2 ) (* 6 x4 ) (* (- 34) x3 ) (* (- 28) x3 ) ) (- 7))) (> (+ (* 49 x3 ) (* (- 9) x3 ) (* (- 6) x2 ) (* (- 39) x2 ) (* 49 x3 ) (* (- 6) x4 ) (* 35 x4 ) (* (- 5) x1 ) ) 47) (not (= (+ (* (- 37) x0 ) (* 23 x0 ) (* 8 x0 ) (* (- 25) x3 ) (* (- 10) x4 ) (* (- 31) x3 ) (* (- 7) x1 ) (* (- 9) x2 ) (* 42 x4 ) (* 9 x2 ) (* (- 29) x1 ) ) (- 47))) )) +(assert (or (> (+ (* 20 x0 ) (* 28 x0 ) (* 40 x0 ) (* (- 33) x1 ) (* 1 x3 ) (* 24 x2 ) (* (- 40) x1 ) (* 33 x1 ) ) (- 45)) (>= (+ (* 26 x0 ) (* 43 x3 ) (* 8 x3 ) (* (- 41) x0 ) (* 23 x0 ) (* (- 18) x2 ) (* 13 x0 ) (* 32 x0 ) (* (- 36) x0 ) (* (- 44) x0 ) ) 15) )) +(assert (or (not (> (+ (* (- 40) x0 ) (* (- 34) x4 ) (* 41 x2 ) (* (- 40) x4 ) (* 44 x2 ) (* (- 3) x1 ) (* (- 44) x3 ) (* (- 29) x2 ) (* (- 31) x3 ) ) (- 14))) (< (+ (* (- 48) x0 ) (* 30 x4 ) (* (- 18) x4 ) ) 39) (>= (+ (* 1 x2 ) (* (- 31) x2 ) (* (- 8) x0 ) ) 31) )) +(assert (or (not (= (+ (* (- 46) x0 ) (* 1 x3 ) (* (- 1) x3 ) (* 27 x2 ) ) (- 8))) (not (= (+ (* 26 x4 ) (* 39 x4 ) (* (- 14) x4 ) (* (- 9) x0 ) (* 18 x0 ) (* (- 15) x2 ) (* (- 4) x2 ) (* 0 x2 ) (* 48 x3 ) ) (- 8))) (<= (+ (* (- 20) x2 ) (* (- 34) x1 ) (* 49 x4 ) ) 33) )) +(assert (or (not (>= (+ (* (- 2) x3 ) (* (- 4) x0 ) (* (- 3) x0 ) (* 4 x1 ) (* 30 x4 ) (* (- 49) x0 ) ) (- 20))) (> (+ (* 8 x0 ) (* 24 x0 ) (* 39 x3 ) (* (- 2) x0 ) (* (- 25) x0 ) (* (- 17) x1 ) (* (- 40) x1 ) (* (- 15) x2 ) (* 9 x3 ) (* (- 2) x3 ) (* 49 x4 ) ) (- 47)) (not (<= (+ (* 11 x0 ) (* 49 x4 ) (* 16 x4 ) (* 17 x4 ) (* 0 x2 ) ) 6)) )) +(assert (or (not (< (+ (* 21 x1 ) (* 35 x1 ) (* (- 41) x3 ) (* 41 x1 ) (* 5 x3 ) (* (- 37) x2 ) (* 23 x4 ) (* (- 6) x3 ) (* (- 25) x4 ) (* (- 29) x0 ) ) (- 7))) (< (+ (* (- 2) x4 ) (* (- 46) x0 ) (* (- 20) x1 ) (* 27 x0 ) (* (- 2) x3 ) (* (- 39) x4 ) ) 8) )) +(check-sat) +(push 1) +(assert (or (not (<= (+ (* (- 49) x1 ) (* 5 x1 ) (* 8 x3 ) (* (- 28) x1 ) (* 18 x2 ) (* 19 x0 ) (* (- 18) x1 ) (* (- 38) x0 ) ) 12)) (not (= (+ (* 5 x1 ) (* (- 21) x3 ) (* 34 x3 ) (* 34 x4 ) (* 32 x2 ) ) 49)) (= (+ (* (- 36) x1 ) (* 39 x0 ) (* (- 16) x3 ) (* 0 x3 ) (* 24 x3 ) ) 33) )) +(assert (or (<= (+ (* (- 23) x0 ) (* 45 x1 ) (* 4 x4 ) (* 8 x0 ) (* 14 x0 ) (* (- 9) x1 ) (* 27 x3 ) (* 29 x3 ) (* (- 27) x3 ) ) 18) (not (< (+ (* (- 37) x4 ) (* (- 33) x3 ) (* 42 x1 ) (* (- 48) x0 ) (* 30 x2 ) (* 10 x4 ) ) (- 23))) (= (+ (* 6 x4 ) (* (- 8) x2 ) ) 47) )) +(assert (not (< (+ (* 43 x2 ) (* (- 13) x0 ) (* 35 x2 ) (* (- 25) x2 ) ) (- 48))) ) +(assert (or (>= (+ (* (- 19) x4 ) (* 27 x0 ) (* (- 34) x2 ) (* (- 27) x1 ) (* 10 x0 ) (* 24 x2 ) (* (- 10) x4 ) (* (- 23) x2 ) (* (- 44) x1 ) (* 7 x1 ) (* 43 x3 ) ) 44) (> (+ (* 37 x0 ) (* (- 3) x3 ) (* (- 31) x3 ) (* 28 x4 ) (* 3 x1 ) (* 35 x2 ) (* (- 26) x3 ) (* (- 5) x2 ) (* 2 x3 ) ) 35) )) +(assert (= (+ (* (- 23) x0 ) (* 44 x0 ) (* (- 35) x0 ) ) 45) ) +(assert (or (< (+ (* 3 x2 ) (* 31 x1 ) (* 10 x1 ) (* (- 16) x1 ) (* 13 x4 ) ) (- 19)) (not (< (+ (* (- 3) x2 ) (* 46 x4 ) (* 10 x4 ) (* 47 x1 ) (* 3 x1 ) (* (- 49) x2 ) (* (- 35) x2 ) ) 16)) (>= (+ (* (- 39) x2 ) (* (- 42) x0 ) (* 48 x2 ) (* (- 42) x4 ) (* (- 25) x3 ) (* 31 x3 ) (* 6 x3 ) (* 3 x0 ) (* 29 x4 ) (* 30 x0 ) (* (- 27) x1 ) ) 35) )) +(assert (or (> (+ (* (- 44) x2 ) (* (- 33) x2 ) (* 24 x4 ) (* (- 9) x2 ) (* 22 x4 ) ) 0) (not (<= (+ (* (- 7) x1 ) (* 1 x1 ) (* 8 x3 ) (* (- 37) x2 ) (* (- 39) x3 ) (* 26 x1 ) (* (- 37) x2 ) (* (- 38) x4 ) (* (- 47) x2 ) (* 1 x0 ) ) (- 30))) )) +(assert (or (not (= (+ (* 33 x2 ) (* (- 27) x2 ) (* 13 x0 ) (* (- 16) x3 ) (* 16 x1 ) (* (- 1) x2 ) (* (- 20) x1 ) (* (- 30) x2 ) (* 14 x3 ) (* (- 3) x0 ) ) (- 22))) (not (> (+ (* (- 27) x1 ) (* (- 26) x2 ) (* 20 x3 ) (* (- 3) x3 ) (* 21 x0 ) (* 36 x1 ) ) (- 16))) (< (+ (* (- 38) x0 ) (* 41 x2 ) (* (- 36) x4 ) ) 13) )) +(assert (or (> (+ (* 5 x3 ) (* (- 9) x3 ) (* (- 5) x1 ) (* 6 x2 ) (* 46 x3 ) (* (- 25) x1 ) (* 29 x2 ) (* 3 x3 ) (* (- 15) x0 ) (* 30 x1 ) (* 10 x4 ) ) (- 26)) (= (+ (* 6 x4 ) (* (- 47) x3 ) (* (- 18) x1 ) (* 24 x1 ) (* 44 x0 ) (* (- 7) x2 ) ) (- 48)) )) +(assert (or (not (> (+ (* 31 x2 ) (* 8 x1 ) (* (- 32) x1 ) (* (- 34) x3 ) (* (- 36) x3 ) (* (- 45) x2 ) (* (- 37) x2 ) (* 40 x3 ) (* 30 x3 ) (* 29 x4 ) ) (- 44))) (not (<= (+ (* (- 22) x0 ) (* (- 16) x2 ) ) 36)) (>= (+ (* 5 x3 ) (* (- 9) x4 ) ) (- 25)) )) +(assert (or (not (> (+ (* 43 x3 ) (* (- 24) x3 ) (* 7 x3 ) (* (- 40) x3 ) (* (- 33) x3 ) (* (- 36) x2 ) (* 7 x2 ) (* 20 x2 ) ) (- 7))) (= (+ (* 37 x4 ) (* 40 x4 ) ) 30) )) +(assert (or (>= (+ (* 43 x0 ) (* 4 x4 ) ) 21) (not (= (+ (* 1 x4 ) (* (- 44) x4 ) (* 48 x0 ) (* 9 x0 ) ) 18)) )) +(check-sat) +(push 1) +(assert (or (not (>= (+ (* (- 48) x2 ) (* 4 x1 ) (* (- 2) x4 ) (* (- 41) x0 ) (* 9 x1 ) (* 14 x0 ) (* 28 x3 ) (* (- 12) x3 ) ) (- 20))) (= (+ (* (- 38) x1 ) (* (- 34) x4 ) (* 1 x4 ) (* (- 26) x4 ) (* (- 30) x2 ) (* 36 x3 ) (* (- 14) x2 ) (* (- 32) x2 ) (* 2 x4 ) ) (- 22)) )) +(assert (or (not (<= (+ (* 42 x4 ) (* (- 46) x0 ) (* 41 x4 ) (* (- 13) x3 ) (* (- 36) x0 ) ) (- 44))) (not (= (+ (* 15 x4 ) (* 24 x2 ) ) 1)) (< (+ (* (- 4) x0 ) (* 0 x3 ) (* 10 x3 ) (* 18 x1 ) ) (- 33)) )) +(assert (or (= (+ (* (- 19) x3 ) (* (- 39) x4 ) (* (- 5) x1 ) (* (- 39) x3 ) ) (- 48)) (= (+ (* 30 x3 ) (* (- 15) x1 ) (* 8 x1 ) (* (- 26) x1 ) (* 6 x4 ) (* 5 x1 ) (* 3 x4 ) (* (- 13) x2 ) (* (- 47) x2 ) (* 23 x4 ) (* 28 x4 ) ) 34) (= (+ (* (- 20) x4 ) (* (- 30) x3 ) ) (- 36)) )) +(check-sat) +(push 1) +(assert (or (not (>= (+ (* 20 x0 ) (* 43 x2 ) (* (- 49) x2 ) (* (- 46) x2 ) (* 14 x3 ) (* 27 x4 ) (* 43 x2 ) (* 23 x3 ) (* (- 14) x1 ) (* 20 x2 ) ) 16)) (< (+ (* 45 x1 ) (* (- 31) x3 ) ) 25) (<= (+ (* 15 x4 ) (* 41 x4 ) (* 23 x4 ) (* (- 41) x2 ) ) 39) )) +(check-sat) +(pop 1) +(assert (or (> (+ (* (- 43) x0 ) (* (- 49) x0 ) (* (- 8) x2 ) (* (- 29) x4 ) (* (- 32) x2 ) (* (- 37) x0 ) (* 31 x2 ) (* 27 x0 ) (* 21 x3 ) ) (- 30)) (> (+ (* (- 16) x4 ) (* 20 x1 ) (* 28 x3 ) (* 15 x4 ) (* (- 46) x3 ) (* 10 x2 ) (* 12 x2 ) (* 42 x3 ) (* 42 x3 ) (* 25 x0 ) (* (- 26) x2 ) ) (- 42)) (not (>= (+ (* 24 x4 ) (* 21 x3 ) (* 9 x4 ) (* (- 30) x0 ) (* (- 32) x4 ) ) 1)) )) +(assert (or (<= (+ (* 10 x2 ) (* (- 23) x4 ) (* (- 41) x4 ) ) (- 31)) (>= (+ (* (- 5) x0 ) (* (- 6) x2 ) (* 8 x4 ) (* 34 x3 ) (* 14 x4 ) (* 36 x4 ) (* 23 x1 ) (* (- 11) x1 ) ) (- 26)) (not (< (+ (* 25 x1 ) (* (- 20) x3 ) (* (- 8) x2 ) (* 23 x4 ) (* 25 x3 ) (* 1 x2 ) ) 22)) )) +(assert (or (not (<= (+ (* 28 x3 ) (* (- 41) x4 ) (* (- 33) x0 ) (* (- 29) x4 ) (* 8 x2 ) (* (- 42) x2 ) (* 23 x2 ) (* 25 x0 ) (* (- 13) x3 ) (* 44 x0 ) ) (- 40))) (<= (+ (* (- 8) x1 ) (* (- 22) x1 ) ) (- 27)) (not (< (+ (* 24 x2 ) (* (- 6) x0 ) (* 29 x2 ) (* (- 1) x2 ) (* (- 15) x0 ) (* (- 23) x4 ) (* 46 x3 ) (* 14 x4 ) (* 26 x3 ) (* 45 x3 ) ) (- 43))) )) +(assert (or (not (>= (+ (* 48 x2 ) (* 12 x4 ) (* 41 x4 ) (* (- 19) x2 ) (* 31 x2 ) (* (- 45) x2 ) (* 2 x2 ) (* (- 7) x0 ) (* (- 50) x4 ) (* (- 16) x4 ) ) 14)) (> (+ (* 19 x4 ) (* (- 18) x0 ) (* (- 20) x0 ) (* 29 x3 ) ) (- 22)) )) +(check-sat) +(pop 1) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2 new file mode 100644 index 000000000..8b41d054c --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2 @@ -0,0 +1,79 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(declare-fun x3 () Real) +(declare-fun x4 () Real) +(assert (or (not (= (+ (* 23 x2 ) (* (- 43) x4 ) (* (- 39) x3 ) (* 4 x2 ) ) (- 2))) (>= (+ (* (- 1) x2 ) (* 0 x0 ) (* 31 x1 ) (* 20 x1 ) (* (- 27) x2 ) ) 22) (<= (+ (* 42 x1 ) (* (- 4) x4 ) (* 12 x2 ) (* 36 x1 ) (* (- 36) x4 ) (* 18 x4 ) (* 47 x0 ) ) (- 19)) )) +(assert (or (>= (+ (* 4 x1 ) (* (- 32) x2 ) (* 47 x1 ) ) 43) (< (+ (* 31 x4 ) (* 33 x0 ) (* 27 x2 ) (* 0 x0 ) (* (- 35) x0 ) (* 14 x4 ) (* 35 x0 ) (* 17 x4 ) (* 7 x3 ) (* (- 19) x3 ) ) (- 42)) )) +(assert (not (>= (+ (* (- 36) x0 ) (* (- 28) x2 ) (* (- 49) x2 ) (* (- 17) x0 ) (* (- 16) x2 ) ) (- 40))) ) +(assert (or (not (>= (+ (* 35 x4 ) (* (- 42) x1 ) (* (- 31) x4 ) (* (- 36) x3 ) (* 28 x3 ) (* (- 10) x0 ) (* 37 x1 ) (* 11 x1 ) (* (- 29) x3 ) (* 31 x1 ) ) (- 28))) (>= (+ (* 26 x1 ) (* 12 x4 ) (* (- 7) x1 ) ) (- 39)) )) +(check-sat) +(push 1) +(assert (or (< (+ (* 48 x4 ) (* 8 x4 ) (* (- 34) x4 ) (* (- 47) x4 ) (* (- 7) x3 ) (* 46 x1 ) (* (- 13) x1 ) (* (- 28) x3 ) (* (- 20) x3 ) (* 30 x0 ) (* (- 35) x1 ) ) 36) (>= (+ (* (- 22) x0 ) (* (- 14) x4 ) (* (- 22) x4 ) (* (- 25) x2 ) (* 1 x3 ) (* 18 x1 ) (* (- 34) x4 ) (* 12 x1 ) (* (- 8) x2 ) (* 33 x0 ) (* (- 47) x1 ) ) 15) )) +(assert (>= (+ (* 12 x2 ) (* 14 x3 ) (* (- 36) x2 ) ) (- 49)) ) +(assert (or (> (+ (* (- 40) x1 ) (* 47 x1 ) (* 14 x1 ) (* 41 x4 ) (* (- 39) x3 ) (* (- 23) x4 ) (* 41 x2 ) (* (- 48) x1 ) (* (- 18) x2 ) (* 46 x1 ) ) (- 4)) (not (< (+ (* (- 36) x3 ) (* (- 47) x4 ) (* 3 x4 ) (* (- 5) x4 ) ) 13)) (< (+ (* (- 45) x2 ) (* (- 33) x2 ) (* 8 x2 ) (* 34 x4 ) ) (- 1)) )) +(assert (or (<= (+ (* 25 x0 ) (* 41 x4 ) (* (- 33) x1 ) (* (- 50) x2 ) (* (- 39) x3 ) ) 3) (> (+ (* (- 48) x4 ) (* 13 x0 ) (* 44 x2 ) (* (- 26) x3 ) ) 3) (= (+ (* (- 3) x2 ) (* 48 x1 ) (* 16 x4 ) (* (- 27) x0 ) (* 43 x4 ) (* 16 x2 ) (* 15 x4 ) (* 49 x2 ) (* 35 x4 ) ) (- 30)) )) +(assert (not (>= (+ (* (- 18) x4 ) (* 27 x4 ) ) 12)) ) +(assert (> (+ (* 42 x4 ) (* 10 x1 ) (* (- 3) x2 ) (* (- 38) x0 ) (* 49 x3 ) (* (- 8) x4 ) ) 1) ) +(check-sat) +(pop 1) +(assert (or (not (< (+ (* 27 x0 ) (* (- 19) x4 ) (* (- 7) x2 ) (* 41 x1 ) (* (- 9) x4 ) (* (- 37) x1 ) (* 47 x4 ) (* 3 x0 ) ) 46)) (not (>= (+ (* 45 x2 ) (* 35 x3 ) (* (- 20) x1 ) ) 6)) )) +(check-sat) +(push 1) +(assert (>= (+ (* (- 10) x3 ) (* (- 29) x3 ) (* 39 x3 ) (* (- 6) x0 ) (* 16 x0 ) (* (- 1) x0 ) (* 34 x3 ) (* 24 x0 ) (* (- 44) x1 ) ) (- 41)) ) +(assert (< (+ (* (- 45) x3 ) (* 14 x2 ) (* (- 3) x0 ) (* (- 17) x3 ) (* 3 x2 ) (* (- 8) x2 ) ) (- 8)) ) +(check-sat) +(pop 1) +(assert (or (not (>= (+ (* (- 10) x0 ) (* (- 43) x3 ) (* (- 46) x1 ) (* (- 43) x2 ) (* (- 38) x4 ) (* (- 48) x3 ) (* (- 13) x2 ) (* (- 26) x1 ) (* (- 28) x0 ) (* 22 x3 ) (* 15 x0 ) ) (- 35))) (>= (+ (* 0 x1 ) (* (- 38) x0 ) ) 21) )) +(assert (or (> (+ (* (- 3) x1 ) (* 20 x0 ) (* (- 41) x4 ) (* (- 21) x4 ) (* 40 x1 ) (* 33 x3 ) ) 14) (<= (+ (* (- 27) x0 ) (* (- 45) x2 ) (* (- 20) x4 ) (* (- 46) x2 ) (* 28 x2 ) ) (- 13)) )) +(assert (or (<= (+ (* 14 x2 ) (* (- 14) x2 ) (* 11 x0 ) (* (- 26) x2 ) (* (- 27) x4 ) (* 18 x2 ) (* (- 35) x1 ) (* 17 x0 ) (* (- 28) x3 ) ) (- 26)) (not (> (+ (* (- 3) x1 ) (* (- 37) x3 ) (* (- 41) x3 ) (* (- 50) x3 ) (* (- 30) x2 ) (* (- 36) x0 ) (* (- 8) x3 ) (* 28 x1 ) (* 30 x1 ) (* 24 x1 ) (* (- 11) x3 ) ) 39)) (<= (+ (* 32 x3 ) (* 38 x1 ) (* (- 23) x2 ) (* 32 x3 ) (* 36 x3 ) (* 38 x2 ) (* 19 x2 ) (* (- 46) x0 ) (* (- 30) x0 ) (* (- 39) x1 ) (* 15 x3 ) ) (- 7)) )) +(assert (or (not (<= (+ (* 47 x0 ) (* (- 10) x0 ) (* 14 x2 ) (* (- 49) x4 ) (* 19 x1 ) (* (- 14) x4 ) ) 5)) (>= (+ (* (- 14) x2 ) (* 34 x0 ) (* (- 1) x4 ) (* (- 43) x3 ) (* 41 x4 ) (* 3 x4 ) (* 0 x2 ) (* (- 6) x3 ) (* (- 4) x4 ) (* 33 x0 ) ) (- 40)) (not (> (+ (* (- 29) x0 ) (* 40 x2 ) (* (- 32) x4 ) (* 48 x2 ) (* 37 x2 ) (* (- 34) x2 ) (* (- 20) x1 ) (* 0 x0 ) ) 24)) )) +(assert (or (< (+ (* (- 14) x3 ) (* (- 7) x4 ) (* (- 1) x4 ) ) (- 41)) (< (+ (* (- 2) x0 ) (* 24 x3 ) (* 25 x2 ) (* (- 24) x4 ) (* (- 43) x3 ) (* 49 x4 ) ) 39) )) +(assert (or (= (+ (* 42 x2 ) (* (- 15) x0 ) (* 39 x3 ) (* (- 2) x0 ) (* 41 x0 ) ) (- 46)) (not (<= (+ (* (- 25) x0 ) (* (- 38) x1 ) (* (- 17) x1 ) (* (- 34) x0 ) (* 34 x0 ) (* 31 x2 ) (* 19 x1 ) ) (- 5))) )) +(assert (or (< (+ (* (- 15) x1 ) (* 41 x1 ) (* (- 37) x0 ) (* (- 11) x4 ) (* (- 29) x0 ) (* 6 x1 ) ) 48) (< (+ (* (- 39) x3 ) (* 5 x2 ) ) (- 3)) )) +(assert (or (< (+ (* 37 x4 ) (* (- 24) x2 ) (* 18 x1 ) (* (- 6) x1 ) (* 46 x1 ) (* (- 5) x2 ) (* 18 x0 ) ) (- 32)) (= (+ (* 46 x4 ) (* (- 48) x0 ) (* 38 x4 ) (* 9 x2 ) (* 43 x0 ) (* 33 x4 ) (* 34 x2 ) (* 36 x3 ) (* (- 6) x0 ) (* (- 27) x2 ) (* (- 32) x0 ) ) (- 31)) )) +(assert (or (not (< (+ (* 43 x0 ) (* 4 x0 ) (* 26 x0 ) (* (- 1) x3 ) (* 15 x1 ) (* (- 7) x3 ) (* (- 25) x1 ) (* (- 12) x1 ) ) (- 41))) (< (+ (* 33 x2 ) (* (- 13) x4 ) (* 15 x2 ) ) 37) (not (>= (+ (* 41 x1 ) (* 14 x3 ) ) 47)) )) +(assert (or (not (< (+ (* 0 x3 ) (* (- 16) x4 ) (* 27 x0 ) (* 34 x4 ) (* (- 49) x1 ) (* 30 x2 ) (* 3 x4 ) (* (- 12) x3 ) ) 20)) (> (+ (* 19 x1 ) (* 9 x1 ) (* (- 16) x3 ) (* 23 x4 ) (* (- 9) x2 ) (* (- 35) x1 ) (* (- 18) x1 ) (* 16 x2 ) (* 28 x1 ) ) (- 48)) (not (>= (+ (* 18 x3 ) (* (- 7) x4 ) (* 34 x1 ) (* (- 31) x0 ) ) (- 21))) )) +(check-sat) +(push 1) +(assert (or (not (<= (+ (* 44 x4 ) (* 15 x2 ) (* 9 x2 ) (* 9 x1 ) (* 24 x1 ) ) (- 30))) (<= (+ (* (- 13) x1 ) (* 41 x3 ) ) 1) (= (+ (* 19 x0 ) (* 48 x2 ) (* 33 x2 ) (* 28 x1 ) (* (- 2) x3 ) ) (- 26)) )) +(assert (or (= (+ (* (- 2) x0 ) (* 32 x3 ) (* (- 25) x0 ) ) (- 3)) (= (+ (* 16 x0 ) (* (- 45) x0 ) (* (- 43) x3 ) (* 20 x4 ) (* (- 19) x1 ) ) (- 45)) (not (> (+ (* 35 x2 ) (* (- 7) x2 ) (* 4 x3 ) (* 48 x2 ) (* 15 x4 ) (* (- 4) x2 ) (* 30 x2 ) (* 7 x4 ) (* (- 34) x4 ) (* 42 x0 ) (* 30 x3 ) ) 49)) )) +(assert (> (+ (* (- 7) x0 ) (* 14 x4 ) (* (- 34) x0 ) (* 18 x4 ) (* (- 22) x0 ) (* 26 x3 ) (* 1 x4 ) ) (- 28)) ) +(assert (or (not (= (+ (* 22 x2 ) (* (- 24) x1 ) (* 46 x0 ) (* (- 42) x0 ) (* (- 42) x3 ) (* (- 10) x3 ) ) (- 47))) (not (>= (+ (* (- 34) x4 ) (* 6 x2 ) (* 21 x0 ) (* 41 x3 ) (* (- 43) x4 ) (* 7 x4 ) (* (- 21) x1 ) (* (- 6) x1 ) (* 8 x1 ) ) (- 28))) )) +(assert (>= (+ (* (- 15) x2 ) (* (- 39) x0 ) (* (- 45) x4 ) (* 40 x2 ) (* 49 x3 ) (* (- 32) x2 ) (* (- 18) x2 ) (* (- 2) x4 ) (* (- 9) x4 ) ) (- 45)) ) +(assert (or (not (> (+ (* (- 1) x2 ) (* 33 x2 ) (* (- 50) x3 ) (* 6 x2 ) (* (- 8) x2 ) (* (- 6) x4 ) (* 16 x4 ) (* 23 x4 ) (* 31 x2 ) (* 42 x3 ) (* (- 45) x0 ) ) (- 10))) (> (+ (* 18 x0 ) (* (- 31) x2 ) (* (- 4) x3 ) (* 27 x0 ) (* 18 x4 ) (* (- 27) x0 ) (* 19 x1 ) (* (- 3) x3 ) (* 19 x3 ) ) 15) (> (+ (* (- 12) x1 ) (* (- 3) x2 ) (* (- 31) x0 ) (* 43 x1 ) (* 46 x2 ) (* 36 x3 ) (* 6 x0 ) (* (- 15) x4 ) (* 15 x1 ) (* 18 x0 ) ) 39) )) +(assert (not (< (+ (* 47 x3 ) (* (- 27) x1 ) (* (- 18) x2 ) (* 9 x3 ) (* (- 42) x1 ) (* 37 x3 ) (* (- 2) x1 ) (* (- 36) x0 ) (* 0 x1 ) (* 21 x2 ) (* 10 x2 ) ) (- 14))) ) +(assert (or (not (< (+ (* 10 x1 ) (* 15 x4 ) (* (- 30) x2 ) (* 39 x0 ) (* (- 45) x4 ) (* (- 14) x3 ) (* 29 x3 ) (* 16 x0 ) (* (- 39) x4 ) ) (- 18))) (not (>= (+ (* 1 x3 ) (* (- 25) x2 ) (* 45 x1 ) (* (- 25) x2 ) (* 41 x3 ) (* (- 16) x0 ) (* (- 7) x3 ) ) 4)) (< (+ (* 35 x3 ) (* (- 32) x4 ) (* 24 x4 ) (* 45 x4 ) (* (- 34) x2 ) (* 1 x0 ) (* (- 49) x2 ) (* 39 x4 ) (* (- 48) x1 ) (* 30 x2 ) ) (- 23)) )) +(check-sat) +(pop 1) +(assert (or (not (> (+ (* (- 6) x4 ) (* 34 x4 ) (* (- 45) x4 ) (* (- 5) x2 ) (* 36 x0 ) (* (- 33) x0 ) (* 2 x4 ) (* (- 21) x0 ) (* 24 x3 ) (* (- 19) x3 ) (* (- 43) x1 ) ) (- 38))) (<= (+ (* 49 x0 ) (* (- 19) x2 ) (* (- 4) x4 ) (* (- 49) x2 ) (* 6 x1 ) (* 35 x1 ) (* 36 x3 ) ) (- 26)) )) +(assert (< (+ (* (- 47) x2 ) (* 28 x1 ) (* 29 x0 ) (* 49 x2 ) (* 49 x0 ) (* (- 43) x4 ) (* 3 x0 ) (* (- 5) x3 ) (* 16 x0 ) (* 33 x1 ) ) 24) ) +(check-sat) +(push 1) +(assert (or (> (+ (* (- 27) x4 ) (* (- 23) x3 ) (* (- 23) x2 ) (* 10 x0 ) (* (- 40) x2 ) ) 48) (not (= (+ (* 6 x2 ) (* (- 49) x3 ) (* (- 5) x1 ) ) 3)) (not (> (+ (* (- 3) x4 ) (* (- 31) x3 ) (* 3 x0 ) (* (- 9) x4 ) (* 18 x1 ) (* 8 x1 ) ) 45)) )) +(assert (or (not (< (+ (* (- 40) x2 ) (* (- 29) x3 ) (* (- 32) x3 ) (* 15 x4 ) (* (- 23) x0 ) (* 8 x4 ) (* (- 30) x2 ) (* 26 x3 ) (* (- 2) x1 ) (* (- 14) x1 ) (* 7 x2 ) ) 6)) (not (> (+ (* (- 12) x4 ) (* 30 x4 ) (* 36 x1 ) (* (- 20) x2 ) (* 11 x2 ) ) (- 50))) )) +(assert (or (not (= (+ (* 31 x1 ) (* 34 x3 ) (* (- 31) x2 ) (* (- 12) x0 ) (* 29 x2 ) (* 13 x2 ) (* 16 x2 ) (* (- 42) x3 ) (* 32 x2 ) (* 18 x3 ) ) 18)) (> (+ (* (- 47) x4 ) (* 20 x2 ) (* (- 27) x1 ) ) (- 21)) )) +(assert (> (+ (* 21 x4 ) (* (- 14) x3 ) (* (- 48) x0 ) (* (- 6) x2 ) (* 20 x4 ) (* 28 x4 ) (* 43 x3 ) (* 23 x1 ) (* 47 x1 ) ) (- 49)) ) +(assert (> (+ (* 21 x4 ) (* 45 x2 ) (* 8 x1 ) (* (- 40) x1 ) (* (- 34) x1 ) (* (- 19) x1 ) (* 0 x1 ) ) (- 23)) ) +(assert (< (+ (* (- 34) x2 ) (* (- 45) x4 ) (* 3 x0 ) (* (- 33) x2 ) ) 18) ) +(assert (or (<= (+ (* 25 x2 ) (* (- 30) x0 ) (* 7 x0 ) (* 34 x1 ) (* (- 43) x0 ) (* 18 x4 ) (* (- 43) x4 ) (* 19 x2 ) (* (- 21) x3 ) (* 35 x3 ) (* 5 x4 ) ) (- 12)) (not (> (+ (* (- 33) x2 ) (* 26 x3 ) (* (- 25) x4 ) ) (- 46))) )) +(check-sat) +(pop 1) +(assert (or (not (>= (+ (* (- 38) x3 ) (* (- 6) x4 ) (* (- 19) x4 ) (* (- 45) x1 ) (* (- 46) x2 ) ) 40)) (not (<= (+ (* (- 14) x1 ) (* 45 x3 ) (* (- 42) x4 ) (* 38 x2 ) (* 26 x0 ) (* 32 x0 ) (* 19 x2 ) (* 45 x1 ) (* 11 x1 ) (* (- 38) x2 ) ) (- 45))) )) +(assert (not (> (+ (* 27 x2 ) (* (- 11) x4 ) (* (- 30) x2 ) ) (- 23))) ) +(assert (or (<= (+ (* 44 x2 ) (* (- 26) x3 ) (* (- 13) x1 ) ) 44) (= (+ (* 41 x0 ) (* 13 x4 ) (* (- 15) x2 ) (* (- 41) x4 ) (* (- 36) x4 ) (* 5 x2 ) ) (- 45)) (not (= (+ (* 41 x1 ) (* (- 45) x1 ) (* 38 x3 ) (* 1 x4 ) (* 25 x2 ) (* 8 x4 ) (* 23 x0 ) (* 27 x2 ) ) 15)) )) +(assert (or (= (+ (* (- 42) x3 ) (* 37 x1 ) (* 48 x3 ) (* 41 x4 ) (* (- 18) x0 ) (* (- 2) x2 ) (* (- 32) x2 ) (* (- 14) x1 ) (* (- 49) x4 ) (* 8 x4 ) (* 34 x1 ) ) 34) (not (< (+ (* 4 x3 ) (* (- 8) x0 ) (* (- 10) x1 ) (* 24 x3 ) (* (- 32) x3 ) (* 14 x2 ) (* 4 x4 ) (* (- 6) x1 ) (* (- 16) x3 ) (* 41 x2 ) (* (- 19) x2 ) ) 42)) (< (+ (* (- 24) x2 ) (* (- 14) x2 ) (* (- 15) x2 ) (* (- 31) x0 ) (* 21 x2 ) (* (- 18) x4 ) (* (- 11) x0 ) (* 19 x1 ) ) (- 47)) )) +(check-sat) +(push 1) diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2 new file mode 100644 index 000000000..8da0aeb7e --- /dev/null +++ b/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2 @@ -0,0 +1,50 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXIT: 10 +(set-logic QF_LRA) +(declare-fun x0 () Real) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(declare-fun x3 () Real) +(declare-fun x4 () Real) +(assert (or (= (+ (* 24 x2 ) (* (- 12) x4 ) (* (- 11) x2 ) (* 21 x1 ) ) (- 25)) (not (< (+ (* (- 42) x2 ) (* 19 x2 ) (* (- 48) x1 ) (* 37 x0 ) ) 38)) )) +(assert (< (+ (* (- 40) x2 ) (* 1 x3 ) (* (- 30) x4 ) (* (- 45) x2 ) (* 39 x3 ) ) (- 6)) ) +(assert (or (not (> (+ (* 26 x0 ) (* (- 42) x1 ) (* (- 40) x2 ) (* (- 33) x0 ) (* 1 x2 ) (* (- 5) x4 ) (* 46 x4 ) (* 13 x1 ) (* (- 49) x4 ) (* (- 22) x4 ) (* (- 6) x1 ) ) (- 16))) (not (<= (+ (* 48 x3 ) (* 27 x0 ) (* (- 23) x2 ) (* (- 35) x3 ) ) 37)) (not (<= (+ (* 25 x0 ) (* 16 x1 ) (* 47 x2 ) (* (- 22) x0 ) ) 10)) )) +(assert (>= (+ (* 38 x0 ) (* 6 x1 ) (* (- 48) x1 ) (* (- 27) x4 ) (* 33 x1 ) (* (- 14) x2 ) (* 40 x4 ) (* 26 x3 ) ) 42) ) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (or (<= (+ (* (- 32) x2 ) (* 30 x1 ) (* 41 x2 ) (* (- 37) x1 ) ) (- 21)) (< (+ (* 9 x0 ) (* (- 1) x2 ) (* 48 x1 ) (* (- 47) x0 ) (* (- 22) x4 ) (* 49 x0 ) (* (- 10) x4 ) (* 9 x1 ) (* (- 30) x4 ) (* 38 x2 ) (* 5 x0 ) ) 19) )) +(check-sat) +(push 1) +(assert (or (< (+ (* 9 x4 ) (* 25 x1 ) (* 47 x4 ) (* (- 26) x1 ) (* (- 10) x2 ) (* 28 x3 ) (* (- 37) x2 ) (* (- 22) x2 ) (* 23 x1 ) (* (- 36) x2 ) ) (- 10)) (< (+ (* (- 31) x2 ) (* (- 6) x4 ) (* (- 28) x4 ) (* 13 x0 ) (* 21 x4 ) ) 40) )) +(check-sat) +(pop 1) +(assert (not (> (+ (* (- 44) x3 ) (* (- 40) x3 ) (* (- 46) x4 ) (* (- 1) x4 ) (* 26 x3 ) (* (- 27) x4 ) (* 26 x4 ) (* 21 x4 ) (* 44 x0 ) (* (- 3) x3 ) ) (- 41))) ) +(assert (or (not (< (+ (* 22 x2 ) (* (- 4) x0 ) ) (- 28))) (<= (+ (* 41 x1 ) (* 7 x4 ) ) (- 10)) )) +(assert (not (<= (+ (* (- 21) x2 ) (* (- 6) x3 ) (* (- 24) x3 ) (* (- 17) x1 ) (* 11 x1 ) (* (- 5) x0 ) ) (- 45))) ) +(assert (or (< (+ (* 16 x2 ) (* 48 x3 ) (* 20 x2 ) (* (- 1) x2 ) (* 43 x0 ) (* 15 x0 ) (* (- 33) x0 ) ) 44) (not (<= (+ (* (- 46) x4 ) (* 22 x0 ) (* (- 10) x3 ) (* (- 27) x0 ) (* (- 11) x4 ) (* (- 32) x0 ) (* 17 x3 ) (* (- 39) x4 ) (* (- 8) x3 ) (* (- 25) x1 ) ) (- 7))) )) +(check-sat) +(push 1) +(check-sat) +(pop 1) +(assert (or (not (< (+ (* (- 5) x2 ) (* (- 22) x3 ) (* 2 x0 ) (* 42 x1 ) (* (- 29) x2 ) (* 12 x3 ) (* 16 x3 ) (* (- 19) x0 ) (* (- 42) x0 ) (* (- 6) x1 ) ) 40)) (> (+ (* 27 x2 ) (* (- 28) x2 ) (* 7 x0 ) (* 9 x1 ) (* 14 x2 ) (* 4 x3 ) (* (- 16) x3 ) (* 41 x1 ) ) (- 42)) )) +(assert (or (= (+ (* (- 36) x4 ) (* 5 x0 ) (* 2 x4 ) ) (- 16)) (< (+ (* (- 10) x1 ) (* 13 x3 ) (* 39 x4 ) (* (- 47) x3 ) (* (- 39) x0 ) (* 24 x2 ) (* 5 x2 ) (* (- 45) x2 ) (* 24 x1 ) ) (- 21)) )) +(check-sat) +(push 1) +(assert (or (< (+ (* (- 7) x3 ) (* 35 x2 ) (* (- 42) x1 ) (* 43 x3 ) (* 27 x3 ) (* (- 47) x2 ) (* (- 5) x2 ) (* 13 x0 ) (* 36 x4 ) ) (- 38)) (not (<= (+ (* 27 x0 ) (* 25 x1 ) (* 36 x0 ) (* 46 x2 ) (* (- 9) x2 ) (* 4 x1 ) (* (- 6) x3 ) (* (- 6) x4 ) (* (- 22) x2 ) (* (- 19) x3 ) (* (- 25) x3 ) ) (- 22))) )) +(assert (or (= (+ (* (- 13) x3 ) (* 3 x4 ) (* (- 25) x2 ) (* (- 26) x0 ) ) (- 38)) (< (+ (* 13 x2 ) (* (- 44) x3 ) (* 12 x2 ) (* (- 6) x2 ) (* 25 x2 ) (* 27 x2 ) ) (- 50)) )) +(assert (or (not (= (+ (* (- 18) x4 ) (* (- 31) x1 ) ) (- 13))) (= (+ (* (- 42) x3 ) (* 10 x2 ) (* 29 x0 ) (* 0 x4 ) (* (- 19) x2 ) ) (- 38)) (= (+ (* (- 47) x4 ) (* (- 36) x1 ) (* 11 x1 ) (* (- 50) x1 ) (* 1 x0 ) (* (- 33) x3 ) (* 20 x2 ) (* (- 32) x2 ) (* (- 30) x0 ) (* 42 x2 ) (* (- 21) x1 ) ) 21) )) +(check-sat) +(pop 1) +(check-sat) +(push 1) |