Some exception specification fixes in SmtEngine/Command infrastructure

3 files changed, 8 insertions, 4 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index fa2a8d1f2..9edc77e39 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -703,8 +703,12 @@ Expr SimplifyCommand::getTerm() const throw() {
 }
 
 void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
-  d_result = smtEngine->simplify(d_term);
-  d_commandStatus = CommandSuccess::instance();
+  try {
+    d_result = smtEngine->simplify(d_term);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
 Expr SimplifyCommand::getResult() const throw() {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6b0d953dd..e7c0999da 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3039,7 +3039,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
   return n.toExpr();
 }
 
-Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) {
+Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, TypeCheckingException, LogicException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index cdae68d96..fecfba14a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -444,7 +444,7 @@ public:
    * 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) throw(ModalException, LogicException);
+  Expr getValue(const Expr& e) throw(ModalException, TypeCheckingException, LogicException);
 
   /**
    * Add a function to the set of expressions whose value is to be