diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 840222e89..111f1df78 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -516,7 +516,7 @@ inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_v
         switch (size) {
         case 2:
             b += array[1]->hash();
-            __fallthrough;
+            Z3_fallthrough;
         case 1:
             c += array[0]->hash();
         }
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 1115663d2..fd7c60a57 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -1500,7 +1500,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
             result = m_util.mk_bv_not(new_args[1]);
             return BR_DONE;
         }
-        __fallthrough;
+        Z3_fallthrough;
     default:
         if (m_bv_sort_ac)
             std::sort(new_args.begin(), new_args.end(), ast_to_lt());
diff --git a/src/smt/smt_almost_cg_table.cpp b/src/smt/smt_almost_cg_table.cpp
index 93f136aad..66eb8c533 100644
--- a/src/smt/smt_almost_cg_table.cpp
+++ b/src/smt/smt_almost_cg_table.cpp
@@ -67,7 +67,7 @@ namespace smt {
             switch (num_args) {
             case 2:
                 b += arg_hash(n, 1);
-                __fallthrough;
+                Z3_fallthrough;
             case 1:
                 c += arg_hash(n, 0);
             }
diff --git a/src/smt/smt_cg_table.cpp b/src/smt/smt_cg_table.cpp
index ed36384c1..83d137ff0 100644
--- a/src/smt/smt_cg_table.cpp
+++ b/src/smt/smt_cg_table.cpp
@@ -127,7 +127,7 @@ namespace smt {
         switch (i) {
         case 2:
             b += n->get_arg(1)->get_root()->hash();
-            __fallthrough;
+            Z3_fallthrough;
         case 1:
             c += n->get_arg(0)->get_root()->hash();
         }
diff --git a/src/util/hash.cpp b/src/util/hash.cpp
index bb5ca0a41..42ba3f4da 100644
--- a/src/util/hash.cpp
+++ b/src/util/hash.cpp
@@ -52,38 +52,38 @@ unsigned string_hash(const char * str, unsigned length, unsigned init_value) {
     switch(len) {        /* all the case statements fall through */
     case 11: 
         c+=((unsigned)str[10]<<24);
-        __fallthrough;
+        Z3_fallthrough;
     case 10: 
         c+=((unsigned)str[9]<<16);
-        __fallthrough;
+        Z3_fallthrough;
     case 9 : 
         c+=((unsigned)str[8]<<8);
-        __fallthrough;
+        Z3_fallthrough;
         /* the first byte of c is reserved for the length */
     case 8 : 
         b+=((unsigned)str[7]<<24);
-        __fallthrough;
+        Z3_fallthrough;
     case 7 : 
         b+=((unsigned)str[6]<<16);
-        __fallthrough;
+        Z3_fallthrough;
     case 6 : 
         b+=((unsigned)str[5]<<8);
-        __fallthrough;
+        Z3_fallthrough;
     case 5 : 
         b+=str[4];
-        __fallthrough;
+        Z3_fallthrough;
     case 4 : 
         a+=((unsigned)str[3]<<24);
-        __fallthrough;
+        Z3_fallthrough;
     case 3 : 
         a+=((unsigned)str[2]<<16);
-        __fallthrough;
+        Z3_fallthrough;
     case 2 : 
         a+=((unsigned)str[1]<<8);
-        __fallthrough;
+        Z3_fallthrough;
     case 1 : 
         a+=str[0];
-        __fallthrough;
+        Z3_fallthrough;
         /* case 0: nothing left to add */
     }
     mix(a,b,c);
diff --git a/src/util/hash.h b/src/util/hash.h
index 59bc2cc3b..82d343661 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -22,10 +22,6 @@ Revision History:
 #include<algorithm>
 #include"util.h"
 
-#ifndef __fallthrough
-#define __fallthrough
-#endif
-
 #define mix(a,b,c)              \
 {                               \
   a -= b; a -= c; a ^= (c>>13); \
@@ -116,7 +112,7 @@ unsigned get_composite_hash(Composite app, unsigned n, GetKindHashProc const & k
         switch (n) {
         case 2:
             b += chasher(app, 1);
-            __fallthrough;
+            Z3_fallthrough;
         case 1:
             c += chasher(app, 0);
         }
diff --git a/src/util/util.h b/src/util/util.h
index 2e7e860d7..f97f5c1f9 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -68,6 +68,18 @@ COMPILE_TIME_ASSERT(sizeof(int64) == 8);
 #define THREAD_LOCAL 
 #endif
 
+#ifdef __fallthrough
+# define Z3_fallthrough __fallthrough
+#elif defined(__has_cpp_attribute)
+# if __has_cpp_attribute(clang::fallthrough)
+#  define Z3_fallthrough [[clang::fallthrough]]
+# else
+#  define Z3_fallthrough
+# endif
+#else
+# define Z3_fallthrough
+#endif
+
 inline bool is_power_of_two(unsigned v) { return !(v & (v - 1)) && v; }
 
 /**
@@ -273,10 +285,6 @@ bool has_duplicates(const IT & begin, const IT & end) {
     return false;
 }
 
-#ifndef __fallthrough
-#define __fallthrough
-#endif
-
 #ifndef _WINDOWS
 #ifndef __declspec
 #define __declspec(X)