Refactor regressions (#1581)

1 files changed, 95 insertions, 0 deletions

diff --git a/test/regress/regress1/push-pop/arith_lra_02.smt2 b/test/regress/regress1/push-pop/arith_lra_02.smt2
new file mode 100644
index 000000000..3cb5674d1
--- /dev/null
+++ b/test/regress/regress1/push-pop/arith_lra_02.smt2
@@ -0,0 +1,95 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+; 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)
+(assert (or (not (>= (+ (* (- 29) x2 ) (* 3 x2 ) (* 49 x0 ) (* 46 x1 ) (* (- 18) x0 ) (* (- 17) x2 ) (* 35 x0 ) (* 9 x2 ) (* (- 16) x0 ) ) 16)) (= (+ (* 25 x1 ) (* 15 x2 ) (* 27 x4 ) (* 7 x2 ) (* 27 x3 ) (* (- 45) x4 ) ) (- 20)) (not (< (+ (* (- 13) x3 ) (* 47 x3 ) (* 20 x3 ) ) 33)) ))
+(check-sat)
+(assert (or (not (<= (+ (* (- 35) x1 ) (* 11 x4 ) ) (- 21))) (not (< (+ (* 12 x1 ) (* (- 24) x2 ) (* (- 41) x4 ) (* 25 x3 ) (* (- 29) x4 ) ) 41)) ))
+(assert (or (not (>= (+ (* (- 3) x1 ) (* (- 12) x0 ) (* 29 x4 ) ) 0)) (>= (+ (* (- 27) x3 ) (* (- 15) x2 ) (* (- 30) x0 ) (* 29 x0 ) (* 44 x2 ) (* (- 20) x0 ) (* (- 9) x2 ) ) (- 47)) ))
+(check-sat)
+(push 1)
+(assert (or (not (<= (+ (* (- 30) x2 ) (* (- 42) x0 ) (* (- 30) x4 ) (* (- 4) x0 ) (* (- 5) x4 ) (* (- 12) x4 ) (* (- 18) x4 ) (* 15 x0 ) ) 32)) (> (+ (* 44 x2 ) (* (- 37) x0 ) (* (- 35) x0 ) (* (- 1) x3 ) (* 25 x2 ) (* (- 39) x0 ) (* 40 x0 ) (* 7 x4 ) (* (- 20) x2 ) (* 27 x3 ) (* (- 50) x2 ) ) 17) ))
+(check-sat)
+(push 1)
+(assert (or (= (+ (* 47 x4 ) (* (- 1) x1 ) (* 39 x4 ) (* (- 44) x0 ) ) (- 34)) (>= (+ (* 39 x0 ) (* 7 x1 ) (* (- 26) x1 ) (* 48 x1 ) ) 26) ))
+(check-sat)
+(push 1)
+(assert (or (= (+ (* (- 25) x2 ) (* 16 x4 ) (* (- 13) x4 ) (* (- 12) x2 ) ) 29) (not (= (+ (* 13 x2 ) (* (- 33) x1 ) (* (- 18) x2 ) (* 26 x4 ) (* (- 37) x4 ) (* (- 13) x4 ) (* (- 2) x3 ) (* (- 7) x3 ) (* 26 x3 ) (* (- 20) x2 ) (* (- 27) x1 ) ) (- 2))) ))
+(assert (or (>= (+ (* (- 7) x0 ) (* (- 15) x1 ) (* 35 x3 ) ) 11) (= (+ (* (- 21) x0 ) (* (- 1) x4 ) (* 21 x3 ) (* (- 6) x2 ) (* (- 49) x0 ) ) (- 15)) (not (< (+ (* 47 x3 ) (* (- 47) x4 ) (* 3 x0 ) (* 16 x3 ) (* (- 21) x1 ) (* 1 x3 ) (* 16 x2 ) ) (- 25))) ))
+(assert (> (+ (* (- 7) x1 ) (* (- 20) x1 ) (* (- 1) x2 ) (* 24 x3 ) (* (- 14) x4 ) (* 24 x2 ) (* 38 x4 ) (* (- 44) x2 ) (* (- 50) x1 ) ) 22) )
+(assert (not (>= (+ (* 16 x1 ) (* (- 43) x4 ) (* (- 22) x3 ) (* 11 x0 ) (* (- 22) x3 ) (* (- 40) x2 ) (* 25 x2 ) ) (- 13))) )
+(assert (or (not (> (+ (* (- 5) x3 ) (* (- 46) x4 ) (* (- 21) x2 ) (* 29 x1 ) (* 38 x4 ) (* 48 x3 ) ) (- 44))) (not (<= (+ (* (- 13) x0 ) (* (- 42) x3 ) (* 27 x2 ) (* 45 x1 ) (* (- 42) x3 ) (* (- 33) x3 ) ) (- 16))) (not (= (+ (* 21 x3 ) (* 0 x4 ) (* (- 50) x0 ) (* (- 43) x0 ) (* (- 40) x3 ) (* 45 x2 ) (* (- 36) x2 ) (* 2 x2 ) (* 2 x3 ) (* (- 30) x2 ) ) (- 20))) ))
+(assert (or (not (< (+ (* 28 x2 ) (* 21 x4 ) (* 19 x0 ) (* 31 x2 ) (* 45 x1 ) (* 3 x4 ) (* 24 x4 ) ) (- 34))) (not (> (+ (* (- 10) x2 ) (* (- 18) x2 ) (* 49 x3 ) (* (- 27) x2 ) (* (- 30) x3 ) ) 8)) (= (+ (* 42 x1 ) (* (- 18) x3 ) (* (- 23) x3 ) (* 34 x0 ) (* 49 x4 ) (* 30 x0 ) (* (- 44) x4 ) (* 45 x3 ) ) 39) ))
+(assert (or (< (+ (* (- 41) x2 ) (* (- 40) x4 ) (* (- 36) x4 ) (* 7 x4 ) (* (- 5) x3 ) (* 11 x1 ) (* 16 x4 ) (* (- 3) x0 ) ) (- 48)) (= (+ (* 22 x0 ) (* 41 x3 ) (* (- 11) x0 ) (* (- 42) x3 ) (* 18 x0 ) (* (- 7) x4 ) (* (- 5) x2 ) ) (- 45)) (not (< (+ (* (- 11) x2 ) (* (- 30) x4 ) (* (- 25) x2 ) (* 42 x1 ) (* (- 10) x2 ) (* 21 x2 ) (* 5 x3 ) (* (- 19) x3 ) (* (- 35) x1 ) (* 11 x3 ) ) (- 27))) ))
+(assert (or (not (> (+ (* 41 x4 ) (* (- 30) x3 ) (* (- 15) x4 ) (* 35 x1 ) (* 13 x0 ) (* 43 x3 ) ) 6)) (<= (+ (* (- 31) x3 ) (* 4 x2 ) (* 18 x0 ) (* 23 x4 ) (* 43 x0 ) (* (- 39) x4 ) (* (- 1) x2 ) ) (- 28)) (<= (+ (* 32 x1 ) (* (- 47) x1 ) (* (- 17) x4 ) (* 32 x3 ) (* 24 x4 ) (* 15 x0 ) (* (- 22) x2 ) (* 14 x4 ) (* 36 x2 ) (* 2 x0 ) (* (- 35) x2 ) ) (- 5)) ))
+(check-sat)
+(push 1)
+(assert (or (not (= (+ (* (- 33) x3 ) (* 19 x4 ) ) 22)) (<= (+ (* 35 x3 ) (* (- 22) x0 ) (* 9 x0 ) (* (- 16) x1 ) (* 41 x3 ) (* (- 42) x3 ) (* 35 x3 ) ) 25) (not (>= (+ (* (- 8) x1 ) (* 22 x1 ) ) 14)) ))
+(assert (or (< (+ (* 27 x1 ) (* 4 x1 ) ) 12) (<= (+ (* (- 8) x2 ) (* (- 47) x4 ) (* (- 26) x3 ) (* (- 22) x1 ) (* (- 11) x4 ) (* (- 28) x3 ) (* 17 x3 ) (* 1 x0 ) (* 31 x4 ) (* 30 x3 ) ) (- 48)) (not (> (+ (* (- 6) x0 ) (* (- 35) x4 ) (* (- 12) x0 ) (* (- 6) x0 ) (* (- 19) x2 ) ) (- 3))) ))
+(check-sat)
+(push 1)
+(check-sat)
+(push 1)
+(assert (or (<= (+ (* 7 x4 ) (* (- 25) x1 ) (* 49 x3 ) (* (- 10) x0 ) (* 48 x0 ) (* (- 23) x0 ) (* 44 x4 ) (* (- 39) x2 ) (* 24 x4 ) ) 6) (<= (+ (* (- 36) x2 ) (* (- 17) x1 ) (* 18 x1 ) (* (- 27) x0 ) (* 36 x3 ) (* 12 x2 ) (* 21 x1 ) (* 18 x3 ) (* 38 x3 ) (* (- 44) x1 ) (* (- 37) x3 ) ) 2) (= (+ (* (- 18) x2 ) (* 45 x1 ) (* 43 x3 ) (* (- 44) x1 ) ) 28) ))
+(assert (= (+ (* (- 2) x2 ) (* 31 x4 ) (* 20 x1 ) ) (- 1)) )
+(assert (not (> (+ (* 47 x3 ) (* 7 x1 ) (* (- 20) x4 ) (* 42 x0 ) (* (- 20) x2 ) (* (- 12) x2 ) (* (- 34) x3 ) (* (- 35) x2 ) (* 0 x4 ) (* 18 x0 ) ) 49)) )
+(check-sat)
+(pop 1)
+(check-sat)
+(push 1)
+(assert (not (< (+ (* (- 46) x0 ) (* (- 32) x4 ) (* 40 x3 ) (* (- 47) x0 ) (* 27 x0 ) (* 22 x0 ) (* (- 24) x2 ) (* 0 x0 ) (* (- 11) x3 ) ) (- 50))) )
+(check-sat)
+(push 1)
+(assert (or (>= (+ (* 37 x2 ) (* 33 x1 ) (* 29 x1 ) (* (- 48) x4 ) (* 3 x2 ) (* 48 x2 ) (* (- 23) x3 ) (* 44 x2 ) (* 45 x2 ) (* (- 6) x2 ) (* 15 x2 ) ) 34) (not (>= (+ (* (- 11) x1 ) (* (- 23) x0 ) (* (- 32) x0 ) (* 49 x1 ) (* 14 x3 ) (* 43 x3 ) (* (- 23) x1 ) (* 9 x1 ) (* (- 44) x2 ) ) (- 12))) (= (+ (* (- 26) x2 ) (* (- 1) x2 ) (* (- 27) x0 ) (* (- 39) x3 ) (* 49 x4 ) (* (- 26) x0 ) (* (- 3) x3 ) ) 44) ))
+(assert (not (>= (+ (* (- 22) x3 ) (* 41 x4 ) (* 31 x4 ) (* (- 21) x2 ) (* 0 x3 ) (* (- 8) x2 ) (* 9 x4 ) (* (- 34) x1 ) (* (- 8) x4 ) (* 3 x2 ) ) 43)) )
+(check-sat)
+(pop 1)
+(check-sat)
+(pop 1)
+(assert (or (= (+ (* 15 x0 ) (* (- 46) x0 ) (* (- 49) x3 ) (* (- 45) x0 ) (* 26 x1 ) ) 5) (= (+ (* 12 x4 ) (* (- 2) x3 ) (* (- 24) x4 ) (* (- 1) x1 ) (* (- 20) x0 ) ) 23) ))
+(assert (< (+ (* (- 42) x4 ) (* 41 x3 ) (* 1 x2 ) (* (- 1) x3 ) (* (- 26) x2 ) (* 14 x0 ) ) (- 23)) )
+(assert (or (= (+ (* (- 36) x1 ) (* 44 x3 ) (* (- 20) x3 ) (* 39 x4 ) (* (- 19) x2 ) ) (- 15)) (not (>= (+ (* 3 x0 ) (* 49 x3 ) (* (- 49) x1 ) (* (- 37) x0 ) (* 28 x0 ) (* (- 46) x0 ) (* (- 22) x4 ) ) 47)) ))
+(assert (<= (+ (* (- 37) x4 ) (* 10 x3 ) ) 4) )
+(assert (or (not (< (+ (* (- 38) x1 ) (* (- 36) x4 ) ) (- 39))) (not (> (+ (* 42 x1 ) (* 8 x1 ) ) (- 2))) (<= (+ (* (- 38) x4 ) (* (- 1) x2 ) (* 21 x4 ) (* (- 3) x3 ) (* 19 x4 ) (* 25 x2 ) (* 24 x4 ) ) (- 22)) ))
+(check-sat)
+(push 1)
+(assert (or (not (<= (+ (* 23 x3 ) (* 4 x4 ) (* 43 x1 ) (* 19 x2 ) (* 23 x0 ) (* 28 x3 ) (* 48 x3 ) (* (- 12) x1 ) (* 35 x0 ) (* (- 7) x2 ) (* (- 31) x3 ) ) (- 33))) (not (< (+ (* (- 29) x1 ) (* 23 x0 ) (* 20 x3 ) ) (- 4))) (not (>= (+ (* 49 x3 ) (* 3 x3 ) (* (- 18) x2 ) (* (- 3) x3 ) (* 35 x0 ) (* (- 23) x2 ) (* (- 5) x2 ) (* (- 15) x0 ) (* (- 10) x1 ) (* (- 45) x4 ) ) (- 2))) ))
+(check-sat)
+(push 1)
+(check-sat)
+(assert (or (>= (+ (* (- 11) x1 ) (* 38 x4 ) (* (- 29) x1 ) ) (- 21)) (not (>= (+ (* (- 16) x4 ) (* (- 43) x2 ) (* (- 10) x0 ) (* 38 x1 ) (* (- 1) x2 ) (* (- 3) x2 ) ) 25)) ))
+(assert (or (not (< (+ (* (- 45) x4 ) (* (- 9) x0 ) (* (- 29) x2 ) (* (- 35) x1 ) (* (- 40) x2 ) (* 25 x1 ) (* (- 20) x2 ) (* (- 16) x1 ) ) 39)) (= (+ (* (- 10) x4 ) (* 9 x1 ) (* 16 x4 ) ) 5) (not (< (+ (* 34 x4 ) (* 17 x3 ) (* (- 8) x2 ) ) 38)) ))
+(assert (or (not (<= (+ (* 13 x3 ) (* 22 x2 ) (* 1 x4 ) (* 26 x3 ) (* (- 15) x3 ) ) 18)) (> (+ (* (- 49) x3 ) (* 28 x4 ) (* (- 20) x4 ) (* (- 16) x4 ) (* 42 x2 ) (* 36 x2 ) (* 36 x3 ) (* (- 26) x4 ) ) 17) ))
+(assert (or (not (= (+ (* (- 13) x1 ) (* (- 24) x0 ) (* (- 16) x2 ) (* (- 32) x3 ) (* (- 32) x2 ) (* 13 x4 ) (* (- 42) x3 ) (* 12 x3 ) (* 41 x4 ) (* 21 x1 ) (* (- 41) x4 ) ) 8)) (<= (+ (* 24 x1 ) (* 35 x1 ) ) 13) ))
+(assert (< (+ (* (- 21) x0 ) (* (- 41) x4 ) (* (- 15) x2 ) ) 22) )
+(assert (or (not (>= (+ (* (- 34) x0 ) (* (- 9) x1 ) (* 21 x2 ) (* 13 x1 ) (* (- 25) x3 ) (* 4 x4 ) (* (- 45) x0 ) (* 34 x4 ) (* 10 x1 ) ) 32)) (not (> (+ (* (- 10) x2 ) (* 36 x0 ) (* 30 x2 ) (* 46 x3 ) (* (- 34) x1 ) ) 14)) ))
+(assert (not (< (+ (* (- 45) x2 ) (* (- 3) x3 ) (* 38 x0 ) (* (- 44) x2 ) (* 40 x4 ) (* 8 x1 ) ) (- 7))) )
+(assert (not (> (+ (* 36 x3 ) (* 48 x0 ) (* (- 4) x4 ) (* 49 x4 ) (* (- 26) x1 ) (* (- 12) x3 ) (* (- 48) x0 ) ) (- 6))) )
+(check-sat)
+(pop 1)
+(assert (or (>= (+ (* 30 x0 ) (* (- 12) x4 ) (* 39 x4 ) (* (- 12) x0 ) (* (- 12) x2 ) (* 9 x1 ) (* (- 40) x2 ) ) 7) (not (> (+ (* 4 x2 ) (* 2 x2 ) (* 23 x4 ) ) (- 43))) ))
+(check-sat)
+(pop 1)
+(check-sat)
+