diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 27d8b97a5..d24823c65 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -459,7 +459,7 @@ public:
                     name n = read_name(d);
                     return mk_metavar(n, read_local_context(d));
                 }}
-                lean_unreachable(); // LCOV_EXCL_LINE
+                throw_corrupted_file();
             });
     }
 };
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index efb5f4464..bb8924620 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -308,7 +308,7 @@ public:
                     }
                     return max_core(lvls.size(), lvls.data());
                 }}
-                lean_unreachable();
+                throw_corrupted_file();
             });
     }
 };
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 1f380f6d2..fb229fd6a 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -404,7 +404,7 @@ public:
                     name prefix = read();
                     return name(prefix, d.read_unsigned());
                 }}
-                lean_unreachable(); // LCOV_EXCL_LINE
+                throw_corrupted_file();
             });
     }
 };
diff --git a/src/util/object_serializer.h b/src/util/object_serializer.h
index c111de4af..34b5a8e10 100644
--- a/src/util/object_serializer.h
+++ b/src/util/object_serializer.h
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 #include <unordered_map>
 #include <vector>
-#include "util/exception.h"
 #include "util/serializer.h"
 
 #ifndef LEAN_OBJECT_SERIALIZER_BUCKET_SIZE
@@ -62,7 +61,7 @@ public:
         } else {
             unsigned i = d.read_unsigned();
             if (i >= m_table.size())
-                throw exception("corrupted binary file");
+                throw_corrupted_file();
             return m_table[i];
         }
     }
diff --git a/src/util/serializer.cpp b/src/util/serializer.cpp
index c914ba0f0..d6c16fe87 100644
--- a/src/util/serializer.cpp
+++ b/src/util/serializer.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <stdio.h>
 #include <ios>
 #include "util/serializer.h"
+#include "util/exception.h"
 
 namespace lean {
 void serializer_core::write_unsigned(unsigned i) {
@@ -69,4 +70,8 @@ double deserializer_core::read_double() {
     in >> r;
     return r;
 }
+
+void throw_corrupted_file() {
+    throw exception("corrupted binary file");
+}
 }
diff --git a/src/util/serializer.h b/src/util/serializer.h
index 8e4e48559..61e06335b 100644
--- a/src/util/serializer.h
+++ b/src/util/serializer.h
@@ -63,4 +63,6 @@ inline deserializer & operator>>(deserializer & d, int & i) { i = d.read_int();
 inline deserializer & operator>>(deserializer & d, char & c) { c = d.read_char(); return d; }
 inline deserializer & operator>>(deserializer & d, bool & b) { b = d.read_bool(); return d; }
 inline deserializer & operator>>(deserializer & d, double & b) { b = d.read_double(); return d; }
+
+[[ noreturn ]] void throw_corrupted_file();
 }
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp
index 23dee703c..6c0ce4f0d 100644
--- a/src/util/sexpr/sexpr.cpp
+++ b/src/util/sexpr/sexpr.cpp
@@ -336,7 +336,7 @@ public:
                     sexpr t = read();
                     return sexpr(h, t);
                 }}
-                lean_unreachable();
+                throw_corrupted_file();
             });
     }
 };