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 Domino : classConst ;



var Domino$Liste$dom254 : Field ref;
var Liste$lp$$rp$$Partie$mains258 : Field [int]ref;
var int$lp$$rp$$Partie$TAILLEMAIN256 : [int]int;
var int$Partie$lastRandom0 : Field int;
var Liste$Partie$pioche257 : Field ref;
var Liste$Sequence$gauche259 : Field ref;
var int$Domino$gauche0 : Field int;
var int$Domino$droite0 : Field int;
var Liste$Liste$suite255 : Field ref;


	 //  @line: 286
// <Partie: int sommeValeursMain(int)>
procedure int$Partie$sommeValeursMain$2248(__this : ref, $param_0 : int) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var i2239 : int;
var i0234 : int;
var r0233 : ref;
var $r2237 : ref;
var $r1235 : [int]ref;
var $i1238 : int;
var r3240 : ref;
Block219:
	r0233 := __this;
	i0234 := $param_0;
	 //  @line: 287
	i2239 := 0;
	 assert ($neref((r0233), ($null))==1);
	 //  @line: 288
	$r1235 := $HeapVar[r0233, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i0234), (0))==1);
	 assert ($ltint((i0234), ($refArrSize[$r1235[$arrSizeIdx]]))==1);
	 //  @line: 288
	r3240 := $r1235[i0234];
	 goto Block220;
	 //  @line: 288
Block220:
	 goto Block223, Block221;
	 //  @line: 288
Block223:
	 //  @line: 288
	 assume ($negInt(($eqref((r3240), ($null))))==1);
	 assert ($neref((r3240), ($null))==1);
	 //  @line: 289
	$r2237 := $HeapVar[r3240, Domino$Liste$dom254];
	 assert ($neref((r0233), ($null))==1);
	 //  @line: 289
	 call $i1238 := int$Partie$valeurDomino$2241((r0233), ($r2237));
	 //  @line: 289
	i2239 := $addint((i2239), ($i1238));
	 assert ($neref((r3240), ($null))==1);
	 //  @line: 288
	r3240 := $HeapVar[r3240, Liste$Liste$suite255];
	 goto Block220;
	 //  @line: 288
Block221:
	 assume ($eqref((r3240), ($null))==1);
	 goto Block222;
	 //  @line: 290
Block222:
	 //  @line: 290
	__ret := i2239;
	 return;
}


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



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



	 //  @line: 85
// <Partie: void <clinit>()>
procedure void$Partie$$la$clinit$ra$$2252()
  modifies int$lp$$rp$$Partie$TAILLEMAIN256, $intArrSize;
 {
var $r0274 : [int]int;
	 //  @line: 86
Block267:
	 //  @line: 86
	$r0274 := $reftointarr(($newvariable((268))));
	$intArrSize[$reftointarr(($newvariable((268))))[$arrSizeIdx]] := 5;
	 assume ($negInt(($eqintarray(($reftointarr(($newvariable((268))))), ($intArrNull))))==1);
	 assert ($geint((0), (0))==1);
	 assert ($ltint((0), ($intArrSize[$r0274[$arrSizeIdx]]))==1);
	 //  @line: 86
	$r0274[0] := 0;
	 assert ($geint((1), (0))==1);
	 assert ($ltint((1), ($intArrSize[$r0274[$arrSizeIdx]]))==1);
	 //  @line: 86
	$r0274[1] := 0;
	 assert ($geint((2), (0))==1);
	 assert ($ltint((2), ($intArrSize[$r0274[$arrSizeIdx]]))==1);
	 //  @line: 86
	$r0274[2] := 7;
	 assert ($geint((3), (0))==1);
	 assert ($ltint((3), ($intArrSize[$r0274[$arrSizeIdx]]))==1);
	 //  @line: 86
	$r0274[3] := 6;
	 assert ($geint((4), (0))==1);
	 assert ($ltint((4), ($intArrSize[$r0274[$arrSizeIdx]]))==1);
	 //  @line: 86
	$r0274[4] := 6;
	 //  @line: 86
	int$lp$$rp$$Partie$TAILLEMAIN256 := $r0274;
	 return;
}


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



	 //  @line: 251
// <Partie: void imprimeMain(int)>
procedure void$Partie$imprimeMain$2246(__this : ref, $param_0 : int)  requires ($neref((__this), ($null))==1);
 {
var $r1198 : [int]ref;
var i0197 : int;
var $r2199 : ref;
var r0196 : ref;
Block183:
	r0196 := __this;
	i0197 := $param_0;
	 assert ($neref((r0196), ($null))==1);
	 //  @line: 252
	$r1198 := $HeapVar[r0196, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i0197), (0))==1);
	 assert ($ltint((i0197), ($refArrSize[$r1198[$arrSizeIdx]]))==1);
	 //  @line: 252
	$r2199 := $r1198[i0197];
	 //  @line: 252
	 call void$Partie$lister$2234(($r2199));
	 return;
}


// 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} $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} $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: 58
// <Sequence: int valeurGauche()>
procedure int$Sequence$valeurGauche$2255(__this : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var r0280 : ref;
var $r2282 : ref;
var $r1281 : ref;
var $i0283 : int;
Block272:
	r0280 := __this;
	 assert ($neref((r0280), ($null))==1);
	 //  @line: 59
	$r1281 := $HeapVar[r0280, Liste$Sequence$gauche259];
	 assert ($neref(($r1281), ($null))==1);
	 //  @line: 59
	$r2282 := $HeapVar[$r1281, Domino$Liste$dom254];
	 assert ($neref(($r2282), ($null))==1);
	 //  @line: 59
	$i0283 := $HeapVar[$r2282, int$Domino$gauche0];
	 //  @line: 59
	__ret := $i0283;
	 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
}


	 //  @line: 299
// <Partie: Liste mettreMeilleurDevant(Liste,Sequence)>
procedure Liste$Partie$mettreMeilleurDevant$2250(__this : ref, $param_0 : ref, $param_1 : ref) returns (__ret : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r1253 : ref;
var r2256 : ref;
var $r10268 : ref;
var r0255 : ref;
var $r8265 : ref;
var $i0267 : int;
var $r6260 : ref;
var $r5257 : ref;
var $i1269 : int;
var $r9266 : ref;
var $r7263 : ref;
var r3259 : ref;
var $r4254 : ref;
var z0262 : int;
var $z1264 : int;
Block240:
	r0255 := __this;
	r1253 := $param_0;
	r2256 := $param_1;
	 goto Block241;
	 //  @line: 300
Block241:
	 goto Block244, Block242;
	 //  @line: 300
Block244:
	 //  @line: 300
	 assume ($negInt(($eqref((r1253), ($null))))==1);
	 assert ($neref((r1253), ($null))==1);
	 //  @line: 300
	$r4254 := $HeapVar[r1253, Liste$Liste$suite255];
	 goto Block245;
	 //  @line: 300
Block242:
	 assume ($eqref((r1253), ($null))==1);
	 goto Block243;
	 //  @line: 300
Block245:
	 goto Block246, Block248;
	 //  @line: 300
Block243:
	 //  @line: 300
	__ret := r1253;
	 return;
	 //  @line: 300
Block246:
	 assume ($neref(($r4254), ($null))==1);
	 goto Block247;
	 //  @line: 300
Block248:
	 //  @line: 300
	 assume ($negInt(($neref(($r4254), ($null))))==1);
	 goto Block243;
	 //  @line: 301
Block247:
	 assert ($neref((r1253), ($null))==1);
	 //  @line: 301
	$r5257 := $HeapVar[r1253, Liste$Liste$suite255];
	 goto Block249;
	 //  @line: 301
Block249:
	 assert ($neref((r0255), ($null))==1);
	 //  @line: 301
	 call r3259 := Liste$Partie$mettreMeilleurDevant$2250((r0255), ($r5257), (r2256));
	 assert ($neref((r3259), ($null))==1);
	 //  @line: 302
	$r6260 := $HeapVar[r3259, Domino$Liste$dom254];
	 //  @line: 302
	 call z0262 := boolean$Partie$jouable$2249(($r6260), (r2256));
	 assert ($neref((r1253), ($null))==1);
	 //  @line: 303
	$r7263 := $HeapVar[r1253, Domino$Liste$dom254];
	 //  @line: 303
	 call $z1264 := boolean$Partie$jouable$2249(($r7263), (r2256));
	 goto Block250;
	 //  @line: 303
Block250:
	 goto Block251, Block253;
	 //  @line: 303
Block251:
	 assume ($eqint(($z1264), (0))==1);
	 goto Block252;
	 //  @line: 303
Block253:
	 //  @line: 303
	 assume ($negInt(($eqint(($z1264), (0))))==1);
	 goto Block254;
	 //  @line: 309
Block252:
	 assert ($neref((r3259), ($null))==1);
	 //  @line: 309
	$r8265 := $HeapVar[r3259, Liste$Liste$suite255];
	 goto Block264;
	 //  @line: 311
Block254:
	 goto Block257, Block255;
	 //  @line: 309
Block264:
	 assert ($neref((r1253), ($null))==1);
	 //  @line: 309
	$HeapVar[r1253, Liste$Liste$suite255] := $r8265;
	 assert ($neref((r3259), ($null))==1);
	 //  @line: 310
	$HeapVar[r3259, Liste$Liste$suite255] := r1253;
	 //  @line: 311
	__ret := r3259;
	 return;
	 //  @line: 311
Block257:
	 //  @line: 311
	 assume ($negInt(($eqint((z0262), (0))))==1);
	 assert ($neref((r1253), ($null))==1);
	 //  @line: 307
	$r9266 := $HeapVar[r1253, Domino$Liste$dom254];
	 assert ($neref((r0255), ($null))==1);
	 //  @line: 307
	 call $i0267 := int$Partie$valeurDomino$2241((r0255), ($r9266));
	 assert ($neref((r3259), ($null))==1);
	 //  @line: 307
	$r10268 := $HeapVar[r3259, Domino$Liste$dom254];
	 assert ($neref((r0255), ($null))==1);
	 //  @line: 307
	 call $i1269 := int$Partie$valeurDomino$2241((r0255), ($r10268));
	 goto Block258;
	 //  @line: 311
Block255:
	 assume ($eqint((z0262), (0))==1);
	 goto Block256;
	 //  @line: 307
Block258:
	 goto Block261, Block259;
	 //  @line: 311
Block256:
	 goto Block263, Block262;
	 //  @line: 307
Block261:
	 //  @line: 307
	 assume ($negInt(($gtint(($i0267), ($i1269))))==1);
	 goto Block256;
	 //  @line: 307
Block259:
	 assume ($gtint(($i0267), ($i1269))==1);
	 goto Block260;
	 //  @line: 311
Block263:
	 //  @line: 311
	 assume ($negInt(($neint((z0262), (0))))==1);
	 goto Block260;
	 //  @line: 311
Block262:
	 assume ($neint((z0262), (0))==1);
	 goto Block252;
	 //  @line: 306
Block260:
	 assert ($neref((r1253), ($null))==1);
	 //  @line: 306
	$HeapVar[r1253, Liste$Liste$suite255] := r3259;
	 //  @line: 307
	__ret := r1253;
	 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} $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);



	 //  @line: 67
