From 36e939d31e8ac8fe2866f996af44ea268447c295 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 11 Nov 2013 11:04:48 -0500
Subject: Change exit status to be more consistent with other command-line
 tools: 0 success, nonzero error

---
 test/regress/regress0/arith/arith.01.cvc                   | 1 -
 test/regress/regress0/arith/arith.02.cvc                   | 1 -
 test/regress/regress0/arith/arith.03.cvc                   | 1 -
 test/regress/regress0/arith/div.02.smt2                    | 1 -
 test/regress/regress0/arith/div.03.smt2                    | 1 -
 test/regress/regress0/arith/div.05.smt2                    | 1 -
 test/regress/regress0/arith/div.06.smt2                    | 1 -
 test/regress/regress0/arith/integers/arith-int-001.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-002.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-003.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-004.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-005.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-006.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-007.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-008.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-009.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-010.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-011.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-012.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-013.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-014.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-015.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-016.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-017.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-018.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-019.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-020.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-021.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-022.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-023.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-024.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-025.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-026.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-027.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-028.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-029.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-030.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-031.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-032.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-033.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-034.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-035.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-036.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-037.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-038.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-039.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-040.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-041.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-042.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-042.min.cvc | 1 -
 test/regress/regress0/arith/integers/arith-int-043.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-044.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-045.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-046.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-047.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-048.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-049.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-050.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-051.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-052.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-053.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-054.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-055.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-056.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-057.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-058.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-059.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-060.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-061.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-062.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-063.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-064.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-065.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-066.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-067.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-068.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-069.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-070.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-071.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-072.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-073.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-074.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-075.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-076.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-077.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-078.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-079.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-080.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-081.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-082.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-083.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-084.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-085.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-086.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-087.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-088.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-089.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-090.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-091.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-092.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-093.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-094.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-095.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-096.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-097.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-098.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-099.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-int-100.cvc     | 1 -
 test/regress/regress0/arith/integers/arith-interval.cvc    | 1 -
 test/regress/regress0/arith/miplib-opt1217--27.smt.expect  | 1 -
 test/regress/regress0/arith/miplib-opt1217--27.smt2        | 1 -
 test/regress/regress0/arith/miplib-pp08a-3000.smt.expect   | 1 -
 test/regress/regress0/arith/miplib-pp08a-3000.smt2         | 1 -
 test/regress/regress0/arith/miplib.cvc                     | 1 -
 test/regress/regress0/arith/miplib2.cvc                    | 1 -
 test/regress/regress0/arith/miplib3.cvc                    | 1 -
 test/regress/regress0/arith/miplib4.cvc                    | 1 -
 test/regress/regress0/arith/mod.01.smt2                    | 1 -
 test/regress/regress0/arith/mod.02.smt2                    | 1 -
 test/regress/regress0/arith/mod.03.smt2                    | 1 -
 test/regress/regress0/arith/mult.01.smt2                   | 1 -
 121 files changed, 121 deletions(-)

(limited to 'test/regress/regress0/arith')

diff --git a/test/regress/regress0/arith/arith.01.cvc b/test/regress/regress0/arith/arith.01.cvc
index d153464e1..1de397ab1 100644
--- a/test/regress/regress0/arith/arith.01.cvc
+++ b/test/regress/regress0/arith/arith.01.cvc
@@ -3,4 +3,3 @@ x : REAL;
 y : REAL;
 
 QUERY (x * y ) = (y * x);
-% EXIT: 20
diff --git a/test/regress/regress0/arith/arith.02.cvc b/test/regress/regress0/arith/arith.02.cvc
index 76a7a4338..d7b0291f7 100644
--- a/test/regress/regress0/arith/arith.02.cvc
+++ b/test/regress/regress0/arith/arith.02.cvc
@@ -4,4 +4,3 @@ y : REAL;
 z : REAL;
 
 QUERY x*(y*z) = (x*y)*z;
-% EXIT: 20
diff --git a/test/regress/regress0/arith/arith.03.cvc b/test/regress/regress0/arith/arith.03.cvc
index 007adf1d6..288c341ef 100644
--- a/test/regress/regress0/arith/arith.03.cvc
+++ b/test/regress/regress0/arith/arith.03.cvc
@@ -3,4 +3,3 @@ x : REAL;
 y : REAL;
 
 QUERY (x + y)*(x + y) = x*x + 2*x*y + y*y;
-% EXIT: 20
diff --git a/test/regress/regress0/arith/div.02.smt2 b/test/regress/regress0/arith/div.02.smt2
index 65dc21549..4ed27f8ae 100644
--- a/test/regress/regress0/arith/div.02.smt2
+++ b/test/regress/regress0/arith/div.02.smt2
@@ -1,5 +1,4 @@
 ; EXPECT: unknown
