Removing miscellaneous throw specifiers. (#1474)

1 files changed, 2 insertions, 23 deletions

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index a12c68791..35a3b6a6e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -109,13 +109,13 @@ public:
    * any expression references that used to be managed by this expression
    * manager and are left-over are bad.
    */
-  ~ExprManager() throw();
+  ~ExprManager();
 
   /** Get this expr manager's options */
   const Options& getOptions() const;
 
   /** Get this expr manager's resource manager */
-  ResourceManager* getResourceManager() throw();
+  ResourceManager* getResourceManager();
 
   /** Get the type for booleans */
   BooleanType booleanType() const;
@@ -436,27 +436,6 @@ public:
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity) const;
 
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression.  A TypeCheckingException can be thrown if lambda is
-   * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that
-   * the resulting predicate subtype is inhabited.
-   */
-  // not in release 1.0
-  //Type mkPredicateSubtype(Expr lambda)
-  //  throw(TypeCheckingException);
-
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression and whose non-emptiness is witnessed by the given
-   * witness.  A TypeCheckingException can be thrown if lambda is not
-   * a LAMBDA, or is ill-typed, or if the witness is not a witness or
-   * ill-typed.
-   */
-  // not in release 1.0
-  //Type mkPredicateSubtype(Expr lambda, Expr witness)
-  //  throw(TypeCheckingException);
-
   /** Get the type of an expression */
   Type getType(Expr e, bool check = false)
     throw(TypeCheckingException);