From 1072bf153660b4606584ca74710aaa3f2f5b321b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 May 2020 14:42:06 -0700
Subject: [PATCH] deal with unsigned / bignum #4361

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_str_mc.cpp | 22 ++++++++++++++++------
 src/util/rational.h       | 21 ++++++++++++++-------
 2 files changed, 30 insertions(+), 13 deletions(-)

diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index 6518a0186..aae8234b0 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -668,14 +668,21 @@ namespace smt {
             if (pos.is_neg() || pos >= rational(base_chars.size()) || len.is_neg()) {
                 eqc_chars.reset();
                 return true;
+            }
+            else if (!pos.is_unsigned() || !len.is_unsigned()) {
+                return false;
             } else {
-                if (pos + len >= rational(base_chars.size())) {
+                unsigned _pos = pos.get_unsigned();
+                unsigned _len = len.get_unsigned();
+                if (_pos + _len < _pos) 
+                    return false;
+                if (_pos + _len >= base_chars.size()) {
                     // take as many characters as possible up to the end of base_chars
-                    for (unsigned i = pos.get_unsigned(); i < base_chars.size(); ++i) {
+                    for (unsigned i = _pos; i < base_chars.size(); ++i) {
                         eqc_chars.push_back(base_chars.get(i));
                     }
                 } else {
-                    for (unsigned i = pos.get_unsigned(); i < pos.get_unsigned() + len.get_unsigned(); ++i) {
+                    for (unsigned i = _pos; i < _pos + _len; ++i) {
                         eqc_chars.push_back(base_chars.get(i));
                     }
                 }
@@ -697,6 +704,9 @@ namespace smt {
             if (pos_value.is_neg() || pos_value >= rational(base_chars.size())) {
                 // return the empty string
                 eqc_chars.reset();
+            }
+            else if (!pos_value.is_unsigned()) {
+                return false;
             } else {
                 eqc_chars.push_back(base_chars.get(pos_value.get_unsigned()));
             }
@@ -728,7 +738,7 @@ namespace smt {
                 eqc_chars.reset();
                 return true;
             } else {
-                if (termLen.get_unsigned() != iValue.to_string().length()) {
+                if (termLen != iValue.get_num_decimal()) {
                     // conflict
                     cex = expr_ref(m.mk_not(m.mk_and(get_context().mk_eq_atom(mk_strlen(term), mk_int(termLen)), get_context().mk_eq_atom(arg0, mk_int(iValue)))), m);
                     return false;
@@ -1093,7 +1103,7 @@ namespace smt {
                 for (expr * chExpr : char_subterms) {
                     expr_ref chAssignment(subModel->get_const_interp(to_app(chExpr)->get_decl()), m);
                     rational n;
-                    if (chAssignment != nullptr && bv.is_numeral(chAssignment, n)) {
+                    if (chAssignment != nullptr && bv.is_numeral(chAssignment, n) && n.is_unsigned()) {
                         assignment.push_back(n.get_unsigned());
                     } else {
                         assignment.push_back((unsigned)'?');
@@ -1115,7 +1125,7 @@ namespace smt {
                 for (expr * chExpr : char_subterms) {
                     expr_ref chAssignment(subModel->get_const_interp(to_app(chExpr)->get_decl()), m);
                     rational n;
-                    if (chAssignment != nullptr && bv.is_numeral(chAssignment, n)) {
+                    if (chAssignment != nullptr && bv.is_numeral(chAssignment, n) && n.is_unsigned()) {
                         assignment.push_back(n.get_unsigned());
                     } else {
                         assignment.push_back((unsigned)'?');
diff --git a/src/util/rational.h b/src/util/rational.h
index d078b62ef..c7f0358dd 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -417,18 +417,25 @@ public:
 
     static bool is_rational() { return true; }
 
-    unsigned get_num_bits() const {
-        rational two(2);
+    unsigned get_num_digits(rational const& base) const {
         SASSERT(is_int());
         SASSERT(!is_neg());
         rational n(*this);
-        unsigned num_bits = 1;
-        n = div(n, two);
+        unsigned num_digits = 1;
+        n = div(n, base);
         while (n.is_pos()) {
-            ++num_bits;
-            n = div(n, two);
+            ++num_digits;
+            n = div(n, base);
         }
-        return num_bits;
+        return num_digits;
+    }
+
+    unsigned get_num_bits() const {
+        return get_num_digits(rational(2));
+    }
+
+    unsigned get_num_decimal() const {
+        return get_num_digits(rational(10));
     }
 
     static bool limit_denominator(rational &num, rational const& limit);