diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-20 18:09:59 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-20 18:41:23 -0500 |
commit | 19847e87a8894d61b59d27bedd35aa73e44c126f (patch) | |
tree | c3c600e21e6fd74edf5d5e8a442cf6c2d2f28bab /src | |
parent | 6fe464a1e87d62aa4ad12f7410542e09c3464436 (diff) |
Some exception specification fixes in SmtEngine/Command infrastructure
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/command.cpp | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 |
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 |