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$n254 : 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);



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



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


	 //  @line: 25
// <List: List createList(int,List)>
procedure List$List$createList$2230($param_0 : int, $param_1 : ref) returns (__ret : ref) {
var r112 : ref;
var $r010 : ref;
var i011 : int;
Block22:
	i011 := $param_0;
	r112 := $param_1;
	 goto Block23;
	 //  @line: 26
Block23:
	 //  @line: 26
	i011 := $addint((i011), (-1));
	 goto Block24;
	 //  @line: 26
Block24:
	 goto Block27, Block25;
	 //  @line: 26
Block27:
	 //  @line: 26
	 assume ($negInt(($leint((i011), (0))))==1);
	 //  @line: 27
	$r010 := $newvariable((28));
	 assume ($neref(($newvariable((28))), ($null))==1);
	 assert ($neref(($r010), ($null))==1);
	 //  @line: 27
	 call void$List$$la$init$ra$$2228(($r010), (r112));
	 //  @line: 27
	r112 := $r010;
	 goto Block23;
	 //  @line: 26
Block25:
	 assume ($leint((i011), (0))==1);
	 goto Block26;
	 //  @line: 29
Block26:
	 //  @line: 29
	__ret := r112;
	 return;
}


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


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



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



	 //  @line: 15
// <List: void reverse(List)>
procedure void$List$reverse$2229($param_0 : ref)
  modifies $HeapVar;
 {
var r27 : ref;
var r16 : ref;
var r05 : ref;
Block17:
	r16 := $param_0;
	 //  @line: 16
	r27 := $null;
	 goto Block18;
	 //  @line: 17
Block18:
	 goto Block21, Block19;
	 //  @line: 17
Block21:
	 //  @line: 17
	 assume ($negInt(($eqref((r16), ($null))))==1);
	 //  @line: 18
	r05 := r16;
	 assert ($neref((r16), ($null))==1);
	 //  @line: 19
	r16 := $HeapVar[r16, List$List$n254];
	 assert ($neref((r05), ($null))==1);
	 //  @line: 20
	$HeapVar[r05, List$List$n254] := r27;
	 //  @line: 21
	r27 := r05;
	 goto Block18;
	 //  @line: 17
Block19:
	 assume ($eqref((r16), ($null))==1);
	 goto Block20;
	 //  @line: 23
Block20:
	 return;
}


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



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



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


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



// <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} $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
// <List: void <init>(List)>
procedure void$List$$la$init$ra$$2228(__this : ref, $param_0 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r01 : ref;
var r12 : ref;
Block16:
	r01 := __this;
	r12 := $param_0;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 11
	 call void$java.lang.Object$$la$init$ra$$28((r01));
	 assert ($neref((r01), ($null))==1);
	 //  @line: 12
	$HeapVar[r01, List$List$n254] := r12;
	 return;
}


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


	 //  @line: 32
// <List: List createCycle(int)>
procedure List$List$createCycle$2231($param_0 : int) returns (__ret : ref)
  modifies $HeapVar;
 {
var r118 : ref;
var i015 : int;
var $i116 : int;
var $r213 : ref;
var r014 : ref;
Block29:
	i015 := $param_0;
	 //  @line: 33
	$r213 := $newvariable((30));
	 assume ($neref(($newvariable((30))), ($null))==1);
	 assert ($neref(($r213), ($null))==1);
	 //  @line: 33
	 call void$List$$la$init$ra$$2228(($r213), ($null));
	 //  @line: 33
	r014 := $r213;
	 //  @line: 34
	$i116 := $subint((i015), (1));
	 //  @line: 34
	 call r118 := List$List$createList$2230(($i116), (r014));
	 assert ($neref((r014), ($null))==1);
	 //  @line: 35
	$HeapVar[r014, List$List$n254] := r118;
	 //  @line: 36
	__ret := r118;
	 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);



	 //  @line: 39
// <List: List createPanhandleList(int,int)>
procedure List$List$createPanhandleList$2232($param_0 : int, $param_1 : int) returns (__ret : ref) {
var $r021 : ref;
var i120 : int;
var $r122 : ref;
var i019 : int;
Block31:
	i019 := $param_0;
	i120 := $param_1;
	 //  @line: 40
	 call $r021 := List$List$createCycle$2231((i120));
	 //  @line: 40
	 call $r122 := List$List$createList$2230((i019), ($r021));
	 //  @line: 40
	__ret := $r122;
	 return;
}


	 //  @line: 2
// <ListReverseCyclicList: void main(java.lang.String[])>
procedure void$ListReverseCyclicList$main$2234($param_0 : [int]ref)
  modifies $stringSize;
 {
var $r225 : ref;
var r128 : ref;
var r024 : [int]ref;
var $i026 : int;
Block33:
	r024 := $param_0;
	 assert ($geint((0), (0))==1);
	 assert ($ltint((0), ($refArrSize[r024[$arrSizeIdx]]))==1);
	 //  @line: 3
	$r225 := r024[0];
	$i026 := $stringSize[$r225];
	 //  @line: 3
	 call r128 := List$List$createCycle$2231(($i026));
	 //  @line: 4
	 call void$List$reverse$2229((r128));
	 return;
}


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