[proof-new] Disabling proofs on regressions with known bug (#6151)

This is so that we can use CI in master for proofs.

diff --git a/test/regress/regress1/push-pop/arith_lra_01.smt2 b/test/regress/regress1/push-pop/arith_lra_01.smt2
index 4216f429a1b51394ee2c9b72c639391cf7e68c78..79c95b4ab26487ba288473f988ea95465895996e 100644 (file)
--- a/test/regress/regress1/push-pop/arith_lra_01.smt2
+++ b/test/regress/regress1/push-pop/arith_lra_01.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --no-proof
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat
@@ -102,4 +102,3 @@
 (assert (or (not (> (+ (* (- 26) x1 ) (* 26 x0 ) ) 48)) (>= (+ (* 35 x3 ) (* (- 43) x2 ) (* 29 x0 ) (* (- 31) x2 ) (* (- 20) x2 ) (* 22 x1 ) ) 49) (>= (+ (* (- 31) x2 ) (* (- 2) x1 ) (* (- 45) x2 ) (* 25 x2 ) (* 29 x4 ) (* (- 23) x1 ) (* (- 1) x0 ) (* 18 x1 ) (* 0 x2 ) (* (- 43) x2 ) (* 24 x2 ) ) (- 23)) ))
 (assert (or (<= (+ (* 5 x0 ) (* (- 8) x0 ) (* 18 x4 ) (* (- 12) x3 ) (* (- 18) x3 ) (* (- 48) x3 ) (* (- 34) x1 ) (* (- 2) x1 ) (* (- 50) x3 ) (* (- 45) x3 ) ) (- 48)) (>= (+ (* 41 x0 ) (* 25 x2 ) (* (- 17) x2 ) (* (- 6) x0 ) (* (- 48) x3 ) (* (- 36) x3 ) (* 31 x0 ) (* (- 7) x3 ) ) 15) ))
 (check-sat)
-

diff --git a/test/regress/regress1/push-pop/fuzz_3_1.smt2 b/test/regress/regress1/push-pop/fuzz_3_1.smt2
index bf2d2a8c312413f8cb107f0a468a3c898a697da2..ad132adcfd2d70e0e7236437e4efb2e8582d3eb2 100644 (file)
--- a/test/regress/regress1/push-pop/fuzz_3_1.smt2
+++ b/test/regress/regress1/push-pop/fuzz_3_1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --no-proof
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: unsat

diff --git a/test/regress/regress1/push-pop/fuzz_3_11.smt2 b/test/regress/regress1/push-pop/fuzz_3_11.smt2
index 81fe3b046d6ff0fe6f0d1b092afc6d96d73b251b..c76a3dfd7e15e4a9ed49d170cfdf53d127894295 100644 (file)
--- a/test/regress/regress1/push-pop/fuzz_3_11.smt2
+++ b/test/regress/regress1/push-pop/fuzz_3_11.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --no-proof
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat

diff --git a/test/regress/regress1/push-pop/fuzz_3_6.smt2 b/test/regress/regress1/push-pop/fuzz_3_6.smt2
index 1901016c2f4b557938fc04f9e26cb6e0764663c7..f645bae0fbd8c008722302784d64325950ac4c1c 100644 (file)
--- a/test/regress/regress1/push-pop/fuzz_3_6.smt2
+++ b/test/regress/regress1/push-pop/fuzz_3_6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --no-proof
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: unsat

diff --git a/test/regress/regress1/push-pop/fuzz_3_9.smt2 b/test/regress/regress1/push-pop/fuzz_3_9.smt2
index 96aaf9f514e7b0ad6e10d96e220cac7dc0b3a575..5afabc868cb70efb77787c1c42fbfc73f2d8c9c6 100644 (file)
--- a/test/regress/regress1/push-pop/fuzz_3_9.smt2
+++ b/test/regress/regress1/push-pop/fuzz_3_9.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --no-proof
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat

diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
index ba5d012a01a66a1b6cb606a5f74c7aee003c58e9..86d2d7b4e76172e77be231e3ca885e097b9ebee9 100644 (file)
--- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
+++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores
+; COMMAND-LINE: --no-check-unsat-cores --no-proof
 (set-logic AUFLIRA)
 (set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods.
 

diff --git a/test/regress/regress1/strings/stoi-400million.smt2 b/test/regress/regress1/strings/stoi-400million.smt2
index 6bb992a5e85c9a8364c1f7fb3dbb53df38c2aeb9..05f7ed213728e7105298fc2b1bd06d00d46c3419 100644 (file)
--- a/test/regress/regress1/strings/stoi-400million.smt2
+++ b/test/regress/regress1/strings/stoi-400million.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp
+; COMMAND-LINE: --strings-exp --no-proof
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic ALL)

diff --git a/test/regress/regress2/instance_1444.smtv1.smt2 b/test/regress/regress2/instance_1444.smtv1.smt2
index 51a6898b439d3604c1efd81216100b079bcf123b..66984c7428e32a735e28f13abc6cbc3630a97729 100644 (file)
--- a/test/regress/regress2/instance_1444.smtv1.smt2
+++ b/test/regress/regress2/instance_1444.smtv1.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-proof
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_UF)