6 files changed, 9 insertions, 28 deletions
diff --git a/src/options/options.h b/src/options/options.h
index 3f2d72b7e..1fc7ed51a 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -52,9 +52,6 @@ class CVC4_PUBLIC Options {
   /** The current Options in effect */
   static thread_local Options* s_current;
 
-  /** Listeners for options::forceLogicString being set. */
-  ListenerCollection d_forceLogicListeners;
-
   /** Listeners for notifyBeforeSearch. */
   ListenerCollection d_beforeSearchListeners;
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 5e98f8f5a..b145da639 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -74,10 +74,6 @@ void throwLazyBBUnsupported(theory::bv::SatSolverMode m)
 
 OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
 
-void OptionsHandler::notifyForceLogic(const std::string& option){
-  d_options->d_forceLogicListeners.notify();
-}
-
 void OptionsHandler::notifyBeforeSearch(const std::string& option)
 {
   try{
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 06f7ab6e4..7ae461fd8 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -174,9 +174,6 @@ public:
   decision::DecisionWeightInternal stringToDecisionWeightInternal(
       std::string option, std::string optarg);
 
-  /* smt/options_handlers.h */
-  void notifyForceLogic(const std::string& option);
-
   /**
    * Throws a ModalException if this option is being set after final
    * initialization.
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 1f7ba05fc..f67493f87 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -231,7 +231,6 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h
 Options::Options()
     : d_holder(new options::OptionsHolder())
     , d_handler(new options::OptionsHandler(this))
-    , d_forceLogicListeners()
     , d_beforeSearchListeners()
     , d_tlimitListeners()
     , d_tlimitPerListeners()
@@ -283,13 +282,6 @@ ListenerCollection::Registration* Options::registerAndNotify(
   return registration;
 }
 
-ListenerCollection::Registration* Options::registerForceLogicListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::forceLogicString);
-  return registerAndNotify(d_forceLogicListeners, listener, notify);
-}
-
 ListenerCollection::Registration* Options::registerBeforeSearchListener(
    Listener* listener)
 {
diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml
index 988bcb6eb..71074d420 100644
--- a/src/options/parser_options.toml
+++ b/src/options/parser_options.toml
@@ -65,3 +65,12 @@ header = "options/parser_options.h"
   category   = "undocumented"
   long       = "no-include-file"
   links      = ["--no-filesystem-access"]
+
+[[option]]
+  name       = "forceLogicString"
+  smt_name   = "force-logic"
+  category   = "expert"
+  long       = "force-logic=LOGIC"
+  type       = "std::string"
+  read_only  = true
+  help       = "set the logic, and override all further user attempts to change it"
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index e0041774a..72dfdd7f8 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -23,16 +23,6 @@ header = "options/smt_options.h"
   help       = "all dumping goes to FILE (instead of stdout)"
 
 [[option]]
-  name       = "forceLogicString"
-  smt_name   = "force-logic"
-  category   = "expert"
-  long       = "force-logic=LOGIC"
-  type       = "std::string"
-  notifies   = ["notifyForceLogic"]
-  read_only  = true
-  help       = "set the logic, and override all further user attempts to change it"
-
-[[option]]
   name       = "simplificationMode"
   smt_name   = "simplification-mode"
   category   = "regular"