From c033f432d857cefe9abd580b4bfe6378098cd068 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 26 Nov 2025 13:57:24 -0800
Subject: [PATCH] remove references to set_has_size

---
 src/api/api_array.cpp   | 1 -
 src/api/api_ast.cpp     | 2 --
 src/api/python/z3/z3.py | 9 +--------
 src/api/z3_api.h        | 8 --------
 4 files changed, 1 insertion(+), 19 deletions(-)

diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp
index 6613892df..e0f71f2b7 100644
--- a/src/api/api_array.cpp
+++ b/src/api/api_array.cpp
@@ -268,7 +268,6 @@ extern "C" {
     MK_UNARY(Z3_mk_set_complement, mk_c(c)->get_array_fid(), OP_SET_COMPLEMENT, SKIP);
     MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP);
     MK_BINARY(Z3_mk_array_ext, mk_c(c)->get_array_fid(), OP_ARRAY_EXT, SKIP);
-    MK_BINARY(Z3_mk_set_has_size, mk_c(c)->get_array_fid(), OP_SET_HAS_SIZE, SKIP);
 
     Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f) {
         Z3_TRY;
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index f22716b19..f936a28c9 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1192,8 +1192,6 @@ extern "C" {
             case OP_SET_SUBSET: return Z3_OP_SET_SUBSET;
             case OP_AS_ARRAY: return Z3_OP_AS_ARRAY;
             case OP_ARRAY_EXT: return Z3_OP_ARRAY_EXT;
-            case OP_SET_CARD: return Z3_OP_SET_CARD;
-            case OP_SET_HAS_SIZE: return Z3_OP_SET_HAS_SIZE;
             default:
                 return Z3_OP_INTERNAL;
             }
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index f57702878..71ae588b1 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -5016,13 +5016,6 @@ def Ext(a, b):
         _z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays")
     return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
 
-
-def SetHasSize(a, k):
-    ctx = a.ctx
-    k = _py2expr(k, ctx)
-    return _to_expr_ref(Z3_mk_set_has_size(ctx.ref(), a.as_ast(), k.as_ast()), ctx)
-
-
 def is_select(a):
     """Return `True` if `a` is a Z3 array select application.
 
@@ -10276,7 +10269,7 @@ class FPNumRef(FPRef):
     """
 
     def sign(self):
-        num = (ctypes.c_bool)()
+        num = ctypes.c_bool()
         nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num))
         if nsign is False:
             raise Z3Exception("error retrieving the sign of a numeral.")
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 5f5a1e04c..8f33ec558 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1063,8 +1063,6 @@ typedef enum {
     Z3_OP_SET_SUBSET,
     Z3_OP_AS_ARRAY,
     Z3_OP_ARRAY_EXT,
-    Z3_OP_SET_HAS_SIZE,
-    Z3_OP_SET_CARD,
 
     // Bit-vectors
     Z3_OP_BNUM = 0x400,
@@ -3357,12 +3355,6 @@ extern "C" {
      */
     Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f);
 
-    /**
-       \brief Create predicate that holds if Boolean array \c set has \c k elements set to true.       
-
-       def_API('Z3_mk_set_has_size', AST, (_in(CONTEXT), _in(AST), _in(AST)))
-    */
-    Z3_ast Z3_API Z3_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k);
 
     /**@}*/