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 CAppE$CAppE$next254 : Field ref;
var int$Random$index0 : int;
var java.lang.String$lp$$rp$$Random$args255 : [int]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);



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



	 //  @line: 4
// <CAppE: void main(java.lang.String[])>
procedure void$CAppE$main$2228($param_0 : [int]ref)
  modifies $stringSize, java.lang.String$lp$$rp$$Random$args255;
 {
var $i04 : int;
var r01 : [int]ref;

 //temp local variables 
var $freshlocal0 : ref;

Block16:
	r01 := $param_0;
	 //  @line: 5
	java.lang.String$lp$$rp$$Random$args255 := r01;
	 //  @line: 6
	 call $freshlocal0 := CAppE$CAppE$createList$2231();
	 //  @line: 7
	 call $i04 := int$Random$random$2235();
	 //  @line: 7
	 call void$CAppE$cappE$2229(($i04));
	 return;
}


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



	 //  @line: 10
// <CAppE: void cappE(int)>
procedure void$CAppE$cappE$2229($param_0 : int) {
var $r28 : ref;
var i07 : int;
var $r15 : ref;
var r06 : ref;
Block17:
	i07 := $param_0;
	 //  @line: 11
	$r15 := $newvariable((18));
	 assume ($neref(($newvariable((18))), ($null))==1);
	 assert ($neref(($r15), ($null))==1);
	 //  @line: 11
	 call void$CAppE$$la$init$ra$$2232(($r15));
	 //  @line: 11
	r06 := $r15;
	 goto Block19;
	 //  @line: 12
Block19:
	 goto Block22, Block20;
	 //  @line: 12
Block22:
	 //  @line: 12
	 assume ($negInt(($leint((i07), (0))))==1);
	 assert ($neref((r06), ($null))==1);
	 //  @line: 13
	 call void$CAppE$appE$2230((r06), (i07));
	 goto Block23;
	 //  @line: 12
Block20:
	 assume ($leint((i07), (0))==1);
	 goto Block21;
	 //  @line: 14
Block23:
	 assert ($neref((r06), ($null))==1);
	 //  @line: 14
	$r28 := $HeapVar[r06, CAppE$CAppE$next254];
	 goto Block24;
	 //  @line: 16
Block21:
	 return;
	 //  @line: 14
Block24:
	 goto Block25, Block26;
	 //  @line: 14
Block25:
	 assume ($neref(($r28), ($null))==1);
	 goto Block21;
	 //  @line: 14
Block26:
	 //  @line: 14
	 assume ($negInt(($neref(($r28), ($null))))==1);
	 goto Block23;
}


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



	 //  @line: 30
// <CAppE: CAppE createList()>
procedure CAppE$CAppE$createList$2231() returns (__ret : ref) {
var r119 : ref;
var $r018 : ref;
var i020 : int;
	 //  @line: 31
Block38:
	 //  @line: 31
	r119 := $null;
	 //  @line: 32
	 call i020 := int$Random$random$2235();
	 goto Block39;
	 //  @line: 33
Block39:
	 goto Block40, Block42;
	 //  @line: 33
Block40:
	 assume ($leint((i020), (0))==1);
	 goto Block41;
	 //  @line: 33
Block42:
	 //  @line: 33
	 assume ($negInt(($leint((i020), (0))))==1);
	 //  @line: 34
	$r018 := $newvariable((43));
	 assume ($neref(($newvariable((43))), ($null))==1);
	 assert ($neref(($r018), ($null))==1);
	 //  @line: 34
	 call void$CAppE$$la$init$ra$$2233(($r018), (r119));
	 //  @line: 34
	r119 := $r018;
	 //  @line: 35
	i020 := $addint((i020), (-1));
	 goto Block39;
	 //  @line: 37
Block41:
	 //  @line: 37
	__ret := r119;
	 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);



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



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


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


	 //  @line: 50
// <Random: void <clinit>()>
procedure void$Random$$la$clinit$ra$$2236()
  modifies int$Random$index0;
 {
	 //  @line: 51
Block48:
	 //  @line: 51
	int$Random$index0 := 0;
	 return;
}


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



	 //  @line: 43
