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 d0fe9036bb86b5d52ca4de0a15e98e90e447f2bd..1af4799beb779bd0f095a1bc7b627e23bc36f868 100644 (file)
--- 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(); }
     )