diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-01 20:06:09 -0400 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-01 20:47:21 -0400 |
| commit | 1898e8aa441a83f83a7603a7e157284accbd019b (patch) | |
| tree | 0a0333ae4b67790e597b5aecb89fa9a37d05c3c5 | |
| parent | 4d7cff8156c2e409be209f1ee489dcf05f922d50 (diff) | |
Disabling eager array index splitting for QF_AX
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d4448787f..8d13b5cc6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -864,12 +864,13 @@ void SmtEngine::setLogicInternal() throw() { Trace("smt") << "setting ite simplification to " << iteSimp << endl; options::doITESimp.set(iteSimp); } - // Turn off array eager index splitting for QF_AUFLIA + // Turn off array eager index splitting for QF_AUFLIA and QF_AX if(! options::arraysEagerIndexSplitting.wasSetByUser()) { if (not d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_ARRAY) && - d_logic.isTheoryEnabled(THEORY_UF) && - d_logic.isTheoryEnabled(THEORY_ARITH)) { + (d_logic.isPure(THEORY_ARRAY) || + (d_logic.isTheoryEnabled(THEORY_UF) && + d_logic.isTheoryEnabled(THEORY_ARITH)))) { Trace("smt") << "setting array eager index splitting to false" << endl; options::arraysEagerIndexSplitting.set(false); } |