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 int$lp$$rp$$Queen$queen254 : [int]int;
var int$Queen$n0 : int;
var int$Queen$nbsol0 : 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);



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


	 //  @line: 60
// <Queen: void main(java.lang.String[])>
procedure void$Queen$main$2233($param_0 : [int]ref)
  modifies $intArrSize, int$lp$$rp$$Queen$queen254, int$Queen$n0, int$Queen$nbsol0;
 {
var r044 : [int]ref;
var $i146 : int;
var $r147 : [int]int;
var $i045 : int;

 //temp local variables 
var $freshlocal0 : int;

Block79:
	r044 := $param_0;
	 //  @line: 61
	$i045 := $refArrSize[r044[$arrSizeIdx]];
	 //  @line: 61
	int$Queen$n0 := $i045;
	 //  @line: 62
	$i146 := int$Queen$n0;
	 //  @line: 62
	$r147 := $reftointarr(($newvariable((80))));
	$intArrSize[$reftointarr(($newvariable((80))))[$arrSizeIdx]] := $i146;
	 assume ($negInt(($eqintarray(($reftointarr(($newvariable((80))))), ($intArrNull))))==1);
	 //  @line: 62
	int$lp$$rp$$Queen$queen254 := $r147;
	 //  @line: 63
	int$Queen$nbsol0 := 0;
	 //  @line: 64
	 call $freshlocal0 := boolean$Queen$search$2232((0));
	 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);



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



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



// procedure is generated by joogie.
function {:inline true} $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: 27
// <Queen: boolean safeMove(int,int)>
procedure boolean$Queen$safeMove$2231($param_0 : int, $param_1 : int) returns (__ret : int) {
var i329 : int;
var z128 : int;
var $r024 : [int]int;
var $z026 : int;
var i022 : int;
var $z230 : int;
var i123 : int;
var $i225 : int;
Block49:
	i022 := $param_0;
	i123 := $param_1;
	 //  @line: 28
	z128 := 1;
	 //  @line: 30
	i329 := 0;
	 goto Block50;
	 //  @line: 30
Block50:
	 goto Block51, Block53;
	 //  @line: 30
Block51:
	 assume ($geint((i329), (i022))==1);
	 goto Block52;
	 //  @line: 30
Block53:
	 //  @line: 30
	 assume ($negInt(($geint((i329), (i022))))==1);
	 goto Block54;
	 //  @line: 33
Block52:
	 //  @line: 33
	__ret := z128;
	 return;
	 //  @line: 31
Block54:
	 goto Block55, Block57;
	 //  @line: 31
Block55:
	 assume ($eqint((z128), (0))==1);
	 goto Block56;
	 //  @line: 31
Block57:
	 //  @line: 31
	 assume ($negInt(($eqint((z128), (0))))==1);
	 //  @line: 30
	$r024 := int$lp$$rp$$Queen$queen254;
	 assert ($geint((i329), (0))==1);
	 assert ($ltint((i329), ($intArrSize[$r024[$arrSizeIdx]]))==1);
	 //  @line: 30
	$i225 := $r024[i329];
	 //  @line: 30
	 call $z026 := boolean$Queen$wrongPos$2230((i022), (i123), (i329), ($i225));
	 goto Block58;
	 //  @line: 30
Block56:
	 //  @line: 30
	$z230 := 0;
	 goto Block61;
	 //  @line: 30
Block58:
	 goto Block60, Block59;
	 //  @line: 31
Block61:
	 //  @line: 31
	z128 := $z230;
	 goto Block62;
	 //  @line: 30
Block60:
	 //  @line: 30
	 assume ($negInt(($neint(($z026), (0))))==1);
	 //  @line: 30
	$z230 := 1;
	 goto Block61;
	 //  @line: 30
Block59:
	 assume ($neint(($z026), (0))==1);
	 goto Block56;
	 //  @line: 30
Block62:
	 //  @line: 30
	i329 := $addint((i329), (1));
	 goto Block50;
}


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



	 //  @line: 12
// <Queen: void displayChessboard()>
procedure void$Queen$displayChessboard$2229() {
var i49 : int;
var $r06 : [int]int;
var i38 : int;
var $i27 : int;
var $i03 : int;
var $i15 : int;
	 //  @line: 13
Block17:
	 //  @line: 13
	i38 := 0;
	 goto Block18;
	 //  @line: 13
Block18:
	 //  @line: 13
	$i03 := int$Queen$n0;
	 goto Block19;
	 //  @line: 13
Block19:
	 goto Block20, Block22;
	 //  @line: 13
Block20:
	 assume ($geint((i38), ($i03))==1);
	 goto Block21;
	 //  @line: 13
Block22:
	 //  @line: 13
	 assume ($negInt(($geint((i38), ($i03))))==1);
	 //  @line: 14
	i49 := 0;
	 goto Block23;
	 //  @line: 20
Block21:
	 return;
	 //  @line: 14
Block23:
	 //  @line: 14
	$i15 := int$Queen$n0;
	 goto Block24;
	 //  @line: 14
Block24:
	 goto Block25, Block27;
	 //  @line: 14
Block25:
	 assume ($geint((i49), ($i15))==1);
	 goto Block26;
	 //  @line: 14
Block27:
	 //  @line: 14
	 assume ($negInt(($geint((i49), ($i15))))==1);
	 //  @line: 15
	$r06 := int$lp$$rp$$Queen$queen254;
	 assert ($geint((i38), (0))==1);
	 assert ($ltint((i38), ($intArrSize[$r06[$arrSizeIdx]]))==1);
	 //  @line: 15
	$i27 := $r06[i38];
	 goto Block28;
	 //  @line: 13
Block26:
	 //  @line: 13
	i38 := $addint((i38), (1));
	 goto Block32;
	 //  @line: 15
Block28:
	 goto Block29, Block31;
	 //  @line: 13
Block32:
	 goto Block18;
	 //  @line: 15
Block29:
	 assume ($eqint(($i27), (i49))==1);
	 goto Block30;
	 //  @line: 15
Block31:
	 //  @line: 15
	 assume ($negInt(($eqint(($i27), (i49))))==1);
	 goto Block30;
	 //  @line: 14
Block30:
	 //  @line: 14
	i49 := $addint((i49), (1));
	 goto Block23;
}


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



	 //  @line: 37
// <Queen: boolean search(int)>
procedure boolean$Queen$search$2232($param_0 : int) returns (__ret : int)
  modifies int$Queen$nbsol0;
 {
var $i440 : int;
var $r037 : [int]int;
var $i338 : int;
var i643 : int;
var z142 : int;
var $i541 : int;
var $i235 : int;
var $z036 : int;
var i032 : int;
var $i133 : int;
Block63:
	i032 := $param_0;
	 //  @line: 38
	z142 := 0;
	 //  @line: 40
	$i133 := int$Queen$n0;
	 goto Block64;
	 //  @line: 40
Block64:
	 goto Block65, Block67;
	 //  @line: 40
Block65:
	 assume ($ltint((i032), ($i133))==1);
	 goto Block66;
	 //  @line: 40
Block67:
	 //  @line: 40
	 assume ($negInt(($ltint((i032), ($i133))))==1);
	 //  @line: 41
	 call void$Queen$displayChessboard$2229();
	 //  @line: 42
	$i440 := int$Queen$nbsol0;
	 //  @line: 42
	$i541 := $addint(($i440), (1));
	 //  @line: 42
	int$Queen$nbsol0 := $i541;
	 goto Block68;
	 //  @line: 45
Block66:
	 //  @line: 45
	i643 := 0;
	 goto Block69;
	 //  @line: 56
Block68:
	 //  @line: 56
	__ret := z142;
	 return;
	 //  @line: 46
Block69:
	 goto Block71, Block70;
	 //  @line: 46
Block71:
	 //  @line: 46
	 assume ($negInt(($neint((z142), (0))))==1);
	 //  @line: 56
	$i235 := int$Queen$n0;
	 goto Block72;
	 //  @line: 46
Block70:
	 assume ($neint((z142), (0))==1);
	 goto Block68;
	 //  @line: 56
Block72:
	 goto Block74, Block73;
	 //  @line: 56
Block74:
	 //  @line: 56
	 assume ($negInt(($geint((i643), ($i235))))==1);
	 //  @line: 47
	 call $z036 := boolean$Queen$safeMove$2231((i032), (i643));
	 goto Block75;
	 //  @line: 56
Block73:
	 assume ($geint((i643), ($i235))==1);
	 goto Block68;
	 //  @line: 47
Block75:
	 goto Block76, Block78;
	 //  @line: 47
Block76:
	 assume ($eqint(($z036), (0))==1);
	 goto Block77;
	 //  @line: 47
Block78:
	 //  @line: 47
	 assume ($negInt(($eqint(($z036), (0))))==1);
	 //  @line: 48
	$r037 := int$lp$$rp$$Queen$queen254;
	 assert ($geint((i032), (0))==1);
	 assert ($ltint((i032), ($intArrSize[$r037[$arrSizeIdx]]))==1);
	 //  @line: 48
	$r037[i032] := i643;
	 //  @line: 49
	$i338 := $addint((i032), (1));
	 //  @line: 49
	 call z142 := boolean$Queen$search$2232(($i338));
	 goto Block77;
	 //  @line: 52
Block77:
	 //  @line: 52
	i643 := $addint((i643), (1));
	 goto Block69;
}


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


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


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



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



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



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



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


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



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


