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 
const unique LinkedList : classConst ;



var LinkedList$Node$LinkedList$Node$link298 : Field ref;
var LinkedList$LinkedList$Node$this$0299 : Field ref;
var int$Entry$count0 : Field int;
var java.lang.Object$LinkedList$Node$data297 : Field ref;
var LinkedList$Node$LinkedList$head296 : Field ref;
var $fresh1 : ref;
var java.lang.String$Entry$item254 : Field ref;


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



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



// <java.lang.Object: java.lang.Class getClass()>
procedure java.lang.Class$java.lang.Object$getClass$30(__this : ref) returns (__ret : ref);



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



	 //  @line: 124
// <LinkedList: boolean equals(java.lang.Object)>
procedure boolean$LinkedList$equals$2463(__this : ref, $param_0 : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var r267 : ref;
var $z175 : int;
var $i069 : int;
var r165 : ref;
var r578 : ref;
var r679 : ref;
var $r373 : ref;
var r068 : ref;
var $z066 : int;
var $i170 : int;
var $r474 : ref;
Block80:
	r068 := __this;
	r165 := $param_0;
	 //  @line: 125
	$z066 := $instanceof((r165), (LinkedList));
	 goto Block81;
	 //  @line: 125
Block81:
	 goto Block82, Block84;
	 //  @line: 125
Block82:
	 assume ($neint(($z066), (0))==1);
	 goto Block83;
	 //  @line: 125
Block84:
	 //  @line: 125
	 assume ($negInt(($neint(($z066), (0))))==1);
	 //  @line: 126
	__ret := 0;
	 return;
	 //  @line: 129
Block83:
	 //  @line: 129
	r267 := r165;
	 goto Block85;
	 //  @line: 130
Block85:
	 assert ($neref((r068), ($null))==1);
	 //  @line: 130
	 call $i069 := int$LinkedList$size$2456((r068));
	 assert ($neref((r267), ($null))==1);
	 //  @line: 130
	 call $i170 := int$LinkedList$size$2456((r267));
	 goto Block86;
	 //  @line: 130
Block86:
	 goto Block89, Block87;
	 //  @line: 130
Block89:
	 //  @line: 130
	 assume ($negInt(($eqint(($i069), ($i170))))==1);
	 //  @line: 131
	__ret := 0;
	 return;
	 //  @line: 130
Block87:
	 assume ($eqint(($i069), ($i170))==1);
	 goto Block88;
	 //  @line: 132
Block88:
	 assert ($neref((r068), ($null))==1);
	 //  @line: 132
	r578 := $HeapVar[r068, LinkedList$Node$LinkedList$head296];
	 goto Block90;
	 //  @line: 133
Block90:
	 assert ($neref((r267), ($null))==1);
	 //  @line: 133
	r679 := $HeapVar[r267, LinkedList$Node$LinkedList$head296];
	 goto Block91;
	 //  @line: 134
Block91:
	 goto Block92, Block94;
	 //  @line: 134
Block92:
	 assume ($eqref((r578), ($null))==1);
	 goto Block93;
	 //  @line: 134
Block94:
	 //  @line: 134
	 assume ($negInt(($eqref((r578), ($null))))==1);
	 //  @line: 136
	 call $r373 := java.lang.Object$LinkedList$Node$access$100$2468((r578));
	 //  @line: 136
	 call $r474 := java.lang.Object$LinkedList$Node$access$100$2468((r679));
	 assert ($neref(($r373), ($null))==1);
	 //  @line: 136
	 call $z175 := boolean$java.lang.Object$equals$32(($r373), ($r474));
	 goto Block95;
	 //  @line: 141
Block93:
	 //  @line: 141
	__ret := 1;
	 return;
	 //  @line: 136
Block95:
	 goto Block98, Block96;
	 //  @line: 136
Block98:
	 //  @line: 136
	 assume ($negInt(($neint(($z175), (0))))==1);
	 //  @line: 137
	__ret := 0;
	 return;
	 //  @line: 136
Block96:
	 assume ($neint(($z175), (0))==1);
	 goto Block97;
	 //  @line: 138
Block97:
	 //  @line: 138
	 call r578 := LinkedList$Node$LinkedList$Node$access$000$2467((r578));
	 goto Block99;
	 //  @line: 139
Block99:
	 //  @line: 139
	 call r679 := LinkedList$Node$LinkedList$Node$access$000$2467((r679));
	 goto Block91;
}


