diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-21 16:18:15 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-21 16:21:25 -0400 |
| commit | 48d863e95d753c0bd477e7e36d0e683e3ec7b27f (patch) | |
| tree | abfd2cd3b9e3d24ca3f0fe90a4c5837ac0c7a7b6 /src/theory/uf/theory_uf.cpp | |
| parent | f72907de5dc6e3f2edec85b67b0ac987bb0f252a (diff) | |
Fix incremental bug in symmetry breaker.
Thanks to Christoph Sticksel for reporting this.
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 69a963360..41935984f 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -38,7 +38,8 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), - d_functionsTerms(c) + d_functionsTerms(c), + d_symb(u) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); |