-; EXIT: 0
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.0)
 (set-info :status unknown)
diff --git a/test/regress/regress0/arith/div.03.smt2 b/test/regress/regress0/arith/div.03.smt2
index 17de612bb..0f67a3df1 100644
--- a/test/regress/regress0/arith/div.03.smt2
+++ b/test/regress/regress0/arith/div.03.smt2
@@ -1,5 +1,4 @@
 ; EXPECT: unknown
-; EXIT: 0
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.0)
 (set-info :status unknown)
diff --git a/test/regress/regress0/arith/div.05.smt2 b/test/regress/regress0/arith/div.05.smt2
index fcc50ec98..9e4972e38 100644
--- a/test/regress/regress0/arith/div.05.smt2
+++ b/test/regress/regress0/arith/div.05.smt2
@@ -1,5 +1,4 @@
 ; EXPECT: unknown
-; EXIT: 0
 (set-logic QF_NRA)
 (set-info :smt-lib-version 2.0)
 (set-info :status unknown)
diff --git a/test/regress/regress0/arith/div.06.smt2 b/test/regress/regress0/arith/div.06.smt2
index b33749cc6..3fb4b124f 100644
--- a/test/regress/regress0/arith/div.06.smt2
+++ b/test/regress/regress0/arith/div.06.smt2
@@ -1,5 +1,4 @@
 ; EXPECT: unknown
-; EXIT: 0
 (set-logic QF_NRA)
 (set-info :smt-lib-version 2.0)
 (set-info :status unknown)
diff --git a/test/regress/regress0/arith/integers/arith-int-001.cvc b/test/regress/regress0/arith/integers/arith-int-001.cvc
index 8b559dc7f..03ed1a6ae 100644
--- a/test/regress/regress0/arith/integers/arith-int-001.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-001.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-002.cvc b/test/regress/regress0/arith/integers/arith-int-002.cvc
index 41113ea2f..849daba79 100644
--- a/test/regress/regress0/arith/integers/arith-int-002.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-002.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-003.cvc b/test/regress/regress0/arith/integers/arith-int-003.cvc
index a76f82c56..9c060c469 100644
--- a/test/regress/regress0/arith/integers/arith-int-003.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-003.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-004.cvc b/test/regress/regress0/arith/integers/arith-int-004.cvc
index 78d10d4b2..314b76d18 100644
--- a/test/regress/regress0/arith/integers/arith-int-004.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-004.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 
 x0, x1, x2, x3 : INT;
 ASSERT (12 * x0) + (-25 * x1) + (21 * x2) + (7 * x3) < 27 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-005.cvc b/test/regress/regress0/arith/integers/arith-int-005.cvc
index b2b1f9bf9..9b9776ad3 100644
--- a/test/regress/regress0/arith/integers/arith-int-005.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-005.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-006.cvc b/test/regress/regress0/arith/integers/arith-int-006.cvc
index cba51db21..999b4a5b4 100644
--- a/test/regress/regress0/arith/integers/arith-int-006.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-006.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-007.cvc b/test/regress/regress0/arith/integers/arith-int-007.cvc
index bc49f9688..4cb4d88ef 100644
--- a/test/regress/regress0/arith/integers/arith-int-007.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-007.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-008.cvc b/test/regress/regress0/arith/integers/arith-int-008.cvc
index a524b86b0..1ae22c993 100644
--- a/test/regress/regress0/arith/integers/arith-int-008.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-008.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-009.cvc b/test/regress/regress0/arith/integers/arith-int-009.cvc
index ccb522d37..9bd7a2ce4 100644
--- a/test/regress/regress0/arith/integers/arith-int-009.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-009.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-010.cvc b/test/regress/regress0/arith/integers/arith-int-010.cvc
index 832f4e63a..4ac85a984 100644
--- a/test/regress/regress0/arith/integers/arith-int-010.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-010.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-011.cvc b/test/regress/regress0/arith/integers/arith-int-011.cvc
index d0cc2e501..bd2fa2a0d 100644
--- a/test/regress/regress0/arith/integers/arith-int-011.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-011.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT (13 * x0) + (-1 * x1) + (11 * x2) + (10 * x3) = 9 ;
 ASSERT  (-7 * x0) + (3 * x1) + (-22 * x2) + (16 * x3) >= 9;
diff --git a/test/regress/regress0/arith/integers/arith-int-012.cvc b/test/regress/regress0/arith/integers/arith-int-012.cvc
index 46127d24f..11b0dab27 100644
--- a/test/regress/regress0/arith/integers/arith-int-012.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-012.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT (18 * x0) + (32 * x1) + (-11 * x2) + (18 * x3) < -25 ;
 ASSERT  (-31 * x0) + (16 * x1) + (24 * x2) + (9 * x3) >= -24;
