From b3144a534dfc801a805e276bc77614c872571dd3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Feb 2021 21:40:45 -0800 Subject: [PATCH] remove string conversion causing regression --- src/api/python/z3/z3.py | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 16efc2f06..9f5c22787 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1100,10 +1100,6 @@ def _coerce_expr_merge(s, a): if z3_debug(): _z3_assert(s1.ctx == s.ctx, "context mismatch") _z3_assert(False, "sort mismatch") - elif s is not None: - return s - elif isinstance(a, str): - return StringSort() else: return s