1 files changed, 9 insertions, 28 deletions
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 72605e9d1..0f46fa790 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -38,38 +38,19 @@ void ExprMiner::initialize(const std::vector<Node>& vars, SygusSampler* ss)
 
 Node ExprMiner::convertToSkolem(Node n)
 {
-  std::vector<Node> fvs;
-  TermUtil::computeVarContains(n, fvs);
-  if (fvs.empty())
+  if (d_skolems.empty())
   {
-    return n;
-  }
-  std::vector<Node> sfvs;
-  std::vector<Node> sks;
-  // map to skolems
-  NodeManager* nm = NodeManager::currentNM();
-  SkolemManager* sm = nm->getSkolemManager();
-  for (unsigned i = 0, size = fvs.size(); i < size; i++)
-  {
-    Node v = fvs[i];
-    // only look at the sampler variables
-    if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end())
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
+    for (const Node& v : d_vars)
     {
-      sfvs.push_back(v);
-      std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
-      if (itf == d_fv_to_skolem.end())
-      {
-        Node sk = sm->mkDummySkolem("rrck", v.getType());
-        d_fv_to_skolem[v] = sk;
-        sks.push_back(sk);
-      }
-      else
-      {
-        sks.push_back(itf->second);
-      }
+      Node sk = sm->mkDummySkolem("rrck", v.getType());
+      d_skolems.push_back(sk);
+      d_fv_to_skolem[v] = sk;
     }
   }
-  return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
+  return n.substitute(
+      d_vars.begin(), d_vars.end(), d_skolems.begin(), d_skolems.end());
 }
 
 void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,