diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake
index 9e11d9082b..b9424e1b25 100644
--- a/cmake/compiler_warnings.cmake
+++ b/cmake/compiler_warnings.cmake
@@ -25,6 +25,7 @@ set(CLANG_ONLY_WARNINGS
   "-Winconsistent-missing-override"
   "-Wno-missing-field-initializers"
   "-Wcast-qual"
+  "-Wimplicit-fallthrough"
 )
 
 set(MSVC_WARNINGS "/W3")
diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp
index 219cea3f86..84079bf7c8 100644
--- a/src/ast/normal_forms/nnf.cpp
+++ b/src/ast/normal_forms/nnf.cpp
@@ -512,10 +512,12 @@ struct nnf::imp {
             fr.m_i = 1;
             if (!visit(t->get_arg(0), !fr.m_pol, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 1:
             fr.m_i = 2;
             if (!visit(t->get_arg(1), fr.m_pol, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         default:
             break;
         }
@@ -544,18 +546,22 @@ struct nnf::imp {
             fr.m_i = 1;
             if (!visit(t->get_arg(0), true, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 1:
             fr.m_i = 2;
             if (!visit(t->get_arg(0), false, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 2:
             fr.m_i = 3;
             if (!visit(t->get_arg(1), fr.m_pol, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 3:
             fr.m_i = 4;
             if (!visit(t->get_arg(2), fr.m_pol, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         default:
             break;
         }
@@ -589,18 +595,22 @@ struct nnf::imp {
             fr.m_i = 1;
             if (!visit(t->get_arg(0), true, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 1:
             fr.m_i = 2;
             if (!visit(t->get_arg(0), false, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 2:
             fr.m_i = 3;
             if (!visit(t->get_arg(1), true, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 3:
             fr.m_i = 4;
             if (!visit(t->get_arg(1), false, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         default:
             break;
         }
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index af45569b40..8aed5bf43a 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -103,6 +103,7 @@ br_status seq_rewriter::mk_bool_app(func_decl* f, unsigned n, expr* const* args,
     case OP_EQ:
         SASSERT(n == 2);
         // return mk_eq_helper(args[0], args[1], result);
+        Z3_fallthrough;
     default:
         return BR_FAILED;
     }
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 0eb204f19d..a47eb6ede6 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2479,6 +2479,7 @@ namespace lp {
             } 
             case GT:
                 y_of_bound += 1;
+                Z3_fallthrough;
             case GE: {
                 auto low = numeric_pair<mpq>(right_side.x, y_of_bound);
                 if (low < get_lower_bound(j)) {
diff --git a/src/muz/spacer/spacer_farkas_learner.cpp b/src/muz/spacer/spacer_farkas_learner.cpp
index 3016b69fe9..263cffadda 100644
--- a/src/muz/spacer/spacer_farkas_learner.cpp
+++ b/src/muz/spacer/spacer_farkas_learner.cpp
@@ -378,6 +378,7 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
                 INSERT(res);
                 b_closed.mark(p, true);
             }
+            break;
         }
         default:
             break;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index b3a1661d67..06b2a60a56 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -650,6 +650,7 @@ namespace opt {
         switch (obj.m_type) {
         case O_MINIMIZE:
             is_ge = !is_ge;
+            Z3_fallthrough;
         case O_MAXIMIZE:
             val = (*mdl)(obj.m_term);
             if (is_numeral(val, k)) {
diff --git a/src/parsers/util/scanner.cpp b/src/parsers/util/scanner.cpp
index a10c50150e..c30543ba1b 100644
--- a/src/parsers/util/scanner.cpp
+++ b/src/parsers/util/scanner.cpp
@@ -124,6 +124,7 @@ scanner::token scanner::read_id(char first_char) {
             if (!is_alpha || ch != '-') {
                 goto bail_out;  
             }
+            Z3_fallthrough;
         case 'a':
         case ':':
         case '.':
diff --git a/src/sat/smt/pb_card.cpp b/src/sat/smt/pb_card.cpp
index eaa994b677..f88ae499fd 100644
--- a/src/sat/smt/pb_card.cpp
+++ b/src/sat/smt/pb_card.cpp
@@ -51,7 +51,9 @@ namespace pb {
         double to_add = do_add ? 0 : 1;
         for (literal l : *this) {
             switch (s.value(l)) {
-            case l_true:  --k; if (k == 0) return 0;
+            case l_true:
+                --k; if (k == 0) return 0;
+                Z3_fallthrough;
             case l_undef:
                 if (do_add) to_add += literal_occs(l);
                 ++slack; break;
diff --git a/src/sat/smt/pb_pb.cpp b/src/sat/smt/pb_pb.cpp
index a2cb20a895..a718e9ebde 100644
--- a/src/sat/smt/pb_pb.cpp
+++ b/src/sat/smt/pb_pb.cpp
@@ -95,7 +95,9 @@ namespace pb {
             literal l = wl.second;
             unsigned w = wl.first;
             switch (s.value(l)) {
-            case l_true:  if (k <= w) return 0;
+            case l_true:
+                if (k <= w) return 0;
+                Z3_fallthrough;
             case l_undef:
                 if (do_add) to_add += occs(l);
                 ++undefs;
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 0e6d88b1a1..f85f747ffa 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -96,7 +96,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_euf = sp.euf() || sp.smt();
     }
 
-    void throw_op_not_handled(std::string const& s) {
+    [[noreturn]] void throw_op_not_handled(std::string const& s) {
         std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator";
         throw tactic_exception(std::move(s0));
     }
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 2c352a6a25..123f40978c 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -2460,6 +2460,7 @@ namespace smt {
         case QUASI_BASE:
             quasi_base_row2base_row(get_var_row(v));
             SASSERT(get_var_kind(v) == BASE);
+            Z3_fallthrough;
         case BASE:
             if (!m_to_patch.contains(v) && get_value(v) < k) {
                 TRACE(to_patch_bug, tout << "need to be patched (assert_lower): "; display_var(tout, v););
@@ -2508,6 +2509,7 @@ namespace smt {
         case QUASI_BASE:
             quasi_base_row2base_row(get_var_row(v));
             SASSERT(get_var_kind(v) == BASE);
+            Z3_fallthrough;
         case BASE:
             if (!m_to_patch.contains(v) && get_value(v) > k) {
                 TRACE(to_patch_bug, tout << "need to be patched (assert upper): "; display_var(tout, v););
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 40c2cec2ae..e0e2b1ea51 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -2116,6 +2116,7 @@ namespace smt {
             switch(ctx.get_assignment(c.lit(i))) {
             case l_true:
                 ++sum;
+                Z3_fallthrough;
             case l_undef:
                 ++maxsum;
                 break;
@@ -2147,6 +2148,7 @@ namespace smt {
             switch(ctx.get_assignment(c.lit(i))) {
             case l_true:
                 sum += c.coeff(i);
+                Z3_fallthrough;
             case l_undef:
                 maxsum += c.coeff(i);
                 break;
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index fc165b009a..a0b7d05382 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -480,6 +480,7 @@ struct aig_manager::imp {
                     case OP_EQ:
                         if (!m.m().is_bool(tapp->get_arg(0)))
                             break;
+                        Z3_fallthrough;
                     case OP_NOT:
                     case OP_OR:      
                     case OP_AND:
@@ -1272,10 +1273,12 @@ struct aig_manager::imp {
                     fr.m_idx++;
                     if (!visit(left(n)))
                         goto start;
+                    Z3_fallthrough;
                 case 1:
                     fr.m_idx++;
                     if (!visit(right(n)))
                         goto start;
+                    Z3_fallthrough;
                 default:
                     if (!is_cached(n))
                         improve_sharing(n);
diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp
index 85d9acd9a0..3e2596e9f6 100644
--- a/src/tactic/arith/probe_arith.cpp
+++ b/src/tactic/arith/probe_arith.cpp
@@ -135,7 +135,7 @@ struct has_nlmul {
     arith_util   a;
     has_nlmul(ast_manager& m):m(m), a(m) {}
     
-    void throw_found(expr* e) {
+    [[noreturn]] void throw_found(expr* e) {
         TRACE(probe, tout << expr_ref(e, m) << ": " << sort_ref(e->get_sort(), m) << "\n";);
         throw found();
     }
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 7aecd4d505..0d836bf4d5 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -763,6 +763,7 @@ class elim_uncnstr_tactic : public tactic {
                     }
                     return r;
                 }
+                return nullptr;
             default:
                 return nullptr;
             }
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index ba396a7565..886a603cd7 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -95,7 +95,7 @@ class tseitin_cnf_tactic : public tactic {
         
         void push_frame(app * n) { m_frame_stack.push_back(frame(n)); }
         
-        void throw_op_not_handled() {
+        [[noreturn]] void throw_op_not_handled() {
             throw tactic_exception("operator not supported, apply simplifier before invoking this strategy");
         }
         
diff --git a/src/util/debug.h b/src/util/debug.h
index 4be061e562..481d46e1a8 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -92,10 +92,16 @@ bool is_debug_enabled(const char * tag);
         INVOKE_DEBUGGER();                                                       \
     })
 
-#ifdef Z3DEBUG
-# define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER();)
+#ifdef __clang__
+#define __compiler_unreachable __builtin_unreachable()
 #else
-# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0)
+#define __compiler_unreachable
+#endif
+
+#ifdef Z3DEBUG
+# define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER(); __compiler_unreachable;)
+#else
+# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); invoke_exit_action(ERR_UNREACHABLE); }; __compiler_unreachable
 #endif
 
 #ifdef Z3DEBUG