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$$Random$args254 : [int]ref;
var java.lang.Object$Tree$value298 : Field ref;
var int$Random$index0 : int;
var Tree$Tree$right297 : Field ref;
var Tree$Tree$left296 : 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);



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



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



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



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



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



	 //  @line: 4
// <Samefringe: void main(java.lang.String[])>
procedure void$Samefringe$main$2454($param_0 : [int]ref)
  modifies java.lang.String$lp$$rp$$Random$args254, $stringSize;
 {
var r09 : [int]ref;
var r213 : ref;
var r111 : ref;

 //temp local variables 
var $freshlocal0 : int;

Block20:
	r09 := $param_0;
	 //  @line: 5
	java.lang.String$lp$$rp$$Random$args254 := r09;
	 //  @line: 6
	 call r111 := Tree$Tree$createTree$2460();
	 //  @line: 7
	 call r213 := Tree$Tree$createTree$2460();
	 //  @line: 8
	 call $freshlocal0 := boolean$Samefringe$samefringe$2456((r111), (r213));
	 return;
}


	 //  @line: 10
// <Tree: void <init>()>
procedure void$Tree$$la$init$ra$$2458(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r036 : ref;
Block47:
	r036 := __this;
	 assert ($neref((r036), ($null))==1);
	 //  @line: 11
	 call void$java.lang.Object$$la$init$ra$$28((r036));
	 return;
}


	 //  @line: 25
// <Samefringe: boolean samefringe(Tree,Tree)>
procedure boolean$Samefringe$samefringe$2456($param_0 : ref, $param_1 : ref) returns (__ret : int) {
var $r129 : ref;
var r331 : ref;
var $r028 : ref;
var r230 : ref;
var $z032 : int;
Block31:
	r230 := $param_0;
	r331 := $param_1;
	 goto Block32;
	 //  @line: 26
Block32:
	 goto Block33, Block35;
	 //  @line: 26
Block33:
	 assume ($eqref((r230), ($null))==1);
	 goto Block34;
	 //  @line: 26
Block35:
	 //  @line: 26
	 assume ($negInt(($eqref((r230), ($null))))==1);
	 goto Block36;
	 //  @line: 30
Block34:
	 goto Block39, Block41;
	 //  @line: 30
Block36:
	 goto Block37, Block38;
	 //  @line: 30
Block39:
	 assume ($neref((r230), ($null))==1);
	 goto Block40;
	 //  @line: 30
Block41:
	 //  @line: 30
	 assume ($negInt(($neref((r230), ($null))))==1);
	 goto Block42;
	 //  @line: 30
Block37:
	 assume ($eqref((r331), ($null))==1);
	 goto Block34;
	 //  @line: 30
Block38:
	 //  @line: 30
	 assume ($negInt(($eqref((r331), ($null))))==1);
	 //  @line: 27
	 call $r028 := Tree$Samefringe$gopher$2455((r230));
	 assert ($neref(($r028), ($null))==1);
	 //  @line: 27
	r230 := $HeapVar[$r028, Tree$Tree$right297];
	 //  @line: 28
	 call $r129 := Tree$Samefringe$gopher$2455((r331));
	 assert ($neref(($r129), ($null))==1);
	 //  @line: 28
	r331 := $HeapVar[$r129, Tree$Tree$right297];
	 goto Block32;
	 //  @line: 30
Block40:
	 //  @line: 30
	$z032 := 0;
	 goto Block45;
	 //  @line: 30
Block42:
	 goto Block43, Block44;
	 //  @line: 30
Block45:
	 //  @line: 30
	__ret := $z032;
	 return;
	 //  @line: 30
Block43:
	 assume ($neref((r331), ($null))==1);
	 goto Block40;
	 //  @line: 30
Block44:
	 //  @line: 30
	 assume ($negInt(($neref((r331), ($null))))==1);
	 //  @line: 30
	$z032 := 1;
	 goto Block45;
}


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


// <Random: void <init>()>
procedure void$Random$$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} $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: 5
// <Tree: void <init>(Tree,Tree)>
procedure void$Tree$$la$init$ra$$2457(__this : ref, $param_0 : ref, $param_1 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r033 : ref;
var r235 : ref;
var r134 : ref;
Block46:
	r033 := __this;
	r134 := $param_0;
	r235 := $param_1;
	 assert ($neref((r033), ($null))==1);
	 //  @line: 6
	 call void$java.lang.Object$$la$init$ra$$28((r033));
	 assert ($neref((r033), ($null))==1);
	 //  @line: 7
	$HeapVar[r033, Tree$Tree$left296] := r134;
	 assert ($neref((r033), ($null))==1);
	 //  @line: 8
	$HeapVar[r033, Tree$Tree$right297] := r235;
	 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);



	 //  @line: 20