// 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: 22
// <Queen: boolean wrongPos(int,int,int,int)>
procedure boolean$Queen$wrongPos$2230($param_0 : int, $param_1 : int, $param_2 : int, $param_3 : int) returns (__ret : int) {
var i010 : int;
var i112 : int;
var $i515 : int;
var $z019 : int;
var i313 : int;
var $i717 : int;
var $i616 : int;
var $i414 : int;
var i211 : int;
Block33:
	i010 := $param_0;
	i112 := $param_1;
	i211 := $param_2;
	i313 := $param_3;
	 goto Block34;
	 //  @line: 23
Block34:
	 goto Block35, Block37;
	 //  @line: 23
Block35:
	 assume ($eqint((i010), (i211))==1);
	 goto Block36;
	 //  @line: 23
Block37:
	 //  @line: 23
	 assume ($negInt(($eqint((i010), (i211))))==1);
	 goto Block38;
	 //  @line: 23
Block36:
	 //  @line: 23
	$z019 := 1;
	 goto Block48;
	 //  @line: 23
Block38:
	 goto Block39, Block40;
	 //  @line: 23
Block48:
	 //  @line: 23
	__ret := $z019;
	 return;
	 //  @line: 23
Block39:
	 assume ($eqint((i112), (i313))==1);
	 goto Block36;
	 //  @line: 23
Block40:
	 //  @line: 23
	 assume ($negInt(($eqint((i112), (i313))))==1);
	 //  @line: 23
	$i515 := $subint((i010), (i211));
	 //  @line: 23
	$i414 := $subint((i112), (i313));
	 goto Block41;
	 //  @line: 23
Block41:
	 goto Block43, Block42;
	 //  @line: 23
Block43:
	 //  @line: 23
	 assume ($negInt(($eqint(($i515), ($i414))))==1);
	 //  @line: 23
	$i717 := $subint((i010), (i211));
	 //  @line: 23
	$i616 := $subint((i313), (i112));
	 goto Block44;
	 //  @line: 23
Block42:
	 assume ($eqint(($i515), ($i414))==1);
	 goto Block36;
	 //  @line: 23
Block44:
	 goto Block47, Block45;
	 //  @line: 23
Block47:
	 //  @line: 23
	 assume ($negInt(($neint(($i717), ($i616))))==1);
	 goto Block36;
	 //  @line: 23
Block45:
	 assume ($neint(($i717), ($i616))==1);
	 goto Block46;
	 //  @line: 23
Block46:
	 //  @line: 23
	$z019 := 0;
	 goto Block48;
}


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