diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7bbc12551..de41a34a0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -874,11 +874,13 @@ void SmtEngine::setLogicInternal() throw() { options::arraysEagerIndexSplitting.set(false); } } - // Turn on model-based arrays for QF_AX + // 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)) { + d_logic.isPure(THEORY_ARRAY) && + !options::produceModels() && + !options::checkModels()) { Trace("smt") << "turning on model-based array solver" << endl; options::arraysModelBased.set(true); } |