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 test command handling and readability

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/dc1d46fc-4b6c-4f64-91a0-9fb57c73c166

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-11 06:59:38 +00:00 • committed by GitHub
parent 21b3f72b36
commit 906ac55c6a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 32 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/test/CMakeLists.txt
View file

@ -164,11 +164,14 @@ add_executable(test-z3
z3_add_install_tactic_rule(${z3_test_deps})
z3_add_memory_initializer_rule(${z3_test_deps})
z3_add_gparams_register_modules_rule(${z3_test_deps})
target_compile_definitions(test-z3 PRIVATE ${Z3_COMPONENT_CXX_DEFINES} Z3_TEST_SRC_DIR="${CMAKE_CURRENT_SOURCE_DIR}" Z3_TEST_BIN_DIR="${PROJECT_BINARY_DIR}")
target_compile_definitions(test-z3 PRIVATE
${Z3_COMPONENT_CXX_DEFINES}
Z3_TEST_SRC_DIR="${CMAKE_CURRENT_SOURCE_DIR}"
Z3_TEST_BIN_DIR="${PROJECT_BINARY_DIR}"
)
target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS})
target_include_directories(test-z3 PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
z3_append_linker_flag_list_to_target(test-z3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps})
add_dependencies(test-z3 shell)

31
src/test/tptp.cpp
View file

@ -2,6 +2,8 @@
#include <sstream>
#include <string>
#include <vector>
#include <cctype>
#include <iostream>
#include "util/debug.h"
#ifdef _WINDOWS
@ -20,16 +22,33 @@ struct tptp_case {
char const* expected_status;
};
constexpr unsigned tptp_buf_sz = 4096;
constexpr unsigned tptp_buffer_size = 4096;
static bool is_safe_file_name(char const* s) {
while (*s) {
unsigned char c = static_cast<unsigned char>(*s);
if (!(std::isalnum(c) || c == '.' || c == '-' || c == '_'))
return false;
++s;
}
return true;
}
static std::string run_tptp(char const* file) {
if (!is_safe_file_name(file)) {
std::cerr << "Unsafe TPTP test filename: " << file << "\n";
ENSURE(false);
}
std::ostringstream cmd;
cmd << "\"" << Z3_TEST_BIN_DIR << "/" << z3_bin_name << "\" -tptp "
<< "\"" << Z3_TEST_SRC_DIR << "/tptp/" << file << "\" 2>&1";
FILE* pipe = Z3_POPEN(cmd.str().c_str(), "r");
ENSURE(pipe != nullptr);
if (!pipe) {
std::cerr << "Failed to execute command: " << cmd.str() << "\n";
ENSURE(false);
}
std::string out;
char buffer[tptp_buf_sz];
char buffer[tptp_buffer_size];
while (fgets(buffer, sizeof(buffer), pipe))
out += buffer;
int code = Z3_PCLOSE(pipe);
@ -37,7 +56,11 @@ static std::string run_tptp(char const* file) {
if (WIFEXITED(code))
code = WEXITSTATUS(code);
#endif
ENSURE(code == 0);
if (code != 0) {
std::cerr << "TPTP command failed for file '" << file << "' with exit code " << code << "\n";
std::cerr << out << "\n";
ENSURE(false);
}
return out;
}