Merge branch 'master' into rm-bv-div-zero-const-refsrm-bv-div-zero-const-refs

5 files changed, 157 insertions, 95 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index c8e977f1f..5759ec856 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -26,6 +26,7 @@
 #include <vector>
 
 #include "main/main.h"
+#include "options/options_public.h"
 #include "smt/command.h"
 #include "smt/smt_engine.h"
 
@@ -64,7 +65,7 @@ CommandExecutor::~CommandExecutor()
 
 void CommandExecutor::printStatistics(std::ostream& out) const
 {
-  if (d_options.getStatistics())
+  if (options::getStatistics(d_options))
   {
     getSmtEngine()->printStatistics(out);
   }
@@ -72,7 +73,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const
 
 void CommandExecutor::printStatisticsSafe(int fd) const
 {
-  if (d_options.getStatistics())
+  if (options::getStatistics(d_options))
   {
     getSmtEngine()->printStatisticsSafe(fd);
   }
@@ -80,7 +81,8 @@ void CommandExecutor::printStatisticsSafe(int fd) const
 
 bool CommandExecutor::doCommand(Command* cmd)
 {
-  if( d_options.getParseOnly() ) {
+  if (options::getParseOnly(d_options))
+  {
     return true;
   }
 
@@ -98,8 +100,9 @@ bool CommandExecutor::doCommand(Command* cmd)
 
     return status;
   } else {
-    if(d_options.getVerbosity() > 2) {
-      *d_options.getOut() << "Invoking: " << *cmd << std::endl;
+    if (options::getVerbosity(d_options) > 2)
+    {
+      *options::getOut(d_options) << "Invoking: " << *cmd << std::endl;
     }
 
     return doCommandSingleton(cmd);
@@ -108,7 +111,7 @@ bool CommandExecutor::doCommand(Command* cmd)
 
 void CommandExecutor::reset()
 {
-  printStatistics(*d_options.getErr());
+  printStatistics(*options::getErr(d_options));
   /* We have to keep options passed via CL on reset. These options are stored
    * in CommandExecutor::d_options (populated and created in the driver), and
    * CommandExecutor::d_options only contains *these* options since the
@@ -121,10 +124,13 @@ void CommandExecutor::reset()
 bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
-  if(d_options.getVerbosity() >= -1) {
-    status =
-        solverInvoke(d_solver.get(), d_symman.get(), cmd, d_options.getOut());
-  } else {
+  if (options::getVerbosity(d_options) >= -1)
+  {
+    status = solverInvoke(
+        d_solver.get(), d_symman.get(), cmd, options::getOut(d_options));
+  }
+  else
+  {
     status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr);
   }
 
@@ -144,8 +150,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     d_result = res = q->getResult();
   }
 
-  if((cs != nullptr || q != nullptr) && d_options.getStatsEveryQuery()) {
-    getSmtEngine()->printStatisticsDiff(*d_options.getErr());
+  if ((cs != nullptr || q != nullptr) && options::getStatsEveryQuery(d_options))
+  {
+    getSmtEngine()->printStatisticsDiff(*options::getErr(d_options));
   }
 
   bool isResultUnsat = res.isUnsat() || res.isEntailed();
@@ -153,20 +160,21 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   // dump the model/proof/unsat core if option is set
   if (status) {
     std::vector<std::unique_ptr<Command> > getterCommands;
-    if (d_options.getDumpModels()
+    if (options::getDumpModels(d_options)
         && (res.isSat()
             || (res.isSatUnknown()
                 && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
     {
       getterCommands.emplace_back(new GetModelCommand());
     }
-    if (d_options.getDumpProofs() && isResultUnsat)
+    if (options::getDumpProofs(d_options) && isResultUnsat)
     {
       getterCommands.emplace_back(new GetProofCommand());
     }
 
-    if (d_options.getDumpInstantiations()
-        && ((d_options.getInstFormatMode() != options::InstFormatMode::SZS
+    if (options::getDumpInstantiations(d_options)
+        && ((options::getInstFormatMode(d_options)
+                 != options::InstFormatMode::SZS
              && (res.isSat()
                  || (res.isSatUnknown()
                      && res.getUnknownExplanation()
@@ -176,14 +184,15 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
       getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
-    if (d_options.getDumpUnsatCores() && isResultUnsat)
+    if (options::getDumpUnsatCores(d_options) && isResultUnsat)
     {
       getterCommands.emplace_back(new GetUnsatCoreCommand());
     }
 
     if (!getterCommands.empty()) {
       // set no time limit during dumping if applicable
-      if (d_options.getForceNoLimitCpuWhileDump()) {
+      if (options::getForceNoLimitCpuWhileDump(d_options))
+      {
         setNoLimitCPU();
       }
       for (const auto& getterCommand : getterCommands) {
@@ -222,11 +231,18 @@ bool solverInvoke(api::Solver* solver,
 }
 
 void CommandExecutor::flushOutputStreams() {
-  printStatistics(*(d_options.getErr()));
+  printStatistics(*(options::getErr(d_options)));
 
   // make sure out and err streams are flushed too
-  d_options.flushOut();
-  d_options.flushErr();
+
+  if (options::getOut(d_options) != nullptr)
+  {
+    *options::getOut(d_options) << std::flush;
+  }
+  if (options::getErr(d_options) != nullptr)
+  {
+    *options::getErr(d_options) << std::flush;
+  }
 }
 
 }  // namespace main
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index a26ee3b73..79c98924a 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -34,6 +34,7 @@
 #include "main/signal_handlers.h"
 #include "main/time_limit.h"
 #include "options/options.h"
+#include "options/options_public.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -78,16 +79,17 @@ TotalTimer::~TotalTimer()
 
 void printUsage(Options& opts, bool full) {
   stringstream ss;
-  ss << "usage: " << opts.getBinaryName() << " [options] [input-file]" << endl
+  ss << "usage: " << options::getBinaryName(opts) << " [options] [input-file]"
+     << endl
      << endl
      << "Without an input file, or with `-', cvc5 reads from standard input."
      << endl
      << endl
      << "cvc5 options:" << endl;
   if(full) {
-    Options::printUsage( ss.str(), *(opts.getOut()) );
+    Options::printUsage(ss.str(), *(options::getOut(opts)));
   } else {
-    Options::printShortUsage( ss.str(), *(opts.getOut()) );
+    Options::printShortUsage(ss.str(), *(options::getOut(opts)));
   }
 }
 
@@ -107,25 +109,30 @@ int runCvc5(int argc, char* argv[], Options& opts)
 
   auto limit = install_time_limit(opts);
 
-  string progNameStr = opts.getBinaryName();
+  string progNameStr = options::getBinaryName(opts);
   progName = &progNameStr;
 
-  if( opts.getHelp() ) {
+  if (options::getHelp(opts))
+  {
     printUsage(opts, true);
     exit(1);
-  } else if( opts.getLanguageHelp() ) {
-    Options::printLanguageHelp(*(opts.getOut()));
+  }
+  else if (options::getLanguageHelp(opts))
+  {
+    Options::printLanguageHelp(*(options::getOut(opts)));
     exit(1);
-  } else if( opts.getVersion() ) {
-    *(opts.getOut()) << Configuration::about().c_str() << flush;
+  }
+  else if (options::getVersion(opts))
+  {
+    *(options::getOut(opts)) << Configuration::about().c_str() << flush;
     exit(0);
   }
 
-  segvSpin = opts.getSegvSpin();
+  segvSpin = options::getSegvSpin(opts);
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC5_COMPETITION_MODE
-  *(opts.getOut()) << unitbuf;
+  *(options::getOut(opts)) << unitbuf;
 #endif /* CVC5_COMPETITION_MODE */
 
   // We only accept one input file
@@ -137,8 +144,9 @@ int runCvc5(int argc, char* argv[], Options& opts)
   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 
   // if we're reading from stdin on a TTY, default to interactive mode
-  if(!opts.wasSetByUserInteractive()) {
-    opts.setInteractive(inputFromStdin && isatty(fileno(stdin)));
+  if (!options::wasSetByUserInteractive(opts))
+  {
+    options::setInteractive(inputFromStdin && isatty(fileno(stdin)), opts);
   }
 
   // Auto-detect input language by filename extension
@@ -150,30 +158,33 @@ int runCvc5(int argc, char* argv[], Options& opts)
   }
   const char* filename = filenameStr.c_str();
 
-  if(opts.getInputLanguage() == language::input::LANG_AUTO) {
+  if (options::getInputLanguage(opts) == language::input::LANG_AUTO)
+  {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
-      opts.setInputLanguage(language::input::LANG_CVC);
+      options::setInputLanguage(language::input::LANG_CVC, opts);
     } else {
-      unsigned len = filenameStr.size();
+      size_t len = filenameStr.size();
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6);
+        options::setInputLanguage(language::input::LANG_SMTLIB_V2_6, opts);
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
-        opts.setInputLanguage(language::input::LANG_TPTP);
+        options::setInputLanguage(language::input::LANG_TPTP, opts);
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        opts.setInputLanguage(language::input::LANG_CVC);
+        options::setInputLanguage(language::input::LANG_CVC, opts);
       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
         // version 2 sygus is the default
-        opts.setInputLanguage(language::input::LANG_SYGUS_V2);
+        options::setInputLanguage(language::input::LANG_SYGUS_V2, opts);
       }
     }
   }
 
-  if(opts.getOutputLanguage() == language::output::LANG_AUTO) {
-    opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
+  if (options::getOutputLanguage(opts) == language::output::LANG_AUTO)
+  {
+    options::setOutputLanguage(
+        language::toOutputLanguage(options::getInputLanguage(opts)), opts);
   }
 
   // Determine which messages to show based on smtcomp_mode and verbosity
@@ -187,7 +198,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
   }
 
   // important even for muzzled builds (to get result output right)
-  (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
+  (*(options::getOut(opts)))
+      << language::SetLanguage(options::getOutputLanguage(opts));
 
   // Create the command executor to execute the parsed commands
   pExecutor = std::make_unique<CommandExecutor>(opts);
@@ -200,19 +212,23 @@ int runCvc5(int argc, char* argv[], Options& opts)
     // Parse and execute commands until we are done
     std::unique_ptr<Command> cmd;
     bool status = true;
-    if(opts.getInteractive() && inputFromStdin) {
-      if(opts.getTearDownIncremental() > 0) {
+    if (options::getInteractive(opts) && inputFromStdin)
+    {
+      if (options::getTearDownIncremental(opts) > 0)
+      {
         throw Exception(
             "--tear-down-incremental doesn't work in interactive mode");
       }
-      if(!opts.wasSetByUserIncrementalSolving()) {
+      if (!options::wasSetByUserIncrementalSolving(opts))
+      {
         cmd.reset(new SetOptionCommand("incremental", "true"));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
       }
       InteractiveShell shell(pExecutor->getSolver(),
                              pExecutor->getSymbolManager());
-      if(opts.getInteractivePrompt()) {
+      if (options::getInteractivePrompt(opts))
+      {
         CVC5Message() << Configuration::getPackageName() << " "
                       << Configuration::getVersionString();
         if(Configuration::isGitBuild()) {
@@ -230,7 +246,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
         try {
           cmd.reset(shell.readCommand());
         } catch(UnsafeInterruptException& e) {
-          (*opts.getOut()) << CommandInterrupted();
+          (*options::getOut(opts)) << CommandInterrupted();
           break;
         }
         if (cmd == nullptr)
@@ -240,14 +256,18 @@ int runCvc5(int argc, char* argv[], Options& opts)
           break;
         }
       }
-    } else if( opts.getTearDownIncremental() > 0) {
-      if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
+    }
+    else if (options::getTearDownIncremental(opts) > 0)
+    {
+      if (!options::getIncrementalSolving(opts)
+          && options::getTearDownIncremental(opts) > 1)
+      {
         // For tear-down-incremental values greater than 1, need incremental
         // on too.
         cmd.reset(new SetOptionCommand("incremental", "true"));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
-        // if(opts.wasSetByUserIncrementalSolving()) {
+        // if(options::wasSetByUserIncrementalSolving(opts)) {
         //   throw OptionException(
         //     "--tear-down-incremental incompatible with --incremental");
         // }
@@ -262,13 +282,14 @@ int runCvc5(int argc, char* argv[], Options& opts)
                                   opts);
       std::unique_ptr<Parser> parser(parserBuilder.build());
       if( inputFromStdin ) {
-        parser->setInput(
-            Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+        parser->setInput(Input::newStreamInput(
+            options::getInputLanguage(opts), cin, filename));
       }
       else
       {
-        parser->setInput(Input::newFileInput(
-            opts.getInputLanguage(), filename, opts.getMemoryMap()));
+        parser->setInput(Input::newFileInput(options::getInputLanguage(opts),
+                                             filename,
+                                             options::getMemoryMap(opts)));
       }
 
       vector< vector<Command*> > allCommands;
@@ -279,7 +300,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
       while (status)
       {
         if (interrupted) {
-          (*opts.getOut()) << CommandInterrupted();
+          (*options::getOut(opts)) << CommandInterrupted();
           break;
         }
 
@@ -292,7 +313,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
         }
 
         if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
-          if(needReset >= opts.getTearDownIncremental()) {
+          if (needReset >= options::getTearDownIncremental(opts))
+          {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
               if (interrupted) break;
@@ -320,7 +342,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
           }
         } else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
           allCommands.pop_back(); // fixme leaks cmds here
-          if (needReset >= opts.getTearDownIncremental()) {
+          if (needReset >= options::getTearDownIncremental(opts))
+          {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
@@ -335,9 +358,11 @@ int runCvc5(int argc, char* argv[], Options& opts)
               }
             }
             if (interrupted) continue;
-            (*opts.getOut()) << CommandSuccess();
+            (*options::getOut(opts)) << CommandSuccess();
             needReset = 0;
-          } else {
+          }
+          else
+          {
             status = pExecutor->doCommand(cmd);
             if(cmd->interrupted()) {
               interrupted = true;
@@ -346,7 +371,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
           }
         } else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
                   dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
-          if(needReset >= opts.getTearDownIncremental()) {
+          if (needReset >= options::getTearDownIncremental(opts))
+          {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
@@ -362,7 +388,9 @@ int runCvc5(int argc, char* argv[], Options& opts)
               }
             }
             needReset = 0;
-          } else {
+          }
+          else
+          {
             ++needReset;
           }
           if (interrupted) {
@@ -406,8 +434,11 @@ int runCvc5(int argc, char* argv[], Options& opts)
           }
         }
       }
-    } else {
-      if(!opts.wasSetByUserIncrementalSolving()) {
+    }
+    else
+    {
+      if (!options::wasSetByUserIncrementalSolving(opts))
+      {
         cmd.reset(new SetOptionCommand("incremental", "false"));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
@@ -418,20 +449,21 @@ int runCvc5(int argc, char* argv[], Options& opts)
                                   opts);
       std::unique_ptr<Parser> parser(parserBuilder.build());
       if( inputFromStdin ) {
-        parser->setInput(
-            Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+        parser->setInput(Input::newStreamInput(
+            options::getInputLanguage(opts), cin, filename));
       }
       else
       {
-        parser->setInput(Input::newFileInput(
-            opts.getInputLanguage(), filename, opts.getMemoryMap()));
+        parser->setInput(Input::newFileInput(options::getInputLanguage(opts),
+                                             filename,
+                                             options::getMemoryMap(opts)));
       }
 
       bool interrupted = false;
       while (status)
       {
         if (interrupted) {
-          (*opts.getOut()) << CommandInterrupted();
+          (*options::getOut(opts)) << CommandInterrupted();
           pExecutor->reset();
           break;
         }
@@ -465,7 +497,10 @@ int runCvc5(int argc, char* argv[], Options& opts)
     }
 
 #ifdef CVC5_COMPETITION_MODE
-    opts.flushOut();
+    if (cvc5::options::getOut(opts) != nullptr)
+    {
+      cvc5::options::getOut(opts) << std::flush;
+    }
     // exit, don't return (don't want destructors to run)
     // _exit() from unistd.h doesn't run global destructors
     // or other on_exit/atexit stuff.
@@ -476,11 +511,13 @@ int runCvc5(int argc, char* argv[], Options& opts)
     pExecutor->flushOutputStreams();
 
 #ifdef CVC5_DEBUG
-    if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) {
+    if (options::getEarlyExit(opts) && options::wasSetByUserEarlyExit(opts))
+    {
       _exit(returnValue);
     }
 #else  /* CVC5_DEBUG */
-    if(opts.getEarlyExit()) {
+    if (options::getEarlyExit(opts))
+    {
       _exit(returnValue);
     }
 #endif /* CVC5_DEBUG */
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 8ca10799f..9a0539490 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -42,6 +42,7 @@
 #include "expr/symbol_manager.h"
 #include "options/language.h"
 #include "options/options.h"
+#include "options/options_public.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -87,15 +88,16 @@ static set<string> s_declarations;
 
 InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
     : d_options(solver->getOptions()),
-      d_in(*d_options.getIn()),
-      d_out(*d_options.getOutConst()),
+      d_in(*options::getIn(d_options)),
+      d_out(*options::getOut(d_options)),
       d_quit(false)
 {
   ParserBuilder parserBuilder(solver, sm, d_options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.build();
-  if(d_options.wasSetByUserForceLogicString()) {
-    LogicInfo tmp(d_options.getForceLogicString());
+  if (options::wasSetByUserForceLogicString(d_options))
+  {
+    LogicInfo tmp(options::getForceLogicString(d_options));
     d_parser->forceLogic(tmp.getLogicString());
   }
 
@@ -109,7 +111,8 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
 #endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
     ::using_history();
 
-    OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage());
+    OutputLanguage lang =
+        toOutputLanguage(options::getInputLanguage(d_options));
     switch(lang) {
       case output::LANG_CVC:
         d_historyFilename = string(getenv("HOME")) + "/.cvc5_history";
@@ -195,7 +198,7 @@ restart:
   if (d_usingEditline)
   {
 #if HAVE_LIBEDITLINE
-    lineBuf = ::readline(d_options.getInteractivePrompt()
+    lineBuf = ::readline(options::getInteractivePrompt(d_options)
                              ? (line == "" ? "cvc5> " : "... > ")
                              : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
@@ -207,7 +210,8 @@ restart:
   }
   else
   {
-    if(d_options.getInteractivePrompt()) {
+    if (options::getInteractivePrompt(d_options))
+    {
       if(line == "") {
         d_out << "cvc5> " << flush;
       } else {
@@ -280,7 +284,8 @@ restart:
       if (d_usingEditline)
       {
 #if HAVE_LIBEDITLINE
-        lineBuf = ::readline(d_options.getInteractivePrompt() ? "... > " : "");
+        lineBuf = ::readline(options::getInteractivePrompt(d_options) ? "... > "
+                                                                      : "");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
         }
@@ -290,7 +295,8 @@ restart:
       }
       else
       {
-        if(d_options.getInteractivePrompt()) {
+        if (options::getInteractivePrompt(d_options))
+        {
           d_out << "... > " << flush;
         }
 
@@ -306,8 +312,8 @@ restart:
     }
   }
 
-  d_parser->setInput(Input::newStringInput(d_options.getInputLanguage(),
-                                           input, INPUT_FILENAME));
+  d_parser->setInput(Input::newStringInput(
+      options::getInputLanguage(d_options), input, INPUT_FILENAME));
 
   /* There may be more than one command in the input. Build up a
      sequence. */
@@ -358,7 +364,7 @@ restart:
   }
   catch (ParserException& pe)
   {
-    if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
+    if (language::isOutputLang_smt2(options::getOutputLanguage(d_options)))
     {
       d_out << "(error \"" << pe << "\")" << endl;
     }
diff --git a/src/main/main.cpp b/src/main/main.cpp
index b96598b0b..2b25e6c93 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -14,12 +14,13 @@
  */
 #include "main/main.h"
 
+#include <stdio.h>
+#include <unistd.h>
+
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
 #include <iostream>
-#include <stdio.h>
-#include <unistd.h>
 
 #include "base/configuration.h"
 #include "base/output.h"
@@ -28,6 +29,7 @@
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/options.h"
+#include "options/options_public.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
@@ -51,25 +53,25 @@ int main(int argc, char* argv[]) {
     return runCvc5(argc, argv, opts);
   } catch(OptionException& e) {
 #ifdef CVC5_COMPETITION_MODE
-    *opts.getOut() << "unknown" << endl;
+    *options::getOut(opts) << "unknown" << endl;
 #endif
     cerr << "(error \"" << e << "\")" << endl
          << endl
          << "Please use --help to get help on command-line options." << endl;
   } catch(Exception& e) {
 #ifdef CVC5_COMPETITION_MODE
-    *opts.getOut() << "unknown" << endl;
+    *options::getOut(opts) << "unknown" << endl;
 #endif
-    if (language::isOutputLang_smt2(opts.getOutputLanguage()))
+    if (language::isOutputLang_smt2(options::getOutputLanguage(opts)))
     {
-      *opts.getOut() << "(error \"" << e << "\")" << endl;
+      *options::getOut(opts) << "(error \"" << e << "\")" << endl;
     } else {
-      *opts.getErr() << "(error \"" << e << "\")" << endl;
+      *options::getErr(opts) << "(error \"" << e << "\")" << endl;
     }
-    if (opts.getStatistics() && pExecutor != nullptr)
+    if (options::getStatistics(opts) && pExecutor != nullptr)
     {
       totalTime.reset();
-      pExecutor->printStatistics(*opts.getErr());
+      pExecutor->printStatistics(*options::getErr(opts));
     }
   }
   exit(1);
diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
index 0f0a824f6..c0fc6846a 100644
--- a/src/main/time_limit.cpp
+++ b/src/main/time_limit.cpp
@@ -56,6 +56,7 @@
 #include <cstring>
 
 #include "base/exception.h"
+#include "options/options_public.h"
 #include "signal_handlers.h"
 
 namespace cvc5 {
@@ -79,7 +80,7 @@ TimeLimit::~TimeLimit()
 
 TimeLimit install_time_limit(const Options& opts)
 {
-  unsigned long ms = opts.getCumulativeTimeLimit();
+  unsigned long ms = options::getCumulativeTimeLimit(opts);
   // Skip if no time limit shall be set.
   if (ms == 0) {
     return TimeLimit();