Fix rewrite rules sat regressions (#3734)

Quantifier rewrite rules are not robust to preprocessing within our check-model infrastructure. This disables check-model on 2 satisfiable rewrite rules regressions. Fixes nightlies.

diff --git a/test/regress/regress1/rewriterules/datatypes_sat.smt2 b/test/regress/regress1/rewriterules/datatypes_sat.smt2
index ab32e41904bbd9960ab82b275d7f52f4b75cf2eb..4b5b5943523371a1511afd0a8c78b880eec7cf61 100644 (file)
--- a/test/regress/regress1/rewriterules/datatypes_sat.smt2
+++ b/test/regress/regress1/rewriterules/datatypes_sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --rewrite-rules --quiet
+; COMMAND-LINE: --rewrite-rules --no-check-models
 ;; try to solve datatypes with rewriterules
 (set-logic AUFLIA)
 (set-info :status sat)

diff --git a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 b/test/regress/regress1/rewriterules/length_gen_020_sat.smt2
index d46065c73e8e9ff15a5523b1d8f53f25b4236d8b..72db8d18b3f877d50a6b3fff25ce9a94493c40bc 100644 (file)
--- a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2
+++ b/test/regress/regress1/rewriterules/length_gen_020_sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --rewrite-rules --quiet
+; COMMAND-LINE: --rewrite-rules --no-check-models
 ;; Same than length.smt2 but the nil case is not a rewrite rule
 ;; So here the rewrite rules have no guards length