diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-23 17:39:12 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-23 17:39:12 -0500 |
| commit | 3471e731b8538a906e37f8aeb4b0301598b34eff (patch) | |
| tree | e67f70809e791c18aa9ca4800de87a7c707d062b /src/smt/smt_engine.cpp | |
| parent | 03925b816a0f9aeb079e2c0037a426b5946e2eae (diff) | |
Generalize symmetry detection for 1 symmetry variable mapped to n input variables (#1888)
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 958fec175..71256e3d8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4330,9 +4330,9 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl; dumpAssertions("post-simplify", d_assertions); - if (options::symmetryBreakerExp()) + if (options::symmetryBreakerExp() && !options::incrementalSolving()) { - // apply symmetry breaking + // apply symmetry breaking if not in incremental mode d_preprocessingPassRegistry.getPass("sym-break")->apply(&d_assertions); } |