Disabling eager array index splitting for QF_AX

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d4448787fa35c9456fd49882aa793d6f345828c8..8d13b5cc6f2a9f48360b6da4fea0350e5ac4a31c 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -864,12 +864,13 @@ void SmtEngine::setLogicInternal() throw() {
     Trace("smt") << "setting ite simplification to " << iteSimp << endl;
     options::doITESimp.set(iteSimp);
   }
-  // Turn off array eager index splitting for QF_AUFLIA
+  // Turn off array eager index splitting for QF_AUFLIA and QF_AX
   if(! options::arraysEagerIndexSplitting.wasSetByUser()) {
     if (not d_logic.isQuantified() &&
         d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-        d_logic.isTheoryEnabled(THEORY_UF) &&
-        d_logic.isTheoryEnabled(THEORY_ARITH)) {
+        (d_logic.isPure(THEORY_ARRAY) ||
+         (d_logic.isTheoryEnabled(THEORY_UF) &&
+          d_logic.isTheoryEnabled(THEORY_ARITH)))) {
       Trace("smt") << "setting array eager index splitting to false" << endl;
       options::arraysEagerIndexSplitting.set(false);
     }