diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-29 12:46:35 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-29 10:46:35 -0700 |
commit | 908158f6833e3765b18041076187ed4cd8004a85 (patch) | |
tree | 2827c94ca3a3dcef49b945232922ec807df4f20b /src/smt | |
parent | 6059866b361d0852d0b70d484b0cb397f3cc5bf4 (diff) |
Disable minisat elimination when nonlinear is enabled (#2006)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9d4462210..6ecf00ccd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2196,8 +2196,15 @@ void SmtEngine::setDefaults() { //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ - //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() ){ + // cannot use minisat elimination for logics where a theory solver + // introduces new literals into the search. This includes quantifiers + // (quantifier instantiation), and the lemma schemas used in non-linear + // and sets. We also can't use it if models are enabled. + if (d_logic.isTheoryEnabled(THEORY_SETS) || d_logic.isQuantified() + || options::produceModels() || options::produceAssignments() + || options::checkModels() + || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear())) + { options::minisatUseElim.set( false ); } } |