From 6a6cd233b8fb91cb94c2550c0452979fa9286c8c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 3 Feb 2022 14:58:20 -0600 Subject: [PATCH] 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. --- test/regress/run_regression.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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"] ) ) -- 2.30.2