From c340233df6bbe98b6225176aed2ba3697236b545 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Jan 2024 10:31:31 -0800 Subject: [PATCH] fix #7081 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 18d3abc9d..b3b4351ab 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -10969,10 +10969,10 @@ def CharVal(ch, ctx=None): raise Z3Exception("character value should be an ordinal") return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx) -def CharFromBv(ch, ctx=None): - if not is_expr(ch): - raise Z3Expression("Bit-vector expression needed") - return _to_expr_ref(Z3_mk_char_from_bv(ch.ctx_ref(), ch.as_ast()), ch.ctx) +def CharFromBv(bv): + if not is_expr(bv): + raise Z3Exception("Bit-vector expression needed") + return _to_expr_ref(Z3_mk_char_from_bv(bv.ctx_ref(), bv.as_ast()), bv.ctx) def CharToBv(ch, ctx=None): ch = _coerce_char(ch, ctx)