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 $fresh13 : int;
var $fresh29 : int;
var $fresh6 : [int][int]realVar;
var $fresh6 : int;
var $fresh8 : int;
var $fresh11 : int;
var $fresh30 : int;
var $fresh2 : int;
var $fresh37 : int;
var $fresh45 : int;
var $fresh28 : int;
var $fresh24 : int;
var $fresh27 : int;
var $fresh1 : [int][int]realVar;
var $fresh7 : int;
var $fresh16 : int;
var $fresh1 : [int]realVar;
var $fresh5 : int;
var $fresh9 : int;
var $fresh15 : int;
var $fresh4 : [int][int]realVar;
var $fresh19 : int;
var $fresh2 : int;
var $fresh34 : int;
var $fresh43 : [int]realVar;
var $fresh41 : int;
var $fresh25 : int;
var $fresh4 : [int]realVar;
var $fresh14 : int;
var $fresh7 : int;
var $fresh22 : int;
var $fresh40 : [int]realVar;
var $fresh39 : int;
var $fresh12 : int;
var $fresh21 : int;
var $fresh3 : realVar;
var $fresh33 : int;
var $fresh18 : int;
var $fresh5 : int;
var $fresh9 : int;
var $fresh44 : int;
var $fresh35 : int;
var $fresh23 : int;
var $fresh3 : int;
var $fresh17 : int;
var $fresh38 : int;
var $fresh26 : int;
var $fresh8 : [int][int]realVar;
var $fresh32 : int;
var double$lp$$rp$$lp$$rp$$Matrix$values254 : Field [int][int]realVar;
var $fresh31 : int;
var $fresh20 : int;
var $fresh36 : int;
var $fresh42 : int;
var $fresh10 : 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);



	 //  @line: 59
// <Matrix: Matrix transpose()>
procedure Matrix$Matrix$transpose$2232(__this : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $i191 : int;
var r085 : ref;
var $r593 : [int][int]realVar;
var i3104 : int;
var $r897 : [int]realVar;
var $r284 : ref;
var $r386 : [int][int]realVar;
var $r795 : [int]realVar;
var $d096 : realVar;
var $i087 : int;
var i2103 : int;
var r188 : ref;
var $r998 : [int][int]realVar;
var $r1099 : [int][int]realVar;
var $r12102 : [int]realVar;
var $r11100 : [int]realVar;
var $r490 : [int][int]realVar;
var $d1101 : realVar;
var $r694 : [int][int]realVar;
Block76:
	r085 := __this;
	 //  @line: 60
	$r284 := $newvariable((77));
	 assume ($neref(($newvariable((77))), ($null))==1);
	 assert ($neref((r085), ($null))==1);
	 //  @line: 60
	$r386 := $HeapVar[r085, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 60
	$i087 := $fresh25;
	 assert ($neref(($r284), ($null))==1);
	 //  @line: 60
	 call void$Matrix$$la$init$ra$$2228(($r284), ($i087));
	 //  @line: 60
	r188 := $r284;
	 //  @line: 61
	i2103 := 0;
	 goto Block78;
	 //  @line: 61
Block78:
	 assert ($neref((r085), ($null))==1);
	 //  @line: 61
	$r490 := $HeapVar[r085, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 61
	$i191 := $fresh26;
	 goto Block79;
	 //  @line: 61
Block79:
	 goto Block80, Block82;
	 //  @line: 61
Block80:
	 assume ($geint((i2103), ($i191))==1);
	 goto Block81;
	 //  @line: 61
Block82:
	 //  @line: 61
	 assume ($negInt(($geint((i2103), ($i191))))==1);
	 //  @line: 62
	i3104 := 0;
	 goto Block83;
	 //  @line: 66
Block81:
	 //  @line: 66
	__ret := r188;
	 return;
	 //  @line: 62
Block83:
	 goto Block84, Block86;
	 //  @line: 62
Block84:
	 assume ($gtint((i3104), (i2103))==1);
	 goto Block85;
	 //  @line: 62
Block86:
	 //  @line: 62
	 assume ($negInt(($gtint((i3104), (i2103))))==1);
	 assert ($neref((r188), ($null))==1);
	 //  @line: 63
	$r593 := $HeapVar[r188, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i2103), (0))==1);
	 assert ($ltint((i2103), ($fresh27))==1);
	 //  @line: 63
	$r897 := $r593[i2103];
	 assert ($neref((r085), ($null))==1);
	 //  @line: 63
	$r694 := $HeapVar[r085, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i3104), (0))==1);
	 assert ($ltint((i3104), ($fresh28))==1);
	 //  @line: 63
	$r795 := $r694[i3104];
	 assert ($geint((i2103), (0))==1);
	 assert ($ltint((i2103), ($realArrSize[$r795[$arrSizeIdx]]))==1);
	 //  @line: 63
	$d096 := $r795[i2103];
	 assert ($geint((i3104), (0))==1);
	 assert ($ltint((i3104), ($realArrSize[$r897[$arrSizeIdx]]))==1);
	 //  @line: 63
	$r897[i3104] := $d096;
	 assert ($neref((r188), ($null))==1);
	 //  @line: 64
	$r998 := $HeapVar[r188, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i3104), (0))==1);
	 assert ($ltint((i3104), ($fresh29))==1);
	 //  @line: 64
	$r12102 := $r998[i3104];
	 assert ($neref((r085), ($null))==1);
	 //  @line: 64
	$r1099 := $HeapVar[r085, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i2103), (0))==1);
	 assert ($ltint((i2103), ($fresh30))==1);
	 //  @line: 64
	$r11100 := $r1099[i2103];
	 assert ($geint((i3104), (0))==1);
	 assert ($ltint((i3104), ($realArrSize[$r11100[$arrSizeIdx]]))==1);
	 //  @line: 64
	$d1101 := $r11100[i3104];
	 assert ($geint((i2103), (0))==1);
	 assert ($ltint((i2103), ($realArrSize[$r12102[$arrSizeIdx]]))==1);
	 //  @line: 64
	$r12102[i2103] := $d1101;
	 //  @line: 62
	i3104 := $addint((i3104), (1));
	 goto Block83;
	 //  @line: 61
