mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 23:25:36 +00:00
Code Activity

Make TPTP check-sat stream redirection exception-safe

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/2a6b01d0-c799-4e44-aa73-ef228cb4402e

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-10 15:20:28 +00:00 • committed by GitHub
parent a9428f64ae
commit 9adfeedc9f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/shell/tptp_frontend.cpp
View file

@ -58,6 +58,13 @@ struct parse_error : public std::exception {
char const* what() const noexcept override { return m_msg.c_str(); }
};
class scoped_regular_stream {
cmd_context& m_ctx;
public:
scoped_regular_stream(cmd_context& ctx, std::ostream& out): m_ctx(ctx) { m_ctx.set_regular_stream(out); }
~scoped_regular_stream() { m_ctx.set_regular_stream("stdout"); }
};
struct token {
token_kind kind = token_kind::eof_tok;
std::string text;
@ -788,9 +795,8 @@ unsigned read_tptp(char const* file_name) {
else p.parse_stream(std::cin);
std::ostringstream sink;
ctx.set_regular_stream(sink);
scoped_regular_stream scoped_stream(ctx, sink);
ctx.check_sat(0, nullptr);
ctx.set_regular_stream("stdout");
switch (ctx.cs_state()) {
case cmd_context::css_unsat:
if (p.has_conjecture()) std::cout << "% SZS status Theorem\n";