From 6ec2d4bc8dc3d199854a7d1e4b6eac05eafe2325 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Fri, 16 Jan 2026 19:54:31 -0800
Subject: [PATCH] Replace fall-through comments with Z3_fallthrough macro
 (#8219)

* Initial plan

* Fix switch fall-through warnings with Z3_fallthrough attribute

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/muz/clp/clp_context.cpp  | 2 +-
 src/smt/diff_logic.h         | 2 +-
 src/smt/smt_context.cpp      | 2 +-
 src/smt/smt_internalizer.cpp | 1 -
 src/smt/theory_pb.cpp        | 2 +-
 5 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp
index 9d4baa4ae..ccaf46702 100644
--- a/src/muz/clp/clp_context.cpp
+++ b/src/muz/clp/clp_context.cpp
@@ -175,7 +175,7 @@ namespace datalog {
                     switch(search(depth-1, index+1)) {
                     case l_undef:
                         status = l_undef;
-                        // fallthrough
+                        Z3_fallthrough;
                     case l_false:
                         m_goals.resize(num_goals);   
                         break;
diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index 7683d8316..6cac49178 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -1884,7 +1884,7 @@ public:
                 switch(m_mark[w]) {
                 case DL_UNMARKED:
                     m_visited.push_back(w);
-                    // fall through
+                    Z3_fallthrough;
                 case DL_PROCESSED:
                     m_mark[w] = DL_FOUND;
                     m_heap.insert(w);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 9b861471e..8556a1607 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2545,7 +2545,7 @@ namespace smt {
                 break;
             case l_true:
                 is_taut = true;
-                // fallthrough
+                Z3_fallthrough;
             case l_undef:
                 if (i != j) {
                     cls.swap_lits(i, j);
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 30dfa2e8c..dccce78a0 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1163,7 +1163,6 @@ namespace smt {
                     simp_lits.push_back(~curr);
                 }
                 break; // ignore literal                
-                // fall through
             case l_undef:
                 if (curr == ~prev)
                     return false; // clause is equivalent to true
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 196f370c4..e340b0f0d 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -552,7 +552,7 @@ namespace smt {
         switch (is_true) {
         case l_false: 
             lit.neg();
-            // fall-through
+            Z3_fallthrough;
         case l_true: 
             ctx.mk_th_axiom(get_id(), 1, &lit);
             return true;