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 36f8cc34f..ff36e87d5 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 2eb6ee297..33c72871c 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -5010,13 +5010,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.
 
@@ -10039,7 +10032,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 e812278ff..746a9d2a6 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1037,8 +1037,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,
@@ -3316,12 +3314,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);
 
     /**@}*/