dump define-funs correctly with "--dump declarations", whether the function is defined via API or through input language

1 files changed, 1 insertions, 1 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 5fb4d1fbd..61702561a 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -338,7 +338,7 @@ Expr DefineFunctionCommand::getFormula() const {
 }
 
 void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
-  Dump("declarations") << *this << endl;
+  //Dump("declarations") << *this << endl; -- done by SmtEngine
   if(!d_func.isNull()) {
     smtEngine->defineFunction(d_func, d_formals, d_formula);
   }