From 9fbe73270fc129c71b10d04c28f7cab4866a6a9f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 19 Sep 2017 01:03:56 -0500
Subject: [PATCH] Fix issue #1105 involving string to int (#1112)

This was introduced by changing the implementation of "isNumber" in this commit:
a94318b

This fixes issue #1105.
---
 src/util/regexp.cpp                          |  3 +++
 test/regress/regress0/strings/Makefile.am    |  3 ++-
 test/regress/regress0/strings/issue1105.smt2 | 10 ++++++++++
 3 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/strings/issue1105.smt2

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index f8fc1833c..ef1ab9249 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -349,6 +349,9 @@ String String::substr(std::size_t i, std::size_t j) const {
 }
 
 bool String::isNumber() const {
+  if (d_str.empty()) {
+    return false;
+  }
   for (unsigned character : d_str) {
     unsigned char c = convertUnsignedIntToChar(character);
     if (c < '0' || c > '9') {
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 8f4e3dc4b..6cdba7c9d 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -88,7 +88,8 @@ TESTS = \
   username_checker_min.smt2 \
   repl-empty-sem.smt2 \
   bug799-min.smt2 \
-  strings-charat.cvc
+  strings-charat.cvc \
+  issue1105.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/issue1105.smt2 b/test/regress/regress0/strings/issue1105.smt2
new file mode 100644
index 000000000..81e7672da
--- /dev/null
+++ b/test/regress/regress0/strings/issue1105.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-datatype Val (
+    (Str (str String))
+    (Num (num Int))))
+
+(declare-const var0 Val)
+(assert (=> (is-Str var0) (distinct (str.to.int (str var0)) (- 1))))
+(check-sat)
-- 
2.30.2