First part of options refactoring (#6428)

This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular

- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()

The removed methods are only used in few places with are changed to using Options::current().X() instead.

In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.

19 files changed, 461 insertions, 642 deletions

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index acb010a2e..18f190ff1 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -51,6 +51,7 @@ header = "options/bv_options.h"
   category   = "expert"
   long       = "bv-aig-simp=COMMAND"
   type       = "std::string"
+  default    = "\"balance;drw\""
   predicates = ["abcEnabledBuild"]
   help       = "abc command to run AIG simplifications (implies --bitblast-aig, default is \"balance;drw\")"
 
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 9c66c6b61..fa2a39b04 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -81,63 +81,35 @@ g_getopt_long_start = 256
 
 TPL_HOLDER_MACRO_NAME = 'CVC5_OPTIONS__{id}__FOR_OPTION_HOLDER'
 
-TPL_RUN_HANDLER = \
-"""template <> options::{name}__option_t::type runHandlerAndPredicates(
-    options::{name}__option_t,
-    std::string option,
-    std::string optionarg,
-    options::OptionsHandler* handler)
-{{
-  options::{name}__option_t::type retval = {handler};
-  {predicates}
-  return retval;
-}}"""
-
-TPL_DECL_ASSIGN = \
+TPL_IMPL_ASSIGN = \
 """template <> void Options::assign(
     options::{name}__option_t,
     std::string option,
-    std::string value);"""
-
-TPL_IMPL_ASSIGN = TPL_DECL_ASSIGN[:-1] + \
-"""
+    std::string optionarg)
 {{
-  d_holder->{name} =
-    runHandlerAndPredicates(options::{name}, option, value, d_handler);
+  auto parsedval = {handler};
+  {predicates}
+  d_holder->{name} = parsedval;
   d_holder->{name}__setByUser__ = true;
   Trace("options") << "user assigned option {name}" << std::endl;
 }}"""
 
-
-TPL_RUN_HANDLER_BOOL = \
-"""template <> void runBoolPredicates(
-    options::{name}__option_t,
-    std::string option,
-    bool b,
-    options::OptionsHandler* handler)
-{{
-  {predicates}
-}}"""
-
-TPL_DECL_ASSIGN_BOOL = \
+TPL_IMPL_ASSIGN_BOOL = \
 """template <> void Options::assignBool(
     options::{name}__option_t,
     std::string option,
-    bool value);"""
-
-TPL_IMPL_ASSIGN_BOOL = TPL_DECL_ASSIGN_BOOL[:-1] + \
-"""
+    bool value)
 {{
-  runBoolPredicates(options::{name}, option, value, d_handler);
+  {predicates}
   d_holder->{name} = value;
   d_holder->{name}__setByUser__ = true;
   Trace("options") << "user assigned option {name}" << std::endl;
 }}"""
 
 TPL_CALL_ASSIGN_BOOL = \
-    '  options->assignBool(options::{name}, {option}, {value});'
+    '  assignBool(options::{name}, {option}, {value});'
 
-TPL_CALL_ASSIGN = '  options->assign(options::{name}, {option}, optionarg);'
+TPL_CALL_ASSIGN = '  assign(options::{name}, {option}, optionarg);'
 
 TPL_CALL_SET_OPTION = 'setOption(std::string("{smtname}"), ("{value}"));'
 
@@ -157,9 +129,7 @@ TPL_OPTION_STRUCT_RW = \
 {{
   typedef {type} type;
   type operator()() const;
-  bool wasSetByUser() const;
-  void set(const type& v);
-  const char* getName() const;
+  static constexpr const char* name = "{long_name}";
 }} thread_local {name};"""
 
 TPL_OPTION_STRUCT_RO = \
@@ -167,20 +137,18 @@ TPL_OPTION_STRUCT_RO = \
 {{
   typedef {type} type;
   type operator()() const;
-  bool wasSetByUser() const;
-  const char* getName() const;
+  static constexpr const char* name = "{long_name}";
 }} thread_local {name};"""
 
 
 TPL_DECL_SET = \
-"""template <> void Options::set(
-    options::{name}__option_t,
-    const options::{name}__option_t::type& x);"""
+"""template <> options::{name}__option_t::type& Options::ref(
+    options::{name}__option_t);"""
 
 TPL_IMPL_SET = TPL_DECL_SET[:-1] + \
 """
 {{
-  d_holder->{name} = x;
+    return d_holder->{name};
 }}"""
 
 
@@ -206,32 +174,12 @@ TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \
 
 # Option specific methods
 
-TPL_IMPL_OPTION_SET = \
-"""inline void {name}__option_t::set(const {name}__option_t::type& v)
-{{
-  Options::current()->set(*this, v);
-}}"""
-
 TPL_IMPL_OP_PAR = \
 """inline {name}__option_t::type {name}__option_t::operator()() const
 {{
-  return (*Options::current())[*this];
-}}"""
-
-TPL_IMPL_OPTION_WAS_SET_BY_USER = \
-"""inline bool {name}__option_t::wasSetByUser() const
-{{
-  return Options::current()->wasSetByUser(*this);
-}}"""
-
-TPL_IMPL_GET_NAME = \
-"""inline const char* {name}__option_t::getName() const
-{{
-  return "{long_name}";
+  return Options::current()[*this];
 }}"""
 
-
-
 # Mode templates
 TPL_DECL_MODE_ENUM = \
 """
@@ -242,16 +190,14 @@ enum class {type}
 
 TPL_DECL_MODE_FUNC = \
 """
-std::ostream&
-operator<<(std::ostream& os, {type} mode);"""
+std::ostream& operator<<(std::ostream& os, {type} mode);"""
 
 TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(";")] + \
 """
 {{
-  os << "{type}::";
   switch(mode) {{{cases}
     default:
-        Unreachable();
+      Unreachable();
   }}
   return os;
 }}
@@ -260,13 +206,11 @@ TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(";")] + \
 TPL_IMPL_MODE_CASE = \
 """
     case {type}::{enum}:
-      os << "{enum}";
-      break;"""
+      return os << "{type}::{enum}";"""
 
 TPL_DECL_MODE_HANDLER = \
 """
-{type}
-stringTo{type}(const std::string& option, const std::string& optarg);"""
+{type} stringTo{type}(const std::string& optarg);"""
 
 TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \
 """
@@ -274,14 +218,11 @@ TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \
   {cases}
   else if (optarg == "help")
   {{
-    puts({help});
-    exit(1);
-  }}
-  else
-  {{
-    throw OptionException(std::string("unknown option for --{long}: `") +
-                          optarg + "'.  Try --{long}=help.");
+    std::cerr << {help};
+    std::exit(1);
   }}
