fixed bv bug due to applying equisatisfiable transformations in ppRewrite

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 5ae07466ab2dd25f6df8ad1e10dc43e1f459e625..d3da10a90f651e0a4d0766375123ae50a1aeecac 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -578,9 +578,7 @@ Node TheoryBV::ppRewrite(TNode t)
     } else {
       res = t;
     }
-  } else if (RewriteRule<IsPowerOfTwo>::applies(t)) {
-    res = RewriteRule<IsPowerOfTwo>::run<false>(t);
-  }
+  } 
   
 
   // if(t.getKind() == kind::EQUAL &&

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 33994782a3d1aea07123f9b5d375eab53f974e55..c8705e1213d6a63621e415c052b1323fd88a850f 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1195,8 +1195,8 @@ Node RewriteRule<UltPlusOne>::apply(TNode node) {
 
 /** 
  * x ^(x-1) = 0 => 1 << sk
- * Note: only to be called in ppRewrite and not rewrite!
- * (it calls the rewriter)
+ * WARNING: this is an **EQUISATISFIABLE** transformation!
+ * Only to be called on top level assertions. 
  * 
  * @param node 
  *