diff options
Diffstat (limited to 'test/regress/regress0/rewriterules')
12 files changed, 11 insertions, 3 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) |