summaryrefslogtreecommitdiff
path: root/test/regress/regress0/push-pop
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-11-11 11:04:48 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-11-11 11:04:48 -0500
commit36e939d31e8ac8fe2866f996af44ea268447c295 (patch)
tree4f626fb54d0c2fd21a70149cf14f1b125c494bb4 /test/regress/regress0/push-pop
parent3ac85900def24af684565f77fe80589595998ad2 (diff)
Change exit status to be more consistent with other command-line tools: 0 success, nonzero error
Diffstat (limited to 'test/regress/regress0/push-pop')
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_1.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_10.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_11.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_12.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_13.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_14.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_15.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_2.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_3.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_4.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_5.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_6.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_7.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_8.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_9.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_1.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_2.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_3.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_4.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_5.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_6.smt21
-rw-r--r--test/regress/regress0/push-pop/arith_lra_01.smt21
-rw-r--r--test/regress/regress0/push-pop/arith_lra_02.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_1.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_10.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_11.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_12.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_13.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_14.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_15.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_16.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_18.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_19.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_1_to_52_merged.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_2.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_20.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_21.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_22.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_23.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_24.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_25.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_26.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_27.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_28.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_29.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_3.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_30.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_31.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_32.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_33.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_34.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_35.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_36.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_37.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_38.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_39.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_4.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_40.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_41.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_42.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_43.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_44.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_45.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_46.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_47.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_48.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_49.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_5.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_50.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_51.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_52.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_6.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_7.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_8.smt21
-rw-r--r--test/regress/regress0/push-pop/boolean/fuzz_9.smt21
-rw-r--r--test/regress/regress0/push-pop/bug216.smt2.expect1
-rw-r--r--test/regress/regress0/push-pop/bug233.cvc1
-rw-r--r--test/regress/regress0/push-pop/bug326.smt21
-rw-r--r--test/regress/regress0/push-pop/bug396.smt21
-rw-r--r--test/regress/regress0/push-pop/incremental-subst-bug.cvc1
-rw-r--r--test/regress/regress0/push-pop/test.00.cvc1
-rw-r--r--test/regress/regress0/push-pop/test.01.cvc1
-rw-r--r--test/regress/regress0/push-pop/tiny_bug.smt21
-rw-r--r--test/regress/regress0/push-pop/units.cvc1
84 files changed, 0 insertions, 84 deletions
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2
index 73399358a..bf2d2a8c3 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2
@@ -3,7 +3,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2
index cdd6a6b18..389c91573 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2
@@ -2,7 +2,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2
index 9078acf46..81fe3b046 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2
@@ -5,7 +5,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2
index f3d6d95de..d797c1897 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2
index ff78a7d39..2e4b9d2b8 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2
index 01191c4da..0399bbffa 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2
@@ -5,7 +5,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2
index e4b824dcc..2a8ffe0fa 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2
@@ -5,7 +5,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2
index 3003fa52b..cbff796c6 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2
index c437a5fb8..ec072821c 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2
@@ -3,7 +3,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2
index 4d42615f4..93be94865 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2
@@ -3,7 +3,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2
index a566eb1f3..fd9204081 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2
@@ -7,7 +7,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2
index 7fcd67745..1901016c2 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2
@@ -5,7 +5,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2
index 88fd866de..c3b8aadc7 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2
@@ -5,7 +5,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2
index 329be0391..cebf4d3e6 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2
index db180f3f4..96aaf9f51 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2
index 9e61f7c4d..05414230a 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2
index cfcd80a44..9c387d89f 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2
index f79d3ee69..b61eb001f 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2
@@ -7,7 +7,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2
index 95a64c578..5d46d281f 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2
@@ -6,7 +6,6 @@
; EXPECT: unsat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2
index 8b41d054c..72b2aa088 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2
index 8da0aeb7e..1cffc92cb 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith_lra_01.smt2 b/test/regress/regress0/push-pop/arith_lra_01.smt2
index 06a22458c..4216f429a 100644
--- a/test/regress/regress0/push-pop/arith_lra_01.smt2
+++ b/test/regress/regress0/push-pop/arith_lra_01.smt2
@@ -16,7 +16,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith_lra_02.smt2 b/test/regress/regress0/push-pop/arith_lra_02.smt2
index 74547db91..3cb5674d1 100644
--- a/test/regress/regress0/push-pop/arith_lra_02.smt2
+++ b/test/regress/regress0/push-pop/arith_lra_02.smt2
@@ -17,7 +17,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_1.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_1.smt2
index a3440c77d..0af648d26 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_1.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_1.smt2
@@ -12,7 +12,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_10.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_10.smt2
index 74be6275a..53493d261 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_10.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_10.smt2
@@ -11,7 +11,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_11.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_11.smt2
index 9cd4a519d..5307ec839 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_11.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_11.smt2
@@ -16,7 +16,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_12.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_12.smt2
index f0ca9c801..172c3d4eb 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_12.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_12.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_13.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_13.smt2
index d5a649471..1752797eb 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_13.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_13.smt2
@@ -3,7 +3,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_14.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_14.smt2
index c8e3566d5..47612e894 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_14.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_14.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_15.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_15.smt2
index 56b2707f5..4345c3231 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_15.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_15.smt2
@@ -4,7 +4,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_16.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_16.smt2
index e686367bd..715b1872c 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_16.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_16.smt2
@@ -9,7 +9,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_18.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_18.smt2
index 7952f0b56..90a9f2332 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_18.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_18.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_19.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_19.smt2
index f29a11344..cbfda64df 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_19.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_19.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_1_to_52_merged.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_1_to_52_merged.smt2
index 7a943e03d..5b225557f 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_1_to_52_merged.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_1_to_52_merged.smt2
@@ -449,7 +449,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(push 1)
(declare-fun x0 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_2.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_2.smt2
index 17dd07336..f7812731d 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_2.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_2.smt2
@@ -2,7 +2,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_20.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_20.smt2
index 0142fe480..b37d6c035 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_20.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_20.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_21.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_21.smt2
index fd1345282..a86c1f8da 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_21.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_21.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_22.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_22.smt2
index f4f71ddd1..9a67f6781 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_22.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_22.smt2
@@ -10,7 +10,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_23.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_23.smt2
index 49fb1e4e2..22ed7dfa5 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_23.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_23.smt2
@@ -7,7 +7,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_24.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_24.smt2
index 4c1ce822d..edff03a9d 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_24.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_24.smt2
@@ -7,7 +7,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_25.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_25.smt2
index 4678a4de7..8ec42e5fc 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_25.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_25.smt2
@@ -16,7 +16,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_26.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_26.smt2
index 9922102b9..d4fd2c710 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_26.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_26.smt2
@@ -10,7 +10,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_27.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_27.smt2
index b961ba72d..828440ef4 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_27.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_27.smt2
@@ -10,7 +10,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_28.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_28.smt2
index 63189797e..09933d521 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_28.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_28.smt2
@@ -7,7 +7,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_29.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_29.smt2
index 1c7586be5..38e72425e 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_29.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_29.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_3.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_3.smt2
index 64693f829..958d44a82 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_3.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_3.smt2
@@ -6,7 +6,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_30.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_30.smt2
index 7f57788c3..58f55bda0 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_30.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_30.smt2
@@ -14,7 +14,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_31.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_31.smt2
index 3df801225..3998897fb 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_31.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_31.smt2
@@ -7,7 +7,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_32.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_32.smt2
index 62efd69ba..109b86ec0 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_32.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_32.smt2
@@ -13,7 +13,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_33.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_33.smt2
index bde870b96..ce2c41beb 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_33.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_33.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_34.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_34.smt2
index e82c6dec1..e1ea02cad 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_34.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_34.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_35.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_35.smt2
index f925e3a04..a2fc1e367 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_35.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_35.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_36.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_36.smt2
index 2b39a3898..e0d0c8bed 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_36.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_36.smt2
@@ -5,7 +5,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_37.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_37.smt2
index 6391cb6d5..cf34c5d35 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_37.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_37.smt2
@@ -11,7 +11,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_38.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_38.smt2
index 25c2620fb..770769878 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_38.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_38.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_39.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_39.smt2
index 363dc0462..abadcc2c1 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_39.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_39.smt2
@@ -17,7 +17,6 @@
; EXPECT: unsat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_4.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_4.smt2
index abe69436a..db191f610 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_4.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_4.smt2
@@ -10,7 +10,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_40.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_40.smt2
index 855dd811b..dfde9eef6 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_40.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_40.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_41.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_41.smt2
index 0fbefd267..b6d2e884f 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_41.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_41.smt2
@@ -4,7 +4,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_42.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_42.smt2
index d02eb035b..2e737763f 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_42.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_42.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_43.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_43.smt2
index 66f745c30..88349dbff 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_43.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_43.smt2
@@ -11,7 +11,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_44.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_44.smt2
index 763e3ecfa..968d30c2e 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_44.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_44.smt2
@@ -2,7 +2,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_45.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_45.smt2
index 228450d7e..1294df46f 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_45.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_45.smt2
@@ -9,7 +9,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_46.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_46.smt2
index 784a6a3c0..d680b0ac7 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_46.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_46.smt2
@@ -9,7 +9,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_47.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_47.smt2
index 69ceead2a..011b37920 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_47.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_47.smt2
@@ -3,7 +3,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
-; EXIT: 20
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_48.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_48.smt2
index 13f626204..13c6d8743 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_48.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_48.smt2
@@ -3,7 +3,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
-; EXIT: 20
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_49.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_49.smt2
index f82ee00b6..1f529f5c8 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_49.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_49.smt2
@@ -1,7 +1,6 @@
; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: unsat
-; EXIT: 20
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_5.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_5.smt2
index 0e30d296c..a29fda6e1 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_5.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_5.smt2
@@ -14,7 +14,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_50.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_50.smt2
index 325d7c415..1d783a59c 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_50.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_50.smt2
@@ -1,7 +1,6 @@
; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: unsat
-; EXIT: 20
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(assert (not (not (or x0 x0))))
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_51.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_51.smt2
index a5d312aff..f9bdb084f 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_51.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_51.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
-; EXIT: 20
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(check-sat)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_52.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_52.smt2
index dd7bbefe3..2ab146602 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_52.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_52.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
-; EXIT: 20
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_6.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_6.smt2
index 9ed3737be..14e82a48a 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_6.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_6.smt2
@@ -5,7 +5,6 @@
; EXPECT: unsat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_7.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_7.smt2
index edb16c09f..b39a6f88f 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_7.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_7.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_8.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_8.smt2
index 01afa0d75..a12773352 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_8.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_8.smt2
@@ -7,7 +7,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/boolean/fuzz_9.smt2 b/test/regress/regress0/push-pop/boolean/fuzz_9.smt2
index 90466c9cf..3ed852966 100644
--- a/test/regress/regress0/push-pop/boolean/fuzz_9.smt2
+++ b/test/regress/regress0/push-pop/boolean/fuzz_9.smt2
@@ -9,7 +9,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LIA)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
diff --git a/test/regress/regress0/push-pop/bug216.smt2.expect b/test/regress/regress0/push-pop/bug216.smt2.expect
index 9a8435b2d..fe118171a 100644
--- a/test/regress/regress0/push-pop/bug216.smt2.expect
+++ b/test/regress/regress0/push-pop/bug216.smt2.expect
@@ -1,4 +1,3 @@
% COMMAND-LINE: --incremental
% EXPECT: sat
% EXPECT: unsat
-% EXIT: 20
diff --git a/test/regress/regress0/push-pop/bug233.cvc b/test/regress/regress0/push-pop/bug233.cvc
index c951aaf2e..2b9eedcdb 100644
--- a/test/regress/regress0/push-pop/bug233.cvc
+++ b/test/regress/regress0/push-pop/bug233.cvc
@@ -9,4 +9,3 @@ QUERY (a AND b) OR NOT (a AND b);
% EXPECT: invalid
QUERY (a OR b);
-% EXIT: 10
diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2
index d32d6fddf..8fe88e9f5 100644
--- a/test/regress/regress0/push-pop/bug326.smt2
+++ b/test/regress/regress0/push-pop/bug326.smt2
@@ -1,5 +1,4 @@
; COMMAND-LINE: --incremental
-; EXIT: 10
(set-logic AUFLIA)
diff --git a/test/regress/regress0/push-pop/bug396.smt2 b/test/regress/regress0/push-pop/bug396.smt2
index 27d309ec6..8e93cf447 100644
--- a/test/regress/regress0/push-pop/bug396.smt2
+++ b/test/regress/regress0/push-pop/bug396.smt2
@@ -9,7 +9,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: unsat
-; EXIT: 20
;(set-option :produce-unsat-cores true)
(set-option :print-success false)
(set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/push-pop/incremental-subst-bug.cvc b/test/regress/regress0/push-pop/incremental-subst-bug.cvc
index b9936bfa4..9b10ef843 100644
--- a/test/regress/regress0/push-pop/incremental-subst-bug.cvc
+++ b/test/regress/regress0/push-pop/incremental-subst-bug.cvc
@@ -19,4 +19,3 @@ QUERY z /= x;
POP;
% EXPECT: invalid
QUERY z /= x;
-% EXIT: 10
diff --git a/test/regress/regress0/push-pop/test.00.cvc b/test/regress/regress0/push-pop/test.00.cvc
index f56abb386..78d7b9f2c 100644
--- a/test/regress/regress0/push-pop/test.00.cvc
+++ b/test/regress/regress0/push-pop/test.00.cvc
@@ -9,4 +9,3 @@ POP;
ASSERT (NOT x);
% EXPECT: sat
CHECKSAT;
-% EXIT: 10
diff --git a/test/regress/regress0/push-pop/test.01.cvc b/test/regress/regress0/push-pop/test.01.cvc
index 5d492db32..2bb5877f5 100644
--- a/test/regress/regress0/push-pop/test.01.cvc
+++ b/test/regress/regress0/push-pop/test.01.cvc
@@ -17,4 +17,3 @@ CHECKSAT;
POP;
% EXPECT: sat
CHECKSAT;
-% EXIT: 10
diff --git a/test/regress/regress0/push-pop/tiny_bug.smt2 b/test/regress/regress0/push-pop/tiny_bug.smt2
index 83ccca49e..b67381baa 100644
--- a/test/regress/regress0/push-pop/tiny_bug.smt2
+++ b/test/regress/regress0/push-pop/tiny_bug.smt2
@@ -1,7 +1,6 @@
; COMMAND-LINE: --incremental --simplification=none
; EXPECT: sat
; EXPECT: unsat
-; EXIT: 20
(set-logic QF_UFLIA)
(declare-fun base () Int)
(declare-fun n () Int)
diff --git a/test/regress/regress0/push-pop/units.cvc b/test/regress/regress0/push-pop/units.cvc
index 9bdfdaadb..edc868a79 100644
--- a/test/regress/regress0/push-pop/units.cvc
+++ b/test/regress/regress0/push-pop/units.cvc
@@ -17,4 +17,3 @@ PUSH;
POP;
% EXPECT: sat
CHECKSAT;
-% EXIT: 10
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback