diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-11 11:04:48 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-11 11:04:48 -0500 |
commit | 36e939d31e8ac8fe2866f996af44ea268447c295 (patch) | |
tree | 4f626fb54d0c2fd21a70149cf14f1b125c494bb4 /test/regress/regress0/push-pop | |
parent | 3ac85900def24af684565f77fe80589595998ad2 (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')
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 |