// <Sequence: int valeurDroite()>
procedure int$Sequence$valeurDroite$2257(__this : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var r0288 : ref;
var $r2291 : ref;
var $i0292 : int;
var $r1290 : ref;
var r3293 : ref;
Block275:
	r0288 := __this;
	 assert ($neref((r0288), ($null))==1);
	 //  @line: 68
	r3293 := $HeapVar[r0288, Liste$Sequence$gauche259];
	 goto Block276;
	 //  @line: 69
Block276:
	 assert ($neref((r3293), ($null))==1);
	 //  @line: 69
	$r1290 := $HeapVar[r3293, Liste$Liste$suite255];
	 goto Block277;
	 //  @line: 69
Block277:
	 goto Block278, Block280;
	 //  @line: 69
Block278:
	 assume ($eqref(($r1290), ($null))==1);
	 goto Block279;
	 //  @line: 69
Block280:
	 //  @line: 69
	 assume ($negInt(($eqref(($r1290), ($null))))==1);
	 assert ($neref((r3293), ($null))==1);
	 //  @line: 70
	r3293 := $HeapVar[r3293, Liste$Liste$suite255];
	 goto Block276;
	 //  @line: 70
Block279:
	 assert ($neref((r3293), ($null))==1);
	 //  @line: 70
	$r2291 := $HeapVar[r3293, Domino$Liste$dom254];
	 goto Block281;
	 //  @line: 70
Block281:
	 assert ($neref(($r2291), ($null))==1);
	 //  @line: 70
	$i0292 := $HeapVar[$r2291, int$Domino$droite0];
	 //  @line: 70
	__ret := $i0292;
	 return;
}


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



	 //  @line: 119
// <Partie: int longueur(Liste)>
procedure int$Partie$longueur$2233($param_0 : ref) returns (__ret : int) {
var $i149 : int;
var $i048 : int;
var r045 : ref;
var $r146 : ref;
Block66:
	r045 := $param_0;
	 goto Block67;
	 //  @line: 120
Block67:
	 goto Block68, Block70;
	 //  @line: 120
Block68:
	 assume ($neref((r045), ($null))==1);
	 goto Block69;
	 //  @line: 120
Block70:
	 //  @line: 120
	 assume ($negInt(($neref((r045), ($null))))==1);
	 //  @line: 121
	__ret := 0;
	 return;
	 //  @line: 121
Block69:
	 assert ($neref((r045), ($null))==1);
	 //  @line: 121
	$r146 := $HeapVar[r045, Liste$Liste$suite255];
	 goto Block71;
	 //  @line: 121
Block71:
	 //  @line: 121
	 call $i048 := int$Partie$longueur$2233(($r146));
	 //  @line: 121
	$i149 := $addint((1), ($i048));
	 //  @line: 121
	__ret := $i149;
	 return;
}


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



	 //  @line: 25
// <Domino: void retourne()>
procedure void$Domino$retourne$2230(__this : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r018 : ref;
var $i120 : int;
var i019 : int;
Block42:
	r018 := __this;
	 assert ($neref((r018), ($null))==1);
	 //  @line: 26
	i019 := $HeapVar[r018, int$Domino$droite0];
	 assert ($neref((r018), ($null))==1);
	 //  @line: 27
	$i120 := $HeapVar[r018, int$Domino$gauche0];
	 assert ($neref((r018), ($null))==1);
	 //  @line: 27
	$HeapVar[r018, int$Domino$droite0] := $i120;
	 assert ($neref((r018), ($null))==1);
	 //  @line: 28
	$HeapVar[r018, int$Domino$gauche0] := i019;
	 return;
}


	 //  @line: 147
// <Partie: Liste supprimer(Liste,Domino)>
procedure Liste$Partie$supprimer$2237($param_0 : ref, $param_1 : ref) returns (__ret : ref) {
var $r370 : ref;
var $r471 : ref;
var $r673 : ref;
var $r774 : ref;
var r167 : ref;
var $r268 : ref;
var r066 : ref;
var $r572 : ref;
var $z069 : int;
Block96:
	r066 := $param_0;
	r167 := $param_1;
	 goto Block97;
	 //  @line: 148
Block97:
	 goto Block100, Block98;
	 //  @line: 148
Block100:
	 //  @line: 148
	 assume ($negInt(($neref((r066), ($null))))==1);
	 //  @line: 150
	__ret := $null;
	 return;
	 //  @line: 148
Block98:
	 assume ($neref((r066), ($null))==1);
	 goto Block99;
	 //  @line: 149
Block99:
	 assert ($neref((r066), ($null))==1);
	 //  @line: 149
	$r268 := $HeapVar[r066, Domino$Liste$dom254];
	 goto Block101;
	 //  @line: 149
Block101:
	 assert ($neref(($r268), ($null))==1);
	 //  @line: 149
	 call $z069 := boolean$Domino$equals$2229(($r268), (r167));
	 goto Block102;
	 //  @line: 149
Block102:
	 goto Block105, Block103;
	 //  @line: 149
Block105:
	 //  @line: 149
	 assume ($negInt(($eqint(($z069), (0))))==1);
	 assert ($neref((r066), ($null))==1);
	 //  @line: 150
	$r774 := $HeapVar[r066, Liste$Liste$suite255];
	 //  @line: 150
	__ret := $r774;
	 return;
	 //  @line: 149
Block103:
	 assume ($eqint(($z069), (0))==1);
	 goto Block104;
	 //  @line: 150
Block104:
	 //  @line: 150
	$r370 := $newvariable((106));
	 assume ($neref(($newvariable((106))), ($null))==1);
	 goto Block107;
	 //  @line: 150
Block107:
	 assert ($neref((r066), ($null))==1);
	 //  @line: 150
	$r572 := $HeapVar[r066, Domino$Liste$dom254];
	 assert ($neref((r066), ($null))==1);
	 //  @line: 150
	$r471 := $HeapVar[r066, Liste$Liste$suite255];
	 //  @line: 150
	 call $r673 := Liste$Partie$supprimer$2237(($r471), (r167));
	 assert ($neref(($r370), ($null))==1);
	 //  @line: 150
	 call void$Liste$$la$init$ra$$2231(($r370), ($r572), ($r673));
	 //  @line: 150
	__ret := $r370;
	 return;
}


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


	 //  @line: 190
// <Partie: int plusForteMain()>
procedure int$Partie$plusForteMain$2243(__this : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var i2134 : int;
var $r1130 : [int]ref;
var i3135 : int;
var i4136 : int;
var i0133 : int;
var $i1131 : int;
var r0125 : ref;
Block133:
	r0125 := __this;
	 assert ($neref((r0125), ($null))==1);
	 //  @line: 191
	 call i2134 := int$Partie$valeurMain$2242((r0125), (0));
	 //  @line: 192
	i3135 := 0;
	 //  @line: 193
	i4136 := 0;
	 goto Block134;
	 //  @line: 193
Block134:
	 assert ($neref((r0125), ($null))==1);
	 //  @line: 193
	$r1130 := $HeapVar[r0125, Liste$lp$$rp$$Partie$mains258];
	 //  @line: 193
	$i1131 := $refArrSize[$r1130[$arrSizeIdx]];
	 goto Block135;
	 //  @line: 193
Block135:
	 goto Block138, Block136;
	 //  @line: 193
Block138:
	 //  @line: 193
	 assume ($negInt(($geint((i4136), ($i1131))))==1);
	 assert ($neref((r0125), ($null))==1);
	 //  @line: 194
	 call i0133 := int$Partie$valeurMain$2242((r0125), (i4136));
	 goto Block139;
	 //  @line: 193
Block136:
	 assume ($geint((i4136), ($i1131))==1);
	 goto Block137;
	 //  @line: 195
Block139:
	 goto Block140, Block142;
	 //  @line: 200
Block137:
	 //  @line: 200
	__ret := i3135;
	 return;
	 //  @line: 195
Block140:
	 assume ($leint((i0133), (i2134))==1);
	 goto Block141;
	 //  @line: 195
Block142:
	 //  @line: 195
	 assume ($negInt(($leint((i0133), (i2134))))==1);
	 //  @line: 196
	i2134 := i0133;
	 //  @line: 197
	i3135 := i4136;
	 goto Block141;
	 //  @line: 193
Block141:
	 //  @line: 193
	i4136 := $addint((i4136), (1));
	 goto Block134;
}


	 //  @line: 256
