From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 3 Feb 2022 20:58:20 +0000 (-0600)
Subject: Test proof granularity theory-rewrite by default (#8038)
X-Git-Tag: cvc5-1.0.0~458
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a6cd233b8fb91cb94c2550c0452979fa9286c8c;p=cvc5.git

Test proof granularity theory-rewrite by default (#8038)

Recently we updated proof granularity to be macro by default, but we should test theory-rewrite granularity in our regressions.
---

diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 362af1730..6f0b00fba 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -174,7 +174,7 @@ class ProofTester(Tester):
     def run(self, benchmark_info):
         return super().run(
             benchmark_info._replace(
-                command_line_args=benchmark_info.command_line_args + ["--check-proofs"]
+                command_line_args=benchmark_info.command_line_args + ["--check-proofs", "--proof-granularity=theory-rewrite"]
             )
         )