From b03cb5dc423e83307479e3a513ad6d4abc98d3e9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 26 Jun 2018 17:11:31 -0500 Subject: [PATCH] Disable uf symmetry breaker in incremental mode (#2091) --- src/smt/smt_engine.cpp | 11 ++++++----- 1 file 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 -- 2.30.2