5 files changed, 10 insertions, 10 deletions
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;