From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sat, 10 Jul 2010 04:32:03 +0000 (+0000)
Subject: Fix for the type in sat propagation.
X-Git-Tag: cvc5-1.0.0~8909
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9f4784e950f295d45cf6b0bdb1def1b83bb11b1a;p=cvc5.git

Fix for the type in sat propagation.
---

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