LARA This is an old revision of the document! Symbolic Execution for Example Integer Program State variables: x :: int y :: int res :: int res = 0; i = x; while (i > 0) { i = i - 1; res = res + 2; }