From 756645326bb2c0578b340e05e03c8276cacd1dd9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 29 May 2014 17:33:03 +0100 Subject: [PATCH] Bugfix for And/Or operators in Python. Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 4eae61c3d..ff0bd6641 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -899,6 +899,7 @@ def _coerce_expr_merge(s, a): return s else: if __debug__: + _z3_assert(s1.ctx == s.ctx, "context mismatch") _z3_assert(False, "sort mismatch") else: return s @@ -1459,9 +1460,18 @@ def And(*args): >>> And(P) And(p__0, p__1, p__2, p__3, p__4) """ - args = _get_args(args) - ctx = _ctx_from_ast_arg_list(args) + last_arg = None + if len(args) > 0: + last_arg = args[len(args)-1] + if isinstance(last_arg, Context): + ctx = args[len(args)-1] + args = args[:len(args)-1] + else: + ctx = main_ctx() + args = _get_args(args) + ctx_args = _ctx_from_ast_arg_list(args, ctx) if __debug__: + _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch") _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): return _probe_and(args, ctx) @@ -1480,9 +1490,18 @@ def Or(*args): >>> Or(P) Or(p__0, p__1, p__2, p__3, p__4) """ - args = _get_args(args) - ctx = _ctx_from_ast_arg_list(args) + last_arg = None + if len(args) > 0: + last_arg = args[len(args)-1] + if isinstance(last_arg, Context): + ctx = args[len(args)-1] + args = args[:len(args)-1] + else: + ctx = main_ctx() + args = _get_args(args) + ctx_args = _ctx_from_ast_arg_list(args, ctx) if __debug__: + _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch") _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): return _probe_or(args, ctx)