From 5e8f88d8a539b73e1777faadb2015f672fc011a0 Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Fri, 6 May 2022 21:49:24 -0500
Subject: [PATCH] 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.
---
 .../regress2/nl/ufnia-factor-open-proof.smt2   |  2 ++
 test/regress/cli/run_regression.py             | 18 ++++++++----------
 2 files changed, 10 insertions(+), 10 deletions(-)

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
 
 
-- 
2.30.2