diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 8524090e9..aafd1e00b 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -724,8 +724,15 @@ namespace smt { void theory_fpa::init_model(model_generator & mg) { TRACE("t_fpa", tout << "initializing model" << std::endl; display(tout);); ast_manager & m = get_manager(); + context & ctx = get_context(); m_factory = alloc(fpa_value_factory, m, get_family_id()); mg.register_factory(m_factory); + + for (enode* n : ctx.enodes()) { + theory_var v = n->get_th_var(get_family_id()); + if (v != -1 && is_uninterp_const(n->get_owner())) + ctx.mark_as_relevant(n->get_owner()); + } } enode* theory_fpa::ensure_enode(expr* e) {