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 Kernel93$Kernel93$next254 : 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: 117
// <Kernel93: void slide93(int,int)>
procedure void$Kernel93$slide93$2234($param_0 : int, $param_1 : int)
  modifies $HeapVar;
 {
var r050 : ref;
var i048 : int;
var r256 : ref;
var r459 : ref;
var r358 : ref;
var i157 : int;
var $z055 : int;
var r153 : ref;
Block55:
	i048 := $param_0;
	i157 := $param_1;
	 //  @line: 118
	 call r050 := Kernel93$Kernel93$create$2230((i048));
	 //  @line: 119
	r358 := r050;
	 assert ($neref((r358), ($null))==1);
	 //  @line: 120
	r459 := $HeapVar[r358, Kernel93$Kernel93$next254];
	 goto Block56;
	 //  @line: 121
Block56:
	 goto Block57, Block59;
	 //  @line: 121
Block57:
	 assume ($eqref((r459), (r050))==1);
	 goto Block58;
	 //  @line: 121
Block59:
	 //  @line: 121
	 assume ($negInt(($eqref((r459), (r050))))==1);
	 //  @line: 122
	r153 := r459;
	 //  @line: 125
	 call $z055 := boolean$Kernel93$check$2231((i157));
	 goto Block60;
	 //  @line: 137
Block58:
	 return;
	 //  @line: 125
Block60:
	 goto Block61, Block63;
	 //  @line: 125
Block61:
	 assume ($eqint(($z055), (0))==1);
	 goto Block62;
	 //  @line: 125
Block63:
	 //  @line: 125
	 assume ($negInt(($eqint(($z055), (0))))==1);
	 assert ($neref((r153), ($null))==1);
	 //  @line: 126
	r256 := $HeapVar[r153, Kernel93$Kernel93$next254];
	 assert ($neref((r358), ($null))==1);
	 //  @line: 127
	$HeapVar[r358, Kernel93$Kernel93$next254] := r256;
	 assert ($neref((r153), ($null))==1);
	 //  @line: 128
	$HeapVar[r153, Kernel93$Kernel93$next254] := r153;
	 goto Block64;
	 //  @line: 130
Block62:
	 //  @line: 130
	r358 := r153;
	 goto Block64;
	 //  @line: 132
Block64:
	 assert ($neref((r459), ($null))==1);
	 //  @line: 132
	r459 := $HeapVar[r459, Kernel93$Kernel93$next254];
	 goto Block65;
	 //  @line: 135
Block65:
	 assert ($neint((2), (0))==1);
	 //  @line: 135
	i157 := $divint((i157), (2));
	 goto Block56;
}


// 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: 139
// <Kernel93: void slide95(int,int)>
procedure void$Kernel93$slide95$2235($param_0 : int, $param_1 : int)
  modifies $HeapVar;
 {
var r268 : ref;
var r165 : ref;
var $z067 : int;
var r370 : ref;
var i060 : int;
var i169 : int;
var r062 : ref;
var r471 : ref;
Block66:
	i060 := $param_0;
	i169 := $param_1;
	 //  @line: 140
	 call r062 := Kernel93$Kernel93$create$2230((i060));
	 //  @line: 141
	r370 := r062;
	 assert ($neref((r370), ($null))==1);
	 //  @line: 142
	r471 := $HeapVar[r370, Kernel93$Kernel93$next254];
	 goto Block67;
	 //  @line: 143
Block67:
	 goto Block70, Block68;
	 //  @line: 143
Block70:
	 //  @line: 143
	 assume ($negInt(($eqref((r471), (r062))))==1);
	 //  @line: 144
	r165 := r471;
	 assert ($neref((r471), ($null))==1);
	 //  @line: 145
	r471 := $HeapVar[r471, Kernel93$Kernel93$next254];
	 //  @line: 147
	 call $z067 := boolean$Kernel93$check$2231((i169));
	 goto Block71;
	 //  @line: 143
Block68:
	 assume ($eqref((r471), (r062))==1);
	 goto Block69;
	 //  @line: 147
Block71:
	 goto Block72, Block74;
	 //  @line: 158
Block69:
	 return;
	 //  @line: 147
Block72:
	 assume ($eqint(($z067), (0))==1);
	 goto Block73;
	 //  @line: 147
Block74:
	 //  @line: 147
	 assume ($negInt(($eqint(($z067), (0))))==1);
	 assert ($neref((r165), ($null))==1);
	 //  @line: 148
	r268 := $HeapVar[r165, Kernel93$Kernel93$next254];
	 assert ($neref((r370), ($null))==1);
	 //  @line: 149
	$HeapVar[r370, Kernel93$Kernel93$next254] := r268;
	 assert ($neref((r165), ($null))==1);
	 //  @line: 150
	$HeapVar[r165, Kernel93$Kernel93$next254] := r165;
	 goto Block75;
	 //  @line: 152
Block73:
	 //  @line: 152
	r370 := r165;
	 goto Block75;
	 //  @line: 156
Block75:
	 assert ($neint((2), (0))==1);
	 //  @line: 156
	i169 := $divint((i169), (2));
	 goto Block76;
	 //  @line: 157
Block76:
	 goto Block67;
}


// 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: 42
// <Kernel93: Kernel93 create(int)>
procedure Kernel93$Kernel93$create$2230($param_0 : int) returns (__ret : ref)
  modifies $HeapVar;
 {
var i015 : int;
var $r110 : ref;
var r012 : ref;
var $r214 : ref;
var r316 : ref;
Block18:
	i015 := $param_0;
	 //  @line: 43
	$r110 := $newvariable((19));
	 assume ($neref(($newvariable((19))), ($null))==1);
	 assert ($neref(($r110), ($null))==1);
	 //  @line: 43
	 call void$Kernel93$$la$init$ra$$2229(($r110), ($null));
	 //  @line: 43
	r316 := $r110;
	 //  @line: 43
	r012 := $r110;
	 goto Block20;
	 //  @line: 44
Block20:
	 //  @line: 44
	i015 := $addint((i015), (-1));
	 goto Block21;
	 //  @line: 44
Block21:
	 goto Block24, Block22;
	 //  @line: 44
Block24:
	 //  @line: 44
	 assume ($negInt(($leint((i015), (0))))==1);
	 //  @line: 45
	$r214 := $newvariable((25));
	 assume ($neref(($newvariable((25))), ($null))==1);
	 assert ($neref(($r214), ($null))==1);
	 //  @line: 45
	 call void$Kernel93$$la$init$ra$$2229(($r214), (r316));
	 //  @line: 45
	r316 := $r214;
	 goto Block20;
	 //  @line: 44
Block22:
	 assume ($leint((i015), (0))==1);
	 goto Block23;
	 //  @line: 46
Block23:
	 assert ($neref((r012), ($null))==1);
	 //  @line: 46
	$HeapVar[r012, Kernel93$Kernel93$next254] := r316;
	 goto Block26;
	 //  @line: 46
Block26:
	 //  @line: 46
	__ret := r316;
	 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: 83
// <Kernel93: void slide88(int,int)>
procedure void$Kernel93$slide88$2233($param_0 : int, $param_1 : int)
  modifies $HeapVar;
 {
var r244 : ref;
var r446 : ref;
var r142 : ref;
var i143 : int;
var i034 : int;
var r036 : ref;
var $z041 : int;
var r345 : ref;
Block44:
	i034 := $param_0;
	i143 := $param_1;
	 //  @line: 84
	 call r036 := Kernel93$Kernel93$create$2230((i034));
	 //  @line: 85
	r244 := r036;
	 assert ($neref((r244), ($null))==1);
	 //  @line: 86
	r345 := $HeapVar[r244, Kernel93$Kernel93$next254];
	 goto Block45;
	 //  @line: 87
Block45:
	 goto Block46, Block48;
	 //  @line: 87
Block46:
	 assume ($eqref((r345), (r036))==1);
	 goto Block47;
	 //  @line: 87
Block48:
	 //  @line: 87
	 assume ($negInt(($eqref((r345), (r036))))==1);
	 //  @line: 88
	r446 := r345;
	 //  @line: 90
	 call $z041 := boolean$Kernel93$check$2231((i143));
	 goto Block49;
	 //  @line: 112
Block47:
	 return;
	 //  @line: 90
Block49:
	 goto Block50, Block52;
	 //  @line: 90
Block50:
	 assume ($eqint(($z041), (0))==1);
	 goto Block51;
	 //  @line: 90
Block52:
	 //  @line: 90
	 assume ($negInt(($eqint(($z041), (0))))==1);
	 assert ($neref((r446), ($null))==1);
	 //  @line: 91
	r142 := $HeapVar[r446, Kernel93$Kernel93$next254];
	 assert ($neref((r244), ($null))==1);
	 //  @line: 92
	$HeapVar[r244, Kernel93$Kernel93$next254] := r142;
	 //  @line: 98
	r345 := $null;
	 goto Block53;
	 //  @line: 105
Block51:
	 //  @line: 105
	r244 := r446;
	 goto Block53;
	 //  @line: 107
Block53:
	 assert ($neref((r345), ($null))==1);
	 //  @line: 107
	r345 := $HeapVar[r345, Kernel93$Kernel93$next254];
	 goto Block54;
	 //  @line: 110
Block54:
	 assert ($neint((2), (0))==1);
	 //  @line: 110
	i143 := $divint((i143), (2));
	 goto Block45;
}


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



	 //  @line: 31
// <Kernel93: void <init>(Kernel93)>
procedure void$Kernel93$$la$init$ra$$2229(__this : ref, $param_0 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r08 : ref;
var r19 : ref;
Block17:
	r08 := __this;
	r19 := $param_0;
	 assert ($neref((r08), ($null))==1);
	 //  @line: 32
	 call void$java.lang.Object$$la$init$ra$$28((r08));
	 assert ($neref((r08), ($null))==1);
	 //  @line: 33
	$HeapVar[r08, Kernel93$Kernel93$next254] := r19;
	 return;
}


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



	 //  @line: 52
// <Kernel93: boolean check(int)>
procedure boolean$Kernel93$check$2231($param_0 : int) returns (__ret : int) {
var $z020 : int;
var $i118 : int;
var i017 : int;
Block27:
	i017 := $param_0;
	 //  @line: 53
	$i118 := $modint((i017), (2));
	 goto Block28;
	 //  @line: 53
Block28:
	 goto Block29, Block31;
	 //  @line: 53
Block29:
	 assume ($leint(($i118), (0))==1);
	 goto Block30;
	 //  @line: 53
Block31:
	 //  @line: 53
	 assume ($negInt(($leint(($i118), (0))))==1);
	 //  @line: 53
	$z020 := 1;
	 goto Block32;
	 //  @line: 53
Block30:
	 //  @line: 53
	$z020 := 0;
	 goto Block32;
	 //  @line: 53
Block32:
	 //  @line: 53
	__ret := $z020;
	 return;
}


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



	 //  @line: 56
// <Kernel93: void slide68(int,int)>
procedure void$Kernel93$slide68$2232($param_0 : int, $param_1 : int)
  modifies $HeapVar;
 {
var i129 : int;
var i021 : int;
var $z028 : int;
var r023 : ref;
var r231 : ref;
var r332 : ref;
var r130 : ref;
Block33:
	i021 := $param_0;
	i129 := $param_1;
	 //  @line: 57
	 call r023 := Kernel93$Kernel93$create$2230((i021));
	 //  @line: 58
	r130 := r023;
	 assert ($neref((r130), ($null))==1);
	 //  @line: 59
	r231 := $HeapVar[r130, Kernel93$Kernel93$next254];
	 goto Block34;
	 //  @line: 60
Block34:
	 goto Block35, Block37;
	 //  @line: 60
Block35:
	 assume ($eqref((r231), (r023))==1);
	 goto Block36;
	 //  @line: 60
Block37:
	 //  @line: 60
	 assume ($negInt(($eqref((r231), (r023))))==1);
	 //  @line: 61
	r332 := r231;
	 assert ($neref((r231), ($null))==1);
	 //  @line: 62
	r231 := $HeapVar[r231, Kernel93$Kernel93$next254];
	 //  @line: 63
	 call $z028 := boolean$Kernel93$check$2231((i129));
	 goto Block38;
	 //  @line: 81
Block36:
	 return;
	 //  @line: 63
Block38:
	 goto Block41, Block39;
	 //  @line: 63
Block41:
	 //  @line: 63
	 assume ($negInt(($eqint(($z028), (0))))==1);
	 assert ($neref((r130), ($null))==1);
	 //  @line: 64
	$HeapVar[r130, Kernel93$Kernel93$next254] := r231;
	 goto Block42;
	 //  @line: 63
Block39:
	 assume ($eqint(($z028), (0))==1);
	 goto Block40;
	 //  @line: 79
Block42:
	 assert ($neint((2), (0))==1);
	 //  @line: 79
	i129 := $divint((i129), (2));
	 goto Block43;
	 //  @line: 75
Block40:
	 //  @line: 75
	r130 := r332;
	 goto Block42;
	 //  @line: 80
Block43:
	 goto Block34;
}


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


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



	 //  @line: 18
// <Kernel93: void main(java.lang.String[])>
procedure void$Kernel93$main$2228($param_0 : [int]ref)
  modifies $stringSize;
 {
var r01 : [int]ref;
var $r25 : ref;
var i04 : int;
var i17 : int;
var $r12 : ref;
Block16:
	r01 := $param_0;
	 assert ($geint((0), (0))==1);
	 assert ($ltint((0), ($refArrSize[r01[$arrSizeIdx]]))==1);
	 //  @line: 19
	$r12 := r01[0];
	i04 := $stringSize[$r12];
	 assert ($geint((1), (0))==1);
	 assert ($ltint((1), ($refArrSize[r01[$arrSizeIdx]]))==1);
	 //  @line: 20
	$r25 := r01[1];
	i17 := $stringSize[$r25];
	 //  @line: 24
	 call void$Kernel93$slide93$2234((i04), (i17));
	 return;
}


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


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



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