From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 15 Feb 2013 16:48:24 +0000 (-0500)
Subject: Fix ECHO command in CVC language parser to not output quotation marks
X-Git-Tag: cvc5-1.0.0~7406^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e73d6564200fb6f4550b217ce5a060242f6ecaf;p=cvc5.git

Fix ECHO command in CVC language parser to not output quotation marks
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index d0fe9036b..1af4799be 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -742,10 +742,7 @@ mainCommand[CVC4::Command*& cmd]
 
   | ECHO_TOK
     ( simpleSymbolicExpr[sexpr]
-      { std::stringstream ss;
-        ss << sexpr;
-        cmd = new EchoCommand(ss.str());
-      }
+      { cmd = new EchoCommand(sexpr.getValue()); }
     | { cmd = new EchoCommand(); }
     )