diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-01 23:06:13 -0400 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-01 23:06:13 -0400 |
commit | f51b6e9a9dc853156ee392c26f40494d91f345e9 (patch) | |
tree | e7fd8c96be799d6f0937f1a55e9a4617c44af8a0 /src | |
parent | 1f1f24f3c8618cb601b2ef95991792c7e3232a71 (diff) |
Fix regression error by turning off model-based solver when models are on
(ironic, yes, but model-based solver doesn't yet produce models)
Diffstat (limited to 'src')
-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); } |