diff --git a/test/regress/regress0/arith/integers/arith-int-013.cvc b/test/regress/regress0/arith/integers/arith-int-013.cvc
index e018d7a15..329251cae 100644
--- a/test/regress/regress0/arith/integers/arith-int-013.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-013.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT (-22 * x0) + (-14 * x1) + (4 * x2) + (-12 * x3) > 25 ;
 ASSERT  (14 * x0) + (11 * x1) + (32 * x2) + (-8 * x3) >= 2;
diff --git a/test/regress/regress0/arith/integers/arith-int-014.cvc b/test/regress/regress0/arith/integers/arith-int-014.cvc
index 75991b051..265d18a84 100644
--- a/test/regress/regress0/arith/integers/arith-int-014.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-014.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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;
diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc b/test/regress/regress0/arith/integers/arith-int-015.cvc
index 00ecbcde2..d2e2639ab 100644
--- a/test/regress/regress0/arith/integers/arith-int-015.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-015.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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;
diff --git a/test/regress/regress0/arith/integers/arith-int-016.cvc b/test/regress/regress0/arith/integers/arith-int-016.cvc
index d01b6c51a..6774dd2d1 100644
--- a/test/regress/regress0/arith/integers/arith-int-016.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-016.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-017.cvc b/test/regress/regress0/arith/integers/arith-int-017.cvc
index 2fee71829..e9a06125a 100644
--- a/test/regress/regress0/arith/integers/arith-int-017.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-017.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-018.cvc b/test/regress/regress0/arith/integers/arith-int-018.cvc
index c25f8e784..4cb97b77e 100644
--- a/test/regress/regress0/arith/integers/arith-int-018.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-018.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-019.cvc b/test/regress/regress0/arith/integers/arith-int-019.cvc
index 661eb288b..cf9ae2d70 100644
--- a/test/regress/regress0/arith/integers/arith-int-019.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-019.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-020.cvc b/test/regress/regress0/arith/integers/arith-int-020.cvc
index 9c6bf3932..07a827465 100644
--- a/test/regress/regress0/arith/integers/arith-int-020.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-020.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-021.cvc b/test/regress/regress0/arith/integers/arith-int-021.cvc
index bfcf022f5..345c90899 100644
--- a/test/regress/regress0/arith/integers/arith-int-021.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-021.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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-022.cvc b/test/regress/regress0/arith/integers/arith-int-022.cvc
index 4a439cdb1..584348da4 100644
--- a/test/regress/regress0/arith/integers/arith-int-022.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-022.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT (-24 * x0) + (25 * x1) + (-28 * x2) + (31 * x3) > 18;
 QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-023.cvc b/test/regress/regress0/arith/integers/arith-int-023.cvc
index fa161b2d9..01d51a226 100644
--- a/test/regress/regress0/arith/integers/arith-int-023.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-023.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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-024.cvc b/test/regress/regress0/arith/integers/arith-int-024.cvc
index c4af43db4..f57136dd1 100644
--- a/test/regress/regress0/arith/integers/arith-int-024.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-024.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT (4 * x0) + (8 * x1) + (27 * x2) + (-12 * x3) = -5;
 QUERY FALSE;