// <Partie: void imprimeGagnants()>
procedure void$Partie$imprimeGagnants$2247(__this : ref)
  modifies $intArrSize;
  requires ($neref((__this), ($null))==1);
 {
var i14230 : int;
var $r5208 : [int]ref;
var $i7220 : int;
var i12227 : int;
var i13229 : int;
var $r4205 : [int]int;
var $i5214 : int;
var r1221 : [int]int;
var $i4213 : int;
var $r6211 : [int]ref;
var $i9224 : int;
var r9228 : [int]int;
var $r7215 : [int]ref;
var $i11226 : int;
var $r2201 : [int]ref;
var $r3202 : ref;
var $r8216 : ref;
var $i10225 : int;
var r0200 : ref;
var $i1209 : int;
var b15231 : int;
var $i8223 : int;
var $i3212 : int;
var i0218 : int;
var $i6219 : int;
var $i2210 : int;
Block184:
	r0200 := __this;
	 assert ($neref((r0200), ($null))==1);
	 //  @line: 257
	$r2201 := $HeapVar[r0200, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((0), (0))==1);
	 assert ($ltint((0), ($refArrSize[$r2201[$arrSizeIdx]]))==1);
	 //  @line: 257
	$r3202 := $r2201[0];
	 //  @line: 257
	 call i12227 := int$Partie$longueur$2233(($r3202));
	 //  @line: 258
	$r4205 := $reftointarr(($newvariable((185))));
	$intArrSize[$reftointarr(($newvariable((185))))[$arrSizeIdx]] := 1;
	 assume ($negInt(($eqintarray(($reftointarr(($newvariable((185))))), ($intArrNull))))==1);
	 assert ($geint((0), (0))==1);
	 assert ($ltint((0), ($intArrSize[$r4205[$arrSizeIdx]]))==1);
	 //  @line: 258
	$r4205[0] := 0;
	 //  @line: 258
	r9228 := $r4205;
	 //  @line: 259
	i13229 := 1;
	 goto Block186;
	 //  @line: 259
Block186:
	 assert ($neref((r0200), ($null))==1);
	 //  @line: 259
	$r5208 := $HeapVar[r0200, Liste$lp$$rp$$Partie$mains258];
	 //  @line: 259
	$i1209 := $refArrSize[$r5208[$arrSizeIdx]];
	 goto Block187;
	 //  @line: 259
Block187:
	 goto Block188, Block190;
	 //  @line: 259
Block188:
	 assume ($geint((i13229), ($i1209))==1);
	 goto Block189;
	 //  @line: 259
Block190:
	 //  @line: 259
	 assume ($negInt(($geint((i13229), ($i1209))))==1);
	 assert ($neref((r0200), ($null))==1);
	 //  @line: 260
	$r7215 := $HeapVar[r0200, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i13229), (0))==1);
	 assert ($ltint((i13229), ($refArrSize[$r7215[$arrSizeIdx]]))==1);
	 //  @line: 260
	$r8216 := $r7215[i13229];
	 //  @line: 260
	 call i0218 := int$Partie$longueur$2233(($r8216));
	 goto Block191;
	 //  @line: 273
Block189:
	 //  @line: 273
	$i2210 := $intArrSize[r9228[$arrSizeIdx]];
	 goto Block207;
	 //  @line: 261
Block191:
	 goto Block194, Block192;
	 //  @line: 273
Block207:
	 goto Block208, Block210;
	 //  @line: 261
Block194:
	 //  @line: 261
	 assume ($negInt(($geint((i0218), (i12227))))==1);
	 //  @line: 262
	i12227 := i0218;
	 //  @line: 263
	r9228 := $reftointarr(($newvariable((195))));
	$intArrSize[$reftointarr(($newvariable((195))))[$arrSizeIdx]] := 1;
	 assume ($negInt(($eqintarray(($reftointarr(($newvariable((195))))), ($intArrNull))))==1);
	 assert ($geint((0), (0))==1);
	 assert ($ltint((0), ($intArrSize[r9228[$arrSizeIdx]]))==1);
	 //  @line: 264
	r9228[0] := i13229;
	 goto Block196;
	 //  @line: 261
Block192:
	 assume ($geint((i0218), (i12227))==1);
	 goto Block193;
	 //  @line: 273
Block208:
	 assume ($neint(($i2210), (1))==1);
	 goto Block209;
	 //  @line: 273
Block210:
	 //  @line: 273
	 assume ($negInt(($neint(($i2210), (1))))==1);
	 return;
	 //  @line: 259
Block196:
	 //  @line: 259
	i13229 := $addint((i13229), (1));
	 goto Block186;
	 //  @line: 266
Block193:
	 goto Block198, Block197;
	 //  @line: 277
Block209:
	 //  @line: 277
	$i4213 := $intArrSize[r9228[$arrSizeIdx]];
	 goto Block211;
	 //  @line: 266
Block198:
	 //  @line: 266
	 assume ($negInt(($neint((i0218), (i12227))))==1);
	 goto Block199;
	 //  @line: 266
Block197:
	 assume ($neint((i0218), (i12227))==1);
	 goto Block196;
	 //  @line: 277
Block211:
	 assert ($neref((r0200), ($null))==1);
	 //  @line: 277
	$r6211 := $HeapVar[r0200, Liste$lp$$rp$$Partie$mains258];
	 //  @line: 277
	$i3212 := $refArrSize[$r6211[$arrSizeIdx]];
	 goto Block212;
	 //  @line: 267
Block199:
	 //  @line: 267
	$i6219 := $intArrSize[r9228[$arrSizeIdx]];
	 //  @line: 267
	$i7220 := $addint(($i6219), (1));
	 //  @line: 267
	r1221 := $reftointarr(($newvariable((200))));
	$intArrSize[$reftointarr(($newvariable((200))))[$arrSizeIdx]] := $i7220;
	 assume ($negInt(($eqintarray(($reftointarr(($newvariable((200))))), ($intArrNull))))==1);
	 //  @line: 268
	i14230 := 0;
	 goto Block201;
	 //  @line: 277
Block212:
	 goto Block213, Block215;
	 //  @line: 268
Block201:
	 //  @line: 268
	$i8223 := $intArrSize[r9228[$arrSizeIdx]];
	 goto Block202;
	 //  @line: 277
Block213:
	 assume ($neint(($i4213), ($i3212))==1);
	 goto Block214;
	 //  @line: 277
Block215:
	 //  @line: 277
	 assume ($negInt(($neint(($i4213), ($i3212))))==1);
	 //  @line: 279
	b15231 := 0;
	 //  @line: 279
	$i5214 := $intArrSize[r9228[$arrSizeIdx]];
	 goto Block216;
	 //  @line: 268
Block202:
	 goto Block205, Block203;
	 //  @line: 283
Block214:
	 return;
	 //  @line: 279
Block216:
	 goto Block217, Block218;
	 //  @line: 268
Block205:
	 //  @line: 268
	 assume ($negInt(($geint((i14230), ($i8223))))==1);
	 assert ($geint((i14230), (0))==1);
	 assert ($ltint((i14230), ($intArrSize[r9228[$arrSizeIdx]]))==1);
	 //  @line: 259
	$i11226 := r9228[i14230];
	 assert ($geint((i14230), (0))==1);
	 assert ($ltint((i14230), ($intArrSize[r1221[$arrSizeIdx]]))==1);
	 //  @line: 259
	r1221[i14230] := $i11226;
	 //  @line: 259
	i14230 := $addint((i14230), (1));
	 goto Block201;
	 //  @line: 268
Block203:
	 assume ($geint((i14230), ($i8223))==1);
	 goto Block204;
	 //  @line: 279
Block217:
	 assume ($geint((b15231), ($i5214))==1);
	 goto Block214;
	 //  @line: 279
Block218:
	 //  @line: 279
	 assume ($negInt(($geint((b15231), ($i5214))))==1);
	 return;
	 //  @line: 269
Block204:
	 //  @line: 269
	r9228 := r1221;
	 goto Block206;
	 //  @line: 270
Block206:
	 //  @line: 270
	$i9224 := $intArrSize[r1221[$arrSizeIdx]];
	 //  @line: 270
	$i10225 := $subint(($i9224), (1));
	 assert ($geint(($i10225), (0))==1);
	 assert ($ltint(($i10225), ($intArrSize[r9228[$arrSizeIdx]]))==1);
	 //  @line: 270
	r9228[$i10225] := i13229;
	 goto Block196;
}


	 //  @line: 3
// <Domino: void <init>(int,int)>
procedure void$Domino$$la$init$ra$$2228(__this : ref, $param_0 : int, $param_1 : int)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r01 : ref;
var i02 : int;
var i13 : int;
Block16:
	r01 := __this;
	i02 := $param_0;
	i13 := $param_1;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 4
	 call void$java.lang.Object$$la$init$ra$$28((r01));
	 assert ($neref((r01), ($null))==1);
	 //  @line: 5
	$HeapVar[r01, int$Domino$gauche0] := i02;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 6
	$HeapVar[r01, int$Domino$droite0] := i13;
	 return;
}


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



	 //  @line: 90
