From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Sat, 7 May 2022 02:49:24 +0000 (-0500)
Subject: Disable proof testers for delicate regressions. (#8735)
X-Git-Tag: cvc5-1.0.1~156
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5e8f88d8a539b73e1777faadb2015f672fc011a0;p=cvc5.git

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 720b2e075..52cb8f9e6 100644
--- 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 838d07e9b..edaf2005b 100755
--- 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