diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
index 71d3be6538b..dba2c0b3ad0 100644
--- a/src/viper/pretty.ml
+++ b/src/viper/pretty.ml
@@ -251,7 +251,8 @@ and pp_fldacc ppf fldacc =
     fprintf ppf "@[(%a).%s@]" pp_exp exp1 id.it
 
 and pp_loop_inv ppf inv =
-    fprintf ppf "invariant %a" pp_exp inv
+    marks := inv.at :: !marks;
+    fprintf ppf "\017invariant %a\019" pp_exp inv
 
 let prog_mapped file p =
     marks := [];
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index ff17d5b221a..b06cc5562b4 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -140,8 +140,8 @@ let rec extract_loop_invariants (e : M.exp) : (M.exp list * M.exp) =
   | _ -> ([], e)
 and extract_loop_invariants' (ds : M.dec list) (acc : M.exp list) : (M.exp list * M.dec list) =
   match ds with
-  | M.({ it = ExpD ({ it = AssertE (Loop_invariant, inv); _ }); _ }) :: ds ->
-      extract_loop_invariants' ds (inv :: acc)
+  | M.({ it = ExpD ({ it = AssertE (Loop_invariant, inv); at = assert_at; _ }); _ }) :: ds ->
+      extract_loop_invariants' ds ({ inv with at = assert_at } :: acc)
   | _ -> (List.rev acc, ds)
 
 let rec extract_concurrency (seq : seqn) : stmt' list * seqn =
diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok
index cd5ccbe1e6f..c072d2c1c57 100644
--- a/test/viper/ok/reverse.vpr.ok
+++ b/test/viper/ok/reverse.vpr.ok
@@ -88,12 +88,13 @@ method reverseArray$Nat($Self: Ref, a: Array)
          invariant ((i < length) && (i >= 0))
          invariant ((j < length) && (j >= 0))
          invariant (i == (($size(a) - 1) - j))
-         invariant forall k : Int :: (((j <= k) && (k <= i)) ==> (($loc(a, k)).$int == 
-                   old(($loc(a, k)).$int)))
+         invariant forall k : Int :: (((j <= k) && (k <= i)) ==> (($loc(a,
+                                                                    k)).$int == 
+                    old(($loc(a, k)).$int)))
          invariant forall k : Int :: (((0 <= k) && (k < j)) ==> (($loc(a, k)).$int == 
-                   old(($loc(a, (($size(a) - 1) - k))).$int)))
+                    old(($loc(a, (($size(a) - 1) - k))).$int)))
          invariant forall k : Int :: (((i < k) && (k < $size(a))) ==> (
-                   ($loc(a, k)).$int == old(($loc(a, (($size(a) - 1) - k))).$int)))
+                    ($loc(a, k)).$int == old(($loc(a, (($size(a) - 1) - k))).$int)))
          invariant ($Perm($Self) && $Inv($Self))
          { var tmp: Int
            tmp := ($loc(a, i)).$int;