In reply to ssureshg_:
It’s mem.sum(), which iterates over one dimension of an unpacked arrays. This would be mem[0] + mem[1]. However, these are both arrays of 16 elements. The with clause selects the second dimension. If we unroll the foreach loop, the constraint becomes
mem.sum() with (int'(mem[item.index][0])) != 2 ;
mem.sum() with (int'(mem[item.index][1])) != 2 ;
...
mem.sum() with (int'(mem[item.index][15])) != 2 ;
Then expand the sum methods
int'(mem[0][0]) + int'(mem[1][0]) !=2;
int'(mem[0][1]) + int'(mem[1][1]) !=2;
...
int'(mem[0][15]) + int'(mem[1][15]) !=2;