From a11995367676365c43e807cd1e49f6091d2e93c5 Mon Sep 17 00:00:00 2001 From: Shaoyuan CHEN Date: Sat, 4 Apr 2020 04:13:51 +0800 Subject: [PATCH] z3py: fix And/Or context deduction (#3687) --- src/api/python/z3/z3.py | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 005c7e8cb..c0f904e7e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1716,11 +1716,10 @@ def And(*args): ctx = args[0].ctx args = [a for a in args[0]] else: - ctx = main_ctx() + ctx = None args = _get_args(args) - ctx_args = _ctx_from_ast_arg_list(args, ctx) + ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx)) if z3_debug(): - _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): return _probe_and(args, ctx) @@ -1745,12 +1744,14 @@ def Or(*args): if isinstance(last_arg, Context): ctx = args[len(args)-1] args = args[:len(args)-1] + elif len(args) == 1 and isinstance(args[0], AstVector): + ctx = args[0].ctx + args = [a for a in args[0]] else: - ctx = main_ctx() + ctx = None args = _get_args(args) - ctx_args = _ctx_from_ast_arg_list(args, ctx) + ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx)) if z3_debug(): - _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): return _probe_or(args, ctx)