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



	 //  @line: 6
// <A: A getSuperType()>
procedure A$A$getSuperType$2230(__this : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var r03 : ref;
Block18:
	r03 := __this;
	 //  @line: 7
	__ret := $null;
	 return;
}


	 //  @line: 2
// <C: A getSuperType()>
procedure A$C$getSuperType$2235(__this : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $r19 : ref;
var r010 : ref;
Block24:
	r010 := __this;
	 //  @line: 3
	$r19 := $newvariable((25));
	 assume ($neref(($newvariable((25))), ($null))==1);
	 assert ($neref(($r19), ($null))==1);
	 //  @line: 3
	 call void$B$$la$init$ra$$2231(($r19));
	 //  @line: 3
	__ret := $r19;
	 return;
}


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



	 //  @line: 2
// <B: boolean hasSuperType()>
procedure boolean$B$hasSuperType$2232(__this : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var r05 : ref;
Block20:
	r05 := __this;
	 //  @line: 3
	__ret := 1;
	 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);



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



	 //  @line: 2
// <A: boolean hasSuperType()>
procedure boolean$A$hasSuperType$2229(__this : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var r02 : ref;
Block17:
	r02 := __this;
	 //  @line: 3
	__ret := 0;
	 return;
}


// procedure is generated by joogie.
function {:inline true} $refarrtoref($param00 : [int]ref) returns (__ret : ref);



// <java.lang.Object: void <init>()>
procedure void$java.lang.Object$$la$init$ra$$28(__this : 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);



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



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



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



	 //  @line: 6
// <B: A getSuperType()>
procedure A$B$getSuperType$2233(__this : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $r16 : ref;
var r07 : ref;
Block21:
	r07 := __this;
	 //  @line: 7
	$r16 := $newvariable((22));
	 assume ($neref(($newvariable((22))), ($null))==1);
	 assert ($neref(($r16), ($null))==1);
	 //  @line: 7
	 call void$A$$la$init$ra$$2228(($r16));
	 //  @line: 7
	__ret := $r16;
	 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);



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



// <C: void <init>()>
procedure void$C$$la$init$ra$$2234(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r08 : ref;
Block23:
	r08 := __this;
	 assert ($neref((r08), ($null))==1);
	 //  @line: 1
	 call void$B$$la$init$ra$$2231((r08));
	 return;
}


// <B: void <init>()>
procedure void$B$$la$init$ra$$2231(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r04 : ref;
Block19:
	r04 := __this;
	 assert ($neref((r04), ($null))==1);
	 //  @line: 1
	 call void$A$$la$init$ra$$2228((r04));
	 return;
}


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


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


	 //  @line: 2
// <TypeSwitch: void main(java.lang.String[])>
procedure void$TypeSwitch$main$2237($param_0 : [int]ref) {
var $r115 : ref;
var $r319 : ref;
var $i014 : int;
var $z016 : int;
var r420 : ref;
var r013 : [int]ref;
var $r218 : ref;
Block27:
	r013 := $param_0;
	 //  @line: 3
	r420 := $null;
	 //  @line: 4
	$i014 := $refArrSize[r013[$arrSizeIdx]];
	 goto Block28;
	 //  @line: 4
Block28:
	 goto Block31, Block29;
	 //  @line: 5
Block31:
	 //  @line: 5
	 assume ($neint(($i014), (0))==1);
	 goto Block32;
	 //  @line: 5
Block29:
	 //  @line: 5
	 assume ($eqint(($i014), (0))==1);
	 goto Block30;
	 //  @line: 5
Block32:
	 goto Block33, Block35;
	 //  @line: 5
Block30:
	 //  @line: 5
	$r115 := $newvariable((42));
	 assume ($neref(($newvariable((42))), ($null))==1);
	 goto Block43;
	 //  @line: 7
Block33:
	 //  @line: 7
	 assume ($eqint(($i014), (1))==1);
	 goto Block34;
	 //  @line: 7
Block35:
	 //  @line: 7
	 assume ($neint(($i014), (1))==1);
	 goto Block36;
	 //  @line: 5
Block43:
	 assert ($neref(($r115), ($null))==1);
	 //  @line: 5
	 call void$A$$la$init$ra$$2228(($r115));
	 //  @line: 5
	r420 := $r115;
	 goto Block41;
	 //  @line: 7
Block34:
	 //  @line: 7
	$r319 := $newvariable((44));
	 assume ($neref(($newvariable((44))), ($null))==1);
	 goto Block45;
	 //  @line: 7
Block36:
	 goto Block37, Block39;
	 //  @line: 13
Block41:
	 assert ($neref((r420), ($null))==1);
	 //  @line: 13
	 call $z016 := boolean$A$hasSuperType$2229((r420));
	 goto Block48;
	 //  @line: 7
Block45:
	 assert ($neref(($r319), ($null))==1);
	 //  @line: 7
	 call void$B$$la$init$ra$$2231(($r319));
	 //  @line: 7
	r420 := $r319;
	 goto Block41;
	 //  @line: 9
Block37:
	 //  @line: 9
	 assume ($eqint(($i014), (2))==1);
	 goto Block38;
	 //  @line: 9
Block39:
	 //  @line: 9
	 assume ($neint(($i014), (2))==1);
	 goto Block40;
	 //  @line: 13
Block48:
	 goto Block51, Block49;
	 //  @line: 9
Block38:
	 //  @line: 9
	$r218 := $newvariable((46));
	 assume ($neref(($newvariable((46))), ($null))==1);
	 goto Block47;
	 //  @line: 9
Block40:
	 goto Block41;
	 //  @line: 13
Block51:
	 //  @line: 13
	 assume ($negInt(($eqint(($z016), (0))))==1);
	 assert ($neref((r420), ($null))==1);
	 //  @line: 14
	 call r420 := A$A$getSuperType$2230((r420));
	 goto Block41;
	 //  @line: 13
Block49:
	 assume ($eqint(($z016), (0))==1);
	 goto Block50;
	 //  @line: 9
Block47:
	 assert ($neref(($r218), ($null))==1);
	 //  @line: 9
	 call void$C$$la$init$ra$$2234(($r218));
	 //  @line: 9
	r420 := $r218;
	 goto Block41;
	 //  @line: 16
Block50:
	 return;
}


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