Removing more miscellaneous throw specifiers. (#1488)

Removing more miscellaneous throw specifiers.

3 files changed, 6 insertions, 7 deletions

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 */