From fc719a5ee82361ffedb9ef46793e3401fdc32cc5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 24 Mar 2018 10:37:05 -0700
Subject: [PATCH] fix diagnostic output #1553

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_parsers.cpp       | 12 +++++++-----
 src/cmd_context/cmd_context.h |  1 +
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index 3af2e567c..28db62cc3 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -122,6 +122,7 @@ extern "C" {
     }
 
     Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) {
+        std::stringstream ous;
         Z3_TRY;
         LOG_Z3_eval_smtlib2_string(c, str);
         if (!mk_c(c)->cmd()) {
@@ -131,21 +132,22 @@ extern "C" {
         scoped_ptr<cmd_context>& ctx = mk_c(c)->cmd();
         std::string s(str);
         std::istringstream is(s);
-        std::stringstream ous;
         ctx->set_regular_stream(ous);
+        ctx->set_diagnostic_stream(ous);
         try {
             if (!parse_smt2_commands(*ctx.get(), is)) {
                 mk_c(c)->m_parser_error_buffer = ous.str();
                 SET_ERROR_CODE(Z3_PARSER_ERROR);
-                RETURN_Z3(nullptr);
+                RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
             }
         }
         catch (z3_exception& e) {
-            mk_c(c)->m_parser_error_buffer = e.msg();
+            if (ous.str().empty()) ous << e.msg();
+            mk_c(c)->m_parser_error_buffer = ous.str();
             SET_ERROR_CODE(Z3_PARSER_ERROR);
-            RETURN_Z3(nullptr);
+            RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
         }
         RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
-        Z3_CATCH_RETURN(nullptr);
+        Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str()));
     }
 };
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index d1e470c3b..90b3f6c56 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -406,6 +406,7 @@ public:
     void reset_user_tactics();
     void set_regular_stream(char const * name) { m_regular.set(name); }
     void set_regular_stream(std::ostream& out) { m_regular.set(out); }
+    void set_diagnostic_stream(std::ostream& out) { m_diagnostic.set(out); }
     void set_diagnostic_stream(char const * name);
     std::ostream & regular_stream() override { return *m_regular; }
     std::ostream & diagnostic_stream() override { return *m_diagnostic; }