1 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress1/push-pop/fuzz_3_3.smt2 b/test/regress/regress1/push-pop/fuzz_3_3.smt2
new file mode 100644
index 000000000..ec072821c
--- /dev/null
+++ b/test/regress/regress1/push-pop/fuzz_3_3.smt2
@@ -0,0 +1,27 @@
+; 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 (= (+ (* (- 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)