From: Clark Barrett Date: Mon, 28 Oct 2013 21:36:56 +0000 (-0700) Subject: Turn off model-based arrays (causing crashes in portfolio) X-Git-Tag: cvc5-1.0.0~7278^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=384952474a1b5e93dd3f08d2fba6a2580c7468e9;p=cvc5.git Turn off model-based arrays (causing crashes in portfolio) --- 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() &&