Turn off model-based arrays (causing crashes in portfolio)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index be6acd09cc3c953b8bce463a53cc15e382228621..0b233e7b68a4998f60b839e11a37d3e66ef85535 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -881,16 +881,16 @@ void SmtEngine::setLogicInternal() throw() {
     }
   }
   // Turn on model-based arrays for QF_AX (unless models are enabled)
-  if(! options::arraysModelBased.wasSetByUser()) {
-    if (not d_logic.isQuantified() &&
-        d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-        d_logic.isPure(THEORY_ARRAY) &&
-        !options::produceModels() &&
-        !options::checkModels()) {
-      Trace("smt") << "turning on model-based array solver" << endl;
-      options::arraysModelBased.set(true);
-    }
-  }
+  // if(! options::arraysModelBased.wasSetByUser()) {
+  //   if (not d_logic.isQuantified() &&
+  //       d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+  //       d_logic.isPure(THEORY_ARRAY) &&
+  //       !options::produceModels() &&
+  //       !options::checkModels()) {
+  //     Trace("smt") << "turning on model-based array solver" << endl;
+  //     options::arraysModelBased.set(true);
+  //   }
+  // }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
   if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&