diff --git a/regression/cbmc-java/exceptions25/main.c b/regression/cbmc-java/exceptions25/main.c
new file mode 100644
index 00000000000..ab24eded4f8
--- /dev/null
+++ b/regression/cbmc-java/exceptions25/main.c
@@ -0,0 +1,7 @@
+int main(void)
+{
+  int x;
+  __CPROVER_assume(x < 10);
+  __CPROVER_assert(x != 0, "");
+  return 0;
+}
diff --git a/regression/cbmc-java/exceptions25/test.desc b/regression/cbmc-java/exceptions25/test.desc
new file mode 100644
index 00000000000..f8823e7d524
--- /dev/null
+++ b/regression/cbmc-java/exceptions25/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+--
+^warning: ignoring
+--
+When compiling CBMC with -DDEBUG uncaught exception analysis prints an
+exceptions map per function.  This test ensures that meta-functions which are
+replaced by explicit GOTO instructions (e.g. __CPROVER_assert, __CPROVER_assume)
+and thus do not occur as explicit function calls in the final GOTO program are
+handled correctly.
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp
index 4b0674c375d..dfd0d9a51ca 100644
--- a/src/analyses/uncaught_exceptions_analysis.cpp
+++ b/src/analyses/uncaught_exceptions_analysis.cpp
@@ -193,9 +193,11 @@ void uncaught_exceptions_analysist::output(
   {
     const auto fn=it->first;
     const exceptions_mapt::const_iterator found=exceptions_map.find(fn);
-    INVARIANT(
-      found!=exceptions_map.end(),
-      "each function expected to be recorded in `exceptions_map`");
+    // Functions like __CPROVER_assert and __CPROVER_assume are replaced by
+    // explicit GOTO instructions and will not show up in exceptions_map.
+    if(found==exceptions_map.end())
+      continue;
+
     const auto &fs=found->second;
     if(!fs.empty())
     {