From c390afa279eacd4e883478f039077f9a34aa053e Mon Sep 17 00:00:00 2001
From: Simon Sobisch <simonsobisch@web.de>
Date: Mon, 5 Jan 2026 16:23:05 +0100
Subject: [PATCH] AIX compat (#8113)

* fix name conflict for struct proc

* aix compat
---
 scripts/mk_util.py      | 4 ++++
 src/ast/occurs.cpp      | 6 +++---
 src/smt/uses_theory.cpp | 6 +++---
 src/test/trigo.cpp      | 4 ++++
 4 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 5245b4c3c..48cdb953a 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2714,6 +2714,10 @@ def mk_config():
             SO_EXT         = '.so'
             SLIBFLAGS      = '-shared'
             SLIBEXTRAFLAGS = '%s -mimpure-text' % SLIBEXTRAFLAGS
+        elif sysname  == 'AIX':
+            SO_EXT         = '.so'
+            SLIBFLAGS      = '-shared'
+            SLIBEXTRAFLAGS = '%s' % LDFLAGS
         elif sysname.startswith('CYGWIN'):
             SO_EXT         = '.dll'
             SLIBFLAGS      = '-shared'
diff --git a/src/ast/occurs.cpp b/src/ast/occurs.cpp
index 4e0008373..a79d201c8 100644
--- a/src/ast/occurs.cpp
+++ b/src/ast/occurs.cpp
@@ -30,12 +30,12 @@ Revision History:
 namespace {
     struct found {}; 
     
-    struct proc {
+    struct proc_z3 {
         expr * m_n;
 
 #define CHECK() { if (n == m_n) throw found(); }
 
-        proc(expr * n):m_n(n) {}
+        proc_z3(expr * n):m_n(n) {}
         void operator()(var const * n) { CHECK(); }
         void operator()(app const * n) { CHECK(); }
         void operator()(quantifier const * n) { CHECK(); }
@@ -63,7 +63,7 @@ namespace {
 
 // Return true if n1 occurs in n2
 bool occurs(expr * n1, expr * n2) {
-    proc p(n1);
+    proc_z3 p(n1);
     try {
         quick_for_each_expr(p, n2);
     }
diff --git a/src/smt/uses_theory.cpp b/src/smt/uses_theory.cpp
index 10e249aab..69bb86217 100644
--- a/src/smt/uses_theory.cpp
+++ b/src/smt/uses_theory.cpp
@@ -27,9 +27,9 @@ bool uses_theory(expr * n, family_id fid) {
 
 namespace {
     struct found {}; 
-    struct proc {
+    struct proc_z3 {
         family_id m_fid;
-        proc(family_id fid):m_fid(fid) {}
+        proc_z3(family_id fid):m_fid(fid) {}
         void operator()(var * n) {}
         void operator()(app * n) { if (n->get_family_id() == m_fid) throw found(); }
         void operator()(quantifier * n) {}
@@ -37,7 +37,7 @@ namespace {
 }
 
 bool uses_theory(expr * n, family_id fid, expr_mark & visited) {
-    proc p(fid);
+    proc_z3 p(fid);
     try {
         for_each_expr(p, visited, n);
     }
diff --git a/src/test/trigo.cpp b/src/test/trigo.cpp
index 380b66d81..3a3426ba6 100644
--- a/src/test/trigo.cpp
+++ b/src/test/trigo.cpp
@@ -92,6 +92,10 @@ static void tst_float_sine_core(std::ostream & out,
     out << "Sin[" << fm.to_rational_string(a) << "] <= " << fm.to_rational_string(hi) << "\n";
 }
 
+#ifdef SBITS
+#undef SBITS
+#endif
+
 const unsigned EBITS = 11;
 const unsigned SBITS = 53;