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$Random$index0 : int;
var java.lang.String$lp$$rp$$Random$args254 : [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);



	 //  @line: 2
// <Random: void <clinit>()>
procedure void$Random$$la$clinit$ra$$2234()
  modifies int$Random$index0;
 {
	 //  @line: 3
Block47:
	 //  @line: 3
	int$Random$index0 := 0;
	 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);



// <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} $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
// <BubbleSortR: void main(java.lang.String[])>
procedure void$BubbleSortR$main$2229($param_0 : [int]ref)
  modifies $stringSize, java.lang.String$lp$$rp$$Random$args254, $intArrSize;
 {
var i510 : int;
var i05 : int;
var $i38 : int;
var r16 : [int]int;
var $i49 : int;
var $i24 : int;
var r02 : [int]ref;
var $i13 : int;
Block17:
	r02 := $param_0;
	 //  @line: 3
	java.lang.String$lp$$rp$$Random$args254 := r02;
	 //  @line: 4
	 call $i13 := int$Random$random$2233();
	 //  @line: 4
	 call $i24 := int$Random$random$2233();
	 //  @line: 4
	i05 := $mulint(($i13), ($i24));
	 //  @line: 5
	r16 := $reftointarr(($newvariable((18))));
	$intArrSize[$reftointarr(($newvariable((18))))[$arrSizeIdx]] := i05;
	 assume ($negInt(($eqintarray(($reftointarr(($newvariable((18))))), ($intArrNull))))==1);
	 //  @line: 6
	i510 := 0;
	 goto Block19;
	 //  @line: 6
Block19:
	 //  @line: 6
	$i38 := $intArrSize[r16[$arrSizeIdx]];
	 goto Block20;
	 //  @line: 6
Block20:
	 goto Block21, Block23;
	 //  @line: 6
Block21:
	 assume ($geint((i510), ($i38))==1);
	 goto Block22;
	 //  @line: 6
Block23:
	 //  @line: 6
	 assume ($negInt(($geint((i510), ($i38))))==1);
	 //  @line: 7
	 call $i49 := int$Random$random$2233();
	 assert ($geint((i510), (0))==1);
	 assert ($ltint((i510), ($intArrSize[r16[$arrSizeIdx]]))==1);
	 //  @line: 7
	r16[i510] := $i49;
	 //  @line: 6
	i510 := $addint((i510), (1));
	 goto Block19;
	 //  @line: 8
Block22:
	 //  @line: 8
	 call void$BubbleSortR$sort$2230((r16));
	 goto Block24;
	 //  @line: 9
Block24:
	 return;
}


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



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



	 //  @line: 20
// <BubbleSortR: void aux(int,int,int[])>
procedure void$BubbleSortR$aux$2231($param_0 : int, $param_1 : int, $param_2 : [int]int) {
var $i723 : int;
var $i622 : int;
var i218 : int;
var $i926 : int;
var r019 : [int]int;
var $i420 : int;
var i117 : int;
var $i1027 : int;
var $i825 : int;
var i016 : int;
var i324 : int;
var $i521 : int;
Block30:
	i016 := $param_0;
	i117 := $param_1;
	r019 := $param_2;
	 goto Block31;
	 //  @line: 21
Block31:
	 goto Block32, Block34;
	 //  @line: 21
Block32:
	 assume ($ltint((i016), (i117))==1);
	 goto Block33;
	 //  @line: 21
Block34:
	 //  @line: 21
	 assume ($negInt(($ltint((i016), (i117))))==1);
	 return;
	 //  @line: 22
Block33:
	 //  @line: 22
	i218 := i016;
	 goto Block35;
	 //  @line: 23
Block35:
	 assert ($geint((i218), (0))==1);
	 assert ($ltint((i218), ($intArrSize[r019[$arrSizeIdx]]))==1);
	 //  @line: 23
	$i622 := r019[i218];
	 //  @line: 23
	$i420 := $addint((i218), (1));
	 assert ($geint(($i420), (0))==1);
	 assert ($ltint(($i420), ($intArrSize[r019[$arrSizeIdx]]))==1);
	 //  @line: 23
	$i521 := r019[$i420];
	 goto Block36;
	 //  @line: 23
Block36:
	 goto Block37, Block39;
	 //  @line: 23
Block37:
	 assume ($leint(($i622), ($i521))==1);
	 goto Block38;
	 //  @line: 23
Block39:
	 //  @line: 23
	 assume ($negInt(($leint(($i622), ($i521))))==1);
	 assert ($geint((i218), (0))==1);
	 assert ($ltint((i218), ($intArrSize[r019[$arrSizeIdx]]))==1);
	 //  @line: 25
	i324 := r019[i218];
	 //  @line: 25
	$i825 := $addint((i218), (1));
	 assert ($geint(($i825), (0))==1);
	 assert ($ltint(($i825), ($intArrSize[r019[$arrSizeIdx]]))==1);
	 //  @line: 25
	$i926 := r019[$i825];
	 assert ($geint((i218), (0))==1);
	 assert ($ltint((i218), ($intArrSize[r019[$arrSizeIdx]]))==1);
	 //  @line: 25
	r019[i218] := $i926;
	 //  @line: 25
	$i1027 := $addint((i218), (1));
	 assert ($geint(($i1027), (0))==1);
	 assert ($ltint(($i1027), ($intArrSize[r019[$arrSizeIdx]]))==1);
	 //  @line: 25
	r019[$i1027] := i324;
	 goto Block38;
	 //  @line: 27
Block38:
	 //  @line: 27
	$i723 := $addint((i016), (1));
	 //  @line: 27
	 call void$BubbleSortR$aux$2231(($i723), (i117), (r019));
	 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
}


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



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


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



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



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


	 //  @line: 5