diff --git a/test/regress/regress0/arith/integers/arith-int-025.cvc b/test/regress/regress0/arith/integers/arith-int-025.cvc
index 8d527322d..5a11212d5 100644
--- a/test/regress/regress0/arith/integers/arith-int-025.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-025.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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-026.cvc b/test/regress/regress0/arith/integers/arith-int-026.cvc
index b08a4e852..9e69aa2d1 100644
--- a/test/regress/regress0/arith/integers/arith-int-026.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-026.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-027.cvc b/test/regress/regress0/arith/integers/arith-int-027.cvc
index 811726726..b45622fea 100644
--- a/test/regress/regress0/arith/integers/arith-int-027.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-027.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-028.cvc b/test/regress/regress0/arith/integers/arith-int-028.cvc
index 49562ad73..61fee4203 100644
--- a/test/regress/regress0/arith/integers/arith-int-028.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-028.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-029.cvc b/test/regress/regress0/arith/integers/arith-int-029.cvc
index 1e8687ec3..ee49bbb68 100644
--- a/test/regress/regress0/arith/integers/arith-int-029.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-029.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-030.cvc b/test/regress/regress0/arith/integers/arith-int-030.cvc
index 1ead5e5a4..70b6a3785 100644
--- a/test/regress/regress0/arith/integers/arith-int-030.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-030.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-031.cvc b/test/regress/regress0/arith/integers/arith-int-031.cvc
index 3eac975fe..86242f7aa 100644
--- a/test/regress/regress0/arith/integers/arith-int-031.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-031.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-032.cvc b/test/regress/regress0/arith/integers/arith-int-032.cvc
index 0128c4dbd..1ee4c9844 100644
--- a/test/regress/regress0/arith/integers/arith-int-032.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-032.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-033.cvc b/test/regress/regress0/arith/integers/arith-int-033.cvc
index 9dda4dbf8..599ba4e9a 100644
--- a/test/regress/regress0/arith/integers/arith-int-033.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-033.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-034.cvc b/test/regress/regress0/arith/integers/arith-int-034.cvc
index b8f4dd5f8..ec615a785 100644
--- a/test/regress/regress0/arith/integers/arith-int-034.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-034.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-035.cvc b/test/regress/regress0/arith/integers/arith-int-035.cvc
index 6adae83fe..e7dee2484 100644
--- a/test/regress/regress0/arith/integers/arith-int-035.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-035.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-036.cvc b/test/regress/regress0/arith/integers/arith-int-036.cvc
index 94074b8e1..9594f9586 100644
--- a/test/regress/regress0/arith/integers/arith-int-036.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-036.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-037.cvc b/test/regress/regress0/arith/integers/arith-int-037.cvc
index 5ad2acd37..4d4422d3f 100644
--- a/test/regress/regress0/arith/integers/arith-int-037.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-037.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-038.cvc b/test/regress/regress0/arith/integers/arith-int-038.cvc
index 807ea029b..476133b24 100644
--- a/test/regress/regress0/arith/integers/arith-int-038.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-038.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-039.cvc b/test/regress/regress0/arith/integers/arith-int-039.cvc
index 3ee88fe80..9e9235ae8 100644
--- a/test/regress/regress0/arith/integers/arith-int-039.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-039.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-040.cvc b/test/regress/regress0/arith/integers/arith-int-040.cvc
index 5484f7dde..68502349f 100644
--- a/test/regress/regress0/arith/integers/arith-int-040.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-040.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-041.cvc b/test/regress/regress0/arith/integers/arith-int-041.cvc
index a3d8889b2..a0c2dc0f9 100644
--- a/test/regress/regress0/arith/integers/arith-int-041.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-041.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-042.cvc b/test/regress/regress0/arith/integers/arith-int-042.cvc
index df9314482..c38231695 100644
--- a/test/regress/regress0/arith/integers/arith-int-042.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-042.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc b/test/regress/regress0/arith/integers/arith-int-042.min.cvc
index e19bdda0e..77571e526 100644
--- a/test/regress/regress0/arith/integers/arith-int-042.min.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-042.min.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 x1: INT;
 x0: INT;
 QUERY NOT (((x0 * 6) + (x1 * 32)) = 1);
diff --git a/test/regress/regress0/arith/integers/arith-int-043.cvc b/test/regress/regress0/arith/integers/arith-int-043.cvc
index 53f0e9903..7efea85e5 100644
--- a/test/regress/regress0/arith/integers/arith-int-043.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-043.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-044.cvc b/test/regress/regress0/arith/integers/arith-int-044.cvc
index b42affada..f933b014b 100644
--- a/test/regress/regress0/arith/integers/arith-int-044.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-044.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 %%%% down from 24, up from 6, up from 39
 x0, x1, x2, x3 : INT;
 ASSERT  (-30 * x0) + (18 * x1) + (17 * x2) + (3 * x3) = 0;
diff --git a/test/regress/regress0/arith/integers/arith-int-045.cvc b/test/regress/regress0/arith/integers/arith-int-045.cvc
index f70eff09a..ca1a12ba6 100644
--- a/test/regress/regress0/arith/integers/arith-int-045.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-045.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-046.cvc b/test/regress/regress0/arith/integers/arith-int-046.cvc
index ec694ad2b..d4d206c6e 100644
--- a/test/regress/regress0/arith/integers/arith-int-046.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-046.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-047.cvc b/test/regress/regress0/arith/integers/arith-int-047.cvc
index b5f4cb3a8..0763e5dc3 100644
--- a/test/regress/regress0/arith/integers/arith-int-047.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-047.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT  (-14 * x0) + (27 * x1) + (10 * x2) + (1 * x3) = 10;
 ASSERT (-29 * x0) + (-26 * x1) + (-16 * x2) + (17 * x3) >= 16 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-048.cvc b/test/regress/regress0/arith/integers/arith-int-048.cvc
index 76fa395bc..e7c05332d 100644
--- a/test/regress/regress0/arith/integers/arith-int-048.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-048.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT (-13 * x0) + (-11 * x1) + (-14 * x2) + (21 * x3) = 6 ;
 ASSERT  (7 * x0) + (5 * x1) + (13 * x2) + (21 * x3) <= 27 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-049.cvc b/test/regress/regress0/arith/integers/arith-int-049.cvc
