Some exception specification fixes in SmtEngine/Command infrastructure

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index fa2a8d1f2fa4fc4661d96ad4e1e3735e77c20003..9edc77e391ef94e3fd38d7ed9912fe73a8f796af 100644 (file)
--- 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 6b0d953ddf66380690285ff74f9aa017d27f36ca..e7c0999da0d49f570f4ceff50a06b1bcf891c1b9 100644 (file)
--- 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 cdae68d96c57162fc8f3123a7043e1f1bc8b42d7..fecfba14a0cfa831410fde49fd56a0ccc22af742 100644 (file)
--- 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