// <java.lang.StringBuilder: void <init>()>
procedure void$java.lang.StringBuilder$$la$init$ra$$2231(__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
}


	 //  @line: 146
// <LinkedList: void main(java.lang.String[])>
procedure void$LinkedList$main$2464($param_0 : [int]ref)
  modifies $stringSize;
 {
var i296 : int;
var $i084 : int;
var r998 : ref;
var r181 : ref;
var $r386 : ref;
var i499 : int;
var $r280 : ref;
var $r894 : ref;
var $r793 : ref;
var i397 : int;
var i5101 : int;
var r083 : [int]ref;
var $r487 : ref;
var r11102 : ref;
var r10100 : ref;
var $r590 : ref;
var $r691 : ref;

 //temp local variables 
var $freshlocal0 : int;

Block100:
	r083 := $param_0;
	 //  @line: 147
	$r280 := $newvariable((101));
	 assume ($neref(($newvariable((101))), ($null))==1);
	 assert ($neref(($r280), ($null))==1);
	 //  @line: 147
	 call void$LinkedList$$la$init$ra$$2453(($r280));
	 //  @line: 147
	r181 := $r280;
	 //  @line: 149
	i296 := 1;
	 goto Block102;
	 //  @line: 149
Block102:
	 //  @line: 149
	$i084 := $refArrSize[r083[$arrSizeIdx]];
	 goto Block103;
	 //  @line: 149
Block103:
	 goto Block104, Block106;
	 //  @line: 149
Block104:
	 assume ($geint((i296), ($i084))==1);
	 goto Block105;
	 //  @line: 149
Block106:
	 //  @line: 149
	 assume ($negInt(($geint((i296), ($i084))))==1);
	 //  @line: 150
	$r386 := $newvariable((107));
	 assume ($neref(($newvariable((107))), ($null))==1);
	 assert ($geint((i296), (0))==1);
	 assert ($ltint((i296), ($refArrSize[r083[$arrSizeIdx]]))==1);
	 //  @line: 150
	$r487 := r083[i296];
	 //  @line: 150
	i397 := $addint((i296), (1));
	 assert ($neref(($r386), ($null))==1);
	 //  @line: 150
	 call void$Entry$$la$init$ra$$2228(($r386), ($r487), (i296));
	 //  @line: 150
	r998 := $r386;
	 assert ($neref((r181), ($null))==1);
	 //  @line: 151
	 call void$LinkedList$addToStart$2454((r181), (r998));
	 //  @line: 152
	$r590 := $newvariable((108));
	 assume ($neref(($newvariable((108))), ($null))==1);
	 assert ($geint((i397), (0))==1);
	 assert ($ltint((i397), ($refArrSize[r083[$arrSizeIdx]]))==1);
	 //  @line: 152
	$r691 := r083[i397];
	 //  @line: 152
	i499 := $addint((i397), (1));
	 assert ($neref(($r590), ($null))==1);
	 //  @line: 152
	 call void$Entry$$la$init$ra$$2228(($r590), ($r691), (i397));
	 //  @line: 152
	r10100 := $r590;
	 assert ($neref((r181), ($null))==1);
	 //  @line: 153
	 call void$LinkedList$addToStart$2454((r181), (r10100));
	 //  @line: 154
	$r793 := $newvariable((109));
	 assume ($neref(($newvariable((109))), ($null))==1);
	 assert ($geint((i499), (0))==1);
	 assert ($ltint((i499), ($refArrSize[r083[$arrSizeIdx]]))==1);
	 //  @line: 154
	$r894 := r083[i499];
	 //  @line: 154
	i5101 := $addint((i499), (1));
	 assert ($neref(($r793), ($null))==1);
	 //  @line: 154
	 call void$Entry$$la$init$ra$$2228(($r793), ($r894), (i499));
	 //  @line: 154
	r11102 := $r793;
	 assert ($neref((r181), ($null))==1);
	 //  @line: 155
	 call void$LinkedList$addToStart$2454((r181), (r11102));
	 //  @line: 149
	i296 := $addint((i5101), (1));
	 goto Block102;
	 //  @line: 158
Block105:
	 assert ($neref((r181), ($null))==1);
	 //  @line: 158
	 call $freshlocal0 := int$LinkedList$size$2456((r181));
	 goto Block110;
	 //  @line: 161
Block110:
	 assert ($neref((r181), ($null))==1);
	 //  @line: 161
	 call void$LinkedList$outputList$2460((r181));
	 return;
}


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



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



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



	 //  @line: 33
