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$$IntListDupRec.Random$args254 : [int]ref;
var IntListDupRec.List$IntListDupRec.List$next255 : Field ref;
var int$IntListDupRec.Random$index0 : int;
var boolean$IntListDupRec.List$dupped0 : 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);



	 //  @line: 4
// <IntListDupRec.IntListDupRec: void main(java.lang.String[])>
procedure void$IntListDupRec.IntListDupRec$main$2229($param_0 : [int]ref)
  modifies java.lang.String$lp$$rp$$IntListDupRec.Random$args254, $stringSize;
 {
var $i03 : int;
var r15 : ref;
var r02 : [int]ref;
Block17:
	r02 := $param_0;
	 //  @line: 5
	java.lang.String$lp$$rp$$IntListDupRec.Random$args254 := r02;
	 //  @line: 6
	 call $i03 := int$IntListDupRec.Random$random$2231();
	 //  @line: 6
	 call r15 := IntListDupRec.List$IntListDupRec.List$createList$2235(($i03));
	 assert ($neref((r15), ($null))==1);
	 //  @line: 8
	 call void$IntListDupRec.List$dupList$2234((r15));
	 return;
}


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



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



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


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



// 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: 45
// <IntListDupRec.Random: int random()>
procedure int$IntListDupRec.Random$random$2231() returns (__ret : int)
  modifies $stringSize, int$IntListDupRec.Random$index0;
 {
var r09 : ref;
var $r18 : [int]ref;
var $i110 : int;
var $i211 : int;
var $i312 : int;
var $i07 : int;
	 //  @line: 46
Block19:
	 //  @line: 46
	$r18 := java.lang.String$lp$$rp$$IntListDupRec.Random$args254;
	 //  @line: 46
	$i07 := int$IntListDupRec.Random$index0;
	 assert ($geint(($i07), (0))==1);
	 assert ($ltint(($i07), ($refArrSize[$r18[$arrSizeIdx]]))==1);
	 //  @line: 46
	r09 := $r18[$i07];
	 //  @line: 47
	$i110 := int$IntListDupRec.Random$index0;
	 //  @line: 47
	$i211 := $addint(($i110), (1));
	 //  @line: 47
	int$IntListDupRec.Random$index0 := $i211;
	$i312 := $stringSize[r09];
	 //  @line: 48
	__ret := $i312;
	 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);



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



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



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



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


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



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



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


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



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



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



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



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


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



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



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


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


	 //  @line: 40
// <IntListDupRec.Random: void <init>()>
procedure void$IntListDupRec.Random$$la$init$ra$$2230(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r06 : ref;
Block18:
	r06 := __this;
	 assert ($neref((r06), ($null))==1);
	 //  @line: 41
	 call void$java.lang.Object$$la$init$ra$$28((r06));
	 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
}


// 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: 42
// <IntListDupRec.Random: void <clinit>()>
procedure void$IntListDupRec.Random$$la$clinit$ra$$2232()
  modifies int$IntListDupRec.Random$index0;
 {
	 //  @line: 43
Block20:
	 //  @line: 43
	int$IntListDupRec.Random$index0 := 0;
	 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);



// 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: 15
// <IntListDupRec.List: void <init>(boolean,IntListDupRec.List)>
procedure void$IntListDupRec.List$$la$init$ra$$2233(__this : ref, $param_0 : int, $param_1 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var z014 : int;
var r013 : ref;
var r115 : ref;
Block21:
	r013 := __this;
	z014 := $param_0;
	r115 := $param_1;
	 assert ($neref((r013), ($null))==1);
	 //  @line: 16
	 call void$java.lang.Object$$la$init$ra$$28((r013));
	 assert ($neref((r013), ($null))==1);
	 //  @line: 17
	$HeapVar[r013, boolean$IntListDupRec.List$dupped0] := z014;
	 assert ($neref((r013), ($null))==1);
	 //  @line: 18
	$HeapVar[r013, IntListDupRec.List$IntListDupRec.List$next255] := r115;
	 return;
}


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



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



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



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



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



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


	 //  @line: 32
