diff options
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 10a729420..d17d5d141 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -31,6 +31,7 @@ #include "util/output.h" #include "util/resource_manager.h" #include "options/options.h" +#include "smt/options.h" using namespace std; using namespace CVC4::kind; @@ -499,14 +500,14 @@ Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) 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(); + d_resourceManager->spendResource(d_exprManager->getOptions()[options::parseStep]); } return cmd; } Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) { Debug("parser") << "nextExpression()" << std::endl; - d_resourceManager->spendResource(); + d_resourceManager->spendResource(d_exprManager->getOptions()[options::parseStep]); Expr result; if(!done()) { try { |