Changes needed to compile at Google, plus some bug fixes from Google.

27 files changed, 51 insertions, 34 deletions

diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index 472eff883..c1f0ce545 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -226,6 +226,7 @@ inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf){
 }
 class BoundUpdateCallback {
 public:
+  virtual ~BoundUpdateCallback() {}
   virtual void operator()(ArithVar v, const BoundsInfo&  up) = 0;
 };
 
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index ad88aea86..734c605c6 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -36,6 +36,7 @@ namespace arith {
  */
 class ArithVarCallBack {
 public:
+  virtual ~ArithVarCallBack() {}
   virtual void operator()(ArithVar x) = 0;
 };
 
@@ -45,22 +46,26 @@ public:
  */
 class ArithVarMalloc {
 public:
+  virtual ~ArithVarMalloc() {}
   virtual ArithVar request() = 0;
   virtual void release(ArithVar v) = 0;
 };
 
 class TNodeCallBack {
 public:
+  virtual ~TNodeCallBack() {}
   virtual void operator()(TNode n) = 0;
 };
 
 class NodeCallBack {
 public:
+  virtual ~NodeCallBack() {}
   virtual void operator()(Node n) = 0;
 };
 
 class RationalCallBack {
 public:
+  virtual ~RationalCallBack() {}
   virtual Rational operator()() const = 0;
 };
 
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index f6717d141..99ec6e52c 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -159,7 +159,8 @@ public:
   }
 
   void dropNonZeroes(){
-    std::remove_if(d_vec.begin(), d_vec.end(), &Border::nonZero);
+    d_vec.erase(std::remove_if(d_vec.begin(), d_vec.end(), &Border::nonZero),
+                d_vec.end());
   }
 
   const Border& top() const {
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index 73235d490..6c218eb0b 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -39,6 +39,7 @@ const RowIndex ROW_INDEX_SENTINEL  = std::numeric_limits<RowIndex>::max();
 
 class CoefficientChangeCallback {
 public:
+  virtual ~CoefficientChangeCallback() {}
   virtual void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) = 0;
   virtual void multiplyRow(RowIndex ridx, int Sgn) = 0;
   virtual bool canUseRow(RowIndex ridx) const = 0;
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index ada9b5efd..2d7fc597a 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -135,7 +135,7 @@ protected:
 
 public:
   SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
-  ~SimplexDecisionProcedure();
+  virtual ~SimplexDecisionProcedure();
 
   /**
    * Tries to update the assignments of variables such that all of the
@@ -217,4 +217,3 @@ protected:
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 79434102e..d4d7bc04c 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -170,7 +170,7 @@ public:
   void storeBBAtom(TNode atom, Node atom_bb);
   bool hasBBAtom(TNode atom) const; 
   TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
-  ~TLazyBitblaster();
+  ~TLazyBitblaster() throw();
   /** 
    * 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 fbebcd952..080f23143 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -62,7 +62,7 @@ void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
   d_abstraction = abs; 
 }
 
-TLazyBitblaster::~TLazyBitblaster() {
+TLazyBitblaster::~TLazyBitblaster() throw() {
   delete d_cnfStream;
   delete d_nullRegistrar;
   delete d_nullContext;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 08fe5f2e9..9dcd5ac62 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -576,8 +576,8 @@ Node TheoryBV::ppRewrite(TNode t)
   } else if( res.getKind() == kind::EQUAL &&
       ((res[0].getKind() == kind::BITVECTOR_PLUS &&
         RewriteRule<ConcatToMult>::applies(res[1])) ||
-       res[1].getKind() == kind::BITVECTOR_PLUS &&
-       RewriteRule<ConcatToMult>::applies(res[0]))) {
+       (res[1].getKind() == kind::BITVECTOR_PLUS &&
+	RewriteRule<ConcatToMult>::applies(res[0])))) {
     Node mult = RewriteRule<ConcatToMult>::applies(res[0])?
       RewriteRule<ConcatToMult>::run<false>(res[0]) :
       RewriteRule<ConcatToMult>::run<true>(res[1]);
@@ -747,8 +747,8 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
   d_staticLearnCache.insert(in);
     
   if (in.getKind() == kind::EQUAL) {
-    if(in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL ||
-       in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL){
+    if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
+       (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
       TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
       TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
 
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 0c41e8ff7..ba9823541 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -202,10 +202,10 @@ namespace rewrite {
 
   // Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder
   RewriteResponse compactMinMax (TNode node, bool isPreRewrite) {
+#ifdef CVC4_ASSERTIONS
     Kind k = node.getKind();
-
     Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX));
-
+#endif
     if (node[0] == node[1]) {
       return RewriteResponse(REWRITE_DONE, node[0]);
     } else {
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 44d327c5c..b2c49c8a3 100644
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -89,6 +89,7 @@ private:
   bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n );
 public:
   AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
+  ~AbsMbqiBuilder() throw() {}
   //process build model
   void processBuildModel(TheoryModel* m, bool fullModel);
   //do exhaustive instantiation
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index c09527f89..dd241b15e 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -110,6 +110,7 @@ private:
   void addLiteralFromRange( Node lit, Node r );
 public:
   BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
+  ~BoundedIntegers() throw() {}
 
   bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 7a959a70d..9d4035970 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -31,7 +31,7 @@ namespace inst {
 class CandidateGenerator {
 public:
   CandidateGenerator(){}
-  ~CandidateGenerator(){}
+  virtual ~CandidateGenerator(){}
 
   /** Get candidates functions.  These set up a context to get all match candidates.
       cg->reset( eqc );
@@ -60,7 +60,7 @@ private:
   int d_candidate_index;
 public:
   CandidateGeneratorQueue() : d_candidate_index( 0 ){}
-  ~CandidateGeneratorQueue(){}
+  ~CandidateGeneratorQueue() throw() {}
 
   void addCandidate( Node n );
 
@@ -94,7 +94,7 @@ private:
   Node d_n;
 public:
   CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
-  ~CandidateGeneratorQE(){}
+  ~CandidateGeneratorQE() throw() {}
 
   void resetInstantiationRound();
   void reset( Node eqc );
@@ -112,7 +112,7 @@ private:
   QuantifiersEngine* d_qe;
 public:
   CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQELitEq(){}
+  ~CandidateGeneratorQELitEq() throw() {}
 
   void resetInstantiationRound();
   void reset( Node eqc );
@@ -130,7 +130,7 @@ private:
   QuantifiersEngine* d_qe;
 public:
   CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQELitDeq(){}
+  ~CandidateGeneratorQELitDeq() throw() {}
 
   void resetInstantiationRound();
   void reset( Node eqc );
@@ -154,7 +154,7 @@ private:
   bool d_firstTime;
 public:
   CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
-  ~CandidateGeneratorQEAll(){}
+  ~CandidateGeneratorQEAll() throw() {}
 
   void resetInstantiationRound();
   void reset( Node eqc );
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index b5ebe3d7c..fc7481739 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -31,6 +31,7 @@ class CegConjecture;
 class CegqiOutput
 {
 public:
+  virtual ~CegqiOutput() {}
   virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0;
   virtual bool isEligibleForInstantiation( Node n ) = 0;
   virtual bool addLemma( Node lem ) = 0;
@@ -83,6 +84,7 @@ class CegqiOutputSingleInv : public CegqiOutput
 {
 public:
   CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
+  ~CegqiOutputSingleInv() {}
   CegConjectureSingleInv * d_out;
   bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
   bool isEligibleForInstantiation( Node n );
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 2d8e8e403..48694c99a 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -406,6 +406,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 eef354e75..88464bb9a 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -585,7 +585,7 @@ FirstOrderModel(qe, c, name){
 
 }
 
-FirstOrderModelFmc::~FirstOrderModelFmc() {
+FirstOrderModelFmc::~FirstOrderModelFmc() throw() {
   for(std::map<Node, Def*>::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 c2cd88e17..fbcaf938f 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -76,7 +76,7 @@ public: //for Theory Quantifiers:
   virtual void processInitializeQuantifier( Node q ) {}
 public:
   FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
-  virtual ~FirstOrderModel() {}
+  virtual ~FirstOrderModel() throw() {}
   virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
   virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
   virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
@@ -181,7 +181,7 @@ private:
   void processInitializeModelForTerm(Node n);
 public:
   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
-  virtual ~FirstOrderModelFmc();
+  virtual ~FirstOrderModelFmc() throw();
   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
   // initialize the model
   void processInitialize( bool ispre );
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 372868ad7..9a7b05090 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -133,7 +133,7 @@ private:
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 public:
   FullModelChecker( context::Context* c, QuantifiersEngine* qe );
-  ~FullModelChecker(){}
+  ~FullModelChecker() throw() {}
 
   bool optBuildAtFullModel();
 
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 1be67caed..f9853ef54 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -33,6 +33,7 @@ namespace inst {
 /** base class for producing InstMatch objects */
 class IMGenerator {
 public:
+  virtual ~IMGenerator() {}
   /** reset instantiation round (call this at beginning of instantiation round) */
   virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
@@ -89,7 +90,7 @@ public:
   InstMatchGenerator( Node pat );
   InstMatchGenerator();
   /** destructor */
-  ~InstMatchGenerator(){}
+  ~InstMatchGenerator() throw() {}
   /** The pattern we are producing matches for.
       If null, this is a multi trigger that is merging matches from d_children.
   */
@@ -123,6 +124,7 @@ public:
 class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
 public:
   VarMatchGeneratorBooleanTerm( Node var, Node comp );
+  ~VarMatchGeneratorBooleanTerm() throw() {}
   Node d_comp;
   bool d_rm_prev;
   /** reset instantiation round (call this at beginning of instantiation round) */
@@ -139,6 +141,7 @@ public:
 class VarMatchGeneratorTermSubs : public InstMatchGenerator {
 public:
   VarMatchGeneratorTermSubs( Node var, Node subs );
+  ~VarMatchGeneratorTermSubs() throw() {}
   TNode d_var;
   Node d_subs;
   bool d_rm_prev;
@@ -186,7 +189,7 @@ public:
   /** constructors */
   InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe );
   /** destructor */
-  ~InstMatchGeneratorMulti(){}
+  ~InstMatchGeneratorMulti() throw() {}
   /** reset instantiation round (call this whenever equivalence classes have changed) */
   void resetInstantiationRound( QuantifiersEngine* qe );
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
@@ -218,7 +221,7 @@ public:
   /** constructors */
   InstMatchGeneratorSimple( Node f, Node pat );
   /** destructor */
-  ~InstMatchGeneratorSimple(){}
+  ~InstMatchGeneratorSimple() throw() {}
   /** reset instantiation round (call this whenever equivalence classes have changed) */
   void resetInstantiationRound( QuantifiersEngine* qe );
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 9435fc97c..586cd492c 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -75,7 +75,7 @@ private:
   int process( Node f, Theory::Effort effort, int e );
 public:
   InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
-  ~InstStrategySimplex(){}
+  ~InstStrategySimplex() throw() {}
   /** identify */
   std::string identify() const { return std::string("Simplex"); }
 };
@@ -107,7 +107,7 @@ private:
   int process( Node f, Theory::Effort effort, int e );
 public:
   InstStrategyCegqi( QuantifiersEngine * qe );
-  ~InstStrategyCegqi(){}
+  ~InstStrategyCegqi() throw() {}
   
   bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
   bool isEligibleForInstantiation( Node n );  
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 7679cf93f..47de4e581 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -35,7 +35,7 @@ protected:
   QuantifiersEngine* d_qe;
 public:
   QModelBuilder( context::Context* c, QuantifiersEngine* qe );
-  virtual ~QModelBuilder(){}
+  virtual ~QModelBuilder() throw() {}
   // is quantifier active?
   virtual bool isQuantifierActive( Node f );
   //do exhaustive instantiation
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index b2dc680f2..829b67777 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -203,6 +203,7 @@ public:
   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/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 1703a9bfc..2e2578af5 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -53,6 +53,7 @@ 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, unsigned quant_e );
