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/regress1 | |
| parent | 3ac85900def24af684565f77fe80589595998ad2 (diff) | |
Change exit status to be more consistent with other command-line tools: 0 success, nonzero error
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect | 1 | ||||
| -rw-r--r-- | test/regress/regress1/GEO123+1.minimized.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress1/bug394.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress1/hole7.cvc | 1 | ||||
| -rw-r--r-- | test/regress/regress1/hole8.cvc | 1 | ||||
| -rw-r--r-- | test/regress/regress1/typed_v1l50016-simp.cvc | 1 | ||||
| -rw-r--r-- | test/regress/regress1/uflia-error0.smt2.expect | 1 | ||||
| -rw-r--r-- | test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect | 1 |
8 files changed, 0 insertions, 8 deletions
diff --git a/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect b/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect index a06e9864e..7cb6ba8c2 100644 --- a/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect +++ b/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect @@ -1,4 +1,3 @@ % COMMAND-LINE: --incremental % EXPECT: unsat % EXPECT: sat -% EXIT: 10 diff --git a/test/regress/regress1/GEO123+1.minimized.smt2 b/test/regress/regress1/GEO123+1.minimized.smt2 index 8cc1fa7fd..764c41699 100644 --- a/test/regress/regress1/GEO123+1.minimized.smt2 +++ b/test/regress/regress1/GEO123+1.minimized.smt2 @@ -1,7 +1,6 @@ ; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: sat -; EXIT: 10 ; ; This is a benchmark demonstrating a nasty incremental bug in the UF ; symmetry breaker, now fixed. diff --git a/test/regress/regress1/bug394.smt2 b/test/regress/regress1/bug394.smt2 index cb2bc32a8..99e19e7fb 100644 --- a/test/regress/regress1/bug394.smt2 +++ b/test/regress/regress1/bug394.smt2 @@ -11,7 +11,6 @@ ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat -; EXIT: 10 ;(set-option :produce-unsat-cores true) (set-option :print-success false) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress1/hole7.cvc index 150c39e38..1f762477a 100644 --- a/test/regress/regress1/hole7.cvc +++ b/test/regress/regress1/hole7.cvc @@ -262,4 +262,3 @@ ASSERT x_56 OR x_55 OR x_54 OR x_53 OR x_52 OR x_51 OR x_50; QUERY FALSE; -% EXIT: 20 diff --git a/test/regress/regress1/hole8.cvc b/test/regress/regress1/hole8.cvc index fb9206aa0..705c95ea6 100644 --- a/test/regress/regress1/hole8.cvc +++ b/test/regress/regress1/hole8.cvc @@ -371,4 +371,3 @@ ASSERT x_72 OR x_71 OR x_70 OR x_69 OR x_68 OR x_67 OR x_66 OR x_65; QUERY FALSE; -% EXIT: 20 diff --git a/test/regress/regress1/typed_v1l50016-simp.cvc b/test/regress/regress1/typed_v1l50016-simp.cvc index b273d99e9..b4a1e4b32 100644 --- a/test/regress/regress1/typed_v1l50016-simp.cvc +++ b/test/regress/regress1/typed_v1l50016-simp.cvc @@ -1,5 +1,4 @@ % EXPECT: invalid -% EXIT: 10 DATATYPE nat = succ(pred : nat) | zero, diff --git a/test/regress/regress1/uflia-error0.smt2.expect b/test/regress/regress1/uflia-error0.smt2.expect index b862d0b39..7fd1d5a98 100644 --- a/test/regress/regress1/uflia-error0.smt2.expect +++ b/test/regress/regress1/uflia-error0.smt2.expect @@ -1,3 +1,2 @@ % COMMAND-LINE: --decision=justification % EXPECT: unsat -% EXIT: 20 diff --git a/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect b/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect index b862d0b39..7fd1d5a98 100644 --- a/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect +++ b/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect @@ -1,3 +1,2 @@ % COMMAND-LINE: --decision=justification % EXPECT: unsat -% EXIT: 20 |