Disable `lfsc` tester if `proof` tester is disabled. (#8857)

This automatically disables the `lfsc` tester for regressions where `proof` tester is disabled.

diff --git a/test/regress/cli/README.md b/test/regress/cli/README.md
index 020b9819b5ba8139fbaf3cc5e843720011f11bc8..efb3fc31f22d41990133afbd6046d1632dab8777 100644 (file)
--- a/test/regress/cli/README.md
+++ b/test/regress/cli/README.md
@@ -124,10 +124,14 @@ excluded by adding the `no-` prefix, e.g. `no-cryptominisat` means that the
 test is not valid for builds that include CryptoMiniSat support.
 
 To disable a specific type of test, the `DISABLE-TESTER` directive can be used.
-The following example disables the proof tester for a regression:
+The following example disables the abduct tester for a regression:
 
 ```
-; DISABLE-TESTER: proof
+; DISABLE-TESTER: abduct
 ```
 
-Multiple testers can be disabled using multiple `DISABLE-TESTER` directives.
+Multiple testers can be disabled using multiple `DISABLE-TESTER` directives. In
+general, each `DISABLE-TESTER` directive disables only the specified tester. The
+only exception to this rule is the proof tester. Disabling the proof tester,
+which directs cvc5 to check generated proofs internally, also disables testers
+that check the printed versions of those proofs (e.g., the lfsc tester).

diff --git a/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2 b/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2
index d5f2e21d888a52c7401e50fe971778767c045fc1..4fdea35d4a213a257243c3ebe6344c8499cded9e 100644 (file)
--- a/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2
+++ b/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2
@@ -2,7 +2,6 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic ALL)
 (declare-const v (_ BitVec 2))
 (declare-const x7 Bool)

diff --git a/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2 b/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2
index d39dc8dca6b1abc30c86438b02fb1be7f0e0050b..ed8cbf55d420f24b35e1fdf5e2c81ea3b7e22d34 100644 (file)
--- a/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2
+++ b/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2
@@ -2,7 +2,6 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic ALL)
 (declare-sort E 0)
 (declare-fun s () (Seq E))

diff --git a/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2 b/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2
index a6b60b68d6ec20bb582540976c78bdc2e3924b88..0d36d2037356adf8d68e5cbef91258702be7c1f6 100644 (file)
--- a/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2
+++ b/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2
@@ -2,7 +2,6 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic LRA)
 (set-info :status unsat)
 (assert (not (exists ((?X Real)) (>= (/ (- 13) 4) ?X))))

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 84dadda4bf0bfe0b8279442d5f4794f08d3c9f9e..269bc515b8e0a7ee2b1871db0c3170498d480f62 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,3 @@
-; 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 2eecb91cc8f33a3d92ee29afe36bf008124bfdc7..f1476c06df8e4f7dc128ea5246bfbd5c639e53f6 100644 (file)
--- a/test/regress/cli/regress1/hole6.cvc.smt2
+++ b/test/regress/cli/regress1/hole6.cvc.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: proof
 ; EXPECT: unsat
 (set-logic ALL)
 (set-option :incremental false)

diff --git a/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2 b/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2
index ef58b42a2db5bfebbe82a881571a5ce9045b7d85..a48660bd8823e18b5205d82a559850c32e47a9e4 100644 (file)
--- a/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2
+++ b/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2
@@ -2,7 +2,6 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic QF_UFNRA)
 (set-option :nl-ext-purify true)
 (set-option :sygus-inference true)

diff --git a/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 b/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2
index adbc5c216d120868979889b2d2368b8db0de2ada..355343d00ab3a6ee4ff7d50e1bf0559b420ac6ec 100644 (file)
--- a/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2
+++ b/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: proof
 ; REQUIRES: poly
 ; COMMAND-LINE: --nl-ext-tplanes
 ; EXPECT: unsat

diff --git a/test/regress/cli/regress1/nl/issue4791-llr.smt2 b/test/regress/cli/regress1/nl/issue4791-llr.smt2
index f11c925f820d466c947ff7ca8e64bfbe90e730bb..fd88a59c0d7c034fa236445988cddafdf3e452e8 100644 (file)
--- a/test/regress/cli/regress1/nl/issue4791-llr.smt2
+++ b/test/regress/cli/regress1/nl/issue4791-llr.smt2
@@ -2,7 +2,6 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 
 ;
 ;!(a,b,c).( 0<=b & 1<=c & 0<=a & 1<=c

diff --git a/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2
index f8ecd754b1dab1adaf5809d39f2812eee660a561..f64ea8e723b189f7c2c3fe2d316aa182ddf3f95e 100644 (file)
--- a/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2
@@ -1,6 +1,5 @@
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic HO_ALL)
 (set-option :miniscope-quant agg)
 (set-option :conjecture-gen true)

diff --git a/test/regress/cli/regress1/sets/sets-disequal.smt2 b/test/regress/cli/regress1/sets/sets-disequal.smt2
index 4b4785fb6d2b2d8296bb08c9e99439343233898c..3acf77108b03e5ebef963ed98f97bfcadcd28aa1 100644 (file)
--- a/test/regress/cli/regress1/sets/sets-disequal.smt2
+++ b/test/regress/cli/regress1/sets/sets-disequal.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: proof
 ; COMMAND-LINE: --incremental
 ; EXPECT: sat
 ; EXPECT: sat

