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.

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index f8fc1833cbc867ddca426c737944fa68621b3a89..ef1ab9249262b7e13f8b89fd09f7696df7faae4d 100644 (file)
--- 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 8f4e3dc4b677f4a24317c1075166fa70f049cf7b..6cdba7c9d4bad92a9a2d45cfe2b707e497bfbe08 100644 (file)
--- 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 (file)
index 0000000..81e7672
--- /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)