1 files changed, 8 insertions, 16 deletions
diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
index 5b56933b5..4bd5239f6 100644
--- a/src/options/options_public_template.cpp
+++ b/src/options/options_public_template.cpp
@@ -211,27 +211,19 @@ namespace cvc5::options
     throw OptionException("Unrecognized option key or setting: " + name);
   }
 
-void setInternal(Options & opts, const std::string& name,
-                                 const std::string& optionarg)
-{
-  // clang-format off
-${setoption_handlers}$
-  // clang-format on
+  void set(
+      Options & opts, const std::string& name, const std::string& optionarg)
+  {
+    Trace("options") << "set option " << name << " = " << optionarg
+                     << std::endl;
+    // clang-format off
+  ${set_impl}$
+    // clang-format on
   }
   else
   {
     throw OptionException("Unrecognized option key or setting: " + name);
   }
-  Trace("options") << "user assigned option " << name << " = " << optionarg << std::endl;
-}
-
-void set(Options& opts, const std::string& name, const std::string& optionarg)
-{
-
-  Trace("options") << "setOption(" << name << ", " << optionarg << ")"
-                   << std::endl;
-  // first update this object
-  setInternal(opts, name, optionarg);
 }
 
 #if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)