// <LinkedList: void addToStart(java.lang.Object)>
procedure void$LinkedList$addToStart$2454(__this : ref, $param_0 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r025 : ref;
var $r226 : ref;
var r127 : ref;
var $r328 : ref;
Block39:
	r025 := __this;
	r127 := $param_0;
	 //  @line: 34
	$r226 := $newvariable((40));
	 assume ($neref(($newvariable((40))), ($null))==1);
	 assert ($neref((r025), ($null))==1);
	 //  @line: 34
	$r328 := $HeapVar[r025, LinkedList$Node$LinkedList$head296];
	 assert ($neref(($r226), ($null))==1);
	 //  @line: 34
	 call void$LinkedList$Node$$la$init$ra$$2466(($r226), (r025), (r127), ($r328));
	 assert ($neref((r025), ($null))==1);
	 //  @line: 34
	$HeapVar[r025, LinkedList$Node$LinkedList$head296] := $r226;
	 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} $ltint(x : int, y : int) returns (__ret : int) {
if (x < y) then 1 else 0
}


	 //  @line: 2
// <LinkedList$Node: java.lang.Object access$100(LinkedList$Node)>
procedure java.lang.Object$LinkedList$Node$access$100$2468($param_0 : ref) returns (__ret : ref) {
var r0111 : ref;
var $r1112 : ref;
Block114:
	r0111 := $param_0;
	 assert ($neref((r0111), ($null))==1);
	 //  @line: 3
	$r1112 := $HeapVar[r0111, java.lang.Object$LinkedList$Node$data297];
	 //  @line: 3
	__ret := $r1112;
	 return;
}


	 //  @line: 42
// <LinkedList: boolean deleteHeadNode()>
procedure boolean$LinkedList$deleteHeadNode$2455(__this : ref) returns (__ret : int)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r029 : ref;
var $r130 : ref;
var $r332 : ref;
var $r231 : ref;
Block41:
	r029 := __this;
	 assert ($neref((r029), ($null))==1);
	 //  @line: 43
	$r130 := $HeapVar[r029, LinkedList$Node$LinkedList$head296];
	 goto Block42;
	 //  @line: 43
Block42:
	 goto Block45, Block43;
	 //  @line: 43
Block45:
	 //  @line: 43
	 assume ($negInt(($eqref(($r130), ($null))))==1);
	 assert ($neref((r029), ($null))==1);
	 //  @line: 45
	$r231 := $HeapVar[r029, LinkedList$Node$LinkedList$head296];
	 //  @line: 45
	 call $r332 := LinkedList$Node$LinkedList$Node$access$000$2467(($r231));
	 assert ($neref((r029), ($null))==1);
	 //  @line: 45
	$HeapVar[r029, LinkedList$Node$LinkedList$head296] := $r332;
	 //  @line: 46
	__ret := 1;
	 return;
	 //  @line: 43
Block43:
	 assume ($eqref(($r130), ($null))==1);
	 goto Block44;
	 //  @line: 49
Block44:
	 //  @line: 49
	__ret := 0;
	 return;
}


// procedure is generated by joogie.
function {:inline true} $mulint($param00 : int, $param11 : int) 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} $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);



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



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



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


	 //  @line: 23
// <LinkedList: void <init>()>
procedure void$LinkedList$$la$init$ra$$2453(__this : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r024 : ref;
Block38:
	r024 := __this;
	 assert ($neref((r024), ($null))==1);
	 //  @line: 24
	 call void$java.lang.Object$$la$init$ra$$28((r024));
	 assert ($neref((r024), ($null))==1);
	 //  @line: 25
	$HeapVar[r024, LinkedList$Node$LinkedList$head296] := $null;
	 return;
}


// procedure is generated by joogie.
function {:inline true} $geref($param00 : ref, $param11 : ref) 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} $eqintarray($param00 : [int]int, $param11 : [int]int) returns (__ret : int);



	 //  @line: 56
