Fix compiler warnings in BV-related code (unused vars mostly).

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 46b521e6b198bca50ed8b28406a65264b64caa52..7322cd0faa547f9827b61f5106d9194f3ca6bc95 100644 (file)
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -26,7 +26,6 @@ BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext, const s
 : context::ContextNotifyObj(mainSatContext, false),
   d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
   d_minisatNotify(0),
-  d_solveCount(0),
   d_assertionsCount(0),
   d_assertionsRealCount(mainSatContext, 0),
   d_lastPropagation(mainSatContext, 0),

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 568d89f7fd5e3c7104587268d56ef40e2ff8a44c..f9d0fbd6a50f748b235acaaedd3e9b6b27bde0d8 100644 (file)
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -55,7 +55,6 @@ private:
   BVMinisat::SimpSolver* d_minisat;
   MinisatNotify* d_minisatNotify;
 
-  unsigned d_solveCount;
   unsigned d_assertionsCount;
   context::CDO<unsigned> d_assertionsRealCount;
   context::CDO<unsigned> d_lastPropagation;

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 9a898ebe63221646fd811b84e8a53428c07ec66b..4a67578712998fffb808df0496ee23fea1abcd8c 100644 (file)
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -39,9 +39,6 @@ extern const ReasonId AxiomReasonId;
 
 class InequalityGraph : public context::ContextNotifyObj{
 
-
-  context::Context* d_context;
-
   struct InequalityEdge {
     TermId next;
     ReasonId reason;
@@ -126,7 +123,6 @@ class InequalityGraph : public context::ContextNotifyObj{
 
   context::CDO<bool> d_inConflict;
   std::vector<TNode> d_conflict;
-  bool d_signed; 
 
   ModelValues  d_modelValues;
   void initializeModelValue(TNode node); 
@@ -214,12 +210,10 @@ public:
   
   InequalityGraph(context::Context* c, bool s = false)
     : ContextNotifyObj(c), 
-      d_context(c),
       d_ineqNodes(),
       d_ineqEdges(),
       d_inConflict(c, false),
       d_conflict(),
-      d_signed(s),
       d_modelValues(c),
       d_disequalities(c),
       d_disequalitiesAlreadySplit(),