diff options
Diffstat (limited to 'test/regress/regress1/push-pop/fuzz_5_4.smt2')
| -rw-r--r-- | test/regress/regress1/push-pop/fuzz_5_4.smt2 | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/test/regress/regress1/push-pop/fuzz_5_4.smt2 b/test/regress/regress1/push-pop/fuzz_5_4.smt2 new file mode 100644 index 000000000..5d46d281f --- /dev/null +++ b/test/regress/regress1/push-pop/fuzz_5_4.smt2 @@ -0,0 +1,54 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: sat +(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) |