Block85:
	 //  @line: 61
	i2103 := $addint((i2103), (1));
	 goto Block87;
	 //  @line: 61
Block87:
	 goto Block78;
}


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



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


// 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: 36
// <Matrix: Matrix sum(Matrix)>
procedure Matrix$Matrix$sum$2230(__this : ref, $param_0 : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $r629 : [int][int]realVar;
var $r836 : [int][int]realVar;
var $r322 : ref;
var r226 : ref;
var $d043 : realVar;
var i648 : int;
var $r1140 : [int]realVar;
var $i437 : int;
var $r733 : [int][int]realVar;
var r023 : ref;
var $r1446 : [int]realVar;
var $i231 : int;
var $i130 : int;
var $i334 : int;
var i547 : int;
var $r1342 : [int]realVar;
var $r424 : [int][int]realVar;
var $d245 : realVar;
var $r527 : [int][int]realVar;
var $r938 : [int][int]realVar;
var $r1241 : [int][int]realVar;
var $r1039 : [int][int]realVar;
var $d144 : realVar;
var r128 : ref;
var $i025 : int;
Block38:
	r023 := __this;
	r128 := $param_0;
	 //  @line: 37
	$r322 := $newvariable((39));
	 assume ($neref(($newvariable((39))), ($null))==1);
	 assert ($neref((r023), ($null))==1);
	 //  @line: 37
	$r424 := $HeapVar[r023, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 37
	$i025 := $fresh7;
	 assert ($neref(($r322), ($null))==1);
	 //  @line: 37
	 call void$Matrix$$la$init$ra$$2228(($r322), ($i025));
	 //  @line: 37
	r226 := $r322;
	 assert ($neref((r023), ($null))==1);
	 //  @line: 38
	$r527 := $HeapVar[r023, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 38
	$i231 := $fresh8;
	 assert ($neref((r128), ($null))==1);
	 //  @line: 38
	$r629 := $HeapVar[r128, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 38
	$i130 := $fresh9;
	 goto Block40;
	 //  @line: 38
Block40:
	 goto Block41, Block43;
	 //  @line: 38
Block41:
	 assume ($neint(($i231), ($i130))==1);
	 goto Block42;
	 //  @line: 38
Block43:
	 //  @line: 38
	 assume ($negInt(($neint(($i231), ($i130))))==1);
	 //  @line: 39
	i547 := 0;
	 goto Block44;
	 //  @line: 43
Block42:
	 //  @line: 43
	__ret := r226;
	 return;
	 //  @line: 39
Block44:
	 assert ($neref((r023), ($null))==1);
	 //  @line: 39
	$r733 := $HeapVar[r023, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 39
	$i334 := $fresh10;
	 goto Block45;
	 //  @line: 39
Block45:
	 goto Block46, Block47;
	 //  @line: 39
Block46:
	 assume ($geint((i547), ($i334))==1);
	 goto Block42;
	 //  @line: 39
Block47:
	 //  @line: 39
	 assume ($negInt(($geint((i547), ($i334))))==1);
	 //  @line: 40
	i648 := 0;
	 goto Block48;
	 //  @line: 40
Block48:
	 assert ($neref((r023), ($null))==1);
	 //  @line: 40
	$r836 := $HeapVar[r023, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 40
	$i437 := $fresh11;
	 goto Block49;
	 //  @line: 40
Block49:
	 goto Block52, Block50;
	 //  @line: 40
Block52:
	 //  @line: 40
	 assume ($negInt(($geint((i648), ($i437))))==1);
	 assert ($neref((r226), ($null))==1);
	 //  @line: 41
	$r938 := $HeapVar[r226, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i547), (0))==1);
	 assert ($ltint((i547), ($fresh12))==1);
	 //  @line: 41
	$r1446 := $r938[i547];
	 assert ($neref((r023), ($null))==1);
	 //  @line: 41
	$r1039 := $HeapVar[r023, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i547), (0))==1);
	 assert ($ltint((i547), ($fresh13))==1);
	 //  @line: 41
	$r1140 := $r1039[i547];
	 assert ($geint((i648), (0))==1);
	 assert ($ltint((i648), ($realArrSize[$r1140[$arrSizeIdx]]))==1);
	 //  @line: 41
	$d144 := $r1140[i648];
	 assert ($neref((r128), ($null))==1);
	 //  @line: 41
	$r1241 := $HeapVar[r128, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i547), (0))==1);
	 assert ($ltint((i547), ($fresh14))==1);
	 //  @line: 41
	$r1342 := $r1241[i547];
	 assert ($geint((i648), (0))==1);
	 assert ($ltint((i648), ($realArrSize[$r1342[$arrSizeIdx]]))==1);
	 //  @line: 41
	$d043 := $r1342[i648];
	 //  @line: 41
	$d245 := $addreal(($d144), ($d043));
	 assert ($geint((i648), (0))==1);
	 assert ($ltint((i648), ($realArrSize[$r1446[$arrSizeIdx]]))==1);
	 //  @line: 41
	$r1446[i648] := $d245;
	 //  @line: 40
	i648 := $addint((i648), (1));
	 goto Block48;
	 //  @line: 40
