From 3609bd8a3ef60a0ed61927567f5321eb28365858 Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Mon, 18 Oct 2021 17:50:04 -0500
Subject: [PATCH] Move check for experimental arrays features to
 `theory_arrays.cpp`. (#7391)

Check for experimental array features was done at the parser module, which meant that users of the API could use them without calling Solver::setOption("arrays-exp"). This PR fixes that by moving the check to the internal theory module.
---
 src/parser/smt2/smt2.cpp            |  5 -----
 src/theory/arrays/theory_arrays.cpp | 17 +++++++++++++++--
 test/regress/CMakeLists.txt         |  1 +
 test/regress/regress0/eqrange0.smt2 |  6 ++++++
 4 files changed, 22 insertions(+), 7 deletions(-)
 create mode 100644 test/regress/regress0/eqrange0.smt2

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a69542b17..e1ce29b65 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1124,11 +1124,6 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       Debug("parser") << "applyParseOp: return uminus " << ret << std::endl;
       return ret;
     }
-    if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true")
-    {
-      parseError(
-          "eqrange predicate requires option --arrays-exp to be enabled.");
-    }
     if (kind == api::SINGLETON && args.size() == 1)
     {
       api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]);
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9e69c9f71..93eadde43 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -296,7 +296,19 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
 
 TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
 {
-  // first, see if we need to expand definitions
+  // first, check for logic exceptions
+  Kind k = term.getKind();
+  if (!options().arrays.arraysExp)
+  {
+    if (k == kind::EQ_RANGE)
+    {
+      std::stringstream ss;
+      ss << "Term of kind " << k
+         << " not supported in default mode, try --arrays-exp";
+      throw LogicException(ss.str());
+    }
+  }
+  // see if we need to expand definitions
   TrustNode texp = d_rewriter.expandDefinition(term);
   if (!texp.isNull())
   {
@@ -309,7 +321,8 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
   d_ppEqualityEngine.addTerm(term);
   NodeManager* nm = NodeManager::currentNM();
   Node ret;
-  switch (term.getKind()) {
+  switch (k)
+  {
     case kind::SELECT: {
       // select(store(a,i,v),j) = select(a,j)
       //    IF i != j
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index da9c9f001..272867d0c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -558,6 +558,7 @@ set(regress_0_tests
   regress0/distinct.smtv1.smt2
   regress0/dump-unsat-core-full.smt2
   regress0/echo.smt2
+  regress0/eqrange0.smt2
   regress0/eqrange1.smt2
   regress0/eqrange2.smt2
   regress0/eqrange3.smt2
diff --git a/test/regress/regress0/eqrange0.smt2 b/test/regress/regress0/eqrange0.smt2
new file mode 100644
index 000000000..01713d18f
--- /dev/null
+++ b/test/regress/regress0/eqrange0.smt2
@@ -0,0 +1,6 @@
+; EXPECT: (error "Term of kind EQ_RANGE not supported in default mode, try --arrays-exp")
+; EXIT: 1
+(set-logic QF_AUFLIA)
+(declare-const a (Array Int Int))
+(assert (eqrange a a 0 0))
+(check-sat)
-- 
2.30.2