// <LinkedList: int size()>
procedure int$LinkedList$size$2456(__this : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var r034 : ref;
var r138 : ref;
var i037 : int;
Block46:
	r034 := __this;
	 //  @line: 57
	i037 := 0;
	 assert ($neref((r034), ($null))==1);
	 //  @line: 58
	r138 := $HeapVar[r034, LinkedList$Node$LinkedList$head296];
	 goto Block47;
	 //  @line: 59
Block47:
	 goto Block50, Block48;
	 //  @line: 59
Block50:
	 //  @line: 59
	 assume ($negInt(($eqref((r138), ($null))))==1);
	 //  @line: 61
	i037 := $addint((i037), (1));
	 //  @line: 62
	 call r138 := LinkedList$Node$LinkedList$Node$access$000$2467((r138));
	 goto Block47;
	 //  @line: 59
Block48:
	 assume ($eqref((r138), ($null))==1);
	 goto Block49;
	 //  @line: 64
Block49:
	 //  @line: 64
	__ret := i037;
	 return;
}


	 //  @line: 110
// <LinkedList: boolean isEmpty()>
procedure boolean$LinkedList$isEmpty$2461(__this : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var $r161 : ref;
var $z063 : int;
var r060 : ref;
Block73:
	r060 := __this;
	 assert ($neref((r060), ($null))==1);
	 //  @line: 111
	$r161 := $HeapVar[r060, LinkedList$Node$LinkedList$head296];
	 goto Block74;
	 //  @line: 111
Block74:
	 goto Block77, Block75;
	 //  @line: 111
Block77:
	 //  @line: 111
	 assume ($negInt(($neref(($r161), ($null))))==1);
	 //  @line: 111
	$z063 := 1;
	 goto Block78;
	 //  @line: 111
Block75:
	 assume ($neref(($r161), ($null))==1);
	 goto Block76;
	 //  @line: 111
Block78:
	 //  @line: 111
	__ret := $z063;
	 return;
	 //  @line: 111
Block76:
	 //  @line: 111
	$z063 := 0;
	 goto Block78;
}


// procedure is generated by joogie.
function {:inline true} $lereal($param00 : realVar, $param11 : realVar) 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);



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



	 //  @line: 115
// <LinkedList: void clear()>
procedure void$LinkedList$clear$2462(__this : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r064 : ref;
Block79:
	r064 := __this;
	 assert ($neref((r064), ($null))==1);
	 //  @line: 116
	$HeapVar[r064, LinkedList$Node$LinkedList$head296] := $null;
	 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
}


// <java.lang.Object: boolean equals(java.lang.Object)>
procedure boolean$java.lang.Object$equals$32(__this : ref, $param_0 : ref) returns (__ret : int);



// procedure is generated by joogie.
function {:inline true} $andint($param00 : int, $param11 : int) 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);



	 //  @line: 18
// <Entry: boolean equals(java.lang.Object)>
procedure boolean$Entry$equals$2230(__this : ref, $param_0 : ref) returns (__ret : int)
  modifies $stringSize;
  requires ($neref((__this), ($null))==1);
 {
var $i121 : int;
var r112 : ref;
var $r314 : ref;
var $r618 : ref;
var $z123 : int;
var $z019 : int;
var r216 : ref;
var $r517 : ref;
var $i020 : int;
var $r415 : ref;
var r013 : ref;
Block19:
	r013 := __this;
	r112 := $param_0;
	 goto Block20;
	 //  @line: 19
Block20:
	 goto Block21, Block23;
	 //  @line: 19
Block21:
	 assume ($neref((r112), ($null))==1);
	 goto Block22;
	 //  @line: 19
Block23:
	 //  @line: 19
	 assume ($negInt(($neref((r112), ($null))))==1);
	 //  @line: 20
	__ret := 0;
	 return;
	 //  @line: 21
Block22:
	 assert ($neref((r013), ($null))==1);
	 //  @line: 21
	 call $r314 := java.lang.Class$java.lang.Object$getClass$30((r013));
	 goto Block24;
	 //  @line: 21
Block24:
	 assert ($neref((r112), ($null))==1);
	 //  @line: 21
	 call $r415 := java.lang.Class$java.lang.Object$getClass$30((r112));
	 goto Block25;
	 //  @line: 21
Block25:
	 goto Block26, Block28;
	 //  @line: 21
Block26:
	 assume ($eqref(($r314), ($r415))==1);
	 goto Block27;
	 //  @line: 21
Block28:
	 //  @line: 21
	 assume ($negInt(($eqref(($r314), ($r415))))==1);
	 //  @line: 22
	__ret := 0;
	 return;
	 //  @line: 25
Block27:
	 //  @line: 25
	r216 := r112;
	 goto Block29;
	 //  @line: 26
Block29:
	 assert ($neref((r013), ($null))==1);
	 //  @line: 26
	$r618 := $HeapVar[r013, java.lang.String$Entry$item254];
	 assert ($neref((r216), ($null))==1);
	 //  @line: 26
	$r517 := $HeapVar[r216, java.lang.String$Entry$item254];
	 assert ($neref(($r618), ($null))==1);
	 //  @line: 26
	 call $z019 := boolean$java.lang.String$equals$72(($r618), ($r517));
	 goto Block30;
	 //  @line: 26
Block30:
	 goto Block31, Block33;
	 //  @line: 26
Block31:
	 assume ($eqint(($z019), (0))==1);
	 goto Block32;
	 //  @line: 26
Block33:
	 //  @line: 26
	 assume ($negInt(($eqint(($z019), (0))))==1);
	 assert ($neref((r013), ($null))==1);
	 //  @line: 26
	$i121 := $HeapVar[r013, int$Entry$count0];
	 assert ($neref((r216), ($null))==1);
	 //  @line: 26
	$i020 := $HeapVar[r216, int$Entry$count0];
	 goto Block34;
	 //  @line: 26
Block32:
	 //  @line: 26
	$z123 := 0;
	 goto Block37;
	 //  @line: 26
Block34:
	 goto Block36, Block35;
	 //  @line: 26
Block37:
	 //  @line: 26
	__ret := $z123;
	 return;
	 //  @line: 26
Block36:
	 //  @line: 26
	 assume ($negInt(($neint(($i121), ($i020))))==1);
	 //  @line: 26
	$z123 := 1;
	 goto Block37;
	 //  @line: 26
Block35:
	 assume ($neint(($i121), ($i020))==1);
	 goto Block32;
}


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


// 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} $modreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar);



// 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: 13
// <Entry: java.lang.String toString()>
procedure java.lang.String$Entry$toString$2229(__this : ref) returns (__ret : ref)
  modifies $stringSize;
  requires ($neref((__this), ($null))==1);
 {
var r05 : ref;
var $r26 : ref;
var $r48 : ref;
var $i09 : int;
var $r37 : ref;
var $r611 : ref;
var $r14 : ref;
var $r510 : ref;
Block17:
	r05 := __this;
	 //  @line: 14
	$r14 := $newvariable((18));
	 assume ($neref(($newvariable((18))), ($null))==1);
	 assert ($neref(($r14), ($null))==1);
	 //  @line: 14
	 call void$java.lang.StringBuilder$$la$init$ra$$2231(($r14));
	 assert ($neref((r05), ($null))==1);
	 //  @line: 14
	$r26 := $HeapVar[r05, java.lang.String$Entry$item254];
	 assert ($neref(($r14), ($null))==1);
	 //  @line: 14
	 call $r37 := java.lang.StringBuilder$java.lang.StringBuilder$append$2236(($r14), ($r26));
	$stringSize[$fresh1] := 1;
	 assert ($neref(($r37), ($null))==1);
	 //  @line: 14
	 call $r48 := java.lang.StringBuilder$java.lang.StringBuilder$append$2236(($r37), ($fresh1));
	 assert ($neref((r05), ($null))==1);
	 //  @line: 14
	$i09 := $HeapVar[r05, int$Entry$count0];
	 assert ($neref(($r48), ($null))==1);
	 //  @line: 14
	 call $r510 := java.lang.StringBuilder$java.lang.StringBuilder$append$2244(($r48), ($i09));
	 assert ($neref(($r510), ($null))==1);
	 //  @line: 14
	 call $r611 := java.lang.String$java.lang.StringBuilder$toString$2269(($r510));
	 //  @line: 14
	__ret := $r611;
	 return;
}


	 //  @line: 77
