diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 5802c1e64..71d1de212 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -105,7 +105,7 @@ extern "C" { symbol sname = to_symbol(name); if (mk_c(c)->get_dt_plugin()->is_declared(sname)) { - SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + SET_ERROR_CODE(Z3_INVALID_ARG, "enumeration sort name is already declared"); RETURN_Z3(nullptr); }