Disable proof testers for delicate regressions. (#8735)

This PR disables regress2/nl/ufnia-factor-open-proof.smt2 benchmark which fails with some debug builds in the nightlies. We should consider adding an option to disable testers under certain build configs. This PR also ensures that the lfsc tester displays all the options used to generate the LFSC proof.

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 720b2e075cb42402a3b9b44fa69237b7f2280170..52cb8f9e62837f3c8819a7f32620a22080c41967 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,3 +1,5 @@
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 ; DISABLE-TESTER: lfsc
 (set-logic QF_UFNIA)
 (set-info :status unsat)

diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py
index 838d07e9ba465ce6b634339e639f064deb036267..edaf2005b053ff240a7252e7a5c938ea177bfe6f 100755 (executable)
--- a/test/regress/cli/run_regression.py
+++ b/test/regress/cli/run_regression.py
@@ -167,15 +167,14 @@ class LfscTester(Tester):
 
     def run(self, benchmark_info):
         with tempfile.NamedTemporaryFile() as tmpf:
-            proof_args = [
+            cvc5_args = benchmark_info.command_line_args + [
                 "--dump-proofs",
                 "--proof-format=lfsc",
                 "--proof-granularity=theory-rewrite",
             ]
             output, error, exit_status = run_process(
                 [benchmark_info.cvc5_binary]
-                + benchmark_info.command_line_args
-                + proof_args
+                + cvc5_args
                 + [benchmark_info.benchmark_basename],
                 benchmark_info.benchmark_dir,
                 benchmark_info.timeout,
@@ -184,12 +183,12 @@ class LfscTester(Tester):
             tmpf.flush()
             output, error = output.decode(), error.decode()
             exit_code = self.check_exit_status(
-                "cvc5", EXIT_OK, exit_status, output, error, benchmark_info.command_line_args)
+                "cvc5", EXIT_OK, exit_status, output, error, cvc5_args)
             if exit_code:
                 return exit_code
             if "check" not in output:
-                print('not ok (cvc5) - Empty proof - Flags: {}'.format(exit_status,
-                      benchmark_info.command_line_args))
+                print(
+                    'not ok (cvc5) - Empty proof - Flags: {}'.format(exit_status, cvc5_args))
                 print()
                 print_outputs(output, error)
                 return EXIT_FAILURE
@@ -201,16 +200,15 @@ class LfscTester(Tester):
             )
             output, error = output.decode(), error.decode()
             exit_code = self.check_exit_status(
-                "lfsc", EXIT_OK, exit_status, output, error, benchmark_info.command_line_args)
+                "lfsc", EXIT_OK, exit_status, output, error, cvc5_args)
             if exit_code:
                 return exit_code
             if "success" not in output:
-                print(
-                    "not ok (lfsc) - Unexpected output - Flags: {}".format(benchmark_info.command_line_args))
+                print("not ok (lfsc) - Unexpected output - Flags: {}".format(cvc5_args))
                 print()
                 print_outputs(output, error)
                 return EXIT_FAILURE
-        print("ok - Flags: {}".format(benchmark_info.command_line_args))
+        print("ok - Flags: {}".format(cvc5_args))
         return EXIT_OK