5 files changed, 49 insertions, 3 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index dd0e34578..c711567ab 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -21,6 +21,7 @@ libcvc4_add_sources(
   language.h
   open_ostream.cpp
   open_ostream.h
+  option_exception.cpp
   option_exception.h
   options.h
   options_handler.cpp
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 54047efcc..498989c80 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -85,6 +85,7 @@ liboptions_la_SOURCES = \
 	language.h \
 	open_ostream.cpp \
 	open_ostream.h \
+	option_exception.cpp \
 	option_exception.h \
 	options.h \
 	options_handler.cpp \
diff --git a/src/options/option_exception.cpp b/src/options/option_exception.cpp
new file mode 100644
index 000000000..33e2e21d1
--- /dev/null
+++ b/src/options/option_exception.cpp
@@ -0,0 +1,21 @@
+/*********************                                                        */
+/*! \file option_exception.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Options-related exceptions
+ **
+ ** Options-related exceptions.
+ **/
+
+#include "options/option_exception.h"
+
+namespace CVC4 {
+const std::string OptionException::s_errPrefix = "Error in option parsing: ";
+}  // namespace CVC4
diff --git a/src/options/option_exception.h b/src/options/option_exception.h
index 97a9de770..63b8aa890 100644
--- a/src/options/option_exception.h
+++ b/src/options/option_exception.h
@@ -31,10 +31,20 @@ namespace CVC4 {
  */
 class CVC4_PUBLIC OptionException : public CVC4::Exception {
  public:
-  OptionException(const std::string& s)
-      : CVC4::Exception("Error in option parsing: " + s)
+  OptionException(const std::string& s) : CVC4::Exception(s_errPrefix + s) {}
+
+  /**
+   * Get the error message without the prefix that is automatically added for
+   * OptionExceptions.
+   */
+  std::string getRawMessage() const
   {
+    return getMessage().substr(s_errPrefix.size());
   }
+
+ private:
+  /** The string to be added in front of the actual error message */
+  static const std::string s_errPrefix;
 };/* class OptionException */
 
 /**
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 609713ce8..85a9747fe 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -265,7 +265,20 @@ ListenerCollection::Registration* Options::registerAndNotify(
   ListenerCollection::Registration* registration =
       collection.registerListener(listener);
   if(notify) {
-    listener->notify();
+    try
+    {
+      listener->notify();
+    }
+    catch (OptionException& e)
+    {
+      // It can happen that listener->notify() throws an OptionException. In
+      // that case, we have to make sure that we delete the registration of our
+      // listener before rethrowing the exception. Otherwise the
+      // ListenerCollection deconstructor will complain that not all
+      // registrations have been removed before invoking the deconstructor.
+      delete registration;
+      throw OptionException(e.getRawMessage());
+    }
   }
   return registration;
 }