LARA

Symbolic Execution for Example Integer Program

State variables: 

x, y, res, i :: int

Code: 

res = 0;
i = x;
while (i > 0) {
  i = i - 1;
  res = res + 2;
}