1 files changed, 27 insertions, 7 deletions

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 2b0cc8a1b..7725b1b0d 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -20,31 +20,51 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-SkolemCache::SkolemCache() {}
+SkolemCache::SkolemCache()
+{
+  d_strType = NodeManager::currentNM()->stringType();
+}
 
 Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c)
 {
+  return mkTypedSkolemCached(d_strType, a, b, id, c);
+}
+
+Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
+{
+  return mkSkolemCached(a, Node::null(), id, c);
+}
+
+Node SkolemCache::mkTypedSkolemCached(
+    TypeNode tn, Node a, Node b, SkolemId id, const char* c)
+{
   a = a.isNull() ? a : Rewriter::rewrite(a);
   b = b.isNull() ? b : Rewriter::rewrite(b);
   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
   if (it == d_skolemCache[a][b].end())
   {
-    Node sk = mkSkolem(c);
+    Node sk = mkTypedSkolem(tn, c);
     d_skolemCache[a][b][id] = sk;
     return sk;
   }
   return it->second;
 }
-
-Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
+Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
+                                      Node a,
+                                      SkolemId id,
+                                      const char* c)
 {
-  return mkSkolemCached(a, Node::null(), id, c);
+  return mkTypedSkolemCached(tn, a, Node::null(), id, c);
 }
 
 Node SkolemCache::mkSkolem(const char* c)
 {
-  NodeManager* nm = NodeManager::currentNM();
-  Node n = nm->mkSkolem(c, nm->stringType(), "string skolem");
+  return mkTypedSkolem(d_strType, c);
+}
+
+Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
+{
+  Node n = NodeManager::currentNM()->mkSkolem(c, tn, "string skolem");
   d_allSkolems.insert(n);
   return n;
 }