// <Partie: void <init>(int)>
procedure void$Partie$$la$init$ra$$2232(__this : ref, $param_0 : int)
  modifies $HeapVar, $refArrSize;
  requires ($neref((__this), ($null))==1);
 {
var $r538 : [int]int;
var i440 : int;
var i541 : int;
var $r226 : [int]ref;
var $r436 : ref;
var r130 : ref;
var $i131 : int;
var $r335 : [int]ref;
var i642 : int;
var $i237 : int;
var i025 : int;
var r024 : ref;
var $z034 : int;
var $i339 : int;
var i844 : int;
Block44:
	r024 := __this;
	i025 := $param_0;
	 assert ($neref((r024), ($null))==1);
	 //  @line: 91
	 call void$java.lang.Object$$la$init$ra$$28((r024));
	 assert ($neref((r024), ($null))==1);
	 //  @line: 153
	$HeapVar[r024, int$Partie$lastRandom0] := 0;
	 //  @line: 92
	$r226 := $reftorefarr(($newvariable((45))));
	$refArrSize[$reftorefarr(($newvariable((45))))[$arrSizeIdx]] := i025;
	 assume ($negInt(($eqrefarray(($reftorefarr(($newvariable((45))))), ($refArrNull))))==1);
	 assert ($neref((r024), ($null))==1);
	 //  @line: 92
	$HeapVar[r024, Liste$lp$$rp$$Partie$mains258] := $r226;
	 assert ($neref((r024), ($null))==1);
	 //  @line: 93
	 call void$Partie$creerPioche$2235((r024));
	 //  @line: 94
	i440 := 0;
	 goto Block46;
	 //  @line: 94
Block46:
	 goto Block47, Block49;
	 //  @line: 94
Block47:
	 assume ($geint((i440), (i025))==1);
	 goto Block48;
	 //  @line: 94
Block49:
	 //  @line: 94
	 assume ($negInt(($geint((i440), (i025))))==1);
	 //  @line: 95
	$r538 := int$lp$$rp$$Partie$TAILLEMAIN256;
	 assert ($geint((i025), (0))==1);
	 assert ($ltint((i025), ($intArrSize[$r538[$arrSizeIdx]]))==1);
	 //  @line: 95
	$i339 := $r538[i025];
	 assert ($neref((r024), ($null))==1);
	 //  @line: 95
	 call void$Partie$creerMain$2240((r024), (i440), ($i339));
	 assert ($neref((r024), ($null))==1);
	 //  @line: 96
	 call void$Partie$imprimeMain$2246((r024), (i440));
	 //  @line: 94
	i440 := $addint((i440), (1));
	 goto Block46;
	 //  @line: 98
Block48:
	 assert ($neref((r024), ($null))==1);
	 //  @line: 98
	 call i541 := int$Partie$plusForteMain$2243((r024));
	 goto Block50;
	 //  @line: 100
Block50:
	 assert ($neref((r024), ($null))==1);
	 //  @line: 100
	 call r130 := Sequence$Partie$premierCoup$2244((r024), (i541));
	 //  @line: 101
	$i131 := $addint((i541), (1));
	 //  @line: 101
	i642 := $modint(($i131), (i025));
	 //  @line: 104
	i844 := 28;
	 goto Block51;
	 //  @line: 104
Block51:
	 goto Block54, Block52;
	 //  @line: 104
Block54:
	 //  @line: 104
	 assume ($negInt(($ltint((i844), (0))))==1);
	 assert ($neref((r130), ($null))==1);
	 //  @line: 105
	 call void$Sequence$imprimer$2254((r130));
	 assert ($neref((r024), ($null))==1);
	 //  @line: 106
	 call void$Partie$imprimeMain$2246((r024), (i642));
	 assert ($neref((r024), ($null))==1);
	 //  @line: 107
	 call $z034 := boolean$Partie$jouer$2245((r024), (i642), (r130));
	 goto Block55;
	 //  @line: 104
Block52:
	 assume ($ltint((i844), (0))==1);
	 goto Block53;
	 //  @line: 107
Block55:
	 goto Block56, Block58;
	 //  @line: 115
Block53:
	 assert ($neref((r024), ($null))==1);
	 //  @line: 115
	 call void$Partie$imprimeGagnants$2247((r024));
	 goto Block65;
	 //  @line: 107
Block56:
	 assume ($eqint(($z034), (0))==1);
	 goto Block57;
	 //  @line: 107
Block58:
	 //  @line: 107
	 assume ($negInt(($eqint(($z034), (0))))==1);
	 goto Block57;
	 //  @line: 116
Block65:
	 return;
	 //  @line: 109
Block57:
	 assert ($neref((r024), ($null))==1);
	 //  @line: 109
	$r335 := $HeapVar[r024, Liste$lp$$rp$$Partie$mains258];
	 goto Block59;
	 //  @line: 109
Block59:
	 assert ($geint((i642), (0))==1);
	 assert ($ltint((i642), ($refArrSize[$r335[$arrSizeIdx]]))==1);
	 //  @line: 109
	$r436 := $r335[i642];
	 goto Block60;
	 //  @line: 109
Block60:
	 goto Block61, Block63;
	 //  @line: 109
Block61:
	 assume ($neref(($r436), ($null))==1);
	 goto Block62;
	 //  @line: 109
Block63:
	 //  @line: 109
	 assume ($negInt(($neref(($r436), ($null))))==1);
	 return;
	 //  @line: 113
Block62:
	 //  @line: 113
	$i237 := $addint((i642), (1));
	 goto Block64;
	 //  @line: 113
Block64:
	 //  @line: 113
	i642 := $modint(($i237), (i025));
	 //  @line: 104
	i844 := $addint((i844), (-1));
	 goto Block51;
}


	 //  @line: 52
// <Sequence: void imprimer()>
procedure void$Sequence$imprimer$2254(__this : ref)  requires ($neref((__this), ($null))==1);
 {
var r0278 : ref;
var $r1279 : ref;
Block271:
	r0278 := __this;
	 assert ($neref((r0278), ($null))==1);
	 //  @line: 53
	$r1279 := $HeapVar[r0278, Liste$Sequence$gauche259];
	 //  @line: 53
	 call void$Partie$lister$2234(($r1279));
	 return;
}


// 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: 141
// <Partie: Domino nieme(Liste,int)>
procedure Domino$Partie$nieme$2236($param_0 : ref, $param_1 : int) returns (__ret : ref) {
var $r365 : ref;
var $r163 : ref;
var $r264 : ref;
var r061 : ref;
var i060 : int;
var $i162 : int;
Block90:
	r061 := $param_0;
	i060 := $param_1;
	 goto Block91;
	 //  @line: 142
Block91:
	 goto Block92, Block94;
	 //  @line: 142
Block92:
	 assume ($gtint((i060), (0))==1);
	 goto Block93;
	 //  @line: 142
Block94:
	 //  @line: 142
	 assume ($negInt(($gtint((i060), (0))))==1);
	 assert ($neref((r061), ($null))==1);
	 //  @line: 143
	$r365 := $HeapVar[r061, Domino$Liste$dom254];
	 //  @line: 143
	__ret := $r365;
	 return;
	 //  @line: 143
Block93:
	 assert ($neref((r061), ($null))==1);
	 //  @line: 143
	$r163 := $HeapVar[r061, Liste$Liste$suite255];
	 goto Block95;
	 //  @line: 143
Block95:
	 //  @line: 143
	$i162 := $subint((i060), (1));
	 //  @line: 143
	 call $r264 := Domino$Partie$nieme$2236(($r163), ($i162));
	 //  @line: 143
	__ret := $r264;
	 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
}


	 //  @line: 62
// <Sequence: void ajouterAGauche(Domino)>
procedure void$Sequence$ajouterAGauche$2256(__this : ref, $param_0 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r1286 : ref;
var $r2285 : ref;
var $r3287 : ref;
var r0284 : ref;
Block273:
	r0284 := __this;
	r1286 := $param_0;
	 //  @line: 63
	$r2285 := $newvariable((274));
	 assume ($neref(($newvariable((274))), ($null))==1);
	 assert ($neref((r0284), ($null))==1);
	 //  @line: 63
	$r3287 := $HeapVar[r0284, Liste$Sequence$gauche259];
	 assert ($neref(($r2285), ($null))==1);
	 //  @line: 63
	 call void$Liste$$la$init$ra$$2231(($r2285), (r1286), ($r3287));
	 assert ($neref((r0284), ($null))==1);
	 //  @line: 63
	$HeapVar[r0284, Liste$Sequence$gauche259] := $r2285;
	 return;
}


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



	 //  @line: 36
// <Liste: void <init>(Domino,Liste)>
procedure void$Liste$$la$init$ra$$2231(__this : ref, $param_0 : ref, $param_1 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r122 : ref;
var r021 : ref;
var r223 : ref;
Block43:
	r021 := __this;
	r122 := $param_0;
	r223 := $param_1;
	 assert ($neref((r021), ($null))==1);
	 //  @line: 37
	 call void$java.lang.Object$$la$init$ra$$28((r021));
	 assert ($neref((r021), ($null))==1);
	 //  @line: 38
	$HeapVar[r021, Domino$Liste$dom254] := r122;
	 assert ($neref((r021), ($null))==1);
	 //  @line: 39
	$HeapVar[r021, Liste$Liste$suite255] := r223;
	 return;
}


	 //  @line: 314
