1 files changed, 2 insertions, 2 deletions
diff --git a/src/options/options.h b/src/options/options.h
index 8ca713642..16210e1a3 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -114,13 +114,13 @@ class CVC4_PUBLIC Options {
    * Options cannot be copied as they are given an explicit list of
    * Listeners to respond to.
    */
-  Options(const Options& options) CVC4_UNDEFINED;
+  Options(const Options& options) = delete;
 
   /**
    * Options cannot be assigned as they are given an explicit list of
    * Listeners to respond to.
    */
-  Options& operator=(const Options& options) CVC4_UNDEFINED;
+  Options& operator=(const Options& options) = delete;
 
   static std::string formatThreadOptionException(const std::string& option);