Block50:
	 assume ($geint((i648), ($i437))==1);
	 goto Block51;
	 //  @line: 39
Block51:
	 //  @line: 39
	i547 := $addint((i547), (1));
	 goto Block53;
	 //  @line: 39
Block53:
	 goto Block44;
}


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



	 //  @line: 3
// <Matrix: void <init>(int)>
procedure void$Matrix$$la$init$ra$$2228(__this : ref, $param_0 : int)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var $r13 : [int][int]realVar;
var i18 : int;
var $r37 : [int]realVar;
var i02 : int;
var r01 : ref;
var i29 : int;
var $r26 : [int][int]realVar;
Block16:
	r01 := __this;
	i02 := $param_0;
	 assert ($neref((r01), ($null))==1);
	 //  @line: 4
	 call void$java.lang.Object$$la$init$ra$$28((r01));
	 //  @line: 5
	$r13 := $fresh1;
	 assume ($negInt(($fresh2))==1);
	 assert ($neref((r01), ($null))==1);
	 //  @line: 5
	$HeapVar[r01, double$lp$$rp$$lp$$rp$$Matrix$values254] := $r13;
	 //  @line: 6
	i18 := 0;
	 goto Block18;
	 //  @line: 6
Block18:
	 goto Block21, Block19;
	 //  @line: 6
Block21:
	 //  @line: 6
	 assume ($negInt(($geint((i18), (i02))))==1);
	 //  @line: 7
	i29 := 0;
	 goto Block22;
	 //  @line: 6
Block19:
	 assume ($geint((i18), (i02))==1);
	 goto Block20;
	 //  @line: 7
Block22:
	 goto Block23, Block25;
	 //  @line: 9
Block20:
	 return;
	 //  @line: 7
Block23:
	 assume ($geint((i29), (i02))==1);
	 goto Block24;
	 //  @line: 7
Block25:
	 //  @line: 7
	 assume ($negInt(($geint((i29), (i02))))==1);
	 assert ($neref((r01), ($null))==1);
	 //  @line: 8
	$r26 := $HeapVar[r01, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i18), (0))==1);
	 assert ($ltint((i18), ($fresh2))==1);
	 //  @line: 8
	$r37 := $r26[i18];
	 assert ($geint((i29), (0))==1);
	 assert ($ltint((i29), ($realArrSize[$r37[$arrSizeIdx]]))==1);
	 //  @line: 8
	$r37[i29] := $fresh3;
	 //  @line: 7
	i29 := $addint((i29), (1));
	 goto Block22;
	 //  @line: 6
Block24:
	 //  @line: 6
	i18 := $addint((i18), (1));
	 goto Block26;
	 //  @line: 6
Block26:
	 goto Block18;
}


	 //  @line: 69
