From a0b25147d9a1ead8bc0c5949a04ff6ffef67be93 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 20 Jun 2017 14:48:03 +0100 Subject: [PATCH] Fix for the fix for #1062. --- src/cmd_context/basic_cmds.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index e915b7b4e..ea6d1c232 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -274,10 +274,9 @@ UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr ctx.regular_stream() << std::endl; }); -UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr *, { - ctx.display(ctx.regular_stream(), arg); - ctx.regular_stream() << std::endl; -}); +UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, + bool smt2c = ctx.params().m_smtlib2_compliant; + ctx.regular_stream() << (smt2c ? "\"" : "") << arg << (smt2c ? "\"" : "") << std::endl;); class set_get_option_cmd : public cmd {