mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 16:03:16 +00:00
Code Activity

FreshConst is_sort (#7748)

Browse source
This commit is contained in:
humnrdble 2025-07-27 12:19:43 +02:00 • committed by GitHub
parent ad2934f8cf
commit eb24488c3e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1506,6 +1506,8 @@ def Consts(names, sort):
def FreshConst(sort, prefix="c"): def FreshConst(sort, prefix="c"):
"""Create a fresh constant of a specified sort""" """Create a fresh constant of a specified sort"""
if z3_debug():
_z3_assert(is_sort(sort), f"Z3 sort expected, got {type(sort)}")
ctx = _get_ctx(sort.ctx) ctx = _get_ctx(sort.ctx)
return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx) return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)