// <IntListDupRec.List: IntListDupRec.List createList(int)>
procedure IntListDupRec.List$IntListDupRec.List$createList$2235($param_0 : int) returns (__ret : ref) {
var $i125 : int;
var i023 : int;
var $r024 : ref;
var $r127 : ref;
Block33:
	i023 := $param_0;
	 goto Block34;
	 //  @line: 33
Block34:
	 goto Block35, Block37;
	 //  @line: 33
Block35:
	 assume ($geint((i023), (0))==1);
	 goto Block36;
	 //  @line: 33
Block37:
	 //  @line: 33
	 assume ($negInt(($geint((i023), (0))))==1);
	 //  @line: 34
	__ret := $null;
	 return;
	 //  @line: 36
Block36:
	 //  @line: 36
	$r024 := $newvariable((38));
	 assume ($neref(($newvariable((38))), ($null))==1);
	 goto Block39;
	 //  @line: 36
Block39:
	 //  @line: 36
	$i125 := $subint((i023), (1));
	 //  @line: 36
	 call $r127 := IntListDupRec.List$IntListDupRec.List$createList$2235(($i125));
	 assert ($neref(($r024), ($null))==1);
	 //  @line: 36
	 call void$IntListDupRec.List$$la$init$ra$$2233(($r024), (0), ($r127));
	 //  @line: 36
	__ret := $r024;
	 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);



	 //  @line: 21
// <IntListDupRec.List: void dupList()>
procedure void$IntListDupRec.List$dupList$2234(__this : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var $r319 : ref;
var $r217 : ref;
var r016 : ref;
var $r522 : ref;
var $r421 : ref;
var $z018 : int;
var r120 : ref;
Block22:
	r016 := __this;
	 assert ($neref((r016), ($null))==1);
	 //  @line: 22
	$r217 := $HeapVar[r016, IntListDupRec.List$IntListDupRec.List$next255];
	 goto Block23;
	 //  @line: 22
Block23:
	 goto Block24, Block26;
	 //  @line: 22
Block24:
	 assume ($neref(($r217), ($null))==1);
	 goto Block25;
	 //  @line: 22
Block26:
	 //  @line: 22
	 assume ($negInt(($neref(($r217), ($null))))==1);
	 //  @line: 23
	$r522 := $newvariable((27));
	 assume ($neref(($newvariable((27))), ($null))==1);
	 assert ($neref(($r522), ($null))==1);
	 //  @line: 23
	 call void$IntListDupRec.List$$la$init$ra$$2233(($r522), (0), (r016));
	 goto Block28;
	 //  @line: 24
Block25:
	 assert ($neref((r016), ($null))==1);
	 //  @line: 24
	$z018 := $HeapVar[r016, boolean$IntListDupRec.List$dupped0];
	 goto Block29;
	 //  @line: 28
Block28:
	 assert ($neref((r016), ($null))==1);
	 //  @line: 28
	$r319 := $HeapVar[r016, IntListDupRec.List$IntListDupRec.List$next255];
	 assert ($neref(($r319), ($null))==1);
	 //  @line: 28
	 call void$IntListDupRec.List$dupList$2234(($r319));
	 assert ($neref((r016), ($null))==1);
	 //  @line: 29
	$HeapVar[r016, boolean$IntListDupRec.List$dupped0] := 0;
	 return;
	 //  @line: 24
Block29:
	 goto Block30, Block31;
	 //  @line: 24
Block30:
	 assume ($neint(($z018), (0))==1);
	 goto Block28;
	 //  @line: 24
Block31:
	 //  @line: 24
	 assume ($negInt(($neint(($z018), (0))))==1);
	 assert ($neref((r016), ($null))==1);
	 //  @line: 25
	r120 := $HeapVar[r016, IntListDupRec.List$IntListDupRec.List$next255];
	 //  @line: 26
	$r421 := $newvariable((32));
	 assume ($neref(($newvariable((32))), ($null))==1);
	 assert ($neref(($r421), ($null))==1);
	 //  @line: 26
	 call void$IntListDupRec.List$$la$init$ra$$2233(($r421), (1), (r120));
	 assert ($neref((r016), ($null))==1);
	 //  @line: 26
	$HeapVar[r016, IntListDupRec.List$IntListDupRec.List$next255] := $r421;
	 goto Block28;
}


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



// <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} $eqref(x : ref, y : ref) returns (__ret : int) {
if (x == y) then 1 else 0
}


	 //  @line: 2
// <IntListDupRec.IntListDupRec: void <init>()>
procedure void$IntListDupRec.IntListDupRec$$la$init$ra$$2228(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r01 : ref;
Block16:
	r01 := __this;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 3
	 call void$java.lang.Object$$la$init$ra$$28((r01));
	 return;
}


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


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



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



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