From e74baf4081853c247df3048bb0172a502a4fa854 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Wed, 11 Jun 2014 14:07:17 -0400
Subject: [PATCH] fixing bv ackermanization cache bug

---
 src/theory/bv/theory_bv.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 117a3e552..f6092031c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -185,6 +185,7 @@ void TheoryBV::collectNumerators(TNode term, TNodeSet& seen) {
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
     collectNumerators(term[i], seen); 
   }
+  seen.insert(term); 
 }
 
 void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
-- 
2.30.2