From 1947446736a89121620a6a0d4d90823ccddb5c63 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 23 May 2026 23:13:50 +0000
Subject: [PATCH] Address TPTP review feedback

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ca1df142-d992-4e45-a8b3-859fa70a5222

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/cmd_context/tptp_frontend.cpp |  2 +-
 src/test/tptp.cpp                 | 33 ++++++++++++++++++-------------
 2 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index 0bb3f8c17..1589c539a 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -1693,7 +1693,7 @@ class tptp_parser {
             }
             catch (z3_exception const& ex) {
                 std::ostringstream out;
-                out << "invalid formula '" << formula_name << "': " << ex.what();
+                out << "semantic error in formula '" << formula_name << "': " << ex.what();
                 throw parse_error(out.str());
             }
         }
diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp
index bfa1df881..9c764ab64 100644
--- a/src/test/tptp.cpp
+++ b/src/test/tptp.cpp
@@ -1,11 +1,11 @@
 #include <cstdio>
+#include <chrono>
 #include <filesystem>
 #include <fstream>
 #include <string>
 #include <vector>
 #include <iostream>
 #include <sstream>
-#include <unistd.h>
 #include "util/debug.h"
 #include "util/error_codes.h"
 #include "cmd_context/tptp_frontend.h"
@@ -45,16 +45,22 @@ static void write_file(char const* path, char const* contents) {
     ENSURE(out.good());
 }
 
-static std::string write_temp_file(char const* contents) {
-    std::string tmpl = (std::filesystem::temp_directory_path() / "z3-tptp-XXXXXX").string();
-    std::vector<char> path(tmpl.begin(), tmpl.end());
-    path.push_back('\0');
-    int fd = mkstemp(path.data());
-    ENSURE(fd != -1);
-    ::close(fd);
-    write_file(path.data(), contents);
-    return path.data();
-}
+class scoped_temp_file {
+    std::string m_path;
+public:
+    scoped_temp_file(char const* contents) {
+        static unsigned counter = 0;
+        auto stamp = std::chrono::steady_clock::now().time_since_epoch().count();
+        m_path = (std::filesystem::temp_directory_path() /
+            ("z3-tptp-" + std::to_string(stamp) + "-" + std::to_string(counter++) + ".p")).string();
+        write_file(m_path.c_str(), contents);
+    }
+    ~scoped_temp_file() {
+        if (!m_path.empty())
+            std::remove(m_path.c_str());
+    }
+    std::string const& path() const { return m_path; }
+};
 
 extern bool g_display_statistics;
 extern bool g_display_model;
@@ -136,16 +142,15 @@ R"(tff(c1,conjecture, $less($uminus(2),0)).)",
     ENSURE(code == ERR_PARSER);
     ENSURE(err.find("denominator of rational literal cannot be zero") != std::string::npos);
 
-    std::string included = write_temp_file(
+    scoped_temp_file included(
 R"(fof(keep,axiom,p).
 fof(poison,axiom,~ p).)");
     std::string selected_include =
-        std::string("include('") + included + R"(',[keep]).
+        std::string("include('") + included.path() + R"(',[keep]).
 fof(a1,axiom,q).)";
     code = run_tptp(selected_include.c_str(), out, err);
     ENSURE(code == 0);
     ENSURE(out.find("% SZS status Satisfiable") != std::string::npos);
-    std::remove(included.c_str());
 
     code = run_tptp("fof(a1,axiom,[p(a),q(a)]).", out, err);
     ENSURE(code == ERR_PARSER);