From a8b02ddb93a4cf15b8827ae57b8754f407214b2e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 13:43:45 -0700 Subject: [PATCH] fix #2323 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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)