1 files changed, 21 insertions, 0 deletions
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());
   }