Remove CVC language support (#7219)

This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.

32 files changed, 176 insertions, 147 deletions

diff --git a/test/regress/regress0/arith/arith.01.cvc b/test/regress/regress0/arith/arith.01.cvc
deleted file mode 100644
index 08d591590..000000000
--- a/test/regress/regress0/arith/arith.01.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-% EXPECT: entailed
-x : REAL;
-y : REAL;
-
-QUERY (x * y ) = (y * x);
diff --git a/test/regress/regress0/arith/arith.01.cvc.smt2 b/test/regress/regress0/arith/arith.01.cvc.smt2
new file mode 100644
index 000000000..eac4fe1b8
--- /dev/null
+++ b/test/regress/regress0/arith/arith.01.cvc.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(check-sat-assuming ( (not (= (* x y) (* y x))) ))
diff --git a/test/regress/regress0/arith/arith.02.cvc b/test/regress/regress0/arith/arith.02.cvc
deleted file mode 100644
index e0a48c357..000000000
--- a/test/regress/regress0/arith/arith.02.cvc
+++ /dev/null
@@ -1,6 +0,0 @@
-% EXPECT: entailed
-x : REAL;
-y : REAL;
-z : REAL;
-
-QUERY x*(y*z) = (x*y)*z;
diff --git a/test/regress/regress0/arith/arith.02.cvc.smt2 b/test/regress/regress0/arith/arith.02.cvc.smt2
new file mode 100644
index 000000000..5c44e1bec
--- /dev/null
+++ b/test/regress/regress0/arith/arith.02.cvc.smt2
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+(check-sat-assuming ( (not (= (* x (* y z)) (* (* x y) z))) ))
diff --git a/test/regress/regress0/arith/arith.03.cvc b/test/regress/regress0/arith/arith.03.cvc
deleted file mode 100644
index ce54c8b7e..000000000
--- a/test/regress/regress0/arith/arith.03.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-% EXPECT: entailed
-x : REAL;
-y : REAL;
-
-QUERY (x + y)*(x + y) = x*x + 2*x*y + y*y;
diff --git a/test/regress/regress0/arith/arith.03.cvc.smt2 b/test/regress/regress0/arith/arith.03.cvc.smt2
new file mode 100644
index 000000000..777526117
--- /dev/null
+++ b/test/regress/regress0/arith/arith.03.cvc.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(check-sat-assuming ( (not (let ((_let_1 (+ x y))) (= (* _let_1 _let_1) (+ (+ (* x x) (* (* 2 x) y)) (* y y))))) ))
diff --git a/test/regress/regress0/arith/bug549.cvc b/test/regress/regress0/arith/bug549.cvc
deleted file mode 100644
index bfb3e75d5..000000000
--- a/test/regress/regress0/arith/bug549.cvc
+++ /dev/null
@@ -1,3 +0,0 @@
-% EXPECT: entailed
-a, b : REAL;
-QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a;
diff --git a/test/regress/regress0/arith/bug549.cvc.smt2 b/test/regress/regress0/arith/bug549.cvc.smt2
new file mode 100644
index 000000000..74bdc8878
--- /dev/null
+++ b/test/regress/regress0/arith/bug549.cvc.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(check-sat-assuming ( (not (= (^ (* a b) 5) (* (* (* (* (* (* (* (* (* b a) a) a) a) b) b) b) b) a))) ))
diff --git a/test/regress/regress0/arith/integers/arith-int-014.cvc b/test/regress/regress0/arith/integers/arith-int-014.cvc
deleted file mode 100644
index 84954a3ea..000000000
--- a/test/regress/regress0/arith/integers/arith-int-014.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (10 * x0) + (25 * x1) + (10 * x2) + (-28 * x3) <= 20 ;
-ASSERT  (24 * x0) + (-9 * x1) + (-12 * x2) + (15 * x3) <= 3;
-QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-014.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-014.cvc.smt2
new file mode 100644
index 000000000..02aa0d5b1
--- /dev/null
+++ b/test/regress/regress0/arith/integers/arith-int-014.cvc.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(assert (<= (+ (+ (+ (* 10 x0) (* 25 x1)) (* 10 x2)) (* (- 28) x3)) 20))
+(assert (<= (+ (+ (+ (* 24 x0) (* (- 9) x1)) (* (- 12) x2)) (* 15 x3)) 3))
+(check-sat)
diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc b/test/regress/regress0/arith/integers/arith-int-015.cvc
deleted file mode 100644
index 8f8b01fc9..000000000
--- a/test/regress/regress0/arith/integers/arith-int-015.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-22 * x0) + (-3 * x1) + (9 * x2) + (-13 * x3) > -31 ;
-ASSERT  (31 * x0) + (-17 * x1) + (28 * x2) + (-16 * x3) > -28;
-QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-015.cvc.smt2
new file mode 100644
index 000000000..5fecc9da0
--- /dev/null
+++ b/test/regress/regress0/arith/integers/arith-int-015.cvc.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(assert (> (+ (+ (+ (* (- 22) x0) (* (- 3) x1)) (* 9 x2)) (* (- 13) x3)) (- 31)))
+(assert (> (+ (+ (+ (* 31 x0) (* (- 17) x1)) (* 28 x2)) (* (- 16) x3)) (- 28)))
+(check-sat)
diff --git a/test/regress/regress0/arith/integers/arith-int-021.cvc b/test/regress/regress0/arith/integers/arith-int-021.cvc
deleted file mode 100644
index 66f02401b..000000000
--- a/test/regress/regress0/arith/integers/arith-int-021.cvc
+++ /dev/null
@@ -1,4 +0,0 @@
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (8 * x0) + (-27 * x1) + (29 * x2) + (-13 * x3) < 12;
-QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-021.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-021.cvc.smt2
new file mode 100644
index 000000000..c7c20c65e
--- /dev/null
+++ b/test/regress/regress0/arith/integers/arith-int-021.cvc.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(assert (< (+ (+ (+ (* 8 x0) (* (- 27) x1)) (* 29 x2)) (* (- 13) x3)) 12))
+(check-sat)
diff --git a/test/regress/regress0/arith/integers/arith-int-023.cvc b/test/regress/regress0/arith/integers/arith-int-023.cvc
deleted file mode 100644
index b3d79e8ff..000000000
--- a/test/regress/regress0/arith/integers/arith-int-023.cvc
+++ /dev/null
@@ -1,4 +0,0 @@
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (29 * x0) + (-19 * x1) + (23 * x2) + (15 * x3) <= 9;
-QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-023.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-023.cvc.smt2
new file mode 100644
index 000000000..5bf51fcc7
--- /dev/null
+++ b/test/regress/regress0/arith/integers/arith-int-023.cvc.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(assert (<= (+ (+ (+ (* 29 x0) (* (- 19) x1)) (* 23 x2)) (* 15 x3)) 9))
+(check-sat)
diff --git a/test/regress/regress0/arith/integers/arith-int-025.cvc b/test/regress/regress0/arith/integers/arith-int-025.cvc
deleted file mode 100644
index e905da9a0..000000000
--- a/test/regress/regress0/arith/integers/arith-int-025.cvc
+++ /dev/null
@@ -1,4 +0,0 @@
-% EXPECT: not_entailed
-x0, x1, x2, x3 : INT;
-ASSERT (-19 * x0) + (-29 * x1) + (2 * x2) + (26 * x3) >= 3;
-QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-025.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-025.cvc.smt2
new file mode 100644
index 000000000..625b5d82d
--- /dev/null
+++ b/test/regress/regress0/arith/integers/arith-int-025.cvc.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(assert (>= (+ (+ (+ (* (- 19) x0) (* (- 29) x1)) (* 2 x2)) (* 26 x3)) 3))
+(check-sat)
diff --git a/test/regress/regress0/arith/integers/arith-int-042.cvc b/test/regress/regress0/arith/integers/arith-int-042.cvc
deleted file mode 100644
index b6db26e86..000000000
--- a/test/regress/regress0/arith/integers/arith-int-042.cvc
+++ /dev/null
@@ -1,9 +0,0 @@
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT  (-9 * x0) + (25 * x1) + (0 * x2) + (13 * x3) = 17 ;
-ASSERT  (-6 * x0) + (32 * x1) + (2 * x2) + (-32 * x3) = -5 ;
-ASSERT (19 * x0) + (25 * x1) + (-32 * x2) + (-29 * x3) <= 14 ;
-ASSERT  (6 * x0) + (22 * x1) + (-24 * x2) + (-6 * x3) < -21 ;
-ASSERT  (-18 * x0) + (-21 * x1) + (-29 * x2) + (12 * x3) > 17 ;
-ASSERT  (-25 * x0) + (-5 * x1) + (-22 * x2) + (-7 * x3) > -21;
-QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-042.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-042.cvc.smt2
new file mode 100644
index 000000000..bbe6d209e
--- /dev/null
+++ b/test/regress/regress0/arith/integers/arith-int-042.cvc.smt2
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(assert (= (+ (+ (+ (* (- 9) x0) (* 25 x1)) (* 0 x2)) (* 13 x3)) 17))
+(assert (= (+ (+ (+ (* (- 6) x0) (* 32 x1)) (* 2 x2)) (* (- 32) x3)) (- 5)))
+(assert (<= (+ (+ (+ (* 19 x0) (* 25 x1)) (* (- 32) x2)) (* (- 29) x3)) 14))
+(assert (< (+ (+ (+ (* 6 x0) (* 22 x1)) (* (- 24) x2)) (* (- 6) x3)) (- 21)))
+(assert (> (+ (+ (+ (* (- 18) x0) (* (- 21) x1)) (* (- 29) x2)) (* 12 x3)) 17))
+(assert (> (+ (+ (+ (* (- 25) x0) (* (- 5) x1)) (* (- 22) x2)) (* (- 7) x3)) (- 21)))
+(check-sat)
diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc b/test/regress/regress0/arith/integers/arith-int-042.min.cvc
deleted file mode 100644
index 3fd20a0b6..000000000
--- a/test/regress/regress0/arith/integers/arith-int-042.min.cvc
+++ /dev/null
@@ -1,4 +0,0 @@
-% EXPECT: entailed
-x1: INT;
-x0: INT;
-QUERY NOT (((x0 * 6) + (x1 * 32)) = 1);
diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-042.min.cvc.smt2
new file mode 100644
index 000000000..62acf2e70
--- /dev/null
+++ b/test/regress/regress0/arith/integers/arith-int-042.min.cvc.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x1 () Int)
+(declare-fun x0 () Int)
+(check-sat-assuming ( (= (+ (* x0 6) (* x1 32)) 1) ))
diff --git a/test/regress/regress0/arith/integers/arith-int-079.cvc b/test/regress/regress0/arith/integers/arith-int-079.cvc
deleted file mode 100644
index 1739b3364..000000000
--- a/test/regress/regress0/arith/integers/arith-int-079.cvc
+++ /dev/null
@@ -1,11 +0,0 @@
-% EXPECT: entailed
-x0, x1, x2, x3 : INT;
-ASSERT  (6 * x0) + (2 * x1) + (22 * x2) + (-18 * x3) = -15 ;
-ASSERT (-8 * x0) + (-25 * x1) + (-25 * x2) + (7 * x3) > 10 ;
-ASSERT  (8 * x0) + (25 * x1) + (-7 * x2) + (-29 * x3) < -25 ;
-ASSERT  (27 * x0) + (17 * x1) + (-24 * x2) + (-5 * x3) <= 13 ;
-ASSERT  (5 * x0) + (-3 * x1) + (0 * x2) + (4 * x3) < -26 ;
-ASSERT  (25 * x0) + (7 * x1) + (27 * x2) + (-14 * x3) < 30 ;
-ASSERT  (-22 * x0) + (-17 * x1) + (9 * x2) + (-20 * x3) < -19 ;
-ASSERT  (31 * x0) + (-16 * x1) + (0 * x2) + (6 * x3) >= 18;
-QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-079.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-079.cvc.smt2
new file mode 100644
index 000000000..16c8c7ea4
--- /dev/null
+++ b/test/regress/regress0/arith/integers/arith-int-079.cvc.smt2
@@ -0,0 +1,16 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(assert (= (+ (+ (+ (* 6 x0) (* 2 x1)) (* 22 x2)) (* (- 18) x3)) (- 15)))
+(assert (let ((_let_1 (- 25))) (> (+ (+ (+ (* (- 8) x0) (* _let_1 x1)) (* _let_1 x2)) (* 7 x3)) 10)))
+(assert (< (+ (+ (+ (* 8 x0) (* 25 x1)) (* (- 7) x2)) (* (- 29) x3)) (- 25)))
+(assert (<= (+ (+ (+ (* 27 x0) (* 17 x1)) (* (- 24) x2)) (* (- 5) x3)) 13))
+(assert (< (+ (+ (+ (* 5 x0) (* (- 3) x1)) (* 0 x2)) (* 4 x3)) (- 26)))
+(assert (< (+ (+ (+ (* 25 x0) (* 7 x1)) (* 27 x2)) (* (- 14) x3)) 30))
+(assert (< (+ (+ (+ (* (- 22) x0) (* (- 17) x1)) (* 9 x2)) (* (- 20) x3)) (- 19)))
+(assert (>= (+ (+ (+ (* 31 x0) (* (- 16) x1)) (* 0 x2)) (* 6 x3)) 18))
+(check-sat)
diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc b/test/regress/regress0/arith/integers/arith-interval.cvc
deleted file mode 100644
index ed6cb747e..000000000
--- a/test/regress/regress0/arith/integers/arith-interval.cvc
+++ /dev/null
@@ -1,7 +0,0 @@
-% EXPECT: entailed
-x: INT;
-P: INT -> BOOLEAN;
-
-ASSERT 1 <= x AND x <= 2;
-ASSERT P(1) AND P(2);
-QUERY P(x);
diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc.smt2 b/test/regress/regress0/arith/integers/arith-interval.cvc.smt2
new file mode 100644
index 000000000..1a0fcd737
--- /dev/null
+++ b/test/regress/regress0/arith/integers/arith-interval.cvc.smt2
@@ -0,0 +1,8 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x () Int)
+(declare-fun P (Int) Bool)
+(assert (and (<= 1 x) (<= x 2)))
+(assert (and (P 1) (P 2)))
+(check-sat-assuming ( (not (P x)) ))
diff --git a/test/regress/regress0/arith/miplib.cvc b/test/regress/regress0/arith/miplib.cvc
deleted file mode 100644
index a7ae19b0a..000000000
--- a/test/regress/regress0/arith/miplib.cvc
+++ /dev/null
@@ -1,28 +0,0 @@
-% COMMAND-LINE: --miplib-trick
-% EXPECT: sat
-
-tmp1, tmp2, tmp3 : INT;
-x, y, z : BOOLEAN;
-
-% x = {0, 1}, (NOT x) = 1 - x
-% i*Nx + j*Ny + k = 0
-% i*x + j*Ny + k = 4
-% i*Nx + j*y + k = 6
-% i*x + j*y + k = 10
-
-ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0;
-ASSERT     x AND (NOT y AND TRUE) => tmp1 = 4;
-ASSERT NOT x AND (    y AND TRUE) => tmp1 = 6;
-ASSERT     x AND (    y AND TRUE) => tmp1 = 10;
-
-ASSERT NOT x AND (NOT z AND TRUE) => tmp2 = 0;
-ASSERT     x AND (NOT z AND TRUE) => tmp2 = 2;
-ASSERT NOT x AND (    z AND TRUE) => tmp2 = 9;
-ASSERT     x AND (    z AND TRUE) => tmp2 = 11;
-
-ASSERT NOT y AND (NOT z AND TRUE) => tmp3 = 0;
-ASSERT     y AND (NOT z AND TRUE) => tmp3 = 5;
-ASSERT NOT y AND (    z AND TRUE) => tmp3 = 16;
-ASSERT     y AND (    z AND TRUE) => tmp3 = 21;
-
-CHECKSAT;
diff --git a/test/regress/regress0/arith/miplib.cvc.smt2 b/test/regress/regress0/arith/miplib.cvc.smt2
new file mode 100644
index 000000000..3b31b4f1b
--- /dev/null
+++ b/test/regress/regress0/arith/miplib.cvc.smt2
@@ -0,0 +1,23 @@
+; COMMAND-LINE: --miplib-trick
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun tmp1 () Int)
+(declare-fun tmp2 () Int)
+(declare-fun tmp3 () Int)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+(assert (=> (and (not x) (and (not y) true)) (= tmp1 0)))
+(assert (=> (and x (and (not y) true)) (= tmp1 4)))
+(assert (=> (and (not x) (and y true)) (= tmp1 6)))
+(assert (=> (and x (and y true)) (= tmp1 10)))
+(assert (=> (and (not x) (and (not z) true)) (= tmp2 0)))
+(assert (=> (and x (and (not z) true)) (= tmp2 2)))
+(assert (=> (and (not x) (and z true)) (= tmp2 9)))
+(assert (=> (and x (and z true)) (= tmp2 11)))
+(assert (=> (and (not y) (and (not z) true)) (= tmp3 0)))
+(assert (=> (and y (and (not z) true)) (= tmp3 5)))
+(assert (=> (and (not y) (and z true)) (= tmp3 16)))
+(assert (=> (and y (and z true)) (= tmp3 21)))
+(check-sat)
diff --git a/test/regress/regress0/arith/miplib2.cvc b/test/regress/regress0/arith/miplib2.cvc
deleted file mode 100644
index ce2e9712e..000000000
--- a/test/regress/regress0/arith/miplib2.cvc
+++ /dev/null
@@ -1,32 +0,0 @@
-% COMMAND-LINE: --miplib-trick
-% EXPECT: sat
-
-tmp1, tmp2, tmp3 : INT;
-x, y, z : BOOLEAN;
-
-% x = {0, 1}, (NOT x) = 1 - x
-% i*Nx + j*Ny + k = 0
-% i*x + j*Ny + k = 4
-% i*Nx + j*y + k = 6
-% i*x + j*y + k = 10
-
-ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0;
-ASSERT     x AND (NOT y AND TRUE) => tmp1 = 4;
-ASSERT NOT x AND (    y AND TRUE) => tmp1 = 6;
-ASSERT     x AND (    y AND TRUE) => tmp1 = 10;
-
-ASSERT NOT x AND (NOT z AND TRUE) => tmp2 = 0;
-ASSERT     x AND (NOT z AND TRUE) => tmp2 = 2;
-ASSERT NOT x AND (    z AND TRUE) => tmp2 = 9;
-ASSERT     x AND (    z AND TRUE) => tmp2 = 11;
-
-ASSERT NOT y AND (NOT z AND TRUE) => tmp3 = 0;
-ASSERT     y AND (NOT z AND TRUE) => tmp3 = 5;
-ASSERT NOT y AND (    z AND TRUE) => tmp3 = 16;
-ASSERT     y AND (    z AND TRUE) => tmp3 = 21;
-
-% miplib trick does not apply to blocks 1 and 2, x occurs outside
-% of the tmp definitions
-ASSERT x;
-
-CHECKSAT;
diff --git a/test/regress/regress0/arith/miplib2.cvc.smt2 b/test/regress/regress0/arith/miplib2.cvc.smt2
new file mode 100644
index 000000000..e95385bb1
--- /dev/null
+++ b/test/regress/regress0/arith/miplib2.cvc.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --miplib-trick
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun tmp1 () Int)
+(declare-fun tmp2 () Int)
+(declare-fun tmp3 () Int)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+(assert (=> (and (not x) (and (not y) true)) (= tmp1 0)))
+(assert (=> (and x (and (not y) true)) (= tmp1 4)))
+(assert (=> (and (not x) (and y true)) (= tmp1 6)))
+(assert (=> (and x (and y true)) (= tmp1 10)))
+(assert (=> (and (not x) (and (not z) true)) (= tmp2 0)))
+(assert (=> (and x (and (not z) true)) (= tmp2 2)))
+(assert (=> (and (not x) (and z true)) (= tmp2 9)))
+(assert (=> (and x (and z true)) (= tmp2 11)))
+(assert (=> (and (not y) (and (not z) true)) (= tmp3 0)))
+(assert (=> (and y (and (not z) true)) (= tmp3 5)))
+(assert (=> (and (not y) (and z true)) (= tmp3 16)))
+(assert (=> (and y (and z true)) (= tmp3 21)))
+(assert x)
+(check-sat)
diff --git a/test/regress/regress0/arith/miplib4.cvc b/test/regress/regress0/arith/miplib4.cvc
deleted file mode 100644
index 722122b38..000000000
--- a/test/regress/regress0/arith/miplib4.cvc
+++ /dev/null
@@ -1,15 +0,0 @@
-% COMMAND-LINE: --miplib-trick
-% EXPECT: sat
-
-tmp1 : INT;
-x, y : BOOLEAN;
-
-% nonlinear combination, not eligible for miplib trick replacement
-ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0;
-ASSERT     x AND (NOT y AND TRUE) => tmp1 = 4;
-ASSERT NOT x AND (    y AND TRUE) => tmp1 = 6;
-ASSERT     x AND (    y AND TRUE) => tmp1 = 12;
-
-ASSERT tmp1 > 10;
-
-CHECKSAT;
diff --git a/test/regress/regress0/arith/miplib4.cvc.smt2 b/test/regress/regress0/arith/miplib4.cvc.smt2
new file mode 100644
index 000000000..d669133d1
--- /dev/null
+++ b/test/regress/regress0/arith/miplib4.cvc.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --miplib-trick
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun tmp1 () Int)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(assert (=> (and (not x) (and (not y) true)) (= tmp1 0)))
+(assert (=> (and x (and (not y) true)) (= tmp1 4)))
+(assert (=> (and (not x) (and y true)) (= tmp1 6)))
+(assert (=> (and x (and y true)) (= tmp1 12)))
+(assert (> tmp1 10))
+(check-sat)