diff --git a/src/ast/rewriter/term_enumeration.cpp b/src/ast/rewriter/term_enumeration.cpp
index 32af302227..886e34bae6 100644
--- a/src/ast/rewriter/term_enumeration.cpp
+++ b/src/ast/rewriter/term_enumeration.cpp
@@ -355,6 +355,7 @@ public:
         m_rewriter(term, simplified);
         if (m_seen_terms.contains(simplified))
             return nullptr;
+        IF_VERBOSE(0, verbose_stream() << "add " << simplified << "\n");
         m_seen_terms.insert(simplified);
         m_bank.add(simplified, cost);
         return simplified;
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 6ef1e55c6e..4ba66a51be 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1423,6 +1423,8 @@ namespace smt {
                         TRACE(model_finder, tout << "inserting " << mk_pp(e, m) << " into inst set\n");
                         S->insert(e, n->get_generation());
                     }
+                    else if (is_app(e) && to_app(e)->get_decl()->is_skolem())
+                        ;
                     else if (is_uninterp_const(e)) {
                         TRACE(model_finder, tout << "add production " << mk_pp(e, m) << "\n");
                         tn.add_production(e);