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;
}