diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-10 12:05:47 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-10 12:05:47 +0000 |
commit | 4b77b48b0069aa5b75163b0ca92d1a066c1f6ebd (patch) | |
tree | 175431c02fd864d381261ddc14855ded2fe6ab91 /src/theory/uf | |
parent | cfd85e45da5400e3d5bd48a6f33bd5cfbf20798f (diff) |
another bugfix for uf
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 7688379d9..438854a9a 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -97,15 +97,20 @@ void TheoryUF::propagate(Effort level) { if (!d_valuation.hasSatValue(literal, satValue)) { d_out->propagate(literal); } else { - std::vector<TNode> assumptions; - if (literal != d_false) { - TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode(); - assumptions.push_back(negatedLiteral); + if (!satValue) { + Debug("uf") << "TheoryUF::propagate(): in conflict" << std::endl; + std::vector<TNode> assumptions; + if (literal != d_false) { + TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode(); + assumptions.push_back(negatedLiteral); + } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + break; + } else { + Debug("uf") << "TheoryUF::propagate(): already asserted" << std::endl; } - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - break; } } } |