diff --git a/examples/publications/2020/permutations/insertion.pvl b/examples/publications/2020/permutations/insertion.pvl
index e5f26c958f..6c04998a7d 100644
--- a/examples/publications/2020/permutations/insertion.pvl
+++ b/examples/publications/2020/permutations/insertion.pvl
@@ -81,7 +81,7 @@ class BubbleSort {
 		int k = 0;
 
 		loop_invariant 0 <= k && k <= |xs|;
-		loop_invariant (\forall int l; l>=0 && l<k; counter(xs + ys, xs[l]) == counter(xs, xs[l]) + counter(ys, xs[l]));
+		loop_invariant (\forall int l; l>=0 && l<k; {: counter(xs + ys, xs[l]) :} == counter(xs, xs[l]) + counter(ys, xs[l]));
 		while(k < |xs|)
 		{
 			lemma_count_app(xs, ys, xs[k]);
@@ -157,7 +157,7 @@ class BubbleSort {
 		int k = 0;
 
 		loop_invariant 0 <= k && k <= |xs|;
-		loop_invariant (\forall int l; l>=0 && l<k; counter(xs, xs[l]) == counter(ys, xs[l]));
+		loop_invariant (\forall int l; l>=0 && l<k; {: counter(xs, xs[l]) :} == counter(ys, xs[l]));
 		while(k < |xs|)
 		{
 			lemma_swap_permutation(xs, ys, i, j, xs[k]);