Disable check proofs/unsat cores for two regs (#1785)

Disabling proof checking/unsat core checking for the two benchmarks in
question, reduces the time to run regressions significantly. After the
change, regression level 2 takes 7m30s to run on my machine and
regression level 1 takes just below 3m (16 threads). Individually, the
tests take over 7m each when checking proofs/unsat cores, so they add
significant overhead.

diff --git a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect b/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect
index 7fd1d5a98b1cb37200814bfff1f2c710c50e4373..9d6ac53ca54f0ec25bbf3e5ee2e6956c7b791fb0 100644 (file)
--- a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect
+++ b/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect
@@ -1,2 +1,2 @@
-% COMMAND-LINE: --decision=justification
+% COMMAND-LINE: --no-check-proofs --no-check-unsat-cores --decision=justification
 % EXPECT: unsat

diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
index 6acf4a3c621e08acfe68d91b9aa0cb8a6e90820b..6465e27d68861b93fafc21953e637dcd67968624 100644 (file)
--- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
+++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
 (set-logic AUFLIRA)
 (set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods.