From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 2 Feb 2021 20:20:44 +0000 (-0600)
Subject: Remove quantifiers regression from decision folder (#5830)
X-Git-Tag: cvc5-1.0.0~2329
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;ds=sidebyside;h=478638868ec11c18882b9036850cafe4ff36f4bb;p=cvc5.git

Remove quantifiers regression from decision folder (#5830)

This is a duplicate of https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 and moreover is slow on proof-new.
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index de84761f0..4cee236c1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1474,7 +1474,6 @@ set(regress_1_tests
   regress1/datatypes/non-simple-rec-param.smt2
   regress1/decision/error3.smtv1.smt2
   regress1/decision/quant-Arrays_Q1-noinfer.smt2
-  regress1/decision/quant-symmetric_unsat_7.smt2
   regress1/error.cvc
   regress1/errorcrash.smt2
   regress1/fmf-fun-dbu.smt2
diff --git a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2 b/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2
deleted file mode 100644
index fd621171c..000000000
--- a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2
+++ /dev/null
@@ -1,37 +0,0 @@
-; COMMAND-LINE: --no-check-unsat-cores --decision=justification
-; EXPECT: unsat
-
-(set-logic AUFLIRA)
-(set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods.
-
-It was translated to SMT-LIB by Leonardo de Moura |)
-(set-info :smt-lib-version 2.0)
-(set-info :category "crafted")
-(set-info :status unsat)
-(declare-fun symmetric ((Array Int (Array Int Real)) Int) Bool)
-(declare-fun n () Int)
-(declare-fun a0 () (Array Int (Array Int Real)))
-(declare-fun e0 () Real)
-(declare-fun a1 () (Array Int (Array Int Real)))
-(declare-fun e1 () Real)
-(declare-fun a2 () (Array Int (Array Int Real)))
-(declare-fun e2 () Real)
-(declare-fun a3 () (Array Int (Array Int Real)))
-(declare-fun e3 () Real)
-(declare-fun a4 () (Array Int (Array Int Real)))
-(declare-fun e4 () Real)
-(declare-fun a5 () (Array Int (Array Int Real)))
-(declare-fun e5 () Real)
-(declare-fun a6 () (Array Int (Array Int Real)))
-(declare-fun e6 () Real)
-(assert (forall ((?a (Array Int (Array Int Real))) (?n Int)) (= (symmetric ?a ?n) (forall ((?i Int) (?j Int)) (=> (and (<= 1 ?i) (<= ?i ?n) (<= 1 ?j) (<= ?j ?n)) (= (select (select ?a ?i) ?j) (select (select ?a ?j) ?i)))))))
-(assert (symmetric a0 n))
-(assert (= a1 (store a0 0 (store (select a0 0) 0 e0))))
-(assert (= a2 (store a1 1 (store (select a1 1) 1 e1))))
-(assert (= a3 (store a2 2 (store (select a2 2) 2 e2))))
-(assert (= a4 (store a3 3 (store (select a3 3) 3 e3))))
-(assert (= a5 (store a4 4 (store (select a4 4) 4 e4))))
-(assert (= a6 (store a5 5 (store (select a5 5) 5 e5))))
-(assert (not (symmetric a6 n)))
-(check-sat)
-(exit)