// <Partie: void main(java.lang.String[])>
procedure void$Partie$main$2251($param_0 : [int]ref) {
var $r2270 : ref;
var $i0272 : int;
var r0271 : [int]ref;
Block265:
	r0271 := $param_0;
	 //  @line: 315
	$r2270 := $newvariable((266));
	 assume ($neref(($newvariable((266))), ($null))==1);
	 //  @line: 315
	$i0272 := $refArrSize[r0271[$arrSizeIdx]];
	 assert ($neref(($r2270), ($null))==1);
	 //  @line: 315
	 call void$Partie$$la$init$ra$$2232(($r2270), ($i0272));
	 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)
}


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


	 //  @line: 15
// <Domino: boolean equals(java.lang.Object)>
procedure boolean$Domino$equals$2229(__this : ref, $param_0 : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var $i210 : int;
var $i513 : int;
var r15 : ref;
var r04 : ref;
var $i19 : int;
var $i615 : int;
var $i311 : int;
var $i08 : int;
var $z06 : int;
var $z117 : int;
var $i716 : int;
var $i412 : int;
var r27 : ref;
Block17:
	r04 := __this;
	r15 := $param_0;
	 goto Block18;
	 //  @line: 16
Block18:
	 goto Block21, Block19;
	 //  @line: 16
Block21:
	 //  @line: 16
	 assume ($negInt(($neref((r04), (r15))))==1);
	 //  @line: 19
	__ret := 1;
	 return;
	 //  @line: 16
Block19:
	 assume ($neref((r04), (r15))==1);
	 goto Block20;
	 //  @line: 17
Block20:
	 //  @line: 17
	$z06 := $instanceof((r15), (Domino));
	 goto Block22;
	 //  @line: 17
Block22:
	 goto Block25, Block23;
	 //  @line: 17
Block25:
	 //  @line: 17
	 assume ($negInt(($eqint(($z06), (0))))==1);
	 //  @line: 18
	r27 := r15;
	 assert ($neref((r04), ($null))==1);
	 //  @line: 19
	$i19 := $HeapVar[r04, int$Domino$gauche0];
	 assert ($neref((r27), ($null))==1);
	 //  @line: 19
	$i08 := $HeapVar[r27, int$Domino$gauche0];
	 goto Block26;
	 //  @line: 17
Block23:
	 assume ($eqint(($z06), (0))==1);
	 goto Block24;
	 //  @line: 19
Block26:
	 goto Block27, Block29;
	 //  @line: 22
Block24:
	 //  @line: 22
	__ret := 0;
	 return;
	 //  @line: 19
Block27:
	 assume ($neint(($i19), ($i08))==1);
	 goto Block28;
	 //  @line: 19
Block29:
	 //  @line: 19
	 assume ($negInt(($neint(($i19), ($i08))))==1);
	 assert ($neref((r04), ($null))==1);
	 //  @line: 19
	$i716 := $HeapVar[r04, int$Domino$droite0];
	 assert ($neref((r27), ($null))==1);
	 //  @line: 19
	$i615 := $HeapVar[r27, int$Domino$droite0];
	 goto Block30;
	 //  @line: 19
Block28:
	 assert ($neref((r04), ($null))==1);
	 //  @line: 19
	$i311 := $HeapVar[r04, int$Domino$gauche0];
	 assert ($neref((r27), ($null))==1);
	 //  @line: 19
	$i210 := $HeapVar[r27, int$Domino$droite0];
	 goto Block34;
	 //  @line: 19
Block30:
	 goto Block31, Block33;
	 //  @line: 19
Block34:
	 goto Block35, Block37;
	 //  @line: 19
Block31:
	 assume ($eqint(($i716), ($i615))==1);
	 goto Block32;
	 //  @line: 19
Block33:
	 //  @line: 19
	 assume ($negInt(($eqint(($i716), ($i615))))==1);
	 goto Block28;
	 //  @line: 19
Block35:
	 assume ($neint(($i311), ($i210))==1);
	 goto Block36;
	 //  @line: 19
Block37:
	 //  @line: 19
	 assume ($negInt(($neint(($i311), ($i210))))==1);
	 assert ($neref((r04), ($null))==1);
	 //  @line: 19
	$i513 := $HeapVar[r04, int$Domino$droite0];
	 assert ($neref((r27), ($null))==1);
	 //  @line: 19
	$i412 := $HeapVar[r27, int$Domino$gauche0];
	 goto Block38;
	 //  @line: 19
Block32:
	 //  @line: 19
	$z117 := 1;
	 goto Block41;
	 //  @line: 19
Block36:
	 //  @line: 19
	$z117 := 0;
	 goto Block41;
	 //  @line: 19
Block38:
	 goto Block39, Block40;
	 //  @line: 19
Block41:
	 //  @line: 19
	__ret := $z117;
	 return;
	 //  @line: 19
Block39:
	 assume ($neint(($i513), ($i412))==1);
	 goto Block36;
	 //  @line: 19
Block40:
	 //  @line: 19
	 assume ($negInt(($neint(($i513), ($i412))))==1);
	 goto Block32;
}


// 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: 160
// <Partie: Domino piocher()>
procedure Domino$Partie$piocher$2239(__this : ref) returns (__ret : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var $r589 : ref;
var r080 : ref;
var $r384 : ref;
var r187 : ref;
var $i185 : int;
var $r281 : ref;
var $r488 : ref;
var i083 : int;
Block109:
	r080 := __this;
	 assert ($neref((r080), ($null))==1);
	 //  @line: 161
	$r281 := $HeapVar[r080, Liste$Partie$pioche257];
	 //  @line: 161
	 call i083 := int$Partie$longueur$2233(($r281));
	 assert ($neref((r080), ($null))==1);
	 //  @line: 162
	$r384 := $HeapVar[r080, Liste$Partie$pioche257];
	 assert ($neref((r080), ($null))==1);
	 //  @line: 162
	 call $i185 := int$Partie$entierAuHasard$2238((r080), (i083));
	 //  @line: 162
	 call r187 := Domino$Partie$nieme$2236(($r384), ($i185));
	 assert ($neref((r080), ($null))==1);
	 //  @line: 163
	$r488 := $HeapVar[r080, Liste$Partie$pioche257];
	 //  @line: 163
	 call $r589 := Liste$Partie$supprimer$2237(($r488), (r187));
	 assert ($neref((r080), ($null))==1);
	 //  @line: 163
	$HeapVar[r080, Liste$Partie$pioche257] := $r589;
	 //  @line: 164
	__ret := r187;
	 return;
}


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



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



	 //  @line: 293
// <Partie: boolean jouable(Domino,Sequence)>
procedure boolean$Partie$jouable$2249($param_0 : ref, $param_1 : ref) returns (__ret : int) {
var $i2247 : int;
var $i3248 : int;
var $z0252 : int;
var i0243 : int;
var r0246 : ref;
var $i5250 : int;
var r1241 : ref;
var i1245 : int;
var $i4249 : int;
Block224:
	r0246 := $param_0;
	r1241 := $param_1;
	 assert ($neref((r1241), ($null))==1);
	 //  @line: 294
	 call i0243 := int$Sequence$valeurGauche$2255((r1241));
	 assert ($neref((r1241), ($null))==1);
	 //  @line: 295
	 call i1245 := int$Sequence$valeurDroite$2257((r1241));
	 assert ($neref((r0246), ($null))==1);
	 //  @line: 296
	$i2247 := $HeapVar[r0246, int$Domino$gauche0];
	 goto Block225;
	 //  @line: 296
Block225:
	 goto Block228, Block226;
	 //  @line: 296
Block228:
	 //  @line: 296
	 assume ($negInt(($eqint(($i2247), (i0243))))==1);
	 assert ($neref((r0246), ($null))==1);
	 //  @line: 296
	$i3248 := $HeapVar[r0246, int$Domino$droite0];
	 goto Block229;
	 //  @line: 296
Block226:
	 assume ($eqint(($i2247), (i0243))==1);
	 goto Block227;
	 //  @line: 296
Block229:
	 goto Block230, Block231;
	 //  @line: 296
Block227:
	 //  @line: 296
	$z0252 := 1;
	 goto Block239;
	 //  @line: 296
Block230:
	 assume ($eqint(($i3248), (i0243))==1);
	 goto Block227;
	 //  @line: 296
Block231:
	 //  @line: 296
	 assume ($negInt(($eqint(($i3248), (i0243))))==1);
	 assert ($neref((r0246), ($null))==1);
	 //  @line: 296
	$i4249 := $HeapVar[r0246, int$Domino$gauche0];
	 goto Block232;
	 //  @line: 296
Block239:
	 //  @line: 296
	__ret := $z0252;
	 return;
	 //  @line: 296
Block232:
	 goto Block233, Block234;
	 //  @line: 296
Block233:
	 assume ($eqint(($i4249), (i1245))==1);
	 goto Block227;
	 //  @line: 296
Block234:
	 //  @line: 296
	 assume ($negInt(($eqint(($i4249), (i1245))))==1);
	 assert ($neref((r0246), ($null))==1);
	 //  @line: 296
	$i5250 := $HeapVar[r0246, int$Domino$droite0];
	 goto Block235;
	 //  @line: 296
Block235:
	 goto Block238, Block236;
	 //  @line: 296
Block238:
	 //  @line: 296
	 assume ($negInt(($neint(($i5250), (i1245))))==1);
	 goto Block227;
	 //  @line: 296
Block236:
	 assume ($neint(($i5250), (i1245))==1);
	 goto Block237;
	 //  @line: 296
Block237:
	 //  @line: 296
	$z0252 := 0;
	 goto Block239;
}


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



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



	 //  @line: 168
