From ab21caf55f52928b1a3cbaf927bcdd6fd73d92bd Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 20 Jun 2017 14:39:22 +0100
Subject: [PATCH] Reverted fix for quoted echo strings when
 smtlib2_compliant=false. Kindly reported by Armael Gueneau. Fixes #1062.

---
 src/cmd_context/basic_cmds.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 563d44afa..e915b7b4e 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -274,7 +274,10 @@ UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr
     ctx.regular_stream() << std::endl;
 });
 
-UNARY_CMD(echo_cmd, "echo", "<string>", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << "\"" << arg << "\"" << std::endl;);
+UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, {
+    ctx.display(ctx.regular_stream(), arg);
+    ctx.regular_stream() << std::endl;
+});
 
 
 class set_get_option_cmd : public cmd {