regress0/bv/core/bv_eq_diamond15.smtv1.smt2
regress0/bv/core/bv_eq_diamond16.smtv1.smt2
regress0/bv/core/bv_eq_diamond17.smtv1.smt2
- regress0/bv/core/concat-merge-0.cvc
- regress0/bv/core/concat-merge-1.cvc
- regress0/bv/core/concat-merge-2.cvc
- regress0/bv/core/concat-merge-3.cvc
regress0/bv/core/constant_core.smt2
- regress0/bv/core/equality-00.cvc
- regress0/bv/core/equality-01.cvc
- regress0/bv/core/equality-02.cvc
- regress0/bv/core/equality-03.cvc
- regress0/bv/core/equality-03.smtv1.smt2
regress0/bv/core/equality-04.smtv1.smt2
regress0/bv/core/equality-05.smtv1.smt2
regress0/bv/core/ext_con_004_001_1024.smtv1.smt2
- regress0/bv/core/extract-concat-0.cvc
- regress0/bv/core/extract-concat-1.cvc
- regress0/bv/core/extract-concat-10.cvc
- regress0/bv/core/extract-concat-11.cvc
- regress0/bv/core/extract-concat-2.cvc
- regress0/bv/core/extract-concat-3.cvc
- regress0/bv/core/extract-concat-4.cvc
- regress0/bv/core/extract-concat-5.cvc
- regress0/bv/core/extract-concat-6.cvc
- regress0/bv/core/extract-concat-7.cvc
- regress0/bv/core/extract-concat-8.cvc
- regress0/bv/core/extract-concat-9.cvc
- regress0/bv/core/extract-constant.cvc
- regress0/bv/core/extract-extract-0.cvc
- regress0/bv/core/extract-extract-1.cvc
- regress0/bv/core/extract-extract-10.cvc
- regress0/bv/core/extract-extract-11.cvc
- regress0/bv/core/extract-extract-2.cvc
- regress0/bv/core/extract-extract-3.cvc
- regress0/bv/core/extract-extract-4.cvc
- regress0/bv/core/extract-extract-5.cvc
- regress0/bv/core/extract-extract-6.cvc
- regress0/bv/core/extract-extract-7.cvc
- regress0/bv/core/extract-extract-8.cvc
- regress0/bv/core/extract-extract-9.cvc
- regress0/bv/core/extract-whole-0.cvc
- regress0/bv/core/extract-whole-1.cvc
- regress0/bv/core/extract-whole-2.cvc
- regress0/bv/core/extract-whole-3.cvc
- regress0/bv/core/extract-whole-4.cvc
regress0/bv/core/incremental.smtv1.smt2
- regress0/bv/core/slice-01.cvc
- regress0/bv/core/slice-02.cvc
- regress0/bv/core/slice-03.cvc
- regress0/bv/core/slice-04.cvc
- regress0/bv/core/slice-05.cvc
- regress0/bv/core/slice-06.cvc
- regress0/bv/core/slice-07.cvc
- regress0/bv/core/slice-08.cvc
- regress0/bv/core/slice-09.cvc
- regress0/bv/core/slice-10.cvc
- regress0/bv/core/slice-11.cvc
- regress0/bv/core/slice-12.cvc
- regress0/bv/core/slice-13.cvc
- regress0/bv/core/slice-14.cvc
- regress0/bv/core/slice-15.cvc
- regress0/bv/core/slice-16.cvc
- regress0/bv/core/slice-17.cvc
- regress0/bv/core/slice-18.cvc
- regress0/bv/core/slice-19.cvc
- regress0/bv/core/slice-20.cvc
regress0/bv/fuzz07-delta.smtv1.smt2
# Proof checking takes too long. Add this back. FIXME
regress0/bv/fuzz15.delta01.smtv1.smt2
regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
# times out on some CI configs after dt fact vs lemma update #5115
regress0/rels/rel_tc_7.cvc
- regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2
regress0/sets/setel-eq.smt2
regress0/sets/sets-new.smt2
regress0/sets/sets-testlemma-ints.smt2
# lianah: disabled these as the unconstrained terms are no longer
# recognized after implementing the divide-by-zero semantics for bv division:
regress0/unconstrained/bvconcat.smt2
- regress0/unconstrained/bvdiv.smtv1.smt2
- ###
- regress1/arith/arith-int-001.cvc
- regress1/arith/arith-int-002.cvc
- regress1/arith/arith-int-003.cvc
- regress1/arith/arith-int-005.cvc
- regress1/arith/arith-int-006.cvc
- regress1/arith/arith-int-007.cvc
- regress1/arith/arith-int-008.cvc
- regress1/arith/arith-int-009.cvc
- regress1/arith/arith-int-010.cvc
- regress1/arith/arith-int-016.cvc
- regress1/arith/arith-int-017.cvc
- regress1/arith/arith-int-018.cvc
- regress1/arith/arith-int-019.cvc
- regress1/arith/arith-int-020.cvc
- regress1/arith/arith-int-026.cvc
- regress1/arith/arith-int-027.cvc
- regress1/arith/arith-int-028.cvc
- regress1/arith/arith-int-029.cvc
- regress1/arith/arith-int-030.cvc
- regress1/arith/arith-int-031.cvc
- regress1/arith/arith-int-032.cvc
- regress1/arith/arith-int-033.cvc
- regress1/arith/arith-int-034.cvc
- regress1/arith/arith-int-035.cvc
- regress1/arith/arith-int-036.cvc
- regress1/arith/arith-int-037.cvc
- regress1/arith/arith-int-038.cvc
- regress1/arith/arith-int-039.cvc
- regress1/arith/arith-int-040.cvc
- regress1/arith/arith-int-041.cvc
- regress1/arith/arith-int-043.cvc
- regress1/arith/arith-int-044.cvc
- regress1/arith/arith-int-045.cvc
- regress1/arith/arith-int-046.cvc
- regress1/arith/arith-int-049.cvc
- regress1/arith/arith-int-051.cvc
- regress1/arith/arith-int-052.cvc
- regress1/arith/arith-int-053.cvc
- regress1/arith/arith-int-054.cvc
- regress1/arith/arith-int-055.cvc
- regress1/arith/arith-int-056.cvc
- regress1/arith/arith-int-057.cvc
- regress1/arith/arith-int-058.cvc
- regress1/arith/arith-int-059.cvc
- regress1/arith/arith-int-060.cvc
- regress1/arith/arith-int-061.cvc
- regress1/arith/arith-int-062.cvc
- regress1/arith/arith-int-063.cvc
- regress1/arith/arith-int-064.cvc
- regress1/arith/arith-int-065.cvc
- regress1/arith/arith-int-066.cvc
- regress1/arith/arith-int-067.cvc
- regress1/arith/arith-int-068.cvc
- regress1/arith/arith-int-069.cvc
- regress1/arith/arith-int-070.cvc
- regress1/arith/arith-int-071.cvc
- regress1/arith/arith-int-072.cvc
- regress1/arith/arith-int-073.cvc
- regress1/arith/arith-int-074.cvc
- regress1/arith/arith-int-075.cvc
- regress1/arith/arith-int-076.cvc
- regress1/arith/arith-int-077.cvc
- regress1/arith/arith-int-078.cvc
- regress1/arith/arith-int-080.cvc
- regress1/arith/arith-int-081.cvc
- regress1/arith/arith-int-082.cvc
- regress1/arith/arith-int-083.cvc
- regress1/arith/arith-int-086.cvc
- regress1/arith/arith-int-087.cvc
- regress1/arith/arith-int-088.cvc
- regress1/arith/arith-int-089.cvc
- regress1/arith/arith-int-090.cvc
- regress1/arith/arith-int-091.cvc
- regress1/arith/arith-int-092.cvc
- regress1/arith/arith-int-093.cvc
- regress1/arith/arith-int-094.cvc
- regress1/arith/arith-int-095.cvc
- regress1/arith/arith-int-096.cvc
- regress1/arith/arith-int-099.cvc
- regress1/arith/arith-int-100.cvc
regress1/auflia/bug337.smt2
regress1/bug472.smt2
- regress1/bug585.cvc
regress1/bug590.smt2
regress1/bv/bench_38.delta.smt2
- regress1/crash_burn_locusts.smt2
- # regress1/ho/hoa0102.smt2 results in an assertion failure (see issue #1650).
+ # results in an assertion failure (see issue #1650).
regress1/ho/hoa0102.smt2
# unknown after update to commands
regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
- # issue1048-arrays-int-real.smt2 -- different errors on debug and production.
- regress1/issue1048-arrays-int-real.smt2
# slow on some builds after changes to tangent planes
regress1/nl/approx-sqrt-unsat.smt2
# times out after no expand definitions for arithmetic
# does not solve after minor modification to search
regress1/sygus/car_3.lus.sy
regress1/sygus/Base16_1.sy
- regress1/sygus/enum-test.sy
regress1/sygus/inv_gen_fig8.sy
# slow (179 seconds) in debug at 45e489e2
regress1/sygus/unifpi-solve-car_1.lus.sy
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[2:1] @ x[0:0] = x[2:0] );
-
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[4:2] @ x[1:0] = x[4:0] );
-
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[8:4] @ x[3:0] = x[8:0] );
-
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[16:8] @ x[7:0] = x[16:0]);
-
+++ /dev/null
-x, y, z : BITVECTOR(32);
-ASSERT(x = y);
-ASSERT(y = z);
-QUERY(x = z);
\ No newline at end of file
+++ /dev/null
-x, y, z, w: BITVECTOR(32);
-ASSERT(x = y);
-ASSERT(y = z);
-ASSERT(z = w);
-QUERY(x = w);
\ No newline at end of file
+++ /dev/null
-x0, x1, x2, x3 : BITVECTOR(32);
-y0, y1, y2, y3 : BITVECTOR(32);
-
-ASSERT (x0 = x1);
-ASSERT (x1 = x2);
-ASSERT (x2 = x3);
-
-ASSERT (y0 = y1);
-ASSERT (y1 = y2);
-ASSERT (y2 = y3);
-
-ASSERT (x0 = y0);
-
-QUERY (x3 = y3);
-
+++ /dev/null
-x0, x1, x2: BITVECTOR(32);
-y0, y1, y2: BITVECTOR(32);
-a0, a1, a2, a3 : BITVECTOR(32);
-
-ASSERT (a0 = x0 AND x0 = a1) XOR (a0 = y0 AND y0 = a1);
-ASSERT (a1 = x1 AND x1 = a2) XOR (a1 = y1 AND y1 = a2);
-ASSERT (a2 = x2 AND x2 = a3) XOR (a2 = y2 AND y2 = a3);
-
-QUERY (a0 = a3);
-
+++ /dev/null
-(set-option :incremental false)
-(set-info :source "Source unknown")
-(set-info :status unknown)
-(set-info :difficulty "unknown")
-(set-info :category "unknown")
-(set-logic QF_BV)
-(declare-fun x0 () (_ BitVec 32))
-(declare-fun x1 () (_ BitVec 32))
-(declare-fun x2 () (_ BitVec 32))
-(declare-fun y0 () (_ BitVec 32))
-(declare-fun y1 () (_ BitVec 32))
-(declare-fun y2 () (_ BitVec 32))
-(declare-fun a0 () (_ BitVec 32))
-(declare-fun a1 () (_ BitVec 32))
-(declare-fun a2 () (_ BitVec 32))
-(declare-fun a3 () (_ BitVec 32))
-(assert (xor (and (= a0 x0) (= x0 a1)) (and (= a0 y0) (= y0 a1))))
-(assert (xor (and (= a1 x1) (= x1 a2)) (and (= a1 y1) (= y1 a2))))
-(assert (xor (and (= a2 x2) (= x2 a3)) (and (= a2 y2) (= y2 a3))))
-(check-sat-assuming ( (not (= a0 a3)) ))
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[63:32] = x[31:0]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[62:33] = x[30:1]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[60:3] = x[28:0] @ y[31:3]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[59:4] = x[27:0] @ y[31:4]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[61:34] = x[29:2]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[60:35] = x[28:3]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[31:0] = y[31:0]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[30:1] = y[30:1]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[29:2] = y[29:2]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[28:3] = y[28:3]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[62:1] = x[30:0] @ y[31:1]);
+++ /dev/null
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[61:2] = x[29:0] @ y[31:2]);
+++ /dev/null
-QUERY (0bin000111000[6:2] = 0bin01110);
-
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[31:0][31:0] = x[31:0]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[31:0][15:1] = x[15:1]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[7:2][2:2] = x[4:4]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[30:1][28:2][26:3][23:4][19:5][14:6][8:7][0:0] = x[28:28]);
\ No newline at end of file
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[31:0][7:2] = x[7:2]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[31:0][4:4] = x[4:4]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[15:1][14:0] = x[15:1]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[15:1][7:1] = x[8:2]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[15:1][3:2] = x[4:3]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[15:1][3:3] = x[4:4]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[7:2][5:0] = x[7:2]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[7:2][3:1] = x[5:3]);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (0bin0 @ x[31:31] @ x[30:20] @ x[19:10] @ x[9:1] @ x[0:0] @ 0bin0 = 0bin0 @ x @ 0bin0);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[31:31] @ x[30:20] @ x[19:10] @ x[9:1] @ x[0:0] = x);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 = x @ 0bin010101);
-
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ x = 0bin010101 @ x);
+++ /dev/null
-x : BITVECTOR(32);
-QUERY (x[31:0] = x);
-
+++ /dev/null
-x: BITVECTOR(64);
-y, z : BITVECTOR(32);
-ASSERT(x = y @ z);
-QUERY(x[63:32] = y);
-
+++ /dev/null
-x: BITVECTOR(64);
-y, z : BITVECTOR(32);
-ASSERT(x = y @ z);
-QUERY(x[31:0] = z);
-
+++ /dev/null
-x1, x2: BITVECTOR(64);
-y, z : BITVECTOR(32);
-ASSERT(x1 = y @ z);
-ASSERT(x2[63:32] = y);
-ASSERT(x2[31:0] = z);
-QUERY(x1 = x2);
-
+++ /dev/null
-x1: BITVECTOR(64);
-x2: BITVECTOR(32);
-x3: BITVECTOR(16);
-x4: BITVECTOR(8);
-x5: BITVECTOR(4);
-x6: BITVECTOR(2);
-x7: BITVECTOR(1);
-ASSERT(x1 = x2 @ x2);
-ASSERT(x2 = x3 @ x3);
-ASSERT(x3 = x4 @ x4);
-ASSERT(x4 = x5 @ x5);
-ASSERT(x5 = x6 @ x6);
-ASSERT(x6 = x7 @ x7);
-QUERY(x1[0:0] = x7);
-
+++ /dev/null
-x1: BITVECTOR(64);
-x2: BITVECTOR(32);
-x3: BITVECTOR(16);
-x4: BITVECTOR(8);
-x5: BITVECTOR(4);
-x6: BITVECTOR(2);
-x7: BITVECTOR(1);
-ASSERT(x1 = x2 @ x2);
-ASSERT(x2 = x3 @ x3);
-ASSERT(x3 = x4 @ x4);
-ASSERT(x4 = x5 @ x5);
-ASSERT(x5 = x6 @ x6);
-ASSERT(x6 = x7 @ x7);
-QUERY(x1[63:63] = x7);
-
+++ /dev/null
-x1: BITVECTOR(64);
-x2: BITVECTOR(32);
-x3: BITVECTOR(16);
-x4: BITVECTOR(8);
-x5: BITVECTOR(4);
-x6: BITVECTOR(2);
-x7: BITVECTOR(1);
-ASSERT(x1 = x2 @ x2);
-ASSERT(x2 = x3 @ x3);
-ASSERT(x3 = x4 @ x4);
-ASSERT(x4 = x5 @ x5);
-ASSERT(x5 = x6 @ x6);
-ASSERT(x6 = x7 @ x7);
-QUERY(x1[63:63] = x1[0:0]);
-
+++ /dev/null
-x: BITVECTOR(5);
-ASSERT(x[4:1] = x[3:0]);
-QUERY(x[4:4]=x[0:0]);
-
+++ /dev/null
-x: BITVECTOR(5);
-ASSERT(x[4:3] = x[1:0]);
-QUERY(x[4:4]=x[0:0]);
-
+++ /dev/null
-x: BITVECTOR(6);
-ASSERT(x[5:2] = x[3:0]);
-QUERY(x[5:4]=x[1:0]);
-
+++ /dev/null
-x : BITVECTOR(8);
-ASSERT(x[3:0] = 0bin0000);
-ASSERT(x[7:4] = 0bin1111);
-QUERY(x = 0bin11110000);
-
+++ /dev/null
-x : BITVECTOR(8);
-ASSERT(x = 0bin01010101);
-QUERY(x[0:0]@x[2:2]@x[4:4]@x[6:6] = 0bin1111);
-
+++ /dev/null
-x, y: BITVECTOR(8);
-z1, z2: BITVECTOR(4);
-ASSERT(x = 0bin01010101);
-ASSERT(y = 0bin10101010);
-ASSERT(z1 = x[0:0]@x[2:2]@x[4:4]@x[6:6]);
-ASSERT(z2 = y[7:7]@y[5:5]@y[3:3]@y[1:1]);
-QUERY(z1 = z2);
-
+++ /dev/null
-x, y: BITVECTOR(8);
-z1, z2: BITVECTOR(4);
-ASSERT(z1 = x[0:0]@x[2:2]@x[4:4]@x[6:6]);
-ASSERT(z2 = y[7:7]@y[5:5]@y[3:3]@y[1:1]);
-ASSERT(x = 0bin01010101);
-ASSERT(y = 0bin10101010);
-QUERY(z1 = z2);
-
+++ /dev/null
-x: BITVECTOR(16);
-ASSERT(x[15:1] = x[14:0]);
-ASSERT(x[0:0] = 0bin0);
-QUERY(x = 0bin0000000000000000);
-
+++ /dev/null
-x: BITVECTOR(16);
-ASSERT(x[15:15] = 0bin1);
-ASSERT(x[15:1] = x[14:0]);
-QUERY(x = 0bin1111111111111111);
-
+++ /dev/null
-x: BITVECTOR(16);
-ASSERT(x[15:15] = 0bin1);
-ASSERT(x[15:2] = x[13:0]);
-QUERY(x = 0bin1111111111111111);
-
+++ /dev/null
-x: BITVECTOR(16);
-y: BITVECTOR(12);
-ASSERT(y = x[11:0]);
-ASSERT(y = x[15:4]);
-ASSERT(y[3:1] = y[2:0]);
-ASSERT(x[0:0] = 0bin1);
-QUERY(x = 0bin1111111111111111);
-
+++ /dev/null
-x: BITVECTOR(16);
-y: BITVECTOR(12);
-ASSERT(x[0:0] = 0bin1);
-ASSERT(y = x[11:0]);
-ASSERT(y = x[15:4]);
-ASSERT(y[3:1] = y[2:0]);
-QUERY(x = 0bin1111111111111111);
-
+++ /dev/null
-x: BITVECTOR(16);
-y: BITVECTOR(12);
-ASSERT(y = x[11:0]);
-ASSERT(y = x[15:4]);
-ASSERT(y[3:2] = y[1:0]);
-ASSERT(x[1:0] = 0bin01);
-QUERY(x = 0bin0101010101010101);
-
+++ /dev/null
-x1, y1: BITVECTOR(4);
-x2, y2: BITVECTOR(2);
-x3, y3: BITVECTOR(1);
-
-ASSERT(x1 = y1);
-
-ASSERT(x1 = x2 @ x2);
-ASSERT(x2 = x3 @ x3);
-
-ASSERT(y1 = y2 @ y2);
-ASSERT(y2 = y3 @ y3);
-
-QUERY(x3 = y3);
\ No newline at end of file
+++ /dev/null
-; PLACEHOLDER: benchmark to be added
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-23 * x0) + (-23 * x1) + (5 * x2) + (-17 * x3) = 7 ;
-ASSERT (-14 * x0) + (-14 * x1) + (19 * x2) + (-24 * x3) = 29 ;
-ASSERT (-16 * x0) + (-17 * x1) + (8 * x2) + (4 * x3) > -10 ;
-ASSERT (6 * x0) + (-10 * x1) + (-22 * x2) + (-22 * x3) >= 0 ;
-ASSERT (18 * x0) + (0 * x1) + (27 * x2) + (7 * x3) <= -2 ;
-ASSERT (-23 * x0) + (27 * x1) + (24 * x2) + (-23 * x3) > -25 ;
-ASSERT (3 * x0) + (32 * x1) + (15 * x2) + (-21 * x3) >= -10 ;
-ASSERT (-27 * x0) + (-16 * x1) + (21 * x2) + (-2 * x3) < 30 ;
-ASSERT (-25 * x0) + (-18 * x1) + (-23 * x2) + (22 * x3) < -15 ;
-ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (-26 * x3) >= 15 ;
-ASSERT (-8 * x0) + (32 * x1) + (9 * x2) + (17 * x3) > -26;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (17 * x0) + (-23 * x1) + (2 * x2) + (-19 * x3) = -18 ;
-ASSERT (25 * x0) + (23 * x1) + (21 * x2) + (20 * x3) = 2 ;
-ASSERT (-24 * x0) + (-30 * x1) + (-14 * x2) + (13 * x3) <= 15 ;
-ASSERT (-26 * x0) + (7 * x1) + (8 * x2) + (14 * x3) <= 16 ;
-ASSERT (-1 * x0) + (-3 * x1) + (-19 * x2) + (26 * x3) <= -15 ;
-ASSERT (31 * x0) + (19 * x1) + (-19 * x2) + (24 * x3) < -25 ;
-ASSERT (8 * x0) + (-27 * x1) + (22 * x2) + (-20 * x3) < -30 ;
-ASSERT (25 * x0) + (7 * x1) + (-18 * x2) + (-18 * x3) >= -31 ;
-ASSERT (7 * x0) + (-22 * x1) + (-8 * x2) + (-6 * x3) >= -17 ;
-ASSERT (-23 * x0) + (14 * x1) + (23 * x2) + (22 * x3) > -29 ;
-ASSERT (-6 * x0) + (-6 * x1) + (-19 * x2) + (-4 * x3) > -5;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (17 * x0) + (-7 * x1) + (15 * x2) + (21 * x3) = 19 ;
-ASSERT (6 * x0) + (-24 * x1) + (25 * x2) + (-18 * x3) > -25 ;
-ASSERT (-26 * x0) + (-28 * x1) + (-23 * x2) + (0 * x3) < -14 ;
-ASSERT (-12 * x0) + (16 * x1) + (26 * x2) + (-23 * x3) <= 11 ;
-ASSERT (14 * x0) + (6 * x1) + (9 * x2) + (-29 * x3) > 24 ;
-ASSERT (5 * x0) + (-10 * x1) + (21 * x2) + (-26 * x3) > -12 ;
-ASSERT (31 * x0) + (6 * x1) + (30 * x2) + (10 * x3) <= -25 ;
-ASSERT (-18 * x0) + (-25 * x1) + (-24 * x2) + (-30 * x3) >= -18 ;
-ASSERT (29 * x0) + (25 * x1) + (29 * x2) + (-31 * x3) < 6 ;
-ASSERT (21 * x0) + (-27 * x1) + (-28 * x2) + (-15 * x3) >= 25 ;
-ASSERT (-13 * x0) + (10 * x1) + (-7 * x2) + (-10 * x3) <= -4;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (13 * x0) + (0 * x1) + (6 * x2) + (-30 * x3) = -16 ;
-ASSERT (-4 * x0) + (-8 * x1) + (14 * x2) + (-8 * x3) = -11 ;
-ASSERT (-23 * x0) + (-26 * x1) + (4 * x2) + (-6 * x3) <= -2 ;
-ASSERT (-22 * x0) + (-18 * x1) + (-23 * x2) + (5 * x3) < -32 ;
-ASSERT (27 * x0) + (-12 * x1) + (-19 * x2) + (-17 * x3) <= -29 ;
-ASSERT (12 * x0) + (21 * x1) + (-22 * x2) + (15 * x3) > 4 ;
-ASSERT (-15 * x0) + (16 * x1) + (2 * x2) + (-14 * x3) >= -26 ;
-ASSERT (4 * x0) + (4 * x1) + (-21 * x2) + (10 * x3) >= -6 ;
-ASSERT (-6 * x0) + (25 * x1) + (-14 * x2) + (8 * x3) >= -31 ;
-ASSERT (-23 * x0) + (2 * x1) + (-9 * x2) + (19 * x3) <= 10 ;
-ASSERT (21 * x0) + (24 * x1) + (14 * x2) + (-6 * x3) <= 0;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-7 * x0) + (-28 * x1) + (8 * x2) + (29 * x3) = -18 ;
-ASSERT (11 * x0) + (2 * x1) + (4 * x2) + (23 * x3) = 6 ;
-ASSERT (24 * x0) + (-20 * x1) + (23 * x2) + (-2 * x3) = 19 ;
-ASSERT (17 * x0) + (-6 * x1) + (2 * x2) + (-22 * x3) = -31 ;
-ASSERT (16 * x0) + (-7 * x1) + (27 * x2) + (17 * x3) = -8;
-ASSERT (-5 * x0) + (18 * x1) + (3 * x2) + (-1 * x3) <= 29 ;
-ASSERT (9 * x0) + (29 * x1) + (30 * x2) + (23 * x3) >= 21 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-19 * x0) + (17 * x1) + (30 * x2) + (-31 * x3) <= -20 ;
-ASSERT (-3 * x0) + (16 * x1) + (20 * x2) + (-25 * x3) < 28 ;
-ASSERT (11 * x0) + (13 * x1) + (-15 * x2) + (-8 * x3) <= 18 ;
-ASSERT (-21 * x0) + (0 * x1) + (32 * x2) + (7 * x3) > -31 ;
-ASSERT (16 * x0) + (24 * x1) + (8 * x2) + (23 * x3) <= 16 ;
-ASSERT (25 * x0) + (-11 * x1) + (-8 * x2) + (14 * x3) <= 17 ;
-ASSERT (16 * x0) + (-25 * x1) + (-1 * x2) + (13 * x3) < -26;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-12 * x0) + (-15 * x1) + (-31 * x2) + (17 * x3) = -16 ;
-ASSERT (11 * x0) + (-5 * x1) + (-8 * x2) + (-17 * x3) > -4 ;
-ASSERT (-12 * x0) + (-22 * x1) + (9 * x2) + (-20 * x3) >= 32 ;
-ASSERT (24 * x0) + (-32 * x1) + (5 * x2) + (31 * x3) > 20 ;
-ASSERT (-30 * x0) + (-4 * x1) + (-4 * x2) + (0 * x3) >= -20 ;
-ASSERT (-10 * x0) + (18 * x1) + (17 * x2) + (20 * x3) <= 30 ;
-ASSERT (12 * x0) + (-13 * x1) + (4 * x2) + (-27 * x3) > 3;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-16 * x0) + (-21 * x1) + (32 * x2) + (32 * x3) = -19 ;
-ASSERT (-10 * x0) + (-21 * x1) + (13 * x2) + (-7 * x3) = 2 ;
-ASSERT (11 * x0) + (15 * x1) + (-8 * x2) + (-24 * x3) = 29 ;
-ASSERT (3 * x0) + (-28 * x1) + (-14 * x2) + (-18 * x3) < 5 ;
-ASSERT (-18 * x0) + (-13 * x1) + (25 * x2) + (22 * x3) <= -24 ;
-ASSERT (-16 * x0) + (-17 * x1) + (-27 * x2) + (4 * x3) >= -5 ;
-ASSERT (21 * x0) + (13 * x1) + (20 * x2) + (-1 * x3) < 19;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (19 * x0) + (-2 * x1) + (-29 * x2) + (-24 * x3) = 3 ;
-ASSERT (3 * x0) + (11 * x1) + (-14 * x2) + (6 * x3) = 4 ;
-ASSERT (-1 * x0) + (-22 * x1) + (4 * x2) + (5 * x3) = -22;
-ASSERT (8 * x0) + (-8 * x1) + (18 * x2) + (-14 * x3) < -20 ;
-ASSERT (22 * x0) + (27 * x1) + (6 * x2) + (-3 * x3) <= -11 ;
-ASSERT (-23 * x0) + (-29 * x1) + (-27 * x2) + (13 * x3) <= 3 ;
-ASSERT (8 * x0) + (0 * x1) + (28 * x2) + (0 * x3) >= -29 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-13 * x0) + (-4 * x1) + (-20 * x2) + (-26 * x3) = 2 ;
-ASSERT (13 * x0) + (13 * x1) + (-14 * x2) + (26 * x3) = -8 ;
-ASSERT (-13 * x0) + (1 * x1) + (16 * x2) + (4 * x3) = -22 ;
-ASSERT (17 * x0) + (7 * x1) + (32 * x2) + (19 * x3) = 16 ;
-ASSERT (11 * x0) + (-8 * x1) + (-10 * x2) + (-10 * x3) <= -1 ;
-ASSERT (-25 * x0) + (-18 * x1) + (-10 * x2) + (-19 * x3) <= 32 ;
-ASSERT (0 * x0) + (-14 * x1) + (30 * x2) + (-5 * x3) > -13 ;
-ASSERT (2 * x0) + (-17 * x1) + (-13 * x2) + (8 * x3) > 1 ;
-ASSERT (-4 * x0) + (-1 * x1) + (29 * x2) + (-9 * x3) > -8 ;
-ASSERT (-32 * x0) + (26 * x1) + (5 * x2) + (6 * x3) <= -1 ;
-ASSERT (-26 * x0) + (3 * x1) + (22 * x2) + (27 * x3) > -2 ;
-ASSERT (13 * x0) + (3 * x1) + (1 * x2) + (9 * x3) < 24 ;
-ASSERT (-10 * x0) + (22 * x1) + (5 * x2) + (-5 * x3) >= -21 ;
-ASSERT (-20 * x0) + (-28 * x1) + (-11 * x2) + (6 * x3) >= -17 ;
-ASSERT (14 * x0) + (16 * x1) + (-15 * x2) + (17 * x3) < 27 ;
-ASSERT (-23 * x0) + (-4 * x1) + (-19 * x2) + (-23 * x3) < 20 ;
-ASSERT (-8 * x0) + (-5 * x1) + (-17 * x2) + (32 * x3) <= 20;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (23 * x0) + (-4 * x1) + (-26 * x2) + (-1 * x3) = 10 ;
-ASSERT (15 * x0) + (31 * x1) + (31 * x2) + (31 * x3) = 13 ;
-ASSERT (19 * x0) + (-15 * x1) + (25 * x2) + (30 * x3) = 23 ;
-ASSERT (10 * x0) + (-17 * x1) + (15 * x2) + (13 * x3) < 22 ;
-ASSERT (-7 * x0) + (22 * x1) + (8 * x2) + (24 * x3) < 14 ;
-ASSERT (24 * x0) + (-12 * x1) + (0 * x2) + (-25 * x3) <= -19 ;
-ASSERT (-27 * x0) + (17 * x1) + (-20 * x2) + (-25 * x3) >= 11 ;
-ASSERT (3 * x0) + (-12 * x1) + (-18 * x2) + (15 * x3) > -27 ;
-ASSERT (-19 * x0) + (24 * x1) + (9 * x2) + (4 * x3) <= 16 ;
-ASSERT (28 * x0) + (-20 * x1) + (-21 * x2) + (4 * x3) > -13 ;
-ASSERT (-21 * x0) + (-23 * x1) + (-31 * x2) + (-6 * x3) < 6 ;
-ASSERT (-30 * x0) + (8 * x1) + (-22 * x2) + (8 * x3) > 14 ;
-ASSERT (-1 * x0) + (17 * x1) + (-22 * x2) + (-4 * x3) >= 4 ;
-ASSERT (2 * x0) + (-4 * x1) + (10 * x2) + (30 * x3) < -15 ;
-ASSERT (29 * x0) + (27 * x1) + (23 * x2) + (-4 * x3) < 21 ;
-ASSERT (-28 * x0) + (0 * x1) + (19 * x2) + (7 * x3) <= -18 ;
-ASSERT (-20 * x0) + (-7 * x1) + (26 * x2) + (-17 * x3) < 23;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-11 * x0) + (-26 * x1) + (9 * x2) + (32 * x3) = -11 ;
-ASSERT (-5 * x0) + (-11 * x1) + (-10 * x2) + (-31 * x3) = -23 ;
-ASSERT (-12 * x0) + (9 * x1) + (-22 * x2) + (11 * x3) = 11 ;
-ASSERT (-27 * x0) + (8 * x1) + (-28 * x2) + (-7 * x3) = 23 ;
-ASSERT (19 * x0) + (4 * x1) + (5 * x2) + (-10 * x3) >= 2 ;
-ASSERT (-6 * x0) + (-20 * x1) + (30 * x2) + (20 * x3) >= 12 ;
-ASSERT (19 * x0) + (26 * x1) + (-21 * x2) + (18 * x3) <= -21 ;
-ASSERT (8 * x0) + (-29 * x1) + (7 * x2) + (20 * x3) >= 29 ;
-ASSERT (-28 * x0) + (6 * x1) + (11 * x2) + (0 * x3) >= -4 ;
-ASSERT (-20 * x0) + (-30 * x1) + (17 * x2) + (25 * x3) >= 4 ;
-ASSERT (-15 * x0) + (9 * x1) + (9 * x2) + (26 * x3) > 11 ;
-ASSERT (-30 * x0) + (-20 * x1) + (-20 * x2) + (14 * x3) <= -27 ;
-ASSERT (-22 * x0) + (-11 * x1) + (-6 * x2) + (18 * x3) > -13 ;
-ASSERT (-22 * x0) + (-25 * x1) + (22 * x2) + (-24 * x3) <= 1 ;
-ASSERT (-24 * x0) + (22 * x1) + (-28 * x2) + (-14 * x3) >= 18 ;
-ASSERT (17 * x0) + (31 * x1) + (-13 * x2) + (-23 * x3) < -5 ;
-ASSERT (-12 * x0) + (-28 * x1) + (19 * x2) + (-21 * x3) < -27;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (25 * x0) + (6 * x1) + (-30 * x2) + (29 * x3) = -5 ;
-ASSERT (14 * x0) + (16 * x1) + (24 * x2) + (-7 * x3) <= 31 ;
-ASSERT (1 * x0) + (20 * x1) + (14 * x2) + (5 * x3) >= 3 ;
-ASSERT (-5 * x0) + (24 * x1) + (-21 * x2) + (-13 * x3) >= -12 ;
-ASSERT (9 * x0) + (-16 * x1) + (23 * x2) + (-11 * x3) > -5 ;
-ASSERT (-24 * x0) + (26 * x1) + (19 * x2) + (29 * x3) > -27 ;
-ASSERT (-30 * x0) + (31 * x1) + (27 * x2) + (-26 * x3) < 23 ;
-ASSERT (14 * x0) + (1 * x1) + (0 * x2) + (29 * x3) > 21 ;
-ASSERT (-32 * x0) + (-5 * x1) + (27 * x2) + (31 * x3) <= 23 ;
-ASSERT (30 * x0) + (10 * x1) + (30 * x2) + (29 * x3) < -28 ;
-ASSERT (7 * x0) + (-4 * x1) + (-25 * x2) + (0 * x3) > -28 ;
-ASSERT (3 * x0) + (-19 * x1) + (11 * x2) + (-21 * x3) <= 10 ;
-ASSERT (-31 * x0) + (21 * x1) + (24 * x2) + (-17 * x3) >= 21 ;
-ASSERT (-20 * x0) + (19 * x1) + (6 * x2) + (5 * x3) >= -27 ;
-ASSERT (-8 * x0) + (-27 * x1) + (0 * x2) + (13 * x3) >= 12 ;
-ASSERT (-21 * x0) + (7 * x1) + (-26 * x2) + (19 * x3) < -10 ;
-ASSERT (32 * x0) + (-26 * x1) + (-24 * x2) + (14 * x3) < 13;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-32 * x0) + (31 * x1) + (-32 * x2) + (-21 * x3) = 5 ;
-ASSERT (32 * x0) + (5 * x1) + (23 * x2) + (-16 * x3) = 8 ;
-ASSERT (-17 * x0) + (-17 * x1) + (-22 * x2) + (30 * x3) = -5 ;
-ASSERT (30 * x0) + (18 * x1) + (26 * x2) + (6 * x3) = -8 ;
-ASSERT (17 * x0) + (-4 * x1) + (-16 * x2) + (-22 * x3) = 11;
-ASSERT (0 * x0) + (-26 * x1) + (-15 * x2) + (12 * x3) > 7 ;
-ASSERT (-30 * x0) + (4 * x1) + (-1 * x2) + (27 * x3) > 11 ;
-ASSERT (23 * x0) + (12 * x1) + (11 * x2) + (-2 * x3) <= -10 ;
-ASSERT (-26 * x0) + (-8 * x1) + (7 * x2) + (-18 * x3) > 1 ;
-ASSERT (3 * x0) + (0 * x1) + (5 * x2) + (24 * x3) > 2 ;
-ASSERT (-13 * x0) + (15 * x1) + (2 * x2) + (2 * x3) <= 17 ;
-ASSERT (-24 * x0) + (21 * x1) + (-21 * x2) + (-13 * x3) >= -30 ;
-ASSERT (7 * x0) + (-11 * x1) + (2 * x2) + (21 * x3) >= -24 ;
-ASSERT (-15 * x0) + (-1 * x1) + (6 * x2) + (-10 * x3) <= -25 ;
-ASSERT (-21 * x0) + (8 * x1) + (3 * x2) + (-5 * x3) <= 22 ;
-ASSERT (-18 * x0) + (-16 * x1) + (21 * x2) + (20 * x3) >= 9 ;
-ASSERT (-17 * x0) + (-10 * x1) + (-20 * x2) + (16 * x3) >= 3 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (22 * x0) + (25 * x1) + (1 * x2) + (-11 * x3) = 19 ;
-ASSERT (-10 * x0) + (-27 * x1) + (6 * x2) + (6 * x3) = 28 ;
-ASSERT (0 * x0) + (-30 * x1) + (-31 * x2) + (12 * x3) = -21 ;
-ASSERT (29 * x0) + (-6 * x1) + (-12 * x2) + (22 * x3) = -13;
-ASSERT (-7 * x0) + (23 * x1) + (-1 * x2) + (-14 * x3) > -6 ;
-ASSERT (-27 * x0) + (-31 * x1) + (25 * x2) + (-23 * x3) <= 12 ;
-ASSERT (-19 * x0) + (6 * x1) + (0 * x2) + (-28 * x3) > -1 ;
-ASSERT (-12 * x0) + (19 * x1) + (2 * x2) + (-4 * x3) <= 12 ;
-ASSERT (10 * x0) + (-26 * x1) + (7 * x2) + (-6 * x3) < 12 ;
-ASSERT (25 * x0) + (-18 * x1) + (-30 * x2) + (-9 * x3) < -2 ;
-ASSERT (-9 * x0) + (-13 * x1) + (-9 * x2) + (-28 * x3) > 18 ;
-ASSERT (-12 * x0) + (-28 * x1) + (-21 * x2) + (32 * x3) > 18 ;
-ASSERT (-23 * x0) + (-26 * x1) + (-21 * x2) + (-24 * x3) <= 3 ;
-ASSERT (-15 * x0) + (13 * x1) + (-4 * x2) + (-1 * x3) <= 0 ;
-ASSERT (11 * x0) + (-30 * x1) + (3 * x2) + (-6 * x3) >= 3 ;
-ASSERT (28 * x0) + (0 * x1) + (0 * x2) + (-22 * x3) >= 9 ;
-ASSERT (-18 * x0) + (15 * x1) + (-27 * x2) + (31 * x3) < 5 ;
-ASSERT (10 * x0) + (30 * x1) + (-28 * x2) + (27 * x3) <= -1 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (17 * x0) + (29 * x1) + (-11 * x2) + (24 * x3) = 13 ;
-ASSERT (16 * x0) + (-20 * x1) + (-5 * x2) + (12 * x3) = 13 ;
-ASSERT (-12 * x0) + (-3 * x1) + (-19 * x2) + (4 * x3) = -21 ;
-ASSERT (-3 * x0) + (10 * x1) + (-6 * x2) + (-31 * x3) = 21 ;
-ASSERT (10 * x0) + (-14 * x1) + (-12 * x2) + (8 * x3) = 5 ;
-ASSERT (-4 * x0) + (15 * x1) + (29 * x2) + (2 * x3) = -32 ;
-ASSERT (-14 * x0) + (-12 * x1) + (16 * x2) + (-14 * x3) = -8 ;
-ASSERT (-31 * x0) + (14 * x1) + (30 * x2) + (-19 * x3) < -20 ;
-ASSERT (-5 * x0) + (9 * x1) + (11 * x2) + (-32 * x3) < 3 ;
-ASSERT (27 * x0) + (-6 * x1) + (0 * x2) + (30 * x3) <= -20 ;
-ASSERT (-15 * x0) + (-13 * x1) + (-21 * x2) + (-5 * x3) > -8 ;
-ASSERT (19 * x0) + (31 * x1) + (-16 * x2) + (-8 * x3) > -15 ;
-ASSERT (9 * x0) + (-9 * x1) + (-4 * x2) + (-16 * x3) < 21 ;
-ASSERT (24 * x0) + (4 * x1) + (28 * x2) + (-14 * x3) >= -1 ;
-ASSERT (5 * x0) + (23 * x1) + (-22 * x2) + (-28 * x3) >= -21 ;
-ASSERT (-31 * x0) + (14 * x1) + (14 * x2) + (-9 * x3) > -32 ;
-ASSERT (25 * x0) + (-18 * x1) + (21 * x2) + (-17 * x3) < -20 ;
-ASSERT (1 * x0) + (-29 * x1) + (11 * x2) + (-24 * x3) >= -20;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-31 * x0) + (-5 * x1) + (-28 * x2) + (16 * x3) = 10 ;
-ASSERT (3 * x0) + (-20 * x1) + (-11 * x2) + (-2 * x3) = 25 ;
-ASSERT (31 * x0) + (28 * x1) + (-20 * x2) + (15 * x3) = -30;
-ASSERT (15 * x0) + (-16 * x1) + (29 * x2) + (-2 * x3) >= -6 ;
-ASSERT (-29 * x0) + (-17 * x1) + (-7 * x2) + (11 * x3) < 26 ;
-ASSERT (-4 * x0) + (14 * x1) + (-29 * x2) + (-7 * x3) >= 28 ;
-ASSERT (-29 * x0) + (-25 * x1) + (9 * x2) + (-17 * x3) <= -25 ;
-ASSERT (10 * x0) + (-25 * x1) + (28 * x2) + (8 * x3) > 6 ;
-ASSERT (10 * x0) + (17 * x1) + (-1 * x2) + (21 * x3) > 24 ;
-ASSERT (-19 * x0) + (-29 * x1) + (-26 * x2) + (-7 * x3) <= -11 ;
-ASSERT (30 * x0) + (-7 * x1) + (-8 * x2) + (6 * x3) >= -32 ;
-ASSERT (-3 * x0) + (24 * x1) + (30 * x2) + (-30 * x3) >= 19 ;
-ASSERT (-9 * x0) + (5 * x1) + (17 * x2) + (-24 * x3) < -22 ;
-ASSERT (11 * x0) + (-16 * x1) + (-1 * x2) + (26 * x3) >= 1 ;
-ASSERT (-13 * x0) + (5 * x1) + (19 * x2) + (4 * x3) >= 27 ;
-ASSERT (23 * x0) + (4 * x1) + (30 * x2) + (-28 * x3) > 13 ;
-ASSERT (-8 * x0) + (-24 * x1) + (0 * x2) + (22 * x3) < -6 ;
-ASSERT (-1 * x0) + (1 * x1) + (-30 * x2) + (12 * x3) >= -26 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-29 * x0) + (-17 * x1) + (11 * x2) + (1 * x3) = -15 ;
-ASSERT (-13 * x0) + (1 * x1) + (-6 * x2) + (-15 * x3) = 32 ;
-ASSERT (-19 * x0) + (29 * x1) + (27 * x2) + (-8 * x3) = -4 ;
-ASSERT (-28 * x0) + (-15 * x1) + (-20 * x2) + (-1 * x3) = -2 ;
-ASSERT (-2 * x0) + (2 * x1) + (3 * x2) + (-4 * x3) = 16 ;
-ASSERT (31 * x0) + (22 * x1) + (15 * x2) + (28 * x3) = -19 ;
-ASSERT (-32 * x0) + (2 * x1) + (-8 * x2) + (6 * x3) <= -21 ;
-ASSERT (-10 * x0) + (23 * x1) + (-9 * x2) + (-26 * x3) < -7 ;
-ASSERT (-11 * x0) + (-13 * x1) + (-17 * x2) + (-19 * x3) >= -11 ;
-ASSERT (20 * x0) + (11 * x1) + (-11 * x2) + (-7 * x3) <= 14 ;
-ASSERT (17 * x0) + (0 * x1) + (-27 * x2) + (-32 * x3) > -1 ;
-ASSERT (17 * x0) + (-7 * x1) + (18 * x2) + (-29 * x3) > -19 ;
-ASSERT (12 * x0) + (-14 * x1) + (27 * x2) + (5 * x3) <= 23 ;
-ASSERT (-2 * x0) + (-6 * x1) + (-6 * x2) + (19 * x3) < -5 ;
-ASSERT (-3 * x0) + (-10 * x1) + (-30 * x2) + (18 * x3) >= -27 ;
-ASSERT (-18 * x0) + (-25 * x1) + (3 * x2) + (2 * x3) < -25 ;
-ASSERT (-19 * x0) + (16 * x1) + (-11 * x2) + (-26 * x3) >= -24 ;
-ASSERT (-2 * x0) + (21 * x1) + (25 * x2) + (28 * x3) > 10;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-13 * x0) + (26 * x1) + (-11 * x2) + (17 * x3) = 17 ;
-ASSERT (-15 * x0) + (2 * x1) + (-9 * x2) + (17 * x3) = -11 ;
-ASSERT (8 * x0) + (-24 * x1) + (20 * x2) + (23 * x3) = -23 ;
-ASSERT (-2 * x0) + (26 * x1) + (4 * x2) + (31 * x3) < 31 ;
-ASSERT (23 * x0) + (14 * x1) + (-29 * x2) + (-11 * x3) > 14 ;
-ASSERT (-19 * x0) + (-32 * x1) + (11 * x2) + (31 * x3) < -4 ;
-ASSERT (3 * x0) + (13 * x1) + (-19 * x2) + (26 * x3) >= -20 ;
-ASSERT (-6 * x0) + (4 * x1) + (-17 * x2) + (-31 * x3) <= 32 ;
-ASSERT (-13 * x0) + (32 * x1) + (-18 * x2) + (7 * x3) < -27 ;
-ASSERT (-19 * x0) + (6 * x1) + (-28 * x2) + (-15 * x3) >= 30 ;
-ASSERT (30 * x0) + (-24 * x1) + (-10 * x2) + (-4 * x3) >= -9 ;
-ASSERT (-4 * x0) + (4 * x1) + (-27 * x2) + (-17 * x3) < 12 ;
-ASSERT (-21 * x0) + (13 * x1) + (31 * x2) + (4 * x3) >= -16 ;
-ASSERT (-11 * x0) + (30 * x1) + (-20 * x2) + (21 * x3) <= 9 ;
-ASSERT (-12 * x0) + (23 * x1) + (2 * x2) + (12 * x3) <= 18 ;
-ASSERT (30 * x0) + (8 * x1) + (4 * x2) + (-5 * x3) <= -24 ;
-ASSERT (12 * x0) + (22 * x1) + (9 * x2) + (30 * x3) >= -3 ;
-ASSERT (10 * x0) + (15 * x1) + (25 * x2) + (-5 * x3) <= 4;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-21 * x0) + (-24 * x1) + (-31 * x2) + (12 * x3) = -10 ;
-ASSERT (-4 * x0) + (22 * x1) + (9 * x2) + (17 * x3) > -20 ;
-ASSERT (0 * x0) + (22 * x1) + (-11 * x2) + (-22 * x3) <= 26 ;
-ASSERT (17 * x0) + (-11 * x1) + (32 * x2) + (8 * x3) < 20 ;
-ASSERT (-30 * x0) + (24 * x1) + (-30 * x2) + (-12 * x3) >= 19 ;
-ASSERT (-27 * x0) + (5 * x1) + (31 * x2) + (-12 * x3) <= -24 ;
-ASSERT (-12 * x0) + (-23 * x1) + (-27 * x2) + (29 * x3) >= 13 ;
-ASSERT (23 * x0) + (-21 * x1) + (24 * x2) + (-17 * x3) >= -20 ;
-ASSERT (-30 * x0) + (-27 * x1) + (-21 * x2) + (-11 * x3) < -24 ;
-ASSERT (31 * x0) + (-14 * x1) + (-3 * x2) + (-9 * x3) >= 13 ;
-ASSERT (8 * x0) + (-2 * x1) + (-13 * x2) + (23 * x3) < 31 ;
-ASSERT (-1 * x0) + (9 * x1) + (-29 * x2) + (17 * x3) >= -7 ;
-ASSERT (11 * x0) + (-8 * x1) + (-29 * x2) + (-25 * x3) >= -5 ;
-ASSERT (19 * x0) + (-32 * x1) + (27 * x2) + (17 * x3) > 17 ;
-ASSERT (23 * x0) + (-1 * x1) + (-9 * x2) + (-12 * x3) < -25 ;
-ASSERT (16 * x0) + (-22 * x1) + (3 * x2) + (30 * x3) >= 11;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (4 * x0) + (-29 * x1) + (-9 * x2) + (9 * x3) = 8 ;
-ASSERT (-26 * x0) + (-26 * x1) + (26 * x2) + (-18 * x3) = -20 ;
-ASSERT (-15 * x0) + (-4 * x1) + (-28 * x2) + (-25 * x3) = 13 ;
-ASSERT (17 * x0) + (-29 * x1) + (19 * x2) + (-32 * x3) = 26 ;
-ASSERT (20 * x0) + (-29 * x1) + (-32 * x2) + (28 * x3) = -12 ;
-ASSERT (17 * x0) + (18 * x1) + (-18 * x2) + (28 * x3) <= 21 ;
-ASSERT (-28 * x0) + (-17 * x1) + (-15 * x2) + (30 * x3) > -19 ;
-ASSERT (-6 * x0) + (-25 * x1) + (-22 * x2) + (-13 * x3) < -8 ;
-ASSERT (12 * x0) + (8 * x1) + (15 * x2) + (-7 * x3) >= 12 ;
-ASSERT (14 * x0) + (6 * x1) + (3 * x2) + (25 * x3) > 3 ;
-ASSERT (31 * x0) + (5 * x1) + (26 * x2) + (-1 * x3) < -13 ;
-ASSERT (31 * x0) + (-27 * x1) + (15 * x2) + (-16 * x3) >= 11 ;
-ASSERT (20 * x0) + (-20 * x1) + (25 * x2) + (18 * x3) > 18 ;
-ASSERT (-2 * x0) + (-30 * x1) + (25 * x2) + (-9 * x3) < -9 ;
-ASSERT (29 * x0) + (-22 * x1) + (-18 * x2) + (-25 * x3) < -2 ;
-ASSERT (-12 * x0) + (9 * x1) + (17 * x2) + (-16 * x3) > 3;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-14 * x0) + (16 * x1) + (-16 * x2) + (0 * x3) = -8 ;
-ASSERT (3 * x0) + (-20 * x1) + (-12 * x2) + (-3 * x3) = -7 ;
-ASSERT (-28 * x0) + (31 * x1) + (32 * x2) + (-11 * x3) = 0 ;
-ASSERT (-20 * x0) + (-11 * x1) + (-27 * x2) + (-6 * x3) = -6 ;
-ASSERT (-7 * x0) + (-7 * x1) + (17 * x2) + (-25 * x3) <= -15 ;
-ASSERT (8 * x0) + (28 * x1) + (8 * x2) + (7 * x3) > -28 ;
-ASSERT (25 * x0) + (7 * x1) + (-17 * x2) + (-28 * x3) > 5 ;
-ASSERT (-19 * x0) + (0 * x1) + (-20 * x2) + (0 * x3) <= 20 ;
-ASSERT (6 * x0) + (2 * x1) + (29 * x2) + (-19 * x3) <= -3 ;
-ASSERT (-9 * x0) + (-1 * x1) + (-18 * x2) + (32 * x3) > 11 ;
-ASSERT (2 * x0) + (21 * x1) + (0 * x2) + (19 * x3) >= 13 ;
-ASSERT (-26 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) < -24 ;
-ASSERT (-23 * x0) + (22 * x1) + (12 * x2) + (19 * x3) < -27 ;
-ASSERT (-25 * x0) + (-31 * x1) + (28 * x2) + (14 * x3) < 14 ;
-ASSERT (-29 * x0) + (1 * x1) + (26 * x2) + (-27 * x3) < -14 ;
-ASSERT (23 * x0) + (26 * x1) + (-5 * x2) + (6 * x3) <= -19;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-20 * x0) + (-5 * x1) + (30 * x2) + (-24 * x3) = 12 ;
-ASSERT (24 * x0) + (27 * x1) + (18 * x2) + (-5 * x3) = -16 ;
-ASSERT (14 * x0) + (11 * x1) + (17 * x2) + (12 * x3) = -5 ;
-ASSERT (-29 * x0) + (-29 * x1) + (-16 * x2) + (14 * x3) = 10 ;
-ASSERT (30 * x0) + (13 * x1) + (10 * x2) + (24 * x3) = 3 ;
-ASSERT (-20 * x0) + (29 * x1) + (28 * x2) + (27 * x3) < -21 ;
-ASSERT (-31 * x0) + (17 * x1) + (14 * x2) + (-14 * x3) <= 14 ;
-ASSERT (-23 * x0) + (19 * x1) + (28 * x2) + (-2 * x3) > -28 ;
-ASSERT (-23 * x0) + (23 * x1) + (19 * x2) + (25 * x3) > 13 ;
-ASSERT (-32 * x0) + (8 * x1) + (-24 * x2) + (10 * x3) >= -5 ;
-ASSERT (-30 * x0) + (1 * x1) + (-22 * x2) + (12 * x3) >= -30 ;
-ASSERT (8 * x0) + (28 * x1) + (17 * x2) + (-7 * x3) < -20 ;
-ASSERT (-28 * x0) + (-8 * x1) + (27 * x2) + (25 * x3) >= 7 ;
-ASSERT (-15 * x0) + (26 * x1) + (9 * x2) + (15 * x3) > -12 ;
-ASSERT (-3 * x0) + (15 * x1) + (-6 * x2) + (-31 * x3) < -24 ;
-ASSERT (-26 * x0) + (22 * x1) + (16 * x2) + (30 * x3) <= -2;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-3 * x0) + (2 * x1) + (17 * x2) + (-4 * x3) = -17 ;
-ASSERT (5 * x0) + (-4 * x1) + (22 * x2) + (14 * x3) = -15 ;
-ASSERT (8 * x0) + (23 * x1) + (26 * x2) + (-1 * x3) >= -6 ;
-ASSERT (-7 * x0) + (4 * x1) + (9 * x2) + (-30 * x3) > -26 ;
-ASSERT (-14 * x0) + (-31 * x1) + (-18 * x2) + (-5 * x3) <= 6 ;
-ASSERT (15 * x0) + (26 * x1) + (3 * x2) + (-24 * x3) >= 6 ;
-ASSERT (13 * x0) + (0 * x1) + (25 * x2) + (-27 * x3) <= -13 ;
-ASSERT (11 * x0) + (20 * x1) + (-28 * x2) + (8 * x3) < 0 ;
-ASSERT (-10 * x0) + (13 * x1) + (20 * x2) + (19 * x3) >= 29 ;
-ASSERT (12 * x0) + (-9 * x1) + (-16 * x2) + (26 * x3) >= -11 ;
-ASSERT (-2 * x0) + (32 * x1) + (-6 * x2) + (21 * x3) > -31 ;
-ASSERT (-1 * x0) + (-22 * x1) + (-22 * x2) + (-5 * x3) > 29 ;
-ASSERT (-8 * x0) + (19 * x1) + (18 * x2) + (32 * x3) >= 12 ;
-ASSERT (26 * x0) + (16 * x1) + (-25 * x2) + (29 * x3) < 29 ;
-ASSERT (1 * x0) + (-18 * x1) + (11 * x2) + (-10 * x3) > 10 ;
-ASSERT (-21 * x0) + (5 * x1) + (-2 * x2) + (-28 * x3) <= -5;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-9 * x0) + (-21 * x1) + (-25 * x2) + (-1 * x3) = -11 ;
-ASSERT (31 * x0) + (-18 * x1) + (5 * x2) + (-11 * x3) = 10 ;
-ASSERT (15 * x0) + (5 * x1) + (5 * x2) + (19 * x3) = -29 ;
-ASSERT (-9 * x0) + (-23 * x1) + (7 * x2) + (-21 * x3) = 28 ;
-ASSERT (-24 * x0) + (-22 * x1) + (30 * x2) + (-31 * x3) = -24 ;
-ASSERT (-29 * x0) + (-21 * x1) + (26 * x2) + (-13 * x3) < -12 ;
-ASSERT (31 * x0) + (6 * x1) + (-23 * x2) + (30 * x3) < -3 ;
-ASSERT (21 * x0) + (-7 * x1) + (-4 * x2) + (-25 * x3) <= -17 ;
-ASSERT (4 * x0) + (24 * x1) + (21 * x2) + (8 * x3) <= 19 ;
-ASSERT (19 * x0) + (30 * x1) + (14 * x2) + (-23 * x3) > 21 ;
-ASSERT (30 * x0) + (3 * x1) + (-28 * x2) + (25 * x3) <= -27 ;
-ASSERT (0 * x0) + (-17 * x1) + (-9 * x2) + (-8 * x3) <= 31 ;
-ASSERT (-6 * x0) + (-23 * x1) + (21 * x2) + (18 * x3) >= 31;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (12 * x0) + (14 * x1) + (-22 * x2) + (-6 * x3) = 29 ;
-ASSERT (-9 * x0) + (14 * x1) + (-23 * x2) + (-31 * x3) = 4 ;
-ASSERT (-10 * x0) + (7 * x1) + (-23 * x2) + (18 * x3) <= -16 ;
-ASSERT (-12 * x0) + (7 * x1) + (-16 * x2) + (16 * x3) > -31 ;
-ASSERT (10 * x0) + (11 * x1) + (-17 * x2) + (19 * x3) <= 9 ;
-ASSERT (-1 * x0) + (-8 * x1) + (-31 * x2) + (16 * x3) > 20 ;
-ASSERT (-9 * x0) + (18 * x1) + (9 * x2) + (-14 * x3) <= -8 ;
-ASSERT (-9 * x0) + (27 * x1) + (-22 * x2) + (-16 * x3) > 27 ;
-ASSERT (-24 * x0) + (-25 * x1) + (-28 * x2) + (29 * x3) <= -9 ;
-ASSERT (4 * x0) + (13 * x1) + (27 * x2) + (-5 * x3) >= -22 ;
-ASSERT (-20 * x0) + (-14 * x1) + (21 * x2) + (-28 * x3) <= 17 ;
-ASSERT (18 * x0) + (-32 * x1) + (-23 * x2) + (-9 * x3) <= -21 ;
-ASSERT (19 * x0) + (-9 * x1) + (18 * x2) + (-9 * x3) <= -19;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-24 * x0) + (25 * x1) + (28 * x2) + (-31 * x3) = -1 ;
-ASSERT (29 * x0) + (17 * x1) + (-2 * x2) + (-6 * x3) <= 4 ;
-ASSERT (-16 * x0) + (-4 * x1) + (-2 * x2) + (-1 * x3) >= -28 ;
-ASSERT (4 * x0) + (-26 * x1) + (2 * x2) + (-8 * x3) > 7 ;
-ASSERT (-17 * x0) + (-6 * x1) + (11 * x2) + (-9 * x3) > -27 ;
-ASSERT (-25 * x0) + (13 * x1) + (-29 * x2) + (15 * x3) > 2 ;
-ASSERT (32 * x0) + (-10 * x1) + (15 * x2) + (-25 * x3) < -25 ;
-ASSERT (-16 * x0) + (-26 * x1) + (16 * x2) + (3 * x3) > -26 ;
-ASSERT (-14 * x0) + (13 * x1) + (4 * x2) + (-24 * x3) >= -14 ;
-ASSERT (-5 * x0) + (-21 * x1) + (-7 * x2) + (10 * x3) < 0 ;
-ASSERT (0 * x0) + (25 * x1) + (31 * x2) + (30 * x3) <= -25 ;
-ASSERT (-1 * x0) + (2 * x1) + (26 * x2) + (4 * x3) <= 4 ;
-ASSERT (14 * x0) + (23 * x1) + (18 * x2) + (-18 * x3) > 19;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (22 * x0) + (21 * x1) + (-18 * x2) + (21 * x3) = 30 ;
-ASSERT (-31 * x0) + (22 * x1) + (-20 * x2) + (18 * x3) = -32 ;
-ASSERT (12 * x0) + (18 * x1) + (29 * x2) + (17 * x3) = 0 ;
-ASSERT (-8 * x0) + (-10 * x1) + (-27 * x2) + (30 * x3) = 32 ;
-ASSERT (-21 * x0) + (-2 * x1) + (20 * x2) + (-7 * x3) <= -27 ;
-ASSERT (-7 * x0) + (-22 * x1) + (8 * x2) + (20 * x3) > -20 ;
-ASSERT (-10 * x0) + (1 * x1) + (21 * x2) + (-6 * x3) > 10 ;
-ASSERT (-21 * x0) + (-24 * x1) + (-15 * x2) + (4 * x3) <= 11 ;
-ASSERT (-32 * x0) + (10 * x1) + (-21 * x2) + (-17 * x3) <= 5 ;
-ASSERT (7 * x0) + (-19 * x1) + (28 * x2) + (27 * x3) <= 14 ;
-ASSERT (-32 * x0) + (5 * x1) + (26 * x2) + (-23 * x3) < -23 ;
-ASSERT (-28 * x0) + (5 * x1) + (22 * x2) + (25 * x3) < 6 ;
-ASSERT (4 * x0) + (17 * x1) + (11 * x2) + (26 * x3) >= 20;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-1 * x0) + (-24 * x1) + (3 * x2) + (-8 * x3) > -5 ;
-ASSERT (29 * x0) + (17 * x1) + (-26 * x2) + (20 * x3) > 11 ;
-ASSERT (18 * x0) + (15 * x1) + (-27 * x2) + (8 * x3) > -11 ;
-ASSERT (-14 * x0) + (4 * x1) + (27 * x2) + (-9 * x3) < -13 ;
-ASSERT (24 * x0) + (11 * x1) + (17 * x2) + (-15 * x3) > 5 ;
-ASSERT (-28 * x0) + (-1 * x1) + (10 * x2) + (-12 * x3) > -14 ;
-ASSERT (-11 * x0) + (-4 * x1) + (7 * x2) + (-32 * x3) >= 31 ;
-ASSERT (18 * x0) + (32 * x1) + (-24 * x2) + (-19 * x3) <= -6 ;
-ASSERT (-15 * x0) + (23 * x1) + (-19 * x2) + (-12 * x3) < 2 ;
-ASSERT (-21 * x0) + (-8 * x1) + (-30 * x2) + (31 * x3) >= -29 ;
-ASSERT (5 * x0) + (-24 * x1) + (-21 * x2) + (-10 * x3) >= -8 ;
-ASSERT (-31 * x0) + (-26 * x1) + (13 * x2) + (-7 * x3) <= -32 ;
-ASSERT (-18 * x0) + (-11 * x1) + (9 * x2) + (6 * x3) >= 8;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-31 * x0) + (8 * x1) + (16 * x2) + (5 * x3) >= 1 ;
-ASSERT (-30 * x0) + (13 * x1) + (-17 * x2) + (13 * x3) < -24 ;
-ASSERT (-16 * x0) + (-11 * x1) + (-32 * x2) + (-18 * x3) > -29 ;
-ASSERT (32 * x0) + (-2 * x1) + (27 * x2) + (0 * x3) >= -1 ;
-ASSERT (12 * x0) + (-17 * x1) + (21 * x2) + (-3 * x3) <= 1 ;
-ASSERT (-26 * x0) + (29 * x1) + (-13 * x2) + (15 * x3) <= 2;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-21 * x0) + (-23 * x1) + (29 * x2) + (-4 * x3) = 25 ;
-ASSERT (20 * x0) + (-19 * x1) + (3 * x2) + (-1 * x3) <= -8 ;
-ASSERT (2 * x0) + (-22 * x1) + (-30 * x2) + (-9 * x3) >= 17 ;
-ASSERT (21 * x0) + (5 * x1) + (-13 * x2) + (0 * x3) <= 18 ;
-ASSERT (9 * x0) + (-5 * x1) + (30 * x2) + (17 * x3) > -12 ;
-ASSERT (-2 * x0) + (-27 * x1) + (-5 * x2) + (-23 * x3) < 24;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-%%%% down from 24, up from 6, up from 39
-x0, x1, x2, x3 : INT;
-ASSERT (-30 * x0) + (18 * x1) + (17 * x2) + (3 * x3) = 0;
-ASSERT (-25 * x0) + (-16 * x1) + (17 * x2) + (26 * x3) < 23 ;
-ASSERT (-27 * x0) + (9 * x1) + (7 * x2) + (-24 * x3) < -27 ;
-ASSERT (14 * x0) + (-27 * x1) + (-10 * x2) + (16 * x3) >= -23 ;
-ASSERT (14 * x0) + (-27 * x1) + (-3 * x2) + (2 * x3) > -9 ;
-ASSERT (-19 * x0) + (-9 * x1) + (-3 * x2) + (29 * x3) <= 5 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-22 * x0) + (-5 * x1) + (-5 * x2) + (25 * x3) = 22 ;
-ASSERT (2 * x0) + (-25 * x1) + (4 * x2) + (-21 * x3) >= 0 ;
-ASSERT (30 * x0) + (6 * x1) + (-17 * x2) + (-6 * x3) > 8 ;
-ASSERT (28 * x0) + (-17 * x1) + (26 * x2) + (-1 * x3) >= 17 ;
-ASSERT (2 * x0) + (-32 * x1) + (30 * x2) + (10 * x3) < -23 ;
-ASSERT (22 * x0) + (-18 * x1) + (7 * x2) + (28 * x3) < -26;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (2 * x0) + (-6 * x1) + (14 * x2) + (-24 * x3) > 4 ;
-ASSERT (-13 * x0) + (-2 * x1) + (-9 * x2) + (-7 * x3) >= 29 ;
-ASSERT (-11 * x0) + (28 * x1) + (-20 * x2) + (-2 * x3) >= 31;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-15 * x0) + (-20 * x1) + (-32 * x2) + (-16 * x3) = -19 ;
-ASSERT (24 * x0) + (23 * x1) + (22 * x2) + (30 * x3) >= 19 ;
-ASSERT (14 * x0) + (-6 * x1) + (28 * x2) + (-22 * x3) < -16;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-13 * x0) + (7 * x1) + (-3 * x2) + (9 * x3) = -3 ;
-ASSERT (17 * x0) + (-22 * x1) + (-15 * x2) + (-21 * x3) >= 9 ;
-ASSERT (-9 * x0) + (12 * x1) + (23 * x2) + (-24 * x3) >= -30 ;
-ASSERT (-13 * x0) + (-3 * x1) + (-15 * x2) + (32 * x3) <= 26 ;
-ASSERT (-27 * x0) + (9 * x1) + (-21 * x2) + (-5 * x3) < -9 ;
-ASSERT (22 * x0) + (24 * x1) + (-10 * x2) + (-6 * x3) > -1 ;
-ASSERT (20 * x0) + (-24 * x1) + (29 * x2) + (-21 * x3) <= 29 ;
-ASSERT (25 * x0) + (11 * x1) + (8 * x2) + (-5 * x3) < -29 ;
-ASSERT (-12 * x0) + (24 * x1) + (4 * x2) + (27 * x3) < 31;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-25 * x0) + (-23 * x1) + (11 * x2) + (10 * x3) = 7 ;
-ASSERT (32 * x0) + (-15 * x1) + (-1 * x2) + (29 * x3) > -25 ;
-ASSERT (29 * x0) + (-8 * x1) + (22 * x2) + (20 * x3) < 14 ;
-ASSERT (31 * x0) + (-16 * x1) + (-17 * x2) + (-21 * x3) >= 32 ;
-ASSERT (-24 * x0) + (-29 * x1) + (9 * x2) + (14 * x3) <= -4 ;
-ASSERT (13 * x0) + (13 * x1) + (14 * x2) + (5 * x3) <= 25 ;
-ASSERT (5 * x0) + (12 * x1) + (-5 * x2) + (-9 * x3) >= -28 ;
-ASSERT (27 * x0) + (19 * x1) + (6 * x2) + (25 * x3) >= -12 ;
-ASSERT (24 * x0) + (-26 * x1) + (2 * x2) + (0 * x3) >= -25;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-21 * x0) + (21 * x1) + (23 * x2) + (-20 * x3) = -8 ;
-ASSERT (-31 * x0) + (-15 * x1) + (-23 * x2) + (29 * x3) = 17;
-ASSERT (28 * x0) + (30 * x1) + (26 * x2) + (2 * x3) < 8 ;
-ASSERT (17 * x0) + (-11 * x1) + (6 * x2) + (8 * x3) > 11 ;
-ASSERT (20 * x0) + (-14 * x1) + (16 * x2) + (-3 * x3) < 9 ;
-ASSERT (-11 * x0) + (2 * x1) + (4 * x2) + (-4 * x3) < -21 ;
-ASSERT (25 * x0) + (6 * x1) + (-22 * x2) + (8 * x3) <= 7 ;
-ASSERT (-8 * x0) + (9 * x1) + (-13 * x2) + (27 * x3) >= 0 ;
-ASSERT (-16 * x0) + (-8 * x1) + (23 * x2) + (25 * x3) >= -13 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-31 * x0) + (-29 * x1) + (6 * x2) + (8 * x3) = -10 ;
-ASSERT (0 * x0) + (8 * x1) + (-20 * x2) + (12 * x3) = 16 ;
-ASSERT (19 * x0) + (-30 * x1) + (8 * x2) + (-4 * x3) = -17 ;
-ASSERT (-10 * x0) + (26 * x1) + (11 * x2) + (-31 * x3) = -26;
-ASSERT (-22 * x0) + (15 * x1) + (14 * x2) + (3 * x3) <= -3 ;
-ASSERT (-15 * x0) + (7 * x1) + (29 * x2) + (16 * x3) >= -6 ;
-ASSERT (-20 * x0) + (20 * x1) + (31 * x2) + (-24 * x3) <= 14 ;
-ASSERT (2 * x0) + (31 * x1) + (15 * x2) + (-1 * x3) >= -6 ;
-ASSERT (-30 * x0) + (-11 * x1) + (26 * x2) + (6 * x3) >= -30 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-21 * x0) + (-4 * x1) + (-28 * x2) + (-7 * x3) = -23 ;
-ASSERT (-7 * x0) + (-21 * x1) + (29 * x2) + (11 * x3) = 29 ;
-ASSERT (-26 * x0) + (-7 * x1) + (-25 * x2) + (-19 * x3) < -4 ;
-ASSERT (4 * x0) + (14 * x1) + (-16 * x2) + (-32 * x3) >= -16 ;
-ASSERT (10 * x0) + (-9 * x1) + (20 * x2) + (-27 * x3) <= 31 ;
-ASSERT (29 * x0) + (16 * x1) + (25 * x2) + (-1 * x3) < -26 ;
-ASSERT (-29 * x0) + (1 * x1) + (11 * x2) + (32 * x3) < 12 ;
-ASSERT (-4 * x0) + (-22 * x1) + (0 * x2) + (-29 * x3) < 31 ;
-ASSERT (12 * x0) + (-8 * x1) + (-17 * x2) + (-8 * x3) > 8;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-25 * x0) + (23 * x1) + (29 * x2) + (21 * x3) = -2 ;
-ASSERT (1 * x0) + (10 * x1) + (-32 * x2) + (-17 * x3) = -2 ;
-ASSERT (3 * x0) + (-32 * x1) + (-23 * x2) + (13 * x3) = 16 ;
-ASSERT (25 * x0) + (-14 * x1) + (-17 * x2) + (16 * x3) <= 24 ;
-ASSERT (1 * x0) + (-21 * x1) + (2 * x2) + (2 * x3) >= 15 ;
-ASSERT (24 * x0) + (9 * x1) + (23 * x2) + (-2 * x3) >= -26 ;
-%%ASSERT (-25 * x0) + (26 * x1) + (-3 * x2) + (-26 * x3) >= -20 ;
-%%ASSERT (4 * x0) + (23 * x1) + (-24 * x2) + (7 * x3) <= -18 ;
-%%ASSERT (-16 * x0) + (-24 * x1) + (26 * x2) + (1 * x3) > 15 ;
-%%%%ASSERT (1 * x0) + (9 * x1) + (-18 * x2) + (11 * x3) > -3 ;
-%%ASSERT (-9 * x0) + (20 * x1) + (15 * x2) + (4 * x3) < -17 ;
-%%ASSERT (25 * x0) + (-22 * x1) + (-26 * x2) + (-21 * x3) > 17;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-8 * x0) + (10 * x1) + (-25 * x2) + (-10 * x3) = -18 ;
-ASSERT (27 * x0) + (5 * x1) + (8 * x2) + (13 * x3) = -8;
-ASSERT (2 * x0) + (22 * x1) + (-13 * x2) + (16 * x3) <= 17 ;
-ASSERT (18 * x0) + (18 * x1) + (15 * x2) + (-17 * x3) < -13 ;
-ASSERT (-24 * x0) + (-8 * x1) + (31 * x2) + (-25 * x3) > 23 ;
-ASSERT (-13 * x0) + (-22 * x1) + (11 * x2) + (28 * x3) >= -6 ;
-ASSERT (20 * x0) + (-26 * x1) + (-20 * x2) + (-7 * x3) < -5 ;
-ASSERT (-23 * x0) + (8 * x1) + (28 * x2) + (17 * x3) > 23 ;
-ASSERT (32 * x0) + (31 * x1) + (-26 * x2) + (29 * x3) <= -1 ;
-ASSERT (-2 * x0) + (-11 * x1) + (15 * x2) + (17 * x3) > -27 ;
-ASSERT (-13 * x0) + (-30 * x1) + (-25 * x2) + (-18 * x3) <= 24 ;
-ASSERT (23 * x0) + (-4 * x1) + (26 * x2) + (32 * x3) >= 23 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-15 * x0) + (3 * x1) + (31 * x2) + (2 * x3) = -18 ;
-ASSERT (-25 * x0) + (-10 * x1) + (15 * x2) + (29 * x3) = -18 ;
-ASSERT (-17 * x0) + (31 * x1) + (-11 * x2) + (-29 * x3) = -2 ;
-ASSERT (18 * x0) + (11 * x1) + (13 * x2) + (-16 * x3) >= 5 ;
-ASSERT (-28 * x0) + (-30 * x1) + (13 * x2) + (-20 * x3) <= -19 ;
-ASSERT (-10 * x0) + (-20 * x1) + (-13 * x2) + (-4 * x3) < 3 ;
-ASSERT (-30 * x0) + (-5 * x1) + (-15 * x2) + (-1 * x3) > 19 ;
-ASSERT (-8 * x0) + (28 * x1) + (17 * x2) + (23 * x3) <= 30 ;
-ASSERT (-28 * x0) + (-16 * x1) + (-19 * x2) + (-23 * x3) >= 9 ;
-ASSERT (-8 * x0) + (-15 * x1) + (-19 * x2) + (29 * x3) > -28 ;
-ASSERT (-27 * x0) + (-12 * x1) + (-2 * x2) + (-29 * x3) >= -5 ;
-ASSERT (32 * x0) + (-16 * x1) + (29 * x2) + (-12 * x3) < 26;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (31 * x0) + (-19 * x1) + (0 * x2) + (32 * x3) = -14 ;
-ASSERT (12 * x0) + (-25 * x1) + (-32 * x2) + (-18 * x3) = 18 ;
-ASSERT (-6 * x0) + (-21 * x1) + (-11 * x2) + (-10 * x3) = 11 ;
-ASSERT (22 * x0) + (-7 * x1) + (2 * x2) + (-16 * x3) = 16;
-ASSERT (15 * x0) + (-14 * x1) + (29 * x2) + (24 * x3) >= 14 ;
-ASSERT (-26 * x0) + (-6 * x1) + (-13 * x2) + (25 * x3) < -4 ;
-ASSERT (-24 * x0) + (-22 * x1) + (-21 * x2) + (-6 * x3) > -21 ;
-ASSERT (17 * x0) + (-21 * x1) + (25 * x2) + (-13 * x3) >= 16 ;
-ASSERT (14 * x0) + (-25 * x1) + (-22 * x2) + (18 * x3) >= -30 ;
-ASSERT (-27 * x0) + (8 * x1) + (-12 * x2) + (26 * x3) >= 15 ;
-ASSERT (-31 * x0) + (2 * x1) + (19 * x2) + (-11 * x3) >= -27 ;
-ASSERT (32 * x0) + (-29 * x1) + (9 * x2) + (-4 * x3) < 3 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (3 * x0) + (8 * x1) + (26 * x2) + (-17 * x3) = 31 ;
-ASSERT (-14 * x0) + (25 * x1) + (4 * x2) + (-8 * x3) = 15 ;
-ASSERT (-21 * x0) + (26 * x1) + (-10 * x2) + (-28 * x3) = 5;
-ASSERT (2 * x0) + (-15 * x1) + (12 * x2) + (22 * x3) < -22 ;
-ASSERT (10 * x0) + (24 * x1) + (11 * x2) + (-17 * x3) < 17 ;
-ASSERT (26 * x0) + (32 * x1) + (-17 * x2) + (-3 * x3) >= 20 ;
-ASSERT (11 * x0) + (26 * x1) + (-23 * x2) + (22 * x3) <= 32 ;
-ASSERT (-19 * x0) + (22 * x1) + (-21 * x2) + (-28 * x3) <= -5 ;
-ASSERT (-5 * x0) + (-18 * x1) + (10 * x2) + (-27 * x3) < -26 ;
-ASSERT (21 * x0) + (-26 * x1) + (25 * x2) + (-13 * x3) < 15 ;
-ASSERT (22 * x0) + (-2 * x1) + (3 * x2) + (-21 * x3) < 7 ;
-ASSERT (20 * x0) + (-3 * x1) + (27 * x2) + (-21 * x3) < -18 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (16 * x0) + (20 * x1) + (-8 * x2) + (-27 * x3) = -2 ;
-ASSERT (15 * x0) + (9 * x1) + (-1 * x2) + (4 * x3) = 1 ;
-ASSERT (-25 * x0) + (19 * x1) + (-26 * x2) + (-20 * x3) = 22 ;
-ASSERT (-11 * x0) + (28 * x1) + (-16 * x2) + (-15 * x3) = 15 ;
-ASSERT (-11 * x0) + (-25 * x1) + (-16 * x2) + (25 * x3) = -3 ;
-ASSERT (-15 * x0) + (-25 * x1) + (11 * x2) + (-24 * x3) = 29 ;
-ASSERT (-12 * x0) + (-32 * x1) + (-28 * x2) + (-27 * x3) = -7 ;
-ASSERT (16 * x0) + (5 * x1) + (10 * x2) + (-18 * x3) = 18 ;
-ASSERT (-2 * x0) + (5 * x1) + (30 * x2) + (29 * x3) = -29 ;
-ASSERT (-14 * x0) + (-20 * x1) + (21 * x2) + (1 * x3) = 31 ;
-ASSERT (15 * x0) + (-7 * x1) + (-3 * x2) + (-24 * x3) > 3 ;
-ASSERT (-16 * x0) + (-30 * x1) + (-31 * x2) + (16 * x3) > -9 ;
-ASSERT (12 * x0) + (27 * x1) + (-11 * x2) + (-10 * x3) > -6 ;
-ASSERT (0 * x0) + (29 * x1) + (32 * x2) + (9 * x3) <= -24 ;
-ASSERT (11 * x0) + (-7 * x1) + (24 * x2) + (-30 * x3) >= 8 ;
-ASSERT (1 * x0) + (25 * x1) + (29 * x2) + (15 * x3) <= -13 ;
-ASSERT (-25 * x0) + (31 * x1) + (-32 * x2) + (-1 * x3) <= 9 ;
-ASSERT (-22 * x0) + (-23 * x1) + (-4 * x2) + (-12 * x3) > 32 ;
-ASSERT (22 * x0) + (-1 * x1) + (27 * x2) + (-22 * x3) > 20 ;
-ASSERT (-20 * x0) + (-21 * x1) + (1 * x2) + (-32 * x3) >= 16;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (11 * x0) + (22 * x1) + (19 * x2) + (-8 * x3) = 12 ;
-ASSERT (23 * x0) + (-6 * x1) + (-5 * x2) + (26 * x3) = 0 ;
-ASSERT (1 * x0) + (-23 * x1) + (22 * x2) + (10 * x3) = -18 ;
-ASSERT (-13 * x0) + (-17 * x1) + (-8 * x2) + (-16 * x3) = 16 ;
-ASSERT (24 * x0) + (-4 * x1) + (-26 * x2) + (9 * x3) = -26 ;
-ASSERT (24 * x0) + (23 * x1) + (17 * x2) + (-10 * x3) >= 5 ;
-ASSERT (-12 * x0) + (-12 * x1) + (-13 * x2) + (-22 * x3) <= 9 ;
-ASSERT (-7 * x0) + (17 * x1) + (-24 * x2) + (-8 * x3) <= -31 ;
-ASSERT (-28 * x0) + (-10 * x1) + (3 * x2) + (-23 * x3) <= -19 ;
-ASSERT (12 * x0) + (-16 * x1) + (27 * x2) + (-28 * x3) > -27 ;
-ASSERT (-15 * x0) + (-24 * x1) + (12 * x2) + (21 * x3) < 21 ;
-ASSERT (6 * x0) + (31 * x1) + (5 * x2) + (-5 * x3) >= 10 ;
-ASSERT (-7 * x0) + (-20 * x1) + (-9 * x2) + (-32 * x3) >= 7 ;
-ASSERT (3 * x0) + (24 * x1) + (-18 * x2) + (-9 * x3) < -30 ;
-ASSERT (-14 * x0) + (22 * x1) + (22 * x2) + (-22 * x3) < -16 ;
-ASSERT (1 * x0) + (4 * x1) + (10 * x2) + (28 * x3) > -31 ;
-ASSERT (-14 * x0) + (-15 * x1) + (-8 * x2) + (2 * x3) >= 3 ;
-ASSERT (13 * x0) + (-27 * x1) + (-14 * x2) + (28 * x3) < 28 ;
-ASSERT (26 * x0) + (-12 * x1) + (-21 * x2) + (-16 * x3) < -26 ;
-ASSERT (-6 * x0) + (-19 * x1) + (-8 * x2) + (18 * x3) >= 27;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (20 * x0) + (-10 * x1) + (-10 * x2) + (26 * x3) = -9 ;
-ASSERT (10 * x0) + (0 * x1) + (16 * x2) + (7 * x3) = 7 ;
-ASSERT (6 * x0) + (-10 * x1) + (4 * x2) + (23 * x3) = 10;
-ASSERT (-8 * x0) + (12 * x1) + (-19 * x2) + (-17 * x3) >= 21 ;
-ASSERT (-20 * x0) + (6 * x1) + (-12 * x2) + (-31 * x3) > -31 ;
-ASSERT (32 * x0) + (-6 * x1) + (-14 * x2) + (-32 * x3) >= 13 ;
-ASSERT (29 * x0) + (12 * x1) + (17 * x2) + (9 * x3) > 32 ;
-ASSERT (1 * x0) + (21 * x1) + (12 * x2) + (23 * x3) <= 14 ;
-ASSERT (-12 * x0) + (-9 * x1) + (26 * x2) + (26 * x3) < 3 ;
-ASSERT (-8 * x0) + (27 * x1) + (29 * x2) + (-10 * x3) >= 22 ;
-ASSERT (-15 * x0) + (29 * x1) + (29 * x2) + (17 * x3) <= 22 ;
-ASSERT (-4 * x0) + (0 * x1) + (1 * x2) + (-24 * x3) < -24 ;
-ASSERT (25 * x0) + (17 * x1) + (31 * x2) + (-28 * x3) >= -12 ;
-ASSERT (32 * x0) + (8 * x1) + (-3 * x2) + (19 * x3) > -19 ;
-ASSERT (-27 * x0) + (-18 * x1) + (18 * x2) + (22 * x3) > 26 ;
-ASSERT (29 * x0) + (29 * x1) + (4 * x2) + (-6 * x3) >= 8 ;
-ASSERT (-12 * x0) + (17 * x1) + (-22 * x2) + (1 * x3) < 30 ;
-ASSERT (-24 * x0) + (16 * x1) + (-26 * x2) + (-27 * x3) > 29 ;
-ASSERT (9 * x0) + (15 * x1) + (-28 * x2) + (0 * x3) > -2 ;
-ASSERT (-5 * x0) + (30 * x1) + (-21 * x2) + (-6 * x3) >= 12 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-8 * x0) + (-11 * x1) + (27 * x2) + (4 * x3) = 6 ;
-ASSERT (32 * x0) + (27 * x1) + (31 * x2) + (-13 * x3) = 21 ;
-ASSERT (-6 * x0) + (17 * x1) + (-20 * x2) + (11 * x3) < -5 ;
-ASSERT (15 * x0) + (-15 * x1) + (-13 * x2) + (-21 * x3) < 27 ;
-ASSERT (-24 * x0) + (-22 * x1) + (5 * x2) + (22 * x3) < 23 ;
-ASSERT (27 * x0) + (23 * x1) + (-19 * x2) + (20 * x3) >= -8 ;
-ASSERT (27 * x0) + (-27 * x1) + (23 * x2) + (17 * x3) < -5 ;
-ASSERT (-11 * x0) + (-8 * x1) + (14 * x2) + (-10 * x3) <= 1 ;
-ASSERT (12 * x0) + (7 * x1) + (-26 * x2) + (-28 * x3) >= -7 ;
-ASSERT (25 * x0) + (-25 * x1) + (5 * x2) + (32 * x3) > -10 ;
-ASSERT (-29 * x0) + (-24 * x1) + (26 * x2) + (-31 * x3) < -16 ;
-ASSERT (10 * x0) + (29 * x1) + (9 * x2) + (23 * x3) < 13 ;
-ASSERT (-26 * x0) + (6 * x1) + (-14 * x2) + (-21 * x3) > -15 ;
-ASSERT (24 * x0) + (-14 * x1) + (-32 * x2) + (22 * x3) > -31 ;
-ASSERT (-31 * x0) + (-16 * x1) + (-9 * x2) + (-32 * x3) > -19 ;
-ASSERT (-1 * x0) + (17 * x1) + (26 * x2) + (-16 * x3) > -27 ;
-ASSERT (10 * x0) + (-11 * x1) + (-20 * x2) + (-25 * x3) < -30 ;
-ASSERT (-16 * x0) + (9 * x1) + (-10 * x2) + (-8 * x3) < -9 ;
-ASSERT (19 * x0) + (10 * x1) + (18 * x2) + (7 * x3) < -30 ;
-ASSERT (20 * x0) + (-25 * x1) + (-18 * x2) + (-2 * x3) <= -11;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (3 * x0) + (-21 * x1) + (-3 * x2) + (6 * x3) = -18 ;
-ASSERT (-15 * x0) + (19 * x1) + (-21 * x2) + (-29 * x3) = -8 ;
-ASSERT (32 * x0) + (-2 * x1) + (14 * x2) + (5 * x3) = -15 ;
-ASSERT (-16 * x0) + (22 * x1) + (0 * x2) + (-26 * x3) >= 18 ;
-ASSERT (11 * x0) + (-19 * x1) + (10 * x2) + (26 * x3) >= -20 ;
-ASSERT (-25 * x0) + (-24 * x1) + (12 * x2) + (4 * x3) >= -14 ;
-ASSERT (-20 * x0) + (-10 * x1) + (21 * x2) + (23 * x3) >= 28 ;
-ASSERT (6 * x0) + (-31 * x1) + (11 * x2) + (-3 * x3) <= 4 ;
-ASSERT (2 * x0) + (11 * x1) + (-13 * x2) + (-16 * x3) >= 23 ;
-ASSERT (-6 * x0) + (-24 * x1) + (24 * x2) + (7 * x3) <= 14 ;
-ASSERT (0 * x0) + (3 * x1) + (-14 * x2) + (-19 * x3) >= 15 ;
-ASSERT (-31 * x0) + (-27 * x1) + (-32 * x2) + (-28 * x3) <= -15 ;
-ASSERT (-11 * x0) + (3 * x1) + (-6 * x2) + (-5 * x3) < -31 ;
-ASSERT (-2 * x0) + (-21 * x1) + (2 * x2) + (28 * x3) >= 7 ;
-ASSERT (-12 * x0) + (19 * x1) + (-17 * x2) + (-14 * x3) > 11 ;
-ASSERT (32 * x0) + (-29 * x1) + (-12 * x2) + (24 * x3) < -9 ;
-ASSERT (-19 * x0) + (1 * x1) + (8 * x2) + (4 * x3) <= 3 ;
-ASSERT (13 * x0) + (17 * x1) + (22 * x2) + (13 * x3) <= -25 ;
-ASSERT (2 * x0) + (-4 * x1) + (-3 * x2) + (19 * x3) <= -12 ;
-ASSERT (-16 * x0) + (-20 * x1) + (21 * x2) + (-30 * x3) <= 2;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (28 * x0) + (-8 * x1) + (32 * x2) + (-3 * x3) = -18 ;
-ASSERT (-4 * x0) + (5 * x1) + (-2 * x2) + (-17 * x3) > 19 ;
-ASSERT (-9 * x0) + (14 * x1) + (-16 * x2) + (15 * x3) > 18 ;
-ASSERT (-28 * x0) + (-25 * x1) + (-10 * x2) + (-10 * x3) < -10 ;
-ASSERT (19 * x0) + (-4 * x1) + (11 * x2) + (22 * x3) <= -6 ;
-ASSERT (2 * x0) + (32 * x1) + (-16 * x2) + (-29 * x3) > 6 ;
-ASSERT (-7 * x0) + (9 * x1) + (-25 * x2) + (6 * x3) <= 5 ;
-ASSERT (4 * x0) + (-18 * x1) + (-21 * x2) + (12 * x3) >= -32 ;
-ASSERT (-27 * x0) + (11 * x1) + (-3 * x2) + (-6 * x3) < 1 ;
-ASSERT (10 * x0) + (13 * x1) + (11 * x2) + (28 * x3) > -15 ;
-ASSERT (-1 * x0) + (-4 * x1) + (30 * x2) + (6 * x3) > 9 ;
-ASSERT (19 * x0) + (14 * x1) + (17 * x2) + (-8 * x3) <= -21 ;
-ASSERT (-15 * x0) + (20 * x1) + (9 * x2) + (19 * x3) <= 4 ;
-ASSERT (-9 * x0) + (-22 * x1) + (29 * x2) + (-6 * x3) <= 3;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-25 * x0) + (-32 * x1) + (-29 * x2) + (-9 * x3) = -2 ;
-ASSERT (22 * x0) + (10 * x1) + (-18 * x2) + (2 * x3) = -17 ;
-ASSERT (22 * x0) + (6 * x1) + (-9 * x2) + (27 * x3) = 10 ;
-ASSERT (1 * x0) + (-26 * x1) + (27 * x2) + (-19 * x3) = 29 ;
-ASSERT (-13 * x0) + (18 * x1) + (5 * x2) + (22 * x3) < -10 ;
-ASSERT (5 * x0) + (1 * x1) + (4 * x2) + (-7 * x3) > -12 ;
-ASSERT (-30 * x0) + (-12 * x1) + (-22 * x2) + (-32 * x3) <= 1 ;
-ASSERT (-15 * x0) + (19 * x1) + (22 * x2) + (-9 * x3) >= 12 ;
-ASSERT (-6 * x0) + (-16 * x1) + (30 * x2) + (-13 * x3) <= -9 ;
-ASSERT (-3 * x0) + (1 * x1) + (10 * x2) + (7 * x3) < -32 ;
-ASSERT (5 * x0) + (-17 * x1) + (25 * x2) + (-31 * x3) >= -6 ;
-ASSERT (18 * x0) + (28 * x1) + (-6 * x2) + (10 * x3) <= -31 ;
-ASSERT (-11 * x0) + (-25 * x1) + (2 * x2) + (-3 * x3) > -3 ;
-ASSERT (-14 * x0) + (-28 * x1) + (-2 * x2) + (20 * x3) < -25;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-20 * x0) + (-8 * x1) + (5 * x2) + (-7 * x3) = -7 ;
-ASSERT (-30 * x0) + (24 * x1) + (-4 * x2) + (-30 * x3) = 22 ;
-ASSERT (31 * x0) + (-32 * x1) + (27 * x2) + (29 * x3) = 23 ;
-ASSERT (8 * x0) + (-19 * x1) + (-7 * x2) + (0 * x3) <= -1 ;
-ASSERT (-32 * x0) + (30 * x1) + (9 * x2) + (-21 * x3) <= 24 ;
-ASSERT (15 * x0) + (-4 * x1) + (27 * x2) + (-26 * x3) >= 23 ;
-ASSERT (7 * x0) + (26 * x1) + (-16 * x2) + (21 * x3) >= 16 ;
-ASSERT (-24 * x0) + (-17 * x1) + (-9 * x2) + (27 * x3) <= 2 ;
-ASSERT (29 * x0) + (-7 * x1) + (-8 * x2) + (32 * x3) <= -2 ;
-ASSERT (32 * x0) + (31 * x1) + (7 * x2) + (-26 * x3) < 1 ;
-ASSERT (-17 * x0) + (-13 * x1) + (-20 * x2) + (29 * x3) >= -21 ;
-ASSERT (-32 * x0) + (27 * x1) + (-29 * x2) + (-11 * x3) >= -23 ;
-ASSERT (29 * x0) + (-4 * x1) + (21 * x2) + (-16 * x3) < 23 ;
-ASSERT (-15 * x0) + (26 * x1) + (14 * x2) + (13 * x3) <= -29;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-12 * x0) + (20 * x1) + (2 * x2) + (-24 * x3) = 16 ;
-ASSERT (-32 * x0) + (27 * x1) + (1 * x2) + (-3 * x3) = -3 ;
-ASSERT (13 * x0) + (27 * x1) + (-17 * x2) + (25 * x3) <= -17 ;
-ASSERT (27 * x0) + (-30 * x1) + (-16 * x2) + (-3 * x3) > -19 ;
-ASSERT (-18 * x0) + (-25 * x1) + (-5 * x2) + (3 * x3) < -10 ;
-ASSERT (9 * x0) + (-32 * x1) + (30 * x2) + (11 * x3) >= 23 ;
-ASSERT (14 * x0) + (18 * x1) + (-21 * x2) + (-19 * x3) > 9 ;
-ASSERT (28 * x0) + (2 * x1) + (23 * x2) + (17 * x3) < -6 ;
-ASSERT (13 * x0) + (-17 * x1) + (-1 * x2) + (29 * x3) < -22 ;
-ASSERT (-19 * x0) + (22 * x1) + (6 * x2) + (12 * x3) <= -9 ;
-ASSERT (24 * x0) + (-14 * x1) + (31 * x2) + (12 * x3) > -26 ;
-ASSERT (-1 * x0) + (24 * x1) + (-1 * x2) + (-31 * x3) > -21 ;
-ASSERT (-22 * x0) + (28 * x1) + (-27 * x2) + (0 * x3) >= 3 ;
-ASSERT (-28 * x0) + (29 * x1) + (-3 * x2) + (-22 * x3) >= -23;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (0 * x0) + (-16 * x1) + (14 * x2) + (20 * x3) = 1 ;
-ASSERT (-27 * x0) + (-5 * x1) + (-22 * x2) + (-24 * x3) = -7 ;
-ASSERT (-3 * x0) + (-28 * x1) + (-15 * x2) + (7 * x3) = -9 ;
-ASSERT (27 * x0) + (4 * x1) + (-31 * x2) + (-32 * x3) <= -12 ;
-ASSERT (16 * x0) + (6 * x1) + (17 * x2) + (22 * x3) <= 5 ;
-ASSERT (-27 * x0) + (-16 * x1) + (1 * x2) + (23 * x3) >= 9 ;
-ASSERT (21 * x0) + (-28 * x1) + (-26 * x2) + (-26 * x3) <= -25 ;
-ASSERT (-12 * x0) + (-32 * x1) + (-22 * x2) + (-20 * x3) > -32 ;
-ASSERT (26 * x0) + (26 * x1) + (30 * x2) + (4 * x3) < 21 ;
-ASSERT (-22 * x0) + (-21 * x1) + (0 * x2) + (30 * x3) < 13 ;
-ASSERT (13 * x0) + (17 * x1) + (-7 * x2) + (-31 * x3) < 29 ;
-ASSERT (-12 * x0) + (30 * x1) + (1 * x2) + (4 * x3) > -24 ;
-ASSERT (-23 * x0) + (-2 * x1) + (29 * x2) + (11 * x3) > 26 ;
-ASSERT (-18 * x0) + (-16 * x1) + (31 * x2) + (14 * x3) <= 32;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (22 * x0) + (3 * x1) + (-17 * x2) + (-21 * x3) = -9 ;
-ASSERT (-12 * x0) + (-9 * x1) + (-9 * x2) + (-16 * x3) = -12 ;
-ASSERT (-5 * x0) + (16 * x1) + (-15 * x2) + (-13 * x3) > 27 ;
-ASSERT (16 * x0) + (-4 * x1) + (17 * x2) + (-24 * x3) > -9 ;
-ASSERT (3 * x0) + (13 * x1) + (-15 * x2) + (-13 * x3) <= -32 ;
-ASSERT (-18 * x0) + (21 * x1) + (-7 * x2) + (2 * x3) >= 13 ;
-ASSERT (5 * x0) + (11 * x1) + (-11 * x2) + (-11 * x3) <= 9 ;
-ASSERT (-9 * x0) + (8 * x1) + (-25 * x2) + (-14 * x3) >= 10 ;
-ASSERT (17 * x0) + (-29 * x1) + (23 * x2) + (7 * x3) <= -31 ;
-ASSERT (20 * x0) + (0 * x1) + (1 * x2) + (-6 * x3) <= 23 ;
-ASSERT (-25 * x0) + (0 * x1) + (-32 * x2) + (17 * x3) > -14 ;
-ASSERT (6 * x0) + (-30 * x1) + (-11 * x2) + (29 * x3) < 28 ;
-ASSERT (-19 * x0) + (23 * x1) + (-19 * x2) + (3 * x3) >= 7 ;
-ASSERT (29 * x0) + (21 * x1) + (-28 * x2) + (-28 * x3) < 22 ;
-ASSERT (28 * x0) + (25 * x1) + (2 * x2) + (-23 * x3) <= -28;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (1 * x0) + (-1 * x1) + (-16 * x2) + (6 * x3) = -11 ;
-ASSERT (-17 * x0) + (17 * x1) + (-15 * x2) + (24 * x3) = -21 ;
-ASSERT (-31 * x0) + (28 * x1) + (-4 * x2) + (31 * x3) = -32 ;
-ASSERT (1 * x0) + (-12 * x1) + (29 * x2) + (-6 * x3) = 25 ;
-ASSERT (2 * x0) + (7 * x1) + (-24 * x2) + (28 * x3) >= -12 ;
-ASSERT (-23 * x0) + (-22 * x1) + (14 * x2) + (-24 * x3) >= 22 ;
-ASSERT (23 * x0) + (-21 * x1) + (22 * x2) + (26 * x3) >= -4 ;
-ASSERT (25 * x0) + (27 * x1) + (14 * x2) + (5 * x3) <= 9 ;
-ASSERT (16 * x0) + (2 * x1) + (24 * x2) + (-11 * x3) < -32 ;
-ASSERT (0 * x0) + (23 * x1) + (29 * x2) + (-15 * x3) < -14 ;
-ASSERT (5 * x0) + (-12 * x1) + (-7 * x2) + (29 * x3) <= -16 ;
-ASSERT (25 * x0) + (26 * x1) + (14 * x2) + (-2 * x3) <= 13 ;
-ASSERT (-30 * x0) + (19 * x1) + (24 * x2) + (7 * x3) < -23 ;
-ASSERT (24 * x0) + (28 * x1) + (12 * x2) + (-25 * x3) >= -22 ;
-ASSERT (27 * x0) + (-13 * x1) + (-16 * x2) + (-3 * x3) < 24;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (8 * x0) + (-14 * x1) + (0 * x2) + (7 * x3) = 26 ;
-ASSERT (-7 * x0) + (-14 * x1) + (15 * x2) + (31 * x3) = 8 ;
-ASSERT (-4 * x0) + (16 * x1) + (3 * x2) + (-1 * x3) = 12 ;
-ASSERT (2 * x0) + (24 * x1) + (-7 * x2) + (4 * x3) = 24 ;
-ASSERT (26 * x0) + (-8 * x1) + (28 * x2) + (9 * x3) = -12 ;
-ASSERT (19 * x0) + (-3 * x1) + (25 * x2) + (10 * x3) <= -19 ;
-ASSERT (-13 * x0) + (-16 * x1) + (-14 * x2) + (8 * x3) <= 25 ;
-ASSERT (-21 * x0) + (-2 * x1) + (-20 * x2) + (8 * x3) <= -22 ;
-ASSERT (16 * x0) + (4 * x1) + (11 * x2) + (-15 * x3) >= -12 ;
-ASSERT (-24 * x0) + (-8 * x1) + (2 * x2) + (-24 * x3) <= -22 ;
-ASSERT (29 * x0) + (23 * x1) + (-20 * x2) + (8 * x3) > 21 ;
-ASSERT (-24 * x0) + (-28 * x1) + (-23 * x2) + (-24 * x3) < -5 ;
-ASSERT (-1 * x0) + (17 * x1) + (19 * x2) + (-7 * x3) > -5 ;
-ASSERT (24 * x0) + (3 * x1) + (6 * x2) + (10 * x3) <= 15 ;
-ASSERT (27 * x0) + (-11 * x1) + (-8 * x2) + (-22 * x3) > -30;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (14 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) = -18 ;
-ASSERT (-11 * x0) + (12 * x1) + (8 * x2) + (-1 * x3) = -32 ;
-ASSERT (24 * x0) + (-10 * x1) + (19 * x2) + (7 * x3) = -30 ;
-ASSERT (1 * x0) + (-12 * x1) + (-13 * x2) + (-17 * x3) = -28 ;
-ASSERT (-17 * x0) + (14 * x1) + (7 * x2) + (-18 * x3) = -14 ;
-ASSERT (7 * x0) + (14 * x1) + (-22 * x2) + (29 * x3) = -6;
-ASSERT (15 * x0) + (-6 * x1) + (3 * x2) + (-19 * x3) > 26 ;
-ASSERT (-20 * x0) + (-18 * x1) + (-24 * x2) + (5 * x3) >= -1 ;
-ASSERT (11 * x0) + (-26 * x1) + (-20 * x2) + (-16 * x3) > -7 ;
-ASSERT (31 * x0) + (-2 * x1) + (6 * x2) + (32 * x3) > -22 ;
-ASSERT (-25 * x0) + (26 * x1) + (-26 * x2) + (-21 * x3) >= -27 ;
-ASSERT (-17 * x0) + (-30 * x1) + (14 * x2) + (17 * x3) <= -19 ;
-ASSERT (-16 * x0) + (4 * x1) + (1 * x2) + (-24 * x3) <= -24 ;
-ASSERT (-13 * x0) + (29 * x1) + (-27 * x2) + (12 * x3) < -15 ;
-ASSERT (26 * x0) + (-2 * x1) + (-28 * x2) + (20 * x3) < -20 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-8 * x0) + (29 * x1) + (15 * x2) + (32 * x3) = 32 ;
-ASSERT (18 * x0) + (-8 * x1) + (18 * x2) + (22 * x3) = 20 ;
-ASSERT (11 * x0) + (9 * x1) + (32 * x2) + (-15 * x3) > 21 ;
-ASSERT (12 * x0) + (1 * x1) + (25 * x2) + (-17 * x3) > -13 ;
-ASSERT (-20 * x0) + (7 * x1) + (13 * x2) + (-15 * x3) <= -3 ;
-ASSERT (32 * x0) + (4 * x1) + (-30 * x2) + (13 * x3) <= -15 ;
-ASSERT (-32 * x0) + (-27 * x1) + (20 * x2) + (22 * x3) <= -28 ;
-ASSERT (28 * x0) + (23 * x1) + (10 * x2) + (20 * x3) < 9 ;
-ASSERT (-30 * x0) + (-32 * x1) + (-28 * x2) + (-30 * x3) > 17 ;
-ASSERT (-26 * x0) + (14 * x1) + (30 * x2) + (31 * x3) < 20 ;
-ASSERT (21 * x0) + (23 * x1) + (-7 * x2) + (-16 * x3) > -19 ;
-ASSERT (6 * x0) + (0 * x1) + (0 * x2) + (21 * x3) < -1 ;
-ASSERT (13 * x0) + (29 * x1) + (17 * x2) + (-29 * x3) < -32 ;
-ASSERT (22 * x0) + (-9 * x1) + (-25 * x2) + (11 * x3) > 29 ;
-ASSERT (-25 * x0) + (-19 * x1) + (22 * x2) + (-27 * x3) >= 10;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (29 * x3) = -15 ;
-ASSERT (3 * x0) + (19 * x1) + (21 * x2) + (-32 * x3) = 11 ;
-ASSERT (-23 * x0) + (-8 * x1) + (-12 * x2) + (-14 * x3) >= -25 ;
-ASSERT (13 * x0) + (30 * x1) + (-12 * x2) + (22 * x3) < -12 ;
-ASSERT (-12 * x0) + (-17 * x1) + (20 * x2) + (14 * x3) > -26 ;
-ASSERT (-13 * x0) + (-17 * x1) + (-25 * x2) + (27 * x3) <= -29 ;
-ASSERT (-8 * x0) + (-31 * x1) + (-3 * x2) + (-22 * x3) > -22 ;
-ASSERT (30 * x0) + (11 * x1) + (-32 * x2) + (32 * x3) >= 28;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (26 * x0) + (-28 * x1) + (27 * x2) + (8 * x3) = 31 ;
-ASSERT (-32 * x0) + (11 * x1) + (-5 * x2) + (14 * x3) = 2;
-ASSERT (3 * x0) + (17 * x1) + (30 * x2) + (31 * x3) < 13 ;
-ASSERT (-17 * x0) + (-21 * x1) + (10 * x2) + (8 * x3) > 23 ;
-ASSERT (-14 * x0) + (10 * x1) + (11 * x2) + (27 * x3) > -13 ;
-ASSERT (-14 * x0) + (24 * x1) + (3 * x2) + (-26 * x3) > 1 ;
-ASSERT (-14 * x0) + (20 * x1) + (-2 * x2) + (-24 * x3) > -26 ;
-ASSERT (20 * x0) + (-23 * x1) + (30 * x2) + (-30 * x3) < 24 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (17 * x0) + (-14 * x1) + (13 * x2) + (13 * x3) = -18 ;
-ASSERT (13 * x0) + (16 * x1) + (-12 * x2) + (19 * x3) = -20 ;
-ASSERT (-28 * x0) + (20 * x1) + (-9 * x2) + (9 * x3) = -3 ;
-ASSERT (24 * x0) + (22 * x1) + (24 * x2) + (20 * x3) = 5;
-ASSERT (-1 * x0) + (-12 * x1) + (20 * x2) + (26 * x3) >= 22 ;
-ASSERT (-23 * x0) + (-20 * x1) + (-8 * x2) + (1 * x3) < 2 ;
-ASSERT (5 * x0) + (-27 * x1) + (-24 * x2) + (25 * x3) > -21 ;
-ASSERT (1 * x0) + (-8 * x1) + (-17 * x2) + (-27 * x3) < -24 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (5 * x0) + (-17 * x1) + (15 * x2) + (-15 * x3) = -14 ;
-ASSERT (-28 * x0) + (-17 * x1) + (-29 * x2) + (-19 * x3) = 14;
-ASSERT (9 * x0) + (-26 * x1) + (-16 * x2) + (-9 * x3) >= 28 ;
-ASSERT (14 * x0) + (-32 * x1) + (-31 * x2) + (0 * x3) >= 30 ;
-ASSERT (-31 * x0) + (-27 * x1) + (23 * x2) + (4 * x3) >= 21 ;
-ASSERT (27 * x0) + (-30 * x1) + (8 * x2) + (13 * x3) < 31 ;
-ASSERT (-1 * x0) + (-29 * x1) + (23 * x2) + (10 * x3) < -10 ;
-ASSERT (15 * x0) + (-2 * x1) + (22 * x2) + (-28 * x3) >= 2 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-8 * x0) + (31 * x1) + (-23 * x2) + (-8 * x3) = 8;
-ASSERT (24 * x0) + (-2 * x1) + (2 * x2) + (-2 * x3) >= -17 ;
-ASSERT (-6 * x0) + (17 * x1) + (27 * x2) + (26 * x3) >= -30 ;
-ASSERT (-19 * x0) + (-15 * x1) + (5 * x2) + (-27 * x3) < -3 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-29 * x0) + (-3 * x1) + (27 * x2) + (13 * x3) = -10 ;
-ASSERT (7 * x0) + (-17 * x1) + (11 * x2) + (-30 * x3) <= 6 ;
-ASSERT (30 * x0) + (17 * x1) + (-3 * x2) + (-31 * x3) > 10 ;
-ASSERT (2 * x0) + (9 * x1) + (9 * x2) + (-16 * x3) <= 11;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (19 * x0) + (-31 * x1) + (31 * x2) + (28 * x3) = -13 ;
-ASSERT (1 * x0) + (13 * x1) + (12 * x2) + (-15 * x3) > -8 ;
-ASSERT (7 * x0) + (17 * x1) + (-20 * x2) + (13 * x3) > -26 ;
-ASSERT (-17 * x0) + (14 * x1) + (-23 * x2) + (17 * x3) <= -27;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-16 * x0) + (28 * x1) + (2 * x2) + (7 * x3) = -25 ;
-ASSERT (-20 * x0) + (-24 * x1) + (4 * x2) + (32 * x3) = -22 ;
-ASSERT (19 * x0) + (28 * x1) + (-15 * x2) + (18 * x3) < -9 ;
-ASSERT (-10 * x0) + (1 * x1) + (-3 * x2) + (6 * x3) <= 1 ;
-ASSERT (-15 * x0) + (-32 * x1) + (28 * x2) + (6 * x3) >= -8 ;
-ASSERT (-18 * x0) + (-16 * x1) + (15 * x2) + (-28 * x3) <= 1 ;
-ASSERT (-20 * x0) + (-31 * x1) + (20 * x2) + (13 * x3) >= -7 ;
-ASSERT (29 * x0) + (16 * x1) + (7 * x2) + (14 * x3) < 11 ;
-ASSERT (-10 * x0) + (22 * x1) + (25 * x2) + (24 * x3) >= 5 ;
-ASSERT (-3 * x0) + (11 * x1) + (27 * x2) + (11 * x3) <= 9;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-4 * x0) + (25 * x1) + (-2 * x2) + (-16 * x3) = 27 ;
-ASSERT (-11 * x0) + (26 * x1) + (18 * x2) + (-18 * x3) = -15 ;
-ASSERT (-19 * x0) + (-27 * x1) + (-31 * x2) + (15 * x3) = 12;
-ASSERT (10 * x0) + (-10 * x1) + (25 * x2) + (-3 * x3) < -30 ;
-ASSERT (5 * x0) + (-18 * x1) + (21 * x2) + (-28 * x3) <= -4 ;
-ASSERT (-6 * x0) + (15 * x1) + (-10 * x2) + (0 * x3) < -20 ;
-ASSERT (10 * x0) + (23 * x1) + (-20 * x2) + (12 * x3) >= -15 ;
-ASSERT (-31 * x0) + (-30 * x1) + (12 * x2) + (11 * x3) > 29 ;
-ASSERT (26 * x0) + (23 * x1) + (28 * x2) + (-5 * x3) > 8 ;
-ASSERT (6 * x0) + (-29 * x1) + (12 * x2) + (16 * x3) < 27 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-19 * x0) + (-9 * x1) + (-27 * x2) + (9 * x3) = -1 ;
-ASSERT (-26 * x0) + (11 * x1) + (23 * x2) + (-5 * x3) >= 20 ;
-ASSERT (7 * x0) + (28 * x1) + (6 * x2) + (-20 * x3) <= -16 ;
-ASSERT (-15 * x0) + (21 * x1) + (5 * x2) + (-2 * x3) <= 11 ;
-ASSERT (-5 * x0) + (-16 * x1) + (-16 * x2) + (14 * x3) <= 12 ;
-ASSERT (3 * x0) + (28 * x1) + (22 * x2) + (-6 * x3) >= -31 ;
-ASSERT (15 * x0) + (-13 * x1) + (10 * x2) + (21 * x3) <= -25 ;
-ASSERT (1 * x0) + (-24 * x1) + (-30 * x2) + (25 * x3) > 17 ;
-ASSERT (12 * x0) + (-3 * x1) + (0 * x2) + (23 * x3) < -12 ;
-ASSERT (16 * x0) + (-9 * x1) + (1 * x2) + (-15 * x3) < -6;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (14 * x0) + (-14 * x1) + (-29 * x2) + (31 * x3) = -15 ;
-ASSERT (-14 * x0) + (2 * x1) + (26 * x2) + (29 * x3) = 25 ;
-ASSERT (19 * x0) + (-7 * x1) + (-15 * x2) + (12 * x3) = 32 ;
-ASSERT (5 * x0) + (32 * x1) + (22 * x2) + (1 * x3) = -13 ;
-ASSERT (-12 * x0) + (-9 * x1) + (-30 * x2) + (-13 * x3) >= 0 ;
-ASSERT (-9 * x0) + (7 * x1) + (-24 * x2) + (22 * x3) >= 11 ;
-ASSERT (28 * x0) + (-5 * x1) + (12 * x2) + (15 * x3) >= 31 ;
-ASSERT (5 * x0) + (-6 * x1) + (5 * x2) + (-2 * x3) >= -5 ;
-ASSERT (-14 * x0) + (-17 * x1) + (-29 * x2) + (-8 * x3) < -32 ;
-ASSERT (20 * x0) + (-19 * x1) + (-27 * x2) + (-20 * x3) >= -2;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-13 * x0) + (-14 * x1) + (-10 * x2) + (32 * x3) = 11 ;
-ASSERT (28 * x0) + (21 * x1) + (-20 * x2) + (-32 * x3) > -31 ;
-ASSERT (10 * x0) + (19 * x1) + (-10 * x2) + (-2 * x3) > -31 ;
-ASSERT (-31 * x0) + (17 * x1) + (15 * x2) + (31 * x3) > -12 ;
-ASSERT (-17 * x0) + (16 * x1) + (17 * x2) + (-11 * x3) >= 17 ;
-ASSERT (19 * x0) + (-31 * x1) + (-16 * x2) + (-29 * x3) >= 15 ;
-ASSERT (24 * x0) + (-32 * x1) + (27 * x2) + (11 * x3) < 26 ;
-ASSERT (-2 * x0) + (5 * x1) + (-21 * x2) + (24 * x3) >= -17 ;
-ASSERT (13 * x0) + (11 * x1) + (-28 * x2) + (-5 * x3) > 16 ;
-ASSERT (-16 * x0) + (17 * x1) + (22 * x2) + (6 * x3) > 21;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (26 * x0) + (32 * x1) + (-26 * x2) + (-26 * x3) = -26 ;
-ASSERT (30 * x0) + (17 * x1) + (28 * x2) + (-9 * x3) = -21 ;
-ASSERT (15 * x0) + (9 * x1) + (-13 * x2) + (-21 * x3) = -13 ;
-ASSERT (-4 * x0) + (16 * x1) + (-5 * x2) + (8 * x3) = -25 ;
-ASSERT (-11 * x0) + (26 * x1) + (1 * x2) + (23 * x3) < 6 ;
-ASSERT (-31 * x0) + (-25 * x1) + (1 * x2) + (16 * x3) > -8 ;
-ASSERT (9 * x0) + (-19 * x1) + (28 * x2) + (15 * x3) < -30 ;
-ASSERT (32 * x0) + (18 * x1) + (2 * x2) + (31 * x3) > -7 ;
-ASSERT (24 * x0) + (29 * x1) + (20 * x2) + (-16 * x3) >= 3 ;
-ASSERT (-1 * x0) + (17 * x1) + (-27 * x2) + (-32 * x3) >= 20 ;
-ASSERT (26 * x0) + (-23 * x1) + (6 * x2) + (30 * x3) <= 5 ;
-ASSERT (13 * x0) + (6 * x1) + (-26 * x2) + (1 * x3) > -29 ;
-ASSERT (26 * x0) + (2 * x1) + (8 * x2) + (-18 * x3) <= 32 ;
-ASSERT (-21 * x0) + (28 * x1) + (23 * x2) + (4 * x3) <= -31 ;
-ASSERT (26 * x0) + (2 * x1) + (-28 * x2) + (12 * x3) > 6 ;
-ASSERT (-20 * x0) + (-22 * x1) + (-16 * x2) + (-21 * x3) <= -1 ;
-ASSERT (21 * x0) + (-22 * x1) + (19 * x2) + (32 * x3) <= -10 ;
-ASSERT (3 * x0) + (28 * x1) + (-11 * x2) + (0 * x3) > 0 ;
-ASSERT (-13 * x0) + (-16 * x1) + (-17 * x2) + (-2 * x3) <= -17;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-20 * x0) + (19 * x1) + (16 * x2) + (-27 * x3) = -22 ;
-ASSERT (12 * x0) + (-18 * x1) + (-25 * x2) + (-1 * x3) = -22 ;
-ASSERT (17 * x0) + (11 * x1) + (24 * x2) + (16 * x3) = -3 ;
-ASSERT (15 * x0) + (-10 * x1) + (-15 * x2) + (25 * x3) = -30 ;
-ASSERT (7 * x0) + (26 * x1) + (-8 * x2) + (-29 * x3) >= -32 ;
-ASSERT (20 * x0) + (25 * x1) + (-23 * x2) + (13 * x3) >= -30 ;
-ASSERT (27 * x0) + (-32 * x1) + (-27 * x2) + (13 * x3) >= -12 ;
-ASSERT (25 * x0) + (-16 * x1) + (32 * x2) + (-6 * x3) >= -30 ;
-ASSERT (32 * x0) + (-18 * x1) + (-6 * x2) + (-32 * x3) <= -26 ;
-ASSERT (25 * x0) + (12 * x1) + (25 * x2) + (-14 * x3) > 5 ;
-ASSERT (-4 * x0) + (-20 * x1) + (12 * x2) + (-30 * x3) >= 13 ;
-ASSERT (8 * x0) + (18 * x1) + (0 * x2) + (-28 * x3) <= 18 ;
-ASSERT (-32 * x0) + (-25 * x1) + (23 * x2) + (5 * x3) < 29 ;
-ASSERT (7 * x0) + (19 * x1) + (2 * x2) + (-31 * x3) > 7 ;
-ASSERT (24 * x0) + (-17 * x1) + (-31 * x2) + (31 * x3) > 0 ;
-ASSERT (13 * x0) + (20 * x1) + (-1 * x2) + (17 * x3) > 1 ;
-ASSERT (17 * x0) + (26 * x1) + (6 * x2) + (29 * x3) >= -10 ;
-ASSERT (-25 * x0) + (4 * x1) + (-22 * x2) + (14 * x3) < -23 ;
-ASSERT (24 * x0) + (2 * x1) + (4 * x2) + (2 * x3) < 1;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (22 * x0) + (-2 * x1) + (-1 * x2) + (-24 * x3) = 8 ;
-ASSERT (-6 * x0) + (9 * x1) + (-20 * x2) + (-23 * x3) = 14 ;
-ASSERT (-11 * x0) + (4 * x1) + (24 * x2) + (-6 * x3) <= -23 ;
-ASSERT (3 * x0) + (5 * x1) + (-5 * x2) + (17 * x3) < -17 ;
-ASSERT (-10 * x0) + (-20 * x1) + (-16 * x2) + (-29 * x3) >= 6 ;
-ASSERT (-28 * x0) + (1 * x1) + (-22 * x2) + (-16 * x3) >= 4 ;
-ASSERT (19 * x0) + (8 * x1) + (-8 * x2) + (-2 * x3) > -23 ;
-ASSERT (11 * x0) + (17 * x1) + (30 * x2) + (31 * x3) < -32 ;
-ASSERT (23 * x0) + (30 * x1) + (-12 * x2) + (16 * x3) <= 4 ;
-ASSERT (-23 * x0) + (-8 * x1) + (21 * x2) + (21 * x3) <= -14 ;
-ASSERT (13 * x0) + (15 * x1) + (-6 * x2) + (-1 * x3) >= -8 ;
-ASSERT (-21 * x0) + (18 * x1) + (27 * x2) + (-16 * x3) <= 11 ;
-ASSERT (30 * x0) + (-6 * x1) + (5 * x2) + (-27 * x3) <= -7 ;
-ASSERT (0 * x0) + (3 * x1) + (13 * x2) + (28 * x3) > -21 ;
-ASSERT (-15 * x0) + (-20 * x1) + (10 * x2) + (-23 * x3) < 27 ;
-ASSERT (24 * x0) + (6 * x1) + (-29 * x2) + (1 * x3) <= -23 ;
-ASSERT (-24 * x0) + (-14 * x1) + (-15 * x2) + (8 * x3) > -19 ;
-ASSERT (17 * x0) + (15 * x1) + (8 * x2) + (-31 * x3) >= -16 ;
-ASSERT (-19 * x0) + (7 * x1) + (-28 * x2) + (20 * x3) < -19;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-7 * x0) + (-11 * x1) + (26 * x2) + (10 * x3) = 31 ;
-ASSERT (-17 * x0) + (-20 * x1) + (24 * x2) + (-9 * x3) = -32 ;
-ASSERT (5 * x0) + (14 * x1) + (7 * x2) + (-29 * x3) = 31 ;
-ASSERT (17 * x0) + (8 * x1) + (23 * x2) + (-26 * x3) <= -12 ;
-ASSERT (7 * x0) + (29 * x1) + (24 * x2) + (4 * x3) <= -21 ;
-ASSERT (-16 * x0) + (7 * x1) + (7 * x2) + (-29 * x3) < -16 ;
-ASSERT (-7 * x0) + (-11 * x1) + (-17 * x2) + (22 * x3) > -11 ;
-ASSERT (-10 * x0) + (-17 * x1) + (21 * x2) + (29 * x3) > -7 ;
-ASSERT (-28 * x0) + (-26 * x1) + (-24 * x2) + (-21 * x3) < -20 ;
-ASSERT (-32 * x0) + (26 * x1) + (-8 * x2) + (2 * x3) >= -18 ;
-ASSERT (18 * x0) + (-23 * x1) + (-26 * x2) + (-24 * x3) > -30 ;
-ASSERT (-9 * x0) + (31 * x1) + (-26 * x2) + (-22 * x3) < -15 ;
-ASSERT (27 * x0) + (-1 * x1) + (10 * x2) + (28 * x3) < -20 ;
-ASSERT (-4 * x0) + (-22 * x1) + (-24 * x2) + (2 * x3) < -13 ;
-ASSERT (-4 * x0) + (-23 * x1) + (-16 * x2) + (18 * x3) > -20 ;
-ASSERT (13 * x0) + (-30 * x1) + (-3 * x2) + (-25 * x3) <= 31 ;
-ASSERT (21 * x0) + (-28 * x1) + (22 * x2) + (19 * x3) > 7 ;
-ASSERT (-2 * x0) + (-31 * x1) + (24 * x2) + (18 * x3) > 27 ;
-ASSERT (-14 * x0) + (-5 * x1) + (-22 * x2) + (1 * x3) <= -15;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT (2 * x0) + (28 * x1) + (3 * x2) + (8 * x3) > -32 ;
-ASSERT (-15 * x0) + (21 * x1) + (-11 * x2) + (28 * x3) <= -19 ;
-ASSERT (32 * x0) + (29 * x1) + (-1 * x2) + (-10 * x3) < -23 ;
-ASSERT (6 * x0) + (-27 * x1) + (29 * x2) + (28 * x3) < 5 ;
-ASSERT (-7 * x0) + (-7 * x1) + (-28 * x2) + (32 * x3) <= -32 ;
-ASSERT (-10 * x0) + (20 * x1) + (-28 * x2) + (-28 * x3) >= -6 ;
-ASSERT (-13 * x0) + (-9 * x1) + (4 * x2) + (-32 * x3) > -1 ;
-ASSERT (-21 * x0) + (4 * x1) + (0 * x2) + (-13 * x3) >= -1 ;
-ASSERT (18 * x0) + (-21 * x1) + (-16 * x2) + (24 * x3) <= -12 ;
-ASSERT (18 * x0) + (-10 * x1) + (-10 * x2) + (-3 * x3) <= -10 ;
-ASSERT (-32 * x0) + (9 * x1) + (-24 * x2) + (-19 * x3) < -4 ;
-ASSERT (12 * x0) + (20 * x1) + (31 * x2) + (-25 * x3) <= 23 ;
-ASSERT (-22 * x0) + (15 * x1) + (-12 * x2) + (-6 * x3) < 18 ;
-ASSERT (-25 * x0) + (-8 * x1) + (32 * x2) + (26 * x3) > -20 ;
-ASSERT (-30 * x0) + (27 * x1) + (0 * x2) + (27 * x3) >= 7 ;
-ASSERT (-8 * x0) + (-2 * x1) + (-6 * x2) + (-21 * x3) <= 21 ;
-ASSERT (8 * x0) + (-31 * x1) + (-4 * x2) + (1 * x3) > -11 ;
-ASSERT (22 * x0) + (-25 * x1) + (-26 * x2) + (10 * x3) < -32 ;
-ASSERT (-12 * x0) + (-13 * x1) + (15 * x2) + (4 * x3) < 26;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (23 * x0) + (24 * x1) + (19 * x2) + (-3 * x3) = -16 ;
-ASSERT (2 * x0) + (-13 * x1) + (5 * x2) + (-1 * x3) = 28;
-ASSERT (-6 * x0) + (-5 * x1) + (-2 * x2) + (-9 * x3) > -3 ;
-ASSERT (30 * x0) + (22 * x1) + (-20 * x2) + (1 * x3) > -12 ;
-ASSERT (-8 * x0) + (-25 * x1) + (28 * x2) + (-25 * x3) <= -8 ;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-31 * x0) + (-20 * x1) + (-30 * x2) + (-28 * x3) = -24 ;
-ASSERT (11 * x0) + (-32 * x1) + (-2 * x2) + (8 * x3) <= 16 ;
-ASSERT (-10 * x0) + (16 * x1) + (31 * x2) + (19 * x3) >= -21 ;
-ASSERT (-15 * x0) + (18 * x1) + (-16 * x2) + (7 * x3) <= -12 ;
-ASSERT (14 * x0) + (-1 * x1) + (12 * x2) + (27 * x3) >= -12;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (27 * x0) + (-21 * x1) + (-6 * x2) + (-6 * x3) > -15 ;
-ASSERT (-5 * x0) + (-10 * x1) + (2 * x2) + (-16 * x3) <= -7 ;
-ASSERT (25 * x0) + (25 * x1) + (-15 * x2) + (-32 * x3) > -31 ;
-ASSERT (17 * x0) + (-26 * x1) + (9 * x2) + (-28 * x3) >= -29 ;
-ASSERT (-10 * x0) + (-18 * x1) + (15 * x2) + (0 * x3) <= 32;
-QUERY FALSE;
+++ /dev/null
-% EXPECT: sat
-
-Cache: TYPE = ARRAY [0..100] OF [# addr: INT, data: REAL #];
-State: TYPE = [# pc: INT, cache: Cache #];
-
-s0: State;
-s1: State = s0 WITH .cache[10].data := 2/3;
-
-CHECKSAT;
+++ /dev/null
-;; This is a nasty parsing test for define-fun-rec
-
-(set-logic UFLIRA)
-(set-info :smt-lib-version 2.5)
-(define-fun-rec (
- (f ((x Int)) Int 5) ;; ok, f : Int -> Int
- (g ((x Int)) Int (h 4)) ;; um, ok, so g : Int -> Int and h : Int -> Int?
- (h ((x Real)) Int 4) ;; oops no we were wrong, **CRASH**
-))
-
-(reset)
-
-(set-logic UFLIRA)
-(set-info :smt-lib-version 2.5)
-(define-fun-rec (
- (f ((x Int)) Int (g (h 4) 5)) ;; ok, f : Int -> Int and g : Int -> X -> Int and h : Int -> X ??! What the F?! (pun intended)
- (g ((x Int)) Int 5) ;; wait, now g has wrong arity?!! **BURN**
- (h ((x Int)) Int 2)
-))
-
-(reset)
-
-(set-logic UFLIRA)
-(set-info :smt-lib-version 2.5)
-(declare-const g Int 2)
-(define-fun-rec (
- (f () Int g) ;; wait, which g does this refer to?! **LOCUSTS**
- (g () Int 5)
-))
+++ /dev/null
-(set-logic QF_ALIRA)
-(declare-fun a () (Array Int Real))
-(declare-fun b () (Array Int Int))
-(assert (= a b))
-(assert (= (select a 0) 0.5))
-(check-sat)
+++ /dev/null
-; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
-(set-logic LIA)
-;; this is the custom enumeration datatype syntax from an early proposal of the sygus standard
-(define-sort D (Enum (a b)))
-(define-fun f ((x D)) Int (ite (= x D::a) 3 7))
-(synth-fun g () D ((Start D)) ((Start D (D::a D::b))))
-(constraint (= (f g) 7))
-(check-synth)
projects / cvc5.git / commitdiff