From 427d38c14eb23026e6866ad4b2663e3d6e82399e Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Mon, 18 Apr 2022 17:21:22 -0500 Subject: [PATCH] Remove instances of `check-proofs` in regressions. (#8630) This PR removes usages of check-proofs option according to the following rules: unsat and no-check-proofs --> DISABLE-TESTER: proof unsat and check-proofs --> remove option sat and no-check-proofs --> remove option sat and check-proofs --> change to produce-proofs no-produce-proofs --> DISABLE-TESTER: proof --- .../regress0/arith/issue5219-conflict-rewrite.smt2 | 2 +- .../preprocess/proj-issue304-circuit-prop-xor.smt2 | 2 +- .../proj-issue305-circuit-prop-ite-a.smt2 | 2 +- .../proj-issue305-circuit-prop-ite-b.smt2 | 2 +- .../proj-issue305-circuit-prop-ite-c.smt2 | 2 +- .../proj-issue305-circuit-prop-ite-d.smt2 | 2 +- .../preprocess/proj-issue309-circuit-prop-ite.smt2 | 2 +- .../preprocess/proj-issue332-circuit-prop-xor.smt2 | 2 +- .../proofs/proj-issue326-nl-bounds-check.smt2 | 2 +- .../proj-issue430-coverings-double-negation.smt2 | 1 - .../regress0/proofs/project-issue330-eqproof.smt2 | 2 +- .../regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 | 2 +- .../regress1/datatypes/dt-param-card4-unsat.smt2 | 2 +- test/regress/cli/regress1/hole6.cvc.smt2 | 2 +- test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 | 3 ++- test/regress/cli/regress1/nl/factor_agg_s.smt2 | 2 +- test/regress/cli/regress1/sets/sets-disequal.smt2 | 3 ++- .../regress/cli/regress1/strings/proj-issue331.smt2 | 1 - test/regress/cli/regress2/instance_1444.smtv1.smt2 | 2 +- test/regress/cli/run_regression.py | 13 ++----------- 20 files changed, 21 insertions(+), 30 deletions(-) diff --git a/test/regress/cli/regress0/arith/issue5219-conflict-rewrite.smt2 b/test/regress/cli/regress0/arith/issue5219-conflict-rewrite.smt2 index b49287c30..c7ec1c1b8 100644 --- a/test/regress/cli/regress0/arith/issue5219-conflict-rewrite.smt2 +++ b/test/regress/cli/regress0/arith/issue5219-conflict-rewrite.smt2 @@ -2,7 +2,7 @@ ; COMMAND-LINE: --theoryof-mode=term --nl-icp ; EXPECT: sat (set-logic QF_NRA) -(set-option :check-proofs true) +(set-option :produce-proofs true) (declare-fun x () Real) (declare-fun y () Real) (assert (and (< 1 y) (= y (+ x (* x x))))) diff --git a/test/regress/cli/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 b/test/regress/cli/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 index 9e4bd285c..a694ecd34 100644 --- a/test/regress/cli/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 +++ b/test/regress/cli/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat (set-logic ALL) -(set-option :check-proofs true) +(set-option :produce-proofs true) (declare-const a Bool) (declare-const b Bool) (assert b) diff --git a/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 b/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 index 6760bdf4d..926411f61 100644 --- a/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 +++ b/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat (set-logic ALL) -(set-option :check-proofs true) +(set-option :produce-proofs true) (declare-const x Bool) (declare-const y Bool) (declare-const z Bool) diff --git a/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 b/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 index fcb26054e..1cb707bff 100644 --- a/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 +++ b/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat (set-logic ALL) -(set-option :check-proofs true) +(set-option :produce-proofs true) (declare-fun a () Bool) (declare-fun b () Bool) (declare-fun c () Bool) diff --git a/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 b/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 index 1765c32f1..20dbf3c2a 100644 --- a/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 +++ b/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat (set-logic ALL) -(set-option :check-proofs true) +(set-option :produce-proofs true) (declare-fun a () Bool) (declare-fun b () Bool) (declare-fun c () Bool) diff --git a/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 b/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 index b3b19f74b..6ed928bd7 100644 --- a/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 +++ b/test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat (set-logic ALL) -(set-option :check-proofs true) +(set-option :produce-proofs true) (declare-fun a () Bool) (declare-fun b () Bool) (declare-fun c () Bool) diff --git a/test/regress/cli/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 b/test/regress/cli/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 index 09626896d..8bf602657 100644 --- a/test/regress/cli/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 +++ b/test/regress/cli/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat (set-logic ALL) -(set-option :check-proofs true) +(set-option :produce-proofs true) (declare-fun a () Bool) (declare-fun c () Bool) (declare-fun d () Bool) diff --git a/test/regress/cli/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 b/test/regress/cli/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 index 841e7392b..614a41327 100644 --- a/test/regress/cli/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 +++ b/test/regress/cli/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat (set-logic ALL) -(set-option :check-proofs true) +(set-option :produce-proofs true) (declare-const x Real) (declare-const x4 Real) (declare-const x8 Bool) diff --git a/test/regress/cli/regress0/proofs/proj-issue326-nl-bounds-check.smt2 b/test/regress/cli/regress0/proofs/proj-issue326-nl-bounds-check.smt2 index 9b7074307..0f3a1d302 100644 --- a/test/regress/cli/regress0/proofs/proj-issue326-nl-bounds-check.smt2 +++ b/test/regress/cli/regress0/proofs/proj-issue326-nl-bounds-check.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: -q ; EXPECT: sat (set-logic ALL) -(set-option :check-proofs true) +(set-option :produce-proofs true) (set-option :proof-check eager) (declare-const x Real) (assert diff --git a/test/regress/cli/regress0/proofs/proj-issue430-coverings-double-negation.smt2 b/test/regress/cli/regress0/proofs/proj-issue430-coverings-double-negation.smt2 index cffdbc047..62ce4d846 100644 --- a/test/regress/cli/regress0/proofs/proj-issue430-coverings-double-negation.smt2 +++ b/test/regress/cli/regress0/proofs/proj-issue430-coverings-double-negation.smt2 @@ -1,5 +1,4 @@ ; REQUIRES: poly -; COMMAND-LINE: --check-proofs ; EXPECT: unsat ; EXPECT: unsat (set-logic QF_NRA) diff --git a/test/regress/cli/regress0/proofs/project-issue330-eqproof.smt2 b/test/regress/cli/regress0/proofs/project-issue330-eqproof.smt2 index 1da778205..1696f104b 100644 --- a/test/regress/cli/regress0/proofs/project-issue330-eqproof.smt2 +++ b/test/regress/cli/regress0/proofs/project-issue330-eqproof.smt2 @@ -2,6 +2,6 @@ (set-logic QF_SLIA) (declare-const x String) (declare-const x1 Int) -(set-option :check-proofs true) +(set-option :produce-proofs true) (declare-const _x String) (check-sat-assuming ((>= 0 (ite (= x (str.++ (str.from_code 0) (str.replace_all x (str.from_code 0) (str.++ (str.from_code 0) (str.from_code 0))) _x) (ite false x (str.++ _x _x _x)) x) x1 0)))) \ No newline at end of file diff --git a/test/regress/cli/regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 b/test/regress/cli/regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 index dfd30e1fd..a3a264614 100644 --- a/test/regress/cli/regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 +++ b/test/regress/cli/regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --check-proofs --proof-check=eager +; COMMAND-LINE: --proof-check=eager ; EXPECT: unsat (set-logic ALL) (declare-const x Bool) diff --git a/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 b/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 index 1e43e3cdc..84dadda4b 100644 --- a/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 +++ b/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; DISABLE-TESTER: proof ; EXPECT: unsat (set-logic QF_ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress1/hole6.cvc.smt2 b/test/regress/cli/regress1/hole6.cvc.smt2 index 80dc40617..2eecb91cc 100644 --- a/test/regress/cli/regress1/hole6.cvc.smt2 +++ b/test/regress/cli/regress1/hole6.cvc.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; DISABLE-TESTER: proof ; EXPECT: unsat (set-logic ALL) (set-option :incremental false) diff --git a/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 b/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 index 774dbffcb..adbc5c216 100644 --- a/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 +++ b/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 @@ -1,5 +1,6 @@ +; DISABLE-TESTER: proof ; REQUIRES: poly -; COMMAND-LINE: --nl-ext-tplanes --no-check-proofs +; COMMAND-LINE: --nl-ext-tplanes ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/cli/regress1/nl/factor_agg_s.smt2 b/test/regress/cli/regress1/nl/factor_agg_s.smt2 index fc2e7a789..bfd574634 100644 --- a/test/regress/cli/regress1/nl/factor_agg_s.smt2 +++ b/test/regress/cli/regress1/nl/factor_agg_s.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) -(set-option :check-proofs true) +(set-option :produce-proofs true) (set-option :proof-check eager) (declare-fun skoX () Real) (declare-fun skoY () Real) diff --git a/test/regress/cli/regress1/sets/sets-disequal.smt2 b/test/regress/cli/regress1/sets/sets-disequal.smt2 index 22cdde8e4..4b4785fb6 100644 --- a/test/regress/cli/regress1/sets/sets-disequal.smt2 +++ b/test/regress/cli/regress1/sets/sets-disequal.smt2 @@ -1,4 +1,5 @@ -; COMMAND-LINE: --incremental --no-check-proofs +; DISABLE-TESTER: proof +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: sat ; EXPECT: unsat diff --git a/test/regress/cli/regress1/strings/proj-issue331.smt2 b/test/regress/cli/regress1/strings/proj-issue331.smt2 index e993419f1..49ceea42b 100644 --- a/test/regress/cli/regress1/strings/proj-issue331.smt2 +++ b/test/regress/cli/regress1/strings/proj-issue331.smt2 @@ -1,7 +1,6 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat (set-logic ALL) -(set-option :check-proofs true) (set-info :status unsat) (declare-const x Int) (check-sat-assuming ((str.< (str.++ (str.from_int x) (str.replace_re (str.from_int x) re.none (str.from_int 0)) (str.replace_re (str.from_int x) re.none (str.from_int 0))) (str.from_int x)))) diff --git a/test/regress/cli/regress2/instance_1444.smtv1.smt2 b/test/regress/cli/regress2/instance_1444.smtv1.smt2 index 47d3fda52..3b25eb264 100644 --- a/test/regress/cli/regress2/instance_1444.smtv1.smt2 +++ b/test/regress/cli/regress2/instance_1444.smtv1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-produce-proofs +; DISABLE-TESTER: proof (set-option :incremental false) (set-info :status unsat) (set-logic QF_UF) diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py index c4c87fecd..af46438ec 100755 --- a/test/regress/cli/run_regression.py +++ b/test/regress/cli/run_regression.py @@ -134,10 +134,7 @@ class UnsatCoreTester(Tester): def applies(self, benchmark_info): return ( benchmark_info.benchmark_ext != ".sy" - and ( - "unsat" in benchmark_info.expected_output.split() - or "entailed" in benchmark_info.expected_output.split() - ) + and "unsat" in benchmark_info.expected_output.split() and "--no-produce-unsat-cores" not in benchmark_info.command_line_args and "--no-check-unsat-cores" not in benchmark_info.command_line_args and "--check-unsat-cores" not in benchmark_info.command_line_args @@ -162,13 +159,7 @@ class ProofTester(Tester): expected_output_lines = benchmark_info.expected_output.split() return ( benchmark_info.benchmark_ext != ".sy" - and ( - "unsat" in benchmark_info.expected_output.split() - or "entailed" in benchmark_info.expected_output.split() - ) - and "--no-produce-proofs" not in benchmark_info.command_line_args - and "--no-check-proofs" not in benchmark_info.command_line_args - and "--check-proofs" not in benchmark_info.command_line_args + and "unsat" in benchmark_info.expected_output.split() ) def run(self, benchmark_info): -- 2.30.2