1 sort bitvec 8 2 sort array 1 1 3 input 2 @arr3 4 input 1 @inp4 5 const 1 00000001 6 add 1 4 5 7 write 2 3 4 6 8 read 1 7 6 9 read 1 3 6 10 sort bitvec 1 11 eq 10 8 9 12 constraint -11