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

45 files changed, 97 insertions, 70 deletions

diff --git a/proofs/lfsc_checker/check.h b/proofs/lfsc_checker/check.h
index a70599b0f..756bb4db6 100644
--- a/proofs/lfsc_checker/check.h
+++ b/proofs/lfsc_checker/check.h
@@ -80,7 +80,7 @@ inline char our_getc() {
 #endif
     colnum = 1;
     break;
-  case EOF:
+  case char(EOF):
     break;
   default:
     colnum++;
@@ -95,7 +95,7 @@ inline char non_ws() {
   while(isspace(c = our_getc()));
   if (c == ';') {
     // comment to end of line
-    while((c = our_getc()) != '\n' && c != EOF);
+    while((c = our_getc()) != '\n' && c != char(EOF));
     return non_ws();
   }
   return c;
@@ -115,7 +115,7 @@ extern char idbuf[];
 inline const char *prefix_id() {
   int i = 0;
   char c = idbuf[i++] = non_ws();
-  while (!isspace(c) && c != '(' && c != ')' && c != EOF) {
+  while (!isspace(c) && c != '(' && c != ')' && c != char(EOF)) {
     if (i == IDBUF_LEN)
       report_error("Identifier is too long");
     
diff --git a/src/context/context.h b/src/context/context.h
index 02d82a6d3..9c631b202 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -613,7 +613,7 @@ public:
   /**
    * Destructor does nothing: subclass must explicitly call destroy() instead.
    */
-  virtual ~ContextObj() {}
+  virtual ~ContextObj() throw(AssertionException) {}
 
   /**
    * If you want to allocate a ContextObj object on the heap, use this
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index c9a6b7e1b..082f3cdbf 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -55,7 +55,7 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
   Trace("decision") << "Justification heuristic enabled" << std::endl;
 }
 
-JustificationHeuristic::~JustificationHeuristic() {
+JustificationHeuristic::~JustificationHeuristic() throw() {
   StatisticsRegistry::unregisterStat(&d_helfulness);
   StatisticsRegistry::unregisterStat(&d_giveup);
   StatisticsRegistry::unregisterStat(&d_timestat);
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 9177ba44d..e1ed431d1 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -114,7 +114,7 @@ public:
                          context::UserContext *uc,
                          context::Context *c);
 
-  ~JustificationHeuristic();
+  ~JustificationHeuristic() throw();
 
   prop::SatLiteral getNext(bool &stopSearch);
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 080034e70..2a884d35a 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -261,7 +261,7 @@ public:
                   std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
 
   /** Default constructor, makes a null expression. */
-  NodeTemplate() : d_nv(&expr::NodeValue::s_null) { }
+  NodeTemplate() : d_nv(&expr::NodeValue::null()) { }
 
   /**
    * Conversion between nodes that are reference-counted and those that are
@@ -322,7 +322,7 @@ public:
    */
   bool isNull() const {
     assertTNodeNotExpired();
-    return d_nv == &expr::NodeValue::s_null;
+    return d_nv == &expr::NodeValue::null();
   }
 
   /**
@@ -1026,7 +1026,7 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
 }
 
 template <bool ref_count>
-NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null);
+NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::null());
 
 // FIXME: escape from type system convenient but is there a better
 // way?  Nodes conceptually don't change their expr values but of
@@ -1039,7 +1039,7 @@ NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
   if(ref_count) {
     d_nv->inc();
   } else {
-    Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::s_null,
+    Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null(),
            "TNode constructed from NodeValue with rc == 0");
   }
 }
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 48aacddf2..4eb5dd680 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -112,7 +112,7 @@ NodeManager::NodeManager(ExprManager* exprManager,
 }
 
 void NodeManager::init() {
-  poolInsert( &expr::NodeValue::s_null );
+  poolInsert( &expr::NodeValue::null() );
 
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
     Kind k = Kind(i);
@@ -163,7 +163,7 @@ NodeManager::~NodeManager() {
     reclaimZombies();
   }
 
-  poolRemove( &expr::NodeValue::s_null );
+  poolRemove( &expr::NodeValue::null() );
 
   if(Debug.isOn("gc:leaks")) {
     Debug("gc:leaks") << "still in pool:" << endl;
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 8af056f62..6b48fd9b7 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -32,12 +32,10 @@ using namespace std;
 namespace CVC4 {
 namespace expr {
 
-NodeValue NodeValue::s_null(0);
-
 string NodeValue::toString() const {
   stringstream ss;
 
-  OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();
+  OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO : options::outputLanguage();
   toStream(ss, -1, false, false, outlang);
   return ss.str();
 }
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index a6e7a6053..785f8909f 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -74,9 +74,6 @@ namespace expr {
  */
 class NodeValue {
 
-  /** A convenient null-valued expression value */
-  static NodeValue s_null;
-
   static const unsigned NBITS_REFCOUNT = __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
   static const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND;
   static const unsigned NBITS_ID = __CVC4__EXPR__NODE_VALUE__NBITS__ID;
@@ -278,8 +275,9 @@ public:
     return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
   }
 
-  static inline const NodeValue& null() {
-    return s_null;
+  static inline NodeValue& null() {
+    static NodeValue* s_null = new NodeValue(0);
+    return *s_null;
   }
 
   /**
diff --git a/src/expr/pickler.h b/src/expr/pickler.h
index f1cdd1c65..8c3da5f40 100644
--- a/src/expr/pickler.h
+++ b/src/expr/pickler.h
@@ -74,7 +74,7 @@ protected:
 
 public:
   Pickler(ExprManager* em);
-  ~Pickler();
+  virtual ~Pickler();
 
   /**
    * Constructs a new Pickle of the node n.
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 9dbcb628f..1f2963e18 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -24,7 +24,7 @@ using namespace std;
 
 namespace CVC4 {
 
-TypeNode TypeNode::s_null( &expr::NodeValue::s_null );
+TypeNode TypeNode::s_null( &expr::NodeValue::null() );
 
 TypeNode TypeNode::substitute(const TypeNode& type,
                               const TypeNode& replacement,
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 5129b7581..4f9e497ea 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -107,7 +107,7 @@ private:
 public:
 
   /** Default constructor, makes a null expression. */
-  TypeNode() : d_nv(&expr::NodeValue::s_null) { }
+  TypeNode() : d_nv(&expr::NodeValue::null()) { }
 
   /** Copy constructor */
   TypeNode(const TypeNode& node);
@@ -404,7 +404,7 @@ public:
    * @return true if null
    */
   bool isNull() const {
-    return d_nv == &expr::NodeValue::s_null;
+    return d_nv == &expr::NodeValue::null();
   }
 
   /**
diff --git a/src/printer/printer.h b/src/printer/printer.h
index e0b80ddfc..fcc0df93c 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -44,6 +44,7 @@ class Printer {
 protected:
   // derived classes can construct, but no one else.
   Printer() throw() {}
+  virtual ~Printer() {}
 
   /** write model response to command */
   virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0;
diff --git a/src/prop/bvminisat/mtl/Map.h b/src/prop/bvminisat/mtl/Map.h
index 8bd5659bc..4e61d6582 100644
--- a/src/prop/bvminisat/mtl/Map.h
+++ b/src/prop/bvminisat/mtl/Map.h
@@ -29,16 +29,17 @@ namespace BVMinisat {
 // Default hash/equals functions
 //
 
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
 template<class K> struct Hash  { uint32_t operator()(const K& k)               const { return hash(k);  } };
 template<class K> struct Equal { bool     operator()(const K& k1, const K& k2) const { return k1 == k2; } };
 
 template<class K> struct DeepHash  { uint32_t operator()(const K* k)               const { return hash(*k);  } };
 template<class K> struct DeepEqual { bool     operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
 
-static inline uint32_t hash(uint32_t x){ return x; }
-static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
-static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
-static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
 
 
 //=================================================================================================
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index bc60542e7..46c2666c8 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -175,6 +175,7 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
 namespace CVC4 {
 class ProofProxyAbstract {
 public:
+  virtual ~ProofProxyAbstract() {}
   virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; 
 };
 }
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index dda6c73d1..72563e6d3 100644
--- a/src/prop/minisat/mtl/Map.h
+++ b/src/prop/minisat/mtl/Map.h
@@ -29,16 +29,17 @@ namespace Minisat {
 // Default hash/equals functions
 //
 
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
 template<class K> struct Hash  { uint32_t operator()(const K& k)               const { return hash(k);  } };
 template<class K> struct Equal { bool     operator()(const K& k1, const K& k2) const { return k1 == k2; } };
 
 template<class K> struct DeepHash  { uint32_t operator()(const K* k)               const { return hash(*k);  } };
 template<class K> struct DeepEqual { bool     operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
 
-static inline uint32_t hash(uint32_t x){ return x; }
-static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
-static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
-static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
 
 
 //=================================================================================================
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index b71844590..8effa8189 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -36,7 +36,7 @@ class SatSolver {
 public:
 
   /** Virtual destructor */
-  virtual ~SatSolver() { }
+  virtual ~SatSolver() throw(AssertionException) { }
 
   /** Assert a clause in the solver. */
   virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0;
@@ -80,6 +80,7 @@ public:
 class BVSatSolverInterface: public SatSolver {
 public:
 
+  virtual ~BVSatSolverInterface() throw(AssertionException) {}
   /** Interface for notifications */
   class Notify {
   public:
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 229cc7c7c..04af80281 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -474,7 +474,7 @@ public:
     d_resourceManager = NodeManager::currentResourceManager();
   }
 
-  ~SmtEnginePrivate() {
+  ~SmtEnginePrivate() throw() {
     if(d_propagatorNeedsFinish) {
       d_propagator.finish();
       d_propagatorNeedsFinish = false;
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;
diff --git a/src/util/didyoumean.cpp b/src/util/didyoumean.cpp
index 228fe721e..dd8941033 100644
--- a/src/util/didyoumean.cpp
+++ b/src/util/didyoumean.cpp
@@ -77,7 +77,12 @@ int DidYouMean::editDistance(const std::string& a, const std::string& b)
   int len1 = a.size();
   int len2 = b.size();
 
-  int C[3][len2+1];             // cost
+  int* C[3];
+  int ii;
+  for (ii = 0; ii < 3; ++ii) {
+    C[ii] = new int[len2+1];
+  }
+  //  int C[3][len2+1];             // cost
 
   for(int j = 0; j <= len2; ++j) {
     C[0][j] = j * addCost;
@@ -123,7 +128,11 @@ int DidYouMean::editDistance(const std::string& a, const std::string& b)
     }
 
   }
-  return C[len1%3][len2];
+  int result = C[len1%3][len2];
+  for (ii = 0; ii < 3; ++ii) {
+    delete [] C[ii];
+  }
+  return result;
 }
 
 string DidYouMean::getMatchAsString(string input, int prefixNewLines, int suffixNewLines) {