diff options
Diffstat (limited to 'src/theory')
-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: |