From 321bad2c84c9bb0c58f44d5797bdf993b47b09d4 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 20 Jan 2020 17:06:35 +0000
Subject: [PATCH] Fix for implicit consts in FPA models. Fixes #2865.

---
 src/smt/theory_fpa.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

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) {