Merge branch 'master' into lfscTestslfscTests

1 files changed, 4 insertions, 3 deletions

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 4af75f1cc..8fb854d91 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -82,12 +82,13 @@ Node SkolemCache::mkTypedSkolemCached(
   }
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Node sk;
   switch (id)
   {
     // exists k. k = a
     case SK_PURIFY:
-      sk = ProofSkolemCache::mkPurifySkolem(a, c, "string purify skolem");
+      sk = sm->mkPurifySkolem(a, c, "string purify skolem");
       break;
     // these are eliminated by normalizeStringSkolem
     case SK_ID_V_SPT:
@@ -113,7 +114,7 @@ Node SkolemCache::mkTypedSkolemCached(
       Notice() << "Don't know how to handle Skolem ID " << id << std::endl;
       Node v = nm->mkBoundVar(tn);
       Node cond = nm->mkConst(true);
-      sk = ProofSkolemCache::mkSkolem(v, cond, c, "string skolem");
+      sk = sm->mkSkolem(v, cond, c, "string skolem");
     }
     break;
   }