diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 3e094e082..34dab3ed6 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1186,6 +1186,10 @@ extern "C" {
             case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV;
             case OP_FPA_INTERNAL_BVWRAP:
             case OP_FPA_INTERNAL_BVUNWRAP:
+            case OP_FPA_INTERNAL_MIN_I:
+            case OP_FPA_INTERNAL_MAX_I:
+            case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
+            case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
             case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
             case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
             case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index 84eb5168b..a351b2610 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -184,6 +184,22 @@ class fpa_decl_plugin : public decl_plugin {
     unsigned mk_id(mpf const & v);
     void recycled_id(unsigned id);
 
+    virtual bool is_considered_uninterpreted(func_decl * f) {
+        if (f->get_family_id() != get_family_id())
+            return false;
+        switch (f->get_decl_kind())
+        {
+        case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
+        case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
+        case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
+        case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
+            return true;
+        default:
+            return false;
+        }
+        return false;
+    }
+
 public:
     fpa_decl_plugin();
 
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 486111ae4..583a8dad5 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -111,7 +111,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = 0;
         family_id fid = f->get_family_id();
-        if (fid == null_family_id && num == 0) {
+        if (num == 0 && (fid == null_family_id || m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) {
             expr * val = m_model.get_const_interp(f);
             if (val != 0) {
                 result = val;