diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index a6ada4ae6..8bf1f39d9 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -62,6 +62,18 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
+        Z3_TRY;
+        LOG_Z3_model_has_interp(c, m, a);
+        CHECK_NON_NULL(m, 0);
+        if (to_model_ref(m)->has_interpretation(to_func_decl(a))) {
+            return Z3_TRUE;
+        } else {
+            return Z3_FALSE;
+        }
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
     Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f) {
         Z3_TRY;
         LOG_Z3_model_get_func_interp(c, m, f);
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 8d00fb044..050c648e9 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4455,6 +4455,15 @@ END_MLAPI_EXCLUDE
     */
     Z3_ast_opt Z3_API Z3_model_get_const_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a);
 
+    /**
+       \brief Test if there exists an interpretation (i.e., assignment) of constant \c a in the model \c m.
+
+       \pre Z3_get_arity(c, a) == 0
+
+       def_API('Z3_model_has_interp', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL)))
+    */
+    Z3_bool Z3_API Z3_model_has_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a);
+
     /**
        \brief Return the interpretation of the function \c f in the model \c m.
        Return \mlonly [None], \endmlonly \conly \c NULL,