diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-21 09:41:50 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-21 09:41:50 -0700 |
| commit | be2702490d684c100ba6abe76ee156078a9aa621 (patch) | |
| tree | 8b22bc7e38aad39da092b409dded4d2ce84b4047 /test | |
| parent | 8f0aae827e16f4dfcebb8dad2cc528649d40b16a (diff) | |
Fix various regression tests (#1657)
While reorganizing the regression tests, I found three tests with a
wrong status, one that CVC4 reported unknown for and some regression
tests that had command line options set in the Makefile.am instead of
the tests themselves. This commit fixes the status of the three
regression tests (verified the status with Z3), adds command line
options to make the previously "unknown" test work, and moves the
command line options from the Makefile.am into the individual regression
tests. The latter also required some minor changes to the regression
script because it would not try to determine the expected output from
the (set-info :status ...) command if there was one directive (such as
EXPECT/COMMAND-LINE/etc.). This was an issue with the tests that now
have a COMMAND-LINE directive.
Diffstat (limited to 'test')
94 files changed, 115 insertions, 31 deletions
diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index 5df254bad..179398c9d 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -13,9 +13,6 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif -override CVC4_REGRESSION_ARGS += --rewrite-rules -export CVC4_REGRESSION_ARGS - MAKEFLAGS = -k # These are run for all build profiles. diff --git a/test/regress/regress0/rewriterules/datatypes.smt2 b/test/regress/regress0/rewriterules/datatypes.smt2 index a914a0c1f..9a5f68100 100644 --- a/test/regress/regress0/rewriterules/datatypes.smt2 +++ b/test/regress/regress0/rewriterules/datatypes.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; try to solve datatypes with rewriterules (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress0/rewriterules/datatypes_clark.smt2 b/test/regress/regress0/rewriterules/datatypes_clark.smt2 index 19163f49d..cc217fc79 100644 --- a/test/regress/regress0/rewriterules/datatypes_clark.smt2 +++ b/test/regress/regress0/rewriterules/datatypes_clark.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules (set-logic AUFLIRA) ;; DATATYPE diff --git a/test/regress/regress0/rewriterules/length.smt2 b/test/regress/regress0/rewriterules/length.smt2 index 215698ade..b144d7745 100644 --- a/test/regress/regress0/rewriterules/length.smt2 +++ b/test/regress/regress0/rewriterules/length.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress0/rewriterules/length_gen_n.smt2 b/test/regress/regress0/rewriterules/length_gen_n.smt2 index 5d1255eb0..7da2f6777 100644 --- a/test/regress/regress0/rewriterules/length_gen_n.smt2 +++ b/test/regress/regress0/rewriterules/length_gen_n.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 index b1462cf98..7d65356ad 100644 --- a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 +++ b/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress0/rewriterules/length_trick.smt2 b/test/regress/regress0/rewriterules/length_trick.smt2 index 84afc5815..e01e97b84 100644 --- a/test/regress/regress0/rewriterules/length_trick.smt2 +++ b/test/regress/regress0/rewriterules/length_trick.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress0/rewriterules/length_trick2.smt2 b/test/regress/regress0/rewriterules/length_trick2.smt2 index af9e7f07d..8d47d9550 100644 --- a/test/regress/regress0/rewriterules/length_trick2.smt2 +++ b/test/regress/regress0/rewriterules/length_trick2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress0/rewriterules/native_arrays.smt2 b/test/regress/regress0/rewriterules/native_arrays.smt2 index b7d19b612..83de7d8f4 100644 --- a/test/regress/regress0/rewriterules/native_arrays.smt2 +++ b/test/regress/regress0/rewriterules/native_arrays.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; This example can't be done if we don't access the EqualityEngine of ;; the theory of arrays diff --git a/test/regress/regress0/rewriterules/native_datatypes.smt2 b/test/regress/regress0/rewriterules/native_datatypes.smt2 index c3c4aad73..365ec0624 100644 --- a/test/regress/regress0/rewriterules/native_datatypes.smt2 +++ b/test/regress/regress0/rewriterules/native_datatypes.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress0/rewriterules/relation.smt2 b/test/regress/regress0/rewriterules/relation.smt2 index e8c0139e8..6b55a9677 100644 --- a/test/regress/regress0/rewriterules/relation.smt2 +++ b/test/regress/regress0/rewriterules/relation.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 index 838c0cd16..f67a0e6a2 100644 --- a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 +++ b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index dd8621618..65f96f469 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -49,7 +49,8 @@ TESTS = \ cnf-ite.smt2 \ cnf-and-neg.smt2 \ cnf_abc.smt2 \ - bool-pred-nested.smt2 + bool-pred-nested.smt2 \ + pred.smt EXTRA_DIST = $(TESTS) \ mkpidgeon diff --git a/test/regress/regress0/uf/pred.smt b/test/regress/regress0/uf/pred.smt index e6f82727e..bdc49e7ce 100644 --- a/test/regress/regress0/uf/pred.smt +++ b/test/regress/regress0/uf/pred.smt @@ -1,5 +1,5 @@ -(benchmark euf_simp1.smt -:status sat +(benchmark pred.smt +:status unsat :logic QF_UF :category { crafted } diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am index 0d0c7cdb2..7a8577677 100644 --- a/test/regress/regress0/unconstrained/Makefile.am +++ b/test/regress/regress0/unconstrained/Makefile.am @@ -13,10 +13,6 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif -# models not supported with unconstrained simp -override CVC4_REGRESSION_ARGS += --unconstrained-simp --no-check-models -export CVC4_REGRESSION_ARGS - MAKEFLAGS = -k # These are run for all build profiles. diff --git a/test/regress/regress0/unconstrained/arith.smt2 b/test/regress/regress0/unconstrained/arith.smt2 index dc2b27414..3dfab3b0e 100644 --- a/test/regress/regress0/unconstrained/arith.smt2 +++ b/test/regress/regress0/unconstrained/arith.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/arith2.smt2 b/test/regress/regress0/unconstrained/arith2.smt2 index f9e829e45..d6206287a 100644 --- a/test/regress/regress0/unconstrained/arith2.smt2 +++ b/test/regress/regress0/unconstrained/arith2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFLIRA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/arith3.smt2 b/test/regress/regress0/unconstrained/arith3.smt2 index 83634a50a..fd24c3f65 100644 --- a/test/regress/regress0/unconstrained/arith3.smt2 +++ b/test/regress/regress0/unconstrained/arith3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFLIRA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/arith4.smt2 b/test/regress/regress0/unconstrained/arith4.smt2 index 2b06d5ea8..507a18a78 100644 --- a/test/regress/regress0/unconstrained/arith4.smt2 +++ b/test/regress/regress0/unconstrained/arith4.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFNIRA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/arith5.smt2 b/test/regress/regress0/unconstrained/arith5.smt2 index de1e305bc..5e54083a5 100644 --- a/test/regress/regress0/unconstrained/arith5.smt2 +++ b/test/regress/regress0/unconstrained/arith5.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLRA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/arith6.smt2 b/test/regress/regress0/unconstrained/arith6.smt2 index 05653415f..ce3630264 100644 --- a/test/regress/regress0/unconstrained/arith6.smt2 +++ b/test/regress/regress0/unconstrained/arith6.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLRA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/arith7.smt2 b/test/regress/regress0/unconstrained/arith7.smt2 index 6cc063ca4..105320632 100644 --- a/test/regress/regress0/unconstrained/arith7.smt2 +++ b/test/regress/regress0/unconstrained/arith7.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFLIRA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/array1.smt2 b/test/regress/regress0/unconstrained/array1.smt2 index 82f084e87..f1acfa759 100644 --- a/test/regress/regress0/unconstrained/array1.smt2 +++ b/test/regress/regress0/unconstrained/array1.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBV) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvbool.smt2 b/test/regress/regress0/unconstrained/bvbool.smt2 index 0dded2a2f..b1943124e 100644 --- a/test/regress/regress0/unconstrained/bvbool.smt2 +++ b/test/regress/regress0/unconstrained/bvbool.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvbool2.smt2 b/test/regress/regress0/unconstrained/bvbool2.smt2 index 949096224..49b7d5fc8 100644 --- a/test/regress/regress0/unconstrained/bvbool2.smt2 +++ b/test/regress/regress0/unconstrained/bvbool2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvbool3.smt2 b/test/regress/regress0/unconstrained/bvbool3.smt2 index a689804f7..f24b129e0 100644 --- a/test/regress/regress0/unconstrained/bvbool3.smt2 +++ b/test/regress/regress0/unconstrained/bvbool3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvcmp.smt2 b/test/regress/regress0/unconstrained/bvcmp.smt2 index ba7316324..ae50d350c 100644 --- a/test/regress/regress0/unconstrained/bvcmp.smt2 +++ b/test/regress/regress0/unconstrained/bvcmp.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvconcat.smt2 b/test/regress/regress0/unconstrained/bvconcat.smt2 index e2941b34a..6f4e38ec7 100644 --- a/test/regress/regress0/unconstrained/bvconcat.smt2 +++ b/test/regress/regress0/unconstrained/bvconcat.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvconcat2.smt2 b/test/regress/regress0/unconstrained/bvconcat2.smt2 index aa901b9b0..789e4c6c8 100644 --- a/test/regress/regress0/unconstrained/bvconcat2.smt2 +++ b/test/regress/regress0/unconstrained/bvconcat2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvdiv.smt2 b/test/regress/regress0/unconstrained/bvdiv.smt2 index d3cadf6c8..990a8d457 100644 --- a/test/regress/regress0/unconstrained/bvdiv.smt2 +++ b/test/regress/regress0/unconstrained/bvdiv.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvext.smt2 b/test/regress/regress0/unconstrained/bvext.smt2 index 56289e245..b31efe3aa 100644 --- a/test/regress/regress0/unconstrained/bvext.smt2 +++ b/test/regress/regress0/unconstrained/bvext.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvite.smt2 b/test/regress/regress0/unconstrained/bvite.smt2 index 9e1ecc193..3cac4670b 100644 --- a/test/regress/regress0/unconstrained/bvite.smt2 +++ b/test/regress/regress0/unconstrained/bvite.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvmul.smt2 b/test/regress/regress0/unconstrained/bvmul.smt2 index fc56695f5..a109d9471 100644 --- a/test/regress/regress0/unconstrained/bvmul.smt2 +++ b/test/regress/regress0/unconstrained/bvmul.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvmul2.smt2 b/test/regress/regress0/unconstrained/bvmul2.smt2 index 89e4ff569..4e413c24f 100644 --- a/test/regress/regress0/unconstrained/bvmul2.smt2 +++ b/test/regress/regress0/unconstrained/bvmul2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvmul3.smt2 b/test/regress/regress0/unconstrained/bvmul3.smt2 index ea67a1b5a..71cf37371 100644 --- a/test/regress/regress0/unconstrained/bvmul3.smt2 +++ b/test/regress/regress0/unconstrained/bvmul3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvnot.smt2 b/test/regress/regress0/unconstrained/bvnot.smt2 index 22fc7e7d2..4f62d2a0d 100644 --- a/test/regress/regress0/unconstrained/bvnot.smt2 +++ b/test/regress/regress0/unconstrained/bvnot.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvsle.smt2 b/test/regress/regress0/unconstrained/bvsle.smt2 index 702f9d7a0..391a6c9d7 100644 --- a/test/regress/regress0/unconstrained/bvsle.smt2 +++ b/test/regress/regress0/unconstrained/bvsle.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvsle2.smt2 b/test/regress/regress0/unconstrained/bvsle2.smt2 index b797fa4e8..f23b119fe 100644 --- a/test/regress/regress0/unconstrained/bvsle2.smt2 +++ b/test/regress/regress0/unconstrained/bvsle2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvsle3.smt2 b/test/regress/regress0/unconstrained/bvsle3.smt2 index 4d897830c..2887cdca8 100644 --- a/test/regress/regress0/unconstrained/bvsle3.smt2 +++ b/test/regress/regress0/unconstrained/bvsle3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvsle4.smt2 b/test/regress/regress0/unconstrained/bvsle4.smt2 index 8927a5f2e..289104ec8 100644 --- a/test/regress/regress0/unconstrained/bvsle4.smt2 +++ b/test/regress/regress0/unconstrained/bvsle4.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvsle5.smt2 b/test/regress/regress0/unconstrained/bvsle5.smt2 index 1aceacbe3..cbe15db58 100644 --- a/test/regress/regress0/unconstrained/bvsle5.smt2 +++ b/test/regress/regress0/unconstrained/bvsle5.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvslt.smt2 b/test/regress/regress0/unconstrained/bvslt.smt2 index f98375653..2e20460c5 100644 --- a/test/regress/regress0/unconstrained/bvslt.smt2 +++ b/test/regress/regress0/unconstrained/bvslt.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvslt2.smt2 b/test/regress/regress0/unconstrained/bvslt2.smt2 index e56500ad2..743cfbebe 100644 --- a/test/regress/regress0/unconstrained/bvslt2.smt2 +++ b/test/regress/regress0/unconstrained/bvslt2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvslt3.smt2 b/test/regress/regress0/unconstrained/bvslt3.smt2 index a4af152f1..db1f3dcd9 100644 --- a/test/regress/regress0/unconstrained/bvslt3.smt2 +++ b/test/regress/regress0/unconstrained/bvslt3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvslt4.smt2 b/test/regress/regress0/unconstrained/bvslt4.smt2 index d702b6d1a..9c696d48b 100644 --- a/test/regress/regress0/unconstrained/bvslt4.smt2 +++ b/test/regress/regress0/unconstrained/bvslt4.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvslt5.smt2 b/test/regress/regress0/unconstrained/bvslt5.smt2 index f4b6a7a63..c5696f0a2 100644 --- a/test/regress/regress0/unconstrained/bvslt5.smt2 +++ b/test/regress/regress0/unconstrained/bvslt5.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvule.smt2 b/test/regress/regress0/unconstrained/bvule.smt2 index cbbb4cc6e..d0678d87c 100644 --- a/test/regress/regress0/unconstrained/bvule.smt2 +++ b/test/regress/regress0/unconstrained/bvule.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvule2.smt2 b/test/regress/regress0/unconstrained/bvule2.smt2 index 0e6f5916b..5dfa6c1b1 100644 --- a/test/regress/regress0/unconstrained/bvule2.smt2 +++ b/test/regress/regress0/unconstrained/bvule2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvule3.smt2 b/test/regress/regress0/unconstrained/bvule3.smt2 index 11e3a9877..e9892e598 100644 --- a/test/regress/regress0/unconstrained/bvule3.smt2 +++ b/test/regress/regress0/unconstrained/bvule3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvule4.smt2 b/test/regress/regress0/unconstrained/bvule4.smt2 index b8d978b71..0fccae301 100644 --- a/test/regress/regress0/unconstrained/bvule4.smt2 +++ b/test/regress/regress0/unconstrained/bvule4.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvule5.smt2 b/test/regress/regress0/unconstrained/bvule5.smt2 index cd927d0c6..4d4e0e95f 100644 --- a/test/regress/regress0/unconstrained/bvule5.smt2 +++ b/test/regress/regress0/unconstrained/bvule5.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvult.smt2 b/test/regress/regress0/unconstrained/bvult.smt2 index fb94994b4..9429237a4 100644 --- a/test/regress/regress0/unconstrained/bvult.smt2 +++ b/test/regress/regress0/unconstrained/bvult.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvult2.smt2 b/test/regress/regress0/unconstrained/bvult2.smt2 index 3fb4a0d23..c86699b48 100644 --- a/test/regress/regress0/unconstrained/bvult2.smt2 +++ b/test/regress/regress0/unconstrained/bvult2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvult3.smt2 b/test/regress/regress0/unconstrained/bvult3.smt2 index b11ab9da3..ceb19ea75 100644 --- a/test/regress/regress0/unconstrained/bvult3.smt2 +++ b/test/regress/regress0/unconstrained/bvult3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvult4.smt2 b/test/regress/regress0/unconstrained/bvult4.smt2 index 8170ec280..04008c006 100644 --- a/test/regress/regress0/unconstrained/bvult4.smt2 +++ b/test/regress/regress0/unconstrained/bvult4.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/bvult5.smt2 b/test/regress/regress0/unconstrained/bvult5.smt2 index 545bcbf64..53f76f0d3 100644 --- a/test/regress/regress0/unconstrained/bvult5.smt2 +++ b/test/regress/regress0/unconstrained/bvult5.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/geq.smt2 b/test/regress/regress0/unconstrained/geq.smt2 index 818bb55b3..d3bcc506f 100644 --- a/test/regress/regress0/unconstrained/geq.smt2 +++ b/test/regress/regress0/unconstrained/geq.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/gt.smt2 b/test/regress/regress0/unconstrained/gt.smt2 index 76b119e42..d4d6d4a5d 100644 --- a/test/regress/regress0/unconstrained/gt.smt2 +++ b/test/regress/regress0/unconstrained/gt.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/ite.smt2 b/test/regress/regress0/unconstrained/ite.smt2 index 4dc1cc295..54f092b8c 100644 --- a/test/regress/regress0/unconstrained/ite.smt2 +++ b/test/regress/regress0/unconstrained/ite.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBV ) (set-info :status sat) (declare-sort U 0) diff --git a/test/regress/regress0/unconstrained/leq.smt2 b/test/regress/regress0/unconstrained/leq.smt2 index 6c03fc254..4eea4df9c 100644 --- a/test/regress/regress0/unconstrained/leq.smt2 +++ b/test/regress/regress0/unconstrained/leq.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/lt.smt2 b/test/regress/regress0/unconstrained/lt.smt2 index 637a6407f..a0a42f4ef 100644 --- a/test/regress/regress0/unconstrained/lt.smt2 +++ b/test/regress/regress0/unconstrained/lt.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/mult1.smt2 b/test/regress/regress0/unconstrained/mult1.smt2 index fdad322af..4a29d9a92 100644 --- a/test/regress/regress0/unconstrained/mult1.smt2 +++ b/test/regress/regress0/unconstrained/mult1.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_LIA) (set-info :status sat) diff --git a/test/regress/regress0/unconstrained/uf1.smt2 b/test/regress/regress0/unconstrained/uf1.smt2 index 0b2a95f49..3e28c2f8b 100644 --- a/test/regress/regress0/unconstrained/uf1.smt2 +++ b/test/regress/regress0/unconstrained/uf1.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/unconstrained/xor.smt2 b/test/regress/regress0/unconstrained/xor.smt2 index 4089bb5dc..fcc66b015 100644 --- a/test/regress/regress0/unconstrained/xor.smt2 +++ b/test/regress/regress0/unconstrained/xor.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress1/quantifiers/Makefile.am b/test/regress/regress1/quantifiers/Makefile.am index 159f2e088..af277af90 100644 --- a/test/regress/regress1/quantifiers/Makefile.am +++ b/test/regress/regress1/quantifiers/Makefile.am @@ -80,7 +80,8 @@ TESTS = \ RNDPRE_4_1-dd-nqe.smt2 \ set8.smt2 \ z3.620661-no-fv-trigger.smt2 \ - arith-rec-fun.smt2 + arith-rec-fun.smt2 \ + set3.smt2 # removed because they take more than 20s # javafe.ast.ArrayInit.35.smt2 diff --git a/test/regress/regress1/quantifiers/set3.smt2 b/test/regress/regress1/quantifiers/set3.smt2 index d3e51d996..bd208c6d3 100644 --- a/test/regress/regress1/quantifiers/set3.smt2 +++ b/test/regress/regress1/quantifiers/set3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --full-saturate-quant (set-logic AUFLIA) (set-info :source | Assertion verification of simple set manipulation programs. |) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress1/rewriterules/Makefile.am b/test/regress/regress1/rewriterules/Makefile.am index fbf3db47a..6c5ce19fb 100644 --- a/test/regress/regress1/rewriterules/Makefile.am +++ b/test/regress/regress1/rewriterules/Makefile.am @@ -13,9 +13,6 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif -override CVC4_REGRESSION_ARGS += --rewrite-rules -export CVC4_REGRESSION_ARGS - MAKEFLAGS = -k # These are run for all build profiles. diff --git a/test/regress/regress1/rewriterules/datatypes2.smt2 b/test/regress/regress1/rewriterules/datatypes2.smt2 index 277ddc3ae..4ef40597a 100644 --- a/test/regress/regress1/rewriterules/datatypes2.smt2 +++ b/test/regress/regress1/rewriterules/datatypes2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; try to solve datatypes with rewriterules (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress1/rewriterules/datatypes3.smt2 b/test/regress/regress1/rewriterules/datatypes3.smt2 index 1ec5dcbc4..fb9d79121 100644 --- a/test/regress/regress1/rewriterules/datatypes3.smt2 +++ b/test/regress/regress1/rewriterules/datatypes3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; try to solve datatypes with rewriterules (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 b/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 index 6e22816d7..a8dc5227a 100644 --- a/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 +++ b/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules (set-logic AUFLIRA) ;; DATATYPE diff --git a/test/regress/regress1/rewriterules/datatypes_sat.smt2 b/test/regress/regress1/rewriterules/datatypes_sat.smt2 index 92576f976..428598c5b 100644 --- a/test/regress/regress1/rewriterules/datatypes_sat.smt2 +++ b/test/regress/regress1/rewriterules/datatypes_sat.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; try to solve datatypes with rewriterules (set-logic AUFLIA) (set-info :status sat) diff --git a/test/regress/regress1/rewriterules/length_gen.smt2 b/test/regress/regress1/rewriterules/length_gen.smt2 index dda478357..df876ef08 100644 --- a/test/regress/regress1/rewriterules/length_gen.smt2 +++ b/test/regress/regress1/rewriterules/length_gen.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_gen_010.smt2 b/test/regress/regress1/rewriterules/length_gen_010.smt2 index 052f5905b..aee09cc96 100644 --- a/test/regress/regress1/rewriterules/length_gen_010.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_010.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 index 02bc877fc..49e6f970d 100644 --- a/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_gen_020.smt2 b/test/regress/regress1/rewriterules/length_gen_020.smt2 index 8e0021175..b7c2e5fd2 100644 --- a/test/regress/regress1/rewriterules/length_gen_020.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_020.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 b/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 index cc75eb85a..70511d9b3 100644 --- a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_gen_040.smt2 b/test/regress/regress1/rewriterules/length_gen_040.smt2 index 687422223..93a04cb7c 100644 --- a/test/regress/regress1/rewriterules/length_gen_040.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_040.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 index 293ea147b..cabd84575 100644 --- a/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 b/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 index 69f9f97be..7530269e8 100644 --- a/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_gen_080.smt2 b/test/regress/regress1/rewriterules/length_gen_080.smt2 index 061042be3..451ea091e 100644 --- a/test/regress/regress1/rewriterules/length_gen_080.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_080.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 index 28b58183e..7a81652ea 100644 --- a/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_gen_inv_160.smt2 b/test/regress/regress1/rewriterules/length_gen_inv_160.smt2 index 9c2a5c307..af134287d 100644 --- a/test/regress/regress1/rewriterules/length_gen_inv_160.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_inv_160.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_trick3.smt2 b/test/regress/regress1/rewriterules/length_trick3.smt2 index f6899541b..fce35d691 100644 --- a/test/regress/regress1/rewriterules/length_trick3.smt2 +++ b/test/regress/regress1/rewriterules/length_trick3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/length_trick3_int.smt2 b/test/regress/regress1/rewriterules/length_trick3_int.smt2 index d58bf55fe..ec10ed6d3 100644 --- a/test/regress/regress1/rewriterules/length_trick3_int.smt2 +++ b/test/regress/regress1/rewriterules/length_trick3_int.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 index 13f7234e9..b73f1b2a4 100644 --- a/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 +++ b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress1/rewriterules/read5.smt2 b/test/regress/regress1/rewriterules/read5.smt2 index e66df7c7e..2cd6eb244 100644 --- a/test/regress/regress1/rewriterules/read5.smt2 +++ b/test/regress/regress1/rewriterules/read5.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules (set-logic AUF) (set-info :source | Translated from old SVC processor verification benchmarks. Contact Clark diff --git a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 index 9bd49f714..7434f4257 100644 --- a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 +++ b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 index 4d65ffac5..256c9bb11 100644 --- a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 +++ b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba (set-logic AUFLIA) (set-info :status sat) diff --git a/test/regress/regress1/rewriterules/test_guards.smt2 b/test/regress/regress1/rewriterules/test_guards.smt2 index 98c845fb5..7344dfba5 100644 --- a/test/regress/regress1/rewriterules/test_guards.smt2 +++ b/test/regress/regress1/rewriterules/test_guards.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 b/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 index 4d39e12bb..5646cd70b 100644 --- a/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 +++ b/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;;; From a verification condition generated by why3. The original program ;; can be found at http://toccata.lri.fr/gallery/vstte10_max_sum.en.html . ;; The problem has been modified by doubling the size of the arrays diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index 144a2225c..34a26aae7 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -48,7 +48,9 @@ TESTS = \ bug812.smt2 \ bug765.smt2 \ simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 \ - bug674.smt2 + bug674.smt2 \ + javafe.ast.WhileStmt.447_no_forall.smt2 \ + javafe.ast.StandardPrettyPrint.319_no_forall.smt2 EXTRA_DIST = $(TESTS) \ FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \ diff --git a/test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 b/test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 index 4d47186df..9a737a3d1 100644 --- a/test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 +++ b/test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 @@ -2,7 +2,7 @@ (set-info :source | Simplify Theorem Prover Benchmark Suite |) (set-info :smt-lib-version 2.0) (set-info :category "industrial") -(set-info :status unsat) +(set-info :status sat) (declare-fun true_term () Int) (declare-fun false_term () Int) (assert (= true_term 1)) diff --git a/test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2 b/test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2 index 534e8f404..ff7c09997 100644 --- a/test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2 +++ b/test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2 @@ -2,7 +2,7 @@ (set-info :source | Simplify Theorem Prover Benchmark Suite |) (set-info :smt-lib-version 2.0) (set-info :category "industrial") -(set-info :status unsat) +(set-info :status sat) (declare-fun true_term () Int) (declare-fun false_term () Int) (assert (= true_term 1)) diff --git a/test/regress/run_regression b/test/regress/run_regression index 6b2447d8e..4ae013911 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -146,9 +146,6 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'` - if [ -z "$expected_exit_status" ]; then - expected_exit_status=0 - fi elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\|ERROR-SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then scrubber=`grep '^; SCRUBBER: ' "$benchmark" | sed 's,^; SCRUBBER: ,,'` errscrubber=`grep '^; ERROR-SCRUBBER: ' "$benchmark" | sed 's,^; ERROR-SCRUBBER: ,,'` @@ -156,19 +153,28 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'` command_line=`grep '^; COMMAND-LINE: ' "$benchmark" | sed 's,^; COMMAND-LINE: ,,'` - if [ -z "$expected_exit_status" ]; then - expected_exit_status=0 + fi + + # If expected output/error was not given, try to determine the status from + # the commands. + if [ -z "$expected_output" -a -z "$expected_error" ]; then + if grep '^ *( *set-info *:status *sat' "$benchmark" &>/dev/null; then + expected_output=sat + elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then + expected_output=unsat fi - elif grep '^ *( *set-info *:status *sat' "$benchmark" &>/dev/null; then - expected_output=sat - expected_exit_status=0 - command_line= - elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then - expected_output=unsat + fi + + # A valid test case needs at least an expected output (explicit or through + # SMT2 commands) or an expected exit status. + if [ -z "$expected_output" -a -z "$expected_error" -a -z "$expected_exit_status" ]; then + error "cannot determine status of \`$benchmark'" + fi + + # If no explicit expected exit status was given, we assume that the solver is + # supposed to succeed. + if [ -z "$expected_exit_status" ]; then expected_exit_status=0 - command_line= - else - error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then lang=cvc4 |