Take change

src/theory/quantifiers/inst_strategy_mbqi.cpp

@@ -212,13 +212,13 @@ void InstStrategyMbqi::process(Node q)
   for (const Node& k : skolems.d_subs)
   {
     TypeNode tn = k.getType();
-    itk = freshVarType.find(tn);
-    if (itk == freshVarType.end())
+    if (!tn.isUninterpretedSort())
     {
       // not an uninterpreted sort, continue
       continue;
     }
-    if (itk->second.empty())
+    itk = freshVarType.find(tn);
+    if (itk == freshVarType.end() || itk->second.empty())
     {
       Trace("mbqi") << "warning: failed to get vars for type " << tn
                     << std::endl;
@@ -386,14 +386,6 @@ Node InstStrategyMbqi::convertToQuery(
       {
         cmap[cur] = cur;
       }
-      else if (ck == Kind::UNINTERPRETED_SORT_VALUE)
-      {
-        // return the fresh variable for this term
-        Node k = sm->mkPurifySkolem(cur);
-        freshVarType[cur.getType()].insert(k);
-        cmap[cur] = k;
-        continue;
-      }
       else if (ck == Kind::CONST_SEQUENCE || ck == Kind::FUNCTION_ARRAY_CONST
                || cur.isVar())
       {
@@ -443,7 +435,17 @@ Node InstStrategyMbqi::convertToQuery(
         }
       }
       else if (d_nonClosedKinds.find(ck) != d_nonClosedKinds.end())
-      {
+      {        
+        // if its a constant, we can continue, we will assume it is distinct
+        // from all others of its type
+        if (cur.isConst())
+        {
+          // return the fresh variable for this term
+          Node k = sm->mkPurifySkolem(cur);
+          freshVarType[cur.getType()].insert(k);
+          cmap[cur] = k;
+          continue;
+        }
         // if this is a bad kind, fail immediately
         return Node::null();
       }