diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-10 12:32:13 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-10 12:32:13 +0000 |
| commit | b7ae17461d929f64e34d5a69afaaac2885ca3b66 (patch) | |
| tree | a4eebb76d85f583a48284f1e3949db6939e3a5e4 | |
| parent | 4b77b48b0069aa5b75163b0ca92d1a066c1f6ebd (diff) | |
yet another uf bug fix, hopefully the last
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 438854a9a..409edc53a 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -65,6 +65,16 @@ void TheoryUF::check(Effort level) { case kind::NOT: if (assertion[0].getKind() == kind::APPLY_UF) { d_equalityEngine.addEquality(assertion[0], d_false, assertion); + } else { + // disequality + TNode equality = assertion[0]; + if (d_equalityEngine.getRepresentative(equality[0]) == d_equalityEngine.getRepresentative(equality[1])) { + std::vector<TNode> assumptions; + assumptions.push_back(assertion); + explain(equality, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + } } break; default: |