// <Matrix: Matrix submatrix(int,int)>
procedure Matrix$Matrix$submatrix$2233(__this : ref, $param_0 : int, $param_1 : int) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $i3109 : int;
var i1120 : int;
var $r3107 : [int][int]realVar;
var i0115 : int;
var i7127 : int;
var i6126 : int;
var $r5118 : [int][int]realVar;
var $r9125 : [int]realVar;
var $r4113 : [int][int]realVar;
var $i5119 : int;
var $r2105 : ref;
var $i2108 : int;
var $r7122 : [int][int]realVar;
var $r8123 : [int]realVar;
var r1110 : ref;
var i8128 : int;
var $i4114 : int;
var r0106 : ref;
var i9129 : int;
var $r6121 : [int][int]realVar;
var $d0124 : realVar;
Block88:
	r0106 := __this;
	i0115 := $param_0;
	i1120 := $param_1;
	 //  @line: 70
	$r2105 := $newvariable((89));
	 assume ($neref(($newvariable((89))), ($null))==1);
	 assert ($neref((r0106), ($null))==1);
	 //  @line: 70
	$r3107 := $HeapVar[r0106, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 70
	$i2108 := $fresh31;
	 //  @line: 70
	$i3109 := $subint(($i2108), (1));
	 assert ($neref(($r2105), ($null))==1);
	 //  @line: 70
	 call void$Matrix$$la$init$ra$$2228(($r2105), ($i3109));
	 //  @line: 70
	r1110 := $r2105;
	 //  @line: 71
	i6126 := 0;
	 //  @line: 71
	i7127 := 0;
	 goto Block90;
	 //  @line: 71
Block90:
	 assert ($neref((r0106), ($null))==1);
	 //  @line: 71
	$r4113 := $HeapVar[r0106, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 71
	$i4114 := $fresh32;
	 goto Block91;
	 //  @line: 71
Block91:
	 goto Block92, Block94;
	 //  @line: 71
Block92:
	 assume ($geint((i6126), ($i4114))==1);
	 goto Block93;
	 //  @line: 71
Block94:
	 //  @line: 71
	 assume ($negInt(($geint((i6126), ($i4114))))==1);
	 goto Block95;
	 //  @line: 80
Block93:
	 //  @line: 80
	__ret := r1110;
	 return;
	 //  @line: 72
Block95:
	 goto Block96, Block98;
	 //  @line: 72
Block96:
	 assume ($eqint((i6126), (i0115))==1);
	 goto Block97;
	 //  @line: 72
Block98:
	 //  @line: 72
	 assume ($negInt(($eqint((i6126), (i0115))))==1);
	 //  @line: 73
	i8128 := 0;
	 //  @line: 73
	i9129 := 0;
	 goto Block99;
	 //  @line: 71
Block97:
	 //  @line: 71
	i6126 := $addint((i6126), (1));
	 goto Block108;
	 //  @line: 73
Block99:
	 assert ($neref((r0106), ($null))==1);
	 //  @line: 73
	$r5118 := $HeapVar[r0106, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 73
	$i5119 := $fresh33;
	 goto Block100;
	 //  @line: 71
Block108:
	 goto Block90;
	 //  @line: 73
Block100:
	 goto Block101, Block103;
	 //  @line: 73
Block101:
	 assume ($geint((i8128), ($i5119))==1);
	 goto Block102;
	 //  @line: 73
Block103:
	 //  @line: 73
	 assume ($negInt(($geint((i8128), ($i5119))))==1);
	 goto Block104;
	 //  @line: 78
Block102:
	 //  @line: 78
	i7127 := $addint((i7127), (1));
	 goto Block97;
	 //  @line: 74
Block104:
	 goto Block107, Block105;
	 //  @line: 74
Block107:
	 //  @line: 74
	 assume ($negInt(($eqint((i8128), (i1120))))==1);
	 assert ($neref((r1110), ($null))==1);
	 //  @line: 75
	$r6121 := $HeapVar[r1110, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i7127), (0))==1);
	 assert ($ltint((i7127), ($fresh34))==1);
	 //  @line: 75
	$r9125 := $r6121[i7127];
	 assert ($neref((r0106), ($null))==1);
	 //  @line: 75
	$r7122 := $HeapVar[r0106, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i6126), (0))==1);
	 assert ($ltint((i6126), ($fresh35))==1);
	 //  @line: 75
	$r8123 := $r7122[i6126];
	 assert ($geint((i8128), (0))==1);
	 assert ($ltint((i8128), ($realArrSize[$r8123[$arrSizeIdx]]))==1);
	 //  @line: 75
	$d0124 := $r8123[i8128];
	 assert ($geint((i9129), (0))==1);
	 assert ($ltint((i9129), ($realArrSize[$r9125[$arrSizeIdx]]))==1);
	 //  @line: 75
	$r9125[i9129] := $d0124;
	 //  @line: 76
	i9129 := $addint((i9129), (1));
	 goto Block106;
	 //  @line: 74
Block105:
	 assume ($eqint((i8128), (i1120))==1);
	 goto Block106;
	 //  @line: 73
Block106:
	 //  @line: 73
	i8128 := $addint((i8128), (1));
	 goto Block99;
}


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



	 //  @line: 10
// <Matrix: void <init>(double[][])>
procedure void$Matrix$$la$init$ra$$2229(__this : ref, $param_0 : [int][int]realVar)
  modifies $HeapVar;
  requires ($neref((__this), ($null))==1);
 {
var r010 : ref;
var $r519 : [int]realVar;
var $d018 : realVar;
var r111 : [int][int]realVar;
var i221 : int;
var i012 : int;
var $r316 : [int][int]realVar;
var i120 : int;
var $r417 : [int]realVar;
var $r213 : [int][int]realVar;
Block27:
	r010 := __this;
	r111 := $param_0;
	 assert ($neref((r010), ($null))==1);
	 //  @line: 11
	 call void$java.lang.Object$$la$init$ra$$28((r010));
	 //  @line: 12
	i012 := $fresh3;
	 //  @line: 13
	$r213 := $fresh4;
	 assume ($negInt(($fresh5))==1);
	 assert ($neref((r010), ($null))==1);
	 //  @line: 13
	$HeapVar[r010, double$lp$$rp$$lp$$rp$$Matrix$values254] := $r213;
	 //  @line: 14
	i120 := 0;
	 goto Block29;
	 //  @line: 14
Block29:
	 goto Block32, Block30;
	 //  @line: 14
Block32:
	 //  @line: 14
	 assume ($negInt(($geint((i120), (i012))))==1);
	 //  @line: 15
	i221 := 0;
	 goto Block33;
	 //  @line: 14
Block30:
	 assume ($geint((i120), (i012))==1);
	 goto Block31;
	 //  @line: 15
Block33:
	 goto Block34, Block36;
	 //  @line: 17
Block31:
	 return;
	 //  @line: 15
Block34:
	 assume ($geint((i221), (i012))==1);
	 goto Block35;
	 //  @line: 15
Block36:
	 //  @line: 15
	 assume ($negInt(($geint((i221), (i012))))==1);
	 assert ($neref((r010), ($null))==1);
	 //  @line: 16
	$r316 := $HeapVar[r010, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i120), (0))==1);
	 assert ($ltint((i120), ($fresh5))==1);
	 //  @line: 16
	$r519 := $r316[i120];
	 assert ($geint((i120), (0))==1);
	 assert ($ltint((i120), ($fresh6))==1);
	 //  @line: 16
	$r417 := r111[i120];
	 assert ($geint((i221), (0))==1);
	 assert ($ltint((i221), ($realArrSize[$r417[$arrSizeIdx]]))==1);
	 //  @line: 16
	$d018 := $r417[i221];
	 assert ($geint((i221), (0))==1);
	 assert ($ltint((i221), ($realArrSize[$r519[$arrSizeIdx]]))==1);
	 //  @line: 16
	$r519[i221] := $d018;
	 //  @line: 15
	i221 := $addint((i221), (1));
	 goto Block33;
	 //  @line: 14
