diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-09 03:57:13 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-09 10:57:13 +0100 |
| commit | 59cd96a33b8f32405be2a20fc8230efc33b8dcdc (patch) | |
| tree | ad6d9b97c1a1da7026e84500f0b2ffe6081a17de | |
| parent | adc9bb5dff0c3d705b91d862d61a0c3057350688 (diff) | |
Remove obsolete regressions (#5633)
This removes benchmarks for the following reasons:
- regress1/arith/arith-int are removed since there are many similar regressions (10 from this set are already enabled)
- bitvector cvc benchmarks are removed since their *.smt2 benchmarks are enabled
- other benchmarks are removed due to features we do not plan to support
- one placeholder benchmark is removed
145 files changed, 1 insertions, 1705 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0bb5c9ef7..efe7dee36 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2352,70 +2352,11 @@ set(regression_disabled_tests 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 @@ -2452,7 +2393,6 @@ set(regression_disabled_tests 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 @@ -2483,100 +2423,14 @@ set(regression_disabled_tests # 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 @@ -2613,7 +2467,6 @@ set(regression_disabled_tests # 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 diff --git a/test/regress/regress0/bv/core/concat-merge-0.cvc b/test/regress/regress0/bv/core/concat-merge-0.cvc deleted file mode 100644 index 60341c03b..000000000 --- a/test/regress/regress0/bv/core/concat-merge-0.cvc +++ /dev/null @@ -1,3 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[2:1] @ x[0:0] = x[2:0] ); - diff --git a/test/regress/regress0/bv/core/concat-merge-1.cvc b/test/regress/regress0/bv/core/concat-merge-1.cvc deleted file mode 100644 index af0e8387b..000000000 --- a/test/regress/regress0/bv/core/concat-merge-1.cvc +++ /dev/null @@ -1,3 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[4:2] @ x[1:0] = x[4:0] ); - diff --git a/test/regress/regress0/bv/core/concat-merge-2.cvc b/test/regress/regress0/bv/core/concat-merge-2.cvc deleted file mode 100644 index 8ad7f2aa3..000000000 --- a/test/regress/regress0/bv/core/concat-merge-2.cvc +++ /dev/null @@ -1,3 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[8:4] @ x[3:0] = x[8:0] ); - diff --git a/test/regress/regress0/bv/core/concat-merge-3.cvc b/test/regress/regress0/bv/core/concat-merge-3.cvc deleted file mode 100644 index d46da1a55..000000000 --- a/test/regress/regress0/bv/core/concat-merge-3.cvc +++ /dev/null @@ -1,3 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[16:8] @ x[7:0] = x[16:0]); - diff --git a/test/regress/regress0/bv/core/equality-00.cvc b/test/regress/regress0/bv/core/equality-00.cvc deleted file mode 100644 index e02c616ad..000000000 --- a/test/regress/regress0/bv/core/equality-00.cvc +++ /dev/null @@ -1,4 +0,0 @@ -x, y, z : BITVECTOR(32); -ASSERT(x = y); -ASSERT(y = z); -QUERY(x = z);
\ No newline at end of file diff --git a/test/regress/regress0/bv/core/equality-01.cvc b/test/regress/regress0/bv/core/equality-01.cvc deleted file mode 100644 index e56af23dd..000000000 --- a/test/regress/regress0/bv/core/equality-01.cvc +++ /dev/null @@ -1,5 +0,0 @@ -x, y, z, w: BITVECTOR(32); -ASSERT(x = y); -ASSERT(y = z); -ASSERT(z = w); -QUERY(x = w);
\ No newline at end of file diff --git a/test/regress/regress0/bv/core/equality-02.cvc b/test/regress/regress0/bv/core/equality-02.cvc deleted file mode 100644 index e8f51d61a..000000000 --- a/test/regress/regress0/bv/core/equality-02.cvc +++ /dev/null @@ -1,15 +0,0 @@ -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); - diff --git a/test/regress/regress0/bv/core/equality-03.cvc b/test/regress/regress0/bv/core/equality-03.cvc deleted file mode 100644 index d2f18682c..000000000 --- a/test/regress/regress0/bv/core/equality-03.cvc +++ /dev/null @@ -1,10 +0,0 @@ -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); - diff --git a/test/regress/regress0/bv/core/equality-03.smtv1.smt2 b/test/regress/regress0/bv/core/equality-03.smtv1.smt2 deleted file mode 100644 index e31d17a83..000000000 --- a/test/regress/regress0/bv/core/equality-03.smtv1.smt2 +++ /dev/null @@ -1,20 +0,0 @@ -(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)) )) diff --git a/test/regress/regress0/bv/core/extract-concat-0.cvc b/test/regress/regress0/bv/core/extract-concat-0.cvc deleted file mode 100644 index 9aa608265..000000000 --- a/test/regress/regress0/bv/core/extract-concat-0.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[63:32] = x[31:0]); diff --git a/test/regress/regress0/bv/core/extract-concat-1.cvc b/test/regress/regress0/bv/core/extract-concat-1.cvc deleted file mode 100644 index e192f159c..000000000 --- a/test/regress/regress0/bv/core/extract-concat-1.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[62:33] = x[30:1]); diff --git a/test/regress/regress0/bv/core/extract-concat-10.cvc b/test/regress/regress0/bv/core/extract-concat-10.cvc deleted file mode 100644 index 8d3b88fba..000000000 --- a/test/regress/regress0/bv/core/extract-concat-10.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[60:3] = x[28:0] @ y[31:3]); diff --git a/test/regress/regress0/bv/core/extract-concat-11.cvc b/test/regress/regress0/bv/core/extract-concat-11.cvc deleted file mode 100644 index 2290eef04..000000000 --- a/test/regress/regress0/bv/core/extract-concat-11.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[59:4] = x[27:0] @ y[31:4]); diff --git a/test/regress/regress0/bv/core/extract-concat-2.cvc b/test/regress/regress0/bv/core/extract-concat-2.cvc deleted file mode 100644 index bd1e3ff30..000000000 --- a/test/regress/regress0/bv/core/extract-concat-2.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[61:34] = x[29:2]); diff --git a/test/regress/regress0/bv/core/extract-concat-3.cvc b/test/regress/regress0/bv/core/extract-concat-3.cvc deleted file mode 100644 index 4e225be42..000000000 --- a/test/regress/regress0/bv/core/extract-concat-3.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[60:35] = x[28:3]); diff --git a/test/regress/regress0/bv/core/extract-concat-4.cvc b/test/regress/regress0/bv/core/extract-concat-4.cvc deleted file mode 100644 index 8ecf96e6f..000000000 --- a/test/regress/regress0/bv/core/extract-concat-4.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[31:0] = y[31:0]); diff --git a/test/regress/regress0/bv/core/extract-concat-5.cvc b/test/regress/regress0/bv/core/extract-concat-5.cvc deleted file mode 100644 index 378ca5d2a..000000000 --- a/test/regress/regress0/bv/core/extract-concat-5.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[30:1] = y[30:1]); diff --git a/test/regress/regress0/bv/core/extract-concat-6.cvc b/test/regress/regress0/bv/core/extract-concat-6.cvc deleted file mode 100644 index 41499b55b..000000000 --- a/test/regress/regress0/bv/core/extract-concat-6.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[29:2] = y[29:2]); diff --git a/test/regress/regress0/bv/core/extract-concat-7.cvc b/test/regress/regress0/bv/core/extract-concat-7.cvc deleted file mode 100644 index 838017f55..000000000 --- a/test/regress/regress0/bv/core/extract-concat-7.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[28:3] = y[28:3]); diff --git a/test/regress/regress0/bv/core/extract-concat-8.cvc b/test/regress/regress0/bv/core/extract-concat-8.cvc deleted file mode 100644 index 68982b0a6..000000000 --- a/test/regress/regress0/bv/core/extract-concat-8.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[62:1] = x[30:0] @ y[31:1]); diff --git a/test/regress/regress0/bv/core/extract-concat-9.cvc b/test/regress/regress0/bv/core/extract-concat-9.cvc deleted file mode 100644 index 5f0e690cb..000000000 --- a/test/regress/regress0/bv/core/extract-concat-9.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x, y : BITVECTOR(32); -QUERY ((x @ y)[61:2] = x[29:0] @ y[31:2]); diff --git a/test/regress/regress0/bv/core/extract-constant.cvc b/test/regress/regress0/bv/core/extract-constant.cvc deleted file mode 100644 index e70ccbf5e..000000000 --- a/test/regress/regress0/bv/core/extract-constant.cvc +++ /dev/null @@ -1,2 +0,0 @@ -QUERY (0bin000111000[6:2] = 0bin01110); - diff --git a/test/regress/regress0/bv/core/extract-extract-0.cvc b/test/regress/regress0/bv/core/extract-extract-0.cvc deleted file mode 100644 index 7d1a4542c..000000000 --- a/test/regress/regress0/bv/core/extract-extract-0.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[31:0][31:0] = x[31:0]); diff --git a/test/regress/regress0/bv/core/extract-extract-1.cvc b/test/regress/regress0/bv/core/extract-extract-1.cvc deleted file mode 100644 index 86158e1cb..000000000 --- a/test/regress/regress0/bv/core/extract-extract-1.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[31:0][15:1] = x[15:1]); diff --git a/test/regress/regress0/bv/core/extract-extract-10.cvc b/test/regress/regress0/bv/core/extract-extract-10.cvc deleted file mode 100644 index 4710aa65a..000000000 --- a/test/regress/regress0/bv/core/extract-extract-10.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[7:2][2:2] = x[4:4]); diff --git a/test/regress/regress0/bv/core/extract-extract-11.cvc b/test/regress/regress0/bv/core/extract-extract-11.cvc deleted file mode 100644 index 27c7e1baa..000000000 --- a/test/regress/regress0/bv/core/extract-extract-11.cvc +++ /dev/null @@ -1,2 +0,0 @@ -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 diff --git a/test/regress/regress0/bv/core/extract-extract-2.cvc b/test/regress/regress0/bv/core/extract-extract-2.cvc deleted file mode 100644 index fc90ab275..000000000 --- a/test/regress/regress0/bv/core/extract-extract-2.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[31:0][7:2] = x[7:2]); diff --git a/test/regress/regress0/bv/core/extract-extract-3.cvc b/test/regress/regress0/bv/core/extract-extract-3.cvc deleted file mode 100644 index 3344c0359..000000000 --- a/test/regress/regress0/bv/core/extract-extract-3.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[31:0][4:4] = x[4:4]); diff --git a/test/regress/regress0/bv/core/extract-extract-4.cvc b/test/regress/regress0/bv/core/extract-extract-4.cvc deleted file mode 100644 index 0ad43466b..000000000 --- a/test/regress/regress0/bv/core/extract-extract-4.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[15:1][14:0] = x[15:1]); diff --git a/test/regress/regress0/bv/core/extract-extract-5.cvc b/test/regress/regress0/bv/core/extract-extract-5.cvc deleted file mode 100644 index 0d6690527..000000000 --- a/test/regress/regress0/bv/core/extract-extract-5.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[15:1][7:1] = x[8:2]); diff --git a/test/regress/regress0/bv/core/extract-extract-6.cvc b/test/regress/regress0/bv/core/extract-extract-6.cvc deleted file mode 100644 index 4c344f619..000000000 --- a/test/regress/regress0/bv/core/extract-extract-6.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[15:1][3:2] = x[4:3]); diff --git a/test/regress/regress0/bv/core/extract-extract-7.cvc b/test/regress/regress0/bv/core/extract-extract-7.cvc deleted file mode 100644 index f911226bc..000000000 --- a/test/regress/regress0/bv/core/extract-extract-7.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[15:1][3:3] = x[4:4]); diff --git a/test/regress/regress0/bv/core/extract-extract-8.cvc b/test/regress/regress0/bv/core/extract-extract-8.cvc deleted file mode 100644 index 9b782a70e..000000000 --- a/test/regress/regress0/bv/core/extract-extract-8.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[7:2][5:0] = x[7:2]); diff --git a/test/regress/regress0/bv/core/extract-extract-9.cvc b/test/regress/regress0/bv/core/extract-extract-9.cvc deleted file mode 100644 index 85c0acf49..000000000 --- a/test/regress/regress0/bv/core/extract-extract-9.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[7:2][3:1] = x[5:3]); diff --git a/test/regress/regress0/bv/core/extract-whole-0.cvc b/test/regress/regress0/bv/core/extract-whole-0.cvc deleted file mode 100644 index ea7e991cd..000000000 --- a/test/regress/regress0/bv/core/extract-whole-0.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (0bin0 @ x[31:31] @ x[30:20] @ x[19:10] @ x[9:1] @ x[0:0] @ 0bin0 = 0bin0 @ x @ 0bin0); diff --git a/test/regress/regress0/bv/core/extract-whole-1.cvc b/test/regress/regress0/bv/core/extract-whole-1.cvc deleted file mode 100644 index 8115c20b4..000000000 --- a/test/regress/regress0/bv/core/extract-whole-1.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[31:31] @ x[30:20] @ x[19:10] @ x[9:1] @ x[0:0] = x); diff --git a/test/regress/regress0/bv/core/extract-whole-2.cvc b/test/regress/regress0/bv/core/extract-whole-2.cvc deleted file mode 100644 index c6eb38be1..000000000 --- a/test/regress/regress0/bv/core/extract-whole-2.cvc +++ /dev/null @@ -1,3 +0,0 @@ -x : BITVECTOR(32); -QUERY (x @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 = x @ 0bin010101); - diff --git a/test/regress/regress0/bv/core/extract-whole-3.cvc b/test/regress/regress0/bv/core/extract-whole-3.cvc deleted file mode 100644 index 689383b7a..000000000 --- a/test/regress/regress0/bv/core/extract-whole-3.cvc +++ /dev/null @@ -1,2 +0,0 @@ -x : BITVECTOR(32); -QUERY (0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ x = 0bin010101 @ x); diff --git a/test/regress/regress0/bv/core/extract-whole-4.cvc b/test/regress/regress0/bv/core/extract-whole-4.cvc deleted file mode 100644 index 1a3f367a0..000000000 --- a/test/regress/regress0/bv/core/extract-whole-4.cvc +++ /dev/null @@ -1,3 +0,0 @@ -x : BITVECTOR(32); -QUERY (x[31:0] = x); - diff --git a/test/regress/regress0/bv/core/slice-01.cvc b/test/regress/regress0/bv/core/slice-01.cvc deleted file mode 100644 index e27f1c902..000000000 --- a/test/regress/regress0/bv/core/slice-01.cvc +++ /dev/null @@ -1,5 +0,0 @@ -x: BITVECTOR(64); -y, z : BITVECTOR(32); -ASSERT(x = y @ z); -QUERY(x[63:32] = y); - diff --git a/test/regress/regress0/bv/core/slice-02.cvc b/test/regress/regress0/bv/core/slice-02.cvc deleted file mode 100644 index 35eb43d55..000000000 --- a/test/regress/regress0/bv/core/slice-02.cvc +++ /dev/null @@ -1,5 +0,0 @@ -x: BITVECTOR(64); -y, z : BITVECTOR(32); -ASSERT(x = y @ z); -QUERY(x[31:0] = z); - diff --git a/test/regress/regress0/bv/core/slice-03.cvc b/test/regress/regress0/bv/core/slice-03.cvc deleted file mode 100644 index 51fb1983c..000000000 --- a/test/regress/regress0/bv/core/slice-03.cvc +++ /dev/null @@ -1,7 +0,0 @@ -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); - diff --git a/test/regress/regress0/bv/core/slice-04.cvc b/test/regress/regress0/bv/core/slice-04.cvc deleted file mode 100644 index 97e5b0b57..000000000 --- a/test/regress/regress0/bv/core/slice-04.cvc +++ /dev/null @@ -1,15 +0,0 @@ -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); - diff --git a/test/regress/regress0/bv/core/slice-05.cvc b/test/regress/regress0/bv/core/slice-05.cvc deleted file mode 100644 index 30fe1ed35..000000000 --- a/test/regress/regress0/bv/core/slice-05.cvc +++ /dev/null @@ -1,15 +0,0 @@ -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); - diff --git a/test/regress/regress0/bv/core/slice-06.cvc b/test/regress/regress0/bv/core/slice-06.cvc deleted file mode 100644 index 554e65567..000000000 --- a/test/regress/regress0/bv/core/slice-06.cvc +++ /dev/null @@ -1,15 +0,0 @@ -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]); - diff --git a/test/regress/regress0/bv/core/slice-07.cvc b/test/regress/regress0/bv/core/slice-07.cvc deleted file mode 100644 index 134037a40..000000000 --- a/test/regress/regress0/bv/core/slice-07.cvc +++ /dev/null @@ -1,4 +0,0 @@ -x: BITVECTOR(5); -ASSERT(x[4:1] = x[3:0]); -QUERY(x[4:4]=x[0:0]); - diff --git a/test/regress/regress0/bv/core/slice-08.cvc b/test/regress/regress0/bv/core/slice-08.cvc deleted file mode 100644 index bf5222844..000000000 --- a/test/regress/regress0/bv/core/slice-08.cvc +++ /dev/null @@ -1,4 +0,0 @@ -x: BITVECTOR(5); -ASSERT(x[4:3] = x[1:0]); -QUERY(x[4:4]=x[0:0]); - diff --git a/test/regress/regress0/bv/core/slice-09.cvc b/test/regress/regress0/bv/core/slice-09.cvc deleted file mode 100644 index 43876c923..000000000 --- a/test/regress/regress0/bv/core/slice-09.cvc +++ /dev/null @@ -1,4 +0,0 @@ -x: BITVECTOR(6); -ASSERT(x[5:2] = x[3:0]); -QUERY(x[5:4]=x[1:0]); - diff --git a/test/regress/regress0/bv/core/slice-10.cvc b/test/regress/regress0/bv/core/slice-10.cvc deleted file mode 100644 index 953d41ec2..000000000 --- a/test/regress/regress0/bv/core/slice-10.cvc +++ /dev/null @@ -1,5 +0,0 @@ -x : BITVECTOR(8); -ASSERT(x[3:0] = 0bin0000); -ASSERT(x[7:4] = 0bin1111); -QUERY(x = 0bin11110000); - diff --git a/test/regress/regress0/bv/core/slice-11.cvc b/test/regress/regress0/bv/core/slice-11.cvc deleted file mode 100644 index 0fc79c13e..000000000 --- a/test/regress/regress0/bv/core/slice-11.cvc +++ /dev/null @@ -1,4 +0,0 @@ -x : BITVECTOR(8); -ASSERT(x = 0bin01010101); -QUERY(x[0:0]@x[2:2]@x[4:4]@x[6:6] = 0bin1111); - diff --git a/test/regress/regress0/bv/core/slice-12.cvc b/test/regress/regress0/bv/core/slice-12.cvc deleted file mode 100644 index 7d0d79336..000000000 --- a/test/regress/regress0/bv/core/slice-12.cvc +++ /dev/null @@ -1,8 +0,0 @@ -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); - diff --git a/test/regress/regress0/bv/core/slice-13.cvc b/test/regress/regress0/bv/core/slice-13.cvc deleted file mode 100644 index 0c3e82f97..000000000 --- a/test/regress/regress0/bv/core/slice-13.cvc +++ /dev/null @@ -1,8 +0,0 @@ -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); - diff --git a/test/regress/regress0/bv/core/slice-14.cvc b/test/regress/regress0/bv/core/slice-14.cvc deleted file mode 100644 index 286f948de..000000000 --- a/test/regress/regress0/bv/core/slice-14.cvc +++ /dev/null @@ -1,5 +0,0 @@ -x: BITVECTOR(16); -ASSERT(x[15:1] = x[14:0]); -ASSERT(x[0:0] = 0bin0); -QUERY(x = 0bin0000000000000000); - diff --git a/test/regress/regress0/bv/core/slice-15.cvc b/test/regress/regress0/bv/core/slice-15.cvc deleted file mode 100644 index 076a54790..000000000 --- a/test/regress/regress0/bv/core/slice-15.cvc +++ /dev/null @@ -1,5 +0,0 @@ -x: BITVECTOR(16); -ASSERT(x[15:15] = 0bin1); -ASSERT(x[15:1] = x[14:0]); -QUERY(x = 0bin1111111111111111); - diff --git a/test/regress/regress0/bv/core/slice-16.cvc b/test/regress/regress0/bv/core/slice-16.cvc deleted file mode 100644 index 8a5b4bab9..000000000 --- a/test/regress/regress0/bv/core/slice-16.cvc +++ /dev/null @@ -1,5 +0,0 @@ -x: BITVECTOR(16); -ASSERT(x[15:15] = 0bin1); -ASSERT(x[15:2] = x[13:0]); -QUERY(x = 0bin1111111111111111); - diff --git a/test/regress/regress0/bv/core/slice-17.cvc b/test/regress/regress0/bv/core/slice-17.cvc deleted file mode 100644 index 1f2a44423..000000000 --- a/test/regress/regress0/bv/core/slice-17.cvc +++ /dev/null @@ -1,8 +0,0 @@ -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); - diff --git a/test/regress/regress0/bv/core/slice-18.cvc b/test/regress/regress0/bv/core/slice-18.cvc deleted file mode 100644 index 99f4707d8..000000000 --- a/test/regress/regress0/bv/core/slice-18.cvc +++ /dev/null @@ -1,8 +0,0 @@ -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); - diff --git a/test/regress/regress0/bv/core/slice-19.cvc b/test/regress/regress0/bv/core/slice-19.cvc deleted file mode 100644 index 0f76359b8..000000000 --- a/test/regress/regress0/bv/core/slice-19.cvc +++ /dev/null @@ -1,8 +0,0 @@ -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); - diff --git a/test/regress/regress0/bv/core/slice-20.cvc b/test/regress/regress0/bv/core/slice-20.cvc deleted file mode 100644 index a211b5f2e..000000000 --- a/test/regress/regress0/bv/core/slice-20.cvc +++ /dev/null @@ -1,13 +0,0 @@ -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 diff --git a/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 b/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 deleted file mode 100644 index 70c0057f9..000000000 --- a/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 +++ /dev/null @@ -1 +0,0 @@ -; PLACEHOLDER: benchmark to be added diff --git a/test/regress/regress1/arith/arith-int-001.cvc b/test/regress/regress1/arith/arith-int-001.cvc deleted file mode 100644 index 3fd528c11..000000000 --- a/test/regress/regress1/arith/arith-int-001.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-002.cvc b/test/regress/regress1/arith/arith-int-002.cvc deleted file mode 100644 index 6cc4b2c5e..000000000 --- a/test/regress/regress1/arith/arith-int-002.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-003.cvc b/test/regress/regress1/arith/arith-int-003.cvc deleted file mode 100644 index f294babe6..000000000 --- a/test/regress/regress1/arith/arith-int-003.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-005.cvc b/test/regress/regress1/arith/arith-int-005.cvc deleted file mode 100644 index 3701d60b4..000000000 --- a/test/regress/regress1/arith/arith-int-005.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-006.cvc b/test/regress/regress1/arith/arith-int-006.cvc deleted file mode 100644 index 53a80310a..000000000 --- a/test/regress/regress1/arith/arith-int-006.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-007.cvc b/test/regress/regress1/arith/arith-int-007.cvc deleted file mode 100644 index c0732e2b2..000000000 --- a/test/regress/regress1/arith/arith-int-007.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-008.cvc b/test/regress/regress1/arith/arith-int-008.cvc deleted file mode 100644 index 1810d6f28..000000000 --- a/test/regress/regress1/arith/arith-int-008.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-009.cvc b/test/regress/regress1/arith/arith-int-009.cvc deleted file mode 100644 index 14b26da6c..000000000 --- a/test/regress/regress1/arith/arith-int-009.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-010.cvc b/test/regress/regress1/arith/arith-int-010.cvc deleted file mode 100644 index aa649ba4a..000000000 --- a/test/regress/regress1/arith/arith-int-010.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-016.cvc b/test/regress/regress1/arith/arith-int-016.cvc deleted file mode 100644 index 951650461..000000000 --- a/test/regress/regress1/arith/arith-int-016.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-017.cvc b/test/regress/regress1/arith/arith-int-017.cvc deleted file mode 100644 index 48287249f..000000000 --- a/test/regress/regress1/arith/arith-int-017.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-018.cvc b/test/regress/regress1/arith/arith-int-018.cvc deleted file mode 100644 index cae6fed72..000000000 --- a/test/regress/regress1/arith/arith-int-018.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-019.cvc b/test/regress/regress1/arith/arith-int-019.cvc deleted file mode 100644 index a26bbac01..000000000 --- a/test/regress/regress1/arith/arith-int-019.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-020.cvc b/test/regress/regress1/arith/arith-int-020.cvc deleted file mode 100644 index c1416b38f..000000000 --- a/test/regress/regress1/arith/arith-int-020.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-026.cvc b/test/regress/regress1/arith/arith-int-026.cvc deleted file mode 100644 index 52f2478e0..000000000 --- a/test/regress/regress1/arith/arith-int-026.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-027.cvc b/test/regress/regress1/arith/arith-int-027.cvc deleted file mode 100644 index 6c38642d2..000000000 --- a/test/regress/regress1/arith/arith-int-027.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-028.cvc b/test/regress/regress1/arith/arith-int-028.cvc deleted file mode 100644 index 7e8b78893..000000000 --- a/test/regress/regress1/arith/arith-int-028.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-029.cvc b/test/regress/regress1/arith/arith-int-029.cvc deleted file mode 100644 index ba49219d8..000000000 --- a/test/regress/regress1/arith/arith-int-029.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-030.cvc b/test/regress/regress1/arith/arith-int-030.cvc deleted file mode 100644 index a6348b107..000000000 --- a/test/regress/regress1/arith/arith-int-030.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-031.cvc b/test/regress/regress1/arith/arith-int-031.cvc deleted file mode 100644 index 056ab622e..000000000 --- a/test/regress/regress1/arith/arith-int-031.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-032.cvc b/test/regress/regress1/arith/arith-int-032.cvc deleted file mode 100644 index 08c29108e..000000000 --- a/test/regress/regress1/arith/arith-int-032.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-033.cvc b/test/regress/regress1/arith/arith-int-033.cvc deleted file mode 100644 index 8259a7725..000000000 --- a/test/regress/regress1/arith/arith-int-033.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-034.cvc b/test/regress/regress1/arith/arith-int-034.cvc deleted file mode 100644 index 2b5ae4f4f..000000000 --- a/test/regress/regress1/arith/arith-int-034.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-035.cvc b/test/regress/regress1/arith/arith-int-035.cvc deleted file mode 100644 index 1bad259e2..000000000 --- a/test/regress/regress1/arith/arith-int-035.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-036.cvc b/test/regress/regress1/arith/arith-int-036.cvc deleted file mode 100644 index 0eb783815..000000000 --- a/test/regress/regress1/arith/arith-int-036.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-037.cvc b/test/regress/regress1/arith/arith-int-037.cvc deleted file mode 100644 index c3ed60011..000000000 --- a/test/regress/regress1/arith/arith-int-037.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-038.cvc b/test/regress/regress1/arith/arith-int-038.cvc deleted file mode 100644 index 52ac2b1e3..000000000 --- a/test/regress/regress1/arith/arith-int-038.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-039.cvc b/test/regress/regress1/arith/arith-int-039.cvc deleted file mode 100644 index cecb7f085..000000000 --- a/test/regress/regress1/arith/arith-int-039.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-040.cvc b/test/regress/regress1/arith/arith-int-040.cvc deleted file mode 100644 index f2dff7796..000000000 --- a/test/regress/regress1/arith/arith-int-040.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-041.cvc b/test/regress/regress1/arith/arith-int-041.cvc deleted file mode 100644 index 9df03a9bd..000000000 --- a/test/regress/regress1/arith/arith-int-041.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-043.cvc b/test/regress/regress1/arith/arith-int-043.cvc deleted file mode 100644 index 7a2d6d6af..000000000 --- a/test/regress/regress1/arith/arith-int-043.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-044.cvc b/test/regress/regress1/arith/arith-int-044.cvc deleted file mode 100644 index 649532a4b..000000000 --- a/test/regress/regress1/arith/arith-int-044.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-045.cvc b/test/regress/regress1/arith/arith-int-045.cvc deleted file mode 100644 index 2c552c915..000000000 --- a/test/regress/regress1/arith/arith-int-045.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-046.cvc b/test/regress/regress1/arith/arith-int-046.cvc deleted file mode 100644 index acf4dc9a9..000000000 --- a/test/regress/regress1/arith/arith-int-046.cvc +++ /dev/null @@ -1,6 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-049.cvc b/test/regress/regress1/arith/arith-int-049.cvc deleted file mode 100644 index 72e3b7f31..000000000 --- a/test/regress/regress1/arith/arith-int-049.cvc +++ /dev/null @@ -1,6 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-051.cvc b/test/regress/regress1/arith/arith-int-051.cvc deleted file mode 100644 index 68654a7df..000000000 --- a/test/regress/regress1/arith/arith-int-051.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-052.cvc b/test/regress/regress1/arith/arith-int-052.cvc deleted file mode 100644 index 9c9433ede..000000000 --- a/test/regress/regress1/arith/arith-int-052.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-053.cvc b/test/regress/regress1/arith/arith-int-053.cvc deleted file mode 100644 index 544d53fb9..000000000 --- a/test/regress/regress1/arith/arith-int-053.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-054.cvc b/test/regress/regress1/arith/arith-int-054.cvc deleted file mode 100644 index 5b4181a11..000000000 --- a/test/regress/regress1/arith/arith-int-054.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-055.cvc b/test/regress/regress1/arith/arith-int-055.cvc deleted file mode 100644 index fdfa45848..000000000 --- a/test/regress/regress1/arith/arith-int-055.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-056.cvc b/test/regress/regress1/arith/arith-int-056.cvc deleted file mode 100644 index 394b3dd4e..000000000 --- a/test/regress/regress1/arith/arith-int-056.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-057.cvc b/test/regress/regress1/arith/arith-int-057.cvc deleted file mode 100644 index 252601514..000000000 --- a/test/regress/regress1/arith/arith-int-057.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-058.cvc b/test/regress/regress1/arith/arith-int-058.cvc deleted file mode 100644 index 7e2a04d45..000000000 --- a/test/regress/regress1/arith/arith-int-058.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-059.cvc b/test/regress/regress1/arith/arith-int-059.cvc deleted file mode 100644 index 87773679e..000000000 --- a/test/regress/regress1/arith/arith-int-059.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-060.cvc b/test/regress/regress1/arith/arith-int-060.cvc deleted file mode 100644 index 74dd16dca..000000000 --- a/test/regress/regress1/arith/arith-int-060.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-061.cvc b/test/regress/regress1/arith/arith-int-061.cvc deleted file mode 100644 index b3bd247b2..000000000 --- a/test/regress/regress1/arith/arith-int-061.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-062.cvc b/test/regress/regress1/arith/arith-int-062.cvc deleted file mode 100644 index 0a185eb68..000000000 --- a/test/regress/regress1/arith/arith-int-062.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-063.cvc b/test/regress/regress1/arith/arith-int-063.cvc deleted file mode 100644 index 13c4aae2e..000000000 --- a/test/regress/regress1/arith/arith-int-063.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-064.cvc b/test/regress/regress1/arith/arith-int-064.cvc deleted file mode 100644 index f50b3cd97..000000000 --- a/test/regress/regress1/arith/arith-int-064.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-065.cvc b/test/regress/regress1/arith/arith-int-065.cvc deleted file mode 100644 index 354eb981c..000000000 --- a/test/regress/regress1/arith/arith-int-065.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-066.cvc b/test/regress/regress1/arith/arith-int-066.cvc deleted file mode 100644 index f53a254bd..000000000 --- a/test/regress/regress1/arith/arith-int-066.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-067.cvc b/test/regress/regress1/arith/arith-int-067.cvc deleted file mode 100644 index 61159e9aa..000000000 --- a/test/regress/regress1/arith/arith-int-067.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-068.cvc b/test/regress/regress1/arith/arith-int-068.cvc deleted file mode 100644 index 683d36801..000000000 --- a/test/regress/regress1/arith/arith-int-068.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-069.cvc b/test/regress/regress1/arith/arith-int-069.cvc deleted file mode 100644 index 356a28013..000000000 --- a/test/regress/regress1/arith/arith-int-069.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-070.cvc b/test/regress/regress1/arith/arith-int-070.cvc deleted file mode 100644 index 791b3b8af..000000000 --- a/test/regress/regress1/arith/arith-int-070.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-071.cvc b/test/regress/regress1/arith/arith-int-071.cvc deleted file mode 100644 index d44b18b45..000000000 --- a/test/regress/regress1/arith/arith-int-071.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-072.cvc b/test/regress/regress1/arith/arith-int-072.cvc deleted file mode 100644 index fb13a6616..000000000 --- a/test/regress/regress1/arith/arith-int-072.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-073.cvc b/test/regress/regress1/arith/arith-int-073.cvc deleted file mode 100644 index 784190cad..000000000 --- a/test/regress/regress1/arith/arith-int-073.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-074.cvc b/test/regress/regress1/arith/arith-int-074.cvc deleted file mode 100644 index 914cbe8e3..000000000 --- a/test/regress/regress1/arith/arith-int-074.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-075.cvc b/test/regress/regress1/arith/arith-int-075.cvc deleted file mode 100644 index d3851e284..000000000 --- a/test/regress/regress1/arith/arith-int-075.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-076.cvc b/test/regress/regress1/arith/arith-int-076.cvc deleted file mode 100644 index 25a3a7d35..000000000 --- a/test/regress/regress1/arith/arith-int-076.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-077.cvc b/test/regress/regress1/arith/arith-int-077.cvc deleted file mode 100644 index 7e4482093..000000000 --- a/test/regress/regress1/arith/arith-int-077.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-078.cvc b/test/regress/regress1/arith/arith-int-078.cvc deleted file mode 100644 index eacccc375..000000000 --- a/test/regress/regress1/arith/arith-int-078.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-080.cvc b/test/regress/regress1/arith/arith-int-080.cvc deleted file mode 100644 index bf6b90c67..000000000 --- a/test/regress/regress1/arith/arith-int-080.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-081.cvc b/test/regress/regress1/arith/arith-int-081.cvc deleted file mode 100644 index 47cc66ae2..000000000 --- a/test/regress/regress1/arith/arith-int-081.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-082.cvc b/test/regress/regress1/arith/arith-int-082.cvc deleted file mode 100644 index a6245f036..000000000 --- a/test/regress/regress1/arith/arith-int-082.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-083.cvc b/test/regress/regress1/arith/arith-int-083.cvc deleted file mode 100644 index 3a7c635cc..000000000 --- a/test/regress/regress1/arith/arith-int-083.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-086.cvc b/test/regress/regress1/arith/arith-int-086.cvc deleted file mode 100644 index 6ee96589b..000000000 --- a/test/regress/regress1/arith/arith-int-086.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-087.cvc b/test/regress/regress1/arith/arith-int-087.cvc deleted file mode 100644 index b969df1a3..000000000 --- a/test/regress/regress1/arith/arith-int-087.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-088.cvc b/test/regress/regress1/arith/arith-int-088.cvc deleted file mode 100644 index de0d23844..000000000 --- a/test/regress/regress1/arith/arith-int-088.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-089.cvc b/test/regress/regress1/arith/arith-int-089.cvc deleted file mode 100644 index e50daa9de..000000000 --- a/test/regress/regress1/arith/arith-int-089.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-090.cvc b/test/regress/regress1/arith/arith-int-090.cvc deleted file mode 100644 index 74d4ba4db..000000000 --- a/test/regress/regress1/arith/arith-int-090.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-091.cvc b/test/regress/regress1/arith/arith-int-091.cvc deleted file mode 100644 index c03b544a3..000000000 --- a/test/regress/regress1/arith/arith-int-091.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-092.cvc b/test/regress/regress1/arith/arith-int-092.cvc deleted file mode 100644 index d080cde0c..000000000 --- a/test/regress/regress1/arith/arith-int-092.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-093.cvc b/test/regress/regress1/arith/arith-int-093.cvc deleted file mode 100644 index e910def47..000000000 --- a/test/regress/regress1/arith/arith-int-093.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-094.cvc b/test/regress/regress1/arith/arith-int-094.cvc deleted file mode 100644 index 2204bba4e..000000000 --- a/test/regress/regress1/arith/arith-int-094.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-095.cvc b/test/regress/regress1/arith/arith-int-095.cvc deleted file mode 100644 index e803dbe9b..000000000 --- a/test/regress/regress1/arith/arith-int-095.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-096.cvc b/test/regress/regress1/arith/arith-int-096.cvc deleted file mode 100644 index 354ae180d..000000000 --- a/test/regress/regress1/arith/arith-int-096.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-099.cvc b/test/regress/regress1/arith/arith-int-099.cvc deleted file mode 100644 index 57a45de03..000000000 --- a/test/regress/regress1/arith/arith-int-099.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% 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; diff --git a/test/regress/regress1/arith/arith-int-100.cvc b/test/regress/regress1/arith/arith-int-100.cvc deleted file mode 100644 index 66be1f8f7..000000000 --- a/test/regress/regress1/arith/arith-int-100.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% 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; diff --git a/test/regress/regress1/bug585.cvc b/test/regress/regress1/bug585.cvc deleted file mode 100644 index 825cb0003..000000000 --- a/test/regress/regress1/bug585.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% 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; diff --git a/test/regress/regress1/crash_burn_locusts.smt2 b/test/regress/regress1/crash_burn_locusts.smt2 deleted file mode 100644 index 313d6f79c..000000000 --- a/test/regress/regress1/crash_burn_locusts.smt2 +++ /dev/null @@ -1,29 +0,0 @@ -;; 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) -)) diff --git a/test/regress/regress1/issue1048-arrays-int-real.smt2 b/test/regress/regress1/issue1048-arrays-int-real.smt2 deleted file mode 100644 index 6bbfe4cb7..000000000 --- a/test/regress/regress1/issue1048-arrays-int-real.smt2 +++ /dev/null @@ -1,6 +0,0 @@ -(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) diff --git a/test/regress/regress1/sygus/enum-test.sy b/test/regress/regress1/sygus/enum-test.sy deleted file mode 100644 index b5fbe4306..000000000 --- a/test/regress/regress1/sygus/enum-test.sy +++ /dev/null @@ -1,9 +0,0 @@ -; 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) |