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 int$Random$index0 : int;
var List$List$next255 : Field ref;
var Tree$Tree$left256 : Field ref;
var java.lang.String$lp$$rp$$Random$args259 : [int]ref;
var Tree$Tree$right257 : Field ref;
var Tree$List$value254 : 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: 14
// <Tree: Tree createNode()>
procedure Tree$Tree$createNode$2231() returns (__ret : ref) {
var $i08 : int;
var $r19 : ref;
var r010 : ref;
	 //  @line: 15
Block19:
	 //  @line: 15
	 call $i08 := int$Random$random$2238();
	 goto Block20;
	 //  @line: 15
Block20:
	 goto Block21, Block23;
	 //  @line: 15
Block21:
	 assume ($neint(($i08), (0))==1);
	 goto Block22;
	 //  @line: 15
Block23:
	 //  @line: 15
	 assume ($negInt(($neint(($i08), (0))))==1);
	 //  @line: 16
	__ret := $null;
	 return;
	 //  @line: 18
Block22:
	 //  @line: 18
	$r19 := $newvariable((24));
	 assume ($neref(($newvariable((24))), ($null))==1);
	 goto Block25;
	 //  @line: 18
Block25:
	 assert ($neref(($r19), ($null))==1);
	 //  @line: 18
	 call void$Tree$$la$init$ra$$2230(($r19));
	 //  @line: 18
	r010 := $r19;
	 //  @line: 19
	__ret := r010;
	 return;
}


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



	 //  @line: 5
// <Tree: void <init>(Tree,Tree)>
procedure void$Tree$$la$init$ra$$2229(__this : ref, $param_0 : ref, $param_1 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r26 : ref;
var r04 : ref;
var r15 : ref;
Block17:
	r04 := __this;
	r15 := $param_0;
	r26 := $param_1;
	 assert ($neref((r04), ($null))==1);
	 //  @line: 6
	 call void$java.lang.Object$$la$init$ra$$28((r04));
	 assert ($neref((r04), ($null))==1);
	 //  @line: 7
	$HeapVar[r04, Tree$Tree$left256] := r15;
	 assert ($neref((r04), ($null))==1);
	 //  @line: 8
	$HeapVar[r04, Tree$Tree$right257] := r26;
	 return;
}


	 //  @line: 10
// <Tree: void <init>()>
procedure void$Tree$$la$init$ra$$2230(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r07 : ref;
Block18:
	r07 := __this;
	 assert ($neref((r07), ($null))==1);
	 //  @line: 11
	 call void$java.lang.Object$$la$init$ra$$28((r07));
	 return;
}


// <Random: void <init>()>
procedure void$Random$$la$init$ra$$2237(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r038 : ref;
Block49:
	r038 := __this;
	 assert ($neref((r038), ($null))==1);
	 //  @line: 1
	 call void$java.lang.Object$$la$init$ra$$28((r038));
	 return;
}


// 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);



// 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);



// 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
}


// 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);



// <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} $xorreal($param00 : realVar, $param11 : realVar) returns (__ret : int);



	 //  @line: 5
// <Random: int random()>
procedure int$Random$random$2238() returns (__ret : int)
  modifies $stringSize, int$Random$index0;
 {
var $i344 : int;
var $r140 : [int]ref;
var $i142 : int;
var $i039 : int;
var $i243 : int;
var r041 : ref;
	 //  @line: 6
Block50:
	 //  @line: 6
	$r140 := java.lang.String$lp$$rp$$Random$args259;
	 //  @line: 6
	$i039 := int$Random$index0;
	 assert ($geint(($i039), (0))==1);
	 assert ($ltint(($i039), ($refArrSize[$r140[$arrSizeIdx]]))==1);
	 //  @line: 6
	r041 := $r140[$i039];
	 //  @line: 7
	$i142 := int$Random$index0;
	 //  @line: 7
	$i243 := $addint(($i142), (1));
	 //  @line: 7
	int$Random$index0 := $i243;
	$i344 := $stringSize[r041];
	 //  @line: 8
	__ret := $i344;
	 return;
}


// 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);



// 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);



// <MirrorTree: void <init>()>
procedure void$MirrorTree$$la$init$ra$$2234(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r029 : ref;
Block42:
	r029 := __this;
	 assert ($neref((r029), ($null))==1);
	 //  @line: 1
	 call void$java.lang.Object$$la$init$ra$$28((r029));
	 return;
}


// 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);



// 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
}


	 //  @line: 22
