In reply to totochan1985:
sum() is one of the array reduction methods (See section 7.12.3 Array reduction methods).
When used in a constraint, these methods get unrolled into a big expression (Section 18.5.8.2 Array reduction iterative constraints)
‘item’ is replaced with each element of the array.
val.sum() with (int'(item==val3))
becomes
int'(val[0]==val3) + int'(val[1]==val3) + int'(val[2]==val3) + ... +int'(val[9]==val3)
The cast to int is needed because otherwise the sum would be limited to 1-bit, which is the result of the equality operator.