mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
#6456 - elaborate on error message
This commit is contained in:
parent
86f3702403
commit
fcaa85d7a8
|
@ -105,7 +105,7 @@ extern "C" {
|
||||||
symbol sname = to_symbol(name);
|
symbol sname = to_symbol(name);
|
||||||
|
|
||||||
if (mk_c(c)->get_dt_plugin()->is_declared(sname)) {
|
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);
|
RETURN_Z3(nullptr);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue