mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

Use unique temp files in TPTP tests

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

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-23 23:12:22 +00:00 • committed by GitHub
parent 991d12a214
commit 5ea9f284eb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 15 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/test/tptp.cpp
View file

@ -1,9 +1,11 @@
#include <cstdio> #include <cstdio>
#include <filesystem>
#include <fstream> #include <fstream>
#include <string> #include <string>
#include <vector> #include <vector>
#include <iostream> #include <iostream>
#include <sstream> #include <sstream>
#include <unistd.h>
#include "util/debug.h" #include "util/debug.h"
#include "util/error_codes.h" #include "util/error_codes.h"
#include "cmd_context/tptp_frontend.h" #include "cmd_context/tptp_frontend.h"
@ -43,6 +45,17 @@ static void write_file(char const* path, char const* contents) {
ENSURE(out.good()); 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_statistics;
extern bool g_display_model; extern bool g_display_model;
@ -123,8 +136,7 @@ R"(tff(c1,conjecture, $less($uminus(2),0)).)",
ENSURE(code == ERR_PARSER); ENSURE(code == ERR_PARSER);
ENSURE(err.find("denominator of rational literal cannot be zero") != std::string::npos); ENSURE(err.find("denominator of rational literal cannot be zero") != std::string::npos);
char const* included = "/tmp/z3-tptp-selected-include.p"; std::string included = write_temp_file(
write_file(included,
R"(fof(keep,axiom,p). R"(fof(keep,axiom,p).
fof(poison,axiom,~ p).)"); fof(poison,axiom,~ p).)");
std::string selected_include = std::string selected_include =
@ -133,7 +145,7 @@ fof(a1,axiom,q).)";
code = run_tptp(selected_include.c_str(), out, err); code = run_tptp(selected_include.c_str(), out, err);
ENSURE(code == 0); ENSURE(code == 0);
ENSURE(out.find("% SZS status Satisfiable") != std::string::npos); 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); code = run_tptp("fof(a1,axiom,[p(a),q(a)]).", out, err);
ENSURE(code == ERR_PARSER); ENSURE(code == ERR_PARSER);