diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-07-10 04:32:03 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-07-10 04:32:03 +0000 |
| commit | 9f4784e950f295d45cf6b0bdb1def1b83bb11b1a (patch) | |
| tree | 157889bff166dcaefc7191039d7ca51e4990df7c /src/prop/sat.cpp | |
| parent | fbcdcf6a0ad9766eb87566c7a9ec5876a65f5585 (diff) | |
Fix for the type in sat propagation.
Diffstat (limited to 'src/prop/sat.cpp')
| -rw-r--r-- | src/prop/sat.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 4cc7f1902..57ec29259 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -71,7 +71,7 @@ void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) { Debug("prop-explain") << "explainPropagation(" << lNode.toString() << ")" << std::endl; Node theoryExplanation = d_theoryEngine->getExplanation(lNode); Debug("prop-explain") << "explainPropagation() => " << theoryExplanation.toString() << std::endl; - if (lNode.getKind() == kind::AND) { + if (theoryExplanation.getKind() == kind::AND) { Node::const_iterator it = theoryExplanation.begin(); Node::const_iterator it_end = theoryExplanation.end(); explanation.push(l); |