procedure SimpleLoop();



implementation SimpleLoop()
{
  var i: int;

  start:
    assume {:inferred} true;
    i := 0;
    assume {:inferred} i == 0;
    goto test;

  test:  // cut point
    assume {:inferred} 0 <= i && i < 11;
    assume {:inferred} 0 <= i && i < 11;
    goto Then, Else;

  Else:
    assume {:inferred} 0 <= i && i < 11;
    assume !(i < 10);
    assume {:inferred} 0 <= i && i < 11;
    return;

  Then:
    assume {:inferred} 0 <= i && i < 11;
    assume i < 10;
    i := i + 1;
    assume {:inferred} 1 <= i && i < 11;
    goto test;
}



procedure VariableBoundLoop(n: int);



implementation VariableBoundLoop(n: int)
{
  var i: int;

  start:
    assume {:inferred} true;
    i := 0;
    assume {:inferred} i == 0;
    goto test;

  test:  // cut point
    assume {:inferred} 0 <= i;
    assume {:inferred} 0 <= i;
    goto Then, Else;

  Else:
    assume {:inferred} 0 <= i;
    assume !(i < n);
    assume {:inferred} 0 <= i;
    return;

  Then:
    assume {:inferred} 0 <= i;
    assume i < n;
    i := i + 1;
    assume {:inferred} 1 <= i && 1 <= n;
    goto test;
}



procedure Foo();



implementation Foo()
{
  var i: int;

  start:
    assume {:inferred} true;
    i := 3 * i + 1;
    i := 3 * (i + 1);
    i := 1 + 3 * i;
    i := (i + 1) * 3;
    assume {:inferred} true;
    return;
}



procedure FooToo();



implementation FooToo()
{
  var i: int;

  start:
    assume {:inferred} true;
    i := 5;
    i := 3 * i + 1;
    i := 3 * (i + 1);
    i := 1 + 3 * i;
    i := (i + 1) * 3;
    assume {:inferred} i == 465;
    return;
}



procedure FooTooStepByStep();



implementation FooTooStepByStep()
{
  var i: int;

  L0:
    assume {:inferred} true;
    i := 5;
    i := 3 * i + 1;
    i := 3 * (i + 1);
    i := 1 + 3 * i;
    i := (i + 1) * 3;
    assume {:inferred} i == 465;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors