1 files changed, 31 insertions, 0 deletions
diff --git a/test/regress/regress1/push-pop/fuzz_3_1.smt2 b/test/regress/regress1/push-pop/fuzz_3_1.smt2
new file mode 100644
index 000000000..bf2d2a8c3
--- /dev/null
+++ b/test/regress/regress1/push-pop/fuzz_3_1.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+(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)