mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
fix diagnostic output #1553
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
753f2c89ef
commit
fc719a5ee8
|
@ -122,6 +122,7 @@ extern "C" {
|
||||||
}
|
}
|
||||||
|
|
||||||
Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) {
|
Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) {
|
||||||
|
std::stringstream ous;
|
||||||
Z3_TRY;
|
Z3_TRY;
|
||||||
LOG_Z3_eval_smtlib2_string(c, str);
|
LOG_Z3_eval_smtlib2_string(c, str);
|
||||||
if (!mk_c(c)->cmd()) {
|
if (!mk_c(c)->cmd()) {
|
||||||
|
@ -131,21 +132,22 @@ extern "C" {
|
||||||
scoped_ptr<cmd_context>& ctx = mk_c(c)->cmd();
|
scoped_ptr<cmd_context>& ctx = mk_c(c)->cmd();
|
||||||
std::string s(str);
|
std::string s(str);
|
||||||
std::istringstream is(s);
|
std::istringstream is(s);
|
||||||
std::stringstream ous;
|
|
||||||
ctx->set_regular_stream(ous);
|
ctx->set_regular_stream(ous);
|
||||||
|
ctx->set_diagnostic_stream(ous);
|
||||||
try {
|
try {
|
||||||
if (!parse_smt2_commands(*ctx.get(), is)) {
|
if (!parse_smt2_commands(*ctx.get(), is)) {
|
||||||
mk_c(c)->m_parser_error_buffer = ous.str();
|
mk_c(c)->m_parser_error_buffer = ous.str();
|
||||||
SET_ERROR_CODE(Z3_PARSER_ERROR);
|
SET_ERROR_CODE(Z3_PARSER_ERROR);
|
||||||
RETURN_Z3(nullptr);
|
RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
catch (z3_exception& e) {
|
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);
|
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()));
|
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()));
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
|
@ -406,6 +406,7 @@ public:
|
||||||
void reset_user_tactics();
|
void reset_user_tactics();
|
||||||
void set_regular_stream(char const * name) { m_regular.set(name); }
|
void set_regular_stream(char const * name) { m_regular.set(name); }
|
||||||
void set_regular_stream(std::ostream& out) { m_regular.set(out); }
|
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);
|
void set_diagnostic_stream(char const * name);
|
||||||
std::ostream & regular_stream() override { return *m_regular; }
|
std::ostream & regular_stream() override { return *m_regular; }
|
||||||
std::ostream & diagnostic_stream() override { return *m_diagnostic; }
|
std::ostream & diagnostic_stream() override { return *m_diagnostic; }
|
||||||
|
|
Loading…
Reference in a new issue