Unsound interaction between arrays and subranges

[yav]

I was trying to understand the semantics of arrays as implemented in jkind, and I came across an example, where just adding an additional property to prove causes jkind to change its mind about the validity of another property:

type T = subrange [2,2] of int;

node main() returns ();
var a : T[2];
    j : T;
    i : int;
    ok1, ok2 : bool;
let
  a   = [2,2];
  i   = 3;
  j   = a[i];
  ok1 = a[i] = 2;
  ok2 = j = 2;
  --%PROPERTY ok1;
  --%PROPERTY ok2;
tel

If you run the example as is, then jkind states the both properties are valid. If you comment out the last line (where we ask it to prove ok2), then it reports that ok1 is invalid.

This is with version 4.0.1

As an aside: what is the intended treatment of "undefined" values---is is an arbitrary value of the given type, or is it some special additional element that is different from all elements in the type?

[agacek]

The intended treatment of indexing an array outside of its bounds is to get a "default" element of the correct type. For subrange types we use the lowest value as the default. Thus both properties should be true.

As your example shows, there is a bug in the handling of subrange types and arrays.