From 51eaf84eed2e4c0c3c93eebcca31bf1edf085893 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Apr 2020 15:37:18 -0700 Subject: [PATCH] fix #3931 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index c0f904e7e..0a01fd2e1 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3060,7 +3060,8 @@ def IntVector(prefix, sz, ctx=None): >>> Sum(X) 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): """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() 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): """Return a fresh real constant in the given context using the given prefix.