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

fix #3931

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-12 15:37:18 -07:00
parent c85113acdb
commit 51eaf84eed
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3060,7 +3060,8 @@ def IntVector(prefix, sz, ctx=None):
>>> Sum(X) >>> Sum(X)
x__0 + x__1 + x__2 x__0 + x__1 + x__2
""" """
return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ] ctx = _get_ctx(ctx)
return [ Int('%s__%s' % (prefix, i), ctx) for i in range(sz) ]
def FreshInt(prefix='x', ctx=None): def FreshInt(prefix='x', ctx=None):
"""Return a fresh integer constant in the given context using the given prefix. """Return a fresh integer constant in the given context using the given prefix.
@ -3112,7 +3113,8 @@ def RealVector(prefix, sz, ctx=None):
>>> Sum(X).sort() >>> Sum(X).sort()
Real Real
""" """
return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ] ctx = _get_ctx(ctx)
return [ Real('%s__%s' % (prefix, i), ctx) for i in range(sz) ]
def FreshReal(prefix='b', ctx=None): def FreshReal(prefix='b', ctx=None):
"""Return a fresh real constant in the given context using the given prefix. """Return a fresh real constant in the given context using the given prefix.