[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

1 files changed, 59 insertions, 59 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index bd514e2a8..9c6a143c5 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -105,7 +105,7 @@ 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() {
+void Command::invoke(SmtEngine* smtEngine, std::ostream& out) {
   invoke(smtEngine);
   if(!(isMuted() && ok())) {
     printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
@@ -127,7 +127,7 @@ void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const t
   Printer::getPrinter(language)->toStream(out, this);
 }
 
-void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void Command::printResult(std::ostream& out, uint32_t verbosity) const {
   if(d_commandStatus != NULL) {
     if((!ok() && verbosity >= 1) || verbosity >= 2) {
       out << *d_commandStatus;
@@ -145,7 +145,7 @@ std::string EmptyCommand::getName() const throw() {
   return d_name;
 }
 
-void EmptyCommand::invoke(SmtEngine* smtEngine) throw() {
+void EmptyCommand::invoke(SmtEngine* smtEngine) {
   /* empty commands have no implementation */
   d_commandStatus = CommandSuccess::instance();
 }
@@ -172,12 +172,12 @@ std::string EchoCommand::getOutput() const throw() {
   return d_output;
 }
 
-void EchoCommand::invoke(SmtEngine* smtEngine) throw() {
+void EchoCommand::invoke(SmtEngine* smtEngine) {
   /* we don't have an output stream here, nothing to do */
   d_commandStatus = CommandSuccess::instance();
 }
 
-void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) {
   out << d_output << std::endl;
   d_commandStatus = CommandSuccess::instance();
   printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
@@ -205,7 +205,7 @@ Expr AssertCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
+void AssertCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->assertFormula(d_expr, d_inUnsatCore);
     d_commandStatus = CommandSuccess::instance();
@@ -230,7 +230,7 @@ std::string AssertCommand::getCommandName() const throw() {
 
 /* class PushCommand */
 
-void PushCommand::invoke(SmtEngine* smtEngine) throw() {
+void PushCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->push();
     d_commandStatus = CommandSuccess::instance();
@@ -255,7 +255,7 @@ std::string PushCommand::getCommandName() const throw() {
 
 /* class PopCommand */
 
-void PopCommand::invoke(SmtEngine* smtEngine) throw() {
+void PopCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->pop();
     d_commandStatus = CommandSuccess::instance();
@@ -292,7 +292,7 @@ Expr CheckSatCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() {
+void CheckSatCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->checkSat(d_expr);
     d_commandStatus = CommandSuccess::instance();
@@ -305,7 +305,7 @@ Result CheckSatCommand::getResult() const throw() {
   return d_result;
 }
 
-void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -339,7 +339,7 @@ Expr QueryCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void QueryCommand::invoke(SmtEngine* smtEngine) throw() {
+void QueryCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->query(d_expr);
     d_commandStatus = CommandSuccess::instance();
@@ -352,7 +352,7 @@ Result QueryCommand::getResult() const throw() {
   return d_result;
 }
 
-void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -391,7 +391,7 @@ Expr CheckSynthCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void CheckSynthCommand::invoke(SmtEngine* smtEngine) throw() {
+void CheckSynthCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->checkSynth(d_expr);
     d_commandStatus = CommandSuccess::instance();
@@ -404,7 +404,7 @@ Result CheckSynthCommand::getResult() const throw() {
   return d_result;
 }
 
-void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -431,7 +431,7 @@ std::string CheckSynthCommand::getCommandName() const throw() {
 
 /* class ResetCommand */
 
-void ResetCommand::invoke(SmtEngine* smtEngine) throw() {
+void ResetCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->reset();
     d_commandStatus = CommandSuccess::instance();
@@ -454,7 +454,7 @@ std::string ResetCommand::getCommandName() const throw() {
 
 /* class ResetAssertionsCommand */
 
-void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->resetAssertions();
     d_commandStatus = CommandSuccess::instance();
@@ -477,7 +477,7 @@ std::string ResetAssertionsCommand::getCommandName() const throw() {
 
 /* class QuitCommand */
 
-void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
+void QuitCommand::invoke(SmtEngine* smtEngine) {
   Dump("benchmark") << *this;
   d_commandStatus = CommandSuccess::instance();
 }
@@ -503,7 +503,7 @@ std::string CommentCommand::getComment() const throw() {
   return d_comment;
 }
 
-void CommentCommand::invoke(SmtEngine* smtEngine) throw() {
+void CommentCommand::invoke(SmtEngine* smtEngine) {
   Dump("benchmark") << *this;
   d_commandStatus = CommandSuccess::instance();
 }
@@ -540,7 +540,7 @@ void CommandSequence::clear() throw() {
   d_commandSequence.clear();
 }
 
-void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
+void CommandSequence::invoke(SmtEngine* smtEngine) {
   for(; d_index < d_commandSequence.size(); ++d_index) {
     d_commandSequence[d_index]->invoke(smtEngine);
     if(! d_commandSequence[d_index]->ok()) {
@@ -555,7 +555,7 @@ void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
-void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
   for(; d_index < d_commandSequence.size(); ++d_index) {
     d_commandSequence[d_index]->invoke(smtEngine, out);
     if(! d_commandSequence[d_index]->ok()) {
@@ -654,7 +654,7 @@ void DeclareFunctionCommand::setPrintInModel( bool p ) {
   d_printInModelSetByUser = true;
 }
 
-void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) {
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -694,7 +694,7 @@ Type DeclareTypeCommand::getType() const throw() {
   return d_type;
 }
 
-void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
+void DeclareTypeCommand::invoke(SmtEngine* smtEngine) {
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -737,7 +737,7 @@ Type DefineTypeCommand::getType() const throw() {
   return d_type;
 }
 
-void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
+void DefineTypeCommand::invoke(SmtEngine* smtEngine) {
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -790,7 +790,7 @@ Expr DefineFunctionCommand::getFormula() const throw() {
   return d_formula;
 }
 
-void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
   try {
     if(!d_func.isNull()) {
       smtEngine->defineFunction(d_func, d_formals, d_formula);
@@ -827,7 +827,7 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
   DefineFunctionCommand(id, func, formals, formula) {
 }
 
-void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) {
   this->DefineFunctionCommand::invoke(smtEngine);
   if(!d_func.isNull() && d_func.getType().isBoolean()) {
     smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func));
@@ -865,7 +865,7 @@ SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr
   d_attr( attr ), d_expr( expr ), d_str_value( value ){
 }
 
-void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){
+void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) {
   try {
     if(!d_expr.isNull()) {
       smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value );
@@ -903,7 +903,7 @@ Expr SimplifyCommand::getTerm() const throw() {
   return d_term;
 }
 
-void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
+void SimplifyCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->simplify(d_term);
     d_commandStatus = CommandSuccess::instance();
@@ -918,7 +918,7 @@ Expr SimplifyCommand::getResult() const throw() {
   return d_result;
 }
 
-void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -952,7 +952,7 @@ Expr ExpandDefinitionsCommand::getTerm() const throw() {
   return d_term;
 }
 
-void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() {
+void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) {
   d_result = smtEngine->expandDefinitions(d_term);
   d_commandStatus = CommandSuccess::instance();
 }
@@ -961,7 +961,7 @@ Expr ExpandDefinitionsCommand::getResult() const throw() {
   return d_result;
 }
 
-void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1002,7 +1002,7 @@ const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
   return d_terms;
 }
 
-void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetValueCommand::invoke(SmtEngine* smtEngine) {
   try {
     vector<Expr> result;
     ExprManager* em = smtEngine->getExprManager();
@@ -1034,7 +1034,7 @@ Expr GetValueCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1068,7 +1068,7 @@ std::string GetValueCommand::getCommandName() const throw() {
 GetAssignmentCommand::GetAssignmentCommand() throw() {
 }
 
-void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetAssignmentCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getAssignment();
     d_commandStatus = CommandSuccess::instance();
@@ -1083,7 +1083,7 @@ SExpr GetAssignmentCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1112,7 +1112,7 @@ std::string GetAssignmentCommand::getCommandName() const throw() {
 GetModelCommand::GetModelCommand() throw() {
 }
 
-void GetModelCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetModelCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getModel();
     d_smtEngine = smtEngine;
@@ -1130,7 +1130,7 @@ Model* GetModelCommand::getResult() const throw() {
 }
 */
 
-void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1161,7 +1161,7 @@ std::string GetModelCommand::getCommandName() const throw() {
 GetProofCommand::GetProofCommand() throw() {
 }
 
-void GetProofCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetProofCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_smtEngine = smtEngine;
     d_result = smtEngine->getProof();
@@ -1177,7 +1177,7 @@ Proof* GetProofCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1209,7 +1209,7 @@ std::string GetProofCommand::getCommandName() const throw() {
 GetInstantiationsCommand::GetInstantiationsCommand() throw() {
 }
 
-void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_smtEngine = smtEngine;
     d_commandStatus = CommandSuccess::instance();
@@ -1222,7 +1222,7 @@ void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
 //  return d_result;
 //}
 
-void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1253,7 +1253,7 @@ std::string GetInstantiationsCommand::getCommandName() const throw() {
 GetSynthSolutionCommand::GetSynthSolutionCommand() throw() {
 }
 
-void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_smtEngine = smtEngine;
     d_commandStatus = CommandSuccess::instance();
@@ -1262,7 +1262,7 @@ void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
-void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1303,7 +1303,7 @@ bool GetQuantifierEliminationCommand::getDoFull() const throw() {
   return d_doFull;
 }
 
-void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
     d_commandStatus = CommandSuccess::instance();
@@ -1316,7 +1316,7 @@ Expr GetQuantifierEliminationCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1348,7 +1348,7 @@ GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
 GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) {
 }
 
-void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getUnsatCore();
     d_commandStatus = CommandSuccess::instance();
@@ -1357,7 +1357,7 @@ void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
-void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1391,7 +1391,7 @@ std::string GetUnsatCoreCommand::getCommandName() const throw() {
 GetAssertionsCommand::GetAssertionsCommand() throw() {
 }
 
-void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetAssertionsCommand::invoke(SmtEngine* smtEngine) {
   try {
     stringstream ss;
     const vector<Expr> v = smtEngine->getAssertions();
@@ -1409,7 +1409,7 @@ std::string GetAssertionsCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1443,7 +1443,7 @@ BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
   return d_status;
 }
 
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
   try {
     stringstream ss;
     ss << d_status;
@@ -1477,7 +1477,7 @@ std::string SetBenchmarkLogicCommand::getLogic() const throw() {
   return d_logic;
 }
 
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setLogic(d_logic);
     d_commandStatus = CommandSuccess::instance();
@@ -1513,7 +1513,7 @@ SExpr SetInfoCommand::getSExpr() const throw() {
   return d_sexpr;
 }
 
-void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setInfo(d_flag, d_sexpr);
     d_commandStatus = CommandSuccess::instance();
@@ -1547,7 +1547,7 @@ std::string GetInfoCommand::getFlag() const throw() {
   return d_flag;
 }
 
-void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     vector<SExpr> v;
     v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
@@ -1570,7 +1570,7 @@ std::string GetInfoCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else if(d_result != "") {
@@ -1609,7 +1609,7 @@ SExpr SetOptionCommand::getSExpr() const throw() {
   return d_sexpr;
 }
 
-void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setOption(d_flag, d_sexpr);
     d_commandStatus = CommandSuccess::instance();
@@ -1642,7 +1642,7 @@ std::string GetOptionCommand::getFlag() const throw() {
   return d_flag;
 }
 
-void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     SExpr res = smtEngine->getOption(d_flag);
     d_result = res.toString();
@@ -1658,7 +1658,7 @@ std::string GetOptionCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else if(d_result != "") {
@@ -1698,7 +1698,7 @@ DatatypeDeclarationCommand::getDatatypes() const throw() {
   return d_datatypes;
 }
 
-void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
+void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -1749,7 +1749,7 @@ const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const thro
   return d_triggers;
 }
 
-void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() {
+void RewriteRuleCommand::invoke(SmtEngine* smtEngine) {
   try {
     ExprManager* em = smtEngine->getExprManager();
     /** build vars list */
@@ -1861,7 +1861,7 @@ bool PropagateRuleCommand::isDeduction() const throw() {
   return d_deduction;
 }
 
-void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() {
+void PropagateRuleCommand::invoke(SmtEngine* smtEngine) {
   try {
     ExprManager* em = smtEngine->getExprManager();
     /** build vars list */