diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 625a8dc875..aee8fceccf 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -363,7 +363,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
     case OP_MUL:     return is_real ? m_r_mul_decl : m_i_mul_decl;
     case OP_DIV:     return m_r_div_decl;
     case OP_IDIV:    return m_i_div_decl;
-    case OP_IDIVIDES: UNREACHABLE(); 
+    case OP_IDIVIDES: Z3_unreachable_case(); 
     case OP_REM:     return m_i_rem_decl;
     case OP_MOD:     return m_i_mod_decl;
     case OP_DIV0:    return m_manager->mk_func_decl(symbol("/0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_DIV0));
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index edc4009b06..2ded7c1b3a 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -774,7 +774,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
     case PR_TRANSITIVITY_STAR:            return mk_proof_decl("trans*", k, num_parents, m_transitivity_star_decls);
     case PR_MONOTONICITY:                 return mk_proof_decl("monotonicity", k, num_parents, m_monotonicity_decls);
     case PR_QUANT_INTRO:                  return mk_proof_decl("quant-intro", k, 1, m_quant_intro_decl);
-    case PR_BIND:                         UNREACHABLE();
+    case PR_BIND:                         Z3_unreachable_case();
     case PR_DISTRIBUTIVITY:               return mk_proof_decl("distributivity", k, num_parents, m_distributivity_decls);
     case PR_AND_ELIM:                     return mk_proof_decl("and-elim", k, 1, m_and_elim_decl);
     case PR_NOT_OR_ELIM:                  return mk_proof_decl("not-or-elim", k, 1, m_not_or_elim_decl);
diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index 8947bae759..d90ca9dac1 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -328,7 +328,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
         SASSERT(to_app(args[0])->get_num_args() == num_args+1);
         switch (compare_args(num_args - 1, args+1, to_app(args[0])->get_args()+1)) {
         case l_true:
-            UNREACHABLE();
+            Z3_unreachable_case();
         case l_false: {
             expr* arg0 = to_app(args[0])->get_arg(0);
             while (m_util.is_store(arg0) && compare_args(num_args-1, args + 1, to_app(arg0)->get_args() + 1) == l_false) {
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 908f505893..0c86c949e7 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -780,7 +780,7 @@ namespace smt {
             case OP_DISTINCT:
                 throw default_exception(std::string("formula has not been simplified") + " : " + mk_pp(n, m));
             case OP_OEQ:
-                UNREACHABLE();
+                Z3_unreachable_case();
             default:
                 break;
             }
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 4b0b8378da..b068547339 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -123,7 +123,7 @@ sexpr * const * sexpr::get_children() const {
 void sexpr::display_atom(std::ostream & out) const {
     switch (get_kind()) {
     case sexpr::kind_t::COMPOSITE:
-        UNREACHABLE();
+        Z3_unreachable_case();
     case sexpr::kind_t::NUMERAL:
         out << static_cast<sexpr_numeral const *>(this)->m_val;
         break;
diff --git a/src/util/util.h b/src/util/util.h
index 34eec199bd..b4e8078d40 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -80,6 +80,12 @@ static_assert(sizeof(int64_t) == 8, "64 bits");
 # define Z3_fallthrough
 #endif
 
+// UNREACHABLE is not defined in a way that makes it clear to the compiler
+// that it does not return (because it calls INVOKE_DEBUGGER() in debug builds,
+// and that *may* return).  Using this for unreachable switch cases avoids
+// any fall-through warnings.
+#define Z3_unreachable_case() UNREACHABLE(); Z3_fallthrough
+
 static inline bool is_power_of_two(unsigned v) { return !(v & (v - 1)) && v; }
 
 /**