index b415776e8..8eabc78a8 100644
--- a/test/regress/regress0/arith/integers/arith-int-049.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-049.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-050.cvc b/test/regress/regress0/arith/integers/arith-int-050.cvc
index d35f445d8..f0ba939b7 100644
--- a/test/regress/regress0/arith/integers/arith-int-050.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-050.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT (-20 * x0) + (-19 * x1) + (6 * x2) + (32 * x3) > 16 ;
 ASSERT  (-1 * x0) + (-30 * x1) + (15 * x2) + (7 * x3) < -10 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-051.cvc b/test/regress/regress0/arith/integers/arith-int-051.cvc
index 8a696d2de..9a2497432 100644
--- a/test/regress/regress0/arith/integers/arith-int-051.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-051.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-052.cvc b/test/regress/regress0/arith/integers/arith-int-052.cvc
index ae7e2c15f..83fdc89c8 100644
--- a/test/regress/regress0/arith/integers/arith-int-052.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-052.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-053.cvc b/test/regress/regress0/arith/integers/arith-int-053.cvc
index 3cd2f3df6..fa38fa3da 100644
--- a/test/regress/regress0/arith/integers/arith-int-053.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-053.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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;
diff --git a/test/regress/regress0/arith/integers/arith-int-054.cvc b/test/regress/regress0/arith/integers/arith-int-054.cvc
index 95eb7a6d6..9b0066966 100644
--- a/test/regress/regress0/arith/integers/arith-int-054.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-054.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-055.cvc b/test/regress/regress0/arith/integers/arith-int-055.cvc
index 6ed1bf4cd..9729fb565 100644
--- a/test/regress/regress0/arith/integers/arith-int-055.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-055.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-056.cvc b/test/regress/regress0/arith/integers/arith-int-056.cvc
index 028c1979b..e1c3ee1da 100644
--- a/test/regress/regress0/arith/integers/arith-int-056.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-056.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-057.cvc b/test/regress/regress0/arith/integers/arith-int-057.cvc
index 1984622c3..4e7b939b4 100644
--- a/test/regress/regress0/arith/integers/arith-int-057.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-057.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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;
diff --git a/test/regress/regress0/arith/integers/arith-int-058.cvc b/test/regress/regress0/arith/integers/arith-int-058.cvc
index c6c87c64b..4d964f1c6 100644
--- a/test/regress/regress0/arith/integers/arith-int-058.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-058.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-059.cvc b/test/regress/regress0/arith/integers/arith-int-059.cvc
index 558789493..841d9c8e1 100644
--- a/test/regress/regress0/arith/integers/arith-int-059.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-059.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-060.cvc b/test/regress/regress0/arith/integers/arith-int-060.cvc
index 75968a935..227cb49b1 100644
--- a/test/regress/regress0/arith/integers/arith-int-060.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-060.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-061.cvc b/test/regress/regress0/arith/integers/arith-int-061.cvc
index 68f54742c..4a3cc28d0 100644
--- a/test/regress/regress0/arith/integers/arith-int-061.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-061.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-062.cvc b/test/regress/regress0/arith/integers/arith-int-062.cvc
index 1c1c54b07..f9a3156a2 100644
--- a/test/regress/regress0/arith/integers/arith-int-062.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-062.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-063.cvc b/test/regress/regress0/arith/integers/arith-int-063.cvc
index 77843cbc3..d88104688 100644
--- a/test/regress/regress0/arith/integers/arith-int-063.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-063.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-064.cvc b/test/regress/regress0/arith/integers/arith-int-064.cvc
index 0c6847c61..21ca822e1 100644
--- a/test/regress/regress0/arith/integers/arith-int-064.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-064.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-065.cvc b/test/regress/regress0/arith/integers/arith-int-065.cvc
index 64fe7fd49..b1b9e1b51 100644
--- a/test/regress/regress0/arith/integers/arith-int-065.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-065.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-066.cvc b/test/regress/regress0/arith/integers/arith-int-066.cvc
index 6c7035ded..9532b4198 100644
--- a/test/regress/regress0/arith/integers/arith-int-066.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-066.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-067.cvc b/test/regress/regress0/arith/integers/arith-int-067.cvc
index fc74cc94c..5d7b52e69 100644
--- a/test/regress/regress0/arith/integers/arith-int-067.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-067.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-068.cvc b/test/regress/regress0/arith/integers/arith-int-068.cvc
index d4360159f..107a21a12 100644
--- a/test/regress/regress0/arith/integers/arith-int-068.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-068.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-069.cvc b/test/regress/regress0/arith/integers/arith-int-069.cvc
index f877d3108..3fab229b0 100644
--- a/test/regress/regress0/arith/integers/arith-int-069.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-069.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-070.cvc b/test/regress/regress0/arith/integers/arith-int-070.cvc
index 65e2fd6d8..cd828da5f 100644
--- a/test/regress/regress0/arith/integers/arith-int-070.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-070.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-071.cvc b/test/regress/regress0/arith/integers/arith-int-071.cvc
index e8b7a206c..ce5336476 100644
--- a/test/regress/regress0/arith/integers/arith-int-071.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-071.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-072.cvc b/test/regress/regress0/arith/integers/arith-int-072.cvc
index 7670bb468..10222deae 100644
--- a/test/regress/regress0/arith/integers/arith-int-072.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-072.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-073.cvc b/test/regress/regress0/arith/integers/arith-int-073.cvc
index 0b0f6b76c..98e74be8f 100644
--- a/test/regress/regress0/arith/integers/arith-int-073.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-073.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-074.cvc b/test/regress/regress0/arith/integers/arith-int-074.cvc
index 1f6578d09..28cc48186 100644
--- a/test/regress/regress0/arith/integers/arith-int-074.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-074.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-075.cvc b/test/regress/regress0/arith/integers/arith-int-075.cvc
index e6f136797..3b5131e8b 100644
--- a/test/regress/regress0/arith/integers/arith-int-075.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-075.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-076.cvc b/test/regress/regress0/arith/integers/arith-int-076.cvc
index d0d2bbd59..2c8de7cdf 100644
--- a/test/regress/regress0/arith/integers/arith-int-076.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-076.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-077.cvc b/test/regress/regress0/arith/integers/arith-int-077.cvc
index 4f2985da8..d14da386e 100644
--- a/test/regress/regress0/arith/integers/arith-int-077.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-077.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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;
diff --git a/test/regress/regress0/arith/integers/arith-int-078.cvc b/test/regress/regress0/arith/integers/arith-int-078.cvc
index d65638290..3197c6524 100644
--- a/test/regress/regress0/arith/integers/arith-int-078.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-078.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-079.cvc b/test/regress/regress0/arith/integers/arith-int-079.cvc
index 83a24f245..7fa2fc937 100644
--- a/test/regress/regress0/arith/integers/arith-int-079.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-079.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-080.cvc b/test/regress/regress0/arith/integers/arith-int-080.cvc
index f29f91896..8be0f9a73 100644
--- a/test/regress/regress0/arith/integers/arith-int-080.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-080.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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;
diff --git a/test/regress/regress0/arith/integers/arith-int-081.cvc b/test/regress/regress0/arith/integers/arith-int-081.cvc
index fcf857e29..546148376 100644
--- a/test/regress/regress0/arith/integers/arith-int-081.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-081.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-082.cvc b/test/regress/regress0/arith/integers/arith-int-082.cvc
index 0fbeeb03b..62bd45de7 100644
--- a/test/regress/regress0/arith/integers/arith-int-082.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-082.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-083.cvc b/test/regress/regress0/arith/integers/arith-int-083.cvc
index 90171f772..6b1084353 100644
--- a/test/regress/regress0/arith/integers/arith-int-083.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-083.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-084.cvc b/test/regress/regress0/arith/integers/arith-int-084.cvc
index f190c5d4d..5f0e17afe 100644
--- a/test/regress/regress0/arith/integers/arith-int-084.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-084.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT (-2 * x0) + (-13 * x1) + (-14 * x2) + (-26 * x3) <= 4 ;
 ASSERT  (-17 * x0) + (-17 * x1) + (21 * x2) + (-4 * x3) < 18 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-085.cvc b/test/regress/regress0/arith/integers/arith-int-085.cvc
