// This example 1 from Chapter 9 of the KeY book, the invariant for the loop is x>=3

\javaSource "code/";

\withOptions transactions:transactionsOff,transactionAbort:abortOff,throughout:toutOn,intRules:arithmeticSemanticsIgnoringOF;

\programVariables {
  int x;
}

\problem {

x >= 2 ->
\[[{
  x = 3;
  while (x < 10) {
    if(x == 2)
      x = 1;
    else
      x++;
  }
}\]] x >= 2

}