From 4e483037765f1e0288df12fcda6c9b331c30b6be Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 13 Jul 2026 03:52:14 +0000
Subject: [PATCH] Fix Java API ClassCastException when getting EnumSort of
 constant

- Add EnumSort(Context ctx, long obj) constructor to allow creating
  EnumSort from an existing native sort object
- Modify Sort.create() to detect enum sorts (all constructors have
  arity 0) and return EnumSort instead of DatatypeSort, mirroring
  Z3's own is_enum_sort implementation

Closes #7335
---
 src/api/java/EnumSort.java |  5 +++++
 src/api/java/Sort.java     | 11 +++++++++++
 2 files changed, 16 insertions(+)

diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java
index 5cd11ba08b..6dcbee519e 100644
--- a/src/api/java/EnumSort.java
+++ b/src/api/java/EnumSort.java
@@ -92,6 +92,11 @@ public class EnumSort<R> extends Sort
         return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
     }
 
+    EnumSort(Context ctx, long obj)
+    {
+        super(ctx, obj);
+    }
+
     EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
     {
         super(ctx, Native.mkEnumerationSort(ctx.nCtx(),
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index 4910338f35..8be2cda7b8 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -125,6 +125,17 @@ public class Sort extends AST
         case Z3_BV_SORT:
             return new BitVecSort(ctx, obj);
         case Z3_DATATYPE_SORT:
+            int n = Native.getDatatypeSortNumConstructors(ctx.nCtx(), obj);
+            boolean isEnum = true;
+            for (int i = 0; i < n && isEnum; i++) {
+                long ctor = Native.getDatatypeSortConstructor(ctx.nCtx(), obj, i);
+                if (Native.getDomainSize(ctx.nCtx(), ctor) != 0) {
+                    isEnum = false;
+                }
+            }
+            if (isEnum) {
+                return new EnumSort<>(ctx, obj);
+            }
             return new DatatypeSort<>(ctx, obj);
         case Z3_INT_SORT:
             return new IntSort(ctx, obj);