mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
1ca3381390
commit
a8b02ddb93
|
@ -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)
|
||||
|
|
Loading…
Reference in a new issue