-------------------- 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;
    assume {:inferred} 0 <= i;
    goto Then, Else;

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

  Else:
    assume {:inferred} 0 <= i;
    assume !(i < 10);
    assume {:inferred} 10 <= i;
    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} i <= n && 1 <= i;
    goto test;

  Else:
    assume {:inferred} 0 <= i;
    assume !(i < n);
    assume {:inferred} n <= i && 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} 1 / 3 * i == 155;
    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} 1 / 3 * i == 155;
    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} x + 1 <= y;
    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} x + 1 <= y;
    goto B, C;

  B:
    assume {:inferred} x + 1 <= y;
    x := x * x;
    assume {:inferred} true;
    return;

  C:
    assume {:inferred} x + 1 <= y;
    assume {:inferred} x + 1 <= y;
    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 0 - 1 <= x;
    assume {:inferred} -1 <= x;
    goto B, E;

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

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

  D:
    assume {:inferred} 0 <= y;
    x := y;
    assume {:inferred} x == y && 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 <= 10;
    assume {:inferred} 9 <= x && x <= 10;
    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 <= 0;
    goto D;

  C:
    assume {:inferred} true;
    assume y <= 0;
    assume {:inferred} y <= 0;
    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 == j + 4 && 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} j == i + 1 && i == 0 && 4 <= n;
    goto exit, loop0;

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

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



Boogie program verifier finished with 0 verified, 0 errors
-------------------- Bound.bpl -------------------- 

Boogie program verifier finished with 1 verified, 0 errors