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 java.lang.String$lp$$rp$$MirrorBinTreeRec.Random$args256 : [int]ref;
var MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$right255 : Field ref;
var int$MirrorBinTreeRec.Random$index0 : int;
var MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$left254 : Field ref;
var int$MirrorBinTreeRec.Tree$value0 : Field int;


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



// 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: 3
// <MirrorBinTreeRec.Random: void <clinit>()>
procedure void$MirrorBinTreeRec.Random$$la$clinit$ra$$2238()
  modifies int$MirrorBinTreeRec.Random$index0;
 {
	 //  @line: 4
Block66:
	 //  @line: 4
	int$MirrorBinTreeRec.Random$index0 := 0;
	 return;
}


	 //  @line: 14
// <MirrorBinTreeRec.MirrorBinTreeRec: void mirror(MirrorBinTreeRec.Tree)>
procedure void$MirrorBinTreeRec.MirrorBinTreeRec$mirror$2230($param_0 : ref)
  modifies $HeapVar;
 {
var r16 : ref;
var $r49 : ref;
var r05 : ref;
var $r27 : ref;
var $r38 : ref;
Block18:
	r05 := $param_0;
	 goto Block19;
	 //  @line: 15
Block19:
	 goto Block20, Block22;
	 //  @line: 15
Block20:
	 assume ($neref((r05), ($null))==1);
	 goto Block21;
	 //  @line: 15
Block22:
	 //  @line: 15
	 assume ($negInt(($neref((r05), ($null))))==1);
	 return;
	 //  @line: 18
Block21:
	 assert ($neref((r05), ($null))==1);
	 //  @line: 18
	r16 := $HeapVar[r05, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$right255];
	 goto Block23;
	 //  @line: 19
Block23:
	 assert ($neref((r05), ($null))==1);
	 //  @line: 19
	$r27 := $HeapVar[r05, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$left254];
	 assert ($neref((r05), ($null))==1);
	 //  @line: 19
	$HeapVar[r05, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$right255] := $r27;
	 assert ($neref((r05), ($null))==1);
	 //  @line: 20
	$HeapVar[r05, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$left254] := r16;
	 assert ($neref((r05), ($null))==1);
	 //  @line: 21
	$r38 := $HeapVar[r05, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$left254];
	 //  @line: 21
	 call void$MirrorBinTreeRec.MirrorBinTreeRec$mirror$2230(($r38));
	 assert ($neref((r05), ($null))==1);
	 //  @line: 22
	$r49 := $HeapVar[r05, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$right255];
	 //  @line: 22
	 call void$MirrorBinTreeRec.MirrorBinTreeRec$mirror$2230(($r49));
	 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);



	 //  @line: 16
// <MirrorBinTreeRec.Tree: MirrorBinTreeRec.Tree createNode()>
procedure MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$createNode$2233() returns (__ret : ref)
  modifies $HeapVar;
 {
var $i016 : int;
var r015 : ref;
var $r114 : ref;
	 //  @line: 17
Block26:
	 //  @line: 17
	$r114 := $newvariable((27));
	 assume ($neref(($newvariable((27))), ($null))==1);
	 assert ($neref(($r114), ($null))==1);
	 //  @line: 17
	 call void$MirrorBinTreeRec.Tree$$la$init$ra$$2232(($r114));
	 //  @line: 17
	r015 := $r114;
	 //  @line: 18
	 call $i016 := int$MirrorBinTreeRec.Random$random$2237();
	 assert ($neref((r015), ($null))==1);
	 //  @line: 18
	$HeapVar[r015, int$MirrorBinTreeRec.Tree$value0] := $i016;
	 //  @line: 19
	__ret := r015;
	 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);



	 //  @line: 8
// <MirrorBinTreeRec.MirrorBinTreeRec: void main(java.lang.String[])>
procedure void$MirrorBinTreeRec.MirrorBinTreeRec$main$2229($param_0 : [int]ref)
  modifies java.lang.String$lp$$rp$$MirrorBinTreeRec.Random$args256, $stringSize;
 {
var r02 : [int]ref;
var r14 : ref;
Block17:
	r02 := $param_0;
	 //  @line: 9
	java.lang.String$lp$$rp$$MirrorBinTreeRec.Random$args256 := r02;
	 //  @line: 10
	 call r14 := MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$createTree$2234();
	 //  @line: 11
	 call void$MirrorBinTreeRec.MirrorBinTreeRec$mirror$2230((r14));
	 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);



	 //  @line: 12
