From b4ddfd32eadf5e1e935c54b561ff4907ba057960 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 12 May 2026 23:00:14 +0000
Subject: [PATCH] Fix missing g_display_* symbol definitions for non-shell link
 targets

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/0283d958-26a8-4b1c-86be-b75a5bc26d8c

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/cmd_context/tptp_frontend.cpp | 4 ++--
 src/shell/main.cpp                | 4 ++--
 src/test/tptp.cpp                 | 7 ++++---
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index 46812d633..8ab66ac1d 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -19,8 +19,8 @@
 #include "util/rational.h"
 #include "util/z3_exception.h"
 
-extern bool g_display_statistics;
-extern bool g_display_model;
+bool g_display_statistics = false;
+bool g_display_model = false;
 
 namespace {
 
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 14e4cff13..9a4cd6f27 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -50,8 +50,8 @@ static char const * g_input_file          = nullptr;
 static char const * g_drat_input_file     = nullptr;
 static bool         g_standard_input      = false;
 static input_kind   g_input_kind          = IN_UNSPECIFIED;
-bool                g_display_statistics  = false;
-bool                g_display_model       = false;
+extern bool         g_display_statistics;
+extern bool         g_display_model;
 static bool         g_display_istatistics = false;
 
 static void error(const char * msg) {
diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp
index 6f59eca14..2ae2fb4f6 100644
--- a/src/test/tptp.cpp
+++ b/src/test/tptp.cpp
@@ -34,11 +34,12 @@ static std::string run_tptp(char const* input) {
     return out;
 }
 
-// Required externs from shell/tptp_frontend.cpp; keep output minimal in tests.
-bool g_display_statistics = false;
-bool g_display_model = false;
+extern bool g_display_statistics;
+extern bool g_display_model;
 
 void tst_tptp() {
+    g_display_statistics = false;
+    g_display_model = false;
     std::vector<tptp_case> cases = {
         {"agatha-butler",
 R"(fof(ax1,axiom, lives(agatha)).