Failure("TODO rearrange_start_inequality at 6:25")

[yav]

The following program causes a crash:

void preserve(int size, int *p)
/*@
requires
  take a1 = each(u64 i; i < (u64)size) { Owned<int>(array_shift<int>(p,i)) };
ensures
  take a2 = each(u64 i; i < (u64)size) { Owned<int>(array_shift<int>(p,i)) };
@*/
{
}

Output:

cn: internal error, uncaught exception:
    Failure("TODO rearrange_start_inequality at 6:25")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__Cn_internal_to_ail.generate_start_expr in ...

CN version: 53c1e48

[yav]

Moved to rems-project#689 in main repo