// <LinkedList: LinkedList$Node find(java.lang.Object)>
procedure LinkedList$Node$LinkedList$find$2458(__this : ref, $param_0 : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var r247 : ref;
var r148 : ref;
var r351 : ref;
var $z049 : int;
var r044 : ref;
Block57:
	r044 := __this;
	r148 := $param_0;
	 assert ($neref((r044), ($null))==1);
	 //  @line: 78
	r351 := $HeapVar[r044, LinkedList$Node$LinkedList$head296];
	 goto Block58;
	 //  @line: 80
Block58:
	 goto Block59, Block61;
	 //  @line: 80
Block59:
	 assume ($eqref((r351), ($null))==1);
	 goto Block60;
	 //  @line: 80
Block61:
	 //  @line: 80
	 assume ($negInt(($eqref((r351), ($null))))==1);
	 //  @line: 82
	 call r247 := java.lang.Object$LinkedList$Node$access$100$2468((r351));
	 assert ($neref((r247), ($null))==1);
	 //  @line: 83
	 call $z049 := boolean$java.lang.Object$equals$32((r247), (r148));
	 goto Block62;
	 //  @line: 87
Block60:
	 //  @line: 87
	__ret := $null;
	 return;
	 //  @line: 83
Block62:
	 goto Block63, Block65;
	 //  @line: 83
Block63:
	 assume ($eqint(($z049), (0))==1);
	 goto Block64;
	 //  @line: 83
Block65:
	 //  @line: 83
	 assume ($negInt(($eqint(($z049), (0))))==1);
	 //  @line: 84
	__ret := r351;
	 return;
	 //  @line: 85
Block64:
	 //  @line: 85
	 call r351 := LinkedList$Node$LinkedList$Node$access$000$2467((r351));
	 goto Block66;
	 //  @line: 85
Block66:
	 goto Block58;
}


// <java.lang.String: boolean equals(java.lang.Object)>
procedure boolean$java.lang.String$equals$72(__this : ref, $param_0 : 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} $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: 14
// <LinkedList$Node: void <init>(LinkedList,java.lang.Object,LinkedList$Node)>
procedure void$LinkedList$Node$$la$init$ra$$2466(__this : ref, $param_0 : ref, $param_1 : ref, $param_2 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r3108 : ref;
var r2107 : ref;
var r0105 : ref;
var r1106 : ref;
Block112:
	r0105 := __this;
	r1106 := $param_0;
	r2107 := $param_1;
	r3108 := $param_2;
	 assert ($neref((r0105), ($null))==1);
	 //  @line: 15
	$HeapVar[r0105, LinkedList$LinkedList$Node$this$0299] := r1106;
	 assert ($neref((r0105), ($null))==1);
	 //  @line: 15
	 call void$java.lang.Object$$la$init$ra$$28((r0105));
	 assert ($neref((r0105), ($null))==1);
	 //  @line: 16
	$HeapVar[r0105, java.lang.Object$LinkedList$Node$data297] := r2107;
	 assert ($neref((r0105), ($null))==1);
	 //  @line: 17
	$HeapVar[r0105, LinkedList$Node$LinkedList$Node$link298] := r3108;
	 return;
}


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



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



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


	 //  @line: 8
// <LinkedList$Node: void <init>(LinkedList)>
procedure void$LinkedList$Node$$la$init$ra$$2465(__this : ref, $param_0 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r1104 : ref;
var r0103 : ref;
Block111:
	r0103 := __this;
	r1104 := $param_0;
	 assert ($neref((r0103), ($null))==1);
	 //  @line: 9
	$HeapVar[r0103, LinkedList$LinkedList$Node$this$0299] := r1104;
	 assert ($neref((r0103), ($null))==1);
	 //  @line: 9
	 call void$java.lang.Object$$la$init$ra$$28((r0103));
	 assert ($neref((r0103), ($null))==1);
	 //  @line: 10
	$HeapVar[r0103, java.lang.Object$LinkedList$Node$data297] := $null;
	 assert ($neref((r0103), ($null))==1);
	 //  @line: 11
	$HeapVar[r0103, LinkedList$Node$LinkedList$Node$link298] := $null;
	 return;
}


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


// <java.lang.StringBuilder: java.lang.StringBuilder append(int)>
procedure java.lang.StringBuilder$java.lang.StringBuilder$append$2244(__this : ref, $param_0 : int) returns (__ret : ref);



// 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} $reftointarr($param00 : ref) returns (__ret : [int]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);



	 //  @line: 6
// <Entry: void <init>(java.lang.String,int)>
procedure void$Entry$$la$init$ra$$2228(__this : ref, $param_0 : ref, $param_1 : int)
  modifies $stringSize, $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var i03 : int;
