1 sort bitvec 32
2 input 1 v1
3 input 1 v2
4 const 1 00000000000000000000000000000000
5 sort bitvec 1
6 eq 5 2 4
7 urem 1 3 2
8 ult 5 7 2
9 constraint -8
10 constraint -6