diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 468dfdf7b..0f0f4cfd5 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4515,9 +4515,7 @@ 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 + \brief Test if there exists an interpretation (i.e., assignment) for \c a in the model \c m. def_API('Z3_model_has_interp', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL))) */