diff options
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 |