Avoid spurious runs in run_regression.py (#6318)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 9 Apr 2021 13:25:04 +0000 (08:25 -0500)
committerGitHub <noreply@github.com>
Fri, 9 Apr 2021 13:25:04 +0000 (13:25 +0000)
The options --check-synth-sol and --check-abducts are independent from the rest of the solver. Hence, it is not necessary to run with/without them enabled in our regressions.

This saves roughly 30-40 seconds on regression regress0-2.

test/regress/run_regression.py

index a4f2b85df2027bfc3a2338019522fde282780ffa..ad46eec88128493fe66b084bf90de6744622f723 100755 (executable)
@@ -327,7 +327,7 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code,
             '--no-check-synth-sol' not in all_args and \
             '--sygus-rr' not in all_args and \
             '--check-synth-sol' not in all_args:
-            extra_command_line_args += ['--check-synth-sol']
+            all_args += ['--check-synth-sol']
         if ('sat' in expected_output_lines or \
             'not_entailed' in expected_output_lines or \
             'unknown' in expected_output_lines) and \
@@ -351,7 +351,7 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code,
         if '--no-check-abducts' not in all_args and \
             '--check-abducts' not in all_args and \
             'get-abduct' in benchmark_content:
-            extra_command_line_args += ['--check-abducts']
+            all_args += ['--check-abducts']
 
         # Create a test case for each extra argument
         for extra_arg in extra_command_line_args: