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 





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



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



	 //  @line: 14
// <Recursions: void rec1(int,int,int)>
procedure void$Recursions$rec1$2231($param_0 : int, $param_1 : int, $param_2 : int) {
var $i314 : int;
var $i415 : int;
var i213 : int;
var i011 : int;
var i112 : int;
Block28:
	i011 := $param_0;
	i112 := $param_1;
	i213 := $param_2;
	 goto Block29;
	 //  @line: 15
Block29:
	 goto Block32, Block30;
	 //  @line: 15
Block32:
	 //  @line: 15
	 assume ($negInt(($gtint((i011), (i112))))==1);
	 //  @line: 16
	$i314 := $addint((i213), (i011));
	 //  @line: 16
	 call void$Recursions$rec2$2232(($i314), (0), (i213), (i011));
	 //  @line: 17
	$i415 := $addint((i011), (1));
	 //  @line: 17
	 call void$Recursions$rec1$2231(($i415), (i112), (i213));
	 goto Block31;
	 //  @line: 15
Block30:
	 assume ($gtint((i011), (i112))==1);
	 goto Block31;
	 //  @line: 19
Block31:
	 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);



	 //  @line: 7
// <Recursions: void rec0(int,int)>
procedure void$Recursions$rec0$2230($param_0 : int, $param_1 : int) {
var $i29 : int;
var $i310 : int;
var i18 : int;
var i07 : int;
Block23:
	i07 := $param_0;
	i18 := $param_1;
	 goto Block24;
	 //  @line: 8
Block24:
	 goto Block27, Block25;
	 //  @line: 8
Block27:
	 //  @line: 8
	 assume ($negInt(($gtint((i07), (i18))))==1);
	 //  @line: 9
	$i29 := $mulint((2), (i07));
	 //  @line: 9
	 call void$Recursions$rec1$2231((0), ($i29), (i07));
	 //  @line: 10
	$i310 := $addint((i07), (1));
	 //  @line: 10
	 call void$Recursions$rec0$2230(($i310), (i18));
	 goto Block26;
	 //  @line: 8
Block25:
	 assume ($gtint((i07), (i18))==1);
	 goto Block26;
	 //  @line: 12
Block26:
	 return;
}


// 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: 35
// <Recursions: void rec4(int,int)>
procedure void$Recursions$rec4$2234($param_0 : int, $param_1 : int) {
var i139 : int;
var i038 : int;
var $i240 : int;
Block43:
	i038 := $param_0;
	i139 := $param_1;
	 goto Block44;
	 //  @line: 36
Block44:
	 goto Block47, Block45;
	 //  @line: 36
Block47:
	 //  @line: 36
	 assume ($negInt(($ltint((i038), (i139))))==1);
	 //  @line: 37
	$i240 := $subint((i038), (1));
	 //  @line: 37
	 call void$Recursions$rec4$2234(($i240), (i139));
	 goto Block46;
	 //  @line: 36
Block45:
	 assume ($ltint((i038), (i139))==1);
	 goto Block46;
	 //  @line: 38
Block46:
	 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);



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



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



	 //  @line: 2
// <Recursions: void main(java.lang.String[])>
procedure void$Recursions$main$2229($param_0 : [int]ref) {
var i26 : int;
var $i15 : int;
var $i04 : int;
var r03 : [int]ref;
Block17:
	r03 := $param_0;
	 //  @line: 3
	i26 := 0;
	 goto Block18;
	 //  @line: 3
Block18:
	 //  @line: 3
	$i04 := $refArrSize[r03[$arrSizeIdx]];
	 goto Block19;
	 //  @line: 3
Block19:
	 goto Block20, Block22;
	 //  @line: 3
Block20:
	 assume ($geint((i26), ($i04))==1);
	 goto Block21;
	 //  @line: 3
Block22:
	 //  @line: 3
	 assume ($negInt(($geint((i26), ($i04))))==1);
	 //  @line: 4
	$i15 := $refArrSize[r03[$arrSizeIdx]];
	 //  @line: 4
	 call void$Recursions$rec0$2230((0), ($i15));
	 //  @line: 3
	i26 := $addint((i26), (1));
	 goto Block18;
	 //  @line: 5
Block21:
	 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);



