summaryrefslogtreecommitdiff
path: root/test/regress/regress0/push-pop/boolean
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/boolean
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/boolean')
-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
52 files changed, 0 insertions, 52 deletions
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback