From a9428f64ae8d58c8a89512675bf526c26940c148 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sun, 10 May 2026 15:19:12 +0000
Subject: [PATCH] Harden TPTP cmd_context integration and suppress check-sat
 echo

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

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/shell/tptp_frontend.cpp | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/shell/tptp_frontend.cpp b/src/shell/tptp_frontend.cpp
index 6e2d4d722..44b52770f 100644
--- a/src/shell/tptp_frontend.cpp
+++ b/src/shell/tptp_frontend.cpp
@@ -323,7 +323,7 @@ class tptp_parser {
     }
 
     static bool is_ttype(sort* s) {
-        return s->get_name() == symbol("$tType");
+        return s && s->get_name() == symbol("$tType");
     }
 
     static std::string mk_decl_key(std::string const& name, unsigned arity, char tag) {
@@ -750,13 +750,16 @@ expr_ref tptp_parser::parse_term() {
     expr_ref e = parse_term_primary();
     while (accept(token_kind::at_tok)) {
         expr_ref arg = parse_term_primary();
-        if (!is_app(e) || to_app(e)->get_decl()->get_family_id() != null_family_id)
+        if (!is_app(e))
             throw parse_error("application operator (@) requires uninterpreted function on left-hand side");
         app* a = to_app(e);
+        func_decl* d = a->get_decl();
+        if (!d || d->get_family_id() != null_family_id)
+            throw parse_error("application operator (@) requires uninterpreted function on left-hand side");
         expr_ref_vector args(m);
         for (unsigned i = 0; i < a->get_num_args(); ++i) args.push_back(a->get_arg(i));
         args.push_back(arg);
-        e = m.mk_app(a->get_decl(), args.size(), args.data());
+        e = m.mk_app(d, args.size(), args.data());
     }
     return e;
 }
@@ -787,6 +790,7 @@ unsigned read_tptp(char const* file_name) {
         std::ostringstream sink;
         ctx.set_regular_stream(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";