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.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 36792e3c0453fa53b61c8ccc38d2ba20b296fe4f..e96393f1197401faa2e45c6cd6714c5fa7042414 100644 (file)
--- 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);
   }