+  throw OptionException(std::string("unknown option for --{long}: `") +
+                        optarg + "'.  Try --{long}=help.");
 }}
 """
 
@@ -513,7 +454,11 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
 
         # Generate module declaration
         tpl_decl = TPL_OPTION_STRUCT_RO if option.read_only else TPL_OPTION_STRUCT_RW
-        decls.append(tpl_decl.format(name=option.name, type=option.type))
+        if option.long:
+            long_name = option.long.split('=')[0]
+        else:
+            long_name = ""
+        decls.append(tpl_decl.format(name=option.name, type=option.type, long_name = long_name))
 
         # Generate module specialization
         if not option.read_only:
@@ -521,11 +466,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         specs.append(TPL_DECL_OP_BRACKET.format(name=option.name))
         specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name))
 
-        if option.type == 'bool':
-            specs.append(TPL_DECL_ASSIGN_BOOL.format(name=option.name))
-        else:
-            specs.append(TPL_DECL_ASSIGN.format(name=option.name))
-
         if option.long and option.type not in ['bool', 'void'] and \
            '=' not in option.long:
             die("module '{}': option '{}' with type '{}' needs an argument " \
@@ -539,15 +479,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
 
         # Generate module inlines
         inls.append(TPL_IMPL_OP_PAR.format(name=option.name))
-        inls.append(TPL_IMPL_OPTION_WAS_SET_BY_USER.format(name=option.name))
-        if not option.read_only:
-            inls.append(TPL_IMPL_OPTION_SET.format(name=option.name))
-        if option.long:
-            long_name = option.long.split('=')[0]
-        else:
-            long_name = ""
-        inls.append(TPL_IMPL_GET_NAME.format(
-                        name=option.name, long_name=long_name))
 
 
         ### Generate code for {module.name}_options.cpp
@@ -704,12 +635,12 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
             handler = None
             if option.handler:
                 if option.type == 'void':
-                    handler = 'handler->{}(option)'.format(option.handler)
+                    handler = 'd_handler->{}(option)'.format(option.handler)
                 else:
                     handler = \
-                        'handler->{}(option, optionarg)'.format(option.handler)
+                        'd_handler->{}(option, optionarg)'.format(option.handler)
             elif option.mode:
-                handler = 'stringTo{}(option, optionarg)'.format(option.type)
+                handler = 'stringTo{}(optionarg)'.format(option.type)
             elif option.type != 'bool':
                 handler = \
                     'handleOption<{}>(option, optionarg)'.format(option.type)
@@ -719,12 +650,12 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
             if option.predicates:
                 if option.type == 'bool':
                     predicates = \
-                        ['handler->{}(option, b);'.format(x) \
+                        ['d_handler->{}(option, value);'.format(x) \
                             for x in option.predicates]
                 else:
                     assert option.type != 'void'
                     predicates = \
-                        ['handler->{}(option, retval);'.format(x) \
+                        ['d_handler->{}(option, parsedval);'.format(x) \
                             for x in option.predicates]
 
             # Generate options_handler and getopt_long
@@ -867,24 +798,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
                     options_getoptions.append(s)
 
 
-                # Define runBoolPredicates/runHandlerAndPredicates
-                tpl = None
-                if option.type == 'bool':
-                    if predicates:
-                        assert handler is None
-                        tpl = TPL_RUN_HANDLER_BOOL
-                elif option.short or option.long:
-                    assert option.type != 'void'
-                    assert handler
-                    tpl = TPL_RUN_HANDLER
-                if tpl:
-                    custom_handlers.append(
-                        tpl.format(
-                            name=option.name,
-                            handler=handler,
-                            predicates='\n'.join(predicates)
-                        ))
-
                 # Define handler assign/assignBool
                 tpl = None
                 if option.type == 'bool':
@@ -893,7 +806,9 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
                     tpl = TPL_IMPL_ASSIGN
                 if tpl:
                     custom_handlers.append(tpl.format(
-                        name=option.name
+                        name=option.name,
+                        handler=handler,
+                        predicates='\n'.join(predicates)
                     ))
 
                 # Default option values
diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp
index 3b928dba0..0de77e8a6 100644
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -19,6 +19,8 @@
 #include "options/options_holder.h"
 #include "base/check.h"
 
+#include <iostream>
+
 // clang-format off
 namespace cvc5 {
 
diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp
index 3b13c42e2..9ebea6da0 100644
--- a/src/options/open_ostream.cpp
+++ b/src/options/open_ostream.cpp
@@ -20,6 +20,7 @@
 
 
 #include <cerrno>
+#include <fstream>
 #include <iostream>
 #include <ostream>
 #include <sstream>
diff --git a/src/options/options.h b/src/options/options.h
index 67707c990..b249c90ed 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -18,8 +18,7 @@
 #ifndef CVC5__OPTIONS__OPTIONS_H
 #define CVC5__OPTIONS__OPTIONS_H
 
-#include <fstream>
-#include <ostream>
+#include <iosfwd>
 #include <string>
 #include <vector>
 
@@ -77,9 +76,6 @@ class CVC5_EXPORT Options
 
   static std::string formatThreadOptionException(const std::string& option);
 
-  static const size_t s_maxoptlen = 128;
-  static const unsigned s_preemptAdditional = 6;
-
 public:
  class OptionsScope
  {
@@ -102,8 +98,8 @@ public:
   }
 
   /** Get the current Options in effect */
-  static inline Options* current() {
-    return s_current;
+  static inline Options& current() {
+    return *s_current;
   }
 
   Options(OptionsListener* ol = nullptr);
@@ -117,15 +113,39 @@ public:
   void copyValues(const Options& options);
 
   /**
-   * Set the value of the given option.  Use of this default
-   * implementation causes a compile-time error; write-able
-   * options specialize this template with a real implementation.
+   * Set the value of the given option.  Uses `ref()`, which causes a
+   * compile-time error if the given option is read-only.
+   */
+  template <class T>
+  void set(T t, const typename T::type& val) {
+    ref(t) = val;
+  }
+
+  /**
+   * Set the default value of the given option. Is equivalent to calling `set()`
+   * if `wasSetByUser()` returns false. Uses `ref()`, which causes a compile-time
+   * error if the given option is read-only.
+   */
+  template <class T>
+  void setDefault(T t, const typename T::type& val)
+  {
+    if (!wasSetByUser(t))
+    {
+      ref(t) = val;
+    }
+  }
+
+  /**
+   * Get a non-const reference to the value of the given option. Causes a
+   * compile-time error if the given option is read-only. Writeable options
+   * specialize this template with a real implementation.
    */
   template <class T>
-  void set(T, const typename T::type&) {
-    // Flag a compile-time error.  Write-able options specialize
-    // this template to provide an implementation.
-    T::you_are_trying_to_assign_to_a_read_only_option;
+  typename T::type& ref(T) {
+    // Flag a compile-time error.
+    T::you_are_trying_to_get_nonconst_access_to_a_read_only_option;
+    // Ensure the compiler does not complain about the return value.
+    return *static_cast<typename T::type*>(nullptr);
   }
 
   /**
@@ -297,8 +317,7 @@ public:
    *
    * Preconditions: options, extender and nonoptions are non-null.
    */
-  static void parseOptionsRecursive(Options* options,
-                                    int argc,
+  void parseOptionsRecursive(int argc,
                                     char* argv[],
                                     std::vector<std::string>* nonoptions);
 }; /* class Options */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 0e2315aa0..dd555ab56 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -159,14 +159,11 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
           || m == SatSolverMode::KISSAT))
   {
     if (options::bitblastMode() == options::BitblastMode::LAZY
-        && options::bitblastMode.wasSetByUser())
+        && Options::current().wasSetByUser(options::bitblastMode))
     {
       throwLazyBBUnsupported(m);
     }
-    if (!options::bitvectorToBool.wasSetByUser())
-    {
-      options::bitvectorToBool.set(true);
-    }
+    Options::current().setDefault(options::bitvectorToBool, true);
   }
 }
 
@@ -174,23 +171,10 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
 {
   if (m == options::BitblastMode::LAZY)
   {
-    if (!options::bitvectorPropagate.wasSetByUser())
-    {
-      options::bitvectorPropagate.set(true);
-    }
-    if (!options::bitvectorEqualitySolver.wasSetByUser())
-    {
-      options::bitvectorEqualitySolver.set(true);
-    }
-
-    if (!options::bitvectorInequalitySolver.wasSetByUser())
-    {
-      options::bitvectorInequalitySolver.set(true);
-    }
-    if (!options::bitvectorAlgebraicSolver.wasSetByUser())
-    {
-      options::bitvectorAlgebraicSolver.set(true);
-    }
+    Options::current().setDefault(options::bitvectorPropagate, true);
+    Options::current().setDefault(options::bitvectorEqualitySolver, true);
+    Options::current().setDefault(options::bitvectorInequalitySolver, true);
+    Options::current().setDefault(options::bitvectorAlgebraicSolver, true);
     if (options::bvSatSolver() != options::SatSolverMode::MINISAT)
     {
       throwLazyBBUnsupported(options::bvSatSolver());
@@ -198,27 +182,21 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
   }
   else if (m == BitblastMode::EAGER)
   {
-    if (!options::bitvectorToBool.wasSetByUser())
-    {
-      options::bitvectorToBool.set(true);
-    }
+    Options::current().setDefault(options::bitvectorToBool, true);
   }
 }
 
 void OptionsHandler::setBitblastAig(std::string option, bool arg)
 {
   if(arg) {
-    if(options::bitblastMode.wasSetByUser()) {
+    if(Options::current().wasSetByUser(options::bitblastMode)) {
       if (options::bitblastMode() != options::BitblastMode::EAGER)
       {
         throw OptionException("bitblast-aig must be used with eager bitblaster");
       }
     } else {
-      options::BitblastMode mode = stringToBitblastMode("", "eager");
-      options::bitblastMode.set(mode);
-    }
-    if(!options::bitvectorAigSimplifications.wasSetByUser()) {
-      options::bitvectorAigSimplifications.set("balance;drw");
+      options::BitblastMode mode = stringToBitblastMode("eager");
+      Options::current().set(options::bitblastMode, mode);
     }
   }
 }
@@ -253,13 +231,13 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
 // decision/options_handlers.h
 void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m)
 {
-  options::decisionStopOnly.set(m == DecisionMode::RELEVANCY);
+  Options::current().set(options::decisionStopOnly, m == DecisionMode::RELEVANCY);
 }
 
 void OptionsHandler::setProduceAssertions(std::string option, bool value)
 {
-  options::produceAssertions.set(value);
-  options::interactiveMode.set(value);
+  Options::current().set(options::produceAssertions, value);
+  Options::current().set(options::interactiveMode, value);
 }
 
 void OptionsHandler::setStats(const std::string& option, bool value)
@@ -278,22 +256,22 @@ void OptionsHandler::setStats(const std::string& option, bool value)
   std::string opt = option.substr(2);
   if (value)
   {
-    if (opt == options::statisticsAll.getName())
+    if (opt == options::statisticsAll.name)
     {
       d_options->d_holder->statistics = true;
     }
-    else if (opt == options::statisticsEveryQuery.getName())
+    else if (opt == options::statisticsEveryQuery.name)
     {
       d_options->d_holder->statistics = true;
     }
-    else if (opt == options::statisticsExpert.getName())
+    else if (opt == options::statisticsExpert.name)
     {
       d_options->d_holder->statistics = true;
     }
   }
   else
   {
-    if (opt == options::statistics.getName())
+    if (opt == options::statistics.name)
     {
       d_options->d_holder->statisticsAll = false;
       d_options->d_holder->statisticsEveryQuery = false;
@@ -508,7 +486,7 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
                                                       std::string optarg)
 {
   if(optarg == "help") {
-    options::languageHelp.set(true);
+    Options::current().set(options::languageHelp, true);
     return language::output::LANG_AUTO;
   }
 
@@ -526,7 +504,7 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
                                                     std::string optarg)
 {
   if(optarg == "help") {
-    options::languageHelp.set(true);
+    Options::current().set(options::languageHelp, true);
     return language::input::LANG_AUTO;
   }
 
@@ -571,12 +549,12 @@ void OptionsHandler::setVerbosity(std::string option, int value)
 }
 
 void OptionsHandler::increaseVerbosity(std::string option) {
-  options::verbosity.set(options::verbosity() + 1);
+  Options::current().set(options::verbosity, options::verbosity() + 1);
   setVerbosity(option, options::verbosity());
 }
 
 void OptionsHandler::decreaseVerbosity(std::string option) {
-  options::verbosity.set(options::verbosity() - 1);
+  Options::current().set(options::verbosity, options::verbosity() - 1);
   setVerbosity(option, options::verbosity());
 }
 
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index f70c1ce3b..6ad537240 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -179,7 +179,7 @@ std::string Options::getBinaryName() const{
 }
 
 std::ostream* Options::currentGetOut() {
-  return current()->getOut();
+  return current().getOut();
 }
 
 
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index f24f83b2b..4493f6094 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -408,7 +408,7 @@ std::vector<std::string> Options::parseOptions(Options* options,
   options->d_holder->binary_name = std::string(progName);
 
   std::vector<std::string> nonoptions;
-  parseOptionsRecursive(options, argc, argv, &nonoptions);
+  options->parseOptionsRecursive(argc, argv, &nonoptions);
   if(Debug.isOn("options")){
     for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
           iend = nonoptions.end(); i != iend; ++i){
@@ -419,8 +419,7 @@ std::vector<std::string> Options::parseOptions(Options* options,
   return nonoptions;
 }
 
-void Options::parseOptionsRecursive(Options* options,
-                                    int argc,
+void Options::parseOptionsRecursive(int argc,
                                     char* argv[],
                                     std::vector<std::string>* nonoptions)
 {
@@ -434,9 +433,6 @@ void Options::parseOptionsRecursive(Options* options,
     }
   }
 
-  // Having this synonym simplifies the generation code in mkoptions.
-  options::OptionsHandler* handler = options->d_handler;
-
   // Reset getopt(), in the case of multiple calls to parseOptions().
   // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
   optind = 0;
@@ -597,7 +593,6 @@ void Options::setOptionInternal(const std::string& key,
                                 const std::string& optionarg)
 {
   options::OptionsHandler* handler = d_handler;
-  Options* options = this;
   ${setoption_handlers}$
   throw UnrecognizedOptionException(key);
 }
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 19d14eb09..927fd1d13 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -127,25 +127,31 @@ void Printer::toStream(std::ostream& out, const SkolemList& sks) const
 
 Printer* Printer::getPrinter(OutputLanguage lang)
 {
-  if(lang == language::output::LANG_AUTO) {
-  // Infer the language to use for output.
-  //
-  // Options can be null in certain circumstances (e.g., when printing
-  // the singleton "null" expr.  So we guard against segfault
-  if(not Options::isCurrentNull()) {
-    if(options::outputLanguage.wasSetByUser()) {
-      lang = options::outputLanguage();
+  if (lang == language::output::LANG_AUTO)
+  {
+    // Infer the language to use for output.
+    //
+    // Options can be null in certain circumstances (e.g., when printing
+    // the singleton "null" expr.  So we guard against segfault
+    if (not Options::isCurrentNull())
+    {
+      if (Options::current().wasSetByUser(options::outputLanguage))
+      {
+        lang = options::outputLanguage();
+      }
+      if (lang == language::output::LANG_AUTO
+          && Options::current().wasSetByUser(options::inputLanguage))
+      {
+        lang = language::toOutputLanguage(options::inputLanguage());
+      }
+    }
+    if (lang == language::output::LANG_AUTO)
+    {
+      lang = language::output::LANG_SMTLIB_V2_6;  // default
     }
-    if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) {
-      lang = language::toOutputLanguage(options::inputLanguage());
-     }
-   }
-   if (lang == language::output::LANG_AUTO)
-   {
-     lang = language::output::LANG_SMTLIB_V2_6;  // default
-   }
   }
-  if(d_printers[lang] == NULL) {
+  if (d_printers[lang] == nullptr)
+  {
     d_printers[lang] = makePrinter(lang);
   }
   return d_printers[lang].get();
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index e8179c5fe..74cbadfc2 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -76,7 +76,7 @@ SimpSolver::SimpSolver(cvc5::prop::TheoryProxy* proxy,
       n_touched(0)
 {
     if(options::minisatUseElim() &&
-       options::minisatUseElim.wasSetByUser() &&
+       Options::current().wasSetByUser(options::minisatUseElim) &&
        enableIncremental) {
         WarningOnce() << "Incremental mode incompatible with --minisat-elim" << std::endl;
     }
diff --git a/src/smt/env.h b/src/smt/env.h
index 209b6f3e7..12e0983cb 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -87,6 +87,12 @@ class Env
   /** Get a pointer to the underlying dump manager. */
   smt::DumpManager* getDumpManager();
 
+  template <typename Opt>
+  const auto& getOption(Opt opt) const
+  {
+    return d_options[opt];
+  }
+
   /** Get the options object (const version only) owned by this Env. */
   const Options& getOptions() const;
 
diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp
index 31bcc5f2f..b2f02b34d 100644
--- a/src/smt/managed_ostreams.cpp
+++ b/src/smt/managed_ostreams.cpp
@@ -90,7 +90,7 @@ ManagedRegularOutputChannel::~ManagedRegularOutputChannel() {
   // to null_os. Consult RegularOutputChannelListener for the list of
   // channels.
   if(options::err() == getManagedOstream()){
-    options::err.set(&null_os);
+    Options::current().set(options::err, &null_os);
   }
 }
 
@@ -114,7 +114,7 @@ ManagedDiagnosticOutputChannel::~ManagedDiagnosticOutputChannel() {
   // to null_os. Consult DiagnosticOutputChannelListener for the list of
   // channels.
   if(options::err() == getManagedOstream()){
-    options::err.set(&null_os);
+    Options::current().set(options::err, &null_os);
   }
 
   if(Debug.getStreamPointer() == getManagedOstream()) {
diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index c84854992..05bad2727 100644
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -33,31 +33,31 @@ OptionsManager::OptionsManager(Options* opts) : d_options(opts)
   // set options that must take effect immediately
   if (opts->wasSetByUser(options::defaultExprDepth))
   {
-    notifySetOption(options::defaultExprDepth.getName());
+    notifySetOption(options::defaultExprDepth.name);
   }
   if (opts->wasSetByUser(options::defaultDagThresh))
   {
-    notifySetOption(options::defaultDagThresh.getName());
+    notifySetOption(options::defaultDagThresh.name);
   }
   if (opts->wasSetByUser(options::dumpModeString))
   {
-    notifySetOption(options::dumpModeString.getName());
+    notifySetOption(options::dumpModeString.name);
   }
   if (opts->wasSetByUser(options::printSuccess))
   {
-    notifySetOption(options::printSuccess.getName());
+    notifySetOption(options::printSuccess.name);
   }
   if (opts->wasSetByUser(options::diagnosticChannelName))
   {
-    notifySetOption(options::diagnosticChannelName.getName());
+    notifySetOption(options::diagnosticChannelName.name);
   }
   if (opts->wasSetByUser(options::regularChannelName))
   {
-    notifySetOption(options::regularChannelName.getName());
+    notifySetOption(options::regularChannelName.name);
   }
   if (opts->wasSetByUser(options::dumpToFileName))
   {
-    notifySetOption(options::dumpToFileName.getName());
+    notifySetOption(options::dumpToFileName.name);
   }
   // set this as a listener to be notified of options changes from now on
   opts->setListener(this);
@@ -69,7 +69,7 @@ void OptionsManager::notifySetOption(const std::string& key)
 {
   Trace("smt") << "SmtEnginePrivate::notifySetOption(" << key << ")"
                << std::endl;
-  if (key == options::defaultExprDepth.getName())
+  if (key == options::defaultExprDepth.name)
   {
     int depth = (*d_options)[options::defaultExprDepth];
     Debug.getStream() << expr::ExprSetDepth(depth);
@@ -80,7 +80,7 @@ void OptionsManager::notifySetOption(const std::string& key)
     Warning.getStream() << expr::ExprSetDepth(depth);
     // intentionally exclude Dump stream from this list
   }
-  else if (key == options::defaultDagThresh.getName())
+  else if (key == options::defaultDagThresh.name)
   {
     int dag = (*d_options)[options::defaultDagThresh];
     Debug.getStream() << expr::ExprDag(dag);
@@ -91,12 +91,12 @@ void OptionsManager::notifySetOption(const std::string& key)
     Warning.getStream() << expr::ExprDag(dag);
     Dump.getStream() << expr::ExprDag(dag);
   }
-  else if (key == options::dumpModeString.getName())
+  else if (key == options::dumpModeString.name)
   {
     const std::string& value = (*d_options)[options::dumpModeString];
     Dump.setDumpFromString(value);
   }
-  else if (key == options::printSuccess.getName())
+  else if (key == options::printSuccess.name)
   {
     bool value = (*d_options)[options::printSuccess];
     Debug.getStream() << Command::printsuccess(value);
@@ -107,15 +107,15 @@ void OptionsManager::notifySetOption(const std::string& key)
     Warning.getStream() << Command::printsuccess(value);
     *options::out() << Command::printsuccess(value);
   }
-  else if (key == options::regularChannelName.getName())
+  else if (key == options::regularChannelName.name)
   {
     d_managedRegularChannel.set(options::regularChannelName());
   }
-  else if (key == options::diagnosticChannelName.getName())
+  else if (key == options::diagnosticChannelName.name)
   {
     d_managedDiagnosticChannel.set(options::diagnosticChannelName());
   }
-  else if (key == options::dumpToFileName.getName())
+  else if (key == options::dumpToFileName.name)
   {
     d_managedDumpChannel.set(options::dumpToFileName());
   }
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 047dbfea6..ed5d986be 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -49,84 +49,85 @@ namespace smt {
 
 void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 {
+  Options& opts = Options::current();
   // implied options
   if (options::debugCheckModels())
   {
-    options::checkModels.set(true);
+    opts.set(options::checkModels, true);
   }
   if (options::checkModels() || options::dumpModels())
   {
-    options::produceModels.set(true);
+    opts.set(options::produceModels, true);
   }
   if (options::checkModels())
   {
-    options::produceAssignments.set(true);
+    opts.set(options::produceAssignments, true);
   }
   // unsat cores and proofs shenanigans
   if (options::dumpUnsatCoresFull())
   {
-    options::dumpUnsatCores.set(true);
+    opts.set(options::dumpUnsatCores, true);
   }
   if (options::checkUnsatCores() || options::dumpUnsatCores()
       || options::unsatAssumptions()
       || options::unsatCoresMode() != options::UnsatCoresMode::OFF)
   {
-    options::unsatCores.set(true);
+    opts.set(options::unsatCores, true);
   }
   if (options::unsatCores()
       && options::unsatCoresMode() == options::UnsatCoresMode::OFF)
   {
-    if (options::unsatCoresMode.wasSetByUser())
+    if (opts.wasSetByUser(options::unsatCoresMode))
     {
       Notice()
           << "Overriding OFF unsat-core mode since cores were requested..\n";
     }
-    options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF);
+    opts.set(options::unsatCoresMode, options::UnsatCoresMode::OLD_PROOF);
   }
 
   if (options::checkProofs() || options::dumpProofs())
   {
-    options::produceProofs.set(true);
+    opts.set(options::produceProofs, true);
   }
 
   if (options::produceProofs()
       && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
   {
-    if (options::unsatCoresMode.wasSetByUser())
+    if (opts.wasSetByUser(options::unsatCoresMode))
     {
       Notice() << "Forcing full-proof mode for unsat cores mode since proofs "
                   "were requested.\n";
     }
     // enable unsat cores, because they are available as a consequence of proofs
-    options::unsatCores.set(true);
-    options::unsatCoresMode.set(options::UnsatCoresMode::FULL_PROOF);
+    opts.set(options::unsatCores, true);
+    opts.set(options::unsatCoresMode, options::UnsatCoresMode::FULL_PROOF);
   }
 
   // set proofs on if not yet set
   if (options::unsatCores() && !options::produceProofs()
       && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF)
   {
-    if (options::produceProofs.wasSetByUser())
+    if (opts.wasSetByUser(options::produceProofs))
     {
       Notice()
           << "Forcing proof production since new unsat cores were requested.\n";
     }
-    options::produceProofs.set(true);
+    opts.set(options::produceProofs, true);
   }
 
   // if unsat cores are disabled, then unsat cores mode should be OFF
   Assert(options::unsatCores()
          == (options::unsatCoresMode() != options::UnsatCoresMode::OFF));
 
-  if (options::bitvectorAigSimplifications.wasSetByUser())
+  if (opts.wasSetByUser(options::bitvectorAigSimplifications))
   {
     Notice() << "SmtEngine: setting bitvectorAig" << std::endl;
-    options::bitvectorAig.set(true);
+    opts.set(options::bitvectorAig, true);
   }
-  if (options::bitvectorAlgebraicBudget.wasSetByUser())
+  if (opts.wasSetByUser(options::bitvectorAlgebraicBudget))
   {
     Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl;
-    options::bitvectorAlgebraicSolver.set(true);
+    opts.set(options::bitvectorAlgebraicSolver, true);
   }
 
   bool isSygus = language::isInputLangSygus(options::inputLanguage());
@@ -138,8 +139,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
         && (logic.isTheoryEnabled(THEORY_ARRAYS)
             || logic.isTheoryEnabled(THEORY_UF)))
     {
-      if (options::bitblastMode.wasSetByUser()
-          || options::produceModels.wasSetByUser())
+      if (opts.wasSetByUser(options::bitblastMode)
+          || opts.wasSetByUser(options::produceModels))
       {
         throw OptionException(std::string(
             "Eager bit-blasting currently does not support model generation "
@@ -148,11 +149,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       }
       Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
                << "generation" << std::endl;
-      options::bitblastMode.set(options::BitblastMode::LAZY);
+      opts.set(options::bitblastMode, options::BitblastMode::LAZY);
     }
     else if (!options::incrementalSolving())
     {
-      options::ackermann.set(true);
+      opts.set(options::ackermann, true);
     }
 
     if (options::incrementalSolving() && !logic.isPure(THEORY_BV))
@@ -164,7 +165,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
     // Force lazy solver since we don't handle EAGER_ATOMS in the
     // BVSolver::BITBLAST solver.
-    options::bvSolver.set(options::BVSolver::LAZY);
+    opts.set(options::bvSolver, options::BVSolver::LAZY);
   }
 
   /* Only BVSolver::LAZY natively supports int2bv and nat2bv, for other solvers
@@ -172,14 +173,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (options::bvSolver() == options::BVSolver::SIMPLE
       || options::bvSolver() == options::BVSolver::BITBLAST)
   {
-    options::bvLazyReduceExtf.set(false);
-    options::bvLazyRewriteExtf.set(false);
+    opts.set(options::bvLazyReduceExtf, false);
+    opts.set(options::bvLazyRewriteExtf, false);
   }
 
   /* Disable bit-level propagation by default for the BITBLAST solver. */
   if (options::bvSolver() == options::BVSolver::BITBLAST)
   {
-    options::bitvectorPropagate.set(false);
+    opts.set(options::bitvectorPropagate, false);
   }
 
   if (options::solveIntAsBV() > 0)
@@ -232,14 +233,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       && (logic.isTheoryEnabled(THEORY_ARRAYS)
           || logic.isTheoryEnabled(THEORY_UF)))
   {
-    if (options::produceModels.wasSetByUser())
+    if (opts.wasSetByUser(options::produceModels))
     {
       throw OptionException(std::string(
           "Ackermannization currently does not support model generation."));
     }
     Notice() << "SmtEngine: turn off ackermannization to support model"
              << "generation" << std::endl;
-    options::ackermann.set(false);
+    opts.set(options::ackermann, false);
   }
 
   if (options::ackermann())
@@ -275,9 +276,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // this by default.
   if (options::doITESimp())
   {
-    if (!options::earlyIteRemoval.wasSetByUser())
+    if (!opts.wasSetByUser(options::earlyIteRemoval))
     {
-      options::earlyIteRemoval.set(true);
+      opts.set(options::earlyIteRemoval, true);
     }
   }
 
@@ -288,7 +289,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     // If the user explicitly set a logic that includes strings, but is not
     // the generic "ALL" logic, then enable stringsExp.
-    options::stringExp.set(true);
+    opts.set(options::stringExp, true);
   }
   if (options::stringExp() || !options::stringLazyPreproc())
   {
@@ -302,9 +303,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                    << std::endl;
     }
     // We require bounded quantifier handling.
-    if (!options::fmfBound.wasSetByUser())
+    if (!opts.wasSetByUser(options::fmfBound))
     {
-      options::fmfBound.set(true);
+      opts.set(options::fmfBound, true);
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
     // Note we allow E-matching by default to support combinations of sequences
@@ -325,9 +326,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
   {
     // no fine-graininess
-    if (!options::proofGranularityMode.wasSetByUser())
+    if (!opts.wasSetByUser(options::proofGranularityMode))
     {
-      options::proofGranularityMode.set(options::ProofGranularityMode::OFF);
+      opts.set(options::proofGranularityMode, options::ProofGranularityMode::OFF);
     }
   }
 
@@ -340,9 +341,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       logic.lock();
     }
     // Allows to answer sat more often by default.
-    if (!options::fmfBound.wasSetByUser())
+    if (!opts.wasSetByUser(options::fmfBound))
     {
-      options::fmfBound.set(true);
+      opts.set(options::fmfBound, true);
       Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl;
     }
   }
@@ -383,24 +384,24 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // if we requiring disabling proofs, disable them now
   if (disableProofs && options::produceProofs())
   {
-    options::unsatCores.set(false);
-    options::unsatCoresMode.set(options::UnsatCoresMode::OFF);
+    opts.set(options::unsatCores, false);
+    opts.set(options::unsatCoresMode, options::UnsatCoresMode::OFF);
     if (options::produceProofs())
     {
       Notice() << "SmtEngine: turning off produce-proofs." << std::endl;
     }
-    options::produceProofs.set(false);
-    options::checkProofs.set(false);
-    options::proofEagerChecking.set(false);
+    opts.set(options::produceProofs, false);
+    opts.set(options::checkProofs, false);
+    opts.set(options::proofEagerChecking, false);
   }
 
   // sygus core connective requires unsat cores
   if (options::sygusCoreConnective())
   {
-    options::unsatCores.set(true);
+    opts.set(options::unsatCores, true);
     if (options::unsatCoresMode() == options::UnsatCoresMode::OFF)
     {
-      options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF);
+      opts.set(options::unsatCoresMode, options::UnsatCoresMode::OLD_PROOF);
     }
   }
 
@@ -414,7 +415,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     Notice() << "SmtEngine: turning on produce-assertions to support "
              << "option requiring assertions." << std::endl;
-    options::produceAssertions.set(true);
+    opts.set(options::produceAssertions, true);
   }
 
   // whether we want to force safe unsat cores, i.e., if we are in the OLD_PROOF
@@ -429,7 +430,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::unconstrainedSimp())
     {
-      if (options::unconstrainedSimp.wasSetByUser())
+      if (opts.wasSetByUser(options::unconstrainedSimp))
       {
         throw OptionException(
             "unconstrained simplification not supported with old unsat "
@@ -438,13 +439,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       Notice() << "SmtEngine: turning off unconstrained simplification to "
                   "support old unsat cores/incremental solving"
                << std::endl;
-      options::unconstrainedSimp.set(false);
+      opts.set(options::unconstrainedSimp, false);
     }
   }
   else
   {
     // Turn on unconstrained simplification for QF_AUFBV
-    if (!options::unconstrainedSimp.wasSetByUser())
+    if (!opts.wasSetByUser(options::unconstrainedSimp))
     {
       bool uncSimp = !logic.isQuantified() && !options::produceModels()
                      && !options::produceAssignments()
@@ -454,7 +455,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                      && !logic.isTheoryEnabled(THEORY_ARITH);
       Trace("smt") << "setting unconstrained simplification to " << uncSimp
                    << std::endl;
-      options::unconstrainedSimp.set(uncSimp);
+      opts.set(options::unconstrainedSimp, uncSimp);
     }
   }
 
@@ -462,7 +463,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::sygusInference())
     {
-      if (options::sygusInference.wasSetByUser())
+      if (opts.wasSetByUser(options::sygusInference))
       {
         throw OptionException(
             "sygus inference not supported with incremental solving");
@@ -470,7 +471,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       Notice() << "SmtEngine: turning off sygus inference to support "
                   "incremental solving"
                << std::endl;
-      options::sygusInference.set(false);
+      opts.set(options::sygusInference, false);
     }
   }
 
@@ -482,7 +483,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
      * Therefore, we enable bv-to-bool, which runs before
      * the translation to integers.
      */
-    options::bitvectorToBool.set(true);
+    opts.set(options::bitvectorToBool, true);
   }
 
   // Disable options incompatible with unsat cores or output an error if enabled
@@ -491,7 +492,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::simplificationMode() != options::SimplificationMode::NONE)
     {
-      if (options::simplificationMode.wasSetByUser())
+      if (opts.wasSetByUser(options::simplificationMode))
       {
         throw OptionException(
             "simplification not supported with old unsat cores");
@@ -499,101 +500,101 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       Notice() << "SmtEngine: turning off simplification to support unsat "
                   "cores"
                << std::endl;
-      options::simplificationMode.set(options::SimplificationMode::NONE);
+      opts.set(options::simplificationMode, options::SimplificationMode::NONE);
     }
 
     if (options::pbRewrites())
     {
-      if (options::pbRewrites.wasSetByUser())
+      if (opts.wasSetByUser(options::pbRewrites))
       {
         throw OptionException(
             "pseudoboolean rewrites not supported with old unsat cores");
       }
       Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
                   "old unsat cores\n";
-      options::pbRewrites.set(false);
+      opts.set(options::pbRewrites, false);
     }
 
     if (options::sortInference())
     {
-      if (options::sortInference.wasSetByUser())
+      if (opts.wasSetByUser(options::sortInference))
       {
         throw OptionException(
             "sort inference not supported with old unsat cores");
       }
       Notice() << "SmtEngine: turning off sort inference to support old unsat "
                   "cores\n";
-      options::sortInference.set(false);
+      opts.set(options::sortInference, false);
     }
 
     if (options::preSkolemQuant())
     {
-      if (options::preSkolemQuant.wasSetByUser())
+      if (opts.wasSetByUser(options::preSkolemQuant))
       {
         throw OptionException(
             "pre-skolemization not supported with old unsat cores");
       }
       Notice() << "SmtEngine: turning off pre-skolemization to support old "
                   "unsat cores\n";
-      options::preSkolemQuant.set(false);
+      opts.set(options::preSkolemQuant, false);
     }
 
     if (options::bitvectorToBool())
     {
-      if (options::bitvectorToBool.wasSetByUser())
+      if (opts.wasSetByUser(options::bitvectorToBool))
       {
         throw OptionException("bv-to-bool not supported with old unsat cores");
       }
       Notice() << "SmtEngine: turning off bitvector-to-bool to support old "
                   "unsat cores\n";
-      options::bitvectorToBool.set(false);
+      opts.set(options::bitvectorToBool, false);
     }
 
     if (options::boolToBitvector() != options::BoolToBVMode::OFF)
     {
-      if (options::boolToBitvector.wasSetByUser())
+      if (opts.wasSetByUser(options::boolToBitvector))
       {
         throw OptionException(
             "bool-to-bv != off not supported with old unsat cores");
       }
       Notice()
           << "SmtEngine: turning off bool-to-bv to support old unsat cores\n";
-      options::boolToBitvector.set(options::BoolToBVMode::OFF);
+      opts.set(options::boolToBitvector, options::BoolToBVMode::OFF);
     }
 
     if (options::bvIntroducePow2())
     {
-      if (options::bvIntroducePow2.wasSetByUser())
+      if (opts.wasSetByUser(options::bvIntroducePow2))
       {
         throw OptionException(
             "bv-intro-pow2 not supported with old unsat cores");
       }
       Notice()
           << "SmtEngine: turning off bv-intro-pow2 to support old unsat cores";
-      options::bvIntroducePow2.set(false);
+      opts.set(options::bvIntroducePow2, false);
     }
 
     if (options::repeatSimp())
     {
-      if (options::repeatSimp.wasSetByUser())
+      if (opts.wasSetByUser(options::repeatSimp))
       {
         throw OptionException("repeat-simp not supported with old unsat cores");
       }
       Notice()
           << "SmtEngine: turning off repeat-simp to support old unsat cores\n";
-      options::repeatSimp.set(false);
+      opts.set(options::repeatSimp, false);
     }
 
     if (options::globalNegate())
     {
-      if (options::globalNegate.wasSetByUser())
+      if (opts.wasSetByUser(options::globalNegate))
       {
         throw OptionException(
             "global-negate not supported with old unsat cores");
       }
       Notice() << "SmtEngine: turning off global-negate to support old unsat "
                   "cores\n";
-      options::globalNegate.set(false);
+      opts.set(options::globalNegate, false);
     }
 
     if (options::bitvectorAig())
@@ -609,16 +610,16 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   else
   {
     // by default, nonclausal simplification is off for QF_SAT
-    if (!options::simplificationMode.wasSetByUser())
+    if (!opts.wasSetByUser(options::simplificationMode))
     {
       bool qf_sat = logic.isPure(THEORY_BOOL) && !logic.isQuantified();
       Trace("smt") << "setting simplification mode to <"
                    << logic.getLogicString() << "> " << (!qf_sat) << std::endl;
       // simplification=none works better for SMT LIB benchmarks with
-      // quantifiers, not others options::simplificationMode.set(qf_sat ||
+      // quantifiers, not others opts.set(options::simplificationMode, qf_sat ||
       // quantifiers ? options::SimplificationMode::NONE :
       // options::SimplificationMode::BATCH);
-      options::simplificationMode.set(qf_sat
+      opts.set(options::simplificationMode, qf_sat
                                           ? options::SimplificationMode::NONE
                                           : options::SimplificationMode::BATCH);
     }
@@ -628,7 +629,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::boolToBitvector() != options::BoolToBVMode::OFF)
     {
-      if (options::boolToBitvector.wasSetByUser())
+      if (opts.wasSetByUser(options::boolToBitvector))
       {
         throw OptionException(
             "bool-to-bv != off not supported with CBQI BV for quantified "
@@ -636,7 +637,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       }
       Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
                << std::endl;
-      options::boolToBitvector.set(options::BoolToBVMode::OFF);
+      opts.set(options::boolToBitvector, options::BoolToBVMode::OFF);
     }
   }
 
@@ -646,7 +647,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
           || usesSygus))
   {
     Notice() << "SmtEngine: turning on produce-models" << std::endl;
-    options::produceModels.set(true);
+    opts.set(options::produceModels, true);
   }
 
   /////////////////////////////////////////////////////////////////////////////
@@ -687,7 +688,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     needsUf = true;
   }
   else if (options::preSkolemQuantNested()
-           && options::preSkolemQuantNested.wasSetByUser())
+           && opts.wasSetByUser(options::preSkolemQuantNested))
   {
     // if pre-skolem nested is explictly set, then we require UF. If it is
     // not explicitly set, it is disabled below if UF is not present.
@@ -742,7 +743,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   /////////////////////////////////////////////////////////////////////////////
 
   // Set the options for the theoryOf
-  if (!options::theoryOfMode.wasSetByUser())
+  if (!opts.wasSetByUser(options::theoryOfMode))
   {
     if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
         && !logic.isTheoryEnabled(THEORY_STRINGS)
@@ -752,18 +753,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
              && !logic.isQuantified()))
     {
       Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
-      options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
+      opts.set(options::theoryOfMode, options::TheoryOfMode::THEORY_OF_TERM_BASED);
     }
   }
 
   // by default, symmetry breaker is on only for non-incremental QF_UF
-  if (!options::ufSymmetryBreaker.wasSetByUser())
+  if (!opts.wasSetByUser(options::ufSymmetryBreaker))
   {
     bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
                        && !options::incrementalSolving() && !safeUnsatCores;
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
                  << std::endl;
-    options::ufSymmetryBreaker.set(qf_uf_noinc);
+    opts.set(options::ufSymmetryBreaker, qf_uf_noinc);
   }
 
   // If in arrays, set the UF handler to arrays
@@ -779,7 +780,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Theory::setUninterpretedSortOwner(THEORY_UF);
   }
 
-  if (!options::simplifyWithCareEnabled.wasSetByUser())
+  if (!opts.wasSetByUser(options::simplifyWithCareEnabled))
   {
     bool qf_aufbv =
         !logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
@@ -788,10 +789,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     bool withCare = qf_aufbv;
     Trace("smt") << "setting ite simplify with care to " << withCare
                  << std::endl;
-    options::simplifyWithCareEnabled.set(withCare);
+    opts.set(options::simplifyWithCareEnabled, withCare);
   }
   // Turn off array eager index splitting for QF_AUFLIA
-  if (!options::arraysEagerIndexSplitting.wasSetByUser())
+  if (!opts.wasSetByUser(options::arraysEagerIndexSplitting))
   {
     if (not logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
         && logic.isTheoryEnabled(THEORY_UF)
@@ -799,11 +800,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       Trace("smt") << "setting array eager index splitting to false"
                    << std::endl;
-      options::arraysEagerIndexSplitting.set(false);
+      opts.set(options::arraysEagerIndexSplitting, false);
     }
   }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
-  if (!options::repeatSimp.wasSetByUser())
+  if (!opts.wasSetByUser(options::repeatSimp))
   {
     bool repeatSimp = !logic.isQuantified()
                       && (logic.isTheoryEnabled(THEORY_ARRAYS)
@@ -812,40 +813,40 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                       && !safeUnsatCores;
     Trace("smt") << "setting repeat simplification to " << repeatSimp
                  << std::endl;
-    options::repeatSimp.set(repeatSimp);
+    opts.set(options::repeatSimp, repeatSimp);
   }
 
   if (options::boolToBitvector() == options::BoolToBVMode::ALL
       && !logic.isTheoryEnabled(THEORY_BV))
   {
-    if (options::boolToBitvector.wasSetByUser())
+    if (opts.wasSetByUser(options::boolToBitvector))
     {
       throw OptionException(
           "bool-to-bv=all not supported for non-bitvector logics.");
     }
     Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: "
              << logic.getLogicString() << std::endl;
-    options::boolToBitvector.set(options::BoolToBVMode::OFF);
+    opts.set(options::boolToBitvector, options::BoolToBVMode::OFF);
   }
 
-  if (!options::bvEagerExplanations.wasSetByUser()
+  if (!opts.wasSetByUser(options::bvEagerExplanations)
       && logic.isTheoryEnabled(THEORY_ARRAYS)
       && logic.isTheoryEnabled(THEORY_BV))
   {
     Trace("smt") << "enabling eager bit-vector explanations " << std::endl;
-    options::bvEagerExplanations.set(true);
+    opts.set(options::bvEagerExplanations, true);
   }
 
   // Turn on arith rewrite equalities only for pure arithmetic
-  if (!options::arithRewriteEq.wasSetByUser())
+  if (!opts.wasSetByUser(options::arithRewriteEq))
   {
     bool arithRewriteEq =
         logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified();
     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
                  << std::endl;
-    options::arithRewriteEq.set(arithRewriteEq);
+    opts.set(options::arithRewriteEq, arithRewriteEq);
   }
-  if (!options::arithHeuristicPivots.wasSetByUser())
+  if (!opts.wasSetByUser(options::arithHeuristicPivots))
   {
     int16_t heuristicPivots = 5;
     if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
@@ -861,9 +862,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
     Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots
                  << std::endl;
-    options::arithHeuristicPivots.set(heuristicPivots);
+    opts.set(options::arithHeuristicPivots, heuristicPivots);
   }
-  if (!options::arithPivotThreshold.wasSetByUser())
+  if (!opts.wasSetByUser(options::arithPivotThreshold))
   {
     uint16_t pivotThreshold = 2;
     if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
@@ -875,9 +876,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
     Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold
                  << std::endl;
-    options::arithPivotThreshold.set(pivotThreshold);
+    opts.set(options::arithPivotThreshold, pivotThreshold);
   }
-  if (!options::arithStandardCheckVarOrderPivots.wasSetByUser())
+  if (!opts.wasSetByUser(options::arithStandardCheckVarOrderPivots))
   {
     int16_t varOrderPivots = -1;
     if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
@@ -886,20 +887,20 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
     Trace("smt") << "setting arithStandardCheckVarOrderPivots  "
                  << varOrderPivots << std::endl;
-    options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
+    opts.set(options::arithStandardCheckVarOrderPivots, varOrderPivots);
   }
   if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed())
   {
-    if (!options::nlExtTangentPlanesInterleave.wasSetByUser())
+    if (!opts.wasSetByUser(options::nlExtTangentPlanesInterleave))
     {
       Trace("smt") << "setting nlExtTangentPlanesInterleave to true"
                    << std::endl;
-      options::nlExtTangentPlanesInterleave.set(true);
+      opts.set(options::nlExtTangentPlanesInterleave, true);
     }
   }
 
   // Set decision mode based on logic (if not set by user)
-  if (!options::decisionMode.wasSetByUser())
+  if (!opts.wasSetByUser(options::decisionMode))
   {
     options::DecisionMode decMode =
         // anything that uses sygus uses internal
@@ -954,50 +955,50 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                       : false);
 
     Trace("smt") << "setting decision mode to " << decMode << std::endl;
-    options::decisionMode.set(decMode);
-    options::decisionStopOnly.set(stoponly);
+    opts.set(options::decisionMode, decMode);
+    opts.set(options::decisionStopOnly, stoponly);
   }
   if (options::incrementalSolving())
   {
     // disable modes not supported by incremental
-    options::sortInference.set(false);
-    options::ufssFairnessMonotone.set(false);
-    options::globalNegate.set(false);
-    options::bvAbstraction.set(false);
-    options::arithMLTrick.set(false);
+    opts.set(options::sortInference, false);
+    opts.set(options::ufssFairnessMonotone, false);
+    opts.set(options::globalNegate, false);
+    opts.set(options::bvAbstraction, false);
+    opts.set(options::arithMLTrick, false);
   }
   if (logic.hasCardinalityConstraints())
   {
     // must have finite model finding on
-    options::finiteModelFind.set(true);
+    opts.set(options::finiteModelFind, true);
   }
 
   if (options::instMaxLevel() != -1)
   {
     Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"
              << std::endl;
-    options::cegqi.set(false);
+    opts.set(options::cegqi, false);
   }
 
-  if ((options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy())
-      || (options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt()))
+  if ((opts.wasSetByUser(options::fmfBoundLazy) && options::fmfBoundLazy())
+      || (opts.wasSetByUser(options::fmfBoundInt) && options::fmfBoundInt()))
   {
-    options::fmfBound.set(true);
+    opts.set(options::fmfBound, true);
   }
   // now have determined whether fmfBoundInt is on/off
   // apply fmfBoundInt options
   if (options::fmfBound())
   {
-    if (!options::mbqiMode.wasSetByUser()
+    if (!opts.wasSetByUser(options::mbqiMode)
         || (options::mbqiMode() != options::MbqiMode::NONE
             && options::mbqiMode() != options::MbqiMode::FMC))
     {
       // if bounded integers are set, use no MBQI by default
-      options::mbqiMode.set(options::MbqiMode::NONE);
+      opts.set(options::mbqiMode, options::MbqiMode::NONE);
     }
-    if (!options::prenexQuant.wasSetByUser())
+    if (!opts.wasSetByUser(options::prenexQuant))
     {
-      options::prenexQuant.set(options::PrenexQuantMode::NONE);
+      opts.set(options::prenexQuant, options::PrenexQuantMode::NONE);
     }
   }
   if (options::ufHo())
@@ -1006,37 +1007,37 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     // cannot be used
     if (options::mbqiMode() != options::MbqiMode::NONE)
     {
-      options::mbqiMode.set(options::MbqiMode::NONE);
+      opts.set(options::mbqiMode, options::MbqiMode::NONE);
     }
-    if (!options::hoElimStoreAx.wasSetByUser())
+    if (!opts.wasSetByUser(options::hoElimStoreAx))
     {
       // by default, use store axioms only if --ho-elim is set
-      options::hoElimStoreAx.set(options::hoElim());
+      opts.set(options::hoElimStoreAx, options::hoElim());
     }
     if (!options::assignFunctionValues())
     {
       // must assign function values
-      options::assignFunctionValues.set(true);
+      opts.set(options::assignFunctionValues, true);
     }
     // Cannot use macros, since lambda lifting and macro elimination are inverse
     // operations.
     if (options::macrosQuant())
     {
-      options::macrosQuant.set(false);
+      opts.set(options::macrosQuant, false);
     }
   }
   if (options::fmfFunWellDefinedRelevant())
   {
-    if (!options::fmfFunWellDefined.wasSetByUser())
+    if (!opts.wasSetByUser(options::fmfFunWellDefined))
     {
-      options::fmfFunWellDefined.set(true);
+      opts.set(options::fmfFunWellDefined, true);
     }
   }
   if (options::fmfFunWellDefined())
   {
-    if (!options::finiteModelFind.wasSetByUser())
+    if (!opts.wasSetByUser(options::finiteModelFind))
     {
-      options::finiteModelFind.set(true);
+      opts.set(options::finiteModelFind, true);
     }
   }
 
@@ -1045,20 +1046,20 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (options::finiteModelFind())
   {
     // apply conservative quantifiers splitting
-    if (!options::quantDynamicSplit.wasSetByUser())
+    if (!opts.wasSetByUser(options::quantDynamicSplit))
     {
-      options::quantDynamicSplit.set(options::QuantDSplitMode::DEFAULT);
+      opts.set(options::quantDynamicSplit, options::QuantDSplitMode::DEFAULT);
     }
-    if (!options::eMatching.wasSetByUser())
+    if (!opts.wasSetByUser(options::eMatching))
     {
-      options::eMatching.set(options::fmfInstEngine());
+      opts.set(options::eMatching, options::fmfInstEngine());
     }
-    if (!options::instWhenMode.wasSetByUser())
+    if (!opts.wasSetByUser(options::instWhenMode))
     {
       // instantiate only on last call
       if (options::eMatching())
       {
-        options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
+        opts.set(options::instWhenMode, options::InstWhenMode::LAST_CALL);
       }
     }
   }
@@ -1071,71 +1072,71 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       Trace("smt") << "turning on sygus" << std::endl;
     }
-    options::sygus.set(true);
+    opts.set(options::sygus, true);
     // must use Ferrante/Rackoff for real arithmetic
-    if (!options::cegqiMidpoint.wasSetByUser())
+    if (!opts.wasSetByUser(options::cegqiMidpoint))
     {
-      options::cegqiMidpoint.set(true);
+      opts.set(options::cegqiMidpoint, true);
     }
     // must disable cegqi-bv since it may introduce witness terms, which
     // cannot appear in synthesis solutions
-    if (!options::cegqiBv.wasSetByUser())
+    if (!opts.wasSetByUser(options::cegqiBv))
     {
-      options::cegqiBv.set(false);
+      opts.set(options::cegqiBv, false);
     }
     if (options::sygusRepairConst())
     {
-      if (!options::cegqi.wasSetByUser())
+      if (!opts.wasSetByUser(options::cegqi))
       {
-        options::cegqi.set(true);
+        opts.set(options::cegqi, true);
       }
     }
     if (options::sygusInference())
     {
       // optimization: apply preskolemization, makes it succeed more often
-      if (!options::preSkolemQuant.wasSetByUser())
+      if (!opts.wasSetByUser(options::preSkolemQuant))
       {
-        options::preSkolemQuant.set(true);
+        opts.set(options::preSkolemQuant, true);
       }
-      if (!options::preSkolemQuantNested.wasSetByUser())
+      if (!opts.wasSetByUser(options::preSkolemQuantNested))
       {
-        options::preSkolemQuantNested.set(true);
+        opts.set(options::preSkolemQuantNested, true);
       }
     }
     // counterexample-guided instantiation for sygus
-    if (!options::cegqiSingleInvMode.wasSetByUser())
+    if (!opts.wasSetByUser(options::cegqiSingleInvMode))
     {
-      options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::USE);
+      opts.set(options::cegqiSingleInvMode, options::CegqiSingleInvMode::USE);
     }
-    if (!options::quantConflictFind.wasSetByUser())
+    if (!opts.wasSetByUser(options::quantConflictFind))
     {
-      options::quantConflictFind.set(false);
+      opts.set(options::quantConflictFind, false);
     }
-    if (!options::instNoEntail.wasSetByUser())
+    if (!opts.wasSetByUser(options::instNoEntail))
     {
-      options::instNoEntail.set(false);
+      opts.set(options::instNoEntail, false);
     }
-    if (!options::cegqiFullEffort.wasSetByUser())
+    if (!opts.wasSetByUser(options::cegqiFullEffort))
     {
       // should use full effort cbqi for single invocation and repair const
-      options::cegqiFullEffort.set(true);
+      opts.set(options::cegqiFullEffort, true);
     }
     if (options::sygusRew())
     {
-      options::sygusRewSynth.set(true);
-      options::sygusRewVerify.set(true);
+      opts.set(options::sygusRewSynth, true);
+      opts.set(options::sygusRewVerify, true);
     }
     if (options::sygusRewSynthInput())
     {
       // If we are using synthesis rewrite rules from input, we use
       // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for
       // details on this technique.
-      options::sygusRewSynth.set(true);
+      opts.set(options::sygusRewSynth, true);
       // we should not use the extended rewriter, since we are interested
       // in rewrites that are not in the main rewriter
-      if (!options::sygusExtRew.wasSetByUser())
+      if (!opts.wasSetByUser(options::sygusExtRew))
       {
-        options::sygusExtRew.set(false);
+        opts.set(options::sygusExtRew, false);
       }
     }
     // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
@@ -1147,9 +1148,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (options::produceAbducts())
     {
       // if doing abduction, we should filter strong solutions
-      if (!options::sygusFilterSolMode.wasSetByUser())
+      if (!opts.wasSetByUser(options::sygusFilterSolMode))
       {
-        options::sygusFilterSolMode.set(options::SygusFilterSolMode::STRONG);
+        opts.set(options::sygusFilterSolMode, options::SygusFilterSolMode::STRONG);
       }
       // we must use basic sygus algorithms, since e.g. we require checking
       // a sygus side condition for consistency with axioms.
@@ -1159,7 +1160,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
         || options::sygusQueryGen())
     {
       // rewrite rule synthesis implies that sygus stream must be true
-      options::sygusStream.set(true);
+      opts.set(options::sygusStream, true);
     }
     if (options::sygusStream() || options::incrementalSolving())
     {
@@ -1170,50 +1171,50 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     // Now, disable options for non-basic sygus algorithms, if necessary.
     if (reqBasicSygus)
     {
-      if (!options::sygusUnifPbe.wasSetByUser())
+      if (!opts.wasSetByUser(options::sygusUnifPbe))
       {
-        options::sygusUnifPbe.set(false);
+        opts.set(options::sygusUnifPbe, false);
       }
-      if (options::sygusUnifPi.wasSetByUser())
+      if (opts.wasSetByUser(options::sygusUnifPi))
       {
-        options::sygusUnifPi.set(options::SygusUnifPiMode::NONE);
+        opts.set(options::sygusUnifPi, options::SygusUnifPiMode::NONE);
       }
-      if (!options::sygusInvTemplMode.wasSetByUser())
+      if (!opts.wasSetByUser(options::sygusInvTemplMode))
       {
-        options::sygusInvTemplMode.set(options::SygusInvTemplMode::NONE);
+        opts.set(options::sygusInvTemplMode, options::SygusInvTemplMode::NONE);
       }
-      if (!options::cegqiSingleInvMode.wasSetByUser())
+      if (!opts.wasSetByUser(options::cegqiSingleInvMode))
       {
-        options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::NONE);
+        opts.set(options::cegqiSingleInvMode, options::CegqiSingleInvMode::NONE);
       }
     }
-    if (!options::dtRewriteErrorSel.wasSetByUser())
+    if (!opts.wasSetByUser(options::dtRewriteErrorSel))
     {
-      options::dtRewriteErrorSel.set(true);
+      opts.set(options::dtRewriteErrorSel, true);
     }
     // do not miniscope
-    if (!options::miniscopeQuant.wasSetByUser())
+    if (!opts.wasSetByUser(options::miniscopeQuant))
     {
-      options::miniscopeQuant.set(false);
+      opts.set(options::miniscopeQuant, false);
     }
-    if (!options::miniscopeQuantFreeVar.wasSetByUser())
+    if (!opts.wasSetByUser(options::miniscopeQuantFreeVar))
     {
-      options::miniscopeQuantFreeVar.set(false);
+      opts.set(options::miniscopeQuantFreeVar, false);
     }
-    if (!options::quantSplit.wasSetByUser())
+    if (!opts.wasSetByUser(options::quantSplit))
     {
-      options::quantSplit.set(false);
+      opts.set(options::quantSplit, false);
     }
     // do not do macros
-    if (!options::macrosQuant.wasSetByUser())
+    if (!opts.wasSetByUser(options::macrosQuant))
     {
-      options::macrosQuant.set(false);
+      opts.set(options::macrosQuant, false);
     }
     // use tangent planes by default, since we want to put effort into
     // the verification step for sygus queries with non-linear arithmetic
-    if (!options::nlExtTangentPlanes.wasSetByUser())
+    if (!opts.wasSetByUser(options::nlExtTangentPlanes))
     {
-      options::nlExtTangentPlanes.set(true);
+      opts.set(options::nlExtTangentPlanes, true);
     }
   }
   // counterexample-guided instantiation for non-sygus
@@ -1225,16 +1226,16 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
            || logic.isTheoryEnabled(THEORY_FP)))
       || options::cegqiAll())
   {
-    if (!options::cegqi.wasSetByUser())
+    if (!opts.wasSetByUser(options::cegqi))
     {
-      options::cegqi.set(true);
+      opts.set(options::cegqi, true);
     }
     // check whether we should apply full cbqi
     if (logic.isPure(THEORY_BV))
     {
-      if (!options::cegqiFullEffort.wasSetByUser())
+      if (!opts.wasSetByUser(options::cegqiFullEffort))
       {
-        options::cegqiFullEffort.set(true);
+        opts.set(options::cegqiFullEffort, true);
       }
     }
   }
@@ -1243,129 +1244,129 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (options::incrementalSolving())
     {
       // cannot do nested quantifier elimination in incremental mode
-      options::cegqiNestedQE.set(false);
+      opts.set(options::cegqiNestedQE, false);
     }
     if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
     {
-      if (!options::quantConflictFind.wasSetByUser())
+      if (!opts.wasSetByUser(options::quantConflictFind))
       {
-        options::quantConflictFind.set(false);
+        opts.set(options::quantConflictFind, false);
       }
-      if (!options::instNoEntail.wasSetByUser())
+      if (!opts.wasSetByUser(options::instNoEntail))
       {
-        options::instNoEntail.set(false);
+        opts.set(options::instNoEntail, false);
       }
-      if (!options::instWhenMode.wasSetByUser() && options::cegqiModel())
+      if (!opts.wasSetByUser(options::instWhenMode) && options::cegqiModel())
       {
         // only instantiation should happen at last call when model is avaiable
-        options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
+        opts.set(options::instWhenMode, options::InstWhenMode::LAST_CALL);
       }
     }
     else
     {
       // only supported in pure arithmetic or pure BV
-      options::cegqiNestedQE.set(false);
+      opts.set(options::cegqiNestedQE, false);
     }
     if (options::globalNegate())
     {
-      if (!options::prenexQuant.wasSetByUser())
+      if (!opts.wasSetByUser(options::prenexQuant))
       {
-        options::prenexQuant.set(options::PrenexQuantMode::NONE);
+        opts.set(options::prenexQuant, options::PrenexQuantMode::NONE);
       }
     }
   }
   // implied options...
   if (options::strictTriggers())
   {
-    if (!options::userPatternsQuant.wasSetByUser())
+    if (!opts.wasSetByUser(options::userPatternsQuant))
     {
-      options::userPatternsQuant.set(options::UserPatMode::TRUST);
+      opts.set(options::userPatternsQuant, options::UserPatMode::TRUST);
     }
   }
-  if (options::qcfMode.wasSetByUser() || options::qcfTConstraint())
+  if (opts.wasSetByUser(options::qcfMode) || options::qcfTConstraint())
   {
-    options::quantConflictFind.set(true);
+    opts.set(options::quantConflictFind, true);
   }
   if (options::cegqiNestedQE())
   {
-    options::prenexQuantUser.set(true);
-    if (!options::preSkolemQuant.wasSetByUser())
+    opts.set(options::prenexQuantUser, true);
+    if (!opts.wasSetByUser(options::preSkolemQuant))
     {
-      options::preSkolemQuant.set(true);
+      opts.set(options::preSkolemQuant, true);
     }
   }
   // for induction techniques
   if (options::quantInduction())
   {
-    if (!options::dtStcInduction.wasSetByUser())
+    if (!opts.wasSetByUser(options::dtStcInduction))
     {
-      options::dtStcInduction.set(true);
+      opts.set(options::dtStcInduction, true);
     }
-    if (!options::intWfInduction.wasSetByUser())
+    if (!opts.wasSetByUser(options::intWfInduction))
     {
-      options::intWfInduction.set(true);
+      opts.set(options::intWfInduction, true);
     }
   }
   if (options::dtStcInduction())
   {
     // try to remove ITEs from quantified formulas
-    if (!options::iteDtTesterSplitQuant.wasSetByUser())
+    if (!opts.wasSetByUser(options::iteDtTesterSplitQuant))
     {
-      options::iteDtTesterSplitQuant.set(true);
+      opts.set(options::iteDtTesterSplitQuant, true);
     }
-    if (!options::iteLiftQuant.wasSetByUser())
+    if (!opts.wasSetByUser(options::iteLiftQuant))
     {
-      options::iteLiftQuant.set(options::IteLiftQuantMode::ALL);
+      opts.set(options::iteLiftQuant, options::IteLiftQuantMode::ALL);
     }
   }
   if (options::intWfInduction())
   {
-    if (!options::purifyTriggers.wasSetByUser())
+    if (!opts.wasSetByUser(options::purifyTriggers))
     {
-      options::purifyTriggers.set(true);
+      opts.set(options::purifyTriggers, true);
     }
   }
   if (options::conjectureNoFilter())
   {
-    if (!options::conjectureFilterActiveTerms.wasSetByUser())
+    if (!opts.wasSetByUser(options::conjectureFilterActiveTerms))
     {
-      options::conjectureFilterActiveTerms.set(false);
+      opts.set(options::conjectureFilterActiveTerms, false);
     }
-    if (!options::conjectureFilterCanonical.wasSetByUser())
+    if (!opts.wasSetByUser(options::conjectureFilterCanonical))
     {
-      options::conjectureFilterCanonical.set(false);
+      opts.set(options::conjectureFilterCanonical, false);
     }
-    if (!options::conjectureFilterModel.wasSetByUser())
+    if (!opts.wasSetByUser(options::conjectureFilterModel))
     {
-      options::conjectureFilterModel.set(false);
+      opts.set(options::conjectureFilterModel, false);
     }
   }
-  if (options::conjectureGenPerRound.wasSetByUser())
+  if (opts.wasSetByUser(options::conjectureGenPerRound))
   {
     if (options::conjectureGenPerRound() > 0)
     {
-      options::conjectureGen.set(true);
+      opts.set(options::conjectureGen, true);
     }
     else
     {
-      options::conjectureGen.set(false);
+      opts.set(options::conjectureGen, false);
     }
   }
   // can't pre-skolemize nested quantifiers without UF theory
   if (!logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant())
   {
-    if (!options::preSkolemQuantNested.wasSetByUser())
+    if (!opts.wasSetByUser(options::preSkolemQuantNested))
     {
-      options::preSkolemQuantNested.set(false);
+      opts.set(options::preSkolemQuantNested, false);
     }
   }
   if (!logic.isTheoryEnabled(THEORY_DATATYPES))
   {
-    options::quantDynamicSplit.set(options::QuantDSplitMode::NONE);
+    opts.set(options::quantDynamicSplit, options::QuantDSplitMode::NONE);
   }
 
   // until bugs 371,431 are fixed
-  if (!options::minisatUseElim.wasSetByUser())
+  if (!opts.wasSetByUser(options::minisatUseElim))
   {
     // cannot use minisat elimination for logics where a theory solver
     // introduces new literals into the search. This includes quantifiers
@@ -1378,7 +1379,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
         || options::checkModels()
         || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
     {
-      options::minisatUseElim.set(false);
+      opts.set(options::minisatUseElim, false);
     }
   }
 
@@ -1387,14 +1388,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (!options::relevanceFilter())
     {
-      if (options::relevanceFilter.wasSetByUser())
+      if (opts.wasSetByUser(options::relevanceFilter))
       {
         Warning() << "SmtEngine: turning on relevance filtering to support "
                      "--nl-ext-rlv="
                   << options::nlRlvMode() << std::endl;
       }
       // must use relevance filtering techniques
-      options::relevanceFilter.set(true);
+      opts.set(options::relevanceFilter, true);
     }
   }
 
@@ -1402,14 +1403,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (options::produceModels() || options::produceAssignments()
       || options::checkModels())
   {
-    options::arraysOptimizeLinear.set(false);
+    opts.set(options::arraysOptimizeLinear, false);
   }
 
   if (!options::bitvectorEqualitySolver())
   {
     if (options::bvLazyRewriteExtf())
     {
-      if (options::bvLazyRewriteExtf.wasSetByUser())
+      if (opts.wasSetByUser(options::bvLazyRewriteExtf))
       {
         throw OptionException(
             "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
@@ -1418,21 +1419,21 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Trace("smt")
         << "disabling bvLazyRewriteExtf since equality solver is disabled"
         << std::endl;
-    options::bvLazyRewriteExtf.set(false);
+    opts.set(options::bvLazyRewriteExtf, false);
   }
 
-  if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser())
+  if (options::stringFMF() && !opts.wasSetByUser(options::stringProcessLoopMode))
   {
     Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
                     "--strings-fmf enabled"
                  << std::endl;
-    options::stringProcessLoopMode.set(options::ProcessLoopMode::SIMPLE);
+    opts.set(options::stringProcessLoopMode, options::ProcessLoopMode::SIMPLE);
   }
 
   // !!! All options that require disabling models go here
   bool disableModels = false;
   std::string sOptNoModel;
-  if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp())
+  if (opts.wasSetByUser(options::unconstrainedSimp) && options::unconstrainedSimp())
   {
     disableModels = true;
     sOptNoModel = "unconstrained-simp";
@@ -1456,7 +1457,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::produceModels())
     {
-      if (options::produceModels.wasSetByUser())
+      if (opts.wasSetByUser(options::produceModels))
       {
         std::stringstream ss;
         ss << "Cannot use " << sOptNoModel << " with model generation.";
@@ -1464,11 +1465,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       }
       Notice() << "SmtEngine: turning off produce-models to support "
                << sOptNoModel << std::endl;
-      options::produceModels.set(false);
+      opts.set(options::produceModels, false);
     }
     if (options::produceAssignments())
     {
-      if (options::produceAssignments.wasSetByUser())
+      if (opts.wasSetByUser(options::produceAssignments))
       {
         std::stringstream ss;
         ss << "Cannot use " << sOptNoModel
@@ -1477,11 +1478,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       }
       Notice() << "SmtEngine: turning off produce-assignments to support "
                << sOptNoModel << std::endl;
-      options::produceAssignments.set(false);
+      opts.set(options::produceAssignments, false);
     }
     if (options::checkModels())
     {
-      if (options::checkModels.wasSetByUser())
+      if (opts.wasSetByUser(options::checkModels))
       {
         std::stringstream ss;
         ss << "Cannot use " << sOptNoModel
@@ -1490,7 +1491,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       }
       Notice() << "SmtEngine: turning off check-models to support "
                << sOptNoModel << std::endl;
-      options::checkModels.set(false);
+      opts.set(options::checkModels, false);
     }
   }
 
@@ -1508,16 +1509,16 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (logic == LogicInfo("QF_UFNRA"))
   {
 #ifdef CVC5_USE_POLY
-    if (!options::nlCad() && !options::nlCad.wasSetByUser())
+    if (!options::nlCad() && !opts.wasSetByUser(options::nlCad))
     {
-      options::nlCad.set(true);
-      if (!options::nlExt.wasSetByUser())
+      opts.set(options::nlCad, true);
+      if (!opts.wasSetByUser(options::nlExt))
       {
-        options::nlExt.set(false);
+        opts.set(options::nlExt, false);
       }
-      if (!options::nlRlvMode.wasSetByUser())
+      if (!opts.wasSetByUser(options::nlRlvMode))
       {
-        options::nlRlvMode.set(options::NlRlvMode::INTERLEAVE);
+        opts.set(options::nlRlvMode, options::NlRlvMode::INTERLEAVE);
       }
     }
 #endif
@@ -1525,18 +1526,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 #ifndef CVC5_USE_POLY
   if (options::nlCad())
   {
-    if (options::nlCad.wasSetByUser())
+    if (opts.wasSetByUser(options::nlCad))
     {
       std::stringstream ss;
-      ss << "Cannot use " << options::nlCad.getName() << " without configuring with --poly.";
+      ss << "Cannot use " << options::nlCad.name << " without configuring with --poly.";
       throw OptionException(ss.str());
     }
     else
     {
-      Notice() << "Cannot use --" << options::nlCad.getName()
+      Notice() << "Cannot use --" << options::nlCad.name
                << " without configuring with --poly." << std::endl;
-      options::nlCad.set(false);
-      options::nlExt.set(true);
+      opts.set(options::nlCad, false);
+      opts.set(options::nlExt, true);
     }
   }
 #endif
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 09b3d64ab..24a3e409e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -147,7 +147,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
 
   // d_proofManager must be created before Options has been finished
   // being parsed from the input file. Because of this, we cannot trust
-  // that options::unsatCores() is set correctly yet.
+  // that d_env->getOption(options::unsatCores) is set correctly yet.
   d_proofManager.reset(new ProofManager(getUserContext()));
 
   d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
@@ -205,7 +205,7 @@ void SmtEngine::finishInit()
   }
 
   // set the random seed
-  Random::getRandom().setSeed(options::seed());
+  Random::getRandom().setSeed(d_env->getOption(options::seed));
 
   // Call finish init on the options manager. This inializes the resource
   // manager based on the options, and sets up the best default options
@@ -213,7 +213,7 @@ void SmtEngine::finishInit()
   d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver);
 
   ProofNodeManager* pnm = nullptr;
-  if (options::produceProofs())
+  if (d_env->getOption(options::produceProofs))
   {
     // ensure bound variable uses canonical bound variables
     getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
@@ -274,11 +274,12 @@ void SmtEngine::finishInit()
   getDumpManager()->finishInit();
 
   // subsolvers
-  if (options::produceAbducts())
+  if (d_env->getOption(options::produceAbducts))
   {
     d_abductSolver.reset(new AbductionSolver(this));
   }
-  if (options::produceInterpols() != options::ProduceInterpols::NONE)
+  if (d_env->getOption(options::produceInterpols)
+      != options::ProduceInterpols::NONE)
   {
     d_interpolSolver.reset(new InterpolationSolver(this));
   }
@@ -322,7 +323,8 @@ SmtEngine::~SmtEngine()
 
     // d_proofManager is always created when proofs are enabled at configure
     // time.  Because of this, this code should not be wrapped in PROOF() which
-    // additionally checks flags such as options::produceProofs().
+    // additionally checks flags such as
+    // d_env->getOption(options::produceProofs).
     //
     // Note: the proof manager must be destroyed before the theory engine.
     // Because the destruction of the proofs depends on contexts owned be the
@@ -465,7 +467,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
   {
     d_state->setFilename(value);
   }
-  else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser())
+  else if (key == "smt-lib-version" && !Options::current().wasSetByUser(options::inputLanguage))
   {
     language::input::Language ilang = language::input::LANG_SMTLIB_V2_6;
 
@@ -475,15 +477,15 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
                 << " unsupported, defaulting to language (and semantics of) "
                    "SMT-LIB 2.6\n";
     }
-    options::inputLanguage.set(ilang);
+    Options::current().set(options::inputLanguage, ilang);
     // also update the output language
-    if (!options::outputLanguage.wasSetByUser())
+    if (!Options::current().wasSetByUser(options::outputLanguage))
     {
       language::output::Language olang = language::toOutputLanguage(ilang);
-      if (options::outputLanguage() != olang)
+      if (d_env->getOption(options::outputLanguage) != olang)
       {
-        options::outputLanguage.set(olang);
-        *options::out() << language::SetLanguage(olang);
+        Options::current().set(options::outputLanguage, olang);
+        *d_env->getOption(options::out) << language::SetLanguage(olang);
       }
     }
   }
@@ -571,7 +573,7 @@ std::string SmtEngine::getInfo(const std::string& key) const
   }
   Assert(key == "all-options");
   // get the options, like all-statistics
-  return toSExpr(Options::current()->getOptions());
+  return toSExpr(Options::current().getOptions());
 }
 
 void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)
@@ -595,7 +597,8 @@ void SmtEngine::debugCheckFunctionBody(Node formula,
                                        const std::vector<Node>& formals,
                                        Node func)
 {
-  TypeNode formulaType = formula.getType(options::typeChecking());
+  TypeNode formulaType =
+      formula.getType(d_env->getOption(options::typeChecking));
   TypeNode funcType = func.getType();
   // We distinguish here between definitions of constants and functions,
   // because the type checking for them is subtly different.  Perhaps we
@@ -777,7 +780,7 @@ Result SmtEngine::quickCheck() {
 
 Model* SmtEngine::getAvailableModel(const char* c) const
 {
-  if (!options::assignFunctionValues())
+  if (!d_env->getOption(options::assignFunctionValues))
   {
     std::stringstream ss;
     ss << "Cannot " << c << " when --assign-function-values is false.";
@@ -794,7 +797,7 @@ Model* SmtEngine::getAvailableModel(const char* c) const
     throw RecoverableModalException(ss.str().c_str());
   }
 
-  if (!options::produceModels())
+  if (!d_env->getOption(options::produceModels))
   {
     std::stringstream ss;
     ss << "Cannot " << c << " when produce-models options is off.";
@@ -938,19 +941,22 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
                  << "(" << assumptions << ") => " << r << endl;
 
     // Check that SAT results generate a model correctly.
-    if(options::checkModels()) {
+    if (d_env->getOption(options::checkModels))
+    {
       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
       {
         checkModel();
       }
     }
     // Check that UNSAT results generate a proof correctly.
-    if (options::checkProofs() || options::proofEagerChecking())
+    if (d_env->getOption(options::checkProofs)
+        || d_env->getOption(options::proofEagerChecking))
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
-        if ((options::checkProofs() || options::proofEagerChecking())
-            && !options::produceProofs())
+        if ((d_env->getOption(options::checkProofs)
+             || d_env->getOption(options::proofEagerChecking))
+            && !d_env->getOption(options::produceProofs))
         {
           throw ModalException(
               "Cannot check-proofs because proofs were disabled.");
@@ -959,7 +965,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
       }
     }
     // Check that UNSAT results generate an unsat core correctly.
-    if (options::checkUnsatCores())
+    if (d_env->getOption(options::checkUnsatCores))
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
@@ -988,7 +994,7 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void)
 {
   Trace("smt") << "SMT getUnsatAssumptions()" << endl;
   SmtScope smts(this);
-  if (!options::unsatAssumptions())
+  if (!d_env->getOption(options::unsatAssumptions))
   {
     throw ModalException(
         "Cannot get unsat assumptions when produce-unsat-assumptions option "
@@ -1201,7 +1207,9 @@ Node SmtEngine::getValue(const Node& ex) const
   Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA
          || resultNode.isConst());
 
-  if(options::abstractValues() && resultNode.getType().isArray()) {
+  if (d_env->getOption(options::abstractValues)
+      && resultNode.getType().isArray())
+  {
     resultNode = d_absValues->mkAbstractValue(resultNode);
     Trace("smt") << "--- abstract value >> " << resultNode << endl;
   }
@@ -1240,13 +1248,15 @@ Model* SmtEngine::getModel() {
   Assert(te != nullptr);
   te->setEagerModelBuilding();
 
-  if (options::modelCoresMode() != options::ModelCoresMode::NONE)
+  if (d_env->getOption(options::modelCoresMode)
+      != options::ModelCoresMode::NONE)
   {
     // If we enabled model cores, we compute a model core for m based on our
     // (expanded) assertions using the model core builder utility
     std::vector<Node> eassertsProc = getExpandedAssertions();
-    ModelCoreBuilder::setModelCore(
-        eassertsProc, m->getTheoryModel(), options::modelCoresMode());
+    ModelCoreBuilder::setModelCore(eassertsProc,
+                                   m->getTheoryModel(),
+                                   d_env->getOption(options::modelCoresMode));
   }
   // set the information on the SMT-level model
   Assert(m != nullptr);
@@ -1269,7 +1279,8 @@ Result SmtEngine::blockModel()
 
   Model* m = getAvailableModel("block model");
 
-  if (options::blockModelsMode() == options::BlockModelsMode::NONE)
+  if (d_env->getOption(options::blockModelsMode)
+      == options::BlockModelsMode::NONE)
   {
     std::stringstream ss;
     ss << "Cannot block model when block-models is set to none.";
@@ -1278,8 +1289,10 @@ Result SmtEngine::blockModel()
 
   // get expanded assertions
   std::vector<Node> eassertsProc = getExpandedAssertions();
-  Node eblocker = ModelBlocker::getModelBlocker(
-      eassertsProc, m->getTheoryModel(), options::blockModelsMode());
+  Node eblocker =
+      ModelBlocker::getModelBlocker(eassertsProc,
+                                    m->getTheoryModel(),
+                                    d_env->getOption(options::blockModelsMode));
   return assertFormula(eblocker);
 }
 
@@ -1375,17 +1388,17 @@ Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
 
 void SmtEngine::checkProof()
 {
-  Assert(options::produceProofs());
+  Assert(d_env->getOption(options::produceProofs));
   // internal check the proof
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
-  if (options::proofEagerChecking())
+  if (d_env->getOption(options::proofEagerChecking))
   {
     pe->checkProof(d_asserts->getAssertionList());
   }
   Assert(pe->getProof() != nullptr);
   std::shared_ptr<ProofNode> pePfn = pe->getProof();
-  if (options::checkProofs())
+  if (d_env->getOption(options::checkProofs))
   {
     d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions);
   }
@@ -1398,7 +1411,7 @@ StatisticsRegistry& SmtEngine::getStatisticsRegistry()
 
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
-  if (!options::unsatCores())
+  if (!d_env->getOption(options::unsatCores))
   {
     throw ModalException(
         "Cannot get an unsat core when produce-unsat-cores[-new] or "
@@ -1438,7 +1451,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
 }
 
 void SmtEngine::checkUnsatCore() {
-  Assert(options::unsatCores())
+  Assert(d_env->getOption(options::unsatCores))
       << "cannot check unsat core if unsat cores are turned off";
 
   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
@@ -1538,7 +1551,7 @@ std::string SmtEngine::getProof()
   {
     getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut());
   }
-  if (!options::produceProofs())
+  if (!d_env->getOption(options::produceProofs))
   {
     throw ModalException("Cannot get a proof when proof option is off.");
   }
@@ -1561,7 +1574,7 @@ std::string SmtEngine::getProof()
 void SmtEngine::printInstantiations( std::ostream& out ) {
   SmtScope smts(this);
   finishInit();
-  if (options::instFormatMode() == options::InstFormatMode::SZS)
+  if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS)
   {
     out << "% SZS output start Proof for " << d_state->getFilename()
         << std::endl;
@@ -1570,9 +1583,9 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
 
   // First, extract and print the skolemizations
   bool printed = false;
-  bool reqNames = !options::printInstFull();
+  bool reqNames = !d_env->getOption(options::printInstFull);
   // only print when in list mode
-  if (options::printInstMode() == options::PrintInstMode::LIST)
+  if (d_env->getOption(options::printInstMode) == options::PrintInstMode::LIST)
   {
     std::map<Node, std::vector<Node>> sks;
     qe->getSkolemTermVectors(sks);
@@ -1607,14 +1620,15 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
       continue;
     }
     // must have a name
-    if (options::printInstMode() == options::PrintInstMode::NUM)
+    if (d_env->getOption(options::printInstMode) == options::PrintInstMode::NUM)
     {
       out << "(num-instantiations " << name << " " << i.second.size() << ")"
           << std::endl;
     }
     else
     {
-      Assert(options::printInstMode() == options::PrintInstMode::LIST);
+      Assert(d_env->getOption(options::printInstMode)
+             == options::PrintInstMode::LIST);
       InstantiationList ilist(name, i.second);
       out << ilist;
     }
@@ -1625,7 +1639,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   {
     out << "No instantiations" << std::endl;
   }
-  if (options::instFormatMode() == options::InstFormatMode::SZS)
+  if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS)
   {
     out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
   }
@@ -1636,9 +1650,9 @@ void SmtEngine::getInstantiationTermVectors(
 {
   SmtScope smts(this);
   finishInit();
-  if (options::produceProofs()
-      && (!options::unsatCores()
-          || options::unsatCoresMode() == options::UnsatCoresMode::FULL_PROOF)
+  if (d_env->getOption(options::produceProofs)
+      && (!d_env->getOption(options::unsatCores)
+          || d_env->getOption(options::unsatCoresMode) == options::UnsatCoresMode::FULL_PROOF)
       && getSmtMode() == SmtMode::UNSAT)
   {
     // minimize instantiations based on proof manager
@@ -1745,7 +1759,8 @@ std::vector<Node> SmtEngine::getAssertions()
     getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut());
   }
   Trace("smt") << "SMT getAssertions()" << endl;
-  if(!options::produceAssertions()) {
+  if (!d_env->getOption(options::produceAssertions))
+  {
     const char* msg =
       "Cannot query the current assertion list when not in produce-assertions mode.";
     throw ModalException(msg);
diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h
index d81a507f8..cc660ba70 100644
--- a/src/smt/update_ostream.h
+++ b/src/smt/update_ostream.h
@@ -72,7 +72,7 @@ public:
 class OptionsErrOstreamUpdate : public OstreamUpdate {
  public:
   std::ostream& get() override { return *(options::err()); }
-  void set(std::ostream* setTo) override { return options::err.set(setTo); }
+  void set(std::ostream* setTo) override { return Options::current().set(options::err, setTo); }
 };  /* class OptionsErrOstreamUpdate */
 
 class DumpOstreamUpdate : public OstreamUpdate {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 4687922a0..ce8e2393b 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2906,10 +2906,10 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu
   if(d_qflraStatus != Result::UNSAT){
     static const int32_t pass2Limit = 20;
     int16_t oldCap = options::arithStandardCheckVarOrderPivots();
-    options::arithStandardCheckVarOrderPivots.set(pass2Limit);
+    Options::current().set(options::arithStandardCheckVarOrderPivots, pass2Limit);
     SimplexDecisionProcedure& simplex = selectSimplex(false);
     d_qflraStatus = simplex.findModel(false);
-    options::arithStandardCheckVarOrderPivots.set(oldCap);
+    Options::current().set(options::arithStandardCheckVarOrderPivots, oldCap);
   }
 
   if(Debug.isOn("arith::importSolution")){
@@ -3048,126 +3048,6 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
   return emmittedConflictOrSplit;
 }
 
-//   LinUnknown,  /* Unknown error */
-//   LinFeasible, /* Relaxation is feasible */
-//   LinInfeasible,   /* Relaxation is infeasible/all integer branches closed */
-//   LinExhausted
-//     // Fancy final tries the following strategy
-//     // At final check, try the preferred simplex solver with a pivot cap
-//     // If that failed, swap the the other simplex solver
-//     // If that failed, check if there are integer variables to cut
-//     // If that failed, do a simplex without a pivot limit
-
-//     int16_t oldCap = options::arithStandardCheckVarOrderPivots();
-
-//     static const int32_t pass2Limit = 10;
-//     static const int32_t relaxationLimit = 10000;
-//     static const int32_t mipLimit = 200000;
-
-//     //cout << "start" << endl;
-//     d_qflraStatus = simplex.findModel(false);
-//     //cout << "end" << endl;
-//     if(d_qflraStatus == Result::SAT_UNKNOWN ||
-//        (d_qflraStatus == Result::SAT && !hasIntegerModel() && !d_likelyIntegerInfeasible)){
-
-//       ApproximateSimplex* approxSolver = ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel, *(getTreeLog()), *(getApproxStats()));
-//       approxSolver->setPivotLimit(relaxationLimit);
-
-//       if(!d_guessedCoeffSet){
-//         d_guessedCoeffs = approxSolver->heuristicOptCoeffs();
-//         d_guessedCoeffSet = true;
-//       }
-//       if(!d_guessedCoeffs.empty()){
-//         approxSolver->setOptCoeffs(d_guessedCoeffs);
-//       }
-
-//       MipResult mipRes;
-//       ApproximateSimplex::Solution relaxSolution, mipSolution;
-//       LinResult relaxRes = approxSolver->solveRelaxation();
-//       switch(relaxRes){
-//       case LinFeasible:
-//         {
-//           relaxSolution = approxSolver->extractRelaxation();
-
-//           /* If the approximate solver  known to be integer infeasible
-//            * only redo*/
-//           int maxDepth =
-//             d_likelyIntegerInfeasible ? 1 : options::arithMaxBranchDepth();
-
-//           if(d_likelyIntegerInfeasible){
-//             d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
-//           }else{
-//             approxSolver->setPivotLimit(mipLimit);
-//             mipRes = approxSolver->solveMIP(false);
-//             if(mipRes == ApproximateSimplex::ApproxUnsat){
-//               mipRes = approxSolver->solveMIP(true);
-//             }
-//             d_errorSet.reduceToSignals();
-//             //CVC5Message() << "here" << endl;
-//             if(mipRes == ApproximateSimplex::ApproxSat){
-//               mipSolution = approxSolver->extractMIP();
-//               d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution);
-//             }else{
-//               if(mipRes == ApproximateSimplex::ApproxUnsat){
-//                 d_likelyIntegerInfeasible = true;
-//               }
-//               vector<Node> lemmas = approxSolver->getValidCuts();
-//               for(size_t i = 0; i < lemmas.size(); ++i){
-//                 d_approxCuts.pushback(lemmas[i]);
-//               }
-//               d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
-//             }
-//           }
-//           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
-//           if(d_qflraStatus != Result::UNSAT){ d_qflraStatus =
-//           simplex.findModel(false); }
-//           //CVC5Message() << "done" << endl;
-//         }
-//         break;
-//       case ApproximateSimplex::ApproxUnsat:
-//         {
-//           ApproximateSimplex::Solution sol =
-//           approxSolver->extractRelaxation();
-
-//           d_qflraStatus = d_attemptSolSimplex.attempt(sol);
-//           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
-
-//           if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); }
-//         }
-//         break;
-//       default:
-//         break;
-//       }
-//       delete approxSolver;
-//     }
-//   }
-
-//   if(!useFancyFinal){
-//     d_qflraStatus = simplex.findModel(noPivotLimit);
-//   }else{
-
-//     if(d_qflraStatus == Result::SAT_UNKNOWN){
-//       //CVC5Message() << "got sat unknown" << endl;
-//       vector<ArithVar> toCut = cutAllBounded();
-//       if(toCut.size() > 0){
-//         //branchVector(toCut);
-//         emmittedConflictOrSplit = true;
-//       }else{
-//         //CVC5Message() << "splitting" << endl;
-
-//         d_qflraStatus = simplex.findModel(noPivotLimit);
-//       }
-//     }
-//     options::arithStandardCheckVarOrderPivots.set(oldCap);
-//   }
-
-//   // TODO Save zeroes with no conflicts
-//   d_linEq.stopTrackingBoundCounts();
-//   d_partialModel.startQueueingBoundCounts();
-
-//   return emmittedConflictOrSplit;
-// }
-
 bool TheoryArithPrivate::hasFreshArithLiteral(Node n) const{
   switch(n.getKind()){
   case kind::LEQ:
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 0d62481f9..582d67b31 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
                                   Node query)
 {
   Assert (!query.isNull());
-  if (options::sygusExprMinerCheckTimeout.wasSetByUser())
+  if (Options::current().wasSetByUser(options::sygusExprMinerCheckTimeout))
   {
     initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout());
   }
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 232b9f736..62f362e2b 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -234,7 +234,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   std::unique_ptr<SmtEngine> repcChecker;
   // initialize the subsolver using the standard method
   initializeSubsolver(repcChecker,
-                      options::sygusRepairConstTimeout.wasSetByUser(),
+                      Options::current().wasSetByUser(options::sygusRepairConstTimeout),
                       options::sygusRepairConstTimeout());
   // renable options disabled by sygus
   repcChecker->setOption("miniscope-quant", "true");