diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 9f5c22787..f5c5ffb98 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -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)