Failure while testing each

[yav]

When I try to generate tests for the following code, I get an exception:

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

This throws:

 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 file "backend/cn/lib/cn_internal_to_ail.ml", line 533, characters 11-53

Another example that leads to the same exception is if you make the size an int, and add a cast:

take a1 = each(u64 i; i <= 0u64 && i < (u64)size) { Owned<int>(array_shift<int>(p,i)) };

Another variation, if we remove the redundant 0 <= 0u64 constraint:

take a1 = each(u64 i; i < size) { Owned<int>(array_shift<int>(p,i)) };

This throws:

cn: internal error, uncaught exception:
    Failure("Not of correct form (unlikely case - i's not matching)")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__Cn_internal_to_ail.generate_start_expr in file "backend/cn/lib/cn_internal_to_ail.ml", line 530, characters 8-73

The only version I was able to run without exceptions is to use int as the size:

take a1 = each(i32 i; 0i32 <= i && i < size) { Owned<int>(array_shift<int>(p,i)) };

This, however, leads to warnings from cn saying that each expects a u64.