From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 16 Apr 2013 15:17:36 +0000 (-0400)
Subject: fixed compile error
X-Git-Tag: cvc5-1.0.0~7293^2~6
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f5750be0382d74569532ae53865158659cf9f2f3;p=cvc5.git

fixed compile error
---

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 7d3f58c8e..44c4bd021 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -241,7 +241,7 @@ bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) {
 }
 
 
-void BvToBoolPreprocessor::liftBoolToBV(const std::vector<TNode>& assertions, std::vector<Node>& new_assertions) {
+void BvToBoolPreprocessor::liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
   TNodeNodeMap candidates;
   for (unsigned i = 0; i < assertions.size(); ++i) {
     if (matchesBooleanPatern(assertions[i])) {
@@ -249,7 +249,7 @@ void BvToBoolPreprocessor::liftBoolToBV(const std::vector<TNode>& assertions, st
       TNode bv_var = assertion[0][0];
       Assert (bv_var.getKind() == kind::VARIABLE &&
               bv_var.getType().isBitVector() &&
-              bv_bar.getType().getBitVectorSize() == 1);
+              bv_var.getType().getBitVectorSize() == 1);
       TNode bool_cond = assertion[1];
       Assert (bool_cond.getType().isBoolean());
       if (candidates.find(bv_var) == candidates.end()) {
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index 9b1534b41..39c6b4251 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -65,7 +65,7 @@ public:
   BvToBoolPreprocessor()
   {}
   ~BvToBoolPreprocessor() {}
-  void liftBoolToBV(const std::vector<TNode>& assertions, std::vector<Node>& new_assertions);
+  void liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
 }; 
 
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8c430d6d4..22a0b00ed 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1277,7 +1277,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
   }
 }
 
-void TheoryEngine::ppBvToBool(const std::vector<TNode>& assertions, std::vector<Node> new_assertions) {
+void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node> new_assertions) {
   d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions);
 }
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index d581aeda2..6d355ccce 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -753,7 +753,7 @@ private:
   theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; 
 public:
 
-  void ppBvToBool(const std::vector<TNode>& assertions, std::vector<Node> new_assertions); 
+  void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node> new_assertions); 
   Node ppSimpITE(TNode assertion);
   void ppUnconstrainedSimp(std::vector<Node>& assertions);