From: lianah <lianahady@gmail.com>
Date: Wed, 11 Jun 2014 18:07:17 +0000 (-0400)
Subject: fixing bv ackermanization cache bug
X-Git-Tag: cvc5-1.0.0~6839
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e74baf4081853c247df3048bb0172a502a4fa854;p=cvc5.git

fixing bv ackermanization cache bug
---

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) {