From 3452e2bd9344ec503329720f41e747510cebade5 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Sat, 14 Jun 2014 23:18:40 -0400
Subject: [PATCH] added rewriting to bv-pow2 pass

---
 src/theory/bv/bvintropow2.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/theory/bv/bvintropow2.cpp b/src/theory/bv/bvintropow2.cpp
index bd092ed12..d7f5d6fde 100644
--- a/src/theory/bv/bvintropow2.cpp
+++ b/src/theory/bv/bvintropow2.cpp
@@ -12,6 +12,10 @@ void BVIntroducePow2::pow2Rewrite(std::vector<Node>& assertionsToPreprocess){
   for(size_t i = 0, N= assertionsToPreprocess.size(); i < N; ++i){
     Node curr = assertionsToPreprocess[i];
     Node next = pow2Rewrite(curr, cache);
+    if(next != curr){
+      Node tmp = Rewriter::rewrite(next);
+      next = tmp;
+    }
     assertionsToPreprocess[i] = next;
   }
 }
-- 
2.30.2