diff --git a/src/theory/strings/options b/src/theory/strings/options
index 11156b5a4..a5b977121 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -8,7 +8,7 @@ module STRINGS "theory/strings/options.h" Strings theory
 option stringExp strings-exp --strings-exp bool :default false :read-write
  experimental features in the theory of strings
 
-option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate less_equal(2) :predicate-include "smt/smt_engine.h"
+option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate options::less_equal(2) :predicate-include "smt/smt_engine.h"
  the strategy of LB rule application: 0-lazy, 1-eager, 2-no
 
 option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate less_equal(2) :predicate-include "smt/smt_engine.h"
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 8d107d36a..cad1f3bf1 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1386,8 +1386,8 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned char> &pcset, SetNodes &pv
 bool RegExpOpr::isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2) {
   for(std::set< PairNodes >::const_iterator itr = s.begin();
       itr != s.end(); ++itr) {
-    if(itr->first == n1 && itr->second == n2 ||
-       itr->first == n2 && itr->second == n1) {
+    if((itr->first == n1 && itr->second == n2) ||
+       (itr->first == n2 && itr->second == n1)) {
       return true;
     }
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5dc4d9408..d0a1eb696 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -962,8 +962,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
   Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl;
 
   Assert(toTheoryId != fromTheoryId);
-  if(! d_logicInfo.isTheoryEnabled(toTheoryId) &&
-     toTheoryId != THEORY_SAT_SOLVER) {
+  if(toTheoryId != THEORY_SAT_SOLVER &&
+     ! d_logicInfo.isTheoryEnabled(toTheoryId)) {
     stringstream ss;
     ss << "The logic was specified as " << d_logicInfo.getLogicString()
        << ", which doesn't include " << toTheoryId
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 6a53cb3ab..072f579be 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -46,7 +46,7 @@ TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncM
   d_eeContext->push();
 }
 
-TheoryModel::~TheoryModel() {
+TheoryModel::~TheoryModel() throw() {
   d_eeContext->pop();
   delete d_equalityEngine;
   delete d_eeContext;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index eeaf3c8da..4e5c84f42 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -38,7 +38,7 @@ protected:
   SubstitutionMap d_substitutions;
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
-  virtual ~TheoryModel();
+  virtual ~TheoryModel() throw();
 
   /** special local context for our equalityEngine so we can clear it independently of search context */
   context::Context* d_eeContext;