// <Random: int random()>
procedure int$Random$random$2233() returns (__ret : int)
  modifies int$Random$index0, $stringSize;
 {
var $r233 : [int]ref;
var $i030 : int;
var $i232 : int;
var $i537 : int;
var $r129 : [int]ref;
var $i436 : int;
var r034 : ref;
var $i131 : int;
var $i335 : int;
	 //  @line: 6
Block41:
	 //  @line: 6
	$i131 := int$Random$index0;
	 //  @line: 6
	$r129 := java.lang.String$lp$$rp$$Random$args254;
	 //  @line: 6
	$i030 := $refArrSize[$r129[$arrSizeIdx]];
	 goto Block42;
	 //  @line: 6
Block42:
	 goto Block45, Block43;
	 //  @line: 6
Block45:
	 //  @line: 6
	 assume ($negInt(($ltint(($i131), ($i030))))==1);
	 //  @line: 7
	__ret := 0;
	 return;
	 //  @line: 6
Block43:
	 assume ($ltint(($i131), ($i030))==1);
	 goto Block44;
	 //  @line: 9
Block44:
	 //  @line: 9
	$r233 := java.lang.String$lp$$rp$$Random$args254;
	 goto Block46;
	 //  @line: 9
Block46:
	 //  @line: 9
	$i232 := int$Random$index0;
	 assert ($geint(($i232), (0))==1);
	 assert ($ltint(($i232), ($refArrSize[$r233[$arrSizeIdx]]))==1);
	 //  @line: 9
	r034 := $r233[$i232];
	 //  @line: 10
	$i335 := int$Random$index0;
	 //  @line: 10
	$i436 := $addint(($i335), (1));
	 //  @line: 10
	int$Random$index0 := $i436;
	$i537 := $stringSize[r034];
	 //  @line: 11
	__ret := $i537;
	 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);



// <BubbleSortR: void <init>()>
procedure void$BubbleSortR$$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} $shlint($param00 : int, $param11 : int) returns (__ret : int);



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



	 //  @line: 11
// <BubbleSortR: void sort(int[])>
procedure void$BubbleSortR$sort$2230($param_0 : [int]int) {
var i012 : int;
var $i114 : int;
var i215 : int;
var r011 : [int]int;
Block25:
	r011 := $param_0;
	 //  @line: 12
	i012 := $intArrSize[r011[$arrSizeIdx]];
	 //  @line: 13
	i215 := 1;
	 goto Block26;
	 //  @line: 13
Block26:
	 goto Block27, Block29;
	 //  @line: 13
Block27:
	 assume ($geint((i215), (i012))==1);
	 goto Block28;
	 //  @line: 13
Block29:
	 //  @line: 13
	 assume ($negInt(($geint((i215), (i012))))==1);
	 //  @line: 15
	$i114 := $subint((i012), (i215));
	 //  @line: 15
	 call void$BubbleSortR$aux$2231((0), ($i114), (r011));
	 //  @line: 13
	i215 := $addint((i215), (1));
	 goto Block26;
	 //  @line: 18
Block28:
	 return;
}


// procedure is generated by joogie.
function {:inline true} $subint(x : int, y : int) returns (__ret : int) {
(x - y)
}