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

Harden TPTP cmd_context integration and suppress check-sat echo

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:19:12 +00:00 • committed by GitHub
parent e36d3936cb
commit a9428f64ae
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/shell/tptp_frontend.cpp
View file

@ -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";