5 files changed, 9 insertions, 5 deletions
diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h
index 16aa32176..8c2e4066e 100644
--- a/src/context/cdchunk_list.h
+++ b/src/context/cdchunk_list.h
@@ -136,7 +136,7 @@ protected:
       d_size(size),
       d_sizeAlloc(sizeAlloc) {
     }
-    ~CDChunkListSave() {
+    ~CDChunkListSave() throw() {
       this->destroy();
     }
     ContextObj* save(ContextMemoryManager* pCMM) {
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index b896b03fb..53ab2eccf 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -32,7 +32,8 @@ MinisatSatSolver::MinisatSatSolver() :
   d_context(NULL)
 {}
 
-MinisatSatSolver::~MinisatSatSolver() {
+MinisatSatSolver::~MinisatSatSolver() throw()
+{
   delete d_minisat;
 }
 
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index a355702bc..2564572c2 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -37,7 +37,8 @@ class MinisatSatSolver : public DPLLSatSolverInterface {
 public:
 
   MinisatSatSolver();
-  ~MinisatSatSolver();
+  ~MinisatSatSolver() throw();
+;
 
   static SatVariable     toSatVariable(Minisat::Var var);
   static Minisat::Lit    toMinisatLit(SatLiteral lit);
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index fbcaf938f..25d71984d 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -136,6 +136,7 @@ private:
 //the following functions are for evaluating quantifier bodies
 public:
   FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
+  ~FirstOrderModelIG() throw() {}
   FirstOrderModelIG * asFirstOrderModelIG() { return this; }
   // initialize the model
   void processInitialize( bool ispre );
@@ -218,6 +219,7 @@ private:
   void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
 public:
   FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
+  ~FirstOrderModelAbs() throw() {}
   FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
   void processInitialize( bool ispre );
   unsigned getRepresentativeId( TNode n );
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 47de4e581..a3d239d18 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -123,7 +123,7 @@ protected:  //helper functions
   bool hasConstantDefinition( Node n );
 public:
   QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
-  virtual ~QModelBuilderIG(){}
+  virtual ~QModelBuilderIG() throw() {}
 public:
   //whether to add inst-gen lemmas
   virtual bool optInstGen();
@@ -192,7 +192,7 @@ protected:
   void constructModelUf( FirstOrderModel* fm, Node op );
 public:
   QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
-  ~QModelBuilderDefault(){}
+  ~QModelBuilderDefault() throw() {}
   //options
   bool optReconsiderFuncConstants() { return true; }
   //has inst gen