Fix compiler errors due to unbalanced throw specifiers.

diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h
index 16aa32176fc55978a9f64ee13c261f47698e7438..8c2e4066e38bd78fb41402380017ae16e551a771 100644 (file)
--- 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 b896b03fba9ac9db38dd871e34626effd7631606..53ab2eccff58765010c4cdba120a6d7fccc1475d 100644 (file)
--- 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 a355702bc5201b92d64937ff07f6ee5d9aeae2be..2564572c209b34270eefbf8a6aec0a3282ce621a 100644 (file)
--- 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 fbcaf938f5840ddfc3aab793ac733de32fcd0e28..25d71984d14c29d21d11b80e8651e0e793884a96 100644 (file)
--- 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 47de4e581449c6f1c6fc85baacb8c6709a35ce52..a3d239d185fa1e0da1d1c30c5e907783c1f67aa5 100644 (file)
--- 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