From: Haniel Barbosa 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)