var r12 : ref;
var r01 : ref;
Block16:
	r01 := __this;
	r12 := $param_0;
	i03 := $param_1;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 7
	 call void$java.lang.Object$$la$init$ra$$28((r01));
	 assert ($neref((r01), ($null))==1);
	 //  @line: 8
	$HeapVar[r01, java.lang.String$Entry$item254] := r12;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 9
	$HeapVar[r01, int$Entry$count0] := i03;
	 return;
}


// <java.lang.StringBuilder: java.lang.String toString()>
procedure java.lang.String$java.lang.StringBuilder$toString$2269(__this : ref) returns (__ret : ref);



	 //  @line: 2
// <LinkedList$Node: LinkedList$Node access$000(LinkedList$Node)>
procedure LinkedList$Node$LinkedList$Node$access$000$2467($param_0 : ref) returns (__ret : ref) {
var $r1110 : ref;
var r0109 : ref;
Block113:
	r0109 := $param_0;
	 assert ($neref((r0109), ($null))==1);
	 //  @line: 3
	$r1110 := $HeapVar[r0109, LinkedList$Node$LinkedList$Node$link298];
	 //  @line: 3
	__ret := $r1110;
	 return;
}


// 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} $realtoint($param00 : realVar) 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} $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} $negRef($param00 : ref) 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: 95
// <LinkedList: java.lang.Object findData(java.lang.Object)>
procedure java.lang.Object$LinkedList$findData$2459(__this : ref, $param_0 : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var r153 : ref;
var $r355 : ref;
var r052 : ref;
var $r254 : ref;
Block67:
	r052 := __this;
	r153 := $param_0;
	 assert ($neref((r052), ($null))==1);
	 //  @line: 96
	 call $r254 := LinkedList$Node$LinkedList$find$2458((r052), (r153));
	 //  @line: 96
	 call $r355 := java.lang.Object$LinkedList$Node$access$100$2468(($r254));
	 //  @line: 96
	__ret := $r355;
	 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} $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
}


	 //  @line: 100
// <LinkedList: void outputList()>
procedure void$LinkedList$outputList$2460(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r159 : ref;
var r056 : ref;
Block68:
	r056 := __this;
	 assert ($neref((r056), ($null))==1);
	 //  @line: 101
	r159 := $HeapVar[r056, LinkedList$Node$LinkedList$head296];
	 goto Block69;
	 //  @line: 102
Block69:
	 goto Block70, Block72;
	 //  @line: 102
Block70:
	 assume ($eqref((r159), ($null))==1);
	 goto Block71;
	 //  @line: 102
Block72:
	 //  @line: 102
	 assume ($negInt(($eqref((r159), ($null))))==1);
	 //  @line: 105
	 call r159 := LinkedList$Node$LinkedList$Node$access$000$2467((r159));
	 goto Block69;
	 //  @line: 107
Block71:
	 return;
}


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


// <java.lang.StringBuilder: java.lang.StringBuilder append(java.lang.String)>
procedure java.lang.StringBuilder$java.lang.StringBuilder$append$2236(__this : ref, $param_0 : ref) returns (__ret : ref);



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



	 //  @line: 68
// <LinkedList: boolean contains(java.lang.Object)>
procedure boolean$LinkedList$contains$2457(__this : ref, $param_0 : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var $r241 : ref;
var r140 : ref;
var $z043 : int;
var r039 : ref;
Block51:
	r039 := __this;
	r140 := $param_0;
	 assert ($neref((r039), ($null))==1);
	 //  @line: 69
	 call $r241 := LinkedList$Node$LinkedList$find$2458((r039), (r140));
	 goto Block52;
	 //  @line: 69
Block52:
	 goto Block55, Block53;
	 //  @line: 69
Block55:
	 //  @line: 69
	 assume ($negInt(($eqref(($r241), ($null))))==1);
	 //  @line: 69
	$z043 := 1;
	 goto Block56;
	 //  @line: 69
Block53:
	 assume ($eqref(($r241), ($null))==1);
	 goto Block54;
	 //  @line: 69
Block56:
	 //  @line: 69
	__ret := $z043;
	 return;
	 //  @line: 69
Block54:
	 //  @line: 69
	$z043 := 0;
	 goto Block56;
}