Even simpler than before. We flatten expressions.

 c ::=  x=T | (if (F) c else c) | c ; c | (while (F) c)
 T ::= K | V | (V + V) | (V * V)
 F ::= (V=0) | (0 < V) | (V < 0)
 V ::= x | y | z | ...
 K ::= 0 | 1 | 2 | ...

We represent programs as control-flow graphs, so we have 'assume(F)' and branches instead of conditional statements.

Basic statements:

V = V
V = K
V = V+V
V = V*V
assume (V=0)
assume (0 < V)
assume (V < 0)