fact: {} -> PROPAGATEx = 1fact: {x: 1}y = 2fact: {x: 1, y: 2}~z = x + y~~{x: 1, y : 2, z: 3} -> REWRITE + PROPAGATEz = 3-- :( rewrite, propagate. --fact: {} -> PROPAGATEx = 1fact: {x: 1}y = 2fact: {x: 1, y: 2}~z = x + y~~{x: 1, y : 2} -> REWRITEz = 3 <- NEW statement from the REWRITE;
fact: {x: 1, y: 2, z: 3}
x = 2 * 10 ; (x = 20; x is EVEN)
y = 2 * z; (y = UNK; y is EVEN)
-> if (y %2 == 0) { T } else { E }<- NEW statement from the REWRITE;
fact: {x: 1, y: 2, z: 3}
x = 2 * 10 ; (x = 20; x is EVEN)
y = 2 * z; (y = UNK; y is EVEN)
->T -> analysis