In reply to dave_59:
Thanks Dave,
“You will see that only solutions choosing a size of 4 succeed.”
Even a size of 14, will succeed, isnt it?
I added
constraint C3 { arr.size >= 4; arr.size <= 14; }
and now it seems to work.
Thanks for all your help.
How do we know this? Is it an arcane interpretation of LRM?
“The value for the size of an array gets chosen and becomes a state variable”