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 List$List$tail255 : Field ref;
var java.lang.Object$List$head254 : 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: 37
// <Test6: int length(List)>
procedure int$Test6$length$2231($param_0 : ref) returns (__ret : int) {
var r040 : ref;
var $r142 : ref;
var $i043 : int;
var $i144 : int;
Block43:
	r040 := $param_0;
	 goto Block44;
	 //  @line: 38
Block44:
	 goto Block45, Block47;
	 //  @line: 38
Block45:
	 assume ($neref((r040), ($null))==1);
	 goto Block46;
	 //  @line: 38
Block47:
	 //  @line: 38
	 assume ($negInt(($neref((r040), ($null))))==1);
	 //  @line: 39
	__ret := 0;
	 return;
	 //  @line: 41
Block46:
	 assert ($neref((r040), ($null))==1);
	 //  @line: 41
	 call $r142 := List$List$getTail$2234((r040));
	 goto Block48;
	 //  @line: 41
Block48:
	 //  @line: 41
	 call $i043 := int$Test6$length$2231(($r142));
	 //  @line: 41
	$i144 := $addint((1), ($i043));
	 //  @line: 41
	__ret := $i144;
	 return;
}


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



	 //  @line: 14
// <List: List mk(int)>
procedure List$List$mk$2235($param_0 : int) returns (__ret : ref) {
var i167 : int;
var $i064 : int;
var r268 : ref;
var $r166 : ref;
var $r065 : ref;
Block58:
	i167 := $param_0;
	 //  @line: 15
	r268 := $null;
	 goto Block59;
	 //  @line: 17
Block59:
	 //  @line: 17
	$i064 := i167;
	 //  @line: 17
	i167 := $addint((i167), (-1));
	 goto Block60;
	 //  @line: 17
Block60:
	 goto Block63, Block61;
	 //  @line: 17
Block63:
	 //  @line: 17
	 assume ($negInt(($leint(($i064), (0))))==1);
	 //  @line: 18
	$r065 := $newvariable((64));
	 assume ($neref(($newvariable((64))), ($null))==1);
	 //  @line: 18
	$r166 := $newvariable((65));
	 assume ($neref(($newvariable((65))), ($null))==1);
	 assert ($neref(($r166), ($null))==1);
	 //  @line: 18
	 call void$java.lang.Object$$la$init$ra$$28(($r166));
	 assert ($neref(($r065), ($null))==1);
	 //  @line: 18
	 call void$List$$la$init$ra$$2233(($r065), ($r166), (r268));
	 //  @line: 18
	r268 := $r065;
	 goto Block59;
	 //  @line: 17
Block61:
	 assume ($leint(($i064), (0))==1);
	 goto Block62;
	 //  @line: 20
Block62:
	 //  @line: 20
	__ret := r268;
	 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);



	 //  @line: 4
// <List: void <init>(java.lang.Object,List)>
procedure void$List$$la$init$ra$$2233(__this : ref, $param_0 : ref, $param_1 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r057 : ref;
var r158 : ref;
var r259 : ref;
Block56:
	r057 := __this;
	r158 := $param_0;
	r259 := $param_1;
	 assert ($neref((r057), ($null))==1);
	 //  @line: 5
	 call void$java.lang.Object$$la$init$ra$$28((r057));
	 assert ($neref((r057), ($null))==1);
	 //  @line: 6
	$HeapVar[r057, java.lang.Object$List$head254] := r158;
	 assert ($neref((r057), ($null))==1);
	 //  @line: 7
	$HeapVar[r057, List$List$tail255] := r259;
	 return;
}


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


	 //  @line: 10
// <Test6: void rec(List,List,List)>
procedure void$Test6$rec$2230($param_0 : ref, $param_1 : ref, $param_2 : ref) {
var $i321 : int;
var r133 : ref;
var $i015 : int;
var r234 : ref;
var $i422 : int;
var r032 : ref;
var r537 : ref;
var r436 : ref;
var $i624 : int;
var $i826 : int;
var $i523 : int;
var $i725 : int;
var r638 : ref;
var $i119 : int;
var $i220 : int;
var r335 : ref;

 //temp local variables 
var $freshlocal0 : ref;

Block18:
	r032 := $param_0;
	r133 := $param_1;
	r234 := $param_2;
	 //  @line: 11
	 call $i015 := int$Test6$length$2231((r032));
	 goto Block19;
	 //  @line: 11
Block19:
	 goto Block20, Block22;
	 //  @line: 11
Block20:
	 assume ($gtint(($i015), (0))==1);
	 goto Block21;
	 //  @line: 11
Block22:
	 //  @line: 11
	 assume ($negInt(($gtint(($i015), (0))))==1);
	 return;
	 //  @line: 14
Block21:
	 //  @line: 14
	r335 := r032;
	 goto Block23;
	 //  @line: 15
Block23:
	 //  @line: 15
	r436 := r133;
	 //  @line: 16
	r537 := r234;
	 //  @line: 17
	r638 := r335;
	 //  @line: 19
	 call $i119 := int$Test6$length$2231((r537));
	 //  @line: 19
	$i220 := $modint(($i119), (3));
	 goto Block24;
	 //  @line: 19
Block24:
	 goto Block27, Block25;
	 //  @line: 19
Block27:
	 //  @line: 19
	 assume ($negInt(($neint(($i220), (0))))==1);
	 assert ($neref((r335), ($null))==1);
	 //  @line: 20
	 call $freshlocal0 := List$List$getTail$2234((r335));
	 goto Block26;
	 //  @line: 19
Block25:
	 assume ($neint(($i220), (0))==1);
	 goto Block26;
	 //  @line: 22
Block26:
	 //  @line: 22
	 call $i321 := int$Test6$length$2231((r638));
	 //  @line: 22
	$i422 := $modint(($i321), (5));
	 goto Block28;
	 //  @line: 22
Block28:
	 goto Block29, Block31;
	 //  @line: 22
Block29:
	 assume ($neint(($i422), (0))==1);
	 goto Block30;
	 //  @line: 22
Block31:
	 //  @line: 22
	 assume ($negInt(($neint(($i422), (0))))==1);
	 assert ($neref((r638), ($null))==1);
	 //  @line: 23
	 call r638 := List$List$getTail$2234((r638));
	 goto Block30;
	 //  @line: 25
Block30:
	 //  @line: 25
	 call $i523 := int$Test6$length$2231((r436));
	 //  @line: 25
	 call $i624 := int$Test6$length$2231((r537));
	 goto Block32;
	 //  @line: 25
Block32:
	 goto Block35, Block33;
	 //  @line: 25
Block35:
	 //  @line: 25
	 assume ($negInt(($leint(($i523), ($i624))))==1);
	 assert ($neref((r436), ($null))==1);
	 //  @line: 26
	 call r436 := List$List$getTail$2234((r436));
	 goto Block36;
	 //  @line: 25
Block33:
	 assume ($leint(($i523), ($i624))==1);
	 goto Block34;
	 //  @line: 32
Block36:
	 //  @line: 32
	 call void$Test6$test$2232((r436), (r537), (r638));
	 goto Block42;
	 //  @line: 27
Block34:
	 //  @line: 27
	 call $i725 := int$Test6$length$2231((r436));
	 goto Block37;
	 //  @line: 34
Block42:
	 //  @line: 34
	 call void$Test6$rec$2230((r436), (r537), (r638));
	 return;
	 //  @line: 27
Block37:
	 //  @line: 27
	 call $i826 := int$Test6$length$2231((r537));
	 goto Block38;
	 //  @line: 27
Block38:
	 goto Block41, Block39;
	 //  @line: 27
Block41:
	 //  @line: 27
	 assume ($negInt(($neint(($i725), ($i826))))==1);
	 assert ($neref((r537), ($null))==1);
	 //  @line: 28
	 call r537 := List$List$getTail$2234((r537));
	 goto Block36;
	 //  @line: 27
Block39:
	 assume ($neint(($i725), ($i826))==1);
	 goto Block40;
	 //  @line: 30
Block40:
	 assert ($neref((r638), ($null))==1);
	 //  @line: 30
	 call r638 := List$List$getTail$2234((r638));
	 goto Block36;
}


// <Test6: void <init>()>
procedure void$Test6$$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} $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);



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


	 //  @line: 10
// <List: List getTail()>
procedure List$List$getTail$2234(__this : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var r060 : ref;
var $r161 : ref;
Block57:
	r060 := __this;
	 assert ($neref((r060), ($null))==1);
	 //  @line: 11
	$r161 := $HeapVar[r060, List$List$tail255];
	 //  @line: 11
	__ret := $r161;
	 return;
}


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



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



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


	 //  @line: 44
// <Test6: void test(List,List,List)>
procedure void$Test6$test$2232($param_0 : ref, $param_1 : ref, $param_2 : ref) {
var r251 : ref;
var $r046 : ref;
var r453 : ref;
var r655 : ref;
var r352 : ref;
var r554 : ref;
var $r148 : ref;
var r756 : ref;
Block49:
	r251 := $param_0;
	r352 := $param_1;
	r453 := $param_2;
	 goto Block50;
	 //  @line: 45
Block50:
	 goto Block53, Block51;
	 //  @line: 45
Block53:
	 //  @line: 45
	 assume ($negInt(($eqref((r251), ($null))))==1);
	 //  @line: 46
	$r046 := $newvariable((54));
	 assume ($neref(($newvariable((54))), ($null))==1);
	 assert ($neref(($r046), ($null))==1);
	 //  @line: 46
	 call void$List$$la$init$ra$$2233(($r046), (r251), (r352));
	 //  @line: 46
	r554 := $r046;
	 //  @line: 47
	$r148 := $newvariable((55));
	 assume ($neref(($newvariable((55))), ($null))==1);
	 assert ($neref(($r148), ($null))==1);
	 //  @line: 47
	 call void$List$$la$init$ra$$2233(($r148), (r554), (r453));
	 //  @line: 47
	r655 := $r148;
	 assert ($neref((r251), ($null))==1);
	 //  @line: 48
	 call r756 := List$List$getTail$2234((r251));
	 //  @line: 49
	 call void$Test6$test$2232((r756), (r554), (r655));
	 goto Block52;
	 //  @line: 45
Block51:
	 assume ($eqref((r251), ($null))==1);
	 goto Block52;
	 //  @line: 51
Block52:
	 return;
}


// 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: 2
// <Test6: void main(java.lang.String[])>
procedure void$Test6$main$2229($param_0 : [int]ref) {
var r15 : ref;
var $i16 : int;
var $i411 : int;
var $i310 : int;
var r313 : ref;
var $i03 : int;
var r02 : [int]ref;
var $i27 : int;
var r29 : ref;
Block17:
	r02 := $param_0;
	 //  @line: 3
	$i03 := $refArrSize[r02[$arrSizeIdx]];
	 //  @line: 3
	 call r15 := List$List$mk$2235(($i03));
	 //  @line: 4
	$i16 := $refArrSize[r02[$arrSizeIdx]];
	 //  @line: 4
	$i27 := $addint(($i16), (3));
	 //  @line: 4
	 call r29 := List$List$mk$2235(($i27));
	 //  @line: 5
	$i310 := $refArrSize[r02[$arrSizeIdx]];
	 //  @line: 5
	$i411 := $addint(($i310), (5));
	 //  @line: 5
	 call r313 := List$List$mk$2235(($i411));
	 //  @line: 7
	 call void$Test6$rec$2230((r15), (r29), (r313));
	 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);



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