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

diff --git a/test/regress/cli/regress0/arith/issue5219-conflict-rewrite.smt2 b/test/regress/cli/regress0/arith/issue5219-conflict-rewrite.smt2
index b49287c30f21a8080f8a82393071a64e5031cdb1..c7ec1c1b8d333678fe37244048c89df2165815b4 100644 (file)
--- 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 9e4bd285ca55b7747df752478a00d08d589d9ceb..a694ecd3407de0911e38611ebb2f9d00eb38ac19 100644 (file)
--- 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 6760bdf4d2e7ca395fb6f0c06e5d26cde18beeb0..926411f61f0c70f9ae86c4faaf2425976c88195b 100644 (file)
--- 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 fcb26054e7bda79c7f3ab122eb8b00e5514ff63b..1cb707bff55f72f8d00c1ffad4f3944a6ebf53eb 100644 (file)
--- 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 1765c32f169c4f92264467d47b5d40f278d469cf..20dbf3c2a658131b59e2b98208a0fa1c00742401 100644 (file)
--- 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 b3b19f74b12eae9c723dc8de3bea705d87292f70..6ed928bd7d4bed0d24434d162b6f29f175664aa1 100644 (file)
--- 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 09626896dc0a006f3e1accbf52835d2e4b981066..8bf602657e14680ac29e4433ac18b9394df31704 100644 (file)
--- 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 841e7392be01c5fd8d98cf88eeaff8a52299066d..614a4132798ab4139281ae6ecdad8b32431be28f 100644 (file)
--- 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 9b7074307f080243d899a9294adbf33e9743fc32..0f3a1d3022db4da17b085d4c2169c7429fc6414e 100644 (file)
--- 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 cffdbc0474a47735e298aaf785b746d3b733a2b8..62ce4d84683c8a0fe19759d2d61883a3eeef150b 100644 (file)
--- 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 1da77820566b98a7ef4ee4908c19e03f733d7ae4..1696f104b28eb86e57a2013313522ee1487bccc6 100644 (file)
--- 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 dfd30e1fd67928b42e2382e6cf7731c8757d8be3..a3a2646144c82fff182d2125f55fa42e5e48e8d5 100644 (file)
--- 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 1e43e3cdc2d4e2b13cdd691761effde77ce40e02..84dadda4bf0bfe0b8279442d5f4794f08d3c9f9e 100644 (file)
--- 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 80dc406172d4b4501be98f876bb6eafc416243bd..2eecb91cc8f33a3d92ee29afe36bf008124bfdc7 100644 (file)
--- 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 774dbffcb487180f600d1182cd27ca1dd4414bdc..adbc5c216d120868979889b2d2368b8db0de2ada 100644 (file)
--- 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 fc2e7a789454c4e38c5d6228c6b112591be598b0..bfd5746345709990e6519c51a77432ab951a9969 100644 (file)
--- 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 22cdde8e489fe73b2940241796eaef74f17b500d..4b4785fb6d2b2d8296bb08c9e99439343233898c 100644 (file)
--- 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 e993419f1a32de9809d16a14dc786f90664c52ea..49ceea42bb7dbe8ac2a3ed8c94d68d2fe2c08398 100644 (file)
--- 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 47d3fda529d36148cb61b5cb3ae8f8ca5c60c431..3b25eb26413d27dcce2a8ca6d25e64dc5527939e 100644 (file)
--- 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 c4c87fecd4ab1839e987515910f8307b9ac7352a..af46438ec151120b6ccdc1253dba26d4be957892 100755 (executable)
--- 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):