diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 1a6e9c43f..0c75edbf6 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -9394,7 +9394,7 @@ def _mk_fp_unary_norm(f, a, ctx): [a] = _coerce_fp_expr_list([a], ctx) if z3_debug(): _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression") - return FPRef(f(ctx.ref(), a.as_ast()), ctx) + return BoolRef(f(ctx.ref(), a.as_ast()), ctx) def _mk_fp_unary_pred(f, a, ctx): ctx = _get_ctx(ctx)