diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index d7b81b424..76f9c4bbf 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1794,7 +1794,8 @@ ast * ast_manager::register_node_core(ast * n) {
     CASSERT("nondet_bug", contains || slow_not_contains(n));
 #endif
 
-    ast * r = m_ast_table.insert_if_not_there(n);
+    ast* r = m_ast_table.insert_if_not_there(n);    
+
     SASSERT(r->m_hash == h);
     if (r != n) {
         SASSERT(contains);
diff --git a/src/util/chashtable.h b/src/util/chashtable.h
index 19ff1ef51..989131609 100644
--- a/src/util/chashtable.h
+++ b/src/util/chashtable.h
@@ -281,6 +281,28 @@ public:
     unsigned used_slots() const {
         return m_used_slots;
     }
+
+    void insert_fresh(T const& d) {
+        if (!has_free_cells()) {
+            expand_table();
+        }
+        unsigned mask = m_slots - 1;
+        unsigned h    = get_hash(d);
+        unsigned idx  = h & mask;
+        cell * c      = m_table + idx;
+        cell * new_c  = nullptr;
+        m_size++;
+        if (c->is_free()) {
+            m_used_slots++;
+        }
+        else {
+            new_c = get_free_cell();
+            *new_c = *c;
+        }
+        c->m_next = new_c;
+        c->m_data = d;
+        CASSERT("chashtable_bug", check_invariant());
+    }
     
     void insert(T const & d) {
         if (!has_free_cells())