From: lianah <lianahady@gmail.com>
Date: Thu, 21 Mar 2013 19:46:52 +0000 (-0400)
Subject: fixed compilation problem
X-Git-Tag: cvc5-1.0.0~7361^2~25
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=43ed2d4e9575232655db7df249ba9be1fc9eba61;p=cvc5.git

fixed compilation problem
---

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index ef87e83b6..437be9bf4 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -631,7 +631,7 @@ void Slicer::registerEquality(TNode eq) {
   }
 }
 
-void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<Node>& explanation) {
+void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<TNode>& explanation) {
   Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl;
   
   Index high = utils::getSize(node) - 1;
@@ -651,7 +651,7 @@ void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::ve
 
   for (unsigned i = 0; i < explanation_ids.size(); ++i) {
     Assert (hasExplanation(explanation_ids[i])); 
-    Node exp = getExplanation(explanation_ids[i]);
+    TNode exp = getExplanation(explanation_ids[i]);
     explanation.push_back(exp); 
   }