fixed compile error

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 7d3f58c8e1ff0d04c0b7802752ee275c8b83cb04..44c4bd0217e0e48cf9bd0e14b312374fbb534769 100644 (file)
--- 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 9b1534b41e2368e01c310793316dfe5172256359..39c6b4251bafbbbe7c6639e9020938eeba068c5f 100644 (file)
--- 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 8c430d6d400f86e108e0c6c6045e542414735f68..22a0b00ed8178e9167dc194246c8c553ae33a229 100644 (file)
--- 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 d581aeda2e43d0415fc91c9292f811006a541e13..6d355ccce4a5e315a91121112b9ddc146e9c7c80 100644 (file)
--- 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);