diff options
Diffstat (limited to 'src/printer/printer.cpp')
| -rw-r--r-- | src/printer/printer.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index b66ae5728..16b626e30 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -16,6 +16,7 @@ #include <string> +#include "expr/node_manager_attributes.h" #include "options/base_options.h" #include "options/language.h" #include "printer/ast/ast_printer.h" @@ -201,9 +202,8 @@ void Printer::toStreamCmdDeclareFunction(std::ostream& out, void Printer::toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const { - std::stringstream vs; - vs << v; - toStreamCmdDeclareFunction(out, vs.str(), v.getType()); + std::string vs = v.getAttribute(expr::VarNameAttr()); + toStreamCmdDeclareFunction(out, vs, v.getType()); } void Printer::toStreamCmdDeclarePool(std::ostream& out, |