From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Jul 2021 14:06:33 +0000 (-0500)
Subject: Revert change to regression (#6940)
X-Git-Tag: cvc5-1.0.0~1443
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c76d9cde04270156030d0a3fa8f1bf8483bfe2eb;p=cvc5.git

Revert change to regression (#6940)

Although it works on most machines, it times out in the nightly builds.
---

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.