Removing more miscellaneous throw specifiers. (#1488)

Removing more miscellaneous throw specifiers.

43 files changed, 438 insertions, 430 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 325f44769..4761ba07e 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -176,7 +176,8 @@ InteractiveShell::~InteractiveShell() {
   delete d_parser;
 }
 
-Command* InteractiveShell::readCommand() throw (UnsafeInterruptException) {
+Command* InteractiveShell::readCommand()
+{
   char* lineBuf = NULL;
   string line = "";
 
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index a3834a1e3..049b0649e 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -57,7 +57,7 @@ public:
    * Read a command from the interactive shell. This will read as
    * many lines as necessary to parse a well-formed command.
    */
-  Command* readCommand() throw (UnsafeInterruptException);
+  Command* readCommand();
 
   /**
    * Return the internal parser being used.
diff --git a/src/main/util.cpp b/src/main/util.cpp
index de6b47aa5..7086ea26f 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -345,7 +345,8 @@ void cvc4_init()
   default_terminator = set_terminate(cvc4terminate);
 }
 
-void cvc4_shutdown() throw () {
+void cvc4_shutdown() noexcept
+{
 #ifndef __WIN32__
 #ifdef HAVE_SIGALTSTACK
   free(cvc4StackBase);
diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h
index b036c7e93..874516265 100644
--- a/src/options/base_handlers.h
+++ b/src/options/base_handlers.h
@@ -35,11 +35,10 @@ class comparator {
   double d_dbound;
   bool d_hasLbound;
 
-public:
-  comparator(int i) throw() : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {}
-  comparator(long l) throw() : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {}
-  comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {}
-
+ public:
+  comparator(int i) : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {}
+  comparator(long l) : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {}
+  comparator(double d) : d_lbound(0), d_dbound(d), d_hasLbound(false) {}
   template <class T>
   void operator()(std::string option, const T& value) {
     if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) ||
@@ -52,33 +51,33 @@ public:
 };/* class comparator */
 
 struct greater : public comparator<std::greater> {
-  greater(int i) throw() : comparator<std::greater>(i) {}
-  greater(long l) throw() : comparator<std::greater>(l) {}
-  greater(double d) throw() : comparator<std::greater>(d) {}
+  greater(int i) : comparator<std::greater>(i) {}
+  greater(long l) : comparator<std::greater>(l) {}
+  greater(double d) : comparator<std::greater>(d) {}
 };/* struct greater */
 
 struct greater_equal : public comparator<std::greater_equal> {
-  greater_equal(int i) throw() : comparator<std::greater_equal>(i) {}
-  greater_equal(long l) throw() : comparator<std::greater_equal>(l) {}
-  greater_equal(double d) throw() : comparator<std::greater_equal>(d) {}
+  greater_equal(int i) : comparator<std::greater_equal>(i) {}
+  greater_equal(long l) : comparator<std::greater_equal>(l) {}
+  greater_equal(double d) : comparator<std::greater_equal>(d) {}
 };/* struct greater_equal */
 
 struct less : public comparator<std::less> {
-  less(int i) throw() : comparator<std::less>(i) {}
-  less(long l) throw() : comparator<std::less>(l) {}
-  less(double d) throw() : comparator<std::less>(d) {}
+  less(int i) : comparator<std::less>(i) {}
+  less(long l) : comparator<std::less>(l) {}
+  less(double d) : comparator<std::less>(d) {}
 };/* struct less */
 
 struct less_equal : public comparator<std::less_equal> {
-  less_equal(int i) throw() : comparator<std::less_equal>(i) {}
-  less_equal(long l) throw() : comparator<std::less_equal>(l) {}
-  less_equal(double d) throw() : comparator<std::less_equal>(d) {}
+  less_equal(int i) : comparator<std::less_equal>(i) {}
+  less_equal(long l) : comparator<std::less_equal>(l) {}
+  less_equal(double d) : comparator<std::less_equal>(d) {}
 };/* struct less_equal */
 
 struct not_equal : public comparator<std::not_equal_to> {
-  not_equal(int i) throw() : comparator<std::not_equal_to>(i) {}
-  not_equal(long l) throw() : comparator<std::not_equal_to>(l) {}
-  not_equal(double d) throw() : comparator<std::not_equal_to>(d) {}
+  not_equal(int i) : comparator<std::not_equal_to>(i) {}
+  not_equal(long l) : comparator<std::not_equal_to>(l) {}
+  not_equal(double d) : comparator<std::not_equal_to>(d) {}
 };/* struct not_equal_to */
 
 }/* CVC4::options namespace */
diff --git a/src/options/options.h b/src/options/options.h
index 474ef0f96..ce0e3c347 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -302,7 +302,7 @@ public:
    * to the given name.  Returns an empty string if there are no
    * suggestions.
    */
-  static std::string suggestCommandLineOptions(const std::string& optionName) throw();
+  static std::string suggestCommandLineOptions(const std::string& optionName);
 
   /**
    * Look up SMT option names that bear some similarity to
@@ -310,7 +310,8 @@ public:
    * useful in case of typos.  Can return an empty vector if there are
    * no suggestions.
    */
-  static std::vector<std::string> suggestSmtOptions(const std::string& optionName) throw();
+  static std::vector<std::string> suggestSmtOptions(
+      const std::string& optionName);
 
   /**
    * Initialize the Options object options based on the given
@@ -329,8 +330,7 @@ public:
   /**
    * Get the setting for all options.
    */
-  std::vector< std::vector<std::string> > getOptions() const throw();
-
+  std::vector<std::vector<std::string> > getOptions() const;
 
   /**
    * Registers a listener for the notification, notifyBeforeSearch.
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 4fb6357bd..583f79d2d 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1361,7 +1361,8 @@ SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode(
   }
 }
 
-void OptionsHandler::setProduceAssertions(std::string option, bool value) throw() {
+void OptionsHandler::setProduceAssertions(std::string option, bool value)
+{
   options::produceAssertions.set(value);
   options::interactiveMode.set(value);
 }
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 9d5f8cc6e..eef4c9b61 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -146,7 +146,7 @@ public:
   SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException);
   SygusSolutionOutMode stringToSygusSolutionOutMode(
       std::string option, std::string optarg) throw(OptionException);
-  void setProduceAssertions(std::string option, bool value) throw();
+  void setProduceAssertions(std::string option, bool value);
   void proofEnabledBuild(std::string option, bool value) throw(OptionException);
   void LFSCEnabledBuild(std::string option, bool value);
   void notifyDumpToFile(std::string option);
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index a48b22625..9de47b388 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -787,7 +787,8 @@ ${all_modules_option_handlers}
   free(argv);
 }
 
-std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() {
+std::string Options::suggestCommandLineOptions(const std::string& optionName)
+{
   DidYouMean didYouMean;
 
   const char* opt;
@@ -804,7 +805,9 @@ static const char* smtOptions[] = {
   NULL
 };/* smtOptions[] */
 
-std::vector<std::string> Options::suggestSmtOptions(const std::string& optionName) throw() {
+std::vector<std::string> Options::suggestSmtOptions(
+    const std::string& optionName)
+{
   std::vector<std::string> suggestions;
 
   const char* opt;
@@ -817,7 +820,8 @@ std::vector<std::string> Options::suggestSmtOptions(const std::string& optionNam
   return suggestions;
 }
 
-std::vector< std::vector<std::string> > Options::getOptions() const throw() {
+std::vector<std::vector<std::string> > Options::getOptions() const
+{
   std::vector< std::vector<std::string> > opts;
 
   ${all_modules_get_options}
diff --git a/src/options/theoryof_mode.cpp b/src/options/theoryof_mode.cpp
index 9eb2be178..3fe7db532 100644
--- a/src/options/theoryof_mode.cpp
+++ b/src/options/theoryof_mode.cpp
@@ -19,19 +19,17 @@
 #include "options/theoryof_mode.h"
 
 #include <ostream>
-#include "base/cvc4_assert.h"
 
 namespace CVC4 {
 namespace theory {
 
-std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() {
+std::ostream& operator<<(std::ostream& out, TheoryOfMode m)
+{
   switch(m) {
   case THEORY_OF_TYPE_BASED: return out << "THEORY_OF_TYPE_BASED";
   case THEORY_OF_TERM_BASED: return out << "THEORY_OF_TERM_BASED";
   default: return out << "TheoryOfMode!UNKNOWN";
   }
-
-  Unreachable();
 }
 
 }/* CVC4::theory namespace */
diff --git a/src/options/theoryof_mode.h b/src/options/theoryof_mode.h
index f999a6081..d1306defd 100644
--- a/src/options/theoryof_mode.h
+++ b/src/options/theoryof_mode.h
@@ -31,7 +31,7 @@ enum TheoryOfMode {
   THEORY_OF_TERM_BASED
 };/* enum TheoryOfMode */
 
-std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, TheoryOfMode m) CVC4_PUBLIC;
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h
index 4a08838fe..deefb02cf 100644
--- a/src/theory/arrays/static_fact_manager.h
+++ b/src/theory/arrays/static_fact_manager.h
@@ -45,7 +45,6 @@ namespace arrays {
 
 public:
   StaticFactManager() {}
-  ~StaticFactManager() throw() { }
 
   /**
    * Return a Node's union-find representative, doing path compression.
diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h
index eb60f339b..3028eaf17 100644
--- a/src/theory/arrays/union_find.h
+++ b/src/theory/arrays/union_find.h
@@ -56,14 +56,12 @@ class UnionFind : context::ContextNotifyObj {
   /** Our current offset in the d_trace stack (context-dependent). */
   context::CDO<size_t> d_offset;
 
-public:
+ public:
   UnionFind(context::Context* ctxt) :
     context::ContextNotifyObj(ctxt),
     d_offset(ctxt, 0) {
   }
 
-  ~UnionFind() throw() { }
-
   /**
    * Return a Node's union-find representative, doing path compression.
    */
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 0e7614221..33dd4387e 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -180,7 +180,7 @@ public:
   bool hasBBAtom(TNode atom) const; 
 
   TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
-  ~TLazyBitblaster() throw();
+  ~TLazyBitblaster();
   /**
    * Pushes the assumption literal associated with node to the SAT
    * solver assumption queue. 
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 831b767e0..d108a37f0 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -71,7 +71,8 @@ void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
   d_abstraction = abs;
 }
 
-TLazyBitblaster::~TLazyBitblaster() throw() {
+TLazyBitblaster::~TLazyBitblaster()
+{
   delete d_cnfStream;
   delete d_nullRegistrar;
   delete d_nullContext;
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index a27d3a64e..718121499 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -49,15 +49,13 @@ public:
     return utils::mkConst(d_size, d_bits);
   }
 
-  BitVectorEnumerator& operator++() throw() {
+  BitVectorEnumerator& operator++()
+  {
     d_bits += 1;
     return *this;
   }
 
-  bool isFinished() throw() {
-    return d_bits != d_bits.modByPow2(d_size);
-  }
-
+  bool isFinished() { return d_bits != d_bits.modByPow2(d_size); }
 };/* BitVectorEnumerator */
 
 }/* CVC4::theory::bv namespace */
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index cc8cee481..317795f0d 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -44,15 +44,13 @@ class LemmaStatus {
       : d_rewrittenLemma(rewrittenLemma), d_level(level) {}
 
   /** Get the T-rewritten form of the lemma. */
-  TNode getRewrittenLemma() const throw() { return d_rewrittenLemma; }
-
+  TNode getRewrittenLemma() const { return d_rewrittenLemma; }
   /**
    * Get the user-level at which the lemma resides.  After this user level
    * is popped, the lemma is un-asserted from the SAT layer.  This level
    * will be 0 if the lemma didn't reach the SAT layer at all.
    */
-  unsigned getLevel() const throw() { return d_level; }
-
+  unsigned getLevel() const { return d_level; }
  private:
   Node d_rewrittenLemma;
   unsigned d_level;
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 89cd8b6a8..c451f0489 100644
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -89,11 +89,13 @@ private:
   bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n );
 public:
   AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
-  ~AbsMbqiBuilder() throw() {}
+
   //process build model
-  bool processBuildModel(TheoryModel* m);
+  bool processBuildModel(TheoryModel* m) override;
   //do exhaustive instantiation
-  int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
+  int doExhaustiveInstantiation(FirstOrderModel* fm,
+                                Node q,
+                                int effort) override;
 };
 
 }
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index dd71ef56e..4662d7c4c 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -61,25 +61,26 @@ public:
 
 /** candidate generator queue (for manual candidate generation) */
 class CandidateGeneratorQueue : public CandidateGenerator {
-private:
+ private:
   std::vector< Node > d_candidates;
   int d_candidate_index;
-public:
+
+ public:
   CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){}
-  ~CandidateGeneratorQueue() throw() {}
 
-  void addCandidate( Node n );
+  void addCandidate(Node n) override;
 
-  void resetInstantiationRound(){}
-  void reset( Node eqc );
-  Node getNextCandidate();
+  void resetInstantiationRound() override {}
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
 };/* class CandidateGeneratorQueue */
 
 //the default generator
 class CandidateGeneratorQE : public CandidateGenerator
 {
   friend class CandidateGeneratorQEDisequal;
-private:
+
+ private:
   //operator you are looking for
   Node d_op;
   //the equality class iterator
@@ -102,56 +103,56 @@ private:
   bool isLegalOpCandidate( Node n );
   Node d_n;
   std::map< Node, bool > d_exclude_eqc;
-public:
+
+ public:
   CandidateGeneratorQE( QuantifiersEngine* qe, Node pat );
-  ~CandidateGeneratorQE() throw() {}
 
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
   void excludeEqc( Node r ) { d_exclude_eqc[r] = true; }
   bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); }
 };
 
 class CandidateGeneratorQELitEq : public CandidateGenerator
 {
-private:
+ private:
   //the equality classes iterator
   eq::EqClassesIterator d_eq;
   //equality you are trying to match equalities for
   Node d_match_pattern;
   Node d_match_gterm;
   bool d_do_mgt;
-public:
+
+ public:
   CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQELitEq() throw() {}
 
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
 };
 
 class CandidateGeneratorQELitDeq : public CandidateGenerator
 {
-private:
+ private:
   //the equality class iterator for false
   eq::EqClassIterator d_eqc_false;
   //equality you are trying to match disequalities for
   Node d_match_pattern;
   //type of disequality
   TypeNode d_match_pattern_type;
-public:
+
+ public:
   CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQELitDeq() throw() {}
 
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
 };
 
 class CandidateGeneratorQEAll : public CandidateGenerator
 {
-private:
+ private:
   //the equality classes iterator
   eq::EqClassesIterator d_eq;
   //equality you are trying to match equalities for
@@ -162,13 +163,13 @@ private:
   unsigned d_index;
   //first time
   bool d_firstTime;
-public:
+
+ public:
   CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQEAll() throw() {}
 
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
 };
 
 }/* CVC4::theory::inst namespace */
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index fa74795c3..85a7d3eb4 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -399,7 +399,7 @@ private:  //information about ground equivalence classes
   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
 public:
   ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
-  ~ConjectureGenerator() throw() {}
+
   /* needs check */
   bool needsCheck( Theory::Effort e );
   /* reset at a round */
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 6749a8c0d..e7070b469 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -836,7 +836,8 @@ FirstOrderModel(qe, c, name){
 
 }
 
-FirstOrderModelFmc::~FirstOrderModelFmc() throw() {
+FirstOrderModelFmc::~FirstOrderModelFmc()
+{
   for(std::map<Node, Def*>::iterator i = d_models.begin(); i != d_models.end(); ++i) {
     delete (*i).second;
   }
@@ -1004,7 +1005,8 @@ FirstOrderModel(qe, c, name) {
 
 }
 
-FirstOrderModelAbs::~FirstOrderModelAbs() throw() {
+FirstOrderModelAbs::~FirstOrderModelAbs()
+{
   for(std::map<Node, AbsDef*>::iterator i = d_models.begin(); i != d_models.end(); ++i) {
     delete (*i).second;
   }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 57582a856..0c4b6b7a4 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -93,7 +93,7 @@ class FirstOrderModel : public TheoryModel
 {
  public:
   FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
-  virtual ~FirstOrderModel() throw() {}
+
   virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; }
   virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
   virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; }
@@ -214,7 +214,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 );
@@ -257,7 +257,7 @@ private:
   void processInitializeModelForTerm(Node n);
 public:
   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
-  virtual ~FirstOrderModelFmc() throw();
+  ~FirstOrderModelFmc() override;
   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
   // initialize the model
   void processInitialize( bool ispre );
@@ -277,24 +277,26 @@ class AbsDef;
 
 class FirstOrderModelAbs : public FirstOrderModel
 {
-public:
+ public:
   std::map< Node, AbsDef * > d_models;
   std::map< Node, bool > d_models_valid;
   std::map< TNode, unsigned > d_rep_id;
   std::map< TypeNode, unsigned > d_domain;
   std::map< Node, std::vector< int > > d_var_order;
   std::map< Node, std::map< int, int > > d_var_index;
-private:
+
+ private:
   /** get current model value */
-  void processInitializeModelForTerm(Node n);
-  void processInitializeQuantifier( Node q );
+  void processInitializeModelForTerm(Node n) override;
+  void processInitializeQuantifier(Node q) override;
   void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
   TNode getUsedRepresentative( TNode n );
-public:
+
+ public:
   FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
-  ~FirstOrderModelAbs() throw();
-  FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
-  void processInitialize( bool ispre );
+  ~FirstOrderModelAbs() override;
+  FirstOrderModelAbs* asFirstOrderModelAbs() override { return this; }
+  void processInitialize(bool ispre) override;
   unsigned getRepresentativeId( TNode n );
   bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
   Node getFunctionValue(Node op, const char* argPrefix );
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index c5d005969..f6d16dc03 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -134,7 +134,6 @@ private:
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 public:
   FullModelChecker( context::Context* c, QuantifiersEngine* qe );
-  ~FullModelChecker() throw() {}
 
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 884ed29f5..46ae8aa84 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -59,7 +59,8 @@ InstMatchGenerator::InstMatchGenerator() {
   d_independent_gen = false;
 }
 
-InstMatchGenerator::~InstMatchGenerator() throw() {
+InstMatchGenerator::~InstMatchGenerator()
+{
   for( unsigned i=0; i<d_children.size(); i++ ){
     delete d_children[i];
   }
@@ -692,10 +693,6 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto
   }
 }
 
-InstMatchGeneratorMultiLinear::~InstMatchGeneratorMultiLinear() throw() {
-
-}
-
 int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){
   for( unsigned i=0; i<d_children.size(); i++ ){
     if( !d_children[i]->reset( Node::null(), qe ) ){
@@ -814,7 +811,8 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q,
   }
 }
 
-InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() {
+InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
+{
   for( unsigned i=0; i<d_children.size(); i++ ){
     delete d_children[i];
   }
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 95faf0279..fc913c7cf 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -191,231 +191,231 @@ class CandidateGenerator;
 * ground terms not in the equivalence class of b.
 */
 class InstMatchGenerator : public IMGenerator {
-public:
- /** destructor */
- virtual ~InstMatchGenerator() throw();
+ public:
+  /** destructor */
+  ~InstMatchGenerator() override;
 
- /** Reset instantiation round. */
- void resetInstantiationRound(QuantifiersEngine* qe) override;
- /** Reset. */
- bool reset(Node eqc, QuantifiersEngine* qe) override;
- /** Get the next match. */
- int getNextMatch(Node q,
-                  InstMatch& m,
-                  QuantifiersEngine* qe,
-                  Trigger* tparent) override;
- /** Add instantiations. */
- int addInstantiations(Node q,
-                       QuantifiersEngine* qe,
-                       Trigger* tparent) override;
+  /** Reset instantiation round. */
+  void resetInstantiationRound(QuantifiersEngine* qe) override;
+  /** Reset. */
+  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  /** Get the next match. */
+  int getNextMatch(Node q,
+                   InstMatch& m,
+                   QuantifiersEngine* qe,
+                   Trigger* tparent) override;
+  /** Add instantiations. */
+  int addInstantiations(Node q,
+                        QuantifiersEngine* qe,
+                        Trigger* tparent) override;
 
- /** set active add flag (true by default)
-  *
- * If active add is true, we call sendInstantiation in calls to getNextMatch,
- * instead of returning the match. This is necessary so that we can ensure
- * policies that are dependent upon knowing when instantiations are
- * successfully added to the output channel through
- * Instantiate::addInstantiation(...).
- */
- void setActiveAdd(bool val);
- /** Get active score for this inst match generator
-  *
-  * See Trigger::getActiveScore for details.
+  /** set active add flag (true by default)
+   *
+  * If active add is true, we call sendInstantiation in calls to getNextMatch,
+  * instead of returning the match. This is necessary so that we can ensure
+  * policies that are dependent upon knowing when instantiations are
+  * successfully added to the output channel through
+  * Instantiate::addInstantiation(...).
   */
- int getActiveScore(QuantifiersEngine* qe);
- /** exclude match
-  *
-  * Exclude matching d_match_pattern with Node n on subsequent calls to
-  * getNextMatch.
+  void setActiveAdd(bool val);
+  /** Get active score for this inst match generator
+   *
+   * See Trigger::getActiveScore for details.
+   */
+  int getActiveScore(QuantifiersEngine* qe);
+  /** exclude match
+   *
+   * Exclude matching d_match_pattern with Node n on subsequent calls to
+   * getNextMatch.
+   */
+  void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
+  /** Get current match.
+   * Returns the term we are currently matching.
+   */
+  Node getCurrentMatch() { return d_curr_matched; }
+  /** set that this match generator is independent
+   *
+  * A match generator is indepndent when this generator fails to produce a
+  * match in a call to getNextMatch, the overall matching fails.
   */
- void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
- /** Get current match.
-  * Returns the term we are currently matching.
+  void setIndependent() { d_independent_gen = true; }
+  //-------------------------------construction of inst match generators
+  /** mkInstMatchGenerator for single triggers, calls the method below */
+  static InstMatchGenerator* mkInstMatchGenerator(Node q,
+                                                  Node pat,
+                                                  QuantifiersEngine* qe);
+  /** mkInstMatchGenerator for the multi trigger case
+  *
+  * This linked list of InstMatchGenerator classes with one
+  * InstMatchGeneratorMultiLinear at the head and a list of trailing
+  * InstMatchGenerators corresponding to each unique subterm of pats with
+  * free variables.
   */
- Node getCurrentMatch() { return d_curr_matched; }
- /** set that this match generator is independent
+  static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q,
+                                                       std::vector<Node>& pats,
+                                                       QuantifiersEngine* qe);
+  /** mkInstMatchGenerator
   *
- * A match generator is indepndent when this generator fails to produce a
- * match in a call to getNextMatch, the overall matching fails.
- */
- void setIndependent() { d_independent_gen = true; }
- //-------------------------------construction of inst match generators
- /** mkInstMatchGenerator for single triggers, calls the method below */
- static InstMatchGenerator* mkInstMatchGenerator(Node q,
-                                                 Node pat,
-                                                 QuantifiersEngine* qe);
- /** mkInstMatchGenerator for the multi trigger case
- *
- * This linked list of InstMatchGenerator classes with one
- * InstMatchGeneratorMultiLinear at the head and a list of trailing
- * InstMatchGenerators corresponding to each unique subterm of pats with
- * free variables.
- */
- static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q,
-                                                      std::vector<Node>& pats,
-                                                      QuantifiersEngine* qe);
- /** mkInstMatchGenerator
- *
- * This generates a linked list of InstMatchGenerators for each unique
- * subterm of pats with free variables.
- *
- * q is the quantified formula associated with the generator we are making
- * pats is a set of terms we are making InstMatchGenerator nodes for
- * qe is a pointer to the quantifiers engine (used for querying necessary
- * information during initialization) pat_map_init maps from terms to
- * generators we have already made for them.
- *
- * It calls initialize(...) for all InstMatchGenerators generated by this call.
- */
- static InstMatchGenerator* mkInstMatchGenerator(
-     Node q,
-     std::vector<Node>& pats,
-     QuantifiersEngine* qe,
-     std::map<Node, InstMatchGenerator*>& pat_map_init);
- //-------------------------------end construction of inst match generators
-
-protected:
- /** constructors
+  * This generates a linked list of InstMatchGenerators for each unique
+  * subterm of pats with free variables.
   *
- * These are intentionally private, and are called during linked list
- * construction in mkInstMatchGenerator.
- */
- InstMatchGenerator(Node pat);
- InstMatchGenerator();
- /** The pattern we are producing matches for.
+  * q is the quantified formula associated with the generator we are making
+  * pats is a set of terms we are making InstMatchGenerator nodes for
+  * qe is a pointer to the quantifiers engine (used for querying necessary
+  * information during initialization) pat_map_init maps from terms to
+  * generators we have already made for them.
   *
- * This term and d_match_pattern can be different since this
- * term may involve  information regarding phase and (dis)equality entailment,
- * or other special cases of Triggers.
- *
- * For example, for the trigger for P( x ) = false, which matches P( x ) with
- * P( t ) in the equivalence class of false,
- *   P( x ) = false is d_pattern
- *   P( x ) is d_match_pattern
- * Another example, for pure theory triggers like head( x ), we have
- *   head( x ) is d_pattern
- *   x is d_match_pattern
- * since head( x ) can match any (List) datatype term x.
- *
- * If null, this is a multi trigger that is merging matches from d_children,
- * which is used in InstMatchGeneratorMulti.
- */
- Node d_pattern;
- /** The match pattern
-  * This is the term that is matched against ground terms,
-  * see examples above.
-  */
- Node d_match_pattern;
- /** The current term we are matching. */
- Node d_curr_matched;
- /** do we need to call reset on this generator? */
- bool d_needsReset;
- /** candidate generator
-  * This is the back-end utility for InstMatchGenerator.
-  * It generates a stream of candidate terms to match against d_match_pattern
-  * below, dependending upon what kind of term we are matching
-  * (e.g. a matchable term, a variable, a relation, etc.).
+  * It calls initialize(...) for all InstMatchGenerators generated by this call.
   */
- CandidateGenerator* d_cg;
- /** children generators
-  * These match generators correspond to the children of the term
-  * we are matching with this generator.
-  * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
-  * in the example (EX1) above.
-  */
- std::vector<InstMatchGenerator*> d_children;
- /** for each child, the index in the term
-  * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
-  * in the example (EX1) above, indicating it is the 2nd child
-  * of the term.
+  static InstMatchGenerator* mkInstMatchGenerator(
+      Node q,
+      std::vector<Node>& pats,
+      QuantifiersEngine* qe,
+      std::map<Node, InstMatchGenerator*>& pat_map_init);
+  //-------------------------------end construction of inst match generators
+
+ protected:
+  /** constructors
+   *
+  * These are intentionally private, and are called during linked list
+  * construction in mkInstMatchGenerator.
   */
- std::vector<int> d_children_index;
- /** children types
+  InstMatchGenerator(Node pat);
+  InstMatchGenerator();
+  /** The pattern we are producing matches for.
+   *
+  * This term and d_match_pattern can be different since this
+  * term may involve  information regarding phase and (dis)equality entailment,
+  * or other special cases of Triggers.
   *
-  * If d_match_pattern is an instantiation constant, then this is a singleton
-  * vector containing the variable number of the d_match_pattern itself.
-  * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
-  * index i, d_children[i] stores the type of node ti is, where:
-  *   >= 0 : variable (indicates its number),
-  *   -1 : ground term,
-  *   -2 : child term.
-  */
- std::vector<int> d_children_types;
- /** The next generator in the linked list
-  * that this generator is a part of.
-  */
- InstMatchGenerator* d_next;
- /** The equivalence class we are currently matching in. */
- Node d_eq_class;
- /** If non-null, then this is a relational trigger of the form x ~
-  * d_eq_class_rel. */
- Node d_eq_class_rel;
- /** Excluded matches
- * Stores the terms we are not allowed to match.
- * These can for instance be specified by the smt2
- * extended syntax (! ... :no-pattern).
- */
- std::map<Node, bool> d_curr_exclude_match;
- /** Current first candidate
- * Used in a key fail-quickly optimization which generates
- * the first candidate term to match during reset().
- */
- Node d_curr_first_candidate;
- /** Indepdendent generate
- * If this flag is true, failures to match should be cached.
- */
- bool d_independent_gen;
- /** active add flag, described above. */
- bool d_active_add;
- /** cached value of d_match_pattern.getType() */
- TypeNode d_match_pattern_type;
- /** the match operator for d_match_pattern
+  * For example, for the trigger for P( x ) = false, which matches P( x ) with
+  * P( t ) in the equivalence class of false,
+  *   P( x ) = false is d_pattern
+  *   P( x ) is d_match_pattern
+  * Another example, for pure theory triggers like head( x ), we have
+  *   head( x ) is d_pattern
+  *   x is d_match_pattern
+  * since head( x ) can match any (List) datatype term x.
   *
-  * See TermDatabase::getMatchOperator for details on match operators.
+  * If null, this is a multi trigger that is merging matches from d_children,
+  * which is used in InstMatchGeneratorMulti.
   */
- Node d_match_pattern_op;
- /** get the match against ground term or formula t.
-  *
-  * d_match_pattern and t should have the same shape, that is,
-  * their match operator (see TermDatabase::getMatchOperator) is the same.
-  * only valid for use where !d_match_pattern.isNull().
+  Node d_pattern;
+  /** The match pattern
+   * This is the term that is matched against ground terms,
+   * see examples above.
+   */
+  Node d_match_pattern;
+  /** The current term we are matching. */
+  Node d_curr_matched;
+  /** do we need to call reset on this generator? */
+  bool d_needsReset;
+  /** candidate generator
+   * This is the back-end utility for InstMatchGenerator.
+   * It generates a stream of candidate terms to match against d_match_pattern
+   * below, dependending upon what kind of term we are matching
+   * (e.g. a matchable term, a variable, a relation, etc.).
+   */
+  CandidateGenerator* d_cg;
+  /** children generators
+   * These match generators correspond to the children of the term
+   * we are matching with this generator.
+   * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
+   * in the example (EX1) above.
+   */
+  std::vector<InstMatchGenerator*> d_children;
+  /** for each child, the index in the term
+   * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
+   * in the example (EX1) above, indicating it is the 2nd child
+   * of the term.
+   */
+  std::vector<int> d_children_index;
+  /** children types
+   *
+   * If d_match_pattern is an instantiation constant, then this is a singleton
+   * vector containing the variable number of the d_match_pattern itself.
+   * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
+   * index i, d_children[i] stores the type of node ti is, where:
+   *   >= 0 : variable (indicates its number),
+   *   -1 : ground term,
+   *   -2 : child term.
+   */
+  std::vector<int> d_children_types;
+  /** The next generator in the linked list
+   * that this generator is a part of.
+   */
+  InstMatchGenerator* d_next;
+  /** The equivalence class we are currently matching in. */
+  Node d_eq_class;
+  /** If non-null, then this is a relational trigger of the form x ~
+   * d_eq_class_rel. */
+  Node d_eq_class_rel;
+  /** Excluded matches
+  * Stores the terms we are not allowed to match.
+  * These can for instance be specified by the smt2
+  * extended syntax (! ... :no-pattern).
   */
- int getMatch(
-     Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent);
- /** Initialize this generator.
-  *
-  * q is the quantified formula associated with this generator.
-  *
-  * This constructs the appropriate information about what
-  * patterns we are matching and children generators.
-  *
-  * It may construct new (child) generators needed to implement
-  * the matching algorithm for this term. For each new generator
-  * constructed in this way, it adds them to gens.
+  std::map<Node, bool> d_curr_exclude_match;
+  /** Current first candidate
+  * Used in a key fail-quickly optimization which generates
+  * the first candidate term to match during reset().
   */
- void initialize(Node q,
-                 QuantifiersEngine* qe,
-                 std::vector<InstMatchGenerator*>& gens);
- /** Continue next match
-  *
- * This is called during getNextMatch when the current generator in the linked
- * list succesfully satisfies its matching constraint. This function either
- * calls getNextMatch of the next element in the linked list, or finalizes the
- * match (calling sendInstantiation(...) if active add is true, or returning a
- * value >0 if active add is false).  Its return value has the same semantics
- * as getNextMatch.
- */
- int continueNextMatch(Node q,
-                       InstMatch& m,
-                       QuantifiersEngine* qe,
-                       Trigger* tparent);
- /** Get inst match generator
-  *
-  * Gets the InstMatchGenerator that implements the
-  * appropriate matching algorithm for n within q
-  * within a linked list of InstMatchGenerators.
+  Node d_curr_first_candidate;
+  /** Indepdendent generate
+  * If this flag is true, failures to match should be cached.
   */
- static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
+  bool d_independent_gen;
+  /** active add flag, described above. */
+  bool d_active_add;
+  /** cached value of d_match_pattern.getType() */
+  TypeNode d_match_pattern_type;
+  /** the match operator for d_match_pattern
+   *
+   * See TermDatabase::getMatchOperator for details on match operators.
+   */
+  Node d_match_pattern_op;
+  /** get the match against ground term or formula t.
+   *
+   * d_match_pattern and t should have the same shape, that is,
+   * their match operator (see TermDatabase::getMatchOperator) is the same.
+   * only valid for use where !d_match_pattern.isNull().
+   */
+  int getMatch(
+      Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent);
+  /** Initialize this generator.
+   *
+   * q is the quantified formula associated with this generator.
+   *
+   * This constructs the appropriate information about what
+   * patterns we are matching and children generators.
+   *
+   * It may construct new (child) generators needed to implement
+   * the matching algorithm for this term. For each new generator
+   * constructed in this way, it adds them to gens.
+   */
+  void initialize(Node q,
+                  QuantifiersEngine* qe,
+                  std::vector<InstMatchGenerator*>& gens);
+  /** Continue next match
+   *
+  * This is called during getNextMatch when the current generator in the linked
+  * list succesfully satisfies its matching constraint. This function either
+  * calls getNextMatch of the next element in the linked list, or finalizes the
+  * match (calling sendInstantiation(...) if active add is true, or returning a
+  * value >0 if active add is false).  Its return value has the same semantics
+  * as getNextMatch.
+  */
+  int continueNextMatch(Node q,
+                        InstMatch& m,
+                        QuantifiersEngine* qe,
+                        Trigger* tparent);
+  /** Get inst match generator
+   *
+   * Gets the InstMatchGenerator that implements the
+   * appropriate matching algorithm for n within q
+   * within a linked list of InstMatchGenerators.
+   */
+  static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
 };/* class InstMatchGenerator */
 
 /** match generator for Boolean term ITEs
@@ -424,7 +424,7 @@ protected:
 class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
 public:
   VarMatchGeneratorBooleanTerm( Node var, Node comp );
-  virtual ~VarMatchGeneratorBooleanTerm() throw() {}
+
   /** Reset */
   bool reset(Node eqc, QuantifiersEngine* qe) override
   {
@@ -451,7 +451,7 @@ public:
 class VarMatchGeneratorTermSubs : public InstMatchGenerator {
 public:
   VarMatchGeneratorTermSubs( Node var, Node subs );
-  virtual ~VarMatchGeneratorTermSubs() throw() {}
+
   /** Reset */
   bool reset(Node eqc, QuantifiersEngine* qe) override
   {
@@ -515,9 +515,6 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator {
   friend class InstMatchGenerator;
 
  public:
-  /** destructor */
-  virtual ~InstMatchGeneratorMultiLinear() throw();
-
   /** Reset. */
   bool reset(Node eqc, QuantifiersEngine* qe) override;
   /** Get the next match. */
@@ -552,7 +549,7 @@ class InstMatchGeneratorMulti : public IMGenerator {
                           std::vector<Node>& pats,
                           QuantifiersEngine* qe);
   /** destructor */
-  virtual ~InstMatchGeneratorMulti() throw();
+  ~InstMatchGeneratorMulti() override;
 
   /** Reset instantiation round. */
   void resetInstantiationRound(QuantifiersEngine* qe) override;
@@ -641,8 +638,7 @@ class InstMatchGeneratorSimple : public IMGenerator {
  public:
   /** constructors */
   InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe);
-  /** destructor */
-  ~InstMatchGeneratorSimple() throw() {}
+
   /** Reset instantiation round. */
   void resetInstantiationRound(QuantifiersEngine* qe) override;
   /** Add instantiations. */
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index bd2b8e78e..70dc9c4e9 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -48,8 +48,6 @@ d_nested_qe_waitlist_proc( qe->getUserContext() )
   d_qid_count = 0;
 }
 
-InstStrategyCbqi::~InstStrategyCbqi() throw(){}
-
 bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
   return e>=Theory::EFFORT_LAST_CALL;
 }
@@ -673,7 +671,8 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe )
   d_check_vts_lemma_lc = false;
 }
 
-InstStrategyCegqi::~InstStrategyCegqi() throw () {
+InstStrategyCegqi::~InstStrategyCegqi()
+{
   delete d_out;
 
   for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(),
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 0b23de10d..c2520a973 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -35,7 +35,8 @@ namespace quantifiers {
 class InstStrategyCbqi : public QuantifiersModule {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
-protected:
+
+ protected:
   bool d_cbqi_set_quant_inactive;
   bool d_incomplete_check;
   /** whether we have added cbqi lemma */
@@ -64,7 +65,8 @@ protected:
   /** process functions */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   virtual void process( Node q, Theory::Effort effort, int e ) = 0;
-protected:
+
+ protected:
   //for identification
   uint64_t d_qid_count;
   //nested qe map
@@ -90,12 +92,14 @@ protected:
   NodeIntMap d_nested_qe_waitlist_size;
   NodeIntMap d_nested_qe_waitlist_proc;
   std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
-public:
+
+ public:
   //do nested quantifier elimination
   Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts );
-public:
+
+ public:
   InstStrategyCbqi( QuantifiersEngine * qe );
-  ~InstStrategyCbqi() throw();
+
   /** whether to do CBQI for quantifier q */
   bool doCbqi( Node q );
   /** process functions */
@@ -138,7 +142,7 @@ protected:
   void registerCounterexampleLemma( Node q, Node lem );
 public:
   InstStrategyCegqi( QuantifiersEngine * qe );
-  ~InstStrategyCegqi() throw();
+  ~InstStrategyCegqi() override;
 
   bool doAddInstantiation( std::vector< Node >& subs );
   bool isEligibleForInstantiation( Node n );
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 73e2937ab..511aebf3b 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -38,7 +38,7 @@ protected:
   unsigned d_triedLemmas;
 public:
   QModelBuilder( context::Context* c, QuantifiersEngine* qe );
-  virtual ~QModelBuilder() throw() {}
+
   //do exhaustive instantiation  
   // 0 :  failed, but resorting to true exhaustive instantiation may work
   // >0 : success
@@ -77,7 +77,8 @@ public:
 class QModelBuilderIG : public QModelBuilder
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
-protected:
+
+ protected:
   BoolMap d_basisNoMatch;
   //map from operators to model preference data
   std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
@@ -87,7 +88,8 @@ protected:
   bool d_didInstGen;
   /** process build model */
   virtual bool processBuildModel( TheoryModel* m );
-protected:
+
+ protected:
   //reset
   virtual void reset( FirstOrderModel* fm ) = 0;
   //initialize quantifiers, return number of lemmas produced
@@ -100,20 +102,23 @@ protected:
   virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0;
   //theory-specific build models
   virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0;
-protected:
+
+ protected:
   //map from quantifiers to if are SAT
   //std::map< Node, bool > d_quant_sat;
   //which quantifiers have been initialized
   std::map< Node, bool > d_quant_basis_match_added;
   //map from quantifiers to model basis match
   std::map< Node, InstMatch > d_quant_basis_match;
-protected:  //helper functions
+
+ protected:  // helper functions
   /** term has constant definition */
   bool hasConstantDefinition( Node n );
-public:
+
+ public:
   QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
-  virtual ~QModelBuilderIG() throw() {}
-public:
+
+ public:
   /** statistics class */
   class Statistics {
   public:
@@ -152,8 +157,8 @@ public:
 
 class QModelBuilderDefault : public QModelBuilderIG
 {
-private:    ///information for (old) InstGen
-  //map from quantifiers to their selection literals
+ private:  /// information for (old) InstGen
+  // map from quantifiers to their selection literals
   std::map< Node, Node > d_quant_selection_lit;
   std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates;
   //map from quantifiers to their selection literal terms
@@ -164,20 +169,23 @@ private:    ///information for (old) InstGen
   std::map< Node, std::vector< Node > > d_op_selection_terms;
   //get selection score
   int getSelectionScore( std::vector< Node >& uf_terms );
-protected:
+
+ protected:
   //reset
-  void reset( FirstOrderModel* fm );
+  void reset(FirstOrderModel* fm) override;
   //analyze quantifier
-  void analyzeQuantifier( FirstOrderModel* fm, Node f );
+  void analyzeQuantifier(FirstOrderModel* fm, Node f) override;
   //do InstGen techniques for quantifier, return number of lemmas produced
-  int doInstGen( FirstOrderModel* fm, Node f );
+  int doInstGen(FirstOrderModel* fm, Node f) override;
   //theory-specific build models
   void constructModelUf( FirstOrderModel* fm, Node op );
-protected:
+
+ protected:
   std::map< Node, QuantPhaseReq > d_phase_reqs;
-public:
+
+ public:
   QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
-  ~QModelBuilderDefault() throw() {}
+
   //options
   bool optReconsiderFuncConstants() { return true; }
   //has inst gen
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index f4d0e8e43..3448e967b 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -236,7 +236,7 @@ private:  //for equivalence classes
   bool areMatchDisequal( TNode n1, TNode n2 );
 public:
   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
-  ~QuantConflictFind() throw() {}
+
   /** register quantifier */
   void registerQuantifier( Node q );
 public:
diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h
index d2e9ec77b..47adddd9e 100644
--- a/src/theory/quantifiers/quant_equality_engine.h
+++ b/src/theory/quantifiers/quant_equality_engine.h
@@ -73,7 +73,6 @@ private:
   TNode getUnivRepresentativeInternal( TNode n );
 public:
   QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
-  virtual ~QuantEqualityEngine() throw (){}
 
   /* whether this module needs to check this round */
   bool needsCheck( Theory::Effort e );
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index d56e7c730..cfca96259 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -49,7 +49,6 @@ private:
   int checkRewriteRule( Node f, Theory::Effort e );
 public:
   RewriteEngine( context::Context* c, QuantifiersEngine* qe );
-  ~RewriteEngine() throw() {}
 
   bool needsCheck( Theory::Effort e );
   void check(Theory::Effort e, QEffort quant_e);
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index ab844c6ec..934a09a8e 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -80,7 +80,7 @@ class TheoryModel : public Model
   friend class TheoryEngineModelBuilder;
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
-  virtual ~TheoryModel() throw();
+  ~TheoryModel() override;
 
   /** reset the model */
   virtual void reset();
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 64ca41df2..bc729bcbf 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -154,17 +154,16 @@ private:
 
   Statistics d_stats;
 
-protected:
-
-  void contextNotifyPop() {
+ protected:
+  void contextNotifyPop() override
+  {
     Debug("ufsymm") << "UFSYMM: clearing state due to pop" << std::endl;
     clear();
   }
 
-public:
-
+ public:
   SymmetryBreaker(context::Context* context, std::string name = "");
-  ~SymmetryBreaker() throw() {}
+
   void assertFormula(TNode phi);
   void apply(std::vector<Node>& newClauses);
 
diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp
index 123d568cb..a957d6809 100644
--- a/src/util/abstract_value.cpp
+++ b/src/util/abstract_value.cpp
@@ -30,9 +30,12 @@ std::ostream& operator<<(std::ostream& out, const AbstractValue& val) {
   return out << "@" << val.getIndex();
 }
 
-AbstractValue::AbstractValue(Integer index) throw(IllegalArgumentException) :
-    d_index(index) {
-    PrettyCheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str());
+AbstractValue::AbstractValue(Integer index) : d_index(index)
+{
+  PrettyCheckArgument(index >= 1,
+                      index,
+                      "index >= 1 required for abstract value, not `%s'",
+                      index.toString().c_str());
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h
index 9c8e1cb37..2fbc26bec 100644
--- a/src/util/abstract_value.h
+++ b/src/util/abstract_value.h
@@ -27,36 +27,25 @@ namespace CVC4 {
 class CVC4_PUBLIC AbstractValue {
   const Integer d_index;
 
-public:
+ public:
+  AbstractValue(Integer index);
 
-  AbstractValue(Integer index) throw(IllegalArgumentException);
-
-  ~AbstractValue() throw() {}
-
-  const Integer& getIndex() const throw() {
-    return d_index;
-  }
-
-  bool operator==(const AbstractValue& val) const throw() {
+  const Integer& getIndex() const { return d_index; }
+  bool operator==(const AbstractValue& val) const
+  {
     return d_index == val.d_index;
   }
-  bool operator!=(const AbstractValue& val) const throw() {
-    return !(*this == val);
-  }
-
-  bool operator<(const AbstractValue& val) const throw() {
+  bool operator!=(const AbstractValue& val) const { return !(*this == val); }
+  bool operator<(const AbstractValue& val) const
+  {
     return d_index < val.d_index;
   }
-  bool operator<=(const AbstractValue& val) const throw() {
+  bool operator<=(const AbstractValue& val) const
+  {
     return d_index <= val.d_index;
   }
-  bool operator>(const AbstractValue& val) const throw() {
-    return !(*this <= val);
-  }
-  bool operator>=(const AbstractValue& val) const throw() {
-    return !(*this < val);
-  }
-
+  bool operator>(const AbstractValue& val) const { return !(*this <= val); }
+  bool operator>=(const AbstractValue& val) const { return !(*this < val); }
 };/* class AbstractValue */
 
 std::ostream& operator<<(std::ostream& out, const AbstractValue& val) CVC4_PUBLIC;
diff --git a/src/util/cache.h b/src/util/cache.h
index 38dc0fc99..4f9af98a6 100644
--- a/src/util/cache.h
+++ b/src/util/cache.h
@@ -58,9 +58,9 @@ public:
     bool d_fired;
 
   public:
-    Scope(Cache<T, U, Hasher>& cache, const T& elt) throw(AssertionException) :
-      d_cache(cache),
-      d_fired(d_cache.computing(elt)) {
+   Scope(Cache<T, U, Hasher>& cache, const T& elt)
+       : d_cache(cache), d_fired(d_cache.computing(elt))
+   {
     }
 
     ~Scope() {
@@ -69,21 +69,21 @@ public:
       }
     }
 
-    operator bool() throw() {
-      return d_fired;
-    }
-
-    const U& get() throw(AssertionException) {
+    operator bool() const { return d_fired; }
+    const U& get() const
+    {
       Assert(d_fired, "nothing in cache");
       return d_cache.get();
     }
 
-    U& operator()(U& computed) throw(AssertionException) {
+    U& operator()(U& computed)
+    {
       Assert(!d_fired, "can only cache a computation once");
       d_fired = true;
       return d_cache(computed);
     }
-    const U& operator()(const U& computed) throw(AssertionException) {
+    const U& operator()(const U& computed)
+    {
       Assert(!d_fired, "can only cache a computation once");
       d_fired = true;
       return d_cache(computed);
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 8f98d908f..c67277ad0 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -59,8 +59,8 @@ Integer Integer::exactQuotient(const Integer& y) const {
   return Integer( cln::exquo(d_value, y.d_value) );
 }
 
-
-void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
+void Integer::parseInt(const std::string& s, unsigned base)
+{
   cln::cl_read_flags flags;
   flags.syntax = cln::syntax_integer;
   flags.lsyntax = cln::lsyntax_standard;
@@ -86,7 +86,10 @@ void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_a
   readInt(flags, s, base);
 }
 
-void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
+void Integer::readInt(const cln::cl_read_flags& flags,
+                      const std::string& s,
+                      unsigned base)
+{
   try {
     // Removing leading zeroes, CLN has a bug for these inputs up to and
     // including CLN v1.3.2.
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 0433494cc..542333b1f 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -52,11 +52,13 @@ private:
    * Constructs an Integer by copying a CLN C++ primitive.
    */
   Integer(const cln::cl_I& val) : d_value(val) {}
+  // Throws a std::invalid_argument on invalid input `s` for the given base.
+  void readInt(const cln::cl_read_flags& flags,
+               const std::string& s,
+               unsigned base);
 
-  void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument);
-
-  void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument);
-
+  // Throws a std::invalid_argument on invalid inputs.
+  void parseInt(const std::string& s, unsigned base);
 
   // These constants are to help with CLN conversion in 32 bit.
   // See http://www.ginac.de/CLN/cln.html#Conversions
@@ -81,11 +83,13 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  explicit Integer(const char* sp, unsigned base = 10) throw (std::invalid_argument) {
+  explicit Integer(const char* sp, unsigned base = 10)
+  {
     parseInt(std::string(sp), base);
   }
 
-  explicit Integer(const std::string& s, unsigned base = 10) throw (std::invalid_argument) {
+  explicit Integer(const std::string& s, unsigned base = 10)
+  {
     parseInt(s, base);
   }
 
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 0b09bf1fd..2752971d2 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -84,14 +84,15 @@ public:
   /** Constructs a rational with the value 0/1. */
   Rational() : d_value(0){
   }
-
   /**
    * Constructs a Rational from a C string in a given base (defaults to 10).
+   *
    * Throws std::invalid_argument if the string is not a valid rational.
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  explicit Rational(const char* s, unsigned base = 10) throw (std::invalid_argument){
+  explicit Rational(const char* s, unsigned base = 10)
+  {
     cln::cl_read_flags flags;
 
     flags.syntax = cln::syntax_rational;
@@ -105,7 +106,8 @@ public:
       throw std::invalid_argument(ss.str());
     }
   }
-  Rational(const std::string& s, unsigned base = 10) throw (std::invalid_argument){
+  Rational(const std::string& s, unsigned base = 10)
+  {
     cln::cl_read_flags flags;
 
     flags.syntax = cln::syntax_rational;
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index b2adb4aba..9bcdcd96b 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -173,13 +173,14 @@ uint64_t ResourceManager::getTimeRemaining() const {
   return d_thisCallTimeBudget - time_passed;
 }
 
-void ResourceManager::spendResource(unsigned ammount) throw (UnsafeInterruptException) {
+void ResourceManager::spendResource(unsigned amount)
+{
   ++d_spendResourceCalls;
-  d_cumulativeResourceUsed += ammount;
+  d_cumulativeResourceUsed += amount;
   if (!d_on) return;
 
   Debug("limit") << "ResourceManager::spendResource()" << std::endl;
-  d_thisCallResourceUsed += ammount;
+  d_thisCallResourceUsed += amount;
   if(out()) {
     Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
     Trace("limit") << "          on call " << d_spendResourceCalls << std::endl;
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 35315559f..e49b27286 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -151,8 +151,8 @@ public:
   uint64_t getResourceBudgetForThisCall() {
     return d_thisCallResourceBudget;
   }
-
-  void spendResource(unsigned ammount) throw(UnsafeInterruptException);
+  // Throws an UnsafeInterruptException if there are no remaining resources.
+  void spendResource(unsigned amount);
 
   void setHardLimit(bool value);
   void setResourceLimit(uint64_t units, bool cumulative = false);
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 016bd2184..11afb99ed 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -140,10 +140,8 @@ std::ostream& operator<<(std::ostream& os, const timespec& t) {
 
 
 /** Construct a statistics registry */
-StatisticsRegistry::StatisticsRegistry(const std::string& name)
-  throw(CVC4::IllegalArgumentException) :
-  Stat(name) {
-
+StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name)
+{
   d_prefix = name;
   if(__CVC4_USE_STATISTICS) {
     PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
@@ -152,7 +150,8 @@ StatisticsRegistry::StatisticsRegistry(const std::string& name)
   }
 }
 
-void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
+void StatisticsRegistry::registerStat(Stat* s)
+{
 #ifdef CVC4_STATISTICS_ON
   PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s,
                 "Statistic `%s' was not registered with this registry.",
@@ -161,7 +160,8 @@ void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentExcept
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::registerStat_() */
 
-void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
+void StatisticsRegistry::unregisterStat(Stat* s)
+{
 #ifdef CVC4_STATISTICS_ON
   PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s,
                 "Statistic `%s' was not registered with this registry.",
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 3de001e32..73a545185 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -91,8 +91,8 @@ public:
    * will throw an assertion exception if the given name contains the
    * statistic delimiter string.
    */
-  Stat(const std::string& name) throw(CVC4::IllegalArgumentException) :
-    d_name(name) {
+  Stat(const std::string& name) : d_name(name)
+  {
     if(__CVC4_USE_STATISTICS) {
       CheckArgument(d_name.find(", ") == std::string::npos, name,
                     "Statistics names cannot include a comma (',')");
@@ -659,8 +659,7 @@ public:
   StatisticsRegistry() {}
 
   /** Construct a statistics registry */
-  StatisticsRegistry(const std::string& name)
-    throw(CVC4::IllegalArgumentException);
+  StatisticsRegistry(const std::string& name);
 
   /**
    * Set the name of this statistic registry, used as prefix during
@@ -689,10 +688,10 @@ public:
   }
 
   /** Register a new statistic */
-  void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
+  void registerStat(Stat* s);
 
   /** Unregister a new statistic */
-  void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
+  void unregisterStat(Stat* s);
 
 };/* class StatisticsRegistry */
 
diff --git a/src/util/tuple.h b/src/util/tuple.h
index e2440cc39..10da466de 100644
--- a/src/util/tuple.h
+++ b/src/util/tuple.h
@@ -28,11 +28,12 @@ namespace CVC4 {
 
 class CVC4_PUBLIC TupleUpdate {
   unsigned d_index;
-public:
-  TupleUpdate(unsigned index) throw() : d_index(index) { }
-  unsigned getIndex() const throw() { return d_index; }
-  bool operator==(const TupleUpdate& t) const throw() { return d_index == t.d_index; }
-  bool operator!=(const TupleUpdate& t) const throw() { return d_index != t.d_index; }
+
+ public:
+  TupleUpdate(unsigned index) : d_index(index) {}
+  unsigned getIndex() const { return d_index; }
+  bool operator==(const TupleUpdate& t) const { return d_index == t.d_index; }
+  bool operator!=(const TupleUpdate& t) const { return d_index != t.d_index; }
 };/* class TupleUpdate */
 
 struct CVC4_PUBLIC TupleUpdateHashFunction {