4 files changed, 9 insertions, 13 deletions
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 773159b09..b59d01fdd 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -215,11 +215,6 @@ Node SkolemManager::mkDummySkolem(const std::string& prefix,
   return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags);
 }
 
-Node SkolemManager::mkBooleanTermVariable(Node t)
-{
-  return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
-}
-
 ProofGenerator* SkolemManager::getProofGenerator(Node t) const
 {
   std::map<Node, ProofGenerator*>::const_iterator it = d_gens.find(t);
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 13d0491a6..a6709373c 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -255,12 +255,6 @@ class SkolemManager
                      const std::string& comment = "",
                      int flags = NodeManager::SKOLEM_DEFAULT);
   /**
-   * Make Boolean term variable for term t. This is a special case of
-   * mkPurifySkolem above, where the returned term has kind
-   * BOOLEAN_TERM_VARIABLE.
-   */
-  Node mkBooleanTermVariable(Node t);
-  /**
    * Get proof generator for existentially quantified formula q. This returns
    * the proof generator that was provided in a call to mkSkolem above.
    */
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index eb2df1285..9b23301f3 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -96,8 +96,14 @@ Node SkolemCache::mkTypedSkolemCached(
   {
     // exists k. k = a
     case SK_PURIFY:
-      sk = sm->mkPurifySkolem(a, c, "string purify skolem");
-      break;
+    {
+      // for sequences of Booleans, we may purify Boolean terms, in which case
+      // they must be Boolean term variables.
+      int flags = a.getType().isBoolean() ? NodeManager::SKOLEM_BOOL_TERM_VAR
+                                          : NodeManager::SKOLEM_DEFAULT;
+      sk = sm->mkPurifySkolem(a, c, "string purify skolem", flags);
+    }
+    break;
     // these are eliminated by normalizeStringSkolem
     case SK_ID_V_SPT:
     case SK_ID_V_SPT_REV:
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 956f2148c..02c0c3130 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -331,6 +331,7 @@ bool TheoryStrings::collectModelInfoType(
               // otherwise, it is a shared term
               argVal = d_valuation.getModelValue(nfe.d_nf[0][0]);
             }
+            Assert(!argVal.isNull());
             Node c = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal));
             pure_eq_assign[eqc] = c;
             Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") ";