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