diff --git a/src/util/hash.h b/src/util/hash.h
index a8d63f0d6..ac6896bf1 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -36,7 +36,7 @@ Revision History:
   c -= a; c -= b; c ^= (b>>15); \
 }
 
-inline unsigned hash_u(unsigned a) {
+static inline unsigned hash_u(unsigned a) {
    a = (a+0x7ed55d16) + (a<<12);
    a = (a^0xc761c23c) ^ (a>>19);
    a = (a+0x165667b1) + (a<<5);
@@ -46,7 +46,7 @@ inline unsigned hash_u(unsigned a) {
    return a;
 }
 
-inline unsigned hash_ull(unsigned long long a) {
+static inline unsigned hash_ull(unsigned long long a) {
   a  = (~a) + (a << 18); 
   a ^= (a >> 31);
   a += (a << 2) + (a << 4);
@@ -56,25 +56,25 @@ inline unsigned hash_ull(unsigned long long a) {
   return static_cast<unsigned>(a);
 }
 
-inline unsigned combine_hash(unsigned h1, unsigned h2) {
+static inline unsigned combine_hash(unsigned h1, unsigned h2) {
     h2 -= h1; h2 ^= (h1 << 8);
     h1 -= h2; h2 ^= (h1 << 16);
     h2 -= h1; h2 ^= (h1 << 10);
     return h2;
 }
 
-inline unsigned hash_u_u(unsigned a, unsigned b) {
+static inline unsigned hash_u_u(unsigned a, unsigned b) {
     return combine_hash(hash_u(a), hash_u(b));
 }
 
 unsigned string_hash(std::string_view str, unsigned init_value);
 
-inline unsigned unsigned_ptr_hash(std::span<unsigned const> vec, unsigned init_value) {
+static inline unsigned unsigned_ptr_hash(std::span<unsigned const> vec, unsigned init_value) {
     return string_hash(std::string_view(reinterpret_cast<char const*>(vec.data()), vec.size() * sizeof(unsigned)), init_value);
 }
 
 // Backward compatibility overload
-inline unsigned unsigned_ptr_hash(unsigned const* vec, unsigned len, unsigned init_value) {
+static inline unsigned unsigned_ptr_hash(unsigned const* vec, unsigned len, unsigned init_value) {
     return unsigned_ptr_hash(std::span<unsigned const>(vec, len), init_value);
 }
 
@@ -251,7 +251,7 @@ struct ptr_hash {
     }
 };
 
-inline unsigned mk_mix(unsigned a, unsigned b, unsigned c) {
+static inline unsigned mk_mix(unsigned a, unsigned b, unsigned c) {
     mix(a, b, c);
     return c;
 }
diff --git a/src/util/sign.h b/src/util/sign.h
index 8352300ec..5221b3f68 100644
--- a/src/util/sign.h
+++ b/src/util/sign.h
@@ -18,7 +18,7 @@ Author:
 #pragma once
 
 typedef enum { sign_neg = -1, sign_zero = 0, sign_pos = 1} sign;
-inline sign operator-(sign s) { switch (s) { case sign_neg: return sign_pos; case sign_pos: return sign_neg; default: return sign_zero; } };
-inline sign to_sign(int s) { return s == 0 ? sign_zero : (s > 0 ? sign_pos : sign_neg); }
-inline sign operator*(sign a, sign b) { return to_sign((int)a * (int)b); }
-inline bool is_zero(sign s) { return s == sign_zero; }
+static inline sign operator-(sign s) { switch (s) { case sign_neg: return sign_pos; case sign_pos: return sign_neg; default: return sign_zero; } };
+static inline sign to_sign(int s) { return s == 0 ? sign_zero : (s > 0 ? sign_pos : sign_neg); }
+static inline sign operator*(sign a, sign b) { return to_sign((int)a * (int)b); }
+static inline bool is_zero(sign s) { return s == sign_zero; }
diff --git a/src/util/tptr.h b/src/util/tptr.h
index 99abe34a7..20c2d6454 100644
--- a/src/util/tptr.h
+++ b/src/util/tptr.h
@@ -44,17 +44,17 @@ Revision History:
 #define UNBOXINT(PTR) static_cast<int>(reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT)
 
 template <typename U, typename T>
-U unbox(T* ptr) {
+inline U unbox(T* ptr) {
     return static_cast<U>(reinterpret_cast<std::uintptr_t>(ptr) >> PTR_ALIGNMENT);
 }
 
 template <typename T>
-unsigned get_tag(T* ptr) {
+inline unsigned get_tag(T* ptr) {
     return reinterpret_cast<std::uintptr_t>(ptr) & TAG_MASK;
 }
 
 template <typename T, typename U>
-T* box(U val, std::uintptr_t tag = 0) {
+inline T* box(U val, std::uintptr_t tag = 0) {
     static_assert( sizeof(T*) >= sizeof(U) + PTR_ALIGNMENT );
     SASSERT_EQ(tag & PTR_MASK, 0);
     T* ptr = reinterpret_cast<T*>((static_cast<std::uintptr_t>(val) << PTR_ALIGNMENT) | tag);
diff --git a/src/util/util.h b/src/util/util.h
index 84584f187..4b5af2b52 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -80,14 +80,14 @@ static_assert(sizeof(int64_t) == 8, "64 bits");
 # define Z3_fallthrough
 #endif
 
-inline bool is_power_of_two(unsigned v) { return !(v & (v - 1)) && v; }
+static inline bool is_power_of_two(unsigned v) { return !(v & (v - 1)) && v; }
 
 /**
    \brief Return the next power of two that is greater than or equal to v.
    
    \warning This function returns 0 for v == 0.
 */
-inline unsigned next_power_of_two(unsigned v) {
+static inline unsigned next_power_of_two(unsigned v) {
     v--;
     v |= v >> 1;
     v |= v >> 2;