diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-15 12:37:50 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-15 12:37:50 -0500 |
| commit | 460ee6b1b8f8f2fd93f65d94cb8f614dd406c758 (patch) | |
| tree | 6cb43246c130bc82681edf3ea00e7fe95b0a6ee8 /src/parser | |
| parent | c5dc113bad86f7027cc46b5fc13b47106ba98d99 (diff) | |
| parent | 814526633b07146d4f0f9e6d24583bd6e645d8cd (diff) | |
Merge branch '1.0.x'
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 5 |
1 files changed, 1 insertions, 4 deletions
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(); } ) |