diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-26 17:11:31 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-26 15:11:31 -0700 |
| commit | b03cb5dc423e83307479e3a513ad6d4abc98d3e9 (patch) | |
| tree | 8bae4cdac2f0ee7fb57453292acea3cee70af80e | |
| parent | d48fc396512ede240e30952793abefce719726d1 (diff) | |
Disable uf symmetry breaker in incremental mode (#2091)
| -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 1b5e88536..5652eeaa6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1657,12 +1657,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 |