Block35:
	 //  @line: 14
	i120 := $addint((i120), (1));
	 goto Block37;
	 //  @line: 14
Block37:
	 goto Block29;
}


// 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
// <Matrix: Matrix product(Matrix)>
procedure Matrix$Matrix$product$2231(__this : ref, $param_0 : ref) returns (__ret : ref)  requires ($neref((__this), ($null))==1);
 {
var $i052 : int;
var $r1168 : [int][int]realVar;
var $i258 : int;
var $r1270 : [int][int]realVar;
var $r965 : [int][int]realVar;
var $d177 : realVar;
var r050 : ref;
var i681 : int;
var $r554 : [int][int]realVar;
var $r656 : [int][int]realVar;
var i883 : int;
var $r1674 : [int][int]realVar;
var $i361 : int;
var $r349 : ref;
var r155 : ref;
var $r760 : [int][int]realVar;
var $r1472 : [int][int]realVar;
var $r863 : [int][int]realVar;
var r253 : ref;
var $r1371 : [int]realVar;
var $d076 : realVar;
var $r1775 : [int]realVar;
var $i157 : int;
var $d379 : realVar;
var $i569 : int;
var $d278 : realVar;
var $r1573 : [int]realVar;
var $r1066 : [int]realVar;
var $i464 : int;
var $r451 : [int][int]realVar;
var i782 : int;
var $d480 : realVar;
Block54:
	r050 := __this;
	r155 := $param_0;
	 //  @line: 47
	$r349 := $newvariable((55));
	 assume ($neref(($newvariable((55))), ($null))==1);
	 assert ($neref((r050), ($null))==1);
	 //  @line: 47
	$r451 := $HeapVar[r050, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 47
	$i052 := $fresh15;
	 assert ($neref(($r349), ($null))==1);
	 //  @line: 47
	 call void$Matrix$$la$init$ra$$2228(($r349), ($i052));
	 //  @line: 47
	r253 := $r349;
	 assert ($neref((r050), ($null))==1);
	 //  @line: 48
	$r554 := $HeapVar[r050, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 48
	$i258 := $fresh16;
	 assert ($neref((r155), ($null))==1);
	 //  @line: 48
	$r656 := $HeapVar[r155, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 48
	$i157 := $fresh17;
	 goto Block56;
	 //  @line: 48
Block56:
	 goto Block57, Block59;
	 //  @line: 48
Block57:
	 assume ($neint(($i258), ($i157))==1);
	 goto Block58;
	 //  @line: 48
Block59:
	 //  @line: 48
	 assume ($negInt(($neint(($i258), ($i157))))==1);
	 //  @line: 49
	i681 := 0;
	 goto Block60;
	 //  @line: 56
Block58:
	 //  @line: 56
	__ret := r253;
	 return;
	 //  @line: 49
Block60:
	 assert ($neref((r050), ($null))==1);
	 //  @line: 49
	$r760 := $HeapVar[r050, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 49
	$i361 := $fresh18;
	 goto Block61;
	 //  @line: 49
Block61:
	 goto Block63, Block62;
	 //  @line: 49
Block63:
	 //  @line: 49
	 assume ($negInt(($geint((i681), ($i361))))==1);
	 //  @line: 50
	i782 := 0;
	 goto Block64;
	 //  @line: 49
Block62:
	 assume ($geint((i681), ($i361))==1);
	 goto Block58;
	 //  @line: 50
Block64:
	 assert ($neref((r050), ($null))==1);
	 //  @line: 50
	$r863 := $HeapVar[r050, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 50
	$i464 := $fresh19;
	 goto Block65;
	 //  @line: 50
Block65:
	 goto Block68, Block66;
	 //  @line: 50
Block68:
	 //  @line: 50
	 assume ($negInt(($geint((i782), ($i464))))==1);
	 assert ($neref((r253), ($null))==1);
	 //  @line: 51
	$r965 := $HeapVar[r253, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i681), (0))==1);
	 assert ($ltint((i681), ($fresh20))==1);
	 //  @line: 51
	$r1066 := $r965[i681];
	 assert ($geint((i782), (0))==1);
	 assert ($ltint((i782), ($realArrSize[$r1066[$arrSizeIdx]]))==1);
	 //  @line: 51
	$r1066[i782] := $fresh3;
	 //  @line: 52
	i883 := 0;
	 goto Block69;
	 //  @line: 50
Block66:
	 assume ($geint((i782), ($i464))==1);
	 goto Block67;
	 //  @line: 52
Block69:
	 assert ($neref((r050), ($null))==1);
	 //  @line: 52
	$r1168 := $HeapVar[r050, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 52
	$i569 := $fresh21;
	 goto Block70;
	 //  @line: 49
Block67:
	 //  @line: 49
	i681 := $addint((i681), (1));
	 goto Block75;
	 //  @line: 52
Block70:
	 goto Block71, Block73;
	 //  @line: 49
Block75:
	 goto Block60;
	 //  @line: 52
Block71:
	 assume ($geint((i883), ($i569))==1);
	 goto Block72;
	 //  @line: 52
Block73:
	 //  @line: 52
	 assume ($negInt(($geint((i883), ($i569))))==1);
	 assert ($neref((r253), ($null))==1);
	 //  @line: 53
	$r1270 := $HeapVar[r253, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i681), (0))==1);
	 assert ($ltint((i681), ($fresh22))==1);
	 //  @line: 53
	$r1371 := $r1270[i681];
	 assert ($geint((i782), (0))==1);
	 assert ($ltint((i782), ($realArrSize[$r1371[$arrSizeIdx]]))==1);
	 //  @line: 53
	$d379 := $r1371[i782];
	 assert ($neref((r050), ($null))==1);
	 //  @line: 53
	$r1472 := $HeapVar[r050, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i681), (0))==1);
	 assert ($ltint((i681), ($fresh23))==1);
	 //  @line: 53
	$r1573 := $r1472[i681];
	 assert ($geint((i883), (0))==1);
	 assert ($ltint((i883), ($realArrSize[$r1573[$arrSizeIdx]]))==1);
	 //  @line: 53
	$d177 := $r1573[i883];
	 assert ($neref((r155), ($null))==1);
	 //  @line: 53
	$r1674 := $HeapVar[r155, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((i883), (0))==1);
	 assert ($ltint((i883), ($fresh24))==1);
	 //  @line: 53
	$r1775 := $r1674[i883];
	 assert ($geint((i782), (0))==1);
	 assert ($ltint((i782), ($realArrSize[$r1775[$arrSizeIdx]]))==1);
	 //  @line: 53
	$d076 := $r1775[i782];
	 //  @line: 53
	$d278 := $mulreal(($d177), ($d076));
	 //  @line: 53
	$d480 := $addreal(($d379), ($d278));
	 assert ($geint((i782), (0))==1);
	 assert ($ltint((i782), ($realArrSize[$r1371[$arrSizeIdx]]))==1);
	 //  @line: 53
	$r1371[i782] := $d480;
	 //  @line: 52
	i883 := $addint((i883), (1));
	 goto Block69;
	 //  @line: 50
Block72:
	 //  @line: 50
	i782 := $addint((i782), (1));
	 goto Block74;
	 //  @line: 50
Block74:
	 goto Block64;
}


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



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



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


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


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



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



	 //  @line: 83
