In reply to CPU_Verif:
I did not follow what is implied by this “foreach (unum[i]) num.sum() with (4’(item==unum[i]))==1;”
“there must be at least 7 unique elements in this array”
You should unroll the foreach loop into 7 constraint expressions and see if that helps you see what it does. If that is not enough, unroll one of the num.sum() methods.