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

z3py: fix And/Or context deduction (#3687)

Browse source
This commit is contained in:
Shaoyuan CHEN 2020-04-04 04:13:51 +08:00 • committed by GitHub
parent 9d58fccd41
commit a119953676
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1716,11 +1716,10 @@ def And(*args):
ctx = args[0].ctx ctx = args[0].ctx
args = [a for a in args[0]] args = [a for a in args[0]]
else: else:
ctx = main_ctx() ctx = None
args = _get_args(args) 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(): 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") _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
if _has_probe(args): if _has_probe(args):
return _probe_and(args, ctx) return _probe_and(args, ctx)
@ -1745,12 +1744,14 @@ def Or(*args):
if isinstance(last_arg, Context): if isinstance(last_arg, Context):
ctx = args[len(args)-1] ctx = args[len(args)-1]
args = 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: else:
ctx = main_ctx() ctx = None
args = _get_args(args) 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(): 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") _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
if _has_probe(args): if _has_probe(args):
return _probe_or(args, ctx) return _probe_or(args, ctx)