// <CAppE: void <init>(CAppE)>
procedure void$CAppE$$la$init$ra$$2233(__this : ref, $param_0 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r123 : ref;
var r022 : ref;
Block45:
	r022 := __this;
	r123 := $param_0;
	 assert ($neref((r022), ($null))==1);
	 //  @line: 44
	 call void$java.lang.Object$$la$init$ra$$28((r022));
	 assert ($neref((r022), ($null))==1);
	 //  @line: 45
	$HeapVar[r022, CAppE$CAppE$next254] := r123;
	 return;
}


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



	 //  @line: 53
// <Random: int random()>
procedure int$Random$random$2235() returns (__ret : int)
  modifies int$Random$index0, $stringSize;
 {
var r027 : ref;
var $r126 : [int]ref;
var $i128 : int;
var $i025 : int;
var $i229 : int;
var $i330 : int;
	 //  @line: 54
Block47:
	 //  @line: 54
	$r126 := java.lang.String$lp$$rp$$Random$args255;
	 //  @line: 54
	$i025 := int$Random$index0;
	 assert ($geint(($i025), (0))==1);
	 assert ($ltint(($i025), ($refArrSize[$r126[$arrSizeIdx]]))==1);
	 //  @line: 54
	r027 := $r126[$i025];
	 //  @line: 55
	$i128 := int$Random$index0;
	 //  @line: 55
	$i229 := $addint(($i128), (1));
	 //  @line: 55
	int$Random$index0 := $i229;
	$i330 := $stringSize[r027];
	 //  @line: 56
	__ret := $i330;
	 return;
}


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


	 //  @line: 39
// <CAppE: void <init>()>
procedure void$CAppE$$la$init$ra$$2232(__this : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r021 : ref;
Block44:
	r021 := __this;
	 assert ($neref((r021), ($null))==1);
	 //  @line: 40
	 call void$java.lang.Object$$la$init$ra$$28((r021));
	 assert ($neref((r021), ($null))==1);
	 //  @line: 41
	$HeapVar[r021, CAppE$CAppE$next254] := $null;
	 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);



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



	 //  @line: 18
// <CAppE: void appE(int)>
procedure void$CAppE$appE$2230(__this : ref, $param_0 : int)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r09 : ref;
var i014 : int;
var $r212 : ref;
var $r110 : ref;
var $r313 : ref;
Block27:
	r09 := __this;
	i014 := $param_0;
	 assert ($neref((r09), ($null))==1);
	 //  @line: 19
	$r110 := $HeapVar[r09, CAppE$CAppE$next254];
	 goto Block28;
	 //  @line: 19
Block28:
	 goto Block31, Block29;
	 //  @line: 19
Block31:
	 //  @line: 19
	 assume ($negInt(($neref(($r110), ($null))))==1);
	 goto Block32;
	 //  @line: 19
Block29:
	 assume ($neref(($r110), ($null))==1);
	 goto Block30;
	 //  @line: 20
Block32:
	 goto Block35, Block33;
	 //  @line: 27
Block30:
	 assert ($neref((r09), ($null))==1);
	 //  @line: 27
	$r212 := $HeapVar[r09, CAppE$CAppE$next254];
	 assert ($neref(($r212), ($null))==1);
	 //  @line: 27
	 call void$CAppE$appE$2230(($r212), (i014));
	 return;
	 //  @line: 20
Block35:
	 //  @line: 20
	 assume ($negInt(($gtint((i014), (0))))==1);
	 return;
	 //  @line: 20
Block33:
	 assume ($gtint((i014), (0))==1);
	 goto Block34;
	 //  @line: 23
Block34:
	 //  @line: 23
	$r313 := $newvariable((36));
	 assume ($neref(($newvariable((36))), ($null))==1);
	 goto Block37;
	 //  @line: 23
Block37:
	 assert ($neref(($r313), ($null))==1);
	 //  @line: 23
	 call void$CAppE$$la$init$ra$$2232(($r313));
	 assert ($neref((r09), ($null))==1);
	 //  @line: 23
	$HeapVar[r09, CAppE$CAppE$next254] := $r313;
	 //  @line: 25
	i014 := $addint((i014), (-1));
	 goto Block30;
}


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