[DRAFT] Zero-sized arrays imply the default, empty array, and vica versa

[msooseth]

Description

This fixes the bug as reported in #664 The empty array is kinda special, actually. It implies zero length and zero length also implies the empty array. This was actually not the case before for empty arrays.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[msooseth]

@blishko what do you think of this? I think we need it, as per #664 It's a kind of a small change, but it also requires some thought. Let me know what you think.

[blishko]

I don't think this is entirely correct. Maybe we can have a short call to discuss this?
But at least the second implication seems suspicious to me. I can have a non-empty buffer where all values are zero, no?
Then it would be represented in SMT as ((as const Buf) #b00000000) but the length would be non-empty.

[msooseth]

Yes, you are right. It's a bit unclear to me, too, hence me asking your advice :) It also depends on SMT semantics. And this as const is not even defined right now :S Call would be good actually. Let me think about this a bit more then I'll ask you for a timeslot :) Thanks so much!