From 6809eb4a11f5cf2188f6492c683c9183045419a3 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Wed, 24 Oct 2012 19:14:01 +0000 Subject: [PATCH] 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 --- .../regress0/push-pop/arith_lra_01.smt2 | 87 +++++++++++++++++++ .../regress0/push-pop/arith_lra_02.smt2 | 76 ++++++++++++++++ 2 files changed, 163 insertions(+) create mode 100644 test/regress/regress0/push-pop/arith_lra_01.smt2 create mode 100644 test/regress/regress0/push-pop/arith_lra_02.smt2 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 index 000000000..4989b9250 --- /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 index 000000000..39db126d0 --- /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) + -- 2.30.2