// <Recursions: void <init>()>
procedure void$Recursions$$la$init$ra$$2228(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r01 : ref;
Block16:
	r01 := __this;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 1
	 call void$java.lang.Object$$la$init$ra$$28((r01));
	 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);



	 //  @line: 28
// <Recursions: void rec3(int,int,int,int,int)>
procedure void$Recursions$rec3$2233($param_0 : int, $param_1 : int, $param_2 : int, $param_3 : int, $param_4 : int) {
var $i834 : int;
var $i935 : int;
var i026 : int;
var i228 : int;
var $i631 : int;
var $i530 : int;
var i127 : int;
var i329 : int;
var $i733 : int;
var $i1036 : int;
var i432 : int;
var $i1137 : int;
Block38:
	i026 := $param_0;
	i127 := $param_1;
	i228 := $param_2;
	i329 := $param_3;
	i432 := $param_4;
	 goto Block39;
	 //  @line: 29
Block39:
	 goto Block40, Block42;
	 //  @line: 29
Block40:
	 assume ($gtint((i026), (i127))==1);
	 goto Block41;
	 //  @line: 29
Block42:
	 //  @line: 29
	 assume ($negInt(($gtint((i026), (i127))))==1);
	 //  @line: 30
	$i631 := $mulint((1000), (i228));
	 //  @line: 30
	$i530 := $mulint((100), (i329));
	 //  @line: 30
	$i834 := $addint(($i631), ($i530));
	 //  @line: 30
	$i733 := $mulint((10), (i432));
	 //  @line: 30
	$i935 := $addint(($i834), ($i733));
	 //  @line: 30
	$i1036 := $addint(($i935), (i026));
	 //  @line: 30
	 call void$Recursions$rec4$2234(($i1036), (0));
	 //  @line: 31
	$i1137 := $addint((i026), (1));
	 //  @line: 31
	 call void$Recursions$rec3$2233(($i1137), (i127), (i228), (i329), (i432));
	 goto Block41;
	 //  @line: 33
Block41:
	 return;
}


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


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



// procedure is generated by joogie.
function {:inline true} $lereal($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} $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);



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



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



	 //  @line: 21
// <Recursions: void rec2(int,int,int,int)>
procedure void$Recursions$rec2$2232($param_0 : int, $param_1 : int, $param_2 : int, $param_3 : int) {
var $i925 : int;
var i319 : int;
var i117 : int;
var $i622 : int;
var $i824 : int;
var $i723 : int;
var $i420 : int;
var i218 : int;
var i016 : int;
var $i521 : int;
Block33:
	i016 := $param_0;
	i117 := $param_1;
	i218 := $param_2;
	i319 := $param_3;
	 goto Block34;
	 //  @line: 22
Block34:
	 goto Block37, Block35;
	 //  @line: 22
Block37:
	 //  @line: 22
	 assume ($negInt(($ltint((i016), (i117))))==1);
	 //  @line: 23
	$i521 := $mulint((2), (i218));
	 //  @line: 23
	$i420 := $mulint((3), (i319));
	 //  @line: 23
	$i723 := $addint(($i521), ($i420));
	 //  @line: 23
	$i622 := $mulint((4), (i016));
	 //  @line: 23
	$i824 := $addint(($i723), ($i622));
	 //  @line: 23
	 call void$Recursions$rec3$2233((0), ($i824), (i218), (i319), (i016));
	 //  @line: 24
	$i925 := $subint((i016), (1));
	 //  @line: 24
	 call void$Recursions$rec2$2232(($i925), (i117), (i218), (i319));
	 goto Block36;
	 //  @line: 22
Block35:
	 assume ($ltint((i016), (i117))==1);
	 goto Block36;
	 //  @line: 26
Block36:
	 return;
}


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