From c76d9cde04270156030d0a3fa8f1bf8483bfe2eb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Jul 2021 09:06:33 -0500 Subject: [PATCH] Revert change to regression (#6940) Although it works on most machines, it times out in the nightly builds. --- test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 index e866d789c..7249e87aa 100644 --- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 +++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 @@ -1,3 +1,8 @@ +; COMMAND-LINE: --no-check-unsat-cores --no-produce-proofs +; EXPECT: unsat + +; Note we require disabling proofs/unsat cores due to timeouts in nightlies + (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