1 sort bitvec 1
2 const 1 1
3 const 1 0
4 ite 1 3 2 3
5 eq 1 2 4
6 ite 1 5 3 2
7 sort bitvec 2
8 concat 7 6 3
9 const 7 10
10 eq 1 8 9
11 constraint -10