From dbe0cf93129899644423b1ca907391b21189131e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Jun 2026 12:04:56 -0700 Subject: [PATCH] disregard skolems in instantiation set? Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/term_enumeration.cpp | 1 + src/smt/smt_model_finder.cpp | 2 ++ 2 files changed, 3 insertions(+) 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);