From bfbe1d5c50547a6040bec1e9f07d47185838aeee Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 21 Jun 2014 21:13:12 -0400
Subject: [PATCH] Fix compiler warnings in BV-related code (unused vars
 mostly).

---
 src/prop/bvminisat/bvminisat.cpp    | 1 -
 src/prop/bvminisat/bvminisat.h      | 1 -
 src/theory/bv/bv_inequality_graph.h | 6 ------
 3 files changed, 8 deletions(-)

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 46b521e6b..7322cd0fa 100644
--- 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 568d89f7f..f9d0fbd6a 100644
--- 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 9a898ebe6..4a6757871 100644
--- 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(),
-- 
2.30.2