var GlobalFlag: bool;

const A: int;

const B: int;

const C: int;

procedure Join(b: bool);
  modifies GlobalFlag;



implementation Join(b: bool)
{
  var x: int;
  var y: int;
  var z: int;

  start:
    assume true;
    GlobalFlag := true;
    x := 3;
    y := 4;
    z := x + y;
    assume x == 3 && y == 4 && z == 7;
    goto Then, Else;

  Then:
    assume x == 3 && y == 4 && z == 7;
    assume b <==> true;
    x := x + 1;
    assume x == 4 && y == 4 && z == 7;
    goto join;

  Else:
    assume x == 3 && y == 4 && z == 7;
    assume b <==> false;
    y := 4;
    assume x == 3 && y == 4 && z == 7;
    goto join;

  join:
    assume y == 4 && z == 7;
    assert y == 4;
    assert z == 7;
    assert GlobalFlag <==> true;
    assume y == 4 && z == 7;
    return;
}



procedure Loop();



implementation Loop()
{
  var c: int;
  var i: int;

  start:
    assume true;
    c := 0;
    i := 0;
    assume c == 0 && i == 0;
    goto test;

  test:  // cut point
    assume c == 0;
    assume c == 0;
    goto Then, Else;

  Then:
    assume c == 0;
    assume i < 10;
    i := i + 1;
    assume c == 0;
    goto test;

  Else:
    assume c == 0;
    assume c == 0;
    return;
}



procedure Evaluate();



implementation Evaluate()
{
  var i: int;

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



Boogie program verifier finished with 0 verified, 0 errors