diff options
author | Andres Notzli <andres.noetzli@gmail.com> | 2017-03-29 23:27:56 +0200 |
---|---|---|
committer | Andres Notzli <andres.noetzli@gmail.com> | 2017-03-30 11:36:14 -0700 |
commit | faec717e89cfd657daaa370a061f4a8e282b0eff (patch) | |
tree | 067f9df357725c07ea7d04a5895801152b5f1a27 /src/smt/smt_engine.cpp | |
parent | 100037d531ff1fd30ed3dd5bed91076c383ad55c (diff) |
[Coverity] Remove throw qualifiers in src/smtremove_throw
Addresses coverity issues:
1172167
1172174
1172176
1172183
1172185
1172186
1172188
1172189
1172191
1172192
1172193
1172194
1172197
1172197
1172198
1172434
1172437
1172438
1172443
1172445
1172446
1172447
1172448
1362695
1362700
1362717
1362736
1362768
1362786
1362811
1379599
1421404
1421405
1421406
1421407
1421408
1421409
1421410
1421411
1421412
1421413
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8e641aca1..20cd5e83e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2104,8 +2104,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) throw UnrecognizedOptionException(); } -CVC4::SExpr SmtEngine::getInfo(const std::string& key) const - throw(OptionException, ModalException) { +CVC4::SExpr SmtEngine::getInfo(const std::string& key) const { SmtScope smts(this); @@ -4649,7 +4648,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin return resultNode.toExpr(); } -bool SmtEngine::addToAssignment(const Expr& ex) throw() { +bool SmtEngine::addToAssignment(const Expr& ex) { SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); @@ -4682,7 +4681,7 @@ bool SmtEngine::addToAssignment(const Expr& ex) throw() { return true; } -CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptException) { +CVC4::SExpr SmtEngine::getAssignment() { Trace("smt") << "SMT getAssignment()" << endl; SmtScope smts(this); finalOptionsAreSet(); @@ -4780,7 +4779,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool } } -Model* SmtEngine::getModel() throw(ModalException, UnsafeInterruptException) { +Model* SmtEngine::getModel() { Trace("smt") << "SMT getModel()" << endl; SmtScope smts(this); @@ -5042,7 +5041,7 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; } -UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptException) { +UnsatCore SmtEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << endl; SmtScope smts(this); finalOptionsAreSet(); @@ -5066,7 +5065,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptExcepti #endif /* IS_PROOFS_BUILD */ } -Proof* SmtEngine::getProof() throw(ModalException, UnsafeInterruptException) { +Proof* SmtEngine::getProof() { Trace("smt") << "SMT getProof()" << endl; SmtScope smts(this); finalOptionsAreSet(); @@ -5202,7 +5201,7 @@ void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< E } } -vector<Expr> SmtEngine::getAssertions() throw(ModalException) { +vector<Expr> SmtEngine::getAssertions() { SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); @@ -5250,7 +5249,7 @@ void SmtEngine::push() throw(ModalException, LogicException, UnsafeInterruptExce << d_userContext->getLevel() << endl; } -void SmtEngine::pop() throw(ModalException, UnsafeInterruptException) { +void SmtEngine::pop() { SmtScope smts(this); finalOptionsAreSet(); Trace("smt") << "SMT pop()" << endl; |