type ref;
type realVar;
type classConst;
// type Field x;
// var $HeapVar : <x>[ref, Field x]x;

const unique $null : ref ;
const unique $intArrNull : [int]int ;
const unique $realArrNull : [int]realVar ;
const unique $refArrNull : [int]ref ;

const unique $arrSizeIdx : int;
var $intArrSize : [int]int;
var $realArrSize : [realVar]int;
var $refArrSize : [ref]int;

var $stringSize : [ref]int;

//built-in axioms 
axiom ($arrSizeIdx == -1);

//note: new version doesn't put helpers in the perlude anymore//Prelude finished 



var java.lang.Object$TreeLeftmostPath.ObjectList$value254 : Field ref;
var TreeLeftmostPath.ObjectList$TreeLeftmostPath.ObjectList$next255 : Field ref;
var int$TreeLeftmostPath.Random$index0 : int;
var TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$left298 : Field ref;
var TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$right299 : Field ref;
var java.lang.String$lp$$rp$$TreeLeftmostPath.Random$args256 : [int]ref;
var java.lang.Object$TreeLeftmostPath.Tree$value300 : Field ref;


// procedure is generated by joogie.
function {:inline true} $neref(x : ref, y : ref) returns (__ret : int) {
if (x != y) then 1 else 0
}


// procedure is generated by joogie.
function {:inline true} $realarrtoref($param00 : [int]realVar) returns (__ret : ref);



// procedure is generated by joogie.
function {:inline true} $modreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar);



	 //  @line: 22
// <TreeLeftmostPath.Tree: TreeLeftmostPath.Tree createTree()>
procedure TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$createTree$2458() returns (__ret : ref)
  modifies $HeapVar;
 {
var $r334 : ref;
var i031 : int;
var $r132 : ref;
var r537 : ref;
var $r435 : ref;
var r028 : ref;
var $r233 : ref;
var i136 : int;
	 //  @line: 23
Block32:
	 //  @line: 23
	 call i136 := int$TreeLeftmostPath.Random$random$2231();
	 goto Block33;
	 //  @line: 24
Block33:
	 goto Block36, Block34;
	 //  @line: 24
Block36:
	 //  @line: 24
	 assume ($negInt(($neint((i136), (0))))==1);
	 //  @line: 25
	__ret := $null;
	 return;
	 //  @line: 24
Block34:
	 assume ($neint((i136), (0))==1);
	 goto Block35;
	 //  @line: 27
Block35:
	 //  @line: 27
	 call r028 := TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$createNode$2457();
	 goto Block37;
	 //  @line: 28
Block37:
	 //  @line: 28
	r537 := r028;
	 goto Block38;
	 //  @line: 30
Block38:
	 goto Block39, Block41;
	 //  @line: 30
Block39:
	 assume ($leint((i136), (0))==1);
	 goto Block40;
	 //  @line: 30
Block41:
	 //  @line: 30
	 assume ($negInt(($leint((i136), (0))))==1);
	 //  @line: 31
	 call i031 := int$TreeLeftmostPath.Random$random$2231();
	 goto Block42;
	 //  @line: 50
Block40:
	 //  @line: 50
	__ret := r028;
	 return;
	 //  @line: 32
Block42:
	 goto Block43, Block45;
	 //  @line: 32
Block43:
	 assume ($leint((i031), (0))==1);
	 goto Block44;
	 //  @line: 32
Block45:
	 //  @line: 32
	 assume ($negInt(($leint((i031), (0))))==1);
	 assert ($neref((r537), ($null))==1);
	 //  @line: 33
	$r334 := $HeapVar[r537, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$left298];
	 goto Block46;
	 //  @line: 40
Block44:
	 assert ($neref((r537), ($null))==1);
	 //  @line: 40
	$r132 := $HeapVar[r537, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$right299];
	 goto Block52;
	 //  @line: 33
Block46:
	 goto Block49, Block47;
	 //  @line: 40
Block52:
	 goto Block53, Block55;
	 //  @line: 33
Block49:
	 //  @line: 33
	 assume ($negInt(($neref(($r334), ($null))))==1);
	 //  @line: 34
	 call $r435 := TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$createNode$2457();
	 assert ($neref((r537), ($null))==1);
	 //  @line: 34
	$HeapVar[r537, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$left298] := $r435;
	 //  @line: 35
	r537 := r028;
	 goto Block50;
	 //  @line: 33
Block47:
	 assume ($neref(($r334), ($null))==1);
	 goto Block48;
	 //  @line: 40
Block53:
	 assume ($neref(($r132), ($null))==1);
	 goto Block54;
	 //  @line: 40
Block55:
	 //  @line: 40
	 assume ($negInt(($neref(($r132), ($null))))==1);
	 //  @line: 41
	 call $r233 := TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$createNode$2457();
	 assert ($neref((r537), ($null))==1);
	 //  @line: 41
	$HeapVar[r537, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$right299] := $r233;
	 //  @line: 42
	r537 := r028;
	 goto Block50;
	 //  @line: 47
Block50:
	 //  @line: 47
	i136 := $addint((i136), (-1));
	 goto Block56;
	 //  @line: 37
Block48:
	 assert ($neref((r537), ($null))==1);
	 //  @line: 37
	r537 := $HeapVar[r537, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$left298];
	 goto Block51;
	 //  @line: 44
Block54:
	 assert ($neref((r537), ($null))==1);
	 //  @line: 44
	r537 := $HeapVar[r537, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$right299];
	 goto Block50;
	 //  @line: 48
Block56:
	 goto Block38;
	 //  @line: 37
Block51:
	 goto Block50;
}


	 //  @line: 2
