From: lianah <lianahady@gmail.com>
Date: Mon, 16 Jun 2014 00:36:12 +0000 (-0400)
Subject: fixed bv bug due to applying equisatisfiable transformations in ppRewrite
X-Git-Tag: cvc5-1.0.0~6804
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=22c89dae0078a89b2c95d07c98e7ae29b5586ebd;p=cvc5.git

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 5ae07466a..d3da10a90 100644
--- 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 33994782a..c8705e121 100644
--- 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 
  *