diff --git a/COMPILING.md b/COMPILING.md
index 058cfc5909b..99aeca0917d 100644
--- a/COMPILING.md
+++ b/COMPILING.md
@@ -1,4 +1,4 @@
-#WHAT ARCHITECTURE ?
+# What architecture?
 
 CPROVER now needs a C++11 compliant compiler and is known to work in the
 following environments:
@@ -18,7 +18,7 @@ past, but are not actively tested:
 - Solaris 11
 - FreeBSD 11
 
-#Building using CMake
+# Building using CMake
 
 Building with CMake is supported across Linux, MacOS X and Windows with Visual
 Studio 2019. There are also hand-written make files which can be used to build
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 5048c5ae92b..a4ca9ecacba 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -166,10 +166,19 @@ void goto_convert_functionst::convert_function(
   // we have a body, make sure all parameter names are valid
   for(const auto &p : f.parameter_identifiers)
   {
-    DATA_INVARIANT(!p.empty(), "parameter identifier should not be empty");
-    DATA_INVARIANT(
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      !p.empty(),
+      "parameter identifier should not be empty",
+      "function:",
+      identifier);
+
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
       symbol_table.has_symbol(p),
-      "parameter identifier must be a known symbol");
+      "parameter identifier must be a known symbol",
+      "function:",
+      identifier,
+      "parameter:",
+      p);
   }
 
   lifetimet parent_lifetime = lifetime;