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$$DoublyLinkedList.Random$args256 : [int]ref;
var DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254 : Field ref;
var int$DoublyLinkedList.Random$index0 : int;
var int$DoublyLinkedList.DoublyLinkedList$value0 : Field int;
var DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255 : 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: 6
// <DoublyLinkedList.MainFind: void <init>()>
procedure void$DoublyLinkedList.MainFind$$la$init$ra$$2238(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r071 : ref;
Block100:
	r071 := __this;
	 assert ($neref((r071), ($null))==1);
	 //  @line: 7
	 call void$java.lang.Object$$la$init$ra$$28((r071));
	 return;
}


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



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



	 //  @line: 6
// <DoublyLinkedList.Random: int random()>
procedure int$DoublyLinkedList.Random$random$2241() returns (__ret : int)
  modifies int$DoublyLinkedList.Random$index0, $stringSize;
 {
var $r178 : [int]ref;
var r083 : ref;
var $i586 : int;
var $i180 : int;
var $i384 : int;
var $r282 : [int]ref;
var $i281 : int;
var $i485 : int;
var $i079 : int;
	 //  @line: 7
Block103:
	 //  @line: 7
	$r178 := java.lang.String$lp$$rp$$DoublyLinkedList.Random$args256;
	 //  @line: 7
	$i180 := $refArrSize[$r178[$arrSizeIdx]];
	 //  @line: 7
	$i079 := int$DoublyLinkedList.Random$index0;
	 goto Block104;
	 //  @line: 7
Block104:
	 goto Block107, Block105;
	 //  @line: 7
Block107:
	 //  @line: 7
	 assume ($negInt(($gtint(($i180), ($i079))))==1);
	 //  @line: 8
	__ret := 0;
	 return;
	 //  @line: 7
Block105:
	 assume ($gtint(($i180), ($i079))==1);
	 goto Block106;
	 //  @line: 10
Block106:
	 //  @line: 10
	$r282 := java.lang.String$lp$$rp$$DoublyLinkedList.Random$args256;
	 goto Block108;
	 //  @line: 10
Block108:
	 //  @line: 10
	$i281 := int$DoublyLinkedList.Random$index0;
	 assert ($geint(($i281), (0))==1);
	 assert ($ltint(($i281), ($refArrSize[$r282[$arrSizeIdx]]))==1);
	 //  @line: 10
	r083 := $r282[$i281];
	 //  @line: 11
	$i384 := int$DoublyLinkedList.Random$index0;
	 //  @line: 11
	$i485 := $addint(($i384), (1));
	 //  @line: 11
	int$DoublyLinkedList.Random$index0 := $i485;
	 goto Block109;
	 //  @line: 12
Block109:
	 goto Block110, Block112;
	 //  @line: 12
Block110:
	 assume ($neref((r083), ($null))==1);
	 goto Block111;
	 //  @line: 12
Block112:
	 //  @line: 12
	 assume ($negInt(($neref((r083), ($null))))==1);
	 //  @line: 13
	__ret := 0;
	 return;
	 //  @line: 15
Block111:
	$i586 := $stringSize[r083];
	 goto Block113;
	 //  @line: 15
Block113:
	 //  @line: 15
	__ret := $i586;
	 return;
}


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



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



	 //  @line: 103
