diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 610d57a8c..b6f678fea 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1929,9 +1929,6 @@ void ast_manager::delete_node(ast * n) {
         TRACE("mk_var_bug", tout << "del_ast: " << " " << n->m_ref_count << "\n";);
         TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";);
 
-        // SASSERT(m_ast_table.contains(n));
-        m_ast_table.erase(n);
-        SASSERT(!m_ast_table.contains(n));
         SASSERT(!m_debug_ref_count || !m_debug_free_indices.contains(n->m_id));
 
 #ifdef RECYCLE_FREE_AST_INDICES