mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

FreshConst is_sort

Browse source
This commit is contained in:
humnrdble 2025-07-27 09:37:48 +02:00 • committed by GitHub
parent ad2934f8cf
commit 6b5d351248
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"):
"""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)
return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)