// <DoublyLinkedList.DoublyLinkedList: DoublyLinkedList.DoublyLinkedList createList()>
procedure DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$createList$2237() returns (__ret : ref)
  modifies $HeapVar;
 {
var r269 : ref;
var r066 : ref;
var $r167 : ref;
var i063 : int;
var $i168 : int;
var i270 : int;
	 //  @line: 104
Block90:
	 //  @line: 104
	 call i063 := int$DoublyLinkedList.Random$random$2241();
	 //  @line: 105
	r269 := $null;
	 //  @line: 106
	i270 := 0;
	 goto Block91;
	 //  @line: 106
Block91:
	 goto Block92, Block94;
	 //  @line: 106
Block92:
	 assume ($geint((i270), (i063))==1);
	 goto Block93;
	 //  @line: 106
Block94:
	 //  @line: 106
	 assume ($negInt(($geint((i270), (i063))))==1);
	 //  @line: 107
	r066 := r269;
	 //  @line: 108
	$r167 := $newvariable((95));
	 assume ($neref(($newvariable((95))), ($null))==1);
	 //  @line: 108
	 call $i168 := int$DoublyLinkedList.Random$random$2241();
	 assert ($neref(($r167), ($null))==1);
	 //  @line: 108
	 call void$DoublyLinkedList.DoublyLinkedList$$la$init$ra$$2228(($r167), ($i168));
	 //  @line: 108
	r269 := $r167;
	 assert ($neref((r269), ($null))==1);
	 //  @line: 109
	$HeapVar[r269, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254] := r066;
	 goto Block96;
	 //  @line: 115
Block93:
	 //  @line: 115
	__ret := r269;
	 return;
	 //  @line: 110
Block96:
	 goto Block97, Block99;
	 //  @line: 110
Block97:
	 assume ($eqref((r066), ($null))==1);
	 goto Block98;
	 //  @line: 110
Block99:
	 //  @line: 110
	 assume ($negInt(($eqref((r066), ($null))))==1);
	 assert ($neref((r066), ($null))==1);
	 //  @line: 111
	$HeapVar[r066, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255] := r269;
	 goto Block98;
	 //  @line: 106
Block98:
	 //  @line: 106
	i270 := $addint((i270), (1));
	 goto Block91;
}


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


	 //  @line: 11
// <DoublyLinkedList.DoublyLinkedList: void <init>(int)>
procedure void$DoublyLinkedList.DoublyLinkedList$$la$init$ra$$2228(__this : ref, $param_0 : int)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var i02 : int;
var r01 : ref;
Block16:
	r01 := __this;
	i02 := $param_0;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 12
	 call void$java.lang.Object$$la$init$ra$$28((r01));
	 assert ($neref((r01), ($null))==1);
	 //  @line: 13
	$HeapVar[r01, int$DoublyLinkedList.DoublyLinkedList$value0] := i02;
	 return;
}


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


	 //  @line: 74
// <DoublyLinkedList.DoublyLinkedList: void delete(int)>
procedure void$DoublyLinkedList.DoublyLinkedList$delete$2234(__this : ref, $param_0 : int)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var $r648 : ref;
var $r749 : ref;
var $r446 : ref;
var i041 : int;
var $r244 : ref;
var r040 : ref;
var r143 : ref;
var $r345 : ref;
var $r547 : ref;
Block67:
	r040 := __this;
	i041 := $param_0;
	 assert ($neref((r040), ($null))==1);
	 //  @line: 75
	 call r143 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$find$2232((r040), (i041));
	 goto Block68;
	 //  @line: 76
Block68:
	 goto Block71, Block69;
	 //  @line: 76