// <Tree: Tree createTree()>
procedure Tree$Tree$createTree$2232() returns (__ret : ref)
  modifies $HeapVar;
 {
var r724 : ref;
var r321 : ref;
var r826 : ref;
var r117 : ref;
var r012 : ref;
var i025 : int;
var $r413 : ref;
var r219 : ref;
var $r522 : ref;
var $r623 : ref;
	 //  @line: 23
Block26:
	 //  @line: 23
	 call r012 := Tree$Tree$createNode$2231();
	 //  @line: 24
	$r413 := $newvariable((27));
	 assume ($neref(($newvariable((27))), ($null))==1);
	 assert ($neref(($r413), ($null))==1);
	 //  @line: 24
	 call void$List$$la$init$ra$$2228(($r413), (r012), ($null));
	 //  @line: 24
	r724 := $r413;
	 //  @line: 26
	 call i025 := int$Random$random$2238();
	 goto Block28;
	 //  @line: 27
Block28:
	 goto Block29, Block31;
	 //  @line: 27
Block29:
	 assume ($leint((i025), (0))==1);
	 goto Block30;
	 //  @line: 27
Block31:
	 //  @line: 27
	 assume ($negInt(($leint((i025), (0))))==1);
	 goto Block32;
	 //  @line: 43
Block30:
	 //  @line: 43
	__ret := r012;
	 return;
	 //  @line: 43
Block32:
	 goto Block34, Block33;
	 //  @line: 43
Block34:
	 //  @line: 43
	 assume ($negInt(($eqref((r724), ($null))))==1);
	 assert ($neref((r724), ($null))==1);
	 //  @line: 28
	r117 := $HeapVar[r724, Tree$List$value254];
	 assert ($neref((r724), ($null))==1);
	 //  @line: 29
	r724 := $HeapVar[r724, List$List$next255];
	 goto Block35;
	 //  @line: 43
Block33:
	 assume ($eqref((r724), ($null))==1);
	 goto Block30;
	 //  @line: 31
Block35:
	 goto Block36, Block38;
	 //  @line: 31
Block36:
	 assume ($eqref((r117), ($null))==1);
	 goto Block37;
	 //  @line: 31
Block38:
	 //  @line: 31
	 assume ($negInt(($eqref((r117), ($null))))==1);
	 //  @line: 32
	 call r219 := Tree$Tree$createNode$2231();
	 //  @line: 33
	 call r321 := Tree$Tree$createNode$2231();
	 assert ($neref((r117), ($null))==1);
	 //  @line: 34
	$HeapVar[r117, Tree$Tree$left256] := r219;
	 assert ($neref((r117), ($null))==1);
	 //  @line: 35
	$HeapVar[r117, Tree$Tree$right257] := r321;
	 //  @line: 36
	$r522 := $newvariable((39));
	 assume ($neref(($newvariable((39))), ($null))==1);
	 assert ($neref(($r522), ($null))==1);
	 //  @line: 36
	 call void$List$$la$init$ra$$2228(($r522), (r219), (r724));
	 //  @line: 36
	r826 := $r522;
	 //  @line: 37
	$r623 := $newvariable((40));
	 assume ($neref(($newvariable((40))), ($null))==1);
	 assert ($neref(($r623), ($null))==1);
	 //  @line: 37
	 call void$List$$la$init$ra$$2228(($r623), (r321), (r826));
	 //  @line: 37
	r724 := $r623;
	 goto Block37;
	 //  @line: 40
Block37:
	 //  @line: 40
	i025 := $addint((i025), (-1));
	 goto Block28;
}


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



// 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);



	 //  @line: 46
// <Tree: void main(java.lang.String[])>
procedure void$Tree$main$2233($param_0 : [int]ref)
  modifies $stringSize, java.lang.String$lp$$rp$$Random$args259;
 {
var r027 : [int]ref;

 //temp local variables 
var $freshlocal0 : ref;

Block41:
	r027 := $param_0;
	 //  @line: 47
	java.lang.String$lp$$rp$$Random$args259 := r027;
	 //  @line: 48
	 call $freshlocal0 := Tree$Tree$createTree$2232();
	 return;
}


// 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);



	 //  @line: 2
// <Random: void <clinit>()>
procedure void$Random$$la$clinit$ra$$2239()
  modifies int$Random$index0;
 {
	 //  @line: 3
Block51:
	 //  @line: 3
	int$Random$index0 := 0;
	 return;
}


// 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: 10
// <MirrorTree: void mirror(Tree)>
procedure void$MirrorTree$mirror$2236($param_0 : ref)
  modifies $HeapVar;
 {
var r033 : ref;
var r337 : ref;
var r135 : ref;
var $r236 : ref;
Block44:
	r033 := $param_0;
	 //  @line: 11
	r337 := r033;
	 goto Block45;
	 //  @line: 12
Block45:
	 goto Block48, Block46;
	 //  @line: 12
Block48:
	 //  @line: 12
	 assume ($negInt(($eqref((r337), ($null))))==1);
	 assert ($neref((r337), ($null))==1);
	 //  @line: 13
	r135 := $HeapVar[r337, Tree$Tree$left256];
	 assert ($neref((r337), ($null))==1);
	 //  @line: 14
	$r236 := $HeapVar[r337, Tree$Tree$right257];
	 assert ($neref((r337), ($null))==1);
	 //  @line: 14
	$HeapVar[r337, Tree$Tree$left256] := $r236;
	 assert ($neref((r337), ($null))==1);
	 //  @line: 15
	$HeapVar[r337, Tree$Tree$right257] := r135;
	 assert ($neref((r337), ($null))==1);
	 //  @line: 16
	r337 := $HeapVar[r337, Tree$Tree$right257];
	 goto Block45;
	 //  @line: 12
Block46:
	 assume ($eqref((r337), ($null))==1);
	 goto Block47;
	 //  @line: 18
Block47:
	 return;
}


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



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


	 //  @line: 4
// <List: void <init>(Tree,List)>
procedure void$List$$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: 5
	 call void$java.lang.Object$$la$init$ra$$28((r01));
	 assert ($neref((r01), ($null))==1);
	 //  @line: 6
	$HeapVar[r01, Tree$List$value254] := r12;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 7
	$HeapVar[r01, List$List$next255] := r23;
	 return;
}


	 //  @line: 2
// <MirrorTree: void main(java.lang.String[])>
procedure void$MirrorTree$main$2235($param_0 : [int]ref)
  modifies $stringSize, java.lang.String$lp$$rp$$Random$args259;
 {
var r030 : [int]ref;
var r132 : ref;
Block43:
	r030 := $param_0;
	 //  @line: 3
	java.lang.String$lp$$rp$$Random$args259 := r030;
	 //  @line: 4
	 call r132 := Tree$Tree$createTree$2232();
	 //  @line: 7
	 call void$MirrorTree$mirror$2236((r132));
	 return;
}


// 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);



// 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)
}