Relaxing the throw specifiers for the destructors for Node, TypeNode, the context/ classes, and their subclasses. Fixes compilation issues with clang 3.5 and -std=c++11 'exception specification of overriding function is more lax than base version' for a couple of different classes.

5 files changed, 5 insertions, 5 deletions

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 452172586..923e1d8c5 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -242,7 +242,7 @@ public:
    */
   bool addDisequality(TNode a, TNode b, TNode reason); 
   void getConflict(std::vector<TNode>& conflict);
-  virtual ~InequalityGraph() throw(AssertionException) {}
+  virtual ~InequalityGraph() {}
   /** 
    * Check that the currently asserted disequalities that have not been split on
    * are still true in the current model. 
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 0dc6cc7a1..b78109dfb 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -37,7 +37,7 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Co
   smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
 }
 
-SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException)
+SharedTermsDatabase::~SharedTermsDatabase()
 {
   smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms);
 }
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index c108122ef..cc8959165 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -149,7 +149,7 @@ private:
 public:
 
   SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
-  ~SharedTermsDatabase() throw(AssertionException);
+  ~SharedTermsDatabase();
 
   /**
    * Asserts the equality to the shared terms database,
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 09d348584..f98ad556f 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -97,7 +97,7 @@ void EqualityEngine::init() {
   d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS;
 }
 
-EqualityEngine::~EqualityEngine() throw(AssertionException) {
+EqualityEngine::~EqualityEngine() {
   free(d_triggerDatabase);
 }
 
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 843e7ce7f..18e83bd1a 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -186,7 +186,7 @@ public:
   /**
    * Just a destructor.
    */
-  virtual ~EqualityEngine() throw(AssertionException);
+  virtual ~EqualityEngine();
 
   /**
    * Set the master equality engine for this one. Master engine will get copies of all