diff --git a/examples/python/mini_ic3.py b/examples/python/mini_ic3.py
index b7b732459..31d3c595b 100644
--- a/examples/python/mini_ic3.py
+++ b/examples/python/mini_ic3.py
@@ -162,6 +162,9 @@ class Goal:
         self.cube = cube
         self.parent = parent
 
+    def __lt__(self, other):
+        return self.level < other.level
+
 def is_seq(f):
     return isinstance(f, list) or isinstance(f, tuple) or isinstance(f, AstVector)
 
@@ -210,12 +213,12 @@ class MiniIC3:
     def next(self, f):
         if is_seq(f):
            return [self.next(f1) for f1 in f]
-        return substitute(f, zip(self.x0, self.xn))    
+        return substitute(f, [p for p in zip(self.x0, self.xn)])    
     
     def prev(self, f):
         if is_seq(f):
            return [self.prev(f1) for f1 in f]
-        return substitute(f, zip(self.xn, self.x0))    
+        return substitute(f, [p for p in zip(self.xn, self.x0)])    
     
     def add_solver(self):
         s = fd_solver()
diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 421441af9..63a38be36 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -890,12 +890,8 @@ namespace dd {
                 rest = p;
             }
         }
-        if (gc_generation != m_gc_generation) {
-            // Cache was reset while factoring (due to GC),
-            // which means the old entry has been removed and we need to insert it again.
-            auto* et = m_factor_cache.insert_if_not_there2({p.root, v, degree});
-            e = &et->get_data();
-        }
+        et = m_factor_cache.insert_if_not_there2({p.root, v, degree});
+        e = &et->get_data();        
         e->m_lc = lc.root;
         e->m_rest = rest.root;
     }