added rewriting to bv-pow2 pass

1 files changed, 4 insertions, 0 deletions

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;
   }
 }