// <Matrix: double determinant()>
procedure double$Matrix$determinant$2234(__this : ref) returns (__ret : realVar)  requires ($neref((__this), ($null))==1);
 {
var $i0133 : int;
var $r5144 : ref;
var b4151 : int;
var $r3139 : [int][int]realVar;
var $d0141 : realVar;
var $r1132 : [int][int]realVar;
var $r2135 : [int][int]realVar;
var $r7148 : [int]realVar;
var $r4140 : [int]realVar;
var d5149 : realVar;
var $d1142 : realVar;
var r0131 : ref;
var $i1136 : int;
var $d3145 : realVar;
var i3150 : int;
var $d4146 : realVar;
var $d2143 : realVar;
var $i2137 : int;
var $r6147 : [int][int]realVar;
Block109:
	r0131 := __this;
	 //  @line: 84
	d5149 := $fresh3;
	 assert ($neref((r0131), ($null))==1);
	 //  @line: 86
	$r1132 := $HeapVar[r0131, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 86
	$i0133 := $fresh36;
	 goto Block110;
	 //  @line: 86
Block110:
	 goto Block111, Block113;
	 //  @line: 86
Block111:
	 assume ($neint(($i0133), (1))==1);
	 goto Block112;
	 //  @line: 86
Block113:
	 //  @line: 86
	 assume ($negInt(($neint(($i0133), (1))))==1);
	 assert ($neref((r0131), ($null))==1);
	 //  @line: 89
	$r6147 := $HeapVar[r0131, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((0), (0))==1);
	 assert ($ltint((0), ($fresh37))==1);
	 //  @line: 89
	$r7148 := $r6147[0];
	 assert ($geint((0), (0))==1);
	 assert ($ltint((0), ($realArrSize[$r7148[$arrSizeIdx]]))==1);
	 //  @line: 89
	d5149 := $r7148[0];
	 goto Block114;
	 //  @line: 89
Block112:
	 //  @line: 89
	i3150 := 0;
	 goto Block115;
	 //  @line: 96
Block114:
	 //  @line: 96
	__ret := d5149;
	 return;
	 //  @line: 89
Block115:
	 assert ($neref((r0131), ($null))==1);
	 //  @line: 89
	$r2135 := $HeapVar[r0131, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 //  @line: 89
	$i1136 := $fresh38;
	 goto Block116;
	 //  @line: 89
Block116:
	 goto Block118, Block117;
	 //  @line: 89
Block118:
	 //  @line: 89
	 assume ($negInt(($geint((i3150), ($i1136))))==1);
	 //  @line: 90
	$i2137 := $modint((i3150), (2));
	 goto Block119;
	 //  @line: 89
Block117:
	 assume ($geint((i3150), ($i1136))==1);
	 goto Block114;
	 //  @line: 90
Block119:
	 goto Block120, Block122;
	 //  @line: 90
Block120:
	 assume ($neint(($i2137), (0))==1);
	 goto Block121;
	 //  @line: 90
Block122:
	 //  @line: 90
	 assume ($negInt(($neint(($i2137), (0))))==1);
	 //  @line: 89
	b4151 := 1;
	 goto Block123;
	 //  @line: 91
Block121:
	 //  @line: 91
	b4151 := -1;
	 goto Block123;
	 //  @line: 92
Block123:
	 //  @line: 92
	$d1142 := $inttoreal((b4151));
	 goto Block124;
	 //  @line: 92
Block124:
	 assert ($neref((r0131), ($null))==1);
	 //  @line: 92
	$r3139 := $HeapVar[r0131, double$lp$$rp$$lp$$rp$$Matrix$values254];
	 assert ($geint((0), (0))==1);
	 assert ($ltint((0), ($fresh39))==1);
	 //  @line: 92
	$r4140 := $r3139[0];
	 assert ($geint((i3150), (0))==1);
	 assert ($ltint((i3150), ($realArrSize[$r4140[$arrSizeIdx]]))==1);
	 //  @line: 92
	$d0141 := $r4140[i3150];
	 //  @line: 92
	$d2143 := $mulreal(($d1142), ($d0141));
	 assert ($neref((r0131), ($null))==1);
	 //  @line: 92
	 call $r5144 := Matrix$Matrix$submatrix$2233((r0131), (0), (i3150));
	 assert ($neref(($r5144), ($null))==1);
	 //  @line: 92
	 call $d3145 := double$Matrix$determinant$2234(($r5144));
	 //  @line: 92
	$d4146 := $mulreal(($d2143), ($d3145));
	 //  @line: 92
	d5149 := $addreal((d5149), ($d4146));
	 //  @line: 89
	i3150 := $addint((i3150), (1));
	 goto Block115;
}


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



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



	 //  @line: 99
// <Matrix: void main(java.lang.String[])>
procedure void$Matrix$main$2235($param_0 : [int]ref) {
var $r5156 : ref;
var i8181 : int;
var $r8173 : [int]realVar;
var $i4174 : int;
var $r9176 : [int]realVar;
var r3154 : [int][int]realVar;
var r0152 : [int]ref;
var r1157 : ref;
var $r6159 : ref;
var i7180 : int;
var i10184 : int;
var $i1168 : int;
var $r10179 : [int]realVar;
var i9183 : int;
var $i5175 : int;
var $r7172 : [int]realVar;
var $d1171 : realVar;
var r2160 : ref;
var $i2169 : int;
var $d2178 : realVar;
var i0153 : int;
var r11182 : [int][int]realVar;
var $i6177 : int;
var $i3170 : int;

 //temp local variables 
var $freshlocal3 : realVar;
var $freshlocal2 : ref;
var $freshlocal1 : ref;
var $freshlocal0 : ref;

Block125:
	r0152 := $param_0;
	 //  @line: 100
	i0153 := $refArrSize[r0152[$arrSizeIdx]];
	 //  @line: 103
	r3154 := $fresh6;
	 assume ($negInt(($fresh7))==1);
	 //  @line: 104
	i7180 := 0;
	 goto Block127;
	 //  @line: 104
Block127:
	 goto Block128, Block130;
	 //  @line: 104
Block128:
	 assume ($geint((i7180), (i0153))==1);
	 goto Block129;
	 //  @line: 104
Block130:
	 //  @line: 104
	 assume ($negInt(($geint((i7180), (i0153))))==1);
	 //  @line: 105
	i8181 := 0;
	 goto Block131;
	 //  @line: 108
Block129:
	 //  @line: 108
	$r5156 := $newvariable((142));
	 assume ($neref(($newvariable((142))), ($null))==1);
	 goto Block143;
	 //  @line: 105
Block131:
	 goto Block134, Block132;
	 //  @line: 108
Block143:
	 assert ($neref(($r5156), ($null))==1);
	 //  @line: 108
	 call void$Matrix$$la$init$ra$$2229(($r5156), (r3154));
	 //  @line: 108
	r1157 := $r5156;
	 //  @line: 110
	r11182 := $fresh8;
	 assume ($negInt(($fresh9))==1);
	 //  @line: 111
	i9183 := 0;
	 goto Block145;
	 //  @line: 105
Block134:
	 //  @line: 105
	 assume ($negInt(($geint((i8181), (i0153))))==1);
	 //  @line: 106
	$i4174 := $addint((i7180), (i8181));
	 //  @line: 106
	$i5175 := $modint(($i4174), (2));
	 goto Block135;
	 //  @line: 105
Block132:
	 assume ($geint((i8181), (i0153))==1);
	 goto Block133;
	 //  @line: 111
Block145:
	 goto Block148, Block146;
	 //  @line: 106
Block135:
	 goto Block136, Block138;
	 //  @line: 104
Block133:
	 //  @line: 104
	i7180 := $addint((i7180), (1));
	 goto Block141;
	 //  @line: 111
Block148:
	 //  @line: 111
	 assume ($negInt(($geint((i9183), (i0153))))==1);
	 //  @line: 112
	i10184 := 0;
	 goto Block149;
	 //  @line: 111
Block146:
	 assume ($geint((i9183), (i0153))==1);
	 goto Block147;
	 //  @line: 106
Block136:
	 assume ($neint(($i5175), (0))==1);
	 goto Block137;
	 //  @line: 106
Block138:
	 //  @line: 106
	 assume ($negInt(($neint(($i5175), (0))))==1);
	 assert ($geint((i7180), (0))==1);
	 assert ($ltint((i7180), ($fresh41))==1);
	 //  @line: 105
	$r10179 := r3154[i7180];
	 //  @line: 105
	$i6177 := $addint((i0153), (i7180));
	 //  @line: 105
	$d2178 := $inttoreal(($i6177));
	 assert ($geint((i8181), (0))==1);
	 assert ($ltint((i8181), ($realArrSize[$r10179[$arrSizeIdx]]))==1);
	 //  @line: 105
	$r10179[i8181] := $d2178;
	 goto Block139;
	 //  @line: 104
Block141:
	 goto Block127;
	 //  @line: 112
Block149:
	 goto Block152, Block150;
	 //  @line: 115
Block147:
	 //  @line: 115
	$r6159 := $newvariable((160));
	 assume ($neref(($newvariable((160))), ($null))==1);
	 goto Block161;
	 //  @line: 107
Block137:
	 assert ($geint((i7180), (0))==1);
	 assert ($ltint((i7180), ($fresh42))==1);
	 //  @line: 107
	$r9176 := r3154[i7180];
	 goto Block140;
	 //  @line: 105
Block139:
	 //  @line: 105
	i8181 := $addint((i8181), (1));
	 goto Block131;
	 //  @line: 112
Block152:
	 //  @line: 112
	 assume ($negInt(($geint((i10184), (i0153))))==1);
	 //  @line: 113
	$i1168 := $addint((i9183), (i10184));
	 //  @line: 113
	$i2169 := $modint(($i1168), (3));
	 goto Block153;
	 //  @line: 112
Block150:
	 assume ($geint((i10184), (i0153))==1);
	 goto Block151;
	 //  @line: 115
Block161:
	 assert ($neref(($r6159), ($null))==1);
	 //  @line: 115
	 call void$Matrix$$la$init$ra$$2229(($r6159), (r11182));
	 //  @line: 115
	r2160 := $r6159;
	 assert ($neref((r1157), ($null))==1);
	 //  @line: 120
	 call $freshlocal0 := Matrix$Matrix$sum$2230((r1157), (r2160));
	 assert ($neref((r1157), ($null))==1);
	 //  @line: 123
	 call $freshlocal1 := Matrix$Matrix$product$2231((r1157), (r2160));
	 assert ($neref((r1157), ($null))==1);
	 //  @line: 126
	 call $freshlocal2 := Matrix$Matrix$transpose$2232((r1157));
	 assert ($neref((r2160), ($null))==1);
	 //  @line: 129
	 call $freshlocal3 := double$Matrix$determinant$2234((r2160));
	 return;
	 //  @line: 107
Block140:
	 assert ($geint((i8181), (0))==1);
	 assert ($ltint((i8181), ($realArrSize[$r9176[$arrSizeIdx]]))==1);
	 //  @line: 107
	$r9176[i8181] := $fresh3;
	 goto Block139;
	 //  @line: 113
Block153:
	 goto Block154, Block156;
	 //  @line: 111
Block151:
	 //  @line: 111
	i9183 := $addint((i9183), (1));
	 goto Block159;
	 //  @line: 113
Block154:
	 assume ($neint(($i2169), (0))==1);
	 goto Block155;
	 //  @line: 113
Block156:
	 //  @line: 113
	 assume ($negInt(($neint(($i2169), (0))))==1);
	 assert ($geint((i9183), (0))==1);
	 assert ($ltint((i9183), ($fresh44))==1);
	 //  @line: 112
	$r8173 := r11182[i9183];
	 assert ($geint((i10184), (0))==1);
	 assert ($ltint((i10184), ($realArrSize[$r8173[$arrSizeIdx]]))==1);
	 //  @line: 112
	$r8173[i10184] := $fresh3;
	 goto Block157;
	 //  @line: 111
Block159:
	 goto Block145;
	 //  @line: 114
Block155:
	 assert ($geint((i9183), (0))==1);
	 assert ($ltint((i9183), ($fresh45))==1);
	 //  @line: 114
	$r7172 := r11182[i9183];
	 goto Block158;
	 //  @line: 112
Block157:
	 //  @line: 112
	i10184 := $addint((i10184), (1));
	 goto Block149;
	 //  @line: 114
Block158:
	 //  @line: 114
	$i3170 := $subint((i0153), (i9183));
	 //  @line: 114
	$d1171 := $inttoreal(($i3170));
	 assert ($geint((i10184), (0))==1);
	 assert ($ltint((i10184), ($realArrSize[$r7172[$arrSizeIdx]]))==1);
	 //  @line: 114
	$r7172[i10184] := $d1171;
	 goto Block157;
}


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