From 21b3f72b367624831f65bbba6f27cd43ba6d31bf Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 11 May 2026 06:58:02 +0000
Subject: [PATCH] Adjust Agatha TPTP expectation and tidy test helper constant

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

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/test/tptp.cpp             | 6 ++++--
 src/test/tptp/agatha-butler.p | 3 +--
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp
index a374401db..f1558a08d 100644
--- a/src/test/tptp.cpp
+++ b/src/test/tptp.cpp
@@ -20,6 +20,8 @@ struct tptp_case {
     char const* expected_status;
 };
 
+constexpr unsigned tptp_buf_sz = 4096;
+
 static std::string run_tptp(char const* file) {
     std::ostringstream cmd;
     cmd << "\"" << Z3_TEST_BIN_DIR << "/" << z3_bin_name << "\" -tptp "
@@ -27,7 +29,7 @@ static std::string run_tptp(char const* file) {
     FILE* pipe = Z3_POPEN(cmd.str().c_str(), "r");
     ENSURE(pipe != nullptr);
     std::string out;
-    char buffer[4096];
+    char buffer[tptp_buf_sz];
     while (fgets(buffer, sizeof(buffer), pipe))
         out += buffer;
     int code = Z3_PCLOSE(pipe);
@@ -41,7 +43,7 @@ static std::string run_tptp(char const* file) {
 
 void tst_tptp() {
     std::vector<tptp_case> cases = {
-        {"agatha-butler.p", "% SZS status CounterSatisfiable"},
+        {"agatha-butler.p", "% SZS status Theorem"},
         {"socrates-theorem.p", "% SZS status Theorem"},
         {"simple-sat.p", "% SZS status Satisfiable"}
     };
diff --git a/src/test/tptp/agatha-butler.p b/src/test/tptp/agatha-butler.p
index d5bbded75..c9a875989 100644
--- a/src/test/tptp/agatha-butler.p
+++ b/src/test/tptp/agatha-butler.p
@@ -15,5 +15,4 @@ fof(ax11,axiom, ! [X] : (? [Y] : ~ hates(X,Y))).
 fof(ax12,axiom, agatha != butler).
 fof(ax13,axiom, ? [X] : killed(X,agatha)).
 
-fof(conj,conjecture, killed(agatha,agatha)).
-
+fof(conj,conjecture, ~ killed(butler,agatha)).