[DMS-22] motoko-san: loop invariants

[int-index]

New features:

• invariants in while-loops

New test cases:

• test/viper/loop-invariant.mo

while (i < n) {
      assert:loop:invariant (i * 2 == j);
      assert:loop:invariant (j - i == i);
      i := i + 1;
      j := j + 2;
    };

[GoPavel]

Suggested change

	fprintf ppf "@[<v 2>while (%a) @[<v 0>%a@] {@ %a}@]"
	fprintf ppf "@[<v 2>while (%a)@;@[<v 0>%a@]@;%a@]"

This removes spare brackets and move invariants on next line

[int-index]

Thank you, yes, this makes the output cleaner

[GoPavel]

Others LGTM