2 files changed, 20 insertions, 4 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 045cd4ae1..dc44ed5ba 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -26,9 +26,12 @@
 #include "parser/parser_exception.h"
 #include "expr/command.h"
 #include "expr/expr.h"
+#include "expr/node.h"
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "util/output.h"
+#include "util/resource_manager.h"
+#include "options/options.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -38,6 +41,7 @@ namespace parser {
 
 Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
   d_exprManager(exprManager),
+  d_resourceManager(d_exprManager->getResourceManager()),
   d_input(input),
   d_symtabAllocated(),
   d_symtab(&d_symtabAllocated),
@@ -460,7 +464,7 @@ void Parser::preemptCommand(Command* cmd) {
   d_commandQueue.push_back(cmd);
 }
 
-Command* Parser::nextCommand() throw(ParserException) {
+Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) {
   Debug("parser") << "nextCommand()" << std::endl;
   Command* cmd = NULL;
   if(!d_commandQueue.empty()) {
@@ -483,11 +487,19 @@ Command* Parser::nextCommand() throw(ParserException) {
     }
   }
   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();
+  }
   return cmd;
 }
 
-Expr Parser::nextExpression() throw(ParserException) {
+Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) {
   Debug("parser") << "nextExpression()" << std::endl;
+  d_resourceManager->spendResource();
   Expr result;
   if(!done()) {
     try {
diff --git a/src/parser/parser.h b/src/parser/parser.h
index ffe33a980..53241709d 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -30,6 +30,7 @@
 #include "expr/symbol_table.h"
 #include "expr/kind.h"
 #include "expr/expr_stream.h"
+#include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 
@@ -39,6 +40,7 @@ class ExprManager;
 class Command;
 class FunctionType;
 class Type;
+class ResourceManager;
 
 namespace parser {
 
@@ -108,6 +110,8 @@ class CVC4_PUBLIC Parser {
 
   /** The expression manager */
   ExprManager *d_exprManager;
+  /** The resource manager associated with this expr manager */
+  ResourceManager *d_resourceManager;
 
   /** The input that we're parsing. */
   Input *d_input;
@@ -504,10 +508,10 @@ public:
   bool isPredicate(const std::string& name);
 
   /** Parse and return the next command. */
-  Command* nextCommand() throw(ParserException);
+  Command* nextCommand() throw(ParserException, UnsafeInterruptException);
 
   /** Parse and return the next expression. */
-  Expr nextExpression() throw(ParserException);
+  Expr nextExpression() throw(ParserException, UnsafeInterruptException);
 
   /** Issue a warning to the user. */
   inline void warning(const std::string& msg) {