From 6d99a8f0cc6e0a91f6d397451f52ad16d900b23b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 31 Jan 2021 14:55:52 -0800
Subject: [PATCH] fixes for unicode

---
 src/ast/char_decl_plugin.cpp | 9 ++++++++-
 src/smt/theory_char.cpp      | 3 ++-
 src/util/zstring.cpp         | 2 +-
 3 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp
index 561efc769..fd9ec1f62 100644
--- a/src/ast/char_decl_plugin.cpp
+++ b/src/ast/char_decl_plugin.cpp
@@ -74,6 +74,7 @@ void char_decl_plugin::set_manager(ast_manager * m, family_id id) {
 
 void char_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const& logic) {
     op_names.push_back(builtin_name("char.<=", OP_CHAR_LE));
+    op_names.push_back(builtin_name("Char", OP_CHAR_CONST));
 }
 
 void char_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const& logic) {
@@ -113,8 +114,14 @@ expr* char_decl_plugin::get_some_value(sort* s) {
 app* char_decl_plugin::mk_le(expr* a, expr* b) {
     expr_ref _ch1(a, *m_manager), _ch2(b, *m_manager);
     unsigned v1 = 0, v2 = 0;
-    if (is_const_char(a, v1) && is_const_char(b, v2))
+    bool c1 = is_const_char(a, v1);
+    bool c2 = is_const_char(b, v2);
+    if (c1 && c2)
         return m_manager->mk_bool_val(v1 <= v2);
+    if (c1 && v1 == 0)
+        return m_manager->mk_true();
+    if (c2 && v2 == max_char())
+        return m_manager->mk_true();
     expr* es[2] = { a, b };
     return m_manager->mk_app(m_family_id, OP_CHAR_LE, 2, es);    
 }
diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp
index e67ab7bd2..e506f5278 100644
--- a/src/smt/theory_char.cpp
+++ b/src/smt/theory_char.cpp
@@ -15,6 +15,7 @@ Author:
 
 --*/
 
+#include "ast/ast_ll_pp.h"
 #include "smt/theory_char.h"
 #include "smt/smt_context.h"
 #include "smt/smt_model_generator.h"
@@ -241,7 +242,7 @@ namespace smt {
                     enforce_ackerman(u, v);
                     return false;
                 }
-                if (c >= seq.max_char()) {
+                if (c > seq.max_char()) {
                     enforce_value_bound(v);
                     return false;
                 }
diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp
index b643c2491..a980bc1d0 100644
--- a/src/util/zstring.cpp
+++ b/src/util/zstring.cpp
@@ -45,7 +45,7 @@ bool zstring::is_escape_char(char const *& s, unsigned& result) {
     unsigned d;
     if (*s == '\\' && *(s+1) == 'u' && *(s+2) == '{') {
         result = 0;
-        for (unsigned i = 0; i < 5; ++i) {
+        for (unsigned i = 0; i < 6; ++i) {
             if (is_hex_digit(*(s+3+i), d)) {
                 result = 16*result + d;
             }