From fcaa85d7a8e48e78c739c40e7c16fb4898a83216 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 20 Nov 2022 11:27:39 +0700
Subject: [PATCH] #6456 - elaborate on error message
---
src/api/api_datatype.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
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);
}