dump define-funs correctly with "--dump declarations", whether the function is define...

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 5fb4d1fbdb4b35afd955ebb4d93db29484ee3bff..61702561aeb1db8242d8b123315fe14711678dc0 100644 (file)
--- 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);
   }

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d11130aac12e3a6faa853c44f122ff488093009c..24ebf9bfdf85346c9be96c3373c0db56cd55be58 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -409,7 +409,6 @@ void SmtEngine::defineFunction(Expr func,
                                const std::vector<Expr>& formals,
                                Expr formula) {
   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
-  /*
   if(Dump.isOn("declarations")) {
     stringstream ss;
     ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations")))
@@ -417,7 +416,6 @@ void SmtEngine::defineFunction(Expr func,
     Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula)
                          << endl;
   }
-  */
   NodeManagerScope nms(d_nodeManager);
 
   // type check body