index 281ba0e29..74dd714e8 100644
--- a/test/regress/regress0/arith/integers/arith-int-085.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-085.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 %% down from 3
 x0, x1, x2, x3 : INT;
 ASSERT (22 * x0) + (-25 * x1) + (-20 * x2) + (8 * x3) = -6 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-086.cvc b/test/regress/regress0/arith/integers/arith-int-086.cvc
index 21c058f7c..64c212b3c 100644
--- a/test/regress/regress0/arith/integers/arith-int-086.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-086.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-087.cvc b/test/regress/regress0/arith/integers/arith-int-087.cvc
index c403fdf3e..312c08917 100644
--- a/test/regress/regress0/arith/integers/arith-int-087.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-087.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-088.cvc b/test/regress/regress0/arith/integers/arith-int-088.cvc
index 04361f9b1..5212640be 100644
--- a/test/regress/regress0/arith/integers/arith-int-088.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-088.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-089.cvc b/test/regress/regress0/arith/integers/arith-int-089.cvc
index 5d7b9e2d2..7ff36d29e 100644
--- a/test/regress/regress0/arith/integers/arith-int-089.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-089.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-090.cvc b/test/regress/regress0/arith/integers/arith-int-090.cvc
index a9f4b03a4..52b9c13f0 100644
--- a/test/regress/regress0/arith/integers/arith-int-090.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-090.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-091.cvc b/test/regress/regress0/arith/integers/arith-int-091.cvc
index ebf728533..29a19db39 100644
--- a/test/regress/regress0/arith/integers/arith-int-091.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-091.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-092.cvc b/test/regress/regress0/arith/integers/arith-int-092.cvc
index f6622eb0b..51c8a6bc4 100644
--- a/test/regress/regress0/arith/integers/arith-int-092.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-092.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-093.cvc b/test/regress/regress0/arith/integers/arith-int-093.cvc
index 3cb1aed11..7d2123d41 100644
--- a/test/regress/regress0/arith/integers/arith-int-093.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-093.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-094.cvc b/test/regress/regress0/arith/integers/arith-int-094.cvc
index 4abce2679..a5f1aefce 100644
--- a/test/regress/regress0/arith/integers/arith-int-094.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-094.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-095.cvc b/test/regress/regress0/arith/integers/arith-int-095.cvc
index 3aa4b2489..bc47d6f49 100644
--- a/test/regress/regress0/arith/integers/arith-int-095.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-095.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-096.cvc b/test/regress/regress0/arith/integers/arith-int-096.cvc
index f409f37af..2f6cf3155 100644
--- a/test/regress/regress0/arith/integers/arith-int-096.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-096.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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;
diff --git a/test/regress/regress0/arith/integers/arith-int-097.cvc b/test/regress/regress0/arith/integers/arith-int-097.cvc
index f0fca22fb..b05061192 100644
--- a/test/regress/regress0/arith/integers/arith-int-097.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-097.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT (19 * x0) + (-11 * x1) + (-19 * x2) + (5 * x3) = 26 ;
 ASSERT  (1 * x0) + (-28 * x1) + (-2 * x2) + (15 * x3) < 9 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-098.cvc b/test/regress/regress0/arith/integers/arith-int-098.cvc
