14 files changed, 48 insertions, 47 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index bc4205217..951b92e1c 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -869,7 +869,8 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
  * @param check whether we should check the type as we compute it
  * (default: false)
  */
-Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
+Type ExprManager::getType(Expr e, bool check)
+{
   NodeManagerScope nms(d_nodeManager);
   Type t;
   try {
@@ -995,12 +996,13 @@ unsigned ExprManager::maxArity(Kind kind) {
 NodeManager* ExprManager::getNodeManager() const {
   return d_nodeManager;
 }
-
-Statistics ExprManager::getStatistics() const throw() {
+Statistics ExprManager::getStatistics() const
+{
   return Statistics(*d_nodeManager->getStatisticsRegistry());
 }
 
-SExpr ExprManager::getStatistic(const std::string& name) const throw() {
+SExpr ExprManager::getStatistic(const std::string& name) const
+{
   return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
 }
 
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 35a3b6a6e..5adb30ad6 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -436,9 +436,13 @@ public:
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity) const;
 
-  /** Get the type of an expression */
-  Type getType(Expr e, bool check = false)
-    throw(TypeCheckingException);
+  /**
+   * Get the type of an expression.
+   *
+   * Throws a TypeCheckingException on failures or if a Type cannot be
+   * computed.
+   */
+  Type getType(Expr e, bool check = false);
 
   /** Bits for use in mkVar() flags. */
   enum {
@@ -524,10 +528,10 @@ public:
   Expr mkNullaryOperator( Type type, Kind k);
 
   /** Get a reference to the statistics registry for this ExprManager */
-  Statistics getStatistics() const throw();
+  Statistics getStatistics() const;
 
   /** Get a reference to the statistics registry for this ExprManager */
-  SExpr getStatistic(const std::string& name) const throw();
+  SExpr getStatistic(const std::string& name) const;
 
   /**
    * Flushes statistics for this ExprManager to a file descriptor. Safe to use
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 0ed3601fc..f4dd294a7 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -337,7 +337,8 @@ Expr Expr::getOperator() const {
   return Expr(d_exprManager, new Node(d_node->getOperator()));
 }
 
-Type Expr::getType(bool check) const throw (TypeCheckingException) {
+Type Expr::getType(bool check) const
+{
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   PrettyCheckArgument(!d_node->isNull(), this,
@@ -499,14 +500,8 @@ void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag,
   d_node->toStream(out, depth, types, dag, language);
 }
 
-Node Expr::getNode() const throw() {
-  return *d_node;
-}
-
-TNode Expr::getTNode() const throw() {
-  return *d_node;
-}
-
+Node Expr::getNode() const { return *d_node; }
+TNode Expr::getTNode() const { return *d_node; }
 Expr Expr::notExpr() const {
   Assert(d_exprManager != NULL,
          "Don't have an expression manager for this expression!");
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 9656781a8..cc9949c30 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -409,7 +409,7 @@ public:
    * @param check whether we should check the type as we compute it
    * (default: false)
    */
-  Type getType(bool check = false) const throw (TypeCheckingException);
+  Type getType(bool check = false) const;
 
   /**
    * Substitute "replacement" in for "e".
@@ -521,13 +521,13 @@ private:
    * Returns the actual internal node.
    * @return the internal node
    */
-  NodeTemplate<true> getNode() const throw();
+  NodeTemplate<true> getNode() const;
 
   /**
    * Returns the actual internal node as a TNode.
    * @return the internal node
    */
-  NodeTemplate<false> getTNode() const throw();
+  NodeTemplate<false> getTNode() const;
 
   // Friend to access the actual internal expr information and private methods
   friend class SmtEngine;
@@ -545,7 +545,7 @@ private:
 
 ${getConst_instantiations}
 
-#line 557 "${template}"
+#line 549 "${template}"
 
 inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
   return (size_t) e.getId();
diff --git a/src/expr/node.h b/src/expr/node.h
index fd3d20afa..92f905c8b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -228,7 +228,10 @@ class NodeTemplate {
    */
   void assignNodeValue(expr::NodeValue* ev);
 
-  inline void assertTNodeNotExpired() const throw(AssertionException) {
+  // May throw an AssertionException if the Node is not live, i.e. the ref count
+  // is not positive.
+  inline void assertTNodeNotExpired() const
+  {
     if(!ref_count) {
       Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
     }
@@ -525,8 +528,7 @@ public:
    * @param check whether we should check the type as we compute it
    * (default: false)
    */
-  TypeNode getType(bool check = false) const
-    throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException);
+  TypeNode getType(bool check = false) const;
 
   /**
    * Substitution of Nodes.
@@ -1271,7 +1273,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const {
 
 template <bool ref_count>
 TypeNode NodeTemplate<ref_count>::getType(bool check) const
-  throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException) {
+{
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 45ac02f10..b0fdd0657 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -687,10 +687,11 @@ private:
   expr::NodeValue* constructNV() const;
 
 #ifdef CVC4_DEBUG
-  void maybeCheckType(const TNode n) const
-    throw(TypeCheckingExceptionPrivate, AssertionException);
+  // Throws a TypeCheckingExceptionPrivate on a failure.
+  void maybeCheckType(const TNode n) const;
 #else /* CVC4_DEBUG */
-  inline void maybeCheckType(const TNode n) const throw() { }
+  // Do nothing if not in debug mode.
+  inline void maybeCheckType(const TNode n) const {}
 #endif /* CVC4_DEBUG */
 
 public:
@@ -1320,7 +1321,7 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
 #ifdef CVC4_DEBUG
 template <unsigned nchild_thresh>
 inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
-    throw(TypeCheckingExceptionPrivate, AssertionException) {
+{
   /* force an immediate type check, if early type checking is
      enabled and the current node isn't a variable or constant */
   if( d_nm->getOptions()[options::earlyTypeChecking] ) {
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 85f5e3c75..3c79e96f2 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -400,8 +400,7 @@ std::vector<NodeValue*> NodeManager::TopologicalSort(
 } /* NodeManager::TopologicalSort() */
 
 TypeNode NodeManager::getType(TNode n, bool check)
-  throw(TypeCheckingExceptionPrivate, AssertionException) {
-
+{
   // Many theories' type checkers call Node::getType() directly.  This
   // is incorrect, since "this" might not be the caller's curent node
   // manager.  Rather than force the individual typecheckers not to do
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d9345a5f5..e1ba28be9 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -902,8 +902,7 @@ public:
    * @param check whether we should check the type as we compute it
    * (default: false)
    */
-  TypeNode getType(TNode n, bool check = false)
-    throw(TypeCheckingExceptionPrivate, AssertionException);
+  TypeNode getType(TNode n, bool check = false);
 
   /**
    * Convert a node to an expression.  Uses the ExprManager
diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp
index e93764eed..ab3675cda 100644
--- a/src/options/open_ostream.cpp
+++ b/src/options/open_ostream.cpp
@@ -42,7 +42,6 @@ void OstreamOpener::addSpecialCase(const std::string& name, std::ostream* out){
 
 
 std::pair< bool, std::ostream* > OstreamOpener::open(const std::string& optarg) const
-    throw(OptionException)
 {
   if(optarg == "") {
     std::stringstream ss;
diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h
index 7630c3bf0..9359d5cda 100644
--- a/src/options/open_ostream.h
+++ b/src/options/open_ostream.h
@@ -47,8 +47,7 @@ class OstreamOpener {
    *   returns <true, stream> where stream is a ostream allocated by new.
    *   The caller is in this case the owner of the allocated memory.
    */
-  std::pair<bool, std::ostream*> open(const std::string& name) const
-    throw(OptionException);
+  std::pair<bool, std::ostream*> open(const std::string& name) const;
 
  private:
   const char* d_channelName;
diff --git a/src/options/options.h b/src/options/options.h
index 608b9906a..d48f16f66 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -176,10 +176,10 @@ public:
 
   /**
    * Set the value of the given option by key.
+   *
+   * Throws OptionException or ModalException on failures.
    */
-  void setOption(const std::string& key, const std::string& optionarg)
-      throw(OptionException, ModalException);
-
+  void setOption(const std::string& key, const std::string& optionarg);
 
   /** Get the value of the given option.  Const access only. */
   template <class T>
@@ -187,9 +187,11 @@ public:
 
   /**
    * Gets the value of the given option by key and returns value as a string.
+   *
+   * Throws OptionException on failures, such as key not being the name of an
+   * option.
    */
-  std::string getOption(const std::string& key) const
-    throw(OptionException);
+  std::string getOption(const std::string& key) const;
 
   // Get accessor functions.
   InputLanguage getInputLanguage() const;
diff --git a/src/options/options_get_option_template.cpp b/src/options/options_get_option_template.cpp
index 81a0daf5f..8a88abaa5 100644
--- a/src/options/options_get_option_template.cpp
+++ b/src/options/options_get_option_template.cpp
@@ -40,7 +40,7 @@ using namespace std;
 namespace CVC4 {
 
 std::string Options::getOption(const std::string& key) const
-  throw(OptionException) {
+{
   Trace("options") << "SMT getOption(" << key << ")" << endl;
 
   ${smt_getoption_handlers}
diff --git a/src/options/options_set_option_template.cpp b/src/options/options_set_option_template.cpp
index cfe642b7b..aa56163f2 100644
--- a/src/options/options_set_option_template.cpp
+++ b/src/options/options_set_option_template.cpp
@@ -38,7 +38,7 @@ using namespace std;
 namespace CVC4 {
 
 void Options::setOption(const std::string& key, const std::string& optionarg)
-  throw(OptionException, ModalException) {
+{
   options::OptionsHandler* handler = d_handler;
   Trace("options") << "SMT setOption(" << key << ", " << optionarg << ")" << endl;
 
diff --git a/src/theory/example/ecdata.h b/src/theory/example/ecdata.h
index 475d0e615..9c93f4710 100644
--- a/src/theory/example/ecdata.h
+++ b/src/theory/example/ecdata.h
@@ -74,8 +74,7 @@ struct Link {
     return pCMM->newData(size);
   }
 
-private:
-
+ private:
   /**
    * The destructor isn't actually defined.  This declaration keeps
    * the compiler from creating (wastefully) a default definition, and
@@ -84,7 +83,7 @@ private:
    * be allocated in a ContextMemoryManager, which doesn't call
    * destructors.
    */
-  ~Link() throw();
+  ~Link();
 
   /**
    * Just like the destructor, this is not defined.  This ensures no