From d3bc11dd3a18408ec8fe45ef3bcf6bbc4ef9d691 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Jan 2022 12:38:25 -0800 Subject: [PATCH] bvs have to be expressions Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 6cea34963..150df9f6b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -10697,7 +10697,8 @@ def CharVal(ch, ctx=None): return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx) def CharFromBv(ch, ctx=None): - ch = _coerce_char(ch, ctx) + 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 CharToBv(ch, ctx=None):