diff options
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 53ca266f4..8b61e92d3 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -479,8 +479,6 @@ Type DeclareFunctionCommand::getType() const throw() { } void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this; - smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_FUN ); d_commandStatus = CommandSuccess::instance(); } @@ -511,8 +509,6 @@ Type DeclareTypeCommand::getType() const throw() { } void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this; - smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_SORT ); d_commandStatus = CommandSuccess::instance(); } @@ -552,7 +548,6 @@ Type DefineTypeCommand::getType() const throw() { } void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this; d_commandStatus = CommandSuccess::instance(); } @@ -602,7 +597,6 @@ Expr DefineFunctionCommand::getFormula() const throw() { } void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - //Dump("declarations") << *this; -- done by SmtEngine try { if(!d_func.isNull()) { smtEngine->defineFunction(d_func, d_formals, d_formula); @@ -1275,8 +1269,6 @@ DatatypeDeclarationCommand::getDatatypes() const throw() { } void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this; - smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_DATATYPES ); d_commandStatus = CommandSuccess::instance(); } |