isolateJump.ppl

procedure IsolateReturn(x: int, y: int) returns (r: int);
  ensures r > 4;



implementation IsolateReturn(x: int, y: int) returns (r: int)
{
  var r#AT#0: int;
  var r#AT#1: int;
  var r#AT#2: int;
  var r#AT#3: int;
  var r#AT#4: int;
  var r#AT#5: int;


  anon0:
    goto anon6_Then, anon6_Else;

  anon6_Then:
    assume {:partition} x > 0;
    assume r#AT#0 == 0 + 1;
    assume r#AT#2 == r#AT#0;
    goto anon7_Then;

  anon6_Else:
    assume {:partition} 0 >= x;
    assume r#AT#1 == 0 + 2;
    assume r#AT#2 == r#AT#1;
    goto anon7_Then;

  anon7_Then:
    assume {:partition} y > 0;
    assume r#AT#3 == r#AT#2 + 3;
    assume r#AT#5 == r#AT#3;
    assert r#AT#5 > 4;
    return;
}



procedure IsolateReturnPaths(x: int, y: int) returns (r: int);
  ensures r > 4;



implementation IsolateReturnPaths(x: int, y: int) returns (r: int)
{
  var r#AT#0: int;
  var r#AT#1: int;
  var r#AT#2: int;
  var r#AT#3: int;
  var r#AT#4: int;
  var r#AT#5: int;
  var r#AT#6: int;


  PreconditionGeneratedEntry:
    goto anon0;

  anon0:
    goto anon10_Then, anon10_Else;

  anon10_Else:
    assume {:partition} 0 >= x;
    goto anon11_Then, anon11_Else;

  anon11_Else:
    assume {:partition} 1 >= x;
    assume r#AT#2 == 0 + 3;
    goto anon12_Then, anon12_Else;

  anon12_Else:
    assume {:partition} 0 >= x + y;
    assume r#AT#3 == 0;
    goto anon7;

  anon7:
    goto anon13_Then, anon13_Else;

  anon13_Else:
    assume {:partition} 0 >= y;
    assume r#AT#5 == r#AT#3 + 6;
    assume r#AT#6 == r#AT#5;
    goto GeneratedUnifiedExit;

  GeneratedUnifiedExit:
    assert r#AT#6 > 4;
    return;

  anon13_Then:
    assume {:partition} y > 0;
    assume r#AT#4 == r#AT#3 + 3;
    assume r#AT#6 == r#AT#4;
    goto GeneratedUnifiedExit;

  anon12_Then:
    assume {:partition} x + y > 0;
    assume r#AT#3 == 0;
    goto anon7;

  anon11_Then:
    assume {:partition} x > 1;
    assume r#AT#1 == 0 + 2;
    goto anon12_Then, anon12_Else;

  anon10_Then:
    assume {:partition} x > 0;
    assume r#AT#0 == 0 + 1;
    goto anon12_Then, anon12_Else;
}