From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 26 Sep 2018 21:50:51 +0000 (-0500)
Subject: Enable quantified array regression. (#2539)
X-Git-Tag: cvc5-1.0.0~4498
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=79e866c5150a1d8e4d613f1673bfbf33eb157653;p=cvc5.git

Enable quantified array regression. (#2539)
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 88be6b94b..3f6aa7956 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -626,6 +626,7 @@ set(regress_0_tests
   regress0/quantifiers/nested-inf.smt2
   regress0/quantifiers/partial-trigger.smt2
   regress0/quantifiers/pure_dt_cbqi.smt2
+  regress0/quantifiers/qarray-sel-over-store.smt2
   regress0/quantifiers/qbv-inequality2.smt2
   regress0/quantifiers/qbv-simp.smt2
   regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index a1cba3b55..c79f42078 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -635,6 +635,7 @@ REG0_TESTS = \
 	regress0/quantifiers/nested-inf.smt2 \
 	regress0/quantifiers/partial-trigger.smt2 \
 	regress0/quantifiers/pure_dt_cbqi.smt2 \
+	regress0/quantifiers/qarray-sel-over-store.smt2 \
 	regress0/quantifiers/qbv-inequality2.smt2 \
 	regress0/quantifiers/qbv-simp.smt2 \
 	regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 \