Fix compiler warnings (mostly unused variables).

8 files changed, 5 insertions, 18 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index b4ab57283..37d4c503d 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -416,6 +416,8 @@ bool Expr::isAtomicFormula() const {
     case CVC4::kind::IFF:
     case CVC4::kind::IMPLIES:
       return false;
+    default:
+      ; /* fall through */
   }
   for (Expr::iterator k = begin(), kend=end(); k != kend; ++k) {
     if (!CVC3::Expr(*k).isAtomic()) {
@@ -450,8 +452,9 @@ bool Expr::isBoolConnective() const {
   case CVC4::kind::XOR:
   case CVC4::kind::ITE:
     return true;
+  default:
+    return false;
   }
-  return false;
 }
 
 bool Expr::isPropLiteral() const {
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index ab8a7b2bc..02bc07847 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -86,7 +86,7 @@ class ProofManager {
   VarSet     d_propVars;
 
   Proof* d_fullProof;
-  ProofFormat d_format;
+  ProofFormat d_format; // used for now only in debug builds
 
 protected:
   std::string d_logic;
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index c4fe58fd7..e4956ecc8 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -29,7 +29,6 @@ using namespace CVC4::prop;
 
 MinisatSatSolver::MinisatSatSolver() :
   d_minisat(NULL),
-  d_theoryProxy(NULL),
   d_context(NULL)
 {}
 
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 201879eb0..a919bbcc4 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -30,9 +30,6 @@ class MinisatSatSolver : public DPLLSatSolverInterface {
   /** The SatSolver used */
   Minisat::SimpSolver* d_minisat;
 
-  /** The SatSolver uses this to communicate with the theories */
-  TheoryProxy* d_theoryProxy;
-
   /** Context we will be using to synchronize the sat solver */
   context::Context* d_context;
 
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 92c81616b..f07f5487e 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -57,9 +57,6 @@ class TheoryProxy {
   /** The theory engine we are using */
   TheoryEngine* d_theoryEngine;
 
-  /** Context we will be using to synchronzie the sat solver */
-  context::Context* d_context;
-
   /** Queue of asserted facts */
   context::CDQueue<TNode> d_queue;
 
@@ -135,7 +132,6 @@ inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
   d_cnfStream(cnfStream),
   d_decisionEngine(decisionEngine),
   d_theoryEngine(theoryEngine),
-  d_context(context),
   d_queue(context)
 {}
 
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 3a767b5c3..7669a9914 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -23,7 +23,6 @@ using namespace theory;
 
 SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context)
 : ContextNotifyObj(context)
-, d_context(context)
 , d_statSharedTerms("theory::shared_terms", 0)
 , d_addedSharedTermsSize(context, 0)
 , d_termsToTheories(context)
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index f5724f488..dba904cdf 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -39,9 +39,6 @@ public:
 
 private:
 
-  /** The context */
-  context::Context* d_context;
-
   /** Some statistics */
   IntStat d_statSharedTerms;
 
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 8572a6abd..48b8fa7e8 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -53,9 +53,6 @@ private:
 
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache;
 
-  /** The context within which this SubstitutionMap was constructed. */
-  context::Context* d_context;
-
   /** The variables, in order of addition */
   NodeMap d_substitutions;
 
@@ -98,7 +95,6 @@ private:
 public:
 
   SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) :
-    d_context(context),
     d_substitutions(context),
     d_substitutionCache(),
     d_substituteUnderQuantifiers(substituteUnderQuantifiers),