-------------------- ineq.bpl --------------------
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;

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

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



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;

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

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



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
-------------------- Linear0.bpl --------------------
var x: int;

var y: int;

procedure p();



implementation p()
{

  start:
    assume {:inferred} true;
    assume {:inferred} true;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Linear1.bpl --------------------
var x: int;

var y: int;

procedure p();



implementation p()
{

  start:
    assume {:inferred} true;
    assume x * x == y;
    assume {:inferred} true;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Linear2.bpl --------------------
var x: int;

var y: int;

procedure p();



implementation p()
{

  start:
    assume {:inferred} true;
    assume x == 8;
    assume {:inferred} x == 8;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Linear3.bpl --------------------
var x: int;

var y: int;

procedure p();



implementation p()
{

  start:
    assume {:inferred} true;
    assume x < y;
    assume {:inferred} true;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Linear4.bpl --------------------
var x: int;

var y: int;

procedure p();
  modifies x;



implementation p()
{

  A:
    assume {:inferred} true;
    assume x < y;
    assume {:inferred} true;
    goto B, C;

  B:
    assume {:inferred} true;
    x := x * x;
    assume {:inferred} true;
    return;

  C:
    assume {:inferred} true;
    assume {:inferred} true;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Linear5.bpl --------------------
var x: int;

var y: int;

procedure p();
  modifies x;



implementation p()
{

  A:
    assume {:inferred} true;
    assume -1 <= x;
    assume {:inferred} -1 <= x;
    goto B, E;

  B:
    assume {:inferred} -1 <= x;
    assume x < y;
    assume {:inferred} -1 <= x && 0 <= y;
    goto C, E;

  C:
    assume {:inferred} -1 <= x && 0 <= y;
    x := x * x;
    assume {:inferred} x < 2 && 0 <= y;
    goto D, E;

  D:
    assume {:inferred} x < 2 && 0 <= y;
    x := y;
    assume {:inferred} 0 <= x && 0 <= y;
    return;

  E:
    assume {:inferred} true;
    assume {:inferred} true;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Linear6.bpl --------------------
var x: int;

var y: int;

var z: int;

procedure p();
  modifies x;



implementation p()
{

  A:
    assume {:inferred} true;
    x := 8;
    assume {:inferred} x == 8;
    goto B, C;

  B:
    assume {:inferred} x == 8;
    x := 9;
    assume {:inferred} x == 9;
    goto D;

  C:
    assume {:inferred} x == 8;
    x := 10;
    assume {:inferred} x == 10;
    goto D;

  D:
    assume {:inferred} 9 <= x && x < 11;
    assume {:inferred} 9 <= x && x < 11;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Linear7.bpl --------------------
var x: int;

var y: int;

var z: int;

procedure p();



implementation p()
{

  A:
    assume {:inferred} true;
    assume {:inferred} true;
    goto B, C;

  B:
    assume {:inferred} true;
    assume x <= 0;
    assume {:inferred} x < 1;
    goto D;

  C:
    assume {:inferred} true;
    assume y <= 0;
    assume {:inferred} y < 1;
    goto D;

  D:
    assume {:inferred} true;
    assume {:inferred} true;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Linear8.bpl --------------------
procedure foo();



implementation foo()
{
  var i: int;
  var j: int;
  var n: int;

  A:
    assume {:inferred} true;
    n := 0;
    j := 0;
    i := j + 1;
    i := i + 1;
    i := i + 1;
    i := i + 1;
    i := i + 1;
    j := j + 1;
    assume {:inferred} i == 5 && j == 1 && n == 0;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Linear9.bpl --------------------
procedure foo();



implementation foo()
{
  var i: int;
  var j: int;
  var n: int;

  entry:
    assume {:inferred} true;
    assume n >= 4;
    i := 0;
    j := i + 1;
    assume {:inferred} i == 0 && j == 1 && 4 <= n;
    goto exit, loop0;

  loop0:  // cut point
    assume {:inferred} 0 <= i && 1 <= j && 4 <= n;
    assume j <= n;
    i := i + 1;
    j := j + 1;
    assume {:inferred} 1 <= i && 2 <= j && 4 <= n;
    goto loop0, exit;

  exit:
    assume {:inferred} 0 <= i && 1 <= j && 4 <= n;
    assume {:inferred} 0 <= i && 1 <= j && 4 <= n;
    return;
}



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Bound.bpl -------------------- 
Bound.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
    Bound.bpl(8,1): start
    Bound.bpl(14,1): LoopHead
    Bound.bpl(22,1): AfterLoop

Boogie program verifier finished with 0 verified, 1 error