2 files changed, 22 insertions, 6 deletions
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index c1e3c7214..f91b3cd9f 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -112,6 +112,10 @@ class SkolemCache
     //       k(x) is the end index of the x^th occurrence of b in a
     //   where n is the number of occurrences of b in a, and k(0)=0.
     SK_OCCUR_INDEX,
+
+    SK_STOI_U,
+    SK_STOI_US,
+    SK_STOI_UD,
   };
   /**
    * Returns a skolem of type string that is cached for (a,b,id) and has
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 8e057a525..09a90ec18 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -291,11 +291,21 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     std::vector<Node> conc2;
     std::vector< TypeNode > argTypes;
     argTypes.push_back(nm->integerType());
-    Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
-    Node us =
-        nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
-    Node ud =
-        nm->mkSkolem("Ud", nm->mkFunctionType(argTypes, nm->stringType()));
+    Node u = d_sc->mkTypedSkolemCached(
+        nm->mkFunctionType(argTypes, nm->integerType()),
+        s,
+        SkolemCache::SK_STOI_U,
+        "U");
+    Node us = d_sc->mkTypedSkolemCached(
+        nm->mkFunctionType(argTypes, nm->stringType()),
+        s,
+        SkolemCache::SK_STOI_US,
+        "Us");
+    Node ud = d_sc->mkTypedSkolemCached(
+        nm->mkFunctionType(argTypes, nm->stringType()),
+        s,
+        SkolemCache::SK_STOI_US,
+        "Ud");
 
     lem = stoit.eqNode(nm->mkNode(APPLY_UF, u, lens));
     conc2.push_back(lem);
@@ -328,7 +338,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node cb =
         nm->mkNode(AND, nm->mkNode(GEQ, c, d_zero), nm->mkNode(LT, c, ten));
 
-    lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eqs, eq, cb));
+    Node lenlem = nm->mkNode(STRING_LENGTH, udx).eqNode(d_one);
+
+    lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eqs, eq, cb, lenlem));
     lem = nm->mkNode(FORALL, xbv, lem);
     conc2.push_back(lem);