Block71:
	 //  @line: 76
	 assume ($negInt(($eqref((r143), ($null))))==1);
	 assert ($neref((r143), ($null))==1);
	 //  @line: 77
	$r244 := $HeapVar[r143, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 goto Block72;
	 //  @line: 76
Block69:
	 assume ($eqref((r143), ($null))==1);
	 goto Block70;
	 //  @line: 77
Block72:
	 goto Block73, Block75;
	 //  @line: 84
Block70:
	 return;
	 //  @line: 77
Block73:
	 assume ($eqref(($r244), ($null))==1);
	 goto Block74;
	 //  @line: 77
Block75:
	 //  @line: 77
	 assume ($negInt(($eqref(($r244), ($null))))==1);
	 assert ($neref((r143), ($null))==1);
	 //  @line: 78
	$r749 := $HeapVar[r143, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 assert ($neref((r143), ($null))==1);
	 //  @line: 78
	$r648 := $HeapVar[r143, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 assert ($neref(($r749), ($null))==1);
	 //  @line: 78
	$HeapVar[$r749, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255] := $r648;
	 goto Block74;
	 //  @line: 80
Block74:
	 assert ($neref((r143), ($null))==1);
	 //  @line: 80
	$r345 := $HeapVar[r143, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 goto Block76;
	 //  @line: 80
Block76:
	 goto Block78, Block77;
	 //  @line: 80
Block78:
	 //  @line: 80
	 assume ($negInt(($eqref(($r345), ($null))))==1);
	 assert ($neref((r143), ($null))==1);
	 //  @line: 81
	$r547 := $HeapVar[r143, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 assert ($neref((r143), ($null))==1);
	 //  @line: 81
	$r446 := $HeapVar[r143, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 assert ($neref(($r547), ($null))==1);
	 //  @line: 81
	$HeapVar[$r547, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254] := $r446;
	 goto Block70;
	 //  @line: 80
Block77:
	 assume ($eqref(($r345), ($null))==1);
	 goto Block70;
}


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



	 //  @line: 3
// <DoublyLinkedList.Random: void <clinit>()>
procedure void$DoublyLinkedList.Random$$la$clinit$ra$$2242()
  modifies int$DoublyLinkedList.Random$index0;
 {
	 //  @line: 4
Block114:
	 //  @line: 4
	int$DoublyLinkedList.Random$index0 := 0;
	 return;
}


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



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


	 //  @line: 64
// <DoublyLinkedList.DoublyLinkedList: DoublyLinkedList.DoublyLinkedList findR(int)>
procedure DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$findR$2233(__this : ref, $param_0 : int) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $r137 : ref;
var r034 : ref;
var $i136 : int;
var i035 : int;
var $r238 : ref;
var $r339 : ref;
Block58:
	r034 := __this;
	i035 := $param_0;
	 assert ($neref((r034), ($null))==1);
	 //  @line: 65
	$i136 := $HeapVar[r034, int$DoublyLinkedList.DoublyLinkedList$value0];
	 goto Block59;
	 //  @line: 65
Block59:
	 goto Block60, Block62;
	 //  @line: 65
Block60:
	 assume ($neint(($i136), (i035))==1);
	 goto Block61;
	 //  @line: 65
Block62:
	 //  @line: 65
	 assume ($negInt(($neint(($i136), (i035))))==1);
	 //  @line: 66
	__ret := r034;
	 return;
	 //  @line: 68
Block61:
	 assert ($neref((r034), ($null))==1);
	 //  @line: 68
	$r137 := $HeapVar[r034, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 goto Block63;
	 //  @line: 68
Block63:
	 goto Block64, Block66;
	 //  @line: 68
Block64:
	 assume ($eqref(($r137), ($null))==1);
	 goto Block65;
	 //  @line: 68
Block66:
	 //  @line: 68
	 assume ($negInt(($eqref(($r137), ($null))))==1);
	 assert ($neref((r034), ($null))==1);
	 //  @line: 69
	$r238 := $HeapVar[r034, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 assert ($neref(($r238), ($null))==1);
	 //  @line: 69
	 call $r339 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$findR$2233(($r238), (i035));
	 //  @line: 69
	__ret := $r339;
	 return;
	 //  @line: 71
Block65:
	 //  @line: 71
	__ret := $null;
	 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);



	 //  @line: 51
// <DoublyLinkedList.DoublyLinkedList: DoublyLinkedList.DoublyLinkedList get(int)>
procedure DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$get$2231(__this : ref, $param_0 : int) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var i027 : int;
var r024 : ref;
var r128 : ref;
Block49:
	r024 := __this;
	i027 := $param_0;
	 assert ($neref((r024), ($null))==1);
	 //  @line: 52
	 call r128 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$getFirst$2229((r024));
	 goto Block50;
	 //  @line: 53
Block50:
	 goto Block53, Block51;
	 //  @line: 53
Block53:
	 //  @line: 53
	 assume ($negInt(($leint((i027), (0))))==1);
	 goto Block54;
	 //  @line: 53
Block51:
	 assume ($leint((i027), (0))==1);
	 goto Block52;
	 //  @line: 56
Block54:
	 goto Block55, Block56;
	 //  @line: 56
Block52:
	 //  @line: 56
	__ret := r128;
	 return;
	 //  @line: 56
Block55:
	 assume ($eqref((r128), ($null))==1);
	 goto Block52;
	 //  @line: 56
Block56:
	 //  @line: 56
	 assume ($negInt(($eqref((r128), ($null))))==1);
	 assert ($neref((r128), ($null))==1);
	 //  @line: 54
	r128 := $HeapVar[r128, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 goto Block50;
}


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



	 //  @line: 91
// <DoublyLinkedList.DoublyLinkedList: DoublyLinkedList.DoublyLinkedList copyR(DoublyLinkedList.DoublyLinkedList)>
procedure DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$copyR$2236(__this : ref, $param_0 : ref) returns (__ret : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var $r459 : ref;
var r158 : ref;
var $r560 : ref;
var $r354 : ref;
var r055 : ref;
var $i056 : int;
var r257 : ref;

 //temp local variables 
var $freshlocal0 : ref;

Block80:
	r055 := __this;
	r158 := $param_0;
	 //  @line: 92
	$r354 := $newvariable((81));
	 assume ($neref(($newvariable((81))), ($null))==1);
	 assert ($neref((r055), ($null))==1);
	 //  @line: 92
	$i056 := $HeapVar[r055, int$DoublyLinkedList.DoublyLinkedList$value0];
	 assert ($neref(($r354), ($null))==1);
	 //  @line: 92
	 call void$DoublyLinkedList.DoublyLinkedList$$la$init$ra$$2228(($r354), ($i056));
	 //  @line: 92
	r257 := $r354;
	 assert ($neref((r257), ($null))==1);
	 //  @line: 93
	$HeapVar[r257, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254] := r158;
	 goto Block82;
	 //  @line: 94
Block82:
	 goto Block85, Block83;
	 //  @line: 94
Block85:
	 //  @line: 94
	 assume ($negInt(($eqref((r158), ($null))))==1);
	 assert ($neref((r158), ($null))==1);
	 //  @line: 95
	$HeapVar[r158, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255] := r257;
	 goto Block84;
	 //  @line: 94
Block83:
	 assume ($eqref((r158), ($null))==1);
	 goto Block84;
	 //  @line: 97
Block84:
	 assert ($neref((r055), ($null))==1);
	 //  @line: 97
	$r459 := $HeapVar[r055, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 goto Block86;
	 //  @line: 97
Block86:
	 goto Block89, Block87;
	 //  @line: 97
Block89:
	 //  @line: 97
	 assume ($negInt(($eqref(($r459), ($null))))==1);
	 assert ($neref((r055), ($null))==1);
	 //  @line: 98
	$r560 := $HeapVar[r055, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 assert ($neref(($r560), ($null))==1);
	 //  @line: 98
	 call $freshlocal0 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$copyR$2236(($r560), (r257));
	 goto Block88;
	 //  @line: 97
Block87:
	 assume ($eqref(($r459), ($null))==1);
	 goto Block88;
	 //  @line: 100
Block88:
	 //  @line: 100
	__ret := r257;
	 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);



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


// 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: 8
// <DoublyLinkedList.MainFind: void main(java.lang.String[])>
procedure void$DoublyLinkedList.MainFind$main$2239($param_0 : [int]ref)
  modifies java.lang.String$lp$$rp$$DoublyLinkedList.Random$args256, $stringSize;
 {
var r072 : [int]ref;
var $i075 : int;
var r174 : ref;

 //temp local variables 
var $freshlocal0 : ref;

Block101:
	r072 := $param_0;
	 //  @line: 9
	java.lang.String$lp$$rp$$DoublyLinkedList.Random$args256 := r072;
	 //  @line: 10
	 call r174 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$createList$2237();
	 //  @line: 11
	 call $i075 := int$DoublyLinkedList.Random$random$2241();
	 assert ($neref((r174), ($null))==1);
	 //  @line: 11
	 call $freshlocal0 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$find$2232((r174), ($i075));
	 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);



	 //  @line: 23
// <DoublyLinkedList.DoublyLinkedList: void move(int)>
procedure void$DoublyLinkedList.DoublyLinkedList$move$2230(__this : ref, $param_0 : int)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var $r312 : ref;
var $i220 : int;
var $r211 : ref;
var $r413 : ref;
var $r616 : ref;
var $r717 : ref;
var r1122 : ref;
var $r818 : ref;
var $r1021 : ref;
var $r515 : ref;
var r08 : ref;
var $r19 : ref;
var r1223 : ref;
var $i114 : int;
var i07 : int;
var $r919 : ref;
Block23:
	r08 := __this;
	i07 := $param_0;
	 goto Block24;
	 //  @line: 24
Block24:
	 goto Block27, Block25;
	 //  @line: 24
Block27:
	 //  @line: 24
	 assume ($negInt(($neint((i07), (0))))==1);
	 return;
	 //  @line: 24
Block25:
	 assume ($neint((i07), (0))==1);
	 goto Block26;
	 //  @line: 27
Block26:
	 goto Block28, Block30;
	 //  @line: 27
Block28:
	 assume ($leint((i07), (0))==1);
	 goto Block29;
	 //  @line: 27
Block30:
	 //  @line: 27
	 assume ($negInt(($leint((i07), (0))))==1);
	 goto Block31;
	 //  @line: 38
Block29:
	 goto Block39, Block41;
	 //  @line: 49
Block31:
	 assert ($neref((r08), ($null))==1);
	 //  @line: 49
	$r616 := $HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 goto Block32;
	 //  @line: 38
Block39:
	 assume ($geint((i07), (0))==1);
	 goto Block40;
	 //  @line: 38
Block41:
	 //  @line: 38
	 assume ($negInt(($geint((i07), (0))))==1);
	 assert ($neref((r08), ($null))==1);
	 //  @line: 49
	$r19 := $HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 goto Block42;
	 //  @line: 49
Block32:
	 goto Block34, Block33;
	 //  @line: 49
Block40:
	 return;
	 //  @line: 49
Block42:
	 goto Block44, Block43;
	 //  @line: 49
Block34:
	 //  @line: 49
	 assume ($negInt(($eqref(($r616), ($null))))==1);
	 assert ($neref((r08), ($null))==1);
	 //  @line: 28
	r1122 := $HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 assert ($neref((r08), ($null))==1);
	 //  @line: 29
	$r717 := $HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 goto Block35;
	 //  @line: 49
Block33:
	 assume ($eqref(($r616), ($null))==1);
	 goto Block29;
	 //  @line: 49
Block44:
	 //  @line: 49
	 assume ($negInt(($eqref(($r19), ($null))))==1);
	 assert ($neref((r08), ($null))==1);
	 //  @line: 39
	r1223 := $HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 assert ($neref((r08), ($null))==1);
	 //  @line: 40
	$r211 := $HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 goto Block45;
	 //  @line: 49
Block43:
	 assume ($eqref(($r19), ($null))==1);
	 goto Block40;
	 //  @line: 29
Block35:
	 goto Block38, Block36;
	 //  @line: 40
Block45:
	 goto Block48, Block46;
	 //  @line: 29
Block38:
	 //  @line: 29
	 assume ($negInt(($eqref(($r717), ($null))))==1);
	 assert ($neref((r08), ($null))==1);
	 //  @line: 30
	$r1021 := $HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 assert ($neref(($r1021), ($null))==1);
	 //  @line: 30
	$HeapVar[$r1021, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255] := r1122;
	 goto Block37;
	 //  @line: 29
Block36:
	 assume ($eqref(($r717), ($null))==1);
	 goto Block37;
	 //  @line: 40
Block48:
	 //  @line: 40
	 assume ($negInt(($eqref(($r211), ($null))))==1);
	 assert ($neref((r08), ($null))==1);
	 //  @line: 41
	$r515 := $HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 assert ($neref(($r515), ($null))==1);
	 //  @line: 41
	$HeapVar[$r515, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254] := r1223;
	 goto Block47;
	 //  @line: 40
Block46:
	 assume ($eqref(($r211), ($null))==1);
	 goto Block47;
	 //  @line: 32
Block37:
	 assert ($neref((r08), ($null))==1);
	 //  @line: 32
	$r818 := $HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 assert ($neref((r1122), ($null))==1);
	 //  @line: 32
	$HeapVar[r1122, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254] := $r818;
	 assert ($neref((r1122), ($null))==1);
	 //  @line: 33
	$r919 := $HeapVar[r1122, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 assert ($neref((r08), ($null))==1);
	 //  @line: 33
	$HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255] := $r919;
	 assert ($neref((r1122), ($null))==1);
	 //  @line: 34
	$HeapVar[r1122, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255] := r08;
	 assert ($neref((r08), ($null))==1);
	 //  @line: 35
	$HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254] := r1122;
	 //  @line: 36
	$i220 := $subint((i07), (1));
	 assert ($neref((r08), ($null))==1);
	 //  @line: 36
	 call void$DoublyLinkedList.DoublyLinkedList$move$2230((r08), ($i220));
	 goto Block29;
	 //  @line: 43
Block47:
	 assert ($neref((r08), ($null))==1);
	 //  @line: 43
	$r312 := $HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255];
	 assert ($neref((r1223), ($null))==1);
	 //  @line: 43
	$HeapVar[r1223, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255] := $r312;
	 assert ($neref((r1223), ($null))==1);
	 //  @line: 44
	$r413 := $HeapVar[r1223, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 assert ($neref((r08), ($null))==1);
	 //  @line: 44
	$HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254] := $r413;
	 assert ($neref((r1223), ($null))==1);
	 //  @line: 45
	$HeapVar[r1223, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254] := r08;
	 assert ($neref((r08), ($null))==1);
	 //  @line: 46
	$HeapVar[r08, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$next255] := r1223;
	 //  @line: 47
	$i114 := $subint((i07), (1));
	 assert ($neref((r08), ($null))==1);
	 //  @line: 47
	 call void$DoublyLinkedList.DoublyLinkedList$move$2230((r08), ($i114));
	 goto Block40;
}


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



	 //  @line: 16
// <DoublyLinkedList.DoublyLinkedList: DoublyLinkedList.DoublyLinkedList getFirst()>
procedure DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$getFirst$2229(__this : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $r36 : ref;
var $r25 : ref;
var $r14 : ref;
var r03 : ref;
Block17:
	r03 := __this;
	 assert ($neref((r03), ($null))==1);
	 //  @line: 17
	$r14 := $HeapVar[r03, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 goto Block18;
	 //  @line: 17
Block18:
	 goto Block21, Block19;
	 //  @line: 17
Block21:
	 //  @line: 17
	 assume ($negInt(($neref(($r14), ($null))))==1);
	 //  @line: 18
	__ret := r03;
	 return;
	 //  @line: 17
Block19:
	 assume ($neref(($r14), ($null))==1);
	 goto Block20;
	 //  @line: 20
Block20:
	 assert ($neref((r03), ($null))==1);
	 //  @line: 20
	$r25 := $HeapVar[r03, DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$prev254];
	 goto Block22;
	 //  @line: 20
Block22:
	 assert ($neref(($r25), ($null))==1);
	 //  @line: 20
	 call $r36 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$getFirst$2229(($r25));
	 //  @line: 20
	__ret := $r36;
	 return;
}


// 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: 86
// <DoublyLinkedList.DoublyLinkedList: DoublyLinkedList.DoublyLinkedList copy()>
procedure DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$copy$2235(__this : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var r152 : ref;
var $r253 : ref;
var r050 : ref;
Block79:
	r050 := __this;
	 assert ($neref((r050), ($null))==1);
	 //  @line: 87
	 call r152 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$getFirst$2229((r050));
	 assert ($neref((r152), ($null))==1);
	 //  @line: 88
	 call $r253 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$copyR$2236((r152), ($null));
	 //  @line: 88
	__ret := $r253;
	 return;
}


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



	 //  @line: 59
// <DoublyLinkedList.DoublyLinkedList: DoublyLinkedList.DoublyLinkedList find(int)>
procedure DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$find$2232(__this : ref, $param_0 : int) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $r233 : ref;
var r131 : ref;
var i032 : int;
var r029 : ref;
Block57:
	r029 := __this;
	i032 := $param_0;
	 assert ($neref((r029), ($null))==1);
	 //  @line: 60
	 call r131 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$getFirst$2229((r029));
	 assert ($neref((r131), ($null))==1);
	 //  @line: 61
	 call $r233 := DoublyLinkedList.DoublyLinkedList$DoublyLinkedList.DoublyLinkedList$findR$2233((r131), (i032));
	 //  @line: 61
	__ret := $r233;
	 return;
}


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