// <Partie: void creerMain(int,int)>
procedure void$Partie$creerMain$2240(__this : ref, $param_0 : int, $param_1 : int)  requires ($neref((__this), ($null))==1);
 {
var $r396 : [int]ref;
var i2100 : int;
var $r497 : ref;
var $r699 : ref;
var $r295 : ref;
var $r192 : [int]ref;
var i091 : int;
var i194 : int;
var r090 : ref;
var $r598 : [int]ref;
Block110:
	r090 := __this;
	i091 := $param_0;
	i194 := $param_1;
	 assert ($neref((r090), ($null))==1);
	 //  @line: 169
	$r192 := $HeapVar[r090, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i091), (0))==1);
	 assert ($ltint((i091), ($refArrSize[$r192[$arrSizeIdx]]))==1);
	 //  @line: 169
	$r192[i091] := $null;
	 //  @line: 170
	i2100 := 0;
	 goto Block111;
	 //  @line: 170
Block111:
	 goto Block112, Block114;
	 //  @line: 170
Block112:
	 assume ($geint((i2100), (i194))==1);
	 goto Block113;
	 //  @line: 170
Block114:
	 //  @line: 170
	 assume ($negInt(($geint((i2100), (i194))))==1);
	 assert ($neref((r090), ($null))==1);
	 //  @line: 171
	$r396 := $HeapVar[r090, Liste$lp$$rp$$Partie$mains258];
	 //  @line: 171
	$r295 := $newvariable((115));
	 assume ($neref(($newvariable((115))), ($null))==1);
	 assert ($neref((r090), ($null))==1);
	 //  @line: 171
	 call $r497 := Domino$Partie$piocher$2239((r090));
	 assert ($neref((r090), ($null))==1);
	 //  @line: 171
	$r598 := $HeapVar[r090, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i091), (0))==1);
	 assert ($ltint((i091), ($refArrSize[$r598[$arrSizeIdx]]))==1);
	 //  @line: 171
	$r699 := $r598[i091];
	 assert ($neref(($r295), ($null))==1);
	 //  @line: 171
	 call void$Liste$$la$init$ra$$2231(($r295), ($r497), ($r699));
	 assert ($geint((i091), (0))==1);
	 assert ($ltint((i091), ($refArrSize[$r396[$arrSizeIdx]]))==1);
	 //  @line: 171
	$r396[i091] := $r295;
	 //  @line: 170
	i2100 := $addint((i2100), (1));
	 goto Block111;
	 //  @line: 173
Block113:
	 return;
}


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


	 //  @line: 125
// <Partie: void lister(Liste)>
procedure void$Partie$lister$2234($param_0 : ref) {
var $r151 : ref;
var r050 : ref;
Block72:
	r050 := $param_0;
	 goto Block73;
	 //  @line: 126
Block73:
	 goto Block76, Block74;
	 //  @line: 126
Block76:
	 //  @line: 126
	 assume ($negInt(($neref((r050), ($null))))==1);
	 return;
	 //  @line: 126
Block74:
	 assume ($neref((r050), ($null))==1);
	 goto Block75;
	 //  @line: 128
Block75:
	 assert ($neref((r050), ($null))==1);
	 //  @line: 128
	$r151 := $HeapVar[r050, Liste$Liste$suite255];
	 goto Block77;
	 //  @line: 128
Block77:
	 //  @line: 128
	 call void$Partie$lister$2234(($r151));
	 return;
}


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



	 //  @line: 155
// <Partie: int entierAuHasard(int)>
procedure int$Partie$entierAuHasard$2238(__this : ref, $param_0 : int) returns (__ret : int)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var i077 : int;
var $i278 : int;
var $i176 : int;
var r075 : ref;
var $i379 : int;
Block108:
	r075 := __this;
	i077 := $param_0;
	 assert ($neref((r075), ($null))==1);
	 //  @line: 156
	$i176 := $HeapVar[r075, int$Partie$lastRandom0];
	 //  @line: 156
	$i278 := $addint(($i176), (100));
	 //  @line: 156
	$i379 := $modint(($i278), (i077));
	 assert ($neref((r075), ($null))==1);
	 //  @line: 156
	$HeapVar[r075, int$Partie$lastRandom0] := $i379;
	 //  @line: 156
	__ret := $i379;
	 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
}


	 //  @line: 181
// <Partie: int valeurMain(int)>
procedure int$Partie$valeurMain$2242(__this : ref, $param_0 : int) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var $r2118 : ref;
var $i3124 : int;
var i0115 : int;
var r0114 : ref;
var $r1116 : [int]ref;
var r3123 : ref;
var i2122 : int;
var i1120 : int;
Block122:
	r0114 := __this;
	i0115 := $param_0;
	 //  @line: 182
	i2122 := 0;
	 assert ($neref((r0114), ($null))==1);
	 //  @line: 183
	$r1116 := $HeapVar[r0114, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i0115), (0))==1);
	 assert ($ltint((i0115), ($refArrSize[$r1116[$arrSizeIdx]]))==1);
	 //  @line: 183
	r3123 := $r1116[i0115];
	 goto Block123;
	 //  @line: 183
Block123:
	 goto Block126, Block124;
	 //  @line: 183
Block126:
	 //  @line: 183
	 assume ($negInt(($eqref((r3123), ($null))))==1);
	 assert ($neref((r3123), ($null))==1);
	 //  @line: 184
	$r2118 := $HeapVar[r3123, Domino$Liste$dom254];
	 assert ($neref((r0114), ($null))==1);
	 //  @line: 184
	 call i1120 := int$Partie$valeurDomino$2241((r0114), ($r2118));
	 goto Block127;
	 //  @line: 183
Block124:
	 assume ($eqref((r3123), ($null))==1);
	 goto Block125;
	 //  @line: 185
Block127:
	 goto Block128, Block130;
	 //  @line: 187
Block125:
	 //  @line: 187
	__ret := i2122;
	 return;
	 //  @line: 185
Block128:
	 assume ($leint((i1120), (i2122))==1);
	 goto Block129;
	 //  @line: 185
Block130:
	 //  @line: 185
	 assume ($negInt(($leint((i1120), (i2122))))==1);
	 //  @line: 183
	$i3124 := i1120;
	 goto Block131;
	 //  @line: 183
Block129:
	 //  @line: 183
	$i3124 := i2122;
	 goto Block131;
	 //  @line: 185
Block131:
	 //  @line: 185
	i2122 := $i3124;
	 goto Block132;
	 //  @line: 183
Block132:
	 assert ($neref((r3123), ($null))==1);
	 //  @line: 183
	r3123 := $HeapVar[r3123, Liste$Liste$suite255];
	 goto Block123;
}


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



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



	 //  @line: 73
// <Sequence: void ajouterADroite(Domino)>
procedure void$Sequence$ajouterADroite$2258(__this : ref, $param_0 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r6301 : ref;
var r0294 : ref;
var $r3297 : ref;
var $r2295 : ref;
var $r5300 : ref;
var $r4298 : ref;
var r1299 : ref;
Block282:
	r0294 := __this;
	r1299 := $param_0;
	 assert ($neref((r0294), ($null))==1);
	 //  @line: 74
	$r2295 := $HeapVar[r0294, Liste$Sequence$gauche259];
	 goto Block283;
	 //  @line: 74
Block283:
	 goto Block286, Block284;
	 //  @line: 74
Block286:
	 //  @line: 74
	 assume ($negInt(($neref(($r2295), ($null))))==1);
	 //  @line: 75
	$r5300 := $newvariable((287));
	 assume ($neref(($newvariable((287))), ($null))==1);
	 assert ($neref(($r5300), ($null))==1);
	 //  @line: 75
	 call void$Liste$$la$init$ra$$2231(($r5300), (r1299), ($null));
	 assert ($neref((r0294), ($null))==1);
	 //  @line: 75
	$HeapVar[r0294, Liste$Sequence$gauche259] := $r5300;
	 return;
	 //  @line: 74
Block284:
	 assume ($neref(($r2295), ($null))==1);
	 goto Block285;
	 //  @line: 78
Block285:
	 assert ($neref((r0294), ($null))==1);
	 //  @line: 78
	r6301 := $HeapVar[r0294, Liste$Sequence$gauche259];
	 goto Block288;
	 //  @line: 79
Block288:
	 assert ($neref((r6301), ($null))==1);
	 //  @line: 79
	$r3297 := $HeapVar[r6301, Liste$Liste$suite255];
	 goto Block289;
	 //  @line: 79
Block289:
	 goto Block292, Block290;
	 //  @line: 79
Block292:
	 //  @line: 79
	 assume ($negInt(($eqref(($r3297), ($null))))==1);
	 assert ($neref((r6301), ($null))==1);
	 //  @line: 81
	r6301 := $HeapVar[r6301, Liste$Liste$suite255];
	 goto Block288;
	 //  @line: 79
Block290:
	 assume ($eqref(($r3297), ($null))==1);
	 goto Block291;
	 //  @line: 80
Block291:
	 //  @line: 80
	$r4298 := $newvariable((293));
	 assume ($neref(($newvariable((293))), ($null))==1);
	 goto Block294;
	 //  @line: 80
Block294:
	 assert ($neref(($r4298), ($null))==1);
	 //  @line: 80
	 call void$Liste$$la$init$ra$$2231(($r4298), (r1299), ($null));
	 assert ($neref((r6301), ($null))==1);
	 //  @line: 80
	$HeapVar[r6301, Liste$Liste$suite255] := $r4298;
	 return;
}


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



