1 sort bitvec 1 2 const 1 0 3 sort bitvec 2 4 const 3 00 5 sort array 3 1 6 input 5 @arr6 7 input 3 3 8 write 5 6 7 2 9 write 5 8 4 -2 10 eq 1 8 9 11 input 1 14 12 and 1 2 -11 13 and 1 -2 -12 14 concat 3 2 -13 15 write 5 9 -4 2 16 read 1 15 14 17 and 1 2 10 18 and 1 2 16 19 and 1 2 17 20 and 1 -2 -18 21 and 1 2 -19 22 and 1 -2 20 23 and 1 2 21 24 and 1 -2 -23 25 and 1 -2 22 26 and 1 -24 -25 27 constraint -26