// <Tree: Tree createTree()>
procedure Tree$Tree$createTree$2460() returns (__ret : ref)
  modifies $HeapVar;
 {
var $r147 : ref;
var $r248 : ref;
var r043 : ref;
var r552 : ref;
var i046 : int;
var $r450 : ref;
var i151 : int;
var $r349 : ref;
	 //  @line: 21
Block51:
	 //  @line: 21
	 call i151 := int$Random$random$2229();
	 goto Block52;
	 //  @line: 22
Block52:
	 goto Block53, Block55;
	 //  @line: 22
Block53:
	 assume ($neint((i151), (0))==1);
	 goto Block54;
	 //  @line: 22
Block55:
	 //  @line: 22
	 assume ($negInt(($neint((i151), (0))))==1);
	 //  @line: 23
	__ret := $null;
	 return;
	 //  @line: 25
Block54:
	 //  @line: 25
	 call r043 := Tree$Tree$createNode$2459();
	 goto Block56;
	 //  @line: 26
Block56:
	 //  @line: 26
	r552 := r043;
	 goto Block57;
	 //  @line: 28
Block57:
	 goto Block60, Block58;
	 //  @line: 28
Block60:
	 //  @line: 28
	 assume ($negInt(($leint((i151), (0))))==1);
	 //  @line: 29
	 call i046 := int$Random$random$2229();
	 goto Block61;
	 //  @line: 28
Block58:
	 assume ($leint((i151), (0))==1);
	 goto Block59;
	 //  @line: 30
Block61:
	 goto Block64, Block62;
	 //  @line: 48
Block59:
	 //  @line: 48
	__ret := r043;
	 return;
	 //  @line: 30
Block64:
	 //  @line: 30
	 assume ($negInt(($leint((i046), (0))))==1);
	 assert ($neref((r552), ($null))==1);
	 //  @line: 31
	$r349 := $HeapVar[r552, Tree$Tree$left296];
	 goto Block65;
	 //  @line: 30
Block62:
	 assume ($leint((i046), (0))==1);
	 goto Block63;
	 //  @line: 31
Block65:
	 goto Block68, Block66;
	 //  @line: 38
Block63:
	 assert ($neref((r552), ($null))==1);
	 //  @line: 38
	$r147 := $HeapVar[r552, Tree$Tree$right297];
	 goto Block71;
	 //  @line: 31
Block68:
	 //  @line: 31
	 assume ($negInt(($neref(($r349), ($null))))==1);
	 //  @line: 32
	 call $r450 := Tree$Tree$createNode$2459();
	 assert ($neref((r552), ($null))==1);
	 //  @line: 32
	$HeapVar[r552, Tree$Tree$left296] := $r450;
	 //  @line: 33
	r552 := r043;
	 goto Block69;
	 //  @line: 31
Block66:
	 assume ($neref(($r349), ($null))==1);
	 goto Block67;
	 //  @line: 38
Block71:
	 goto Block74, Block72;
	 //  @line: 45
Block69:
	 //  @line: 45
	i151 := $addint((i151), (-1));
	 goto Block75;
	 //  @line: 35
Block67:
	 assert ($neref((r552), ($null))==1);
	 //  @line: 35
	r552 := $HeapVar[r552, Tree$Tree$left296];
	 goto Block70;
	 //  @line: 38
Block74:
	 //  @line: 38
	 assume ($negInt(($neref(($r147), ($null))))==1);
	 //  @line: 39
	 call $r248 := Tree$Tree$createNode$2459();
	 assert ($neref((r552), ($null))==1);
	 //  @line: 39
	$HeapVar[r552, Tree$Tree$right297] := $r248;
	 //  @line: 40
	r552 := r043;
	 goto Block69;
	 //  @line: 38
Block72:
	 assume ($neref(($r147), ($null))==1);
	 goto Block73;
	 //  @line: 46
Block75:
	 goto Block57;
	 //  @line: 35
Block70:
	 goto Block69;
	 //  @line: 42
Block73:
	 assert ($neref((r552), ($null))==1);
	 //  @line: 42
	r552 := $HeapVar[r552, Tree$Tree$right297];
	 goto Block69;
}


// 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: 5
// <Random: int random()>
procedure int$Random$random$2229() returns (__ret : int)
  modifies $stringSize, int$Random$index0;
 {
var $i02 : int;
var $i37 : int;
var $i15 : int;
var r04 : ref;
var $r13 : [int]ref;
var $i26 : int;
	 //  @line: 6
Block17:
	 //  @line: 6
	$r13 := java.lang.String$lp$$rp$$Random$args254;
	 //  @line: 6
	$i02 := int$Random$index0;
	 assert ($geint(($i02), (0))==1);
	 assert ($ltint(($i02), ($refArrSize[$r13[$arrSizeIdx]]))==1);
	 //  @line: 6
	r04 := $r13[$i02];
	 //  @line: 7
	$i15 := int$Random$index0;
	 //  @line: 7
	$i26 := $addint(($i15), (1));
	 //  @line: 7
	int$Random$index0 := $i26;
	$i37 := $stringSize[r04];
	 //  @line: 8
	__ret := $i37;
	 return;
}


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



	 //  @line: 50
