diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2013-10-28 14:36:56 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-10-28 14:36:56 -0700 |
| commit | 384952474a1b5e93dd3f08d2fba6a2580c7468e9 (patch) | |
| tree | e7508a459fb6ec7a930ee0d99ec8d465952e0a22 | |
| parent | 0274d973ae504fa74fd73aa80c725a778581bb26 (diff) | |
Turn off model-based arrays (causing crashes in portfolio)
| -rw-r--r-- | src/smt/smt_engine.cpp | 20 |
1 files 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() && |