From 84f0e9f58671083794dce8ed8e71a8fa9fe587cd Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 16 Sep 2011 21:54:21 +0000
Subject: [PATCH] dump define-funs correctly with "--dump declarations",
 whether the function is defined via API or through input language

---
 src/expr/command.cpp   | 2 +-
 src/smt/smt_engine.cpp | 2 --
 2 files changed, 1 insertion(+), 3 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);
   }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d11130aac..24ebf9bfd 100644
--- 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
-- 
2.30.2