diff --git a/regression/crangler/loop-invariant-01/main.c b/regression/crangler/loop-invariant-01/main.c
new file mode 100644
index 00000000000..b2f019df0df
--- /dev/null
+++ b/regression/crangler/loop-invariant-01/main.c
@@ -0,0 +1,27 @@
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+
+  for(int i = 0; i < 2; i++)
+  {
+    arr[i] = 0;
+  }
+
+  int i = 0;
+  while(i < 2)
+  {
+    arr[i] = 0;
+    i++;
+  }
+
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}
diff --git a/regression/crangler/loop-invariant-01/test.desc b/regression/crangler/loop-invariant-01/test.desc
new file mode 100644
index 00000000000..27a51043cc2
--- /dev/null
+++ b/regression/crangler/loop-invariant-01/test.desc
@@ -0,0 +1,10 @@
+CORE
+test.json
+
+^\s+while\(i \< 2\) \_\_CPROVER\_loop\_invariant
+^EXIT=0$
+^SIGNAL=0$
+--
+^\s+for\(int i = 0; i \< 2; i\+\+\) \_\_CPROVER
+--
+Annotate loop invariant only to the for-loop.
diff --git a/regression/crangler/loop-invariant-01/test.json b/regression/crangler/loop-invariant-01/test.json
new file mode 100644
index 00000000000..5451a5c3850
--- /dev/null
+++ b/regression/crangler/loop-invariant-01/test.json
@@ -0,0 +1,13 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "while 1 invariant 1==1"
+      ]
+    }
+  ],
+  "output": "stdout"
+}
diff --git a/regression/crangler/loop-invariant-02/main.c b/regression/crangler/loop-invariant-02/main.c
new file mode 100644
index 00000000000..a0b723e699f
--- /dev/null
+++ b/regression/crangler/loop-invariant-02/main.c
@@ -0,0 +1,26 @@
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  for(int i = 0; i < 2; i++)
+  {
+    arr[i] = 0;
+  }
+
+  int i = 0;
+  while(i < 2)
+  {
+    arr[i] = 0;
+    i++;
+  }
+
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}
diff --git a/regression/crangler/loop-invariant-02/test.desc b/regression/crangler/loop-invariant-02/test.desc
new file mode 100644
index 00000000000..644520896f1
--- /dev/null
+++ b/regression/crangler/loop-invariant-02/test.desc
@@ -0,0 +1,10 @@
+CORE
+test.json
+
+^\s+for\(int i = 0; i \< 2; i\+\+\) \_\_CPROVER\_loop\_invariant
+^EXIT=0$
+^SIGNAL=0$
+--
+^\s+while\(i \< 2\) \_\_CPROVER
+--
+Annotate loop invariant only to the while-loop.
diff --git a/regression/crangler/loop-invariant-02/test.json b/regression/crangler/loop-invariant-02/test.json
new file mode 100644
index 00000000000..fad9df457b8
--- /dev/null
+++ b/regression/crangler/loop-invariant-02/test.json
@@ -0,0 +1,13 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "for 1 invariant 1==1"
+      ]
+    }
+  ],
+  "output": "stdout"
+}
diff --git a/src/crangler/c_wrangler.cpp b/src/crangler/c_wrangler.cpp
index a92e610caa9..e62a35243b6 100644
--- a/src/crangler/c_wrangler.cpp
+++ b/src/crangler/c_wrangler.cpp
@@ -456,8 +456,8 @@ static void mangle_function(
             auto t_end = match_bracket(t, '(', ')');
             for(; t != t_end; t++)
               out << t->text;
-            out << ' ' << CPROVER_PREFIX << "invariant(" << defines(invariant)
-                << ')';
+            out << ' ' << CPROVER_PREFIX << "loop_invariant("
+                << defines(invariant) << ')';
           }
         }
       }