From 9f4784e950f295d45cf6b0bdb1def1b83bb11b1a Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Sat, 10 Jul 2010 04:32:03 +0000
Subject: [PATCH] Fix for the type in sat propagation.

---
 src/prop/sat.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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);
-- 
2.30.2