4 files changed, 16 insertions, 26 deletions

diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 68ee629dc..c84854992 100644
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -28,8 +28,7 @@
 namespace cvc5 {
 namespace smt {
 
-OptionsManager::OptionsManager(Options* opts, ResourceManager* rm)
-    : d_options(opts), d_resourceManager(rm)
+OptionsManager::OptionsManager(Options* opts) : d_options(opts)
 {
   // set options that must take effect immediately
   if (opts->wasSetByUser(options::defaultExprDepth))
@@ -125,20 +124,6 @@ void OptionsManager::notifySetOption(const std::string& key)
 
 void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver)
 {
-  // set up the timeouts and resource limits
-  if ((*d_options)[options::perCallResourceLimit] != 0)
-  {
-    d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
-  }
-  if ((*d_options)[options::cumulativeResourceLimit] != 0)
-  {
-    d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(),
-                                        true);
-  }
-  if ((*d_options)[options::perCallMillisecondLimit] != 0)
-  {
-    d_resourceManager->setTimeLimit(options::perCallMillisecondLimit());
-  }
   // ensure that our heuristics are properly set up
   setDefaults(logic, isInternalSubsolver);
 }
diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h
index 4705b4273..2201ceb40 100644
--- a/src/smt/options_manager.h
+++ b/src/smt/options_manager.h
@@ -42,7 +42,7 @@ namespace smt {
 class OptionsManager : public OptionsListener
 {
  public:
-  OptionsManager(Options* opts, ResourceManager* rm = nullptr);
+  OptionsManager(Options* opts);
   ~OptionsManager();
   /**
    * Called when a set option call is made on the options object associated
@@ -65,8 +65,6 @@ class OptionsManager : public OptionsListener
  private:
   /** Reference to the options object */
   Options* d_options;
-  /** Pointer to the resource manager */
-  ResourceManager* d_resourceManager;
   /** Manager for the memory of regular-output-channel. */
   ManagedRegularOutputChannel d_managedRegularChannel;
   /** Manager for the memory of diagnostic-output-channel. */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c877b7ce3..88cb078ae 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -123,7 +123,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // non-null. This may throw an options exception.
   d_env->setOptions(optr);
   // set the options manager
-  d_optm.reset(new smt::OptionsManager(&getOptions(), getResourceManager()));
+  d_optm.reset(new smt::OptionsManager(&getOptions()));
   // listen to node manager events
   getNodeManager()->subscribeEvents(d_snmListener.get());
   // listen to resource out
@@ -1841,13 +1841,20 @@ void SmtEngine::interrupt()
   d_smtSolver->interrupt();
 }
 
-void SmtEngine::setResourceLimit(unsigned long units, bool cumulative)
+void SmtEngine::setResourceLimit(uint64_t units, bool cumulative)
 {
-  getResourceManager()->setResourceLimit(units, cumulative);
+  if (cumulative)
+  {
+    d_env->d_options.set(options::cumulativeResourceLimit__option_t(), units);
+  }
+  else
+  {
+    d_env->d_options.set(options::perCallResourceLimit__option_t(), units);
+  }
 }
-void SmtEngine::setTimeLimit(unsigned long milis)
+void SmtEngine::setTimeLimit(uint64_t millis)
 {
-  getResourceManager()->setTimeLimit(milis);
+  d_env->d_options.set(options::perCallMillisecondLimit__option_t(), millis);
 }
 
 unsigned long SmtEngine::getResourceUsage() const
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 151b6106b..ff1a955ee 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -776,7 +776,7 @@ class CVC4_EXPORT SmtEngine
    * resource limit for all remaining calls into the SmtEngine (true), or
    * whether it's a per-call resource limit (false); the default is false
    */
-  void setResourceLimit(unsigned long units, bool cumulative = false);
+  void setResourceLimit(uint64_t units, bool cumulative = false);
 
   /**
    * Set a per-call time limit for SmtEngine operations.
@@ -801,7 +801,7 @@ class CVC4_EXPORT SmtEngine
    *
    * @param millis the time limit in milliseconds, or 0 for no limit
    */
-  void setTimeLimit(unsigned long millis);
+  void setTimeLimit(uint64_t millis);
 
   /**
    * Get the current resource usage count for this SmtEngine.  This