Address comments from PR #1164. (#1174)

Make eliminateSkolemFunctions(...) iterative and some more minor fixes.

1 files changed, 1 insertions, 6 deletions

diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index ca6c97f83..724b3b7a7 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -42,7 +42,7 @@ class BvInverterStatus {
   BvInverterStatus() : d_status(0) {}
   ~BvInverterStatus() {}
   int d_status;
-  // TODO : may not need this (conditions are now appear explicitly in solved
+  // TODO : may not need this (conditions now appear explicitly in solved
   // forms) side conditions
   std::vector<Node> d_conds;
 };
@@ -111,11 +111,6 @@ class BvInverter {
   Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path,
                    std::unordered_set<TNode, TNodeHashFunction>& visited);
 
-  /** helper function for eliminateSkolemFunctions */
-  Node eliminateSkolemFunctions(
-      TNode n, std::vector<Node>& side_conditions,
-      std::unordered_map<TNode, Node, TNodeHashFunction>& visited);
-
   // is operator k invertible?
   bool isInvertible(Kind k);