Resource-limiting work.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

58 files changed, 1111 insertions, 414 deletions

diff --git a/src/cvc4.i b/src/cvc4.i
index 62cd68cab..3ad08660c 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -153,6 +153,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %typemap(throws) CVC4::ScopeException = CVC4::Exception;
 %typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception;
 %typemap(throws) CVC4::AssertionException = CVC4::Exception;
+%typemap(throws) CVC4::UnsafeInterruptException = CVC4::Exception;
 %typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception;
 %typemap(throws) CVC4::parser::ParserException = CVC4::Exception;
 
@@ -293,6 +294,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 #endif /* SWIGJAVA */
 
 %include "util/exception.i"
+%include "util/unsafe_interrupt_exception.i"
 %include "util/integer.i"
 %include "util/rational.i"
 %include "util/language.i"
@@ -319,6 +321,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "util/regexp.i"
 %include "util/uninterpreted_constant.i"
 %include "util/proof.i"
+%include "util/resource_manager.i"
 
 %include "expr/kind.i"
 %include "expr/expr.i"
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 39ed89a68..61900e59d 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -30,6 +30,7 @@
 #include "theory/decision_attributes.h"
 #include "util/ite_removal.h"
 #include "util/output.h"
+#include "smt/smt_engine_scope.h"
 
 using namespace std;
 using namespace CVC4::prop;