index 37a472265..08cfd9c9c 100644
--- a/test/regress/regress0/arith/integers/arith-int-098.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-098.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 x0, x1, x2, x3 : INT;
 ASSERT  (-28 * x0) + (12 * x1) + (-19 * x2) + (10 * x3) = 16 ;
 ASSERT  (19 * x0) + (-25 * x1) + (-8 * x2) + (-32 * x3) = 12;
diff --git a/test/regress/regress0/arith/integers/arith-int-099.cvc b/test/regress/regress0/arith/integers/arith-int-099.cvc
index 9ff8724af..0d74dcb39 100644
--- a/test/regress/regress0/arith/integers/arith-int-099.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-099.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-int-100.cvc b/test/regress/regress0/arith/integers/arith-int-100.cvc
index a75128232..7e07bee14 100644
--- a/test/regress/regress0/arith/integers/arith-int-100.cvc
+++ b/test/regress/regress0/arith/integers/arith-int-100.cvc
@@ -1,5 +1,4 @@
 % EXPECT: invalid
-% EXIT: 10
 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 ;
diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc b/test/regress/regress0/arith/integers/arith-interval.cvc
index e8b229faa..d79ec94a7 100644
--- a/test/regress/regress0/arith/integers/arith-interval.cvc
+++ b/test/regress/regress0/arith/integers/arith-interval.cvc
@@ -1,5 +1,4 @@
 % EXPECT: valid
-% EXIT: 20
 x: INT;
 P: INT -> BOOLEAN;
 
diff --git a/test/regress/regress0/arith/miplib-opt1217--27.smt.expect b/test/regress/regress0/arith/miplib-opt1217--27.smt.expect
index f6ae1d85b..f0bc97ee5 100644
--- a/test/regress/regress0/arith/miplib-opt1217--27.smt.expect
+++ b/test/regress/regress0/arith/miplib-opt1217--27.smt.expect
@@ -1,3 +1,2 @@
 % COMMAND-LINE: --enable-miplib-trick
 % EXPECT: unsat
-% EXIT: 20
diff --git a/test/regress/regress0/arith/miplib-opt1217--27.smt2 b/test/regress/regress0/arith/miplib-opt1217--27.smt2
index e6ac8e69e..dc0ca78a8 100644
--- a/test/regress/regress0/arith/miplib-opt1217--27.smt2
+++ b/test/regress/regress0/arith/miplib-opt1217--27.smt2
@@ -1,6 +1,5 @@
 ; COMMAND-LINE: --enable-miplib-trick
 ; EXPECT: unsat
