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.

diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am
index 5df254badbff8b5564c600418f0f1d632ff9b5f3..179398c9d6303a0a1368212148ff9d794ef88c1c 100644 (file)
--- 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 a914a0c1fff76b59a7fbf88df10c0f719958598d..9a5f68100ca8b85b9dc61e49660afe5225ad66e6 100644 (file)
--- 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 19163f49d913c255769e6d31543dcc21eff8c82d..cc217fc7938f25dea220bdbb4dfba0d315fb9d46 100644 (file)
--- 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 215698ade91a5fe73757478c8b94a5f2f822adc1..b144d7745083bfddcaac790b2983a291be216f58 100644 (file)
--- 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 5d1255eb0ba8f698f062b012adf11dc0817cc554..7da2f677788014466542677d35dbf3f8efe7e2b9 100644 (file)
--- 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 b1462cf98b9433afb7512ec0b3c376f935180fd9..7d65356adf2922302e1ba2d4d83e12554eedceac 100644 (file)
--- 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 84afc58153e6b29c469204d3d6a649d15cf299ac..e01e97b84bd030b04a1da8ae5a706f76fff9ff83 100644 (file)
--- 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 af9e7f07d164c7bb736c5f62e334ab969c9fba25..8d47d95506eaf6740b6d6ccfe8943754f79fb7e2 100644 (file)
--- 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 b7d19b612017beb07bb15d08996e5af9be27b92f..83de7d8f4fa65873d0d3fd0919fb549192a475b1 100644 (file)
--- 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 c3c4aad73da3b36c7a83477bccd496e5972c0aac..365ec06249c5e24d398d1f983cc214deba48bdf6 100644 (file)
--- 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 e8c0139e82506d815d07b66333b1023e9d79464e..6b55a967719de72cc3a274c3b6f2cabed0036c2b 100644 (file)
--- 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 838c0cd16624cb49b3945acc333ff73f35a1abf5..f67a0e6a2478f230ad7b1ede3dee92b3298764a7 100644 (file)
--- 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 dd8621618d0348e84a9da3fab1c32d6f6dcb81a6..65f96f4694f3fdb78010f51908a682ad50e91b50 100644 (file)
--- 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 e6f82727ed398add52601235309497a6d30132a3..bdc49e7ce29c9da60b2137123e7a118311ecd4a6 100644 (file)
--- 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 0d0c7cdb23e71e0f9a524aef235ff905faebc92b..7a8577677910bd5ae5af919fb0a612a0a1a22e1a 100644 (file)
--- 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 dc2b274140c524b6b0486329a711ed3420cb4739..3dfab3b0ebca419c5e69c7424277c4d99d0b670b 100644 (file)
--- 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 f9e829e45a8a1b60f6376ef6f06f96be01ae2ac5..d6206287a5f034560c8108285fe2434777b44c94 100644 (file)
--- 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 83634a50aa65a6aa6befcf7f350a0515018ed01f..fd24c3f654bd8905e4198276b243eb9b05629d68 100644 (file)
--- 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 2b06d5ea8a060688b5860240b1e2047bfb58de68..507a18a783e98ee19c8703dbde7df9ce14d445f4 100644 (file)
--- 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 de1e305bc428defc139f82239b79976b43ef9423..5e54083a5b14997bef56b12b7a56380e5ab9d8e8 100644 (file)
--- 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 05653415f1c5d67b42eb2ca189bc7ac939d0eb66..ce36302640cabf2e057440dda9a446ccbe043e1e 100644 (file)
--- 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 6cc063ca46b4bb90b5d2b8d97150da3959dfb85b..105320632e2a1fac84855d2708972fa8812328fb 100644 (file)
--- 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 82f084e87c6c1c4f4eac83c1f168c6a54ef78df4..f1acfa7598a10dc703dc43e004f8cd1f29fdb7e0 100644 (file)
--- 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 0dded2a2ffaf807d3276131b744fe8eead775f11..b1943124e5a31d91a521bb039e049893aaf6f676 100644 (file)
--- 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 94909622414098f1c23262ce687a6ccf8eaed03f..49b7d5fc8d54b225f4527a497b9ec9d6bde5d910 100644 (file)
--- 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 a689804f767e5c7e9f845bba8d44c6d61b22eda9..f24b129e04efb776b9eaace52fab18e86e86ba76 100644 (file)
--- 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 ba7316324d07fdcfbe25b00e0504671c84c0aad1..ae50d350cc4debf4121c65bbbfa3c01ac714f6b2 100644 (file)
--- 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 e2941b34adc7faaa0feb91e86ad9fd852ab878c6..6f4e38ec7e75f7e79188936f0d0b8dac595dbe01 100644 (file)
--- 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 aa901b9b09f54526c72d8951907440ee0273c7f6..789e4c6c8db67096fbe32d26bb9963d08e52108b 100644 (file)
--- 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 d3cadf6c8a91eb8ca19fec267e9a9159de4f3860..990a8d45712a6083e85b8f24c5520bcc50503d7c 100644 (file)
--- 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 56289e2456f6c4a20a6a9a1824f61e6e12392dc5..b31efe3aa57e39cbfa1de613072c640aba7382c8 100644 (file)
--- 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 9e1ecc193bdaced0167f62581f310e8f5b620cc3..3cac4670be021b60081b37ae93ecbae66be3f6f3 100644 (file)
--- 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 fc56695f59617ce1126e0ac4e9ba9c6d66e749e4..a109d9471db056972c2c2d6013739e0adcd9fcdf 100644 (file)
--- 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 89e4ff5695a8337fbf7713d7d6adcc020a67dd7b..4e413c24f88ed9374a2e4fa889cbd78eb58f2a55 100644 (file)
--- 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 ea67a1b5a3516782fdc223288936220ccf5884c7..71cf37371b06da4f386c63eeab94ae5c8f513e68 100644 (file)
--- 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 22fc7e7d2c77ce20bfd008c01fb79581f544bd42..4f62d2a0d794281776afcde05d87f21fd90bca76 100644 (file)
--- 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 702f9d7a017c6c13e5ff4bfb86d6f5e3282048bb..391a6c9d77265e9e2056a5e26fa87c7970afbcd0 100644 (file)
--- 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 b797fa4e8ac71ab0e0f428cda3cba00bba3a3f4b..f23b119fe0a22ef2137bb0c6014c79d7443848ae 100644 (file)
--- 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 4d897830cd0733e959e8663aad64c0a2cae58734..2887cdca8380bc649ae3bb4c90c24d42aaaa12ff 100644 (file)
--- 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 8927a5f2eb67834db69ad74cc7ca78def2b923c7..289104ec8cd1de5e1b68a06fd9d3978d76a9b9a8 100644 (file)
--- 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 1aceacbe3aea482b690bc6562898ce50cdf072cb..cbe15db5815b4924d4c5c4668f403d3821e01202 100644 (file)
--- 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 f98375653d6e11e38608aeeb3d17db07d23959b4..2e20460c54244c834a966cc86ea48828c786f2d9 100644 (file)
--- 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 e56500ad249309d13e1d91475a0cfb3bd16b7604..743cfbebe309b98075c2555df9da773a5c8657e8 100644 (file)
--- 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 a4af152f107bfbb28207acc0142cad9a2a95e000..db1f3dcd9ba34e3e55cea5e2e3157a27123c9462 100644 (file)
--- 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 d702b6d1ac555906edae2688ea65778b431fd60d..9c696d48b1fec205d27a0d9f2cf136002d8911de 100644 (file)
--- 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 f4b6a7a630ee19b8f8a2d9daebc27624e28c970a..c5696f0a2ab138db84e1e25c95441641a87463bd 100644 (file)
--- 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 cbbb4cc6e968b28d07b26d7824aa3ce7bebaca12..d0678d87cbb5244cb11b2dd341d661240527d7d8 100644 (file)
--- 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 0e6f5916bcc805bccf553d700fbf97d8ee8dcae0..5dfa6c1b1b315d2741f45133dd747fb2be8d7386 100644 (file)
--- 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 11e3a98776af04c84e6bbe332ee4d5d389a2e0e8..e9892e5981f3033111e0cd913ad1380c92b904ea 100644 (file)
--- 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 b8d978b7170bc5922ff111fb7cdf0978550db77d..0fccae301e1624eae1f5433a511443acd1d84795 100644 (file)
--- 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 cd927d0c6835506a8f9fd9d5f1f5e058781b0317..4d4e0e95f5f67992ec0e9d9d25c35801feccae43 100644 (file)
--- 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 fb94994b40e3dc361ce4e0fea5d9ffbff7b95a68..9429237a4ac19df09e74d995e62627a4c30b92f5 100644 (file)
--- 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 3fb4a0d23bc3082af1ded39a13fc160fa49a23b6..c86699b480e99de2f292b87f7914cc25d3a020df 100644 (file)
--- 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 b11ab9da3da32fd50c79aef2454f8724143023a7..ceb19ea75012f03b26682a44011ff28793f51202 100644 (file)
--- 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 8170ec28093288ceeb03dc0bd91cc91f3d8af6c7..04008c006824b920abdfec7d4c27c6876b05002c 100644 (file)
--- 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 545bcbf64e9e62b13f50fc42110a126bfdd7df45..53f76f0d3315d5a3c799f9fb263a50101d2913a2 100644 (file)
--- 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 818bb55b37c09424e5652125f6daf389dda4a9ce..d3bcc506f84f9548c080f581f38d545fb93b020e 100644 (file)
--- 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 76b119e42290f8012f18d0ef96bdd4951eab5b3e..d4d6d4a5d6deb51b52779919ba620e3601be434b 100644 (file)
--- 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 4dc1cc2950320af2b8dffe97e11516c181c9070c..54f092b8c6d3c31402863bdd8e002eef91fb7638 100644 (file)
--- 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 6c03fc254c85ece3b7b4926633e2b0262300d704..4eea4df9caac60f8f0c564e76a1e62359bc30942 100644 (file)
--- 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 637a6407f63f57a426c65263046f0723cc6b4fa3..a0a42f4ef7cee8f5727390b0a68d8cb04689e616 100644 (file)
--- 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 fdad322af001511425460aca680dbf592a2cbf49..4a29d9a92436001666acffc75cef6e96ab183c60 100644 (file)
--- 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 0b2a95f4907f9c7387bfc8a00cdb27f7058f1599..3e28c2f8bf48b6b38a62a6ee3c7fd0f26470e4ba 100644 (file)
--- 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 4089bb5dc4e28754d64f281d5cd36d54a2c73f51..fcc66b015267cd83637989d62db6dc1243f3919c 100644 (file)
--- 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 159f2e088b470da73ef7349d225038d61ed901e1..af277af90b1d00402b865d384021d9b0a4b80c89 100644 (file)
--- 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 d3e51d996bca20a0a5df87ce90fc6702f55962aa..bd208c6d39061bfa0bc26272c62912b71281bfc2 100644 (file)
--- 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 fbf3db47a167fd119b00bb0d0c3fbf1c5232727d..6c5ce19fbc3e1f928cecb17273d80136536b321c 100644 (file)
--- 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 277ddc3ae0d0eb47ee574d2ac1d870610d6faee2..4ef40597a0c031c43e9b1fd7db46b6af528e0115 100644 (file)
--- 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 1ec5dcbc4f5c0e333d2f18b529c117fc68768ddd..fb9d79121f03dc28f7bf9254c7138d623114a985 100644 (file)
--- 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 6e22816d71736bdedcdb5f778c3b07a8782db088..a8dc5227a6d031bb2f6ab9de2b77fce03cdca0a2 100644 (file)
--- 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 92576f976fa264c4c94107e5ede5ecb5769139d3..428598c5b5892b185ff9f0851d9c203e50f323da 100644 (file)
--- 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 dda478357cf69abc22c5236f4691f536b2259149..df876ef0826961090cad818f484565e8fca759e8 100644 (file)
--- 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 052f5905bf6ace8f627f5f765c41e7ce9037f48f..aee09cc964f7cf0720261c9d28bdf92802521bc1 100644 (file)
--- 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 02bc877fc8e42ed2ec45c330a4a7f17160b4933e..49e6f970d01f65eb50a1cf33be5d607770817889 100644 (file)
--- 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 8e00211755426cc400e6cb7f43e43ce2c5adb14d..b7c2e5fd2c9d1106b0b8b64a4a810f15e40c0cff 100644 (file)
--- 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 cc75eb85a966e46beda4dbfa4b9f1db6922fb6aa..70511d9b302cd1fe29be40ab61ad90af20fd7c8e 100644 (file)
--- 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 687422223eb54f91469ff577bf51c19821c2ad94..93a04cb7cd6cd1e907b98a9bc3dd3db10d8c5bce 100644 (file)
--- 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 293ea147b460bfdb3c94a0beff90f5ae1a0cc3af..cabd8457557aeb110575bf04fcdb70ce10037e0e 100644 (file)
--- 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 69f9f97be98fc8d6d087bed001a7a362e89d2bd7..7530269e8c0360e85c6a78bae277e30b278b6e48 100644 (file)
--- 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 061042be35a8e3d32ccdacd62b4fd0423cc78e60..451ea091eb18e00b2c8b57f8d520ce70f776ae91 100644 (file)
--- 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 28b58183efb15db0ec52041f9f13324c128f6f36..7a81652ea7a391f61d9b78d416b802949de89ba2 100644 (file)
--- 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 9c2a5c307a1e529bbf9de30804a8e92f81403ceb..af134287db55d4408f2d1200490abd8b42605629 100644 (file)
--- 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 f6899541b93bc88beea9e2deb52ee478d7b1d63c..fce35d69140817293f6605bba1809c99b67184b5 100644 (file)
--- 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 d58bf55fe7d1fd48d92602faeb79eb4a6b804926..ec10ed6d308ff8b0164e07646485b0995e5e3e1e 100644 (file)
--- 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 13f7234e965a36c3438b9cbe620bdf531cff09c5..b73f1b2a411a23d7209355ce4125863f18631804 100644 (file)
--- 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 e66df7c7e40a33ca13cd486b275835454b1d6371..2cd6eb2447a1fca454488c151e7231794de127f6 100644 (file)
--- 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 9bd49f71463c607ac22cfcc67227172cca640995..7434f42573305a8725eb222763c9c725b1cfc055 100644 (file)
--- 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 4d65ffac5b3fddbaf594514fa186beb1a7e46815..256c9bb11ce4265a25cd8d6da88be6b13dd05976 100644 (file)
--- 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 98c845fb571b50814cbaec5796663a9be45632d6..7344dfba5f90f6303bcd92c45af9f4d647112a56 100644 (file)
--- 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 4d39e12bb509badfe6012b3207d4c74cc82720a7..5646cd70b4d135946d25cb0cae4633e6b4b88d4f 100644 (file)
--- 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 144a2225c174116ad6f0d581020c01c76f262470..34a26aae7ebad9d62eba26fd012d4ce99c32324f 100644 (file)
--- 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 4d47186df6d720903d52e6804d3f77485f2ec29c..9a737a3d1fc77a9eeb7c3e3294eb3f7c90ef5f1f 100644 (file)
--- 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 534e8f40496b0f9259ae105e98f7486212139b22..ff7c099970042faa5b4533c113538aa19f00a95d 100644 (file)
--- 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 6b2447d8e2aa4d5d2b069137ed175be14672aebe..4ae0139118f218a240769fac56aa679b6ae95359 100755 (executable)
--- 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