Fix for the type in sat propagation.

diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 4cc7f19027ab6cff9cb6790a9717418af241eaa9..57ec29259653d274cde885fc7f4fe48e9d97048a 100644 (file)
--- 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);