diff --git a/test/regress/cli/regress1/sygus/issue3201.smt2 b/test/regress/cli/regress1/sygus/issue3201.smt2
index 831fce6d42c7bb593ce96351151f2c08033464c1..212fca782c45d911922ee57337e09b32a44476ae 100644 (file)
--- a/test/regress/cli/regress1/sygus/issue3201.smt2
+++ b/test/regress/cli/regress1/sygus/issue3201.smt2
@@ -2,7 +2,6 @@
 ; COMMAND-LINE: --sygus-inference -q
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic ALL)
 (declare-fun v () Bool)
 (assert false)

diff --git a/test/regress/cli/regress1/sygus/issue3247.smt2 b/test/regress/cli/regress1/sygus/issue3247.smt2
index a6f3f6951b23f478aea0a89d325887aedb0bbadc..7e2f439ceada3c12e7219995ac61ebceff961265 100644 (file)
--- a/test/regress/cli/regress1/sygus/issue3247.smt2
+++ b/test/regress/cli/regress1/sygus/issue3247.smt2
@@ -2,7 +2,6 @@
 ; COMMAND-LINE: --sygus-inference --strings-exp -q
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic ALL)
 (declare-fun a () String) 
 (declare-fun b () String) 

diff --git a/test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2
index 6a41fc7a09fef9920f3adffee25ad6b0510b8a39..48b4ab38c59d1ad5e714f66a4c18ce66c7f725ad 100644 (file)
--- a/test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2
+++ b/test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2
@@ -2,7 +2,6 @@
 ; COMMAND-LINE: --sygus-inference --fmf-bound
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic HO_ALL)
 (declare-fun a () (_ BitVec 1))
 (assert (bvsgt (bvsmod a a) #b0))

diff --git a/test/regress/cli/regress1/sygus/issue4009-qep.smt2 b/test/regress/cli/regress1/sygus/issue4009-qep.smt2
index 8f540bf135b67b4dfd71a331b7887c03096e2b48..b27901a1142f5e85d78225bf29594eabed3e3b5d 100644 (file)
--- a/test/regress/cli/regress1/sygus/issue4009-qep.smt2
+++ b/test/regress/cli/regress1/sygus/issue4009-qep.smt2
@@ -2,7 +2,6 @@
 ; COMMAND-LINE: --sygus-inference --sygus-qe-preproc -q
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic ALL)
 (declare-fun a () Real)
 (declare-fun b () Real)

diff --git a/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 b/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2
index 17a9dfa3ca4df00e1e7521e4c4f1a037285bb136..4e867e8aaab58dfdab1e789540a4cf66d50defda 100644 (file)
--- a/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2
+++ b/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2
@@ -2,7 +2,6 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic ALL)
 (set-option :miniscope-quant conj-and-fv)
 (set-option :sygus-inference true)

diff --git a/test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2 b/test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2
index 4e35869b6096e1b9c98dd755e171ba2d0562722e..466bb73130563590d7485034312ee557302300db 100644 (file)
--- a/test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2
+++ b/test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2
@@ -2,7 +2,6 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic ALL)
 (declare-fun a () Int)
 (declare-fun d () Int)

diff --git a/test/regress/cli/regress1/sygus/proj-issue185.smt2 b/test/regress/cli/regress1/sygus/proj-issue185.smt2
index b6228d453ae621feed2603c11264c82df37a1b2e..141ab0ae00f8224b176223ecba791e3f14d6a47c 100644 (file)
--- a/test/regress/cli/regress1/sygus/proj-issue185.smt2
+++ b/test/regress/cli/regress1/sygus/proj-issue185.smt2
@@ -2,7 +2,6 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic ALL)
 (set-option :sygus-inference true)
 (set-info :status unsat)

diff --git a/test/regress/cli/regress2/fp/issue7056.smt2 b/test/regress/cli/regress2/fp/issue7056.smt2
index 17b439a83f81670585b53343938b301e56569b99..e9283c38b5367999319cba7e95b37113e938f238 100644 (file)
--- a/test/regress/cli/regress2/fp/issue7056.smt2
+++ b/test/regress/cli/regress2/fp/issue7056.smt2
@@ -1,6 +1,5 @@
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 ; timeout with unsat cores
 (set-logic ALL)
 (set-info :smt-lib-version 2.6)

diff --git a/test/regress/cli/regress2/instance_1444.smtv1.smt2 b/test/regress/cli/regress2/instance_1444.smtv1.smt2
index fc4cd5802abf56e61da7eea00ad6d50033633afe..3b25eb26413d27dcce2a8ca6d25e64dc5527939e 100644 (file)
--- a/test/regress/cli/regress2/instance_1444.smtv1.smt2
+++ b/test/regress/cli/regress2/instance_1444.smtv1.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: lfsc
 ; DISABLE-TESTER: proof
 (set-option :incremental false)
 (set-info :status unsat)

diff --git a/test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2 b/test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2
index 52cb8f9e62837f3c8819a7f32620a22080c41967..5b6c534b15432a7adc2466728821989bd0cd8e55 100644 (file)
--- a/test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2
+++ b/test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2
@@ -1,6 +1,5 @@
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
-; DISABLE-TESTER: lfsc
 (set-logic QF_UFNIA)
 (set-info :status unsat)
 (declare-fun p2 (Int) Int)

diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py
index edaf2005b053ff240a7252e7a5c938ea177bfe6f..87cb2b5514a7f62dea88c43171b3c4816d66e742 100755 (executable)
--- a/test/regress/cli/run_regression.py
+++ b/test/regress/cli/run_regression.py
@@ -613,6 +613,8 @@ def run_regression(
                 return EXIT_FAILURE
             if disable_tester in testers:
                 testers.remove(disable_tester)
+                if disable_tester == "proof" and "lfsc" in testers:
+                    testers.remove("lfsc")
 
     expected_output = expected_output.strip()
     expected_error = expected_error.strip()