diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 16:23:58 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 16:23:58 -0500 |
commit | 031722bee8682005bd4c8700ef78b5f893fc48fe (patch) | |
tree | 46a936a1bd20ea2cc588df0d3205cf7eb0fd4177 /src/smt | |
parent | e79e64329ce7d6df0003cab28dadb9b8bcc6f9ca (diff) |
New implementation of sets+cardinality. Merge Paul Meng's relation solver as extension of sets solver, add regressions.
Diffstat (limited to 'src/smt')
-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 */ + |