// procedure is generated by joogie.
function {:inline true} $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: 46
// <Sequence: void <init>(Domino)>
procedure void$Sequence$$la$init$ra$$2253(__this : ref, $param_0 : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r0275 : ref;
var $r2276 : ref;
var r1277 : ref;
Block269:
	r0275 := __this;
	r1277 := $param_0;
	 assert ($neref((r0275), ($null))==1);
	 //  @line: 47
	 call void$java.lang.Object$$la$init$ra$$28((r0275));
	 //  @line: 48
	$r2276 := $newvariable((270));
	 assume ($neref(($newvariable((270))), ($null))==1);
	 assert ($neref(($r2276), ($null))==1);
	 //  @line: 48
	 call void$Liste$$la$init$ra$$2231(($r2276), (r1277), ($null));
	 assert ($neref((r0275), ($null))==1);
	 //  @line: 48
	$HeapVar[r0275, Liste$Sequence$gauche259] := $r2276;
	 return;
}


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



	 //  @line: 176
// <Partie: int valeurDomino(Domino)>
procedure int$Partie$valeurDomino$2241(__this : ref, $param_0 : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var r0112 : ref;
var $i9111 : int;
var $i2104 : int;
var $i4106 : int;
var $i6108 : int;
var $i0102 : int;
var $i7109 : int;
var $i3105 : int;
var $i8110 : int;
var r1101 : ref;
var $i5107 : int;
var $i1103 : int;
Block116:
	r0112 := __this;
	r1101 := $param_0;
	 assert ($neref((r1101), ($null))==1);
	 //  @line: 177
	$i1103 := $HeapVar[r1101, int$Domino$gauche0];
	 assert ($neref((r1101), ($null))==1);
	 //  @line: 177
	$i0102 := $HeapVar[r1101, int$Domino$droite0];
	 goto Block117;
	 //  @line: 177
Block117:
	 goto Block118, Block120;
	 //  @line: 177
Block118:
	 assume ($leint(($i1103), ($i0102))==1);
	 goto Block119;
	 //  @line: 177
Block120:
	 //  @line: 177
	 assume ($negInt(($leint(($i1103), ($i0102))))==1);
	 assert ($neref((r1101), ($null))==1);
	 //  @line: 178
	$i6108 := $HeapVar[r1101, int$Domino$gauche0];
	 //  @line: 178
	$i8110 := $mulint(($i6108), (10));
	 assert ($neref((r1101), ($null))==1);
	 //  @line: 178
	$i7109 := $HeapVar[r1101, int$Domino$droite0];
	 //  @line: 178
	$i9111 := $addint(($i8110), ($i7109));
	 //  @line: 178
	__ret := $i9111;
	 return;
	 //  @line: 178
Block119:
	 assert ($neref((r1101), ($null))==1);
	 //  @line: 178
	$i2104 := $HeapVar[r1101, int$Domino$droite0];
	 goto Block121;
	 //  @line: 178
Block121:
	 //  @line: 178
	$i4106 := $mulint(($i2104), (10));
	 assert ($neref((r1101), ($null))==1);
	 //  @line: 178
	$i3105 := $HeapVar[r1101, int$Domino$gauche0];
	 //  @line: 178
	$i5107 := $addint(($i4106), ($i3105));
	 //  @line: 178
	__ret := $i5107;
	 return;
}


// 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: 203
// <Partie: Sequence premierCoup(int)>
procedure Sequence$Partie$premierCoup$2244(__this : ref, $param_0 : int) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $i1143 : int;
var $r6147 : [int]ref;
var $r2139 : [int]ref;
var $i2144 : int;
var $r8149 : [int]ref;
var r1146 : ref;
var $r3140 : [int]ref;
var $r7148 : ref;
var $r10151 : ref;
var i0138 : int;
var $r5142 : ref;
var $r4141 : ref;
var r0137 : ref;
var $r9150 : ref;
Block143:
	r0137 := __this;
	i0138 := $param_0;
	 assert ($neref((r0137), ($null))==1);
	 //  @line: 204
	$r2139 := $HeapVar[r0137, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i0138), (0))==1);
	 assert ($ltint((i0138), ($refArrSize[$r2139[$arrSizeIdx]]))==1);
	 //  @line: 204
	$r5142 := $r2139[i0138];
	 assert ($neref((r0137), ($null))==1);
	 //  @line: 204
	$r3140 := $HeapVar[r0137, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i0138), (0))==1);
	 assert ($ltint((i0138), ($refArrSize[$r3140[$arrSizeIdx]]))==1);
	 //  @line: 204
	$r4141 := $r3140[i0138];
	 //  @line: 204
	 call $i1143 := int$Partie$longueur$2233(($r4141));
	 assert ($neref((r0137), ($null))==1);
	 //  @line: 204
	 call $i2144 := int$Partie$entierAuHasard$2238((r0137), ($i1143));
	 //  @line: 204
	 call r1146 := Domino$Partie$nieme$2236(($r5142), ($i2144));
	 assert ($neref((r0137), ($null))==1);
	 //  @line: 206
	$r8149 := $HeapVar[r0137, Liste$lp$$rp$$Partie$mains258];
	 assert ($neref((r0137), ($null))==1);
	 //  @line: 206
	$r6147 := $HeapVar[r0137, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i0138), (0))==1);
	 assert ($ltint((i0138), ($refArrSize[$r6147[$arrSizeIdx]]))==1);
	 //  @line: 206
	$r7148 := $r6147[i0138];
	 //  @line: 206
	 call $r9150 := Liste$Partie$supprimer$2237(($r7148), (r1146));
	 assert ($geint((i0138), (0))==1);
	 assert ($ltint((i0138), ($refArrSize[$r8149[$arrSizeIdx]]))==1);
	 //  @line: 206
	$r8149[i0138] := $r9150;
	 //  @line: 207
	$r10151 := $newvariable((144));
	 assume ($neref(($newvariable((144))), ($null))==1);
	 assert ($neref(($r10151), ($null))==1);
	 //  @line: 207
	 call void$Sequence$$la$init$ra$$2253(($r10151), (r1146));
	 //  @line: 207
	__ret := $r10151;
	 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} $andreal($param00 : realVar, $param11 : realVar) returns (__ret : int);



	 //  @line: 132
// <Partie: void creerPioche()>
procedure void$Partie$creerPioche$2235(__this : ref)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var i159 : int;
var r052 : ref;
var i058 : int;
var $r256 : ref;
var $r357 : ref;
var $r155 : ref;
Block78:
	r052 := __this;
	 assert ($neref((r052), ($null))==1);
	 //  @line: 133
	$HeapVar[r052, Liste$Partie$pioche257] := $null;
	 //  @line: 134
	i058 := 0;
	 goto Block79;
	 //  @line: 134
Block79:
	 goto Block82, Block80;
	 //  @line: 134
Block82:
	 //  @line: 134
	 assume ($negInt(($geint((i058), (7))))==1);
	 //  @line: 135
	i159 := i058;
	 goto Block83;
	 //  @line: 134
Block80:
	 assume ($geint((i058), (7))==1);
	 goto Block81;
	 //  @line: 135
Block83:
	 goto Block84, Block86;
	 //  @line: 138
Block81:
	 return;
	 //  @line: 135
Block84:
	 assume ($geint((i159), (7))==1);
	 goto Block85;
	 //  @line: 135
Block86:
	 //  @line: 135
	 assume ($negInt(($geint((i159), (7))))==1);
	 //  @line: 136
	$r155 := $newvariable((87));
	 assume ($neref(($newvariable((87))), ($null))==1);
	 //  @line: 136
	$r256 := $newvariable((88));
	 assume ($neref(($newvariable((88))), ($null))==1);
	 assert ($neref(($r256), ($null))==1);
	 //  @line: 136
	 call void$Domino$$la$init$ra$$2228(($r256), (i058), (i159));
	 assert ($neref((r052), ($null))==1);
	 //  @line: 136
	$r357 := $HeapVar[r052, Liste$Partie$pioche257];
	 assert ($neref(($r155), ($null))==1);
	 //  @line: 136
	 call void$Liste$$la$init$ra$$2231(($r155), ($r256), ($r357));
	 assert ($neref((r052), ($null))==1);
	 //  @line: 136
	$HeapVar[r052, Liste$Partie$pioche257] := $r155;
	 //  @line: 135
	i159 := $addint((i159), (1));
	 goto Block83;
	 //  @line: 134
Block85:
	 //  @line: 134
	i058 := $addint((i058), (1));
	 goto Block89;
	 //  @line: 134
Block89:
	 goto Block79;
}


	 //  @line: 212
