1 files changed, 4 insertions, 4 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index f48e07887..f4b40cbb3 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -990,11 +990,11 @@ std::string GetInfoCommand::getFlag() const throw() {
 
 void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    vector<SExpr> v;
-    v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
-    v.push_back(smtEngine->getInfo(d_flag));
+    SExpr response = smtEngine->getInfo(d_flag);
     stringstream ss;
-    ss << SExpr(v);
+    ss << SExpr(SExpr::Keyword(d_flag))
+       << ' '
+       << response;
     d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {