From 91e864914a579549703cdeae5c21484e3e72cd5f Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 8 May 2026 17:28:27 +0000
Subject: [PATCH] Polish TPTP frontend keys/path checks and deduplicate skip
 logic

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ba80bc5a-d80f-4d9f-8ed4-a962f697697c

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/shell/main.cpp          |  4 ++--
 src/shell/tptp_frontend.cpp | 20 ++++++++++++--------
 2 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index a4a93c8ab..5f324e604 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -134,8 +134,8 @@ static bool validate_is_ulong(char const* s) {
 }
 
 static bool is_tptp_extension(char const* ext) {
-    static char const* exts[] = {"p", "tptp", "fof", "cnf", "tff", "thf"};
-    for (char const* known_ext : exts) {
+    static char const* tptp_extensions[] = {"p", "tptp", "fof", "cnf", "tff", "thf"};
+    for (char const* known_ext : tptp_extensions) {
         if (strcmp(ext, known_ext) == 0)
             return true;
     }
diff --git a/src/shell/tptp_frontend.cpp b/src/shell/tptp_frontend.cpp
index c024f2751..5351855d4 100644
--- a/src/shell/tptp_frontend.cpp
+++ b/src/shell/tptp_frontend.cpp
@@ -322,7 +322,7 @@ class tptp_parser {
     }
 
     static std::string mk_decl_key(std::string const& name, unsigned arity, char tag) {
-        return std::to_string(name.size()) + ":" + name + ":" + std::to_string(arity) + ":" + tag;
+        return std::to_string(name.size()) + ":" + name + "\x1f" + std::to_string(arity) + "\x1f" + tag;
     }
 
     static std::string mk_typed_key(std::string const& name, unsigned arity) {
@@ -432,6 +432,15 @@ class tptp_parser {
         }
     }
 
+    void skip_balanced(token_kind open_k, token_kind close_k) {
+        int depth = 1;
+        while (depth > 0 && !is(token_kind::eof_tok)) {
+            if (accept(open_k)) ++depth;
+            else if (accept(close_k)) --depth;
+            else next();
+        }
+    }
+
     z3::expr parse_term();
 
     z3::expr parse_term_primary() {
@@ -612,7 +621,7 @@ class tptp_parser {
     static bool is_absolute_path(std::string const& name) {
         return !name.empty() &&
             (name[0] == '/' ||
-             (name.size() > 2 && std::isalpha(static_cast<unsigned char>(name[0])) && name[1] == ':'));
+             (name.size() >= 2 && std::isalpha(static_cast<unsigned char>(name[0])) && name[1] == ':'));
     }
 
     std::string dirname(std::string const& f) const {
@@ -638,12 +647,7 @@ class tptp_parser {
         std::string file = parse_name();
         if (accept(token_kind::comma)) {
             if (accept(token_kind::lbrack)) {
-                int depth = 1;
-                while (depth > 0 && !is(token_kind::eof_tok)) {
-                    if (accept(token_kind::lbrack)) ++depth;
-                    else if (accept(token_kind::rbrack)) --depth;
-                    else next();
-                }
+                skip_balanced(token_kind::lbrack, token_kind::rbrack);
             }
             else {
                 skip_annotations_until_rparen();