// <Partie: boolean jouer(int,Sequence)>
procedure boolean$Partie$jouer$2245(__this : ref, $param_0 : int, $param_1 : ref) returns (__ret : int)  requires ($neref((__this), ($null))==1);
 {
var $i4179 : int;
var $r24189 : ref;
var $r7168 : [int]ref;
var $r15176 : ref;
var $r6167 : ref;
var $r4165 : [int]ref;
var r0160 : ref;
var i0153 : int;
var $r3162 : ref;
var r1155 : ref;
var $r19184 : ref;
var $r9170 : [int]ref;
var $r26192 : ref;
var r27194 : ref;
var $r22187 : ref;
var $r20185 : ref;
var $r8169 : ref;
var $r25190 : [int]ref;
var i1157 : int;
var $r13174 : [int]ref;
var $r16178 : ref;
var $r12173 : ref;
var $r23188 : [int]ref;
var $r2161 : [int]ref;
var $i5181 : int;
var $i3177 : int;
var r28195 : ref;
var $r14175 : ref;
var $r10171 : ref;
var $r21186 : ref;
var $r17180 : ref;
var i2159 : int;
var $i6183 : int;
var $r11172 : [int]ref;
var $r5166 : ref;
var $r18182 : ref;

 //temp local variables 
var $freshlocal0 : int;

Block145:
	r0160 := __this;
	i0153 := $param_0;
	r1155 := $param_1;
	 goto Block146;
	 //  @line: 213
Block146:
	 goto Block147, Block149;
	 //  @line: 213
Block147:
	 assume ($neint((i0153), (1))==1);
	 goto Block148;
	 //  @line: 213
Block149:
	 //  @line: 213
	 assume ($negInt(($neint((i0153), (1))))==1);
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 214
	$r25190 := $HeapVar[r0160, Liste$lp$$rp$$Partie$mains258];
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 214
	$r23188 := $HeapVar[r0160, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((1), (0))==1);
	 assert ($ltint((1), ($refArrSize[$r23188[$arrSizeIdx]]))==1);
	 //  @line: 214
	$r24189 := $r23188[1];
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 214
	 call $r26192 := Liste$Partie$mettreMeilleurDevant$2250((r0160), ($r24189), (r1155));
	 assert ($geint((1), (0))==1);
	 assert ($ltint((1), ($refArrSize[$r25190[$arrSizeIdx]]))==1);
	 //  @line: 214
	$r25190[1] := $r26192;
	 goto Block148;
	 //  @line: 215
Block148:
	 //  @line: 215
	r27194 := $null;
	 assert ($neref((r1155), ($null))==1);
	 //  @line: 216
	 call i1157 := int$Sequence$valeurGauche$2255((r1155));
	 assert ($neref((r1155), ($null))==1);
	 //  @line: 217
	 call i2159 := int$Sequence$valeurDroite$2257((r1155));
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 218
	$r2161 := $HeapVar[r0160, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i0153), (0))==1);
	 assert ($ltint((i0153), ($refArrSize[$r2161[$arrSizeIdx]]))==1);
	 //  @line: 218
	$r3162 := $r2161[i0153];
	 //  @line: 218
	 call $freshlocal0 := int$Partie$longueur$2233(($r3162));
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 219
	$r4165 := $HeapVar[r0160, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i0153), (0))==1);
	 assert ($ltint((i0153), ($refArrSize[$r4165[$arrSizeIdx]]))==1);
	 //  @line: 219
	r28195 := $r4165[i0153];
	 goto Block150;
	 //  @line: 219
Block150:
	 goto Block153, Block151;
	 //  @line: 219
Block153:
	 //  @line: 219
	 assume ($negInt(($eqref((r28195), ($null))))==1);
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 220
	$r15176 := $HeapVar[r28195, Domino$Liste$dom254];
	 assert ($neref(($r15176), ($null))==1);
	 //  @line: 220
	$i3177 := $HeapVar[$r15176, int$Domino$gauche0];
	 goto Block154;
	 //  @line: 219
Block151:
	 assume ($eqref((r28195), ($null))==1);
	 goto Block152;
	 //  @line: 220
Block154:
	 goto Block157, Block155;
	 //  @line: 234
Block152:
	 goto Block173, Block175;
	 //  @line: 220
Block157:
	 //  @line: 220
	 assume ($negInt(($neint(($i3177), (i1157))))==1);
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 221
	$r22187 := $HeapVar[r28195, Domino$Liste$dom254];
	 assert ($neref(($r22187), ($null))==1);
	 //  @line: 221
	 call void$Domino$retourne$2230(($r22187));
	 goto Block158;
	 //  @line: 220
Block155:
	 assume ($neint(($i3177), (i1157))==1);
	 goto Block156;
	 //  @line: 234
Block173:
	 assume ($eqref((r27194), ($null))==1);
	 goto Block174;
	 //  @line: 234
Block175:
	 //  @line: 234
	 assume ($negInt(($eqref((r27194), ($null))))==1);
	 goto Block176;
	 //  @line: 224
Block158:
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 224
	$r17180 := $HeapVar[r28195, Domino$Liste$dom254];
	 assert ($neref(($r17180), ($null))==1);
	 //  @line: 224
	$i5181 := $HeapVar[$r17180, int$Domino$droite0];
	 goto Block163;
	 //  @line: 222
Block156:
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 222
	$r16178 := $HeapVar[r28195, Domino$Liste$dom254];
	 goto Block159;
	 //  @line: 239
Block174:
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 239
	$r5166 := $HeapVar[r0160, Liste$Partie$pioche257];
	 goto Block177;
	 //  @line: 236
Block176:
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 236
	$r13174 := $HeapVar[r0160, Liste$lp$$rp$$Partie$mains258];
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 236
	$r11172 := $HeapVar[r0160, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i0153), (0))==1);
	 assert ($ltint((i0153), ($refArrSize[$r11172[$arrSizeIdx]]))==1);
	 //  @line: 236
	$r12173 := $r11172[i0153];
	 //  @line: 236
	 call $r14175 := Liste$Partie$supprimer$2237(($r12173), (r27194));
	 assert ($geint((i0153), (0))==1);
	 assert ($ltint((i0153), ($refArrSize[$r13174[$arrSizeIdx]]))==1);
	 //  @line: 236
	$r13174[i0153] := $r14175;
	 //  @line: 237
	__ret := 1;
	 return;
	 //  @line: 224
Block163:
	 goto Block166, Block164;
	 //  @line: 222
Block159:
	 assert ($neref(($r16178), ($null))==1);
	 //  @line: 222
	$i4179 := $HeapVar[$r16178, int$Domino$droite0];
	 goto Block160;
	 //  @line: 239
Block177:
	 goto Block178, Block180;
	 //  @line: 224
Block166:
	 //  @line: 224
	 assume ($negInt(($neint(($i5181), (i1157))))==1);
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 225
	$r20185 := $HeapVar[r28195, Domino$Liste$dom254];
	 assert ($neref((r1155), ($null))==1);
	 //  @line: 225
	 call void$Sequence$ajouterAGauche$2256((r1155), ($r20185));
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 226
	r27194 := $HeapVar[r28195, Domino$Liste$dom254];
	 goto Block152;
	 //  @line: 224
Block164:
	 assume ($neint(($i5181), (i1157))==1);
	 goto Block165;
	 //  @line: 222
Block160:
	 goto Block162, Block161;
	 //  @line: 239
Block178:
	 assume ($neref(($r5166), ($null))==1);
	 goto Block179;
	 //  @line: 239
Block180:
	 //  @line: 239
	 assume ($negInt(($neref(($r5166), ($null))))==1);
	 //  @line: 241
	__ret := 0;
	 return;
	 //  @line: 228
Block165:
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 228
	$r18182 := $HeapVar[r28195, Domino$Liste$dom254];
	 goto Block167;
	 //  @line: 222
Block162:
	 //  @line: 222
	 assume ($negInt(($neint(($i4179), (i2159))))==1);
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 223
	$r21186 := $HeapVar[r28195, Domino$Liste$dom254];
	 assert ($neref(($r21186), ($null))==1);
	 //  @line: 223
	 call void$Domino$retourne$2230(($r21186));
	 goto Block158;
	 //  @line: 222
Block161:
	 assume ($neint(($i4179), (i2159))==1);
	 goto Block158;
	 //  @line: 244
Block179:
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 244
	$r7168 := $HeapVar[r0160, Liste$lp$$rp$$Partie$mains258];
	 goto Block181;
	 //  @line: 228
Block167:
	 assert ($neref(($r18182), ($null))==1);
	 //  @line: 228
	$i6183 := $HeapVar[$r18182, int$Domino$gauche0];
	 goto Block168;
	 //  @line: 244
Block181:
	 //  @line: 244
	$r6167 := $newvariable((182));
	 assume ($neref(($newvariable((182))), ($null))==1);
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 244
	 call $r8169 := Domino$Partie$piocher$2239((r0160));
	 assert ($neref((r0160), ($null))==1);
	 //  @line: 244
	$r9170 := $HeapVar[r0160, Liste$lp$$rp$$Partie$mains258];
	 assert ($geint((i0153), (0))==1);
	 assert ($ltint((i0153), ($refArrSize[$r9170[$arrSizeIdx]]))==1);
	 //  @line: 244
	$r10171 := $r9170[i0153];
	 assert ($neref(($r6167), ($null))==1);
	 //  @line: 244
	 call void$Liste$$la$init$ra$$2231(($r6167), ($r8169), ($r10171));
	 assert ($geint((i0153), (0))==1);
	 assert ($ltint((i0153), ($refArrSize[$r7168[$arrSizeIdx]]))==1);
	 //  @line: 244
	$r7168[i0153] := $r6167;
	 //  @line: 246
	__ret := 1;
	 return;
	 //  @line: 228
Block168:
	 goto Block169, Block171;
	 //  @line: 228
Block169:
	 assume ($neint(($i6183), (i2159))==1);
	 goto Block170;
	 //  @line: 228
Block171:
	 //  @line: 228
	 assume ($negInt(($neint(($i6183), (i2159))))==1);
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 229
	$r19184 := $HeapVar[r28195, Domino$Liste$dom254];
	 assert ($neref((r1155), ($null))==1);
	 //  @line: 229
	 call void$Sequence$ajouterADroite$2258((r1155), ($r19184));
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 230
	r27194 := $HeapVar[r28195, Domino$Liste$dom254];
	 goto Block152;
	 //  @line: 219
Block170:
	 assert ($neref((r28195), ($null))==1);
	 //  @line: 219
	r28195 := $HeapVar[r28195, Liste$Liste$suite255];
	 goto Block172;
	 //  @line: 219
Block172:
	 goto Block150;
}