-; EXIT: 20
 (set-logic QF_LRA)
 (set-info :source |
 Relaxation of the Mixed-Integer Programming
diff --git a/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect b/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect
index f6ae1d85b..f0bc97ee5 100644
--- a/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect
+++ b/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect
@@ -1,3 +1,2 @@
 % COMMAND-LINE: --enable-miplib-trick
 % EXPECT: unsat
-% EXIT: 20
diff --git a/test/regress/regress0/arith/miplib-pp08a-3000.smt2 b/test/regress/regress0/arith/miplib-pp08a-3000.smt2
index e94506a23..3e34badc2 100644
--- a/test/regress/regress0/arith/miplib-pp08a-3000.smt2
+++ b/test/regress/regress0/arith/miplib-pp08a-3000.smt2
@@ -1,6 +1,5 @@
 ; COMMAND-LINE: --enable-miplib-trick
 ; EXPECT: unsat
-; EXIT: 10
 (set-logic QF_LRA)
 (set-info :source |
 Relaxation of the Mixed-Integer Programming
diff --git a/test/regress/regress0/arith/miplib.cvc b/test/regress/regress0/arith/miplib.cvc
index db2aa2ac5..49c0b61cb 100644
--- a/test/regress/regress0/arith/miplib.cvc
+++ b/test/regress/regress0/arith/miplib.cvc
@@ -1,6 +1,5 @@
 % COMMAND-LINE: --enable-miplib-trick
 % EXPECT: sat
-% EXIT: 10
 
 tmp1, tmp2, tmp3 : INT;
 x, y, z : BOOLEAN;
diff --git a/test/regress/regress0/arith/miplib2.cvc b/test/regress/regress0/arith/miplib2.cvc
index 84f17e848..5cd2f545c 100644
--- a/test/regress/regress0/arith/miplib2.cvc
+++ b/test/regress/regress0/arith/miplib2.cvc
@@ -1,6 +1,5 @@
 % COMMAND-LINE: --enable-miplib-trick
 % EXPECT: sat
-% EXIT: 10
 
 tmp1, tmp2, tmp3 : INT;
 x, y, z : BOOLEAN;
diff --git a/test/regress/regress0/arith/miplib3.cvc b/test/regress/regress0/arith/miplib3.cvc
index 009effb74..9e1ae5a62 100644
--- a/test/regress/regress0/arith/miplib3.cvc
+++ b/test/regress/regress0/arith/miplib3.cvc
@@ -1,6 +1,5 @@
 % COMMAND-LINE: --enable-miplib-trick
 % EXPECT: sat
-% EXIT: 10
 
 tmp1, tmp2, tmp3, tmp4 : INT;
 x, y, z : BOOLEAN;
diff --git a/test/regress/regress0/arith/miplib4.cvc b/test/regress/regress0/arith/miplib4.cvc
index 2f7db1f54..9d7c4592e 100644
--- a/test/regress/regress0/arith/miplib4.cvc
+++ b/test/regress/regress0/arith/miplib4.cvc
@@ -1,6 +1,5 @@
 % COMMAND-LINE: --enable-miplib-trick
 % EXPECT: sat
-% EXIT: 10
 
 tmp1 : INT;
 x, y : BOOLEAN;
diff --git a/test/regress/regress0/arith/mod.01.smt2 b/test/regress/regress0/arith/mod.01.smt2
index 27a79ff17..f9633c597 100644
--- a/test/regress/regress0/arith/mod.01.smt2
+++ b/test/regress/regress0/arith/mod.01.smt2
@@ -1,5 +1,4 @@
 ; EXPECT: unknown
-; EXIT: 0
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.0)
 (set-info :status unknown)
diff --git a/test/regress/regress0/arith/mod.02.smt2 b/test/regress/regress0/arith/mod.02.smt2
index 75b25c181..c6281a5c2 100644
--- a/test/regress/regress0/arith/mod.02.smt2
+++ b/test/regress/regress0/arith/mod.02.smt2
@@ -1,5 +1,4 @@
 ; EXPECT: unknown
-; EXIT: 0
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.0)
 (set-info :status unknown)
diff --git a/test/regress/regress0/arith/mod.03.smt2 b/test/regress/regress0/arith/mod.03.smt2
index 760350c89..110de05d7 100644
--- a/test/regress/regress0/arith/mod.03.smt2
+++ b/test/regress/regress0/arith/mod.03.smt2
@@ -1,5 +1,4 @@
 ; EXPECT: unknown
-; EXIT: 0
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.0)
 (set-info :status unknown)
diff --git a/test/regress/regress0/arith/mult.01.smt2 b/test/regress/regress0/arith/mult.01.smt2
index 4b1a937f6..f415e0f25 100644
--- a/test/regress/regress0/arith/mult.01.smt2
+++ b/test/regress/regress0/arith/mult.01.smt2
@@ -1,5 +1,4 @@
 ; EXPECT: unknown
-; EXIT: 0
 (set-logic QF_NRA)
 (set-info :smt-lib-version 2.0)
 (set-info :status unknown)
-- 
cgit v1.2.3