diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-22 11:43:15 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-22 11:43:15 -0700 |
| commit | 7b3494856e47945dd5c9774d2063f095f46fc4df (patch) | |
| tree | 26b2a95e86630b87069227eedf2bd829430c746b | |
| parent | cdf7aacd6b682645cf1a2bc609db005b2f4dafc7 (diff) | |
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.
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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); } |