diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 22c0bcf13..331e27d95 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1656,12 +1656,13 @@ void SmtEngine::setDefaults() { } } - // by default, symmetry breaker is on only for QF_UF + // by default, symmetry breaker is on only for non-incremental QF_UF if(! options::ufSymmetryBreaker.wasSetByUser()) { - bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified() - && !options::proof() && !options::unsatCores(); - Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl; - options::ufSymmetryBreaker.set(qf_uf); + bool qf_uf_noinc = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified() + && !options::incrementalSolving() && !options::proof() + && !options::unsatCores(); + Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << endl; + options::ufSymmetryBreaker.set(qf_uf_noinc); } // If in arrays, set the UF handler to arrays |