// <MirrorBinTreeRec.Tree: void <init>()>
procedure void$MirrorBinTreeRec.Tree$$la$init$ra$$2232(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r013 : ref;
Block25:
	r013 := __this;
	 assert ($neref((r013), ($null))==1);
	 //  @line: 13
	 call void$java.lang.Object$$la$init$ra$$28((r013));
	 return;
}


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


	 //  @line: 6
// <MirrorBinTreeRec.Random: int random()>
procedure int$MirrorBinTreeRec.Random$random$2237() returns (__ret : int)
  modifies int$MirrorBinTreeRec.Random$index0, $stringSize;
 {
var $i339 : int;
var $i034 : int;
var $i236 : int;
var $i541 : int;
var $r133 : [int]ref;
var $i440 : int;
var $r237 : [int]ref;
var $i135 : int;
var r038 : ref;
	 //  @line: 7
Block55:
	 //  @line: 7
	$r133 := java.lang.String$lp$$rp$$MirrorBinTreeRec.Random$args256;
	 //  @line: 7
	$i135 := $refArrSize[$r133[$arrSizeIdx]];
	 //  @line: 7
	$i034 := int$MirrorBinTreeRec.Random$index0;
	 goto Block56;
	 //  @line: 7
Block56:
	 goto Block59, Block57;
	 //  @line: 7
Block59:
	 //  @line: 7
	 assume ($negInt(($gtint(($i135), ($i034))))==1);
	 //  @line: 8
	__ret := 0;
	 return;
	 //  @line: 7
Block57:
	 assume ($gtint(($i135), ($i034))==1);
	 goto Block58;
	 //  @line: 10
Block58:
	 //  @line: 10
	$r237 := java.lang.String$lp$$rp$$MirrorBinTreeRec.Random$args256;
	 goto Block60;
	 //  @line: 10
Block60:
	 //  @line: 10
	$i236 := int$MirrorBinTreeRec.Random$index0;
	 assert ($geint(($i236), (0))==1);
	 assert ($ltint(($i236), ($refArrSize[$r237[$arrSizeIdx]]))==1);
	 //  @line: 10
	r038 := $r237[$i236];
	 //  @line: 11
	$i339 := int$MirrorBinTreeRec.Random$index0;
	 //  @line: 11
	$i440 := $addint(($i339), (1));
	 //  @line: 11
	int$MirrorBinTreeRec.Random$index0 := $i440;
	 goto Block61;
	 //  @line: 12
Block61:
	 goto Block64, Block62;
	 //  @line: 12
Block64:
	 //  @line: 12
	 assume ($negInt(($neref((r038), ($null))))==1);
	 //  @line: 13
	__ret := 0;
	 return;
	 //  @line: 12
Block62:
	 assume ($neref((r038), ($null))==1);
	 goto Block63;
	 //  @line: 15
Block63:
	$i541 := $stringSize[r038];
	 goto Block65;
	 //  @line: 15
Block65:
	 //  @line: 15
	__ret := $i541;
	 return;
}


