nodemanager robust skolem numbering

2 files changed, 1 insertions, 10 deletions

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index edb245d99..9d00cde7b 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -760,12 +760,6 @@ bool TheorySetsPrivate::isComplete() {
   return d_pending.empty() && d_pendingDisequal.empty();
 }
 
-Node TheorySetsPrivate::newSkolem(TypeNode t) {
-  ostringstream oss;
-  oss << "sde_" << (++d_skolemCounter);
-  return NodeManager::currentNM()->mkSkolem(oss.str(), t, "", NodeManager::SKOLEM_EXACT_NAME);
-}
-
 Node TheorySetsPrivate::getLemma() {
   Assert(!d_pending.empty() || !d_pendingDisequal.empty());
 
@@ -786,7 +780,7 @@ Node TheorySetsPrivate::getLemma() {
     d_pendingEverInserted.insert(n);
 
     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
-    Node x = newSkolem( n[0].getType().getSetElementType() );
+    Node x = NodeManager::currentNM()->mkSkolem("sde_", n[0].getType().getSetElementType() );
     Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
 
     lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
@@ -812,7 +806,6 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_pending(u),
   d_pendingDisequal(u),
   d_pendingEverInserted(u),
-  d_skolemCounter(0),
   d_scrutinize(NULL)
 {
   d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 4f2c3c173..7e9d60905 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -158,11 +158,9 @@ private:
   context::CDQueue <TNode> d_pending;
   context::CDQueue <TNode> d_pendingDisequal;
   context::CDHashSet <Node, NodeHashFunction> d_pendingEverInserted;
-  int d_skolemCounter;
 
   void addToPending(Node n);
   bool isComplete();
-  Node newSkolem(TypeNode);
   Node getLemma();
 
   /** model generation and helper function */