3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00

build again

This commit is contained in:
Nikolaj Bjorner 2021-02-04 12:36:44 -08:00
parent b3144a534d
commit cc39cf037e

View file

@ -1107,10 +1107,10 @@ def _coerce_exprs(a, b, ctx=None):
if not is_expr(a) and not is_expr(b):
a = _py2expr(a, ctx)
b = _py2expr(b, ctx)
if isinstance(a, str):
a = StringVal(a, ctx)
if isinstance(b, str):
b = StringVal(b, ctx)
if isinstance(a, str) and isinstance(b, SeqRef):
a = StringVal(a, b.ctx)
if isinstance(b, str) and isinstance(a, SeqRef):
b = StringVal(b, a.ctx)
s = None
s = _coerce_expr_merge(s, a)
s = _coerce_expr_merge(s, b)