From 7b3494856e47945dd5c9774d2063f095f46fc4df Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 22 May 2018 11:43:15 -0700 Subject: [PATCH] Disable symmetry breaker for unsat cores (#1958) Currently, --check-unsat-cores fails for one of our regressions. It turns out that the issue is due to preprocessing done by the symmetry breaker. The symmetry breaker does not add dependencies and thus the generated unsat core is incomplete/wrong. This commit disables the symmetry breaker when we are generating unsat cores (it was previously only disabled when generating proofs). Fixes issue #1953. --- src/smt/smt_engine.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 36792e3c0..e96393f11 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1565,7 +1565,8 @@ void SmtEngine::setDefaults() { // by default, symmetry breaker is on only for QF_UF if(! options::ufSymmetryBreaker.wasSetByUser()) { - bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified() && !options::proof(); + 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); } -- 2.30.2