diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 005c90ecb..11652d06f 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2724,6 +2724,10 @@ def mk_config():
             SLIBFLAGS      = '-shared'
             EXE_EXT        = '.exe'
             LIB_EXT        = '.lib'
+        elif sysname  == 'AIX':
+            SO_EXT         = '.so'
+            SLIBFLAGS      = '-shared'
+            SLIBEXTRAFLAGS = '%s' % LDFLAGS
         else:
             raise MKException('Unsupported platform: %s' % sysname)
         if is64():
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;