From 5ea9f284ebee8303239d83debab7e6f665f12322 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 23 May 2026 23:12:22 +0000
Subject: [PATCH] Use unique temp files in TPTP tests

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/test/tptp.cpp | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp
index e95edbb3a..bfa1df881 100644
--- a/src/test/tptp.cpp
+++ b/src/test/tptp.cpp
@@ -1,9 +1,11 @@
 #include <cstdio>
+#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"
@@ -43,6 +45,17 @@ 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();
+}
+
 extern bool g_display_statistics;
 extern bool g_display_model;
 
@@ -123,8 +136,7 @@ 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);
 
-    char const* included = "/tmp/z3-tptp-selected-include.p";
-    write_file(included,
+    std::string included = write_temp_file(
 R"(fof(keep,axiom,p).
 fof(poison,axiom,~ p).)");
     std::string selected_include =
@@ -133,7 +145,7 @@ 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);
+    std::remove(included.c_str());
 
     code = run_tptp("fof(a1,axiom,[p(a),q(a)]).", out, err);
     ENSURE(code == ERR_PARSER);