4 files changed, 12 insertions, 20 deletions
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 548035aec..e6475b58e 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -234,8 +234,6 @@ std::ostream& operator<<(std::ostream& os, const NodeLog& nl);
 class ApproximateSimplex;
 class TreeLog {
 private:
-  ApproximateSimplex* d_generator;
-
   int next_exec_ord;
   typedef std::map<int, NodeLog> ToNodeMap;
   ToNodeMap d_toNode;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 3e414ca6d..51bbd67f3 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -25,10 +25,6 @@
 namespace CVC4 {
 namespace theory {
 
-namespace quantifiers {
-  class InstStrategySimplex;
-}
-
 namespace arith {
 
 /**
@@ -38,7 +34,6 @@ namespace arith {
  */
 class TheoryArith : public Theory {
 private:
-  friend class quantifiers::InstStrategySimplex;
   friend class TheoryArithPrivate;
 
   TheoryArithPrivate* d_internal;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index e47231128..069d3530c 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2520,34 +2520,37 @@ struct SizeOrd {
     return a.size() < b.size();
   }
 };
-void TheoryArithPrivate::subsumption(std::vector<ConstraintCPVec>& confs) const {
+
+void TheoryArithPrivate::subsumption(
+    std::vector<ConstraintCPVec> &confs) const {
   int checks CVC4_UNUSED = 0;
   int subsumed CVC4_UNUSED = 0;
 
-  for(size_t i =0, N= confs.size(); i < N; ++i){
-    ConstraintCPVec& conf = confs[i];
+  for (size_t i = 0, N = confs.size(); i < N; ++i) {
+    ConstraintCPVec &conf = confs[i];
     std::sort(conf.begin(), conf.end());
   }
 
   std::sort(confs.begin(), confs.end(), SizeOrd());
-  for(size_t i = 0; i < confs.size(); i++){
-    ConstraintCPVec& a = confs[i];
+  for (size_t i = 0; i < confs.size(); i++) {
     // i is not subsumed
-    for(size_t j = i+1; j < confs.size();){
+    for (size_t j = i + 1; j < confs.size();) {
+      ConstraintCPVec& a = confs[i];
       ConstraintCPVec& b = confs[j];
       checks++;
       bool subsumes = std::includes(a.begin(), a.end(), b.begin(), b.end());
-      if(subsumes){
+      if (subsumes) {
         ConstraintCPVec& back = confs.back();
         b.swap(back);
         confs.pop_back();
         subsumed++;
-      }else{
+      } else {
         j++;
       }
     }
   }
-  Debug("arith::subsumption") << "subsumed " << subsumed << "/" << checks << endl;
+  Debug("arith::subsumption") << "subsumed " << subsumed << "/" << checks
+                              << endl;
 }
 
 std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth){
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index edc3a5bc0..ed7efe008 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -70,9 +70,6 @@
 
 namespace CVC4 {
 namespace theory {
-namespace quantifiers {
-  class InstStrategySimplex;
-}
 namespace arith {
 
 class BranchCutInfo;
@@ -93,7 +90,6 @@ class InferBoundsResult;
  */
 class TheoryArithPrivate {
 private:
-  friend class quantifiers::InstStrategySimplex;
 
   static const uint32_t RESET_START = 2;