From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 16 Mar 2021 13:16:31 +0000 (-0300)
Subject: [proof-new] Disabling proofs on regressions with known bug (#6151)
X-Git-Tag: cvc5-1.0.0~2071
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5a879f4315d0105f8487c8718659a4f060ea634e;p=cvc5.git

[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 4216f429a..79c95b4ab 100644
--- 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 bf2d2a8c3..ad132adcf 100644
--- 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 81fe3b046..c76a3dfd7 100644
--- 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 1901016c2..f645bae0f 100644
--- 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 96aaf9f51..5afabc868 100644
--- 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 ba5d012a0..86d2d7b4e 100644
--- 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 6bb992a5e..05f7ed213 100644
--- 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 51a6898b4..66984c742 100644
--- 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)