@@ -117,6 +118,7 @@ public:
 
   /** Gets the next decision based on strategies that are enabled */
   SatLiteral getNext(bool &stopSearch) {
+    NodeManager::currentResourceManager()->spendResource();
     Assert(d_cnfStream != NULL,
            "Forgot to set cnfStream for decision engine?");
     Assert(d_satSolver != NULL,
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index be1b06cb8..242e018f6 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -39,6 +39,7 @@ namespace CVC4 {
 
 const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
 const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
+const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted();
 
 std::ostream& operator<<(std::ostream& out, const Command& c) throw() {
   c.toStream(out,
@@ -97,6 +98,10 @@ bool Command::fail() const throw() {
   return d_commandStatus != NULL && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL;
 }
 
+bool Command::interrupted() const throw() {
+  return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
+}
+
 void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
   invoke(smtEngine);
   if(!(isMuted() && ok())) {
@@ -201,6 +206,8 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->assertFormula(d_expr, d_inUnsatCore);
     d_commandStatus = CommandSuccess::instance();
+  } catch(UnsafeInterruptException& e) {
+    d_commandStatus = new CommandInterrupted();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
@@ -224,6 +231,8 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->push();
     d_commandStatus = CommandSuccess::instance();
+  } catch(UnsafeInterruptException& e) {
+    d_commandStatus = new CommandInterrupted();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
@@ -247,6 +256,8 @@ void PopCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->pop();
     d_commandStatus = CommandSuccess::instance();
+  } catch(UnsafeInterruptException& e) {
+    d_commandStatus = new CommandInterrupted();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
@@ -840,6 +851,8 @@ void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     d_result = smtEngine->simplify(d_term);
     d_commandStatus = CommandSuccess::instance();
+  } catch(UnsafeInterruptException& e) {
+    d_commandStatus = new CommandInterrupted();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
@@ -953,6 +966,8 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
     }
     d_result = em->mkExpr(kind::SEXPR, result);
     d_commandStatus = CommandSuccess::instance();
+  } catch(UnsafeInterruptException& e) {
+    d_commandStatus = new CommandInterrupted();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
@@ -1000,6 +1015,8 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     d_result = smtEngine->getAssignment();
     d_commandStatus = CommandSuccess::instance();
+  } catch(UnsafeInterruptException& e) {
+    d_commandStatus = new CommandInterrupted();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
@@ -1043,6 +1060,8 @@ void GetModelCommand::invoke(SmtEngine* smtEngine) throw() {
     d_result = smtEngine->getModel();
     d_smtEngine = smtEngine;
     d_commandStatus = CommandSuccess::instance();
+  } catch(UnsafeInterruptException& e) {
+    d_commandStatus = new CommandInterrupted();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
@@ -1089,6 +1108,8 @@ void GetProofCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     d_result = smtEngine->getProof();
     d_commandStatus = CommandSuccess::instance();
+  } catch(UnsafeInterruptException& e) {
+    d_commandStatus = new CommandInterrupted();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
diff --git a/src/expr/command.h b/src/expr/command.h
index c4f2fc1bc..cfa00bff4 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -168,6 +168,13 @@ public:
   CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); }
 };/* class CommandSuccess */
 
+class CVC4_PUBLIC CommandInterrupted : public CommandStatus {
+  static const CommandInterrupted* s_instance;
+public:
+  static const CommandInterrupted* instance() throw() { return s_instance; }
+  CommandStatus& clone() const { return const_cast<CommandInterrupted&>(*this); }
+};/* class CommandInterrupted */
+
 class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
 public:
   CommandStatus& clone() const { return *new CommandUnsupported(*this); }
@@ -240,6 +247,11 @@ public:
    */
   bool fail() const throw();
 
+  /**
+   * The command was ran but was interrupted due to resource limiting.
+   */
+  bool interrupted() const throw();
+
   /** Get the command status (it's NULL if we haven't run yet). */
   const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index fb9da3e37..c5249075b 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -130,6 +130,10 @@ const Options& ExprManager::getOptions() const {
   return d_nodeManager->getOptions();
 }
 
+ResourceManager* ExprManager::getResourceManager() throw() {
+  return d_nodeManager->getResourceManager();
+}
+
 BooleanType ExprManager::booleanType() const {
   NodeManagerScope nms(d_nodeManager);
   return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index deb2f6918..2fabea0ff 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -45,6 +45,7 @@ class Options;
 class IntStat;
 struct ExprManagerMapCollection;
 class StatisticsRegistry;
+class ResourceManager;
 
 namespace expr {
   namespace pickle {
@@ -120,9 +121,12 @@ public:
    */
   ~ExprManager() throw();
 
-  /** Get this node manager's options */
+  /** Get this expr manager's options */
   const Options& getOptions() const;
 
+  /** Get this expr manager's resource manager */
+  ResourceManager* getResourceManager() throw();
+
   /** Get the type for booleans */
   BooleanType booleanType() const;
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 5c2b81645..48aacddf2 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -22,7 +22,9 @@
 #include "expr/attribute.h"
 #include "util/cvc4_assert.h"
 #include "options/options.h"
+#include "smt/options.h"
 #include "util/statistics_registry.h"
+#include "util/resource_manager.h"
 #include "util/tls.h"
 
 #include "expr/type_checker.h"
@@ -83,6 +85,7 @@ struct NVReclaim {
 NodeManager::NodeManager(ExprManager* exprManager) :
   d_options(new Options()),
   d_statisticsRegistry(new StatisticsRegistry()),
+  d_resourceManager(new ResourceManager()),
   next_id(0),
   d_attrManager(new expr::attr::AttributeManager()),
   d_exprManager(exprManager),
@@ -97,6 +100,7 @@ NodeManager::NodeManager(ExprManager* exprManager,
                          const Options& options) :
   d_options(new Options(options)),
   d_statisticsRegistry(new StatisticsRegistry()),
+  d_resourceManager(new ResourceManager()),
   next_id(0),
   d_attrManager(new expr::attr::AttributeManager()),
   d_exprManager(exprManager),
@@ -117,6 +121,22 @@ void NodeManager::init() {
       d_operators[i] = mkConst(Kind(k));
     }
   }
+  d_resourceManager->setHardLimit((*d_options)[options::hardLimit]);
+  if((*d_options)[options::perCallResourceLimit] != 0) {
+    d_resourceManager->setResourceLimit((*d_options)[options::perCallResourceLimit], false);
+  }
+  if((*d_options)[options::cumulativeResourceLimit] != 0) {
+    d_resourceManager->setResourceLimit((*d_options)[options::cumulativeResourceLimit], true);
+  }
+  if((*d_options)[options::perCallMillisecondLimit] != 0) {
+    d_resourceManager->setTimeLimit((*d_options)[options::perCallMillisecondLimit], false);
+  }
+  if((*d_options)[options::cumulativeMillisecondLimit] != 0) {
+    d_resourceManager->setTimeLimit((*d_options)[options::cumulativeMillisecondLimit], true);
+  }
+  if((*d_options)[options::cpuTime]) {
+    d_resourceManager->useCPUTime(true);
+  }
 }
 
 NodeManager::~NodeManager() {
@@ -162,6 +182,8 @@ NodeManager::~NodeManager() {
   // defensive coding, in case destruction-order issues pop up (they often do)
   delete d_statisticsRegistry;
   d_statisticsRegistry = NULL;
+  delete d_resourceManager;
+  d_resourceManager = NULL;
   delete d_attrManager;
   d_attrManager = NULL;
   delete d_options;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d4d89109c..f4c3a1999 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -42,6 +42,7 @@
 namespace CVC4 {
 
 class StatisticsRegistry;
+class ResourceManager;
 
 namespace expr {
   namespace attr {
@@ -101,6 +102,7 @@ class NodeManager {
 
   Options* d_options;
   StatisticsRegistry* d_statisticsRegistry;
+  ResourceManager* d_resourceManager;
 
   NodeValuePool d_nodeValuePool;
 
@@ -317,6 +319,8 @@ public:
 
   /** The node manager in the current public-facing CVC4 library context */
   static NodeManager* currentNM() { return s_current; }
+  /** The resource manager associated with the current node manager */
+  static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; }
 
   /** Get this node manager's options (const version) */
   const Options& getOptions() const {
@@ -328,6 +332,9 @@ public:
     return *d_options;
   }
 
+  /** Get this node manager's resource manager */
+  ResourceManager* getResourceManager() throw() { return d_resourceManager; }
+
   /** Get this node manager's statistics registry */
   StatisticsRegistry* getStatisticsRegistry() const throw() {
     return d_statisticsRegistry;
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index df71f13c9..9035ed8b8 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -298,8 +298,21 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         // have the replay parser use the declarations input interactively
         replayParser->useDeclarationsFrom(shell.getParser());
       }
-      while((cmd = shell.readCommand())) {
+
+      while(true) {
+        try {
+          cmd = shell.readCommand();
+        } catch(UnsafeInterruptException& e) {
+          *opts[options::out] << CommandInterrupted();
+          break;
+        }
+        if (cmd == NULL)
+          break;
         status = pExecutor->doCommand(cmd) && status;
+        if (cmd->interrupted()) {
+          delete cmd;
+          break;
+        }
         delete cmd;
       }
     } else if(opts[options::tearDownIncremental]) {
@@ -332,15 +345,34 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         replayParser->useDeclarationsFrom(parser);
       }
       bool needReset = false;
-      while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) {
+      // true if one of the commands was interrupted
+      bool interrupted = false;
+      while (status || opts[options::continuedExecution]) {
+        if (interrupted) {
+          *opts[options::out] << CommandInterrupted();
+          break;
+        }
+
+        try {
+          cmd = parser->nextCommand();
+          if (cmd == NULL) break;
+        } catch (UnsafeInterruptException& e) {
+          interrupted = true;
+          continue;
+        }
+
         if(dynamic_cast<PushCommand*>(cmd) != NULL) {
           if(needReset) {
             pExecutor->reset();
-            for(size_t i = 0; i < allCommands.size(); ++i) {
-              for(size_t j = 0; j < allCommands[i].size(); ++j) {
+            for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
+              if (interrupted) break;
+              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
                 Command* cmd = allCommands[i][j]->clone();
                 cmd->setMuted(true);
                 pExecutor->doCommand(cmd);
+                if(cmd->interrupted()) {
+                  interrupted = true;
+                }
                 delete cmd;
               }
             }
@@ -351,29 +383,44 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
           allCommands.pop_back(); // fixme leaks cmds here
           pExecutor->reset();
-          for(size_t i = 0; i < allCommands.size(); ++i) {
-            for(size_t j = 0; j < allCommands[i].size(); ++j) {
+          for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
+            for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
               Command* cmd = allCommands[i][j]->clone();
               cmd->setMuted(true);
               pExecutor->doCommand(cmd);
+              if(cmd->interrupted()) {
+                interrupted = true;
+              }
               delete cmd;
             }
           }
+          if (interrupted) continue;
           *opts[options::out] << CommandSuccess();
         } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
                   dynamic_cast<QueryCommand*>(cmd) != NULL) {
           if(needReset) {
             pExecutor->reset();
-            for(size_t i = 0; i < allCommands.size(); ++i) {
-              for(size_t j = 0; j < allCommands[i].size(); ++j) {
+            for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
+              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
                 Command* cmd = allCommands[i][j]->clone();
                 cmd->setMuted(true);
                 pExecutor->doCommand(cmd);
+                if(cmd->interrupted()) {
+                  interrupted = true;
+                }
                 delete cmd;
               }
             }
           }
+          if (interrupted) {
+            continue;
+          }
+
           status = pExecutor->doCommand(cmd);
+          if(cmd->interrupted()) {
+            interrupted = true;
+            continue;
+          }
           needReset = true;
         } else if(dynamic_cast<ResetCommand*>(cmd) != NULL) {
           pExecutor->doCommand(cmd);
@@ -396,6 +443,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
             allCommands.back().push_back(copy);
           }
           status = pExecutor->doCommand(cmd);
+          if(cmd->interrupted()) {
+            interrupted = true;
+            continue;
+          }
+
           if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
             delete cmd;
             break;
@@ -428,8 +480,27 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         // have the replay parser use the file's declarations
         replayParser->useDeclarationsFrom(parser);
       }
-      while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) {
+      bool interrupted = false;
+      while(status || opts[options::continuedExecution]) {
+        if (interrupted) {
+          *opts[options::out] << CommandInterrupted();
+          pExecutor->reset();
+          break;
+        }
+        try {
+          cmd = parser->nextCommand();
+          if (cmd == NULL) break;
+        } catch (UnsafeInterruptException& e) {
+          interrupted = true;
+          continue;
+        }
+
         status = pExecutor->doCommand(cmd);
+        if (cmd->interrupted() && status == 0) {
+          interrupted = true;
+          break;
+        }
+
         if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
           delete cmd;
           break;
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 0aee195e4..3b237f6a4 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -172,7 +172,7 @@ InteractiveShell::~InteractiveShell() {
 #endif /* HAVE_LIBREADLINE */
 }
 
-Command* InteractiveShell::readCommand() {
+Command* InteractiveShell::readCommand() throw (UnsafeInterruptException) {
   char* lineBuf = NULL;
   string line = "";
 
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 43054f980..ef55919a1 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -19,6 +19,7 @@
 #include <string>
 
 #include "util/language.h"
+#include "util/unsafe_interrupt_exception.h"
 #include "options/options.h"
 
 namespace CVC4 {
@@ -56,7 +57,7 @@ public:
    * Read a command from the interactive shell. This will read as
    * many lines as necessary to parse a well-formed command.
    */
-  Command* readCommand();
+  Command* readCommand() throw (UnsafeInterruptException);
 
   /**
    * Return the internal parser being used.
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) {
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 94ca46257..c24ed8372 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -179,7 +179,8 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
   if(tryToStream<CommandSuccess>(out, s) ||
      tryToStream<CommandFailure>(out, s) ||
-     tryToStream<CommandUnsupported>(out, s)) {
+     tryToStream<CommandUnsupported>(out, s) ||
+     tryToStream<CommandInterrupted>(out, s)) {
     return;
   }
 
@@ -373,6 +374,10 @@ static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
   }
 }
 
+static void toStream(std::ostream& out, const CommandInterrupted* s) throw() {
+  out << "INTERRUPTED" << endl;
+}
+
 static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
   out << "UNSUPPORTED" << endl;
 }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f8df9d906..2e1170666 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -905,7 +905,8 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
   if(tryToStream<CommandSuccess>(out, s, d_cvc3Mode) ||
      tryToStream<CommandFailure>(out, s, d_cvc3Mode) ||
-     tryToStream<CommandUnsupported>(out, s, d_cvc3Mode)) {
+     tryToStream<CommandUnsupported>(out, s, d_cvc3Mode) ||
+     tryToStream<CommandInterrupted>(out, s, d_cvc3Mode)) {
     return;
   }
 
@@ -1267,6 +1268,10 @@ static void toStream(std::ostream& out, const CommandUnsupported* s, bool cvc3Mo
   out << "UNSUPPORTED" << endl;
 }
 
+static void toStream(std::ostream& out, const CommandInterrupted* s, bool cvc3Mode) throw() {
+  out << "INTERRUPTED" << endl;
+}
+
 static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode) throw() {
   out << s->getMessage() << endl;
 }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 88bcce5ae..4f12ed012 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -794,7 +794,8 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
 
   if(tryToStream<CommandSuccess>(out, s, d_variant) ||
      tryToStream<CommandFailure>(out, s, d_variant) ||
-     tryToStream<CommandUnsupported>(out, s, d_variant)) {
+     tryToStream<CommandUnsupported>(out, s, d_variant) ||
+     tryToStream<CommandInterrupted>(out, s, d_variant)) {
     return;
   }
 
@@ -1208,6 +1209,10 @@ static void toStream(std::ostream& out, const CommandSuccess* s, Variant v) thro
   }
 }
 
+static void toStream(std::ostream& out, const CommandInterrupted* s, Variant v) throw() {
+  out << "interrupted" << endl;
+}
+
 static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) throw() {
 #ifdef CVC4_COMPETITION_MODE
   // if in competition mode, lie and say we're ok
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 71b8eb69d..aceb0f2e9 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -97,10 +97,6 @@ void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
   d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
 }
 
-bool BVMinisatSatSolver::spendResource(){
-  // Do nothing for the BV solver.
-  return false;
-}
 
 void BVMinisatSatSolver::interrupt(){
   d_minisat->interrupt();
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index fea437565..e163ddcfd 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -46,8 +46,11 @@ private:
       d_notify->notify(satClause);
     }
 
+    void spendResource() {
+      d_notify->spendResource();
+    }
     void safePoint() {
-      d_notify->safePoint(); 
+      d_notify->safePoint();
     }
   };
 
@@ -86,8 +89,6 @@ public:
 
   void markUnremovable(SatLiteral lit);
 
-  bool spendResource();
-
   void interrupt();
   
   SatValue solve();
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 882f23ef7..a7a55208d 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -52,6 +52,7 @@ public:
    */
   virtual void notify(vec<Lit>& learnt) = 0;
 
+  virtual void spendResource() = 0;
   virtual void safePoint() = 0;
 };
 
@@ -412,8 +413,10 @@ inline void     Solver::interrupt(){ asynch_interrupt = true; }
 inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
 inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
 inline bool     Solver::withinBudget() const {
-    Assert (notify); 
-    notify->safePoint(); 
+    Assert (notify);
+    notify->spendResource();
+    notify->safePoint();
+
     return !asynch_interrupt &&
            (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
            (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index ad187aa46..8d7b014cc 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -30,6 +30,7 @@
 #include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
 #include "prop/minisat/minisat.h"
+#include "smt/smt_engine_scope.h"
 #include <queue>
 
 using namespace std;
@@ -665,6 +666,12 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated
 void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
+  if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
+    NodeManager::currentResourceManager()->spendResource();
+    d_convertAndAssertCounter = 0;
+  }
+  ++d_convertAndAssertCounter;
+
   switch(node.getKind()) {
   case AND:
     convertAndAssertAnd(node, negated);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index b76051279..b22290ae4 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -74,6 +74,12 @@ protected:
    */
   const bool d_fullLitToNodeMap;
 
+  /**
+   * Counter for resource limiting that is used to spend a resource
+   * every ResourceManager::resourceCounter calls to convertAndAssert.
+   */
+  unsigned long d_convertAndAssertCounter;
+
   /** The "registrar" for pre-registration of terms */
   Registrar* d_registrar;
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index e5e28bb0b..ea370ac08 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1593,7 +1593,7 @@ CRef Solver::updateLemmas() {
   Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
 
   // Avoid adding lemmas indefinitely without resource-out
-  spendResource();
+  proxy->spendResource();
 
   CRef conflict = CRef_Undef;
 
@@ -1710,3 +1710,15 @@ CRef Solver::updateLemmas() {
 
   return conflict;
 }
+
+inline bool Solver::withinBudget() const {
+  Assert (proxy);
+  // spendResource sets async_interrupt or throws UnsafeInterruptException
+  // depending on whether hard-limit is enabled
+  proxy->spendResource();
+
+  bool within_budget =  !asynch_interrupt &&
+    (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
+    (propagation_budget < 0 || propagations < (uint64_t)propagation_budget);
+  return within_budget;
+}
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 6d9fd538f..3ec19b026 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -219,7 +219,6 @@ public:
     void    budgetOff();
     void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
     void    clearInterrupt();     // Clear interrupt indicator flag.
-    void    spendResource();
 
     // Memory managment:
     //
@@ -535,11 +534,6 @@ inline void     Solver::setPropBudget(int64_t x){ propagation_budget = propagati
 inline void     Solver::interrupt(){ asynch_interrupt = true; }
 inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
 inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
-inline bool     Solver::withinBudget() const {
-    return !asynch_interrupt &&
-           (conflict_budget    < 0 || conflicts + resources_consumed < (uint64_t)conflict_budget) &&
-           (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
-inline void     Solver::spendResource() { ++resources_consumed; }
 
 // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
 // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 99341455c..b9fa37230 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -182,10 +182,6 @@ SatValue MinisatSatSolver::solve() {
   return toSatLiteralValue(d_minisat->solve());
 }
 
-bool MinisatSatSolver::spendResource() {
-  d_minisat->spendResource();
-  return !d_minisat->withinBudget();
-}
 
 void MinisatSatSolver::interrupt() {
   d_minisat->interrupt();
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 96893fe41..7c6e10170 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -61,7 +61,6 @@ public:
   SatValue solve();
   SatValue solve(long unsigned int&);
 
-  bool spendResource();
   void interrupt();
 
   SatValue value(SatLiteral l);
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index a998d4240..c7dae533e 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -32,6 +32,7 @@
 #include "main/options.h"
 #include "util/output.h"
 #include "util/result.h"
+#include "util/resource_manager.h"
 #include "expr/expr.h"
 #include "expr/command.h"
 
@@ -74,8 +75,8 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
   d_satSolver(NULL),
   d_registrar(NULL),
   d_cnfStream(NULL),
-  d_satTimer(*this),
-  d_interrupted(false) {
+  d_interrupted(false),
+  d_resourceManager(NodeManager::currentResourceManager()) {
 
   Debug("prop") << "Constructing the PropEngine" << endl;
 
@@ -159,7 +160,7 @@ void PropEngine::printSatisfyingAssignment(){
   }
 }
 
-Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
+Result PropEngine::checkSat() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "PropEngine::checkSat()" << endl;
 
@@ -171,25 +172,23 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
   d_theoryEngine->presolve();
 
   if(options::preprocessOnly()) {
-    millis = resource = 0;
     return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
   }
 
-  // Set the timer
-  d_satTimer.set(millis);
-
   // Reset the interrupted flag
   d_interrupted = false;
 
   // Check the problem
-  SatValue result = d_satSolver->solve(resource);
-
-  millis = d_satTimer.elapsed();
+  SatValue result = d_satSolver->solve();
 
   if( result == SAT_VALUE_UNKNOWN ) {
-    Result::UnknownExplanation why =
-      d_satTimer.expired() ? Result::TIMEOUT :
-        (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT);
+
+    Result::UnknownExplanation why = Result::INTERRUPTED;
+    if (d_resourceManager->outOfTime())
+      why = Result::TIMEOUT;
+    if (d_resourceManager->outOfResources())
+      why = Result::RESOURCEOUT;
+
     return Result(Result::SAT_UNKNOWN, why);
   }
 
@@ -279,16 +278,11 @@ void PropEngine::interrupt() throw(ModalException) {
 
   d_interrupted = true;
   d_satSolver->interrupt();
-  d_theoryEngine->interrupt();
   Debug("prop") << "interrupt()" << endl;
 }
 
-void PropEngine::spendResource() throw() {
-  if(d_satSolver->spendResource()) {
-    d_satSolver->interrupt();
-    d_theoryEngine->interrupt();
-  }
-  checkTime();
+void PropEngine::spendResource() throw (UnsafeInterruptException) {
+  d_resourceManager->spendResource();
 }
 
 bool PropEngine::properExplanation(TNode node, TNode expl) const {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index ed022a64f..2750319e6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -24,12 +24,14 @@
 #include "expr/node.h"
 #include "options/options.h"
 #include "util/result.h"
+#include "util/unsafe_interrupt_exception.h"
 #include "smt/modal_exception.h"
 #include "proof/proof_manager.h"
 #include <sys/time.h>
 
 namespace CVC4 {
 
+class ResourceManager;
 class DecisionEngine;
 class TheoryEngine;
 
@@ -45,78 +47,6 @@ class DPLLSatSolverInterface;
 class PropEngine;
 
 /**
- * A helper class to keep track of a time budget and signal
- * the PropEngine when the budget expires.
- */
-class SatTimer {
-
-  PropEngine& d_propEngine;
-  unsigned long d_ms;
-  timeval d_limit;
-
-public:
-
-  /** Construct a SatTimer attached to the given PropEngine. */
-  SatTimer(PropEngine& propEngine) :
-    d_propEngine(propEngine),
-    d_ms(0) {
-  }
-
-  /** Is the timer currently active? */
-  bool on() const {
-    return d_ms != 0;
-  }
-
-  /** Set a millisecond timer (0==off). */
-  void set(unsigned long millis) {
-    d_ms = millis;
-    // keep track of when it was set, even if it's disabled (i.e. == 0)
-    Trace("limit") << "SatTimer::set(" << d_ms << ")" << std::endl;
-    gettimeofday(&d_limit, NULL);
-    Trace("limit") << "SatTimer::set(): it's " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
-    d_limit.tv_sec += millis / 1000;
-    d_limit.tv_usec += (millis % 1000) * 1000;
-    if(d_limit.tv_usec > 1000000) {
-      ++d_limit.tv_sec;
-      d_limit.tv_usec -= 1000000;
-    }
-    Trace("limit") << "SatTimer::set(): limit is at " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
-  }
-
-  /** Return the milliseconds elapsed since last set(). */
-  unsigned long elapsed() {
-    timeval tv;
-    gettimeofday(&tv, NULL);
-    Trace("limit") << "SatTimer::elapsed(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl;
-    tv.tv_sec -= d_limit.tv_sec - d_ms / 1000;
-    tv.tv_usec -= d_limit.tv_usec - (d_ms % 1000) * 1000;
-    Trace("limit") << "SatTimer::elapsed(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
-    return tv.tv_sec * 1000 + tv.tv_usec / 1000;
-  }
-
-  bool expired() {
-    if(on()) {
-      timeval tv;
-      gettimeofday(&tv, NULL);
-      Trace("limit") << "SatTimer::expired(): current time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
-      Trace("limit") << "SatTimer::expired(): limit time is " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
-      if(d_limit.tv_sec < tv.tv_sec ||
-         (d_limit.tv_sec == tv.tv_sec && d_limit.tv_usec <= tv.tv_usec)) {
-        Trace("limit") << "SatTimer::expired(): OVER LIMIT!" << std::endl;
-        return true;
-      } else {
-        Trace("limit") << "SatTimer::expired(): within limit" << std::endl;
-      }
-    }
-    return false;
-  }
-
-  /** Check the current time and signal the PropEngine if over-time. */
-  void check();
-
-};/* class SatTimer */
-
-/**
  * PropEngine is the abstraction of a Sat Solver, providing methods for
  * solving the SAT problem and conversion to CNF (via the CnfStream).
  */
@@ -152,11 +82,10 @@ class PropEngine {
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
 
-  /** A timer for SAT calls */
-  SatTimer d_satTimer;
-
   /** Whether we were just interrupted (or not) */
   bool d_interrupted;
+  /** Pointer to resource manager for associated SmtEngine */
+  ResourceManager* d_resourceManager;
 
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
@@ -236,12 +165,8 @@ public:
   /**
    * Checks the current context for satisfiability.
    *
-   * @param millis the time limit for this call in milliseconds
-   * (0==off); on output, it is set to the milliseconds used
-   * @param on input, resource the number of resource units permitted
-   * for this call (0==off); on output, it is set to the resource used
    */
-  Result checkSat(unsigned long& millis, unsigned long& resource);
+  Result checkSat();
 
   /**
    * Get the value of a boolean variable.
@@ -295,21 +220,15 @@ public:
   bool isRunning() const;
 
   /**
-   * Check the current time budget.
-   */
-  void checkTime();
-
-  /**
    * Interrupt a running solver (cause a timeout).
    */
   void interrupt() throw(ModalException);
 
   /**
-   * "Spend" a "resource."  If the sum of these externally-counted
-   * resources and SAT-internal resources exceed the current limit,
-   * SAT should terminate.
+   * Informs the ResourceManager that a resource has been spent.  If out of
+   * resources, can throw an UnsafeInterruptException exception.
    */
-  void spendResource() throw();
+  void spendResource() throw (UnsafeInterruptException);
 
   /**
    * For debugging.  Return true if "expl" is a well-formed
@@ -326,17 +245,6 @@ public:
 };/* class PropEngine */
 
 
-inline void SatTimer::check() {
-  if(d_propEngine.isRunning() && expired()) {
-    Trace("limit") << "SatTimer::check(): interrupt!" << std::endl;
-    d_propEngine.interrupt();
-  }
-}
-
-inline void PropEngine::checkTime() {
-  d_satTimer.check();
-}
-
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index adf6dfd07..b71844590 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -62,12 +62,6 @@ public:
   /** Check the satisfiability of the added clauses */
   virtual SatValue solve(long unsigned int&) = 0;
 
-  /**
-   * Instruct the solver that it should bump its consumed resource count.
-   * Returns true if resources are exhausted.
-   */
-  virtual bool spendResource() = 0;
-
   /** Interrupt the solver */
   virtual void interrupt() = 0;
 
@@ -102,6 +96,7 @@ public:
      * Notify about a learnt clause.
      */
     virtual void notify(SatClause& clause) = 0;
+    virtual void spendResource() = 0;
     virtual void safePoint() = 0;
     
   };/* class BVSatSolverInterface::Notify */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 2bcd48099..59e87dd33 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -103,7 +103,7 @@ TNode TheoryProxy::getNode(SatLiteral lit) {
 }
 
 void TheoryProxy::notifyRestart() {
-  d_propEngine->checkTime();
+  d_propEngine->spendResource();
   d_theoryEngine->notifyRestart();
 
   static uint32_t lemmaCount = 0;
@@ -179,8 +179,8 @@ void TheoryProxy::logDecision(SatLiteral lit) {
 #endif /* CVC4_REPLAY */
 }
 
-void TheoryProxy::checkTime() {
-  d_propEngine->checkTime();
+void TheoryProxy::spendResource() {
+  d_theoryEngine->spendResource();
 }
 
 bool TheoryProxy::isDecisionRelevant(SatVariable var) {
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index a962f653a..3565aa501 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -111,7 +111,7 @@ public:
 
   void logDecision(SatLiteral lit);
 
-  void checkTime();
+  void spendResource();
 
   bool isDecisionEngineDone();
 
diff --git a/src/smt/options b/src/smt/options
index 0dc416474..20dd5b7d5 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -87,14 +87,18 @@ option - regular-output-channel argument :handler CVC4::smt::setRegularOutputCha
 option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h"
  set the diagnostic output channel of the solver
 
-common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long"
+common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler CVC4::smt::tlimitHandler :handler-include "smt/options_handlers.h"
  enable time limiting (give milliseconds)
-common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long"
+common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long" :handler CVC4::smt::tlimitPerHandler :handler-include "smt/options_handlers.h"
  enable time limiting per query (give milliseconds)
-common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
+common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler CVC4::smt::rlimitHandler :handler-include "smt/options_handlers.h"
  enable resource limiting (currently, roughly the number of SAT conflicts)
-common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long"
+common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler CVC4::smt::rlimitPerHandler :handler-include "smt/options_handlers.h"
  enable resource limiting per query
+common-option hardLimit hard-limit --hard-limit bool :default false
+ the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)
+common-option cpuTime cpu-time --cpu-time bool :default false
+ measures CPU time if set to true and wall time if false (default false)
 
 expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
  eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index d02b88fd2..fc2b796d3 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -21,6 +21,7 @@
 
 #include "cvc4autoconfig.h"
 #include "util/dump.h"
+#include "util/resource_manager.h"
 #include "smt/modal_exception.h"
 #include "smt/smt_engine.h"
 #include "lib/strtok_r.h"
@@ -452,6 +453,63 @@ inline void statsEnabledBuild(std::string option, bool value, SmtEngine* smt) th
 #endif /* CVC4_STATISTICS_ON */
 }
 
+inline unsigned long tlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  unsigned long ms;
+  std::istringstream convert(optarg);
+  if (!(convert >> ms))
+    throw OptionException("option `"+option+"` requires a number as an argument");
+
+  // make sure the resource is set if the option is updated
+  // if the smt engine is null the resource will be set in the
+  if (smt != NULL) {
+    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
+    rm->setTimeLimit(ms, true);
+  }
+  return ms;
+}
+
+inline unsigned long tlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  unsigned long ms;
+
+  std::istringstream convert(optarg);
+  if (!(convert >> ms))
+    throw OptionException("option `"+option+"` requires a number as an argument");
+
+  if (smt != NULL) {
+    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
+    rm->setTimeLimit(ms, false);
+  }
+  return ms;
+}
+
+inline unsigned long rlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  unsigned long ms;
+
+  std::istringstream convert(optarg);
+  if (!(convert >> ms))
+    throw OptionException("option `"+option+"` requires a number as an argument");
+
+  if (smt != NULL) {
+    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
+    rm->setResourceLimit(ms, true);
+  }
+  return ms;
+}
+
+inline unsigned long rlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  unsigned long ms;
+
+  std::istringstream convert(optarg);
+  if (!(convert >> ms))
+    throw OptionException("option `"+option+"` requires a number as an argument");
+
+  if (smt != NULL) {
+    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
+    rm->setResourceLimit(ms, false);
+  }
+  return ms;
+}
+
 }/* CVC4::smt namespace */
 }/* CVC4 namespace */
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8bf093370..c87753d8d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -51,6 +51,7 @@
 #include "main/options.h"
 #include "util/unsat_core.h"
 #include "util/proof.h"
+#include "util/resource_manager.h"
 #include "proof/proof.h"
 #include "proof/proof_manager.h"
 #include "util/boolean_simplification.h"
@@ -297,6 +298,10 @@ struct SmtEngineStatistics {
  */
 class SmtEnginePrivate : public NodeManagerListener {
   SmtEngine& d_smt;
+  /**
+   * Manager for limiting time and abstract resource usage.
+   */
+  ResourceManager* d_resourceManager;
 
   /** Learned literals */
   vector<Node> d_nonClausalLearnedLiterals;
@@ -435,12 +440,13 @@ private:
    *
    * Returns false if the formula simplifies to "false"
    */
-  bool simplifyAssertions() throw(TypeCheckingException, LogicException);
+  bool simplifyAssertions() throw(TypeCheckingException, LogicException, UnsafeInterruptException);
 
 public:
 
   SmtEnginePrivate(SmtEngine& smt) :
     d_smt(smt),
+    d_resourceManager(NULL),
     d_nonClausalLearnedLiterals(),
     d_realAssertionsEnd(0),
     d_booleanTermConverter(NULL),
@@ -460,6 +466,7 @@ public:
   {
     d_smt.d_nodeManager->subscribeEvents(this);
     d_true = NodeManager::currentNM()->mkConst(true);
+    d_resourceManager = NodeManager::currentResourceManager();
   }
 
   ~SmtEnginePrivate() {
@@ -474,6 +481,11 @@ public:
     d_smt.d_nodeManager->unsubscribeEvents(this);
   }
 
+  ResourceManager* getResourceManager() { return d_resourceManager; }
+  void spendResource() throw(UnsafeInterruptException) {
+    d_resourceManager->spendResource();
+  }
+
   void nmNotifyNewSort(TypeNode tn, uint32_t flags) {
     DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
                          0,
@@ -562,7 +574,7 @@ public:
    * Expand definitions in n.
    */
   Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly = false)
-    throw(TypeCheckingException, LogicException);
+    throw(TypeCheckingException, LogicException, UnsafeInterruptException);
 
   /**
    * Rewrite Boolean terms in a Node.
@@ -685,12 +697,6 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_queryMade(false),
   d_needPostsolve(false),
   d_earlyTheoryPP(true),
-  d_timeBudgetCumulative(0),
-  d_timeBudgetPerCall(0),
-  d_resourceBudgetCumulative(0),
-  d_resourceBudgetPerCall(0),
-  d_cumulativeTimeUsed(0),
-  d_cumulativeResourceUsed(0),
   d_status(),
   d_private(NULL),
   d_smtAttributes(NULL),
@@ -764,19 +770,6 @@ void SmtEngine::finishInit() {
   }
   d_dumpCommands.clear();
 
-  if(options::perCallResourceLimit() != 0) {
-    setResourceLimit(options::perCallResourceLimit(), false);
-  }
-  if(options::cumulativeResourceLimit() != 0) {
-    setResourceLimit(options::cumulativeResourceLimit(), true);
-  }
-  if(options::perCallMillisecondLimit() != 0) {
-    setTimeLimit(options::perCallMillisecondLimit(), false);
-  }
-  if(options::cumulativeMillisecondLimit() != 0) {
-    setTimeLimit(options::cumulativeMillisecondLimit(), true);
-  }
-
   PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); );
 }
 
@@ -1058,7 +1051,7 @@ void SmtEngine::setDefaults() {
   }
 
   // If in arrays, set the UF handler to arrays
-  if(d_logic.isTheoryEnabled(THEORY_ARRAY) && ( !d_logic.isQuantified() || 
+  if(d_logic.isTheoryEnabled(THEORY_ARRAY) && ( !d_logic.isQuantified() ||
      (d_logic.isQuantified() && !d_logic.isTheoryEnabled(THEORY_UF)))) {
     Theory::setUninterpretedSortOwner(THEORY_ARRAY);
   } else {
@@ -1639,7 +1632,7 @@ void SmtEngine::defineFunction(Expr func,
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
-  throw(TypeCheckingException, LogicException) {
+  throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
 
   stack< triple<Node, Node, bool> > worklist;
   stack<Node> result;
@@ -1649,6 +1642,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
   // or upward pass).
 
   do {
+    spendResource();
     n = worklist.top().first;                      // n is the input / original
     Node node = worklist.top().second;             // node is the output / result
     bool childrenPushed = worklist.top().third;
@@ -1785,7 +1779,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 
 void SmtEnginePrivate::removeITEs() {
   d_smt.finalOptionsAreSet();
-
+  spendResource();
   Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
 
   // Remove all of the ITE occurrences and normalize
@@ -1797,6 +1791,7 @@ void SmtEnginePrivate::removeITEs() {
 
 void SmtEnginePrivate::staticLearning() {
   d_smt.finalOptionsAreSet();
+  spendResource();
 
   TimerStat::CodeTimer staticLearningTimer(d_smt.d_stats->d_staticLearningTime);
 
@@ -1829,6 +1824,7 @@ static void dumpAssertions(const char* key, const AssertionPipeline& assertionLi
 
 // returns false if it learns a conflict
 bool SmtEnginePrivate::nonClausalSimplify() {
+  spendResource();
   d_smt.finalOptionsAreSet();
 
   if(options::unsatCores()) {
@@ -2157,6 +2153,7 @@ void SmtEnginePrivate::bvAbstraction() {
 
 void SmtEnginePrivate::bvToBool() {
   Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
+  spendResource();
   std::vector<Node> new_assertions;
   d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions);
   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
@@ -2167,10 +2164,13 @@ void SmtEnginePrivate::bvToBool() {
 bool SmtEnginePrivate::simpITE() {
   TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
 
+  spendResource();
+
   Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
 
   unsigned numAssertionOnEntry = d_assertions.size();
   for (unsigned i = 0; i < d_assertions.size(); ++i) {
+    spendResource();
     Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]);
     d_assertions.replace(i, result);
     if(result.isConst() && !result.getConst<bool>()){
@@ -2217,6 +2217,7 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
 
 void SmtEnginePrivate::unconstrainedSimp() {
   TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
+  spendResource();
   Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
   d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
 }
@@ -2664,7 +2665,8 @@ void SmtEnginePrivate::doMiplibTrick() {
 
 // returns false if simplification led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
-  throw(TypeCheckingException, LogicException) {
+  throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
+  spendResource();
   Assert(d_smt.d_pendingPops == 0);
   try {
     ScopeCounter depth(d_simplifyAssertionsDepth);
@@ -2791,6 +2793,18 @@ Result SmtEngine::check() {
 
   Trace("smt") << "SmtEngine::check()" << endl;
 
+  ResourceManager* resourceManager = d_private->getResourceManager();
+
+  resourceManager->beginCall();
+
+  // Only way we can be out of resource is if cumulative budget is on
+  if (resourceManager->cumulativeLimitOn() &&
+      resourceManager->out()) {
+    Result::UnknownExplanation why = resourceManager->outOfResources() ?
+                             Result::RESOURCEOUT : Result::TIMEOUT;
+    return Result(Result::VALIDITY_UNKNOWN, why, d_filename);
+  }
+
   // Make sure the prop layer has all of the assertions
   Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
   d_private->processAssertions();
@@ -2810,41 +2824,16 @@ Result SmtEngine::check() {
     }
   }
 
-  unsigned long millis = 0;
-  if(d_timeBudgetCumulative != 0) {
-    millis = getTimeRemaining();
-    if(millis == 0) {
-      return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT, d_filename);
-    }
-  }
-  if(d_timeBudgetPerCall != 0 && (millis == 0 || d_timeBudgetPerCall < millis)) {
-    millis = d_timeBudgetPerCall;
-  }
-
-  unsigned long resource = 0;
-  if(d_resourceBudgetCumulative != 0) {
-    resource = getResourceRemaining();
-    if(resource == 0) {
-      return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT, d_filename);
-    }
-  }
-  if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) {
-    resource = d_resourceBudgetPerCall;
-  }
-
   TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
 
   Chat() << "solving..." << endl;
   Trace("smt") << "SmtEngine::check(): running check" << endl;
-  Result result = d_propEngine->checkSat(millis, resource);
+  Result result = d_propEngine->checkSat();
 
-  // PropEngine::checkSat() returns the actual amount used in these
-  // variables.
-  d_cumulativeTimeUsed += millis;
-  d_cumulativeResourceUsed += resource;
+  resourceManager->endCall();
+  Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager->getTimeUsage()
+                 << ", resources " << resourceManager->getResourceUsage() << endl;
 
-  Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
-                 << ", conflicts " << d_cumulativeResourceUsed << endl;
 
   return Result(result, d_filename);
 }
@@ -2917,6 +2906,9 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node,
 
 Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
   TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
+
+  spendResource();
+
   if(d_booleanTermConverter == NULL) {
     // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
     // to ExprManager notifications, etc.  Otherwise we might miss the "BooleanTerm" datatype
@@ -2950,7 +2942,7 @@ Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
 
 void SmtEnginePrivate::processAssertions() {
   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
-
+  spendResource();
   Assert(d_smt.d_fullyInited);
   Assert(d_smt.d_pendingPops == 0);
 
@@ -3069,6 +3061,7 @@ void SmtEnginePrivate::processAssertions() {
                         << "applying substitutions" << endl;
       for (unsigned i = 0; i < d_assertions.size(); ++ i) {
         Trace("simplify") << "applying to " << d_assertions[i] << endl;
+         spendResource();
         d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
         Trace("simplify") << "  got " << d_assertions[i] << endl;
       }
@@ -3085,6 +3078,7 @@ void SmtEnginePrivate::processAssertions() {
     Chat() << "...doing bvToBool..." << endl;
     bvToBool();
     dumpAssertions("post-bv-to-bool", d_assertions);
+    Trace("smt") << "POST bvToBool" << endl;
   }
 
   if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
@@ -3189,7 +3183,6 @@ void SmtEnginePrivate::processAssertions() {
   }
   dumpAssertions("post-static-learning", d_assertions);
 
-  Trace("smt") << "POST bvToBool" << endl;
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
 
@@ -3332,14 +3325,14 @@ void SmtEnginePrivate::processAssertions() {
   // introducing new ones
 
   dumpAssertions("post-everything", d_assertions);
-  
+
   //set instantiation level of everything to zero
   if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
     for( unsigned i=0; i < d_assertions.size(); i++ ) {
       theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertions[i], 0 );
     }
   }
-  
+
   // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
@@ -3384,86 +3377,93 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
 }
 
 Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
-  Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
-  SmtScope smts(this);
-  finalOptionsAreSet();
-  doPendingPops();
+  try {
+    Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
+    SmtScope smts(this);
+    finalOptionsAreSet();
+    doPendingPops();
 
-  Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl;
+    Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl;
 
-  if(d_queryMade && !options::incrementalSolving()) {
-    throw ModalException("Cannot make multiple queries unless "
-                         "incremental solving is enabled "
-                         "(try --incremental)");
-  }
+    if(d_queryMade && !options::incrementalSolving()) {
+      throw ModalException("Cannot make multiple queries unless "
+                           "incremental solving is enabled "
+                           "(try --incremental)");
+    }
 
-  Expr e;
-  if(!ex.isNull()) {
-    // Substitute out any abstract values in ex.
-    e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
-    // Ensure expr is type-checked at this point.
-    ensureBoolean(e);
-    // Give it to proof manager
-    PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); );
-  }
+    Expr e;
+    if(!ex.isNull()) {
+      // Substitute out any abstract values in ex.
+      e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
+      // Ensure expr is type-checked at this point.
+      ensureBoolean(e);
+      // Give it to proof manager
+      PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); );
+    }
 
-  // check to see if a postsolve() is pending
-  if(d_needPostsolve) {
-    d_theoryEngine->postsolve();
-    d_needPostsolve = false;
-  }
+    // check to see if a postsolve() is pending
+    if(d_needPostsolve) {
+      d_theoryEngine->postsolve();
+      d_needPostsolve = false;
+    }
 
-  // Push the context
-  internalPush();
+    // Push the context
+    internalPush();
 
-  // Note that a query has been made
-  d_queryMade = true;
+    // Note that a query has been made
+    d_queryMade = true;
 
-  // Add the formula
-  if(!e.isNull()) {
-    d_problemExtended = true;
-    if(d_assertionList != NULL) {
-      d_assertionList->push_back(e);
+    // Add the formula
+    if(!e.isNull()) {
+      d_problemExtended = true;
+      if(d_assertionList != NULL) {
+        d_assertionList->push_back(e);
+      }
+      d_private->addFormula(e.getNode());
     }
-    d_private->addFormula(e.getNode());
-  }
 
-  // Run the check
-  Result r = check().asSatisfiabilityResult();
-  d_needPostsolve = true;
+    Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+    r = check().asSatisfiabilityResult();
+    d_needPostsolve = true;
 
-  // Dump the query if requested
-  if(Dump.isOn("benchmark")) {
-    // the expr already got dumped out if assertion-dumping is on
-    Dump("benchmark") << CheckSatCommand();
-  }
+    // Dump the query if requested
+    if(Dump.isOn("benchmark")) {
+      // the expr already got dumped out if assertion-dumping is on
+      Dump("benchmark") << CheckSatCommand();
+    }
 
-  // Pop the context
-  internalPop();
+    // Pop the context
+    internalPop();
 
-  // Remember the status
-  d_status = r;
+    // Remember the status
+    d_status = r;
 
-  d_problemExtended = false;
+    d_problemExtended = false;
 
-  Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
+    Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
 
-  // Check that SAT results generate a model correctly.
-  if(options::checkModels()) {
-    if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
-       (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
-      checkModel(/* hard failure iff */ ! r.isUnknown());
+    // Check that SAT results generate a model correctly.
+    if(options::checkModels()) {
+      if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
+         (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
+        checkModel(/* hard failure iff */ ! r.isUnknown());
+      }
     }
-  }
-  // Check that UNSAT results generate a proof correctly.
-  if(options::checkProofs()) {
-    if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
-      TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
-      checkProof();
+    // Check that UNSAT results generate a proof correctly.
+    if(options::checkProofs()) {
+      if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+        TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
+        checkProof();
+      }
     }
-  }
 
-  return r;
+    return r;
+  } catch (UnsafeInterruptException& e) {
+    AlwaysAssert(d_private->getResourceManager()->out());
+    Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ?
+      Result::RESOURCEOUT : Result::TIMEOUT;
+    return Result(Result::SAT_UNKNOWN, why, d_filename);
+  }
 }/* SmtEngine::checkSat() */
 
 Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
@@ -3474,6 +3474,7 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce
   doPendingPops();
   Trace("smt") << "SMT query(" << ex << ")" << endl;
 
+  try {
   if(d_queryMade && !options::incrementalSolving()) {
     throw ModalException("Cannot make multiple queries unless "
                          "incremental solving is enabled "
@@ -3507,7 +3508,8 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce
   d_private->addFormula(e.getNode().notNode());
 
   // Run the check
-  Result r = check().asValidityResult();
+  Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+  r = check().asValidityResult();
   d_needPostsolve = true;
 
   // Dump the query if requested
@@ -3542,9 +3544,15 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce
   }
 
   return r;
+  } catch (UnsafeInterruptException& e) {
+    AlwaysAssert(d_private->getResourceManager()->out());
+    Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ?
+      Result::RESOURCEOUT : Result::TIMEOUT;
+    return Result(Result::VALIDITY_UNKNOWN, why, d_filename);
+  }
 }/* SmtEngine::query() */
 
-Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException) {
+Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -3575,7 +3583,7 @@ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
   return realValue;
 }
 
-Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) {
+Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -3598,7 +3606,9 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep
   return n.toExpr();
 }
 
-Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException) {
+Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
+  d_private->spendResource();
+
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -3621,7 +3631,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
   return n.toExpr();
 }
 
-Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException) {
+Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
 
@@ -3727,7 +3737,7 @@ bool SmtEngine::addToAssignment(const Expr& ex) throw() {
   return true;
 }
 
-CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
+CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptException) {
   Trace("smt") << "SMT getAssignment()" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -3826,7 +3836,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool
   }
 }
 
-Model* SmtEngine::getModel() throw(ModalException) {
+Model* SmtEngine::getModel() throw(ModalException, UnsafeInterruptException) {
   Trace("smt") << "SMT getModel()" << endl;
   SmtScope smts(this);
 
@@ -4034,7 +4044,7 @@ void SmtEngine::checkModel(bool hardFailure) {
   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
 }
 
-UnsatCore SmtEngine::getUnsatCore() throw(ModalException) {
+UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptException) {
   Trace("smt") << "SMT getUnsatCore()" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -4058,7 +4068,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException) {
 #endif /* CVC4_PROOF */
 }
 
-Proof* SmtEngine::getProof() throw(ModalException) {
+Proof* SmtEngine::getProof() throw(ModalException, UnsafeInterruptException) {
   Trace("smt") << "SMT getProof()" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -4111,7 +4121,7 @@ vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
   return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
 }
 
-void SmtEngine::push() throw(ModalException, LogicException) {
+void SmtEngine::push() throw(ModalException, LogicException, UnsafeInterruptException) {
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
@@ -4141,7 +4151,7 @@ void SmtEngine::push() throw(ModalException, LogicException) {
                        << d_userContext->getLevel() << endl;
 }
 
-void SmtEngine::pop() throw(ModalException) {
+void SmtEngine::pop() throw(ModalException, UnsafeInterruptException) {
   SmtScope smts(this);
   finalOptionsAreSet();
   Trace("smt") << "SMT pop()" << endl;
@@ -4263,49 +4273,26 @@ void SmtEngine::interrupt() throw(ModalException) {
 }
 
 void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
-  if(cumulative) {
-    Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << endl;
-    d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
-  } else {
-    Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << endl;
-    d_resourceBudgetPerCall = units;
-  }
+  d_private->getResourceManager()->setResourceLimit(units, cumulative);
 }
-
-void SmtEngine::setTimeLimit(unsigned long millis, bool cumulative) {
-  if(cumulative) {
-    Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << endl;
-    d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis);
-  } else {
-    Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << endl;
-    d_timeBudgetPerCall = millis;
-  }
+void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) {
+  d_private->getResourceManager()->setTimeLimit(milis, cumulative);
 }
 
 unsigned long SmtEngine::getResourceUsage() const {
-  return d_cumulativeResourceUsed;
+  return d_private->getResourceManager()->getResourceUsage();
 }
 
 unsigned long SmtEngine::getTimeUsage() const {
-  return d_cumulativeTimeUsed;
+  return d_private->getResourceManager()->getTimeUsage();
 }
 
 unsigned long SmtEngine::getResourceRemaining() const throw(ModalException) {
-  if(d_resourceBudgetCumulative == 0) {
-    throw ModalException("No cumulative resource limit is currently set");
-  }
-
-  return d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 :
-    d_resourceBudgetCumulative - d_cumulativeResourceUsed;
+  return d_private->getResourceManager()->getResourceRemaining();
 }
 
 unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) {
-  if(d_timeBudgetCumulative == 0) {
-    throw ModalException("No cumulative time limit is currently set");
-  }
-
-  return d_timeBudgetCumulative <= d_cumulativeTimeUsed ? 0 :
-    d_timeBudgetCumulative - d_cumulativeTimeUsed;
+  return d_private->getResourceManager()->getTimeRemaining();
 }
 
 Statistics SmtEngine::getStatistics() const throw() {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 489d34d79..a39d2a7b5 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -35,6 +35,7 @@
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/hash.h"
+#include "util/unsafe_interrupt_exception.h"
 #include "util/statistics.h"
 #include "theory/logic_info.h"
 
@@ -233,19 +234,6 @@ class CVC4_PUBLIC SmtEngine {
    */
   bool d_earlyTheoryPP;
 
-  /** A user-imposed cumulative time budget, in milliseconds.  0 = no limit. */
-  unsigned long d_timeBudgetCumulative;
-  /** A user-imposed per-call time budget, in milliseconds.  0 = no limit. */
-  unsigned long d_timeBudgetPerCall;
-  /** A user-imposed cumulative resource budget.  0 = no limit. */
-  unsigned long d_resourceBudgetCumulative;
-  /** A user-imposed per-call resource budget.  0 = no limit. */
-  unsigned long d_resourceBudgetPerCall;
-
-  /** The number of milliseconds used by this SmtEngine since its inception. */
-  unsigned long d_cumulativeTimeUsed;
-  /** The amount of resource used by this SmtEngine since its inception. */
-  unsigned long d_cumulativeResourceUsed;
 
   /**
    * Most recent result of last checkSat/query or (set-info :status).
@@ -383,7 +371,7 @@ class CVC4_PUBLIC SmtEngine {
    * or INVALID query).  Only permitted if CVC4 was built with model
    * support and produce-models is on.
    */
-  Model* getModel() throw(ModalException);
+  Model* getModel() throw(ModalException, UnsafeInterruptException);
 
   // disallow copy/assignment
   SmtEngine(const SmtEngine&) CVC4_UNDEFINED;
@@ -463,7 +451,7 @@ public:
    * takes a Boolean flag to determine whether to include this asserted
    * formula in an unsat core (if one is later requested).
    */
-  Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException);
+  Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
 
   /**
    * Check validity of an expression with respect to the current set
@@ -487,20 +475,20 @@ public:
    * @todo (design) is this meant to give an equivalent or an
    * equisatisfiable formula?
    */
-  Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException);
+  Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
 
   /**
    * Expand the definitions in a term or formula.  No other
    * simplification or normalization is done.
    */
-  Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException);
+  Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
 
   /**
    * Get the assigned value of an expr (only if immediately preceded
    * by a SAT or INVALID query).  Only permitted if the SmtEngine is
    * set to operate interactively and produce-models is on.
    */
-  Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException);
+  Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException);
 
   /**
    * Add a function to the set of expressions whose value is to be
@@ -518,14 +506,14 @@ public:
    * INVALID query).  Only permitted if the SmtEngine is set to
    * operate interactively and produce-assignments is on.
    */
-  CVC4::SExpr getAssignment() throw(ModalException);
+  CVC4::SExpr getAssignment() throw(ModalException, UnsafeInterruptException);
 
   /**
    * Get the last proof (only if immediately preceded by an UNSAT
    * or VALID query).  Only permitted if CVC4 was built with proof
    * support and produce-proofs is on.
    */
-  Proof* getProof() throw(ModalException);
+  Proof* getProof() throw(ModalException, UnsafeInterruptException);
 
   /**
    * Print all instantiations made by the quantifiers module.
@@ -537,7 +525,7 @@ public:
    * UNSAT or VALID query).  Only permitted if CVC4 was built with
    * unsat-core support and produce-unsat-cores is on.
    */
-  UnsatCore getUnsatCore() throw(ModalException);
+  UnsatCore getUnsatCore() throw(ModalException, UnsafeInterruptException);
 
   /**
    * Get the current set of assertions.  Only permitted if the
@@ -548,12 +536,12 @@ public:
   /**
    * Push a user-level context.
    */
-  void push() throw(ModalException, LogicException);
+  void push() throw(ModalException, LogicException, UnsafeInterruptException);
 
   /**
    * Pop a user-level context.  Throws an exception if nothing to pop.
    */
-  void pop() throw(ModalException);
+  void pop() throw(ModalException, UnsafeInterruptException);
 
   /**
    * Completely reset the state of the solver, as though destroyed and
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index fb5810fd5..701775c9c 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -38,6 +38,9 @@ inline SmtEngine* currentSmtEngine() {
   Assert(s_smtEngine_current != NULL);
   return s_smtEngine_current;
 }
+inline bool smtEngineInScope() {
+  return s_smtEngine_current != NULL;
+}
 
 inline ProofManager* currentProofManager() {
 #ifdef CVC4_PROOF
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 0ff12da95..e13587323 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -28,6 +28,7 @@
 #include "prop/sat_solver.h"
 #include "theory/valuation.h"
 #include "theory/theory_registrar.h"
+#include "util/resource_manager.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
@@ -134,6 +135,7 @@ class TLazyBitblaster :  public TBitblaster<Node> {
     {}
     bool notify(prop::SatLiteral lit);
     void notify(prop::SatClause& clause);
+    void spendResource();
     void safePoint();
   };
   
@@ -228,7 +230,8 @@ private:
     Statistics(const std::string& name);
     ~Statistics();
   };
-  std::string d_name; 
+  std::string d_name;
+public:
   Statistics d_statistics;
 };
 
@@ -237,6 +240,9 @@ public:
   MinisatEmptyNotify() {}
   bool notify(prop::SatLiteral lit) { return true; }
   void notify(prop::SatClause& clause) { }
+  void spendResource() {
+    NodeManager::currentResourceManager()->spendResource();
+  }
   void safePoint() {}
 };
 
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index f9f8ff581..57a635c20 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -67,6 +67,7 @@ bool EagerBitblastSolver::isInitialized() {
 }
 
 void EagerBitblastSolver::assertFormula(TNode formula) {
+  d_bv->spendResource();
   Assert (isInitialized());
   Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n"; 
   d_assertionSet.insert(formula);
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index e8acf268f..5b139e327 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -557,6 +557,7 @@ bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) {
 void AlgebraicSolver::processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst) {
   bool changed = true;
   while(changed) {
+    // d_bv->spendResource();
     changed = false;
     for (unsigned i = 0; i < worklist.size(); ++i) {
       // apply current substitutions
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index d0b99f869..c86572ead 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -103,8 +103,11 @@ void BitblastSolver::bitblastQueue() {
       // don't bit-blast lemma atoms
       continue;
     }
-    Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n"; 
-    d_bitblaster->bbAtom(atom);
+    Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
+    {
+      TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
+      d_bitblaster->bbAtom(atom);
+    }
   }
 }
 
@@ -149,6 +152,7 @@ bool BitblastSolver::check(Theory::Effort e) {
 
   // We need to ensure we are fully propagated, so propagate now
   if (d_useSatPropagation) {
+    d_bv->spendResource();
     bool ok = d_bitblaster->propagate();
     if (!ok) {
       std::vector<TNode> conflictAtoms;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index d2c79fec2..938a93b85 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -166,6 +166,9 @@ bool CoreSolver::decomposeFact(TNode fact) {
 
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
+
+  d_bv->spendResource();
+
   d_checkCalled = true; 
   Assert (!d_bv->inConflict());
   ++(d_statistics.d_numCallstoCheck);
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 917b10c33..660551fe2 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -29,6 +29,7 @@ using namespace CVC4::theory::bv::utils;
 bool InequalitySolver::check(Theory::Effort e) {
   Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
   ++(d_statistics.d_numCallstoCheck);
+  d_bv->spendResource();
 
   bool ok = true;
   while (!done() && ok) {
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 877baec4e..065d5d5ef 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -103,6 +103,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
+  d_bv->spendResource();
   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
 
   d_termBBStrategies[node.getKind()] (node, bits, this);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index b74506e4d..e5b5ed664 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -170,6 +170,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
+  d_bv->spendResource();
   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numTerms;
 
@@ -355,6 +356,10 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 }
 
+void TLazyBitblaster::MinisatNotify::spendResource() {
+  d_bv->spendResource();
+}
+
 void TLazyBitblaster::MinisatNotify::safePoint() {
   d_bv->d_out->safePoint();
 }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 99bc764dd..eddd5017c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -107,6 +107,10 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   }
 }
 
+void TheoryBV::spendResource() throw(UnsafeInterruptException) {
+  getOutputChannel().spendResource();
+}
+
 TheoryBV::Statistics::Statistics():
   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
   d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
@@ -362,6 +366,7 @@ void TheoryBV::check(Effort e)
     return;
   }
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
   // we may be getting new assertions so the model cache may not be sound
   d_invalidateModelCache.set(true); 
   // if we are using the eager solver
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index a37a4019e..11d8cb895 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -103,6 +103,7 @@ private:
 
   Statistics d_statistics;
 
+  void spendResource() throw(UnsafeInterruptException);
 
   /**
    * Return the uninterpreted function symbol corresponding to division-by-zero
@@ -218,6 +219,7 @@ private:
   friend class CoreSolver;
   friend class InequalitySolver;
   friend class AlgebraicSolver;
+  friend class EagerBitblastSolver;
 };/* class TheoryBV */
 
 }/* CVC4::theory::bv namespace */
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 40eba6ff5..fdf253d3f 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -21,6 +21,7 @@
 
 #include "util/cvc4_assert.h"
 #include "theory/interrupted.h"
+#include "util/resource_manager.h"
 
 namespace CVC4 {
 namespace theory {
@@ -84,7 +85,7 @@ public:
    * With safePoint(), the theory signals that it is at a safe point
    * and can be interrupted.
    */
-  virtual void safePoint() throw(Interrupted, AssertionException) {
+  virtual void safePoint() throw(Interrupted, UnsafeInterruptException, AssertionException) {
   }
 
   /**
@@ -97,7 +98,7 @@ public:
    * unit conflict) which is assigned TRUE (and T-conflicting) in the
    * current assignment.
    */
-  virtual void conflict(TNode n) throw(AssertionException) = 0;
+  virtual void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Propagate a theory literal.
@@ -105,7 +106,7 @@ public:
    * @param n - a theory consequence at the current decision level
    * @return false if an immediate conflict was encountered
    */
-  virtual bool propagate(TNode n) throw(AssertionException) = 0;
+  virtual bool propagate(TNode n) throw(AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Tell the core that a valid theory lemma at decision level 0 has
@@ -119,7 +120,7 @@ public:
    */
   virtual LemmaStatus lemma(TNode n, bool removable = false,
                             bool preprocess = false)
-    throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
+    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Request a split on a new theory atom.  This is equivalent to
@@ -128,12 +129,12 @@ public:
    * @param n - a theory atom; must be of Boolean type
    */
   LemmaStatus split(TNode n)
-    throw(TypeCheckingExceptionPrivate, AssertionException) {
+    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
     return splitLemma(n.orNode(n.notNode()));
   }
 
   virtual LemmaStatus splitLemma(TNode n, bool removable = false)
-    throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
+    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * If a decision is made on n, it must be in the phase specified.
@@ -148,7 +149,7 @@ public:
    * @param phase - the phase to decide on n
    */
   virtual void requirePhase(TNode n, bool phase)
-    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0;
+    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Flips the most recent unflipped decision to the other phase and
@@ -191,14 +192,14 @@ public:
    * could be flipped, or if the root decision was re-flipped
    */
   virtual bool flipDecision()
-    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0;
+    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Notification from a theory that it realizes it is incomplete at
    * this context level.  If SAT is later determined by the
    * TheoryEngine, it should actually return an UNKNOWN result.
    */
-  virtual void setIncomplete() throw(AssertionException) = 0;
+  virtual void setIncomplete() throw(AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * "Spend" a "resource."  The meaning is specific to the context in
@@ -211,7 +212,7 @@ public:
    * long-running operations, they cannot rely on resource() to break
    * out of infinite or intractable computations.
    */
-  virtual void spendResource() throw() {}
+  virtual void spendResource() throw(UnsafeInterruptException) {}
 
   /**
    * Handle user attribute.
@@ -226,7 +227,7 @@ public:
    * Using this leads to non-termination issues.
    * It is appropriate for prototyping for theories.
    */
-  virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {}
+  virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {}
 
 };/* class OutputChannel */
 
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 960602846..a940bcc3d 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -18,12 +18,16 @@
 #include "theory/theory.h"
 #include "theory/rewriter.h"
 #include "theory/rewriter_tables.h"
+#include "smt/smt_engine_scope.h"
+#include "util/resource_manager.h"
 
 using namespace std;
 
 namespace CVC4 {
 namespace theory {
 
+unsigned long Rewriter::d_iterationCount = 0;
+
 static TheoryId theoryOf(TNode node) {
   return Theory::theoryOf(THEORY_OF_TYPE_BASED, node);
 }
@@ -76,7 +80,7 @@ struct RewriteStackElement {
   }
 };
 
-Node Rewriter::rewrite(TNode node) {
+Node Rewriter::rewrite(TNode node) throw (UnsafeInterruptException){
   return rewriteTo(theoryOf(node), node);
 }
 
@@ -102,9 +106,20 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
   vector<RewriteStackElement> rewriteStack;
   rewriteStack.push_back(RewriteStackElement(node, theoryId));
 
+  ResourceManager* rm = NULL;
+  bool hasSmtEngine = smt::smtEngineInScope();
+  if (hasSmtEngine) {
+    rm = NodeManager::currentResourceManager();
+  }
   // Rewrite until the stack is empty
   for (;;){
 
+    if (hasSmtEngine &&
+		d_iterationCount % ResourceManager::getFrequencyCount() == 0) {
+      rm->spendResource();
+      d_iterationCount = 0;
+    }
+
     // Get the top of the recursion stack
     RewriteStackElement& rewriteStackTop = rewriteStack.back();
 
@@ -139,7 +154,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
         rewriteStackTop.theoryId = theoryOf(cached);
       }
     }
-    
+
     rewriteStackTop.original =rewriteStackTop.node;
     // Now it's time to rewrite the children, check if this has already been done
     Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
@@ -233,5 +248,15 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
   return Node::null();
 }/* Rewriter::rewriteTo() */
 
+void Rewriter::clearCaches() {
+#ifdef CVC4_ASSERTIONS
+  if(s_rewriteStack != NULL) {
+    delete s_rewriteStack;
+    s_rewriteStack = NULL;
+  }
+#endif
+  Rewriter::clearCachesInternal();
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index b150b186a..44035e7d9 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -19,6 +19,8 @@
 #pragma once
 
 #include "expr/node.h"
+#include "util/unsafe_interrupt_exception.h"
+
 //#include "expr/attribute.h"
 
 namespace CVC4 {
@@ -56,7 +58,7 @@ class RewriterInitializer;
 class Rewriter {
 
   friend class RewriterInitializer;
-
+  static unsigned long d_iterationCount;
   /** Returns the appropriate cache for a node */
   static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
 
@@ -100,20 +102,19 @@ class Rewriter {
    * Should be called to clean up any state.
    */
   static void shutdown();
-
+  static void clearCachesInternal();
 public:
 
   /**
    * Rewrites the node using theoryOf() to determine which rewriter to
    * use on the node.
    */
-  static Node rewrite(TNode node);
+  static Node rewrite(TNode node) throw (UnsafeInterruptException);
 
   /**
    * Garbage collects the rewrite caches.
    */
-  static void garbageCollect();
-
+  static void clearCaches();
 };/* class Rewriter */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 9b51d2b32..d79f464b5 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -85,7 +85,7 @@ void Rewriter::shutdown() {
 ${rewrite_shutdown}
 }
 
-void Rewriter::garbageCollect() {
+void Rewriter::clearCachesInternal() {
   typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId;
   std::vector<AttributeUniqueId> preids;
   ${pre_rewrite_attribute_ids}
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 12a169e09..d83626a6b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -26,6 +26,7 @@
 #include "expr/node_builder.h"
 #include "options/options.h"
 #include "util/lemma_output_channel.h"
+#include "util/resource_manager.h"
 
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
@@ -142,6 +143,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_true(),
   d_false(),
   d_interrupted(false),
+  d_resourceManager(NodeManager::currentResourceManager()),
   d_inPreregister(false),
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
@@ -334,8 +336,7 @@ void TheoryEngine::dumpAssertions(const char* tag) {
  * @param effort the effort level to use
  */
 void TheoryEngine::check(Theory::Effort effort) {
-
-  d_propEngine->checkTime();
+  // spendResource();
 
   // Reset the interrupt flag
   d_interrupted = false;
@@ -846,6 +847,7 @@ struct preprocess_stack_element {
 Node TheoryEngine::preprocess(TNode assertion) {
 
   Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion << ")" << endl;
+  // spendResource();
 
   // Do a topological sort of the subexpressions and substitute them
   vector<preprocess_stack_element> toVisit;
@@ -1082,7 +1084,7 @@ void TheoryEngine::assertFact(TNode literal)
 {
   Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
 
-  d_propEngine->checkTime();
+  // spendResource();
 
   // If we're in conflict, nothing to do
   if (d_inConflict) {
@@ -1145,7 +1147,7 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
 
   Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
 
-  d_propEngine->checkTime();
+  // spendResource();
 
   if(Dump.isOn("t-propagations")) {
     Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
@@ -1368,7 +1370,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
 
 theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) {
   // For resource-limiting (also does a time check).
-  spendResource();
+  // spendResource();
 
   // Do we need to check atoms
   if (atomsTo != theory::THEORY_LAST) {
@@ -1553,7 +1555,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
         Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl;
         Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
         d_iteUtilities->clear();
-        Rewriter::garbageCollect();
+        Rewriter::clearCaches();
         d_iteRemover.garbageCollect();
         nm->reclaimZombiesUntil(options::zombieHuntThreshold());
         Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
@@ -1742,3 +1744,7 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T
 
   return th->entailmentCheck(lit, params, seffects);
 }
+
+void TheoryEngine::spendResource() {
+  d_resourceManager->spendResource();
+}
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 136c0409f..6360ea5fb 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -39,6 +39,7 @@
 #include "util/statistics_registry.h"
 #include "util/cvc4_assert.h"
 #include "util/sort_inference.h"
+#include "util/unsafe_interrupt_exception.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/bv/bv_to_bool.h"
@@ -46,6 +47,8 @@
 
 namespace CVC4 {
 
+class ResourceManager;
+  
 /**
  * A pair of a theory and a node. This is used to mark the flow of
  * propagations between theories.
@@ -279,42 +282,42 @@ class TheoryEngine {
     {
     }
 
-    void safePoint() throw(theory::Interrupted, AssertionException) {
+      void safePoint() throw(theory::Interrupted, UnsafeInterruptException, AssertionException) {
       spendResource();
       if (d_engine->d_interrupted) {
         throw theory::Interrupted();
       }
     }
 
-    void conflict(TNode conflictNode) throw(AssertionException) {
+    void conflict(TNode conflictNode) throw(AssertionException, UnsafeInterruptException) {
       Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
       ++ d_statistics.conflicts;
       d_engine->d_outputChannelUsed = true;
       d_engine->conflict(conflictNode, d_theory);
     }
 
-    bool propagate(TNode literal) throw(AssertionException) {
+    bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) {
       Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
       ++ d_statistics.propagations;
       d_engine->d_outputChannelUsed = true;
       return d_engine->propagate(literal, d_theory);
     }
 
-    theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
+    theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
       return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST);
     }
 
-    theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
+    theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
       return d_engine->lemma(lemma, false, removable, false, d_theory);
     }
 
-    void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {
+    void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
       NodeManager* curr = NodeManager::currentNM();
       Node restartVar =  curr->mkSkolem("restartVar",
                                         curr->booleanType(),
@@ -325,7 +328,7 @@ class TheoryEngine {
     }
 
     void requirePhase(TNode n, bool phase)
-      throw(theory::Interrupted, AssertionException) {
+      throw(theory::Interrupted, AssertionException, UnsafeInterruptException) {
       Debug("theory") << "EngineOutputChannel::requirePhase("
                       << n << ", " << phase << ")" << std::endl;
       ++ d_statistics.requirePhase;
@@ -333,18 +336,18 @@ class TheoryEngine {
     }
 
     bool flipDecision()
-      throw(theory::Interrupted, AssertionException) {
+      throw(theory::Interrupted, AssertionException, UnsafeInterruptException) {
       Debug("theory") << "EngineOutputChannel::flipDecision()" << std::endl;
       ++ d_statistics.flipDecision;
       return d_engine->d_propEngine->flipDecision();
     }
 
-    void setIncomplete() throw(AssertionException) {
+    void setIncomplete() throw(AssertionException, UnsafeInterruptException) {
       Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl;
       d_engine->setIncomplete(d_theory);
     }
 
-    void spendResource() throw() {
+    void spendResource() throw(UnsafeInterruptException) {
       d_engine->spendResource();
     }
 
@@ -387,12 +390,6 @@ class TheoryEngine {
     d_incomplete = true;
   }
 
-  /**
-   * "Spend" a resource during a search or preprocessing.
-   */
-  void spendResource() throw() {
-    d_propEngine->spendResource();
-  }
 
   /**
    * Mapping of propagations from recievers to senders.
@@ -477,6 +474,7 @@ class TheoryEngine {
 
   /** Whether we were just interrupted (or not) */
   bool d_interrupted;
+  ResourceManager* d_resourceManager;
 
 public:
 
@@ -487,6 +485,10 @@ public:
   ~TheoryEngine();
 
   void interrupt() throw(ModalException);
+  /**
+   * "Spend" a resource during a search or preprocessing.
+   */
+  void spendResource();
 
   /**
    * Adds a theory. Only one theory per TheoryId can be present, so if
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 6d1275c20..46a717cc5 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -23,13 +23,13 @@
 #include "expr/node.h"
 #include "theory/output_channel.h"
 #include "theory/interrupted.h"
+#include "util/unsafe_interrupt_exception.h"
 
 #include <vector>
 #include <utility>
 #include <iostream>
 
 namespace CVC4 {
-
 namespace theory {
 
 /**
@@ -72,42 +72,44 @@ public:
   void safePoint()  throw(Interrupted, AssertionException) {}
 
   void conflict(TNode n)
-    throw(AssertionException) {
+    throw(AssertionException, UnsafeInterruptException) {
     push(CONFLICT, n);
   }
 
   bool propagate(TNode n)
-    throw(AssertionException) {
+    throw(AssertionException, UnsafeInterruptException) {
     push(PROPAGATE, n);
     return true;
   }
 
   void propagateAsDecision(TNode n)
-    throw(AssertionException) {
+    throw(AssertionException, UnsafeInterruptException) {
     push(PROPAGATE_AS_DECISION, n);
   }
 
-  LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) {
+  LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException, UnsafeInterruptException) {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
 
-  void requirePhase(TNode, bool) throw(Interrupted, AssertionException) {
+  void requirePhase(TNode, bool) throw(Interrupted, AssertionException, UnsafeInterruptException) {
   }
 
-  bool flipDecision() throw(Interrupted, AssertionException) {
+  bool flipDecision() throw(Interrupted, AssertionException, UnsafeInterruptException) {
     return true;
   }
 
-  void setIncomplete() throw(AssertionException) {}
+  void setIncomplete() throw(AssertionException, UnsafeInterruptException) {
+  }
 
-  void handleUserAttribute( const char* attr, theory::Theory* t ){}
+  void handleUserAttribute( const char* attr, theory::Theory* t ) {
+  }
 
   void clear() {
     d_callHistory.clear();
   }
 
-  LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException){
+  LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
@@ -125,7 +127,7 @@ public:
     return d_callHistory.size();
   }
 
-  void printIth(std::ostream& os, int i){
+  void printIth(std::ostream& os, int i) {
     os << "[TestOutputChannel " << i;
     os << " " << getIthCallType(i);
     os << " " << getIthNode(i) << "]";
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index fc9192dd9..a6543391d 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -99,7 +99,10 @@ libutil_la_SOURCES = \
 	didyoumean.h \
 	didyoumean.cpp \
 	unsat_core.h \
-	unsat_core.cpp
+	unsat_core.cpp \
+	resource_manager.h \
+	resource_manager.cpp \
+	unsafe_interrupt_exception.h
 
 libstatistics_la_SOURCES = \
 	statistics_registry.h \
@@ -158,6 +161,7 @@ EXTRA_DIST = \
 	uninterpreted_constant.i \
 	chain.i \
 	regexp.i \
+	resource_manager.i \
 	proof.i \
 	unsat_core.i
 
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
new file mode 100644
index 000000000..2aca55616
--- /dev/null
+++ b/src/util/resource_manager.cpp
@@ -0,0 +1,285 @@
+/*********************                                                        */
+/*! \file resource_manager.h
+** \verbatim
+** Original author: Liana Hadarean
+** Major contributors: none
+** Minor contributors (to current version): none
+** This file is part of the CVC4 project.
+** Copyright (c) 2009-2014  New York University and The University of Iowa
+** See the file COPYING in the top-level source directory for licensing
+** information.\endverbatim
+**
+** \brief Manages and updates various resource and time limits.
+**
+** Manages and updates various resource and time limits.
+**/
+
+#include "util/resource_manager.h"
+#include "util/output.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/options.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4;
+using namespace std;
+
+void Timer::set(unsigned long millis, bool wallTime) {
+  d_ms = millis;
+  Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl;
+  // keep track of when it was set, even if it's disabled (i.e. == 0)
+  d_wall_time = wallTime;
+  if (d_wall_time) {
+    // Wall time
+    gettimeofday(&d_wall_limit, NULL);
+    Trace("limit") << "Timer::set(): it's " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl;
+    d_wall_limit.tv_sec += millis / 1000;
+    d_wall_limit.tv_usec += (millis % 1000) * 1000;
+    if(d_wall_limit.tv_usec > 1000000) {
+      ++d_wall_limit.tv_sec;
+      d_wall_limit.tv_usec -= 1000000;
+    }
+    Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl;
+  } else {
+    // CPU time
+    d_cpu_start_time = ((double)clock())/(CLOCKS_PER_SEC *0.001);
+    d_cpu_limit = d_cpu_start_time + d_ms;
+  }
+}
+
+/** Return the milliseconds elapsed since last set(). */
+unsigned long Timer::elapsedWall() const {
+  Assert (d_wall_time);
+  timeval tv;
+  gettimeofday(&tv, NULL);
+  Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+  tv.tv_sec -= d_wall_limit.tv_sec - d_ms / 1000;
+  tv.tv_usec -= d_wall_limit.tv_usec - (d_ms % 1000) * 1000;
+  Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+  return tv.tv_sec * 1000 + tv.tv_usec / 1000;
+}
+
+unsigned long Timer::elapsedCPU() const {
+  Assert (!d_wall_time);
+  clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time;
+  Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <<std::endl;
+  return elapsed;
+}
+
+unsigned long Timer::elapsed() const {
+  if (d_wall_time)
+    return elapsedWall();
+  return elapsedCPU();
+}
+
+bool Timer::expired() const {
+  if (!on()) return false;
+
+  if (d_wall_time) {
+    timeval tv;
+    gettimeofday(&tv, NULL);
+    Debug("limit") << "Timer::expired(): current wall time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+    Debug("limit") << "Timer::expired(): limit wall time is " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl;
+    if(d_wall_limit.tv_sec < tv.tv_sec ||
+       (d_wall_limit.tv_sec == tv.tv_sec && d_wall_limit.tv_usec <= tv.tv_usec)) {
+      Debug("limit") << "Timer::expired(): OVER LIMIT!" << std::endl;
+      return true;
+    }
+    Debug("limit") << "Timer::expired(): within limit" << std::endl;
+    return false;
+  }
+
+  // cpu time
+  double current = ((double)clock())/(CLOCKS_PER_SEC*0.001);
+  Debug("limit") << "Timer::expired(): current cpu time is " << current <<  std::endl;
+  Debug("limit") << "Timer::expired(): limit cpu time is " << d_cpu_limit <<  std::endl;
+  if (current >= d_cpu_limit) {
+    Debug("limit") << "Timer::expired(): OVER LIMIT!" << current <<  std::endl;
+    return true;
+  }
+  return false;
+}
+
+const unsigned long ResourceManager::s_resourceCount = 1000;
+
+ResourceManager::ResourceManager()
+  : d_cumulativeTimer()
+  , d_perCallTimer()
+  , d_timeBudgetCumulative(0)
+  , d_timeBudgetPerCall(0)
+  , d_resourceBudgetCumulative(0)
+  , d_resourceBudgetPerCall(0)
+  , d_cumulativeTimeUsed(0)
+  , d_cumulativeResourceUsed(0)
+  , d_thisCallResourceUsed(0)
+  , d_thisCallTimeBudget(0)
+  , d_thisCallResourceBudget(0)
+  , d_isHardLimit()
+  , d_on(false)
+  , d_cpuTime(false)
+  , d_spendResourceCalls(0)
+{}
+
+
+void ResourceManager::setResourceLimit(unsigned long units, bool cumulative) {
+  d_on = true;
+  if(cumulative) {
+    Trace("limit") << "ResourceManager: setting cumulative resource limit to " << units << endl;
+    d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
+    d_thisCallResourceBudget = d_resourceBudgetCumulative;
+  } else {
+    Trace("limit") << "ResourceManager: setting per-call resource limit to " << units << endl;
+    d_resourceBudgetPerCall = units;
+  }
+}
+
+void ResourceManager::setTimeLimit(unsigned long millis, bool cumulative) {
+  d_on = true;
+  if(cumulative) {
+    Trace("limit") << "ResourceManager: setting cumulative time limit to " << millis << " ms" << endl;
+    d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis);
+    d_cumulativeTimer.set(millis, !d_cpuTime);
+  } else {
+    Trace("limit") << "ResourceManager: setting per-call time limit to " << millis << " ms" << endl;
+    d_timeBudgetPerCall = millis;
+    // perCall timer will be set in beginCall
+  }
+
+}
+
+unsigned long ResourceManager::getResourceUsage() const {
+  return d_cumulativeResourceUsed;
+}
+
+unsigned long ResourceManager::getTimeUsage() const {
+  if (d_timeBudgetCumulative) {
+    return d_cumulativeTimer.elapsed();
+  }
+  return d_cumulativeTimeUsed;
+}
+
+unsigned long ResourceManager::getResourceRemaining() const {
+  if (d_thisCallResourceBudget <= d_thisCallResourceUsed)
+    return 0;
+  return d_thisCallResourceBudget - d_thisCallResourceUsed;
+}
+
+unsigned long ResourceManager::getTimeRemaining() const {
+  unsigned long time_passed = d_cumulativeTimer.elapsed();
+  if (time_passed >= d_thisCallTimeBudget)
+    return 0;
+  return d_thisCallTimeBudget - time_passed;
+}
+
+void ResourceManager::spendResource() throw (UnsafeInterruptException) {
+  ++d_spendResourceCalls;
+  if (!d_on) return;
+
+  Debug("limit") << "ResourceManager::spendResource()" << std::endl;
+  ++d_cumulativeResourceUsed;
+  ++d_thisCallResourceUsed;
+  if(out()) {
+    Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
+	Trace("limit") << "                 on call " << d_spendResourceCalls << std::endl;
+    if (outOfTime()) {
+      Trace("limit") << "ResourceManager::spendResource: elapsed time" << d_cumulativeTimer.elapsed() << std::endl;
+    }
+
+    if (smt::smtEngineInScope()) {
+      theory::Rewriter::clearCaches();
+    }
+    if (d_isHardLimit) {
+      throw UnsafeInterruptException();
+    }
+
+    // interrupt it next time resources are checked
+    if (smt::smtEngineInScope()) {
+      smt::currentSmtEngine()->interrupt();
+    }
+  }
+}
+
+void ResourceManager::beginCall() {
+
+  d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime);
+  d_thisCallResourceUsed = 0;
+  if (!d_on) return;
+
+  if (cumulativeLimitOn()) {
+    if (d_resourceBudgetCumulative) {
+      d_thisCallResourceBudget = d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 :
+                                 d_resourceBudgetCumulative - d_cumulativeResourceUsed;
+    }
+
+    if (d_timeBudgetCumulative) {
+
+      AlwaysAssert(d_cumulativeTimer.on());
+      // timer was on since the option was set
+      d_cumulativeTimeUsed = d_cumulativeTimer.elapsed();
+      d_thisCallTimeBudget = d_timeBudgetCumulative <= d_cumulativeTimeUsed? 0 :
+                             d_timeBudgetCumulative - d_cumulativeTimeUsed;
+      d_cumulativeTimer.set(d_thisCallTimeBudget, d_cpuTime);
+    }
+    // we are out of resources so we shouldn't update the
+    // budget for this call to the per call budget
+    if (d_thisCallTimeBudget == 0 ||
+        d_thisCallResourceUsed == 0)
+      return;
+  }
+
+  if (perCallLimitOn()) {
+    // take min of what's left and per-call budget
+    if (d_resourceBudgetPerCall) {
+      d_thisCallResourceBudget = d_thisCallResourceBudget < d_resourceBudgetPerCall && d_thisCallResourceBudget != 0 ? d_thisCallResourceBudget : d_resourceBudgetPerCall;
+    }
+
+    if (d_timeBudgetPerCall) {
+      d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall && d_thisCallTimeBudget != 0 ? d_thisCallTimeBudget : d_timeBudgetPerCall;
+    }
+  }
+}
+
+void ResourceManager::endCall() {
+  unsigned long usedInCall = d_perCallTimer.elapsed();
+  d_perCallTimer.set(0);
+  d_cumulativeTimeUsed += usedInCall;
+}
+
+bool ResourceManager::cumulativeLimitOn() const {
+  return d_timeBudgetCumulative || d_resourceBudgetCumulative;
+}
+
+bool ResourceManager::perCallLimitOn() const {
+  return d_timeBudgetPerCall || d_resourceBudgetPerCall;
+}
+
+bool ResourceManager::outOfResources() const {
+  // resource limiting not enabled
+  if (d_resourceBudgetPerCall == 0 &&
+      d_resourceBudgetCumulative == 0)
+    return false;
+
+  return getResourceRemaining() == 0;
+}
+
+bool ResourceManager::outOfTime() const {
+  if (d_timeBudgetPerCall == 0 &&
+      d_timeBudgetCumulative == 0)
+    return false;
+
+  return d_cumulativeTimer.expired() || d_perCallTimer.expired();
+}
+
+void ResourceManager::useCPUTime(bool cpu) {
+  Trace("limit") << "ResourceManager::useCPUTime("<< cpu <<")\n";
+  d_cpuTime = cpu;
+}
+
+void ResourceManager::setHardLimit(bool value) {
+  Trace("limit") << "ResourceManager::setHardLimit("<< value <<")\n";
+  d_isHardLimit = value;
+}
+
+void ResourceManager::enable(bool on) {
+  Trace("limit") << "ResourceManager::enable("<< on <<")\n";
+  d_on = on;
+}
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
new file mode 100644
index 000000000..a16f60910
--- /dev/null
+++ b/src/util/resource_manager.h
@@ -0,0 +1,158 @@
+/*********************                                                        */
+/*! \file resource_manager.h
+** \verbatim
+** Original author: Liana Hadarean
+** Major contributors: none
+** Minor contributors (to current version): none
+** This file is part of the CVC4 project.
+** Copyright (c) 2009-2014  New York University and The University of Iowa
+** See the file COPYING in the top-level source directory for licensing
+** information.\endverbatim
+**
+** \brief Manages and updates various resource and time limits
+**
+** Manages and updates various resource and time limits.
+**/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__RESOURCE_MANAGER_H
+#define __CVC4__RESOURCE_MANAGER_H
+
+#include <cstddef>
+#include <sys/time.h>
+
+#include "util/exception.h"
+#include "util/unsafe_interrupt_exception.h"
+
+namespace CVC4 {
+
+/**
+ * A helper class to keep track of a time budget and signal
+ * the PropEngine when the budget expires.
+ */
+class CVC4_PUBLIC Timer {
+
+  unsigned long d_ms;
+  timeval d_wall_limit;
+  clock_t d_cpu_start_time;
+  clock_t d_cpu_limit;
+
+  bool d_wall_time;
+
+  /** Return the milliseconds elapsed since last set() cpu time. */
+  unsigned long elapsedCPU() const;
+  /** Return the milliseconds elapsed since last set() wall time. */
+  unsigned long elapsedWall() const;
+
+public:
+
+  /** Construct a Timer. */
+  Timer()
+    : d_ms(0)
+    , d_cpu_start_time(0)
+    , d_cpu_limit(0)
+    , d_wall_time(true)
+  {}
+
+  /** Is the timer currently active? */
+  bool on() const {
+    return d_ms != 0;
+  }
+
+  /** Set a millisecond timer (0==off). */
+  void set(unsigned long millis, bool wall_time = true);
+  /** Return the milliseconds elapsed since last set() wall/cpu time
+   depending on d_wall_time*/
+  unsigned long elapsed() const;
+  bool expired() const;
+
+};/* class Timer */
+
+
+class CVC4_PUBLIC ResourceManager {
+
+  Timer d_cumulativeTimer;
+  Timer d_perCallTimer;
+
+  /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
+  unsigned long d_timeBudgetCumulative;
+  /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
+  unsigned long d_timeBudgetPerCall;
+  /** A user-imposed cumulative resource budget. 0 = no limit. */
+  unsigned long d_resourceBudgetCumulative;
+  /** A user-imposed per-call resource budget. 0 = no limit. */
+  unsigned long d_resourceBudgetPerCall;
+
+  /** The number of milliseconds used. */
+  unsigned long d_cumulativeTimeUsed;
+  /** The amount of resource used. */
+  unsigned long d_cumulativeResourceUsed;
+
+  /** The ammount of resource used during this call. */
+  unsigned long d_thisCallResourceUsed;
+
+  /**
+   * The ammount of resource budget for this call (min between per call
+   * budget and left-over cumulative budget.
+   */
+  unsigned long d_thisCallTimeBudget;
+  unsigned long d_thisCallResourceBudget;
+
+  bool d_isHardLimit;
+  bool d_on;
+  bool d_cpuTime;
+  unsigned long d_spendResourceCalls;
+
+  /** Counter indicating how often to check resource manager in loops */
+  static const unsigned long s_resourceCount;
+
+public:
+
+  ResourceManager();
+
+  bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
+  bool cumulativeLimitOn() const;
+  bool perCallLimitOn() const;
+
+  bool outOfResources() const;
+  bool outOfTime() const;
+  bool out() const { return d_on && (outOfResources() || outOfTime()); }
+
+  unsigned long getResourceUsage() const;
+  unsigned long getTimeUsage() const;
+  unsigned long getResourceRemaining() const;
+  unsigned long getTimeRemaining() const;
+
+  unsigned long getResourceBudgetForThisCall() {
+    return d_thisCallResourceBudget;
+  }
+
+  void spendResource() throw(UnsafeInterruptException);
+
+  void setHardLimit(bool value);
+  void setResourceLimit(unsigned long units, bool cumulative = false);
+  void setTimeLimit(unsigned long millis, bool cumulative = false);
+  void useCPUTime(bool cpu);
+
+  void enable(bool on);
+
+  /**
+   * Resets perCall limits to mark the start of a new call,
+   * updates budget for current call and starts the timer
+   */
+  void beginCall();
+
+  /**
+   * Marks the end of a SmtEngine check call, stops the per
+   * call timer, updates cumulative time used.
+   */
+  void endCall();
+
+  static unsigned long getFrequencyCount() { return s_resourceCount; }
+
+};/* class ResourceManager */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RESOURCE_MANAGER_H */
diff --git a/src/util/resource_manager.i b/src/util/resource_manager.i
new file mode 100644
index 000000000..0f55c2bce
--- /dev/null
+++ b/src/util/resource_manager.i
@@ -0,0 +1,5 @@
+%{
+#include "util/resource_manager.h"
+%}
+
+%include "util/resource_manager.h"
diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h
new file mode 100644
index 000000000..e19fc37ce
--- /dev/null
+++ b/src/util/unsafe_interrupt_exception.h
@@ -0,0 +1,43 @@
+/*********************                                                        */
+/*! \file modal_exception.h
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An exception that is thrown when the solver is out of time/resources
+ ** and is interrupted in an unsafe state
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
+#define __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC UnsafeInterruptException : public CVC4::Exception {
+public:
+  UnsafeInterruptException() :
+    Exception("Interrupted in unsafe state due to "
+              "time/resource limit.") {
+  }
+
+  UnsafeInterruptException(const std::string& msg) :
+    Exception(msg) {
+  }
+
+  UnsafeInterruptException(const char* msg) :
+    Exception(msg) {
+  }
+};/* class UnsafeInterruptException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */
diff --git a/src/util/unsafe_interrupt_exception.i b/src/util/unsafe_interrupt_exception.i
new file mode 100644
index 000000000..94a552877
--- /dev/null
+++ b/src/util/unsafe_interrupt_exception.i
@@ -0,0 +1,7 @@
+%{
+#include "util/unsafe_interrupt_exception.h"
+%}
+
+%ignore CVC4::UnsafeInterruptException::UnsafeInterruptException(const char*);
+
+%include "util/unsafe_interrupt_exception.h"