From 7dd7d83a36ea0d18b0d6d15afe1a78fd73507da0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 26 Jan 2021 11:01:03 -0800
Subject: [PATCH] make it easier to use string literals

---
 src/api/python/z3/z3.py     | 10 ++++++++++
 src/ast/seq_decl_plugin.cpp |  4 +++-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 0e87fdd42..622d2152b 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -1100,6 +1100,10 @@ def _coerce_expr_merge(s, a):
             if z3_debug():
                 _z3_assert(s1.ctx == s.ctx, "context mismatch")
                 _z3_assert(False, "sort mismatch")
+    elif s:
+        return s
+    elif isinstance(a, str):
+        return StringSort()
     else:
         return s
 
@@ -1107,6 +1111,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)
     s = None
     s = _coerce_expr_merge(s, a)
     s = _coerce_expr_merge(s, b)
@@ -2934,6 +2942,8 @@ def _py2expr(a, ctx=None):
         return IntVal(a, ctx)
     if isinstance(a, float):
         return RealVal(a, ctx)
+    if isinstance(a, str):
+        return StringVal(a, ctx)
     if is_expr(a):
         return a
     if z3_debug():
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 41f3a6b50..45c318f7d 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -180,8 +180,10 @@ bool zstring::uses_unicode() const {
 
 bool zstring::well_formed() const {
     for (unsigned ch : m_buffer) {
-        if (ch > unicode_max_char())
+        if (ch > unicode_max_char()) {
+            IF_VERBOSE(0, verbose_stream() << "large character: " << ch << "\n";);
             return false;
+        }
     }
     return true;
 }