Merge remote-tracking branch 'origin/master' into segfaultfix

17 files changed, 14 insertions, 24 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/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 3d2c29798..e0697735f 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters, Dejan Jovanovic
  ** Minor contributors (to current version): Kshitij Bansal, Liana Hadarean, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 1c66be911..266362ef5 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters, Dejan Jovanovic
  ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
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/options_handlers.h b/src/prop/options_handlers.h
index 31d567ac4..8ed53a3f5 100644
--- a/src/prop/options_handlers.h
+++ b/src/prop/options_handlers.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index cb4a32ee7..82c0bae1a 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: Dejan Jovanovic
  ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Kshitij Bansal, Christopher L. Conway, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 753890087..a5132e3da 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -5,7 +5,7 @@
  ** Major contributors: Dejan Jovanovic
  ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway, Kshitij Bansal, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 18a1dcf68..929b867c9 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters, Liana Hadarean
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index e937c718c..650c05dd4 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Tim King
- ** Minor contributors (to current version): Liana Hadarean
+ ** Minor contributors (to current version): Morgan Deters, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 291609de7..0b419d545 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Liana Hadarean, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/sat_solver_registry.cpp b/src/prop/sat_solver_registry.cpp
index 111cd1836..7867c6cc3 100644
--- a/src/prop/sat_solver_registry.cpp
+++ b/src/prop/sat_solver_registry.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/sat_solver_registry.h b/src/prop/sat_solver_registry.h
index 3a19bdb99..b8173866f 100644
--- a/src/prop/sat_solver_registry.h
+++ b/src/prop/sat_solver_registry.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index 2674c82b1..c47c2b67b 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Morgan Deters, Liana Hadarean, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index c9f19b42e..67325cb18 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: Kshitij Bansal, Morgan Deters
  ** Minor contributors (to current version): Clark Barrett, Christopher L. Conway, Tim King, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 92c81616b..a962f653a 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -5,7 +5,7 @@
  ** Major contributors: Liana Hadarean, Kshitij Bansal, Morgan Deters
  ** Minor contributors (to current version): Christopher L. Conway, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -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)
 {}