added rewriting to bv-pow2 pass

diff --git a/src/theory/bv/bvintropow2.cpp b/src/theory/bv/bvintropow2.cpp
index bd092ed126318a53dc048a9050b48e9e01ef90eb..d7f5d6fde4985644c799cceb40f93ab357f8e29c 100644 (file)
--- 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;
   }
 }