Enable quantified array regression. (#2539)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 88be6b94bd9800cc2723b842cf9f80c95614d591..3f6aa79566672c6136ad0ee0dbc7b057b8e107a6 100644 (file)
--- 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 a1cba3b5548ce07a54a8e6f73aa4aa2ff108fd14..c79f42078e51d5af0a398f9530508fc14b846fdf 100644 (file)
--- 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 \