Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

7 files changed, 8 insertions, 14 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 54e3f2e8b..368a79b80 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -39,7 +39,7 @@ BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Co
 }
 
 
-BVMinisatSatSolver::~BVMinisatSatSolver() throw(AssertionException) {
+BVMinisatSatSolver::~BVMinisatSatSolver() {
   delete d_minisat;
   delete d_minisatNotify;
 }
@@ -309,5 +309,3 @@ void toSatClause< BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_
 }
 
 }
-
-
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 56a7c61e2..732bd0313 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -72,7 +72,7 @@ protected:
 public:
 
   BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = "");
-  ~BVMinisatSatSolver() throw(AssertionException);
+  virtual ~BVMinisatSatSolver();
 
   void setNotify(Notify* notify);
 
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index d8f25a786..eff079cc9 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -45,7 +45,7 @@ CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
 }
 
 
-CryptoMinisatSolver::~CryptoMinisatSolver() throw(AssertionException) {
+CryptoMinisatSolver::~CryptoMinisatSolver() {
   delete d_solver;
 }
 
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 54d52af0e..7ad861def 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -38,7 +38,7 @@ private:
 public:
   CryptoMinisatSolver(StatisticsRegistry* registry,
                       const std::string& name = "");
-  ~CryptoMinisatSolver() throw(AssertionException);
+  virtual ~CryptoMinisatSolver();
 
   ClauseId addClause(SatClause& clause, bool removable);
   ClauseId addXorClause(SatClause& clause, bool rhs, bool removable);
@@ -132,7 +132,3 @@ public:
 } // CVC4
 
 #endif // CVC4_USE_CRYPTOMINISAT
-
-
-
-
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index ff726e299..a88a872c8 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -38,7 +38,7 @@ MinisatSatSolver::MinisatSatSolver(StatisticsRegistry* registry) :
   d_statistics(registry)
 {}
 
-MinisatSatSolver::~MinisatSatSolver() throw()
+MinisatSatSolver::~MinisatSatSolver()
 {
   delete d_minisat;
 }
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index ec5297bb7..1627a6575 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -29,7 +29,7 @@ class MinisatSatSolver : public DPLLSatSolverInterface {
 public:
 
   MinisatSatSolver(StatisticsRegistry* registry);
-  ~MinisatSatSolver() throw();
+  virtual ~MinisatSatSolver();
 ;
 
   static SatVariable     toSatVariable(Minisat::Var var);
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 81fb94242..4afaea5a0 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -43,7 +43,7 @@ class SatSolver {
 public:
 
   /** Virtual destructor */
-  virtual ~SatSolver() throw(AssertionException) { }
+  virtual ~SatSolver() { }
 
   /** Assert a clause in the solver. */
   virtual ClauseId addClause(SatClause& clause,
@@ -99,7 +99,7 @@ public:
 class BVSatSolverInterface: public SatSolver {
 public:
 
-  virtual ~BVSatSolverInterface() throw(AssertionException) {}
+  virtual ~BVSatSolverInterface() {}
   /** Interface for notifications */
   class Notify {
   public: