diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 19bc85e3e..f288c6c0a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1926,7 +1926,8 @@ void SmtEngine::setDefaults() { //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ - if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ + //AJR: cannot use minisat elim for new implementation of sets TODO: why? + if( d_logic.isTheoryEnabled(THEORY_SETS) || d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ options::minisatUseElim.set( false ); } } @@ -5467,3 +5468,4 @@ void SmtEngine::setReplayStream(ExprStream* replayStream) { } }/* CVC4 namespace */ + |