From a66a1915cb12faa18ac806d83b4fc2aae18426aa Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 16 Apr 2018 16:03:31 -0700 Subject: [PATCH] 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. --- .../regress1/decision/quant-symmetric_unsat_7.smt2.expect | 2 +- test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) 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 7fd1d5a98..9d6ac53ca 100644 --- 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 6acf4a3c6..6465e27d6 100644 --- 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. -- 2.30.2