// 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: 22
// <MirrorBinTreeRec.Tree: MirrorBinTreeRec.Tree createTree()>
procedure MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$createTree$2234() returns (__ret : ref)
  modifies $HeapVar;
 {
var r529 : ref;
var $r326 : ref;
var $r427 : ref;
var $r124 : ref;
var i023 : int;
var $r225 : ref;
var i128 : int;
var r020 : ref;
	 //  @line: 23
Block28:
	 //  @line: 23
	 call i128 := int$MirrorBinTreeRec.Random$random$2237();
	 goto Block29;
	 //  @line: 24
Block29:
	 goto Block32, Block30;
	 //  @line: 24
Block32:
	 //  @line: 24
	 assume ($negInt(($neint((i128), (0))))==1);
	 //  @line: 25
	__ret := $null;
	 return;
	 //  @line: 24
Block30:
	 assume ($neint((i128), (0))==1);
	 goto Block31;
	 //  @line: 27
Block31:
	 //  @line: 27
	 call r020 := MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$createNode$2233();
	 goto Block33;
	 //  @line: 28
Block33:
	 //  @line: 28
	r529 := r020;
	 goto Block34;
	 //  @line: 30
Block34:
	 goto Block35, Block37;
	 //  @line: 30
Block35:
	 assume ($leint((i128), (0))==1);
	 goto Block36;
	 //  @line: 30
Block37:
	 //  @line: 30
	 assume ($negInt(($leint((i128), (0))))==1);
	 //  @line: 31
	 call i023 := int$MirrorBinTreeRec.Random$random$2237();
	 goto Block38;
	 //  @line: 50
Block36:
	 //  @line: 50
	__ret := r020;
	 return;
	 //  @line: 32
Block38:
	 goto Block39, Block41;
	 //  @line: 32
Block39:
	 assume ($leint((i023), (0))==1);
	 goto Block40;
	 //  @line: 32
Block41:
	 //  @line: 32
	 assume ($negInt(($leint((i023), (0))))==1);
	 assert ($neref((r529), ($null))==1);
	 //  @line: 33
	$r326 := $HeapVar[r529, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$left254];
	 goto Block42;
	 //  @line: 40
Block40:
	 assert ($neref((r529), ($null))==1);
	 //  @line: 40
	$r124 := $HeapVar[r529, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$right255];
	 goto Block48;
	 //  @line: 33
Block42:
	 goto Block45, Block43;
	 //  @line: 40
Block48:
	 goto Block49, Block51;
	 //  @line: 33
Block45:
	 //  @line: 33
	 assume ($negInt(($neref(($r326), ($null))))==1);
	 //  @line: 34
	 call $r427 := MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$createNode$2233();
	 assert ($neref((r529), ($null))==1);
	 //  @line: 34
	$HeapVar[r529, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$left254] := $r427;
	 //  @line: 35
	r529 := r020;
	 goto Block46;
	 //  @line: 33
Block43:
	 assume ($neref(($r326), ($null))==1);
	 goto Block44;
	 //  @line: 40
Block49:
	 assume ($neref(($r124), ($null))==1);
	 goto Block50;
	 //  @line: 40
Block51:
	 //  @line: 40
	 assume ($negInt(($neref(($r124), ($null))))==1);
	 //  @line: 41
	 call $r225 := MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$createNode$2233();
	 assert ($neref((r529), ($null))==1);
	 //  @line: 41
	$HeapVar[r529, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$right255] := $r225;
	 //  @line: 42
	r529 := r020;
	 goto Block46;
	 //  @line: 47
Block46:
	 //  @line: 47
	i128 := $addint((i128), (-1));
	 goto Block52;
	 //  @line: 37
Block44:
	 assert ($neref((r529), ($null))==1);
	 //  @line: 37
	r529 := $HeapVar[r529, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$left254];
	 goto Block47;
	 //  @line: 44
Block50:
	 assert ($neref((r529), ($null))==1);
	 //  @line: 44
	r529 := $HeapVar[r529, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$right255];
	 goto Block46;
	 //  @line: 48
Block52:
	 goto Block34;
	 //  @line: 37
Block47:
	 goto Block46;
}


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



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



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



	 //  @line: 53
// <MirrorBinTreeRec.Tree: void main(java.lang.String[])>
procedure void$MirrorBinTreeRec.Tree$main$2235($param_0 : [int]ref)
  modifies java.lang.String$lp$$rp$$MirrorBinTreeRec.Random$args256, $stringSize;
 {
var r030 : [int]ref;

 //temp local variables 
var $freshlocal0 : ref;

Block53:
	r030 := $param_0;
	 //  @line: 54
	java.lang.String$lp$$rp$$MirrorBinTreeRec.Random$args256 := r030;
	 //  @line: 55
	 call $freshlocal0 := MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$createTree$2234();
	 return;
}


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


	 //  @line: 1
// <MirrorBinTreeRec.Random: void <init>()>
procedure void$MirrorBinTreeRec.Random$$la$init$ra$$2236(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r032 : ref;
Block54:
	r032 := __this;
	 assert ($neref((r032), ($null))==1);
	 //  @line: 2
	 call void$java.lang.Object$$la$init$ra$$28((r032));
	 return;
}


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



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



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


	 //  @line: 7
// <MirrorBinTreeRec.Tree: void <init>(MirrorBinTreeRec.Tree,MirrorBinTreeRec.Tree)>
procedure void$MirrorBinTreeRec.Tree$$la$init$ra$$2231(__this : ref, $param_0 : ref, $param_1 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r010 : ref;
var r111 : ref;
var r212 : ref;
Block24:
	r010 := __this;
	r111 := $param_0;
	r212 := $param_1;
	 assert ($neref((r010), ($null))==1);
	 //  @line: 8
	 call void$java.lang.Object$$la$init$ra$$28((r010));
	 assert ($neref((r010), ($null))==1);
	 //  @line: 9
	$HeapVar[r010, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$left254] := r111;
	 assert ($neref((r010), ($null))==1);
	 //  @line: 10
	$HeapVar[r010, MirrorBinTreeRec.Tree$MirrorBinTreeRec.Tree$right255] := r212;
	 return;
}


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


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



// <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} $subint(x : int, y : int) returns (__ret : int) {
(x - y)
}