fixing bv ackermanization cache bug

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 117a3e552767e87a66acff23592a73cd88e1ac9b..f6092031cc7ccb86ebb99e48b564e8a1546328b4 100644 (file)
--- 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) {