diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-09-16 21:54:21 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-09-16 21:54:21 +0000 |
| commit | 84f0e9f58671083794dce8ed8e71a8fa9fe587cd (patch) | |
| tree | 2dcf0b3d91cc2a16eda91635f367913d9dc27803 | |
| parent | 67bc89bd3fa304ea39934c14a7187c088e600011 (diff) | |
dump define-funs correctly with "--dump declarations", whether the function is defined via API or through input language
| -rw-r--r-- | src/expr/command.cpp | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 2 |
2 files changed, 1 insertions, 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 |