diff --git a/src/ast/ast.h b/src/ast/ast.h
index 03713ee4b8..4c68fdcea7 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -47,6 +47,7 @@ Revision History:
 #include "util/z3_exception.h"
 #include "util/dependency.h"
 #include "util/rlimit.h"
+#include "util/manage_warnings.h"
 #include <variant>
 #include <span>
 #include <initializer_list>
@@ -2168,6 +2169,7 @@ public:
 
 public:
 
+    START_DISABLE_EXTRA_SEMI_WARNING;
     MATCH_UNARY(is_not);
     MATCH_BINARY(is_eq);
     MATCH_BINARY(is_implies);
@@ -2176,6 +2178,7 @@ public:
     MATCH_BINARY(is_xor);
     MATCH_TERNARY(is_and);
     MATCH_TERNARY(is_or);
+    END_DISABLE_WARNING;
 
     bool is_iff(expr const* n, expr*& lhs, expr*& rhs) const { return is_eq(n, lhs, rhs) && is_bool(lhs); } 
 
@@ -2311,9 +2314,11 @@ public:
     bool is_apply_def(expr const * e) const { return is_app_of(e, basic_family_id, PR_APPLY_DEF); }
     bool is_skolemize(expr const * e) const { return is_app_of(e, basic_family_id, PR_SKOLEMIZE); }
 
+    START_DISABLE_EXTRA_SEMI_WARNING;
     MATCH_UNARY(is_asserted);
     MATCH_UNARY(is_hypothesis);
     MATCH_UNARY(is_lemma);
+    END_DISABLE_WARNING;
 
     bool has_fact(proof const * p) const {
         SASSERT(is_proof(p));
diff --git a/src/util/manage_warnings.h b/src/util/manage_warnings.h
new file mode 100644
index 0000000000..adc6059646
--- /dev/null
+++ b/src/util/manage_warnings.h
@@ -0,0 +1,60 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    build_warnings.h
+
+Abstract:
+
+    Macros to control compiler build warnings.
+
+Author:
+
+    Dave Detlefs 2026-07-20.
+
+Revision History:
+
+--*/
+#pragma once
+
+// #define PRAGMA_MACRO(s) _Pragma(s)
+
+// In some cases, we wish to be able to terminate macros with semicolons,
+// even when the semi is (strictly speaking) illegal when following the
+// expansion of the macro.  (The macro invocations can look like function
+// invocations to some IDE's, and the lack of a trailing semi can confuse them.)
+// In those cases, we add this DUMMY_DECL to the macro; it "consumes" the trailing
+// semi, making it legal.
+
+// Standard preprocessor concatenation gymnastics
+#define CONCAT_IMPL(x, y) x##y
+#define CONCAT(x, y) CONCAT_IMPL(x, y)
+
+#define DUMMY_DECL using CONCAT(__dummy_decl_, __COUNTER__) = int
+
+#define DO_PRAGMA(x) _Pragma(#x)
+
+#ifdef __clang__
+
+#define START_DISABLE_WARNING(s)		\
+  _Pragma("clang diagnostic push")		\
+  DO_PRAGMA(clang diagnostic ignored #s)
+
+
+#define END_DISABLE_WARNING			\
+  _Pragma("clang diagnostic pop")		\
+  DUMMY_DECL
+
+#define START_DISABLE_EXTRA_SEMI_WARNING START_DISABLE_WARNING(-Wextra-semi)
+
+#else
+
+#define START_DISABLE_EXTRA_SEMI_WARNING
+#define END_DISABLE_WARNING
+
+#endif
+
+
+
+