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 /src/expr | |
parent | 67bc89bd3fa304ea39934c14a7187c088e600011 (diff) |
dump define-funs correctly with "--dump declarations", whether the function is defined via API or through input language
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 2 |
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); } |