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)