This looks good, but as you said: it needs tests.

Do you see a better solution for the edge cases where the length overflows? The current behaviour is silently wrap around, right? There probably shouldn't be an overflow warning for that, because it can never really happen in practice... However, what about something like the following:

contract C {
  uint256[] x;
  constructor() public { x.push(42); }
  function f() public {
    x.push(23);
    assert(x[0] == 42);
  }
}

in practice this assertion should always hold (in CHC), but in your encoding it will break, because you can call f 2^256 times and have x[0] == 23, right?
Is this a problem :-)?

Similarly maybe something like:

contract C {
  uint256[] x;
  function f(uint256 l) public {
    require(x.length == 0);
    x.push(42);
    x.push(84);
    for(uint256 i = 0; i < l; ++i)
      x.push(23);
    assert(x[0] == 42);
  }
}

when calling f with sufficiently large l...

I just looked at our codegen, in fact it will silently wrap around in those cases... still a bit weird to have such assertions as in the examples break because of that, because in practice there can never be such an overflow...