// <Tree: void main(java.lang.String[])>
procedure void$Tree$main$2461($param_0 : [int]ref)
  modifies java.lang.String$lp$$rp$$Random$args254, $stringSize;
 {
var r053 : [int]ref;

 //temp local variables 
var $freshlocal0 : ref;

Block76:
	r053 := $param_0;
	 //  @line: 51
	java.lang.String$lp$$rp$$Random$args254 := r053;
	 //  @line: 52
	 call $freshlocal0 := Tree$Tree$createTree$2460();
	 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
}


// <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} $instanceof($param00 : ref, $param11 : classConst) returns (__ret : int);



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



// <Samefringe: void <init>()>
procedure void$Samefringe$$la$init$ra$$2453(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r08 : ref;
Block19:
	r08 := __this;
	 assert ($neref((r08), ($null))==1);
	 //  @line: 1
	 call void$java.lang.Object$$la$init$ra$$28((r08));
	 return;
}


// 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: 14
// <Samefringe: Tree gopher(Tree)>
procedure Tree$Samefringe$gopher$2455($param_0 : ref) returns (__ret : ref) {
var r824 : ref;
var $r519 : ref;
var $r723 : ref;
var r221 : ref;
var r018 : ref;
var $r622 : ref;
var $r316 : ref;
var $r417 : ref;
var r120 : ref;
Block21:
	r824 := $param_0;
	 goto Block22;
	 //  @line: 15
Block22:
	 goto Block23, Block25;
	 //  @line: 15
Block23:
	 assume ($eqref((r824), ($null))==1);
	 goto Block24;
	 //  @line: 15
Block25:
	 //  @line: 15
	 assume ($negInt(($eqref((r824), ($null))))==1);
	 assert ($neref((r824), ($null))==1);
	 //  @line: 21
	$r316 := $HeapVar[r824, Tree$Tree$left296];
	 goto Block26;
	 //  @line: 21
Block24:
	 //  @line: 21
	__ret := r824;
	 return;
	 //  @line: 21
Block26:
	 goto Block28, Block27;
	 //  @line: 21
Block28:
	 //  @line: 21
	 assume ($negInt(($eqref(($r316), ($null))))==1);
	 assert ($neref((r824), ($null))==1);
	 //  @line: 16
	$r417 := $HeapVar[r824, Tree$Tree$left296];
	 assert ($neref(($r417), ($null))==1);
	 //  @line: 16
	r018 := $HeapVar[$r417, Tree$Tree$left296];
	 assert ($neref((r824), ($null))==1);
	 //  @line: 17
	$r519 := $HeapVar[r824, Tree$Tree$left296];
	 assert ($neref(($r519), ($null))==1);
	 //  @line: 17
	r120 := $HeapVar[$r519, Tree$Tree$right297];
	 assert ($neref((r824), ($null))==1);
	 //  @line: 18
	r221 := $HeapVar[r824, Tree$Tree$right297];
	 //  @line: 19
	$r622 := $newvariable((29));
	 assume ($neref(($newvariable((29))), ($null))==1);
	 //  @line: 19
	$r723 := $newvariable((30));
	 assume ($neref(($newvariable((30))), ($null))==1);
	 assert ($neref(($r723), ($null))==1);
	 //  @line: 19
	 call void$Tree$$la$init$ra$$2457(($r723), (r120), (r221));
	 assert ($neref(($r622), ($null))==1);
	 //  @line: 19
	 call void$Tree$$la$init$ra$$2457(($r622), (r018), ($r723));
	 //  @line: 19
	r824 := $r622;
	 goto Block22;
	 //  @line: 21
Block27:
	 assume ($eqref(($r316), ($null))==1);
	 goto Block24;
}


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



	 //  @line: 14
// <Tree: Tree createNode()>
procedure Tree$Tree$createNode$2459() returns (__ret : ref)
  modifies $HeapVar;
 {
var $r137 : ref;
var r038 : ref;
var $r239 : ref;
	 //  @line: 15
Block48:
	 //  @line: 15
	$r137 := $newvariable((49));
	 assume ($neref(($newvariable((49))), ($null))==1);
	 assert ($neref(($r137), ($null))==1);
	 //  @line: 15
	 call void$Tree$$la$init$ra$$2458(($r137));
	 //  @line: 15
	r038 := $r137;
	 //  @line: 16
	$r239 := $newvariable((50));
	 assume ($neref(($newvariable((50))), ($null))==1);
	 assert ($neref(($r239), ($null))==1);
	 //  @line: 16
	 call void$java.lang.Object$$la$init$ra$$28(($r239));
	 assert ($neref((r038), ($null))==1);
	 //  @line: 16
	$HeapVar[r038, java.lang.Object$Tree$value298] := $r239;
	 //  @line: 17
	__ret := r038;
	 return;
}


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



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