diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 5e177ef08..6f4dcf430 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -11252,35 +11252,38 @@ def user_prop_fresh(id, ctx):
     _prop_closures.set(new_prop.id, new_prop)
     return ctypes.c_void_p(new_prop.id)
 
+def to_Ast(ptr,):
+    ast = Ast(ptr)
+    super(ctypes.c_void_p, ast).__init__(ptr)
+    return ast
 
 def user_prop_fixed(ctx, cb, id, value):
     prop = _prop_closures.get(ctx)
     prop.cb = cb
-    prop.fixed(_to_expr_ref(ctypes.c_void_p(id), prop.ctx()), _to_expr_ref(ctypes.c_void_p(value), prop.ctx()))
+    id = _to_expr_ref(to_Ast(id), prop.ctx())
+    value = _to_expr_ref(to_Ast(value), prop.ctx())
+    prop.fixed(id, value)
     prop.cb = None
 
-
 def user_prop_final(ctx, cb):
     prop = _prop_closures.get(ctx)
     prop.cb = cb
     prop.final()
     prop.cb = None
 
-
 def user_prop_eq(ctx, cb, x, y):
     prop = _prop_closures.get(ctx)
     prop.cb = cb
-    x = _to_expr_ref(ctypes.c_void_p(x), prop.ctx())
-    y = _to_expr_ref(ctypes.c_void_p(y), prop.ctx())
+    x = _to_expr_ref(to_Ast(x), prop.ctx())
+    y = _to_expr_ref(to_Ast(y), prop.ctx())
     prop.eq(x, y)
     prop.cb = None
 
-
 def user_prop_diseq(ctx, cb, x, y):
     prop = _prop_closures.get(ctx)
     prop.cb = cb
-    x = _to_expr_ref(ctypes.c_void_p(x), prop.ctx())
-    y = _to_expr_ref(ctypes.c_void_p(y), prop.ctx())
+    x = _to_expr_ref(to_Ast(x), prop.ctx())
+    y = _to_expr_ref(to_Ast(y), prop.ctx())
     prop.diseq(x, y)
     prop.cb = None