// <TreeLeftmostPath.TreeLeftmostPath: void <init>()>
procedure void$TreeLeftmostPath.TreeLeftmostPath$$la$init$ra$$2460(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r040 : ref;
Block58:
	r040 := __this;
	 assert ($neref((r040), ($null))==1);
	 //  @line: 3
	 call void$java.lang.Object$$la$init$ra$$28((r040));
	 return;
}


// procedure is generated by joogie.
function {:inline true} $leref($param00 : ref, $param11 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $modint($param00 : int, $param11 : int) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $gtref($param00 : ref, $param11 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $eqrealarray($param00 : [int]realVar, $param11 : [int]realVar) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $addint(x : int, y : int) returns (__ret : int) {
(x + y)
}


// procedure is generated by joogie.
function {:inline true} $subref($param00 : ref, $param11 : ref) returns (__ret : ref);



	 //  @line: 7
// <TreeLeftmostPath.Random: int random()>
procedure int$TreeLeftmostPath.Random$random$2231() returns (__ret : int)
  modifies int$TreeLeftmostPath.Random$index0, $stringSize;
 {
var $i317 : int;
var $r113 : [int]ref;
var r014 : ref;
var $i012 : int;
var $i216 : int;
var $i115 : int;
	 //  @line: 8
Block25:
	 //  @line: 8
	$r113 := java.lang.String$lp$$rp$$TreeLeftmostPath.Random$args256;
	 //  @line: 8
	$i012 := int$TreeLeftmostPath.Random$index0;
	 assert ($geint(($i012), (0))==1);
	 assert ($ltint(($i012), ($refArrSize[$r113[$arrSizeIdx]]))==1);
	 //  @line: 8
	r014 := $r113[$i012];
	 //  @line: 9
	$i115 := int$TreeLeftmostPath.Random$index0;
	 //  @line: 9
	$i216 := $addint(($i115), (1));
	 //  @line: 9
	int$TreeLeftmostPath.Random$index0 := $i216;
	$i317 := $stringSize[r014];
	 //  @line: 10
	__ret := $i317;
	 return;
}


// procedure is generated by joogie.
function {:inline true} $inttoreal($param00 : int) returns (__ret : realVar);



// procedure is generated by joogie.
function {:inline true} $shrint($param00 : int, $param11 : int) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $negReal($param00 : realVar) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $ushrint($param00 : int, $param11 : int) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $refarrtoref($param00 : [int]ref) returns (__ret : ref);



// procedure is generated by joogie.
function {:inline true} $divref($param00 : ref, $param11 : ref) returns (__ret : ref);



	 //  @line: 4
// <TreeLeftmostPath.TreeLeftmostPath: void main(java.lang.String[])>
procedure void$TreeLeftmostPath.TreeLeftmostPath$main$2461($param_0 : [int]ref)
  modifies $HeapVar, $stringSize, java.lang.String$lp$$rp$$TreeLeftmostPath.Random$args256;
 {
var r551 : ref;
var r143 : ref;
var $r746 : ref;
var $r645 : ref;
var r041 : [int]ref;
var r952 : ref;
var r248 : ref;
var r450 : ref;
var $r847 : ref;
var r349 : ref;
Block59:
	r041 := $param_0;
	 //  @line: 5
	java.lang.String$lp$$rp$$TreeLeftmostPath.Random$args256 := r041;
	 //  @line: 6
	 call r143 := TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$createTree$2458();
	 //  @line: 7
	r952 := $null;
	 goto Block60;
	 //  @line: 8
Block60:
	 assert ($neref((r143), ($null))==1);
	 //  @line: 8
	$r645 := $HeapVar[r143, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$left298];
	 goto Block61;
	 //  @line: 8
Block61:
	 goto Block62, Block64;
	 //  @line: 8
Block62:
	 assume ($eqref(($r645), ($null))==1);
	 goto Block63;
	 //  @line: 8
Block64:
	 //  @line: 8
	 assume ($negInt(($eqref(($r645), ($null))))==1);
	 //  @line: 15
	$r746 := $newvariable((65));
	 assume ($neref(($newvariable((65))), ($null))==1);
	 assert ($neref((r143), ($null))==1);
	 //  @line: 15
	$r847 := $HeapVar[r143, java.lang.Object$TreeLeftmostPath.Tree$value300];
	 assert ($neref(($r746), ($null))==1);
	 //  @line: 15
	 call void$TreeLeftmostPath.ObjectList$$la$init$ra$$2228(($r746), ($r847), (r952));
	 //  @line: 15
	r952 := $r746;
	 assert ($neref((r143), ($null))==1);
	 //  @line: 16
	r248 := $HeapVar[r143, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$left298];
	 assert ($neref((r248), ($null))==1);
	 //  @line: 17
	r349 := $HeapVar[r248, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$left298];
	 assert ($neref((r248), ($null))==1);
	 //  @line: 18
	r450 := $HeapVar[r248, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$right299];
	 assert ($neref((r143), ($null))==1);
	 //  @line: 19
	r551 := $HeapVar[r143, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$right299];
	 assert ($neref((r143), ($null))==1);
	 //  @line: 20
	$HeapVar[r143, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$right299] := r248;
	 assert ($neref((r248), ($null))==1);
	 //  @line: 21
	$HeapVar[r248, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$right299] := r551;
	 assert ($neref((r248), ($null))==1);
	 //  @line: 22
	$HeapVar[r248, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$left298] := r450;
	 assert ($neref((r143), ($null))==1);
	 //  @line: 23
	$HeapVar[r143, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$left298] := r349;
	 goto Block60;
	 //  @line: 25
Block63:
	 return;
}


// procedure is generated by joogie.
function {:inline true} $mulref($param00 : ref, $param11 : ref) returns (__ret : ref);



// procedure is generated by joogie.
function {:inline true} $neint(x : int, y : int) returns (__ret : int) {
if (x != y) then 1 else 0
}


// <java.lang.String: int length()>
procedure int$java.lang.String$length$59(__this : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $ltreal($param00 : realVar, $param11 : realVar) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $reftorefarr($param00 : ref) returns (__ret : [int]ref);



// procedure is generated by joogie.
function {:inline true} $gtint(x : int, y : int) returns (__ret : int) {
if (x > y) then 1 else 0
}


// procedure is generated by joogie.
function {:inline true} $reftoint($param00 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $addref($param00 : ref, $param11 : ref) returns (__ret : ref);



	 //  @line: 52
// <TreeLeftmostPath.Tree: void main(java.lang.String[])>
procedure void$TreeLeftmostPath.Tree$main$2459($param_0 : [int]ref)
  modifies $stringSize, java.lang.String$lp$$rp$$TreeLeftmostPath.Random$args256;
 {
var r038 : [int]ref;

 //temp local variables 
var $freshlocal0 : ref;

Block57:
	r038 := $param_0;
	 //  @line: 53
	java.lang.String$lp$$rp$$TreeLeftmostPath.Random$args256 := r038;
	 //  @line: 54
	 call $freshlocal0 := TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$createTree$2458();
	 return;
}


// procedure is generated by joogie.
function {:inline true} $xorreal($param00 : realVar, $param11 : realVar) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $andref($param00 : ref, $param11 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $cmpreal(x : realVar, y : realVar) returns (__ret : int) {
if ($ltreal((x), (y)) == 1) then 1 else if ($eqreal((x), (y)) == 1) then 0 else -1
}


// procedure is generated by joogie.
function {:inline true} $addreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar);



// procedure is generated by joogie.
function {:inline true} $gtreal($param00 : realVar, $param11 : realVar) returns (__ret : int);



	 //  @line: 2
// <TreeLeftmostPath.Random: void <init>()>
procedure void$TreeLeftmostPath.Random$$la$init$ra$$2230(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r011 : ref;
Block24:
	r011 := __this;
	 assert ($neref((r011), ($null))==1);
	 //  @line: 3
	 call void$java.lang.Object$$la$init$ra$$28((r011));
	 return;
}


// procedure is generated by joogie.
function {:inline true} $eqreal(x : realVar, y : realVar) returns (__ret : int) {
if (x == y) then 1 else 0
}


// procedure is generated by joogie.
function {:inline true} $ltint(x : int, y : int) returns (__ret : int) {
if (x < y) then 1 else 0
}


// procedure is generated by joogie.
function {:inline true} $newvariable($param00 : int) returns (__ret : ref);



// procedure is generated by joogie.
function {:inline true} $divint($param00 : int, $param11 : int) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $geint(x : int, y : int) returns (__ret : int) {
if (x >= y) then 1 else 0
}


// procedure is generated by joogie.
function {:inline true} $mulint($param00 : int, $param11 : int) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $leint(x : int, y : int) returns (__ret : int) {
if (x <= y) then 1 else 0
}


// procedure is generated by joogie.
function {:inline true} $shlref($param00 : ref, $param11 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $eqrefarray($param00 : [int]ref, $param11 : [int]ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $reftointarr($param00 : ref) returns (__ret : [int]int);



// procedure is generated by joogie.
function {:inline true} $ltref($param00 : ref, $param11 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $mulreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar);



// procedure is generated by joogie.
function {:inline true} $shrref($param00 : ref, $param11 : ref) returns (__ret : int);



	 //  @line: 7
// <TreeLeftmostPath.Tree: void <init>(TreeLeftmostPath.Tree,TreeLeftmostPath.Tree)>
procedure void$TreeLeftmostPath.Tree$$la$init$ra$$2455(__this : ref, $param_0 : ref, $param_1 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r119 : ref;
var r018 : ref;
var r220 : ref;
Block27:
	r018 := __this;
	r119 := $param_0;
	r220 := $param_1;
	 assert ($neref((r018), ($null))==1);
	 //  @line: 8
	 call void$java.lang.Object$$la$init$ra$$28((r018));
	 assert ($neref((r018), ($null))==1);
	 //  @line: 9
	$HeapVar[r018, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$left298] := r119;
	 assert ($neref((r018), ($null))==1);
	 //  @line: 10
	$HeapVar[r018, TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$right299] := r220;
	 return;
}


// procedure is generated by joogie.
function {:inline true} $ushrreal($param00 : realVar, $param11 : realVar) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $shrreal($param00 : realVar, $param11 : realVar) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $divreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar);



// procedure is generated by joogie.
function {:inline true} $orint($param00 : int, $param11 : int) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $reftorealarr($param00 : ref) returns (__ret : [int]realVar);



// procedure is generated by joogie.
function {:inline true} $cmpref(x : ref, y : ref) returns (__ret : int) {
if ($ltref((x), (y)) == 1) then 1 else if ($eqref((x), (y)) == 1) then 0 else -1
}


// procedure is generated by joogie.
function {:inline true} $realtoint($param00 : realVar) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $geref($param00 : ref, $param11 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $orreal($param00 : realVar, $param11 : realVar) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $eqint(x : int, y : int) returns (__ret : int) {
if (x == y) then 1 else 0
}


// procedure is generated by joogie.
function {:inline true} $ushrref($param00 : ref, $param11 : ref) returns (__ret : int);



	 //  @line: 6
// <TreeLeftmostPath.ObjectList: void <init>(java.lang.Object,TreeLeftmostPath.ObjectList)>
procedure void$TreeLeftmostPath.ObjectList$$la$init$ra$$2228(__this : ref, $param_0 : ref, $param_1 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r23 : ref;
var r01 : ref;
var r12 : ref;
Block16:
	r01 := __this;
	r12 := $param_0;
	r23 := $param_1;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 7
	 call void$java.lang.Object$$la$init$ra$$28((r01));
	 assert ($neref((r01), ($null))==1);
	 //  @line: 8
	$HeapVar[r01, java.lang.Object$TreeLeftmostPath.ObjectList$value254] := r12;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 9
	$HeapVar[r01, TreeLeftmostPath.ObjectList$TreeLeftmostPath.ObjectList$next255] := r23;
	 return;
}


	 //  @line: 12
// <TreeLeftmostPath.Tree: void <init>()>
procedure void$TreeLeftmostPath.Tree$$la$init$ra$$2456(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r021 : ref;
Block28:
	r021 := __this;
	 assert ($neref((r021), ($null))==1);
	 //  @line: 13
	 call void$java.lang.Object$$la$init$ra$$28((r021));
	 return;
}


// procedure is generated by joogie.
function {:inline true} $modref($param00 : ref, $param11 : ref) returns (__ret : ref);



// procedure is generated by joogie.
function {:inline true} $eqintarray($param00 : [int]int, $param11 : [int]int) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $negRef($param00 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $lereal($param00 : realVar, $param11 : realVar) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $nereal(x : realVar, y : realVar) returns (__ret : int) {
if (x != y) then 1 else 0
}


// procedure is generated by joogie.
function {:inline true} $instanceof($param00 : ref, $param11 : classConst) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $xorref($param00 : ref, $param11 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $orref($param00 : ref, $param11 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $intarrtoref($param00 : [int]int) returns (__ret : ref);



// procedure is generated by joogie.
function {:inline true} $subreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar);



// procedure is generated by joogie.
function {:inline true} $shlreal($param00 : realVar, $param11 : realVar) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $negInt(x : int) returns (__ret : int) {
if (x == 0) then 1 else 0
}


// procedure is generated by joogie.
function {:inline true} $gereal($param00 : realVar, $param11 : realVar) returns (__ret : int);



	 //  @line: 12
// <TreeLeftmostPath.ObjectList: TreeLeftmostPath.ObjectList createList()>
procedure TreeLeftmostPath.ObjectList$TreeLeftmostPath.ObjectList$createList$2229() returns (__ret : ref) {
var $r18 : ref;
var $r07 : ref;
var i010 : int;
var r29 : ref;
	 //  @line: 13
Block17:
	 //  @line: 13
	r29 := $null;
	 //  @line: 14
	 call i010 := int$TreeLeftmostPath.Random$random$2231();
	 goto Block18;
	 //  @line: 15
Block18:
	 goto Block19, Block21;
	 //  @line: 15
Block19:
	 assume ($leint((i010), (0))==1);
	 goto Block20;
	 //  @line: 15
Block21:
	 //  @line: 15
	 assume ($negInt(($leint((i010), (0))))==1);
	 //  @line: 16
	$r07 := $newvariable((22));
	 assume ($neref(($newvariable((22))), ($null))==1);
	 //  @line: 16
	$r18 := $newvariable((23));
	 assume ($neref(($newvariable((23))), ($null))==1);
	 assert ($neref(($r18), ($null))==1);
	 //  @line: 16
	 call void$java.lang.Object$$la$init$ra$$28(($r18));
	 assert ($neref(($r07), ($null))==1);
	 //  @line: 16
	 call void$TreeLeftmostPath.ObjectList$$la$init$ra$$2228(($r07), ($r18), (r29));
	 //  @line: 16
	r29 := $r07;
	 //  @line: 17
	i010 := $addint((i010), (-1));
	 goto Block18;
	 //  @line: 19
Block20:
	 //  @line: 19
	__ret := r29;
	 return;
}


	 //  @line: 16
// <TreeLeftmostPath.Tree: TreeLeftmostPath.Tree createNode()>
procedure TreeLeftmostPath.Tree$TreeLeftmostPath.Tree$createNode$2457() returns (__ret : ref)
  modifies $HeapVar;
 {
var $r122 : ref;
var $r224 : ref;
var r023 : ref;
	 //  @line: 17
Block29:
	 //  @line: 17
	$r122 := $newvariable((30));
	 assume ($neref(($newvariable((30))), ($null))==1);
	 assert ($neref(($r122), ($null))==1);
	 //  @line: 17
	 call void$TreeLeftmostPath.Tree$$la$init$ra$$2456(($r122));
	 //  @line: 17
	r023 := $r122;
	 //  @line: 18
	$r224 := $newvariable((31));
	 assume ($neref(($newvariable((31))), ($null))==1);
	 assert ($neref(($r224), ($null))==1);
	 //  @line: 18
	 call void$java.lang.Object$$la$init$ra$$28(($r224));
	 assert ($neref((r023), ($null))==1);
	 //  @line: 18
	$HeapVar[r023, java.lang.Object$TreeLeftmostPath.Tree$value300] := $r224;
	 //  @line: 19
	__ret := r023;
	 return;
}


	 //  @line: 4
// <TreeLeftmostPath.Random: void <clinit>()>
procedure void$TreeLeftmostPath.Random$$la$clinit$ra$$2232()
  modifies int$TreeLeftmostPath.Random$index0;
 {
	 //  @line: 5
Block26:
	 //  @line: 5
	int$TreeLeftmostPath.Random$index0 := 0;
	 return;
}


// procedure is generated by joogie.
function {:inline true} $eqref(x : ref, y : ref) returns (__ret : int) {
if (x == y) then 1 else 0
}


// procedure is generated by joogie.
function {:inline true} $cmpint(x : int, y : int) returns (__ret : int) {
if (x < y) then 1 else if (x == y) then 0 else -1
}


// procedure is generated by joogie.
function {:inline true} $andint($param00 : int, $param11 : int) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $andreal($param00 : realVar, $param11 : realVar) returns (__ret : int);



// <java.lang.Object: void <init>()>
procedure void$java.lang.Object$$la$init$ra$$28(__this : ref);



// procedure is generated by joogie.
function {:inline true} $shlint($param00 : int, $param11 : int) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $xorint($param00 : int, $param11 : int) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $subint(x : int, y : int) returns (__ret : int) {
(x - y)
}