From 384952474a1b5e93dd3f08d2fba6a2580c7468e9 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 28 Oct 2013 14:36:56 -0700 Subject: [PATCH] Turn off model-based arrays (causing crashes in portfolio) --- src/smt/smt_engine.cpp | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index be6acd09c..0b233e7b6 100644 --- 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() && -- 2.30.2