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$ListInt$head0 : Field int;
var ListInt$ListInt$tail254 : 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);



	 //  @line: 57
// <ListInt: ListInt merge(ListInt)>
procedure ListInt$ListInt$merge$2234(__this : ref, $param_0 : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var r047 : ref;
var $r351 : ref;
var $r554 : ref;
var $r858 : ref;
var $r250 : ref;
var $i252 : int;
var $i149 : int;
var $r757 : ref;
var $i459 : int;
var r146 : ref;
var $r960 : ref;
var $i356 : int;
var $r453 : ref;
var $r655 : ref;
var $i048 : int;
Block50:
	r047 := __this;
	r146 := $param_0;
	 goto Block51;
	 //  @line: 58
Block51:
	 goto Block52, Block54;
	 //  @line: 58
Block52:
	 assume ($neref((r146), ($null))==1);
	 goto Block53;
	 //  @line: 58
Block54:
	 //  @line: 58
	 assume ($negInt(($neref((r146), ($null))))==1);
	 //  @line: 61
	__ret := r047;
	 return;
	 //  @line: 59
Block53:
	 assert ($neref((r047), ($null))==1);
	 //  @line: 59
	$i149 := $HeapVar[r047, int$ListInt$head0];
	 goto Block55;
	 //  @line: 59
Block55:
	 assert ($neref((r146), ($null))==1);
	 //  @line: 59
	$i048 := $HeapVar[r146, int$ListInt$head0];
	 goto Block56;
	 //  @line: 59
Block56:
	 goto Block57, Block59;
	 //  @line: 59
Block57:
	 assume ($gtint(($i149), ($i048))==1);
	 goto Block58;
	 //  @line: 59
Block59:
	 //  @line: 59
	 assume ($negInt(($gtint(($i149), ($i048))))==1);
	 assert ($neref((r047), ($null))==1);
	 //  @line: 60
	$r554 := $HeapVar[r047, ListInt$ListInt$tail254];
	 goto Block60;
	 //  @line: 62
Block58:
	 //  @line: 62
	$r250 := $newvariable((67));
	 assume ($neref(($newvariable((67))), ($null))==1);
	 goto Block68;
	 //  @line: 60
Block60:
	 goto Block61, Block63;
	 //  @line: 62
Block68:
	 assert ($neref((r146), ($null))==1);
	 //  @line: 62
	$i252 := $HeapVar[r146, int$ListInt$head0];
	 assert ($neref((r146), ($null))==1);
	 //  @line: 62
	$r351 := $HeapVar[r146, ListInt$ListInt$tail254];
	 assert ($neref((r047), ($null))==1);
	 //  @line: 62
	 call $r453 := ListInt$ListInt$merge$2234((r047), ($r351));
	 assert ($neref(($r250), ($null))==1);
	 //  @line: 62
	 call void$ListInt$$la$init$ra$$2229(($r250), ($i252), ($r453));
	 //  @line: 62
	__ret := $r250;
	 return;
	 //  @line: 60
Block61:
	 assume ($eqref(($r554), ($null))==1);
	 goto Block62;
	 //  @line: 60
Block63:
	 //  @line: 60
	 assume ($negInt(($eqref(($r554), ($null))))==1);
	 //  @line: 61
	$r757 := $newvariable((64));
	 assume ($neref(($newvariable((64))), ($null))==1);
	 assert ($neref((r047), ($null))==1);
	 //  @line: 61
	$i459 := $HeapVar[r047, int$ListInt$head0];
	 assert ($neref((r047), ($null))==1);
	 //  @line: 61
	$r858 := $HeapVar[r047, ListInt$ListInt$tail254];
	 assert ($neref(($r858), ($null))==1);
	 //  @line: 61
	 call $r960 := ListInt$ListInt$merge$2234(($r858), (r146));
	 assert ($neref(($r757), ($null))==1);
	 //  @line: 61
	 call void$ListInt$$la$init$ra$$2229(($r757), ($i459), ($r960));
	 //  @line: 61
	__ret := $r757;
	 return;
	 //  @line: 61
Block62:
	 //  @line: 61
	$r655 := $newvariable((65));
	 assume ($neref(($newvariable((65))), ($null))==1);
	 goto Block66;
	 //  @line: 61
Block66:
	 assert ($neref((r047), ($null))==1);
	 //  @line: 61
	$i356 := $HeapVar[r047, int$ListInt$head0];
	 assert ($neref(($r655), ($null))==1);
	 //  @line: 61
	 call void$ListInt$$la$init$ra$$2229(($r655), ($i356), (r146));
	 //  @line: 61
	__ret := $r655;
	 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
}


	 //  @line: 42
// <ListInt: ListInt append(ListInt)>
procedure ListInt$ListInt$append$2231(__this : ref, $param_0 : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var r021 : ref;
var $r222 : ref;
var $i026 : int;
var r124 : ref;
var $r425 : ref;
var $r527 : ref;
var $r323 : ref;
var $r628 : ref;
var $i129 : int;
Block27:
	r021 := __this;
	r124 := $param_0;
	 assert ($neref((r021), ($null))==1);
	 //  @line: 43
	$r222 := $HeapVar[r021, ListInt$ListInt$tail254];
	 goto Block28;
	 //  @line: 43
Block28:
	 goto Block29, Block31;
	 //  @line: 43
Block29:
	 assume ($neref(($r222), ($null))==1);
	 goto Block30;
	 //  @line: 43
Block31:
	 //  @line: 43
	 assume ($negInt(($neref(($r222), ($null))))==1);
	 //  @line: 44
	$r628 := $newvariable((32));
	 assume ($neref(($newvariable((32))), ($null))==1);
	 assert ($neref((r021), ($null))==1);
	 //  @line: 44
	$i129 := $HeapVar[r021, int$ListInt$head0];
	 assert ($neref(($r628), ($null))==1);
	 //  @line: 44
	 call void$ListInt$$la$init$ra$$2229(($r628), ($i129), (r124));
	 //  @line: 44
	__ret := $r628;
	 return;
	 //  @line: 44
Block30:
	 //  @line: 44
	$r323 := $newvariable((33));
	 assume ($neref(($newvariable((33))), ($null))==1);
	 goto Block34;
	 //  @line: 44
Block34:
	 assert ($neref((r021), ($null))==1);
	 //  @line: 44
	$i026 := $HeapVar[r021, int$ListInt$head0];
	 assert ($neref((r021), ($null))==1);
	 //  @line: 44
	$r425 := $HeapVar[r021, ListInt$ListInt$tail254];
	 assert ($neref(($r425), ($null))==1);
	 //  @line: 44
	 call $r527 := ListInt$ListInt$append$2231(($r425), (r124));
	 assert ($neref(($r323), ($null))==1);
	 //  @line: 44
	 call void$ListInt$$la$init$ra$$2229(($r323), ($i026), ($r527));
	 //  @line: 44
	__ret := $r323;
	 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);



	 //  @line: 21
// <ListInt: void main(java.lang.String[])>
procedure void$ListInt$main$2228($param_0 : [int]ref)
  modifies $HeapVar;
 {
var r014 : [int]ref;
var $r55 : ref;
var $r31 : ref;
var $r42 : ref;
var r14 : ref;
var r28 : ref;
var $r66 : ref;
var $r810 : ref;

 //temp local variables 
var $freshlocal2 : ref;
var $freshlocal0 : ref;
var $freshlocal1 : ref;
var $freshlocal3 : ref;

Block16:
	r014 := $param_0;
	 //  @line: 22
	$r31 := $newvariable((17));
	 assume ($neref(($newvariable((17))), ($null))==1);
	 //  @line: 22
	$r42 := $newvariable((18));
	 assume ($neref(($newvariable((18))), ($null))==1);
	 assert ($neref(($r42), ($null))==1);
	 //  @line: 22
	 call void$ListInt$$la$init$ra$$2229(($r42), (6), ($null));
	 assert ($neref(($r31), ($null))==1);
	 //  @line: 22
	 call void$ListInt$$la$init$ra$$2229(($r31), (5), ($r42));
	 //  @line: 22
	r14 := $r31;
	 //  @line: 23
	$r55 := $newvariable((19));
	 assume ($neref(($newvariable((19))), ($null))==1);
	 //  @line: 23
	$r66 := $newvariable((20));
	 assume ($neref(($newvariable((20))), ($null))==1);
	 assert ($neref(($r66), ($null))==1);
	 //  @line: 23
	 call void$ListInt$$la$init$ra$$2229(($r66), (3), ($null));
	 assert ($neref(($r55), ($null))==1);
	 //  @line: 23
	 call void$ListInt$$la$init$ra$$2229(($r55), (1), ($r66));
	 //  @line: 23
	r28 := $r55;
	 assert ($neref((r14), ($null))==1);
	 //  @line: 24
	 call $freshlocal0 := ListInt$ListInt$merge$2234((r14), (r28));
	 assert ($neref((r28), ($null))==1);
	 //  @line: 25
	$r810 := $HeapVar[r28, ListInt$ListInt$tail254];
	 assert ($neref(($r810), ($null))==1);
	 //  @line: 25
	$HeapVar[$r810, ListInt$ListInt$tail254] := r28;
	 assert ($neref((r14), ($null))==1);
	 //  @line: 27
	 call $freshlocal1 := ListInt$ListInt$append$2231((r14), (r28));
	 assert ($neref((r14), ($null))==1);
	 //  @line: 28
	 call void$ListInt$iter$2230((r14));
	 assert ($neref((r14), ($null))==1);
	 //  @line: 29
	 call $freshlocal2 := ListInt$ListInt$reverseAcc$2232((r14), ($null));
	 assert ($neref((r14), ($null))==1);
	 //  @line: 30
	 call $freshlocal3 := ListInt$ListInt$reverse$2233((r14));
	 return;
}


	 //  @line: 32
// <ListInt: void <init>(int,ListInt)>
procedure void$ListInt$$la$init$ra$$2229(__this : ref, $param_0 : int, $param_1 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r117 : ref;
var i016 : int;
var r015 : ref;
Block21:
	r015 := __this;
	i016 := $param_0;
	r117 := $param_1;
	 assert ($neref((r015), ($null))==1);
	 //  @line: 33
	 call void$java.lang.Object$$la$init$ra$$28((r015));
	 assert ($neref((r015), ($null))==1);
	 //  @line: 34
	$HeapVar[r015, int$ListInt$head0] := i016;
	 assert ($neref((r015), ($null))==1);
	 //  @line: 35
	$HeapVar[r015, ListInt$ListInt$tail254] := r117;
	 return;
}


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



	 //  @line: 52
// <ListInt: ListInt reverse()>
procedure ListInt$ListInt$reverse$2233(__this : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $r140 : ref;
var $i044 : int;
var $r342 : ref;
var r039 : ref;
var $r545 : ref;
var $r241 : ref;
var $r443 : ref;
Block43:
	r039 := __this;
	 assert ($neref((r039), ($null))==1);
	 //  @line: 53
	$r140 := $HeapVar[r039, ListInt$ListInt$tail254];
	 goto Block44;
	 //  @line: 53
Block44:
	 goto Block45, Block47;
	 //  @line: 53
Block45:
	 assume ($neref(($r140), ($null))==1);
	 goto Block46;
	 //  @line: 53
Block47:
	 //  @line: 53
	 assume ($negInt(($neref(($r140), ($null))))==1);
	 //  @line: 54
	__ret := r039;
	 return;
	 //  @line: 54
Block46:
	 assert ($neref((r039), ($null))==1);
	 //  @line: 54
	$r241 := $HeapVar[r039, ListInt$ListInt$tail254];
	 goto Block48;
	 //  @line: 54
Block48:
	 assert ($neref(($r241), ($null))==1);
	 //  @line: 54
	 call $r342 := ListInt$ListInt$reverse$2233(($r241));
	 //  @line: 54
	$r443 := $newvariable((49));
	 assume ($neref(($newvariable((49))), ($null))==1);
	 assert ($neref((r039), ($null))==1);
	 //  @line: 54
	$i044 := $HeapVar[r039, int$ListInt$head0];
	 assert ($neref(($r443), ($null))==1);
	 //  @line: 54
	 call void$ListInt$$la$init$ra$$2229(($r443), ($i044), ($null));
	 assert ($neref(($r342), ($null))==1);
	 //  @line: 54
	 call $r545 := ListInt$ListInt$append$2231(($r342), ($r443));
	 //  @line: 54
	__ret := $r545;
	 return;
}


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


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


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



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



	 //  @line: 38
// <ListInt: void iter()>
procedure void$ListInt$iter$2230(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var $r220 : ref;
var r018 : ref;
var $r119 : ref;
Block22:
	r018 := __this;
	 assert ($neref((r018), ($null))==1);
	 //  @line: 39
	$r119 := $HeapVar[r018, ListInt$ListInt$tail254];
	 goto Block23;
	 //  @line: 39
Block23:
	 goto Block24, Block26;
	 //  @line: 39
Block24:
	 assume ($eqref(($r119), ($null))==1);
	 goto Block25;
	 //  @line: 39
Block26:
	 //  @line: 39
	 assume ($negInt(($eqref(($r119), ($null))))==1);
	 assert ($neref((r018), ($null))==1);
	 //  @line: 40
	$r220 := $HeapVar[r018, ListInt$ListInt$tail254];
	 assert ($neref(($r220), ($null))==1);
	 //  @line: 40
	 call void$ListInt$iter$2230(($r220));
	 goto Block25;
	 //  @line: 40
Block25:
	 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: 47
// <ListInt: ListInt reverseAcc(ListInt)>
procedure ListInt$ListInt$reverseAcc$2232(__this : ref, $param_0 : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $r536 : ref;
var r133 : ref;
var $i138 : int;
var $r637 : ref;
var $r332 : ref;
var $i034 : int;
var $r231 : ref;
var r030 : ref;
var $r435 : ref;
Block35:
	r030 := __this;
	r133 := $param_0;
	 assert ($neref((r030), ($null))==1);
	 //  @line: 48
	$r231 := $HeapVar[r030, ListInt$ListInt$tail254];
	 goto Block36;
	 //  @line: 48
Block36:
	 goto Block37, Block39;
	 //  @line: 48
Block37:
	 assume ($neref(($r231), ($null))==1);
	 goto Block38;
	 //  @line: 48
Block39:
	 //  @line: 48
	 assume ($negInt(($neref(($r231), ($null))))==1);
	 //  @line: 49
	$r637 := $newvariable((40));
	 assume ($neref(($newvariable((40))), ($null))==1);
	 assert ($neref((r030), ($null))==1);
	 //  @line: 49
	$i138 := $HeapVar[r030, int$ListInt$head0];
	 assert ($neref(($r637), ($null))==1);
	 //  @line: 49
	 call void$ListInt$$la$init$ra$$2229(($r637), ($i138), (r133));
	 //  @line: 49
	__ret := $r637;
	 return;
	 //  @line: 49
Block38:
	 assert ($neref((r030), ($null))==1);
	 //  @line: 49
	$r435 := $HeapVar[r030, ListInt$ListInt$tail254];
	 goto Block41;
	 //  @line: 49
Block41:
	 //  @line: 49
	$r332 := $newvariable((42));
	 assume ($neref(($newvariable((42))), ($null))==1);
	 assert ($neref((r030), ($null))==1);
	 //  @line: 49
	$i034 := $HeapVar[r030, int$ListInt$head0];
	 assert ($neref(($r332), ($null))==1);
	 //  @line: 49
	 call void$ListInt$$la$init$ra$$2229(($r332), ($i034), (r133));
	 assert ($neref(($r435), ($null))==1);
	 //  @line: 49
	 call $r536 := ListInt$ListInt$reverseAcc$2232(($r435), ($r332));
	 //  @line: 49
	__ret := $r536;
	 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)
}