two smaller random pure LRA push-pop cases that fail

dejan@church:~/workspace/fuzz/problems$ ./check.sh arith_lra_01.smt2
z3:   sat sat sat sat sat sat sat sat sat unsat sat sat sat sat sat unsat sat
cvc4: sat sat sat sat sat sat sat sat sat unsat sat sat sat sat sat unsat unsat
dejan@church:~/workspace/fuzz/problems$ ./check.sh arith_lra_02.smt2
z3:   sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat unsat sat
cvc4: sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat unsat unsat

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

diff --git a/test/regress/regress0/push-pop/arith_lra_02.smt2 b/test/regress/regress0/push-pop/arith_lra_02.smt2
new file mode 100644 (file)
index 0000000..39db126
--- /dev/null
+++ b/test/regress/regress0/push-pop/arith_lra_02.smt2
@@ -0,0 +1,76 @@
+(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)
+