1 sort bitvec 1
2 sort bitvec 2
3 input 1 s
4 input 1 t
5 zero 2
6 state 2 a
7 state 2 b
8 init 2 6 5
9 init 2 7 5
10 one 2
11 add 2 6 10
12 add 2 7 10
13 ite 2 3 11 6
14 ite 2 4 12 7
15 next 2 6 13
16 next 2 7 14
17 ones 2
18 eq 1 6 17
19 eq 1 7 17
20 and 1 18 19
21 bad 20
22 nand 1 3 4
23 constraint 22