diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 52958a782..8524090e9 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -728,6 +728,33 @@ namespace smt {
         mg.register_factory(m_factory);
     }
 
+    enode* theory_fpa::ensure_enode(expr* e) {
+        context& ctx = get_context();
+        if (!ctx.e_internalized(e)) {
+            ctx.internalize(e, false);
+        }
+        enode* n = ctx.get_enode(e);
+        ctx.mark_as_relevant(n);
+        return n;
+    }
+
+    app* theory_fpa::get_ite_value(expr* e) {
+        ast_manager & m = get_manager();
+        expr* e1, *e2, *e3;
+        while (m.is_ite(e, e1, e2, e3)) {
+            if (get_root(e2) == get_root(e)) {
+                e = e2;
+            }
+            else if (get_root(e3) == get_root(e)) {
+                e = e3;
+            }
+            else {
+                break;
+            }
+        }
+        return to_app(e);
+    }
+
     model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
         TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) <<
                             " (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";);
@@ -735,7 +762,7 @@ namespace smt {
         ast_manager & m = get_manager();
         context & ctx = get_context();
         app_ref owner(m);
-        owner = n->get_owner();
+        owner = get_ite_value(n->get_owner());
 
         // If the owner is not internalized, it doesn't have an enode associated.
         SASSERT(ctx.e_internalized(owner));
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index dd9fcfc65..aa95dd2e0 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -196,6 +196,10 @@ namespace smt {
 
         app_ref wrap(expr * e);
         app_ref unwrap(expr * e, sort * s);
+
+        enode* ensure_enode(expr* e);
+        enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
+        app* get_ite_value(expr* e);
     };
 
 };