4 files changed, 6 insertions, 19 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index a5ce1bed0..bf12ee87d 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -35,7 +35,6 @@
 #include "parser/input.h"
 #include "parser/parser_exception.h"
 #include "smt/command.h"
-#include "util/resource_manager.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -47,8 +46,7 @@ Parser::Parser(api::Solver* solver,
                Input* input,
                bool strictMode,
                bool parseOnly)
-    : d_resourceManager(solver->getExprManager()->getResourceManager()),
-      d_input(input),
+    : d_input(input),
       d_symtabAllocated(),
       d_symtab(&d_symtabAllocated),
       d_assertionLevel(0),
@@ -743,19 +741,12 @@ Command* Parser::nextCommand()
     }
   }
   Debug("parser") << "nextCommand() => " << cmd << std::endl;
-  if (cmd != NULL && dynamic_cast<SetOptionCommand*>(cmd) == NULL &&
-      dynamic_cast<QuitCommand*>(cmd) == NULL) {
-    // don't count set-option commands as to not get stuck in an infinite
-    // loop of resourcing out
-    d_resourceManager->spendResource(ResourceManager::Resource::ParseStep);
-  }
   return cmd;
 }
 
 api::Term Parser::nextExpression()
 {
   Debug("parser") << "nextExpression()" << std::endl;
-  d_resourceManager->spendResource(ResourceManager::Resource::ParseStep);
   api::Term result;
   if (!done()) {
     try {
@@ -920,8 +911,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
 
 api::Term Parser::mkStringConstant(const std::string& s)
 {
-  ExprManager* em = d_solver->getExprManager();
-  if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage()))
+  if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage()))
   {
     return api::Term(d_solver, d_solver->mkString(s, true).getExpr());
   }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 84dd4be0c..b993b08fb 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -135,8 +135,6 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
 class CVC4_PUBLIC Parser {
   friend class ParserBuilder;
 private:
- /** The resource manager associated with this expr manager */
- ResourceManager* d_resourceManager;
 
  /** The input that we're parsing. */
  Input* d_input;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index aba409109..46a2e2c59 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -332,8 +332,7 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
 
 bool Smt2::isHoEnabled() const
 {
-  return getLogic().isHigherOrder()
-         && d_solver->getExprManager()->getOptions().getUfHo();
+  return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo();
 }
 
 bool Smt2::logicIsSet() {
@@ -999,7 +998,7 @@ void Smt2::addSygusConstructorVariables(api::DatatypeDecl& dt,
 
 InputLanguage Smt2::getLanguage() const
 {
-  return d_solver->getExprManager()->getOptions().getInputLanguage();
+  return d_solver->getOptions().getInputLanguage();
 }
 
 void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
@@ -1162,7 +1161,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     }
   }
   // Second phase: apply the arguments to the parse op
-  const Options& opts = d_solver->getExprManager()->getOptions();
+  const Options& opts = d_solver->getOptions();
   // handle special cases
   if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull())
   {
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 403cab42b..cb4d3fd9e 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -311,7 +311,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     isBuiltinKind = true;
   }
   assert(kind != api::NULL_EXPR);
-  const Options& opts = d_solver->getExprManager()->getOptions();
+  const Options& opts = d_solver->getOptions();
   // Second phase: apply parse op to the arguments
   if (isBuiltinKind)
   {