mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

fix #7081

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-16 10:31:31 -08:00
parent afba43a5a7
commit c340233df6
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/python/z3/z3.py
View file

@ -10969,10 +10969,10 @@ def CharVal(ch, ctx=None):
raise Z3Exception("character value should be an ordinal") raise Z3Exception("character value should be an ordinal")
return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx) return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx)
def CharFromBv(ch, ctx=None): def CharFromBv(bv):
if not is_expr(ch): if not is_expr(bv):
raise Z3Expression("Bit-vector expression needed") raise Z3Exception("Bit-vector expression needed")
return _to_expr_ref(Z3_mk_char_from_bv(ch.ctx_ref(), ch.as_ast()), ch.ctx) return _to_expr_ref(Z3_mk_char_from_bv(bv.ctx_ref(), bv.as_ast()), bv.ctx)
def CharToBv(ch, ctx=None): def CharToBv(ch, ctx=None):
ch = _coerce_char(ch, ctx) ch = _coerce_char(ch, ctx)