1 sort bitvec 4
2 constd 1 6
3 constd 1 3
4 neg 1 3
5 input 1 res
6 smod 1 2 4
7 sort bitvec 1
8 eq 7 5 6
9 constraint 8