; int i = 1, factorial = 1;
; assert (i <= 2 || !(factorial & 1));
; for (;;) {
;   factorial *= i;
;   i++;
;   assert (i <= 2 || !(factorial & 1));
; }
1 sort bitvec 4
2 one 1
3 state 1 factorial
4 state 1 i
5 init 1 3 2
6 init 1 4 2
7 add 1 4 2
8 mul 1 3 4
9 next 1 4 7
10 next 1 3 8
11 ones 1
12 sort bitvec 1
13 eq 12 4 11
14 bad 13
15 slice 12 3 0 0
16 constd 1 3
17 ugt 12 4 16
18 and 12 17 15
19 bad 18