// Testfile dumped by Ultimate at 2013/11/09 20:30:42 print(numberOfStates(nwa)); NestedWordAutomaton complement = buchiComplementFKV(nwa); print(numberOfStates(complement)); assert(numberOfStates(complement) == 89);// with MatthiasTightLevelRankingStateGenerator result was 101 and minimizeSevpa reduced it to 65 NestedWordAutomaton live = removeNonLiveStates(complement); print(numberOfStates(live)); assert(numberOfStates(live) == 89); minimizeSevpa(complement); //reduced to 65 NestedWordAutomaton nwa = ( callAlphabet = {"39711call #t~ret428 := main();" }, internalAlphabet = {"42807assume !(~v61~3 <= ~v46~3);" "40191assume !!(~v71~3 <= ~v60~3);assume !!(1 ..." "42805assume !(~v46~3 <= ~v61~3);" "42803assume !(~v40~3 <= ~v60~3);" "42801assume !(~v60~3 <= ~v40~3);" "41852assume !!(0 <= ~v36~3);call #t~ret95 := ..." "40184assume !!(~v71~3 <= ~v40~3);assume !!(~v..." "42815assume !(#t~ret208 != 0);havoc #t~ret208..." "42813assume !(1 + ~v43~3 <= ~v46~3);" "40181assume !!(~v60~3 <= ~v40~3);assume !!(~v..." "42811assume !(2 <= ~v43~3);" "40178assume !!(~v46~3 <= ~v61~3);assume !!(~v..." "42809assume !(~v43~3 <= 2);" "40175assume !!(~v43~3 <= 1);assume !!(~v61~3 ..." "42791assume !(1 <= ~v46~3);" "40172assume !!(1 + ~v43~3 <= ~v46~3);~v71~3 :..." "42789assume !!(1 <= ~v46~3);assume !(2 <= ~v4..." "42786assume !(0 <= ~v43~3);" "42784assume !!(0 <= ~v43~3);call #t~ret117 :=..." "42799assume !(~v40~3 <= ~v71~3);" "40164assume #t~ret336 != 0;havoc #t~ret336;ca..." "42797assume !(~v71~3 <= ~v40~3);" "42795assume !(~v60~3 <= ~v71~3);" "42793assume !(~v71~3 <= ~v60~3);" "42769assume !!(~v43~3 <= 1 + ~v41~3);assume !..." "40152assume !(#t~ret291 != 0);havoc #t~ret291..." "42771assume !(~v43~3 <= 1 + ~v41~3);" "41809assume !(#t~ret94 != 0);havoc #t~ret94;" "41811assume #t~ret94 != 0;havoc #t~ret94;" "40146assume !!(~v46~3 <= ~v61~3);call #t~ret2..." "40140assume !!(~v40~3 <= 0);assume !!(~v61~3 ..." "42757assume !!(0 <= ~v43~3);call #t~ret102 :=..." "41801call #t~ret81 := nondet_bool();havoc ~a~..." "42759assume !(0 <= ~v43~3);" "40137assume !!(~v43~3 <= 0);assume !!(0 <= ~v..." "41807assume !(#t~ret81 != 0);havoc #t~ret81;c..." "42764assume !!(~v41~3 <= -1 + ~v43~3);assume ..." "41793assume !!(1 <= ~v61~3);assume !!(2 <= ~v..." "40134assume #t~ret191 != 0;havoc #t~ret191;ca..." "42766assume !(~v41~3 <= -1 + ~v43~3);" "41796assume !!(-1 + ~v44~3 <= ~v35~3);assume ..." "42761assume !(1 + ~v41~3 <= ~v46~3);" "40121call #t~ret0 := nondet();havoc ~a~1;#res..." "41785assume #t~ret188 != 0;havoc #t~ret188;~v..." "41778assume #t~ret188 != 0;havoc #t~ret188;~v..." "42850assume !(1 + ~v43~3 <= ~v46~3);" "42848assume !!(1 + ~v43~3 <= ~v46~3);~v71~3 :..." "42854assume #t~ret291 != 0;havoc #t~ret291;" "41771assume #t~ret186 != 0;havoc #t~ret186;~v..." "42852assume !(#t~ret336 != 0);havoc #t~ret336..." "41760assume !!(~v35~3 <= ~v36~3);assume !!(~v..." "42833assume !!(~v46~3 <= ~v61~3);assume !(~v4..." "42835assume !(~v46~3 <= ~v61~3);" "41753assume !!(~v38~3 <= ~v80~3);assume !!(~v..." "42838assume !!(~v43~3 <= 1);assume !(~v61~3 <..." "42840assume !(~v43~3 <= 1);" "41750assume !!(~v73~3 <= ~v79~3);assume !!(~v..." "41744assume !!(~v72~3 <= ~v79~3);assume !!(~v..." "41747assume !!(~v72~3 <= ~v66~3);assume !!(~v..." "41741assume !!(~v72~3 <= ~v73~3);assume !!(~v..." "42818assume !!(~v71~3 <= ~v60~3);assume !(1 <..." "42820assume !(~v71~3 <= ~v60~3);" "41738assume !!(0 <= -1 * ~v35~3 + ~v36~3);ass..." "42823assume !!(~v71~3 <= ~v40~3);assume !(~v6..." "41732assume !!(0 <= ~v38~3);assume !!(~v38~3 ..." "42825assume !(~v71~3 <= ~v40~3);" "41735assume !!(0 <= ~v80~3);assume !!(~v80~3 ..." "42828assume !!(~v60~3 <= ~v40~3);assume !(~v4..." "41729assume #t~ret183 != 0;havoc #t~ret183;~v..." "42830assume !(~v60~3 <= ~v40~3);" "41970assume !(~v79~3 <= ~v73~3);" "41968assume !!(~v79~3 <= ~v73~3);assume !(~v3..." "41975assume !(~v79~3 <= ~v72~3);" "41973assume !!(~v79~3 <= ~v72~3);assume !(~v7..." "41978assume !!(~v73~3 <= ~v72~3);assume !(~v7..." "41983assume !!(~v80~3 <= 0);assume !(~v72~3 <..." "41980assume !(~v73~3 <= ~v72~3);" "41958assume !!(-1 + ~v36~3 <= ~v37~3);call #t..." "41963assume !!(~v80~3 <= ~v38~3);assume !(~v3..." "42918assume !!(0 <= ~v77~3);" "41960assume !(-1 + ~v36~3 <= ~v37~3);" "42916assume !!(~v46~3 <= ~v43~3);~v69~3 := ~v..." "41965assume !(~v80~3 <= ~v38~3);" "41937assume !(2 <= ~v61~3);" "41940assume #t~ret425 != 0;havoc #t~ret425;as..." "41942assume !(#t~ret425 != 0);havoc #t~ret425..." "41949assume #t~ret423 != 0;havoc #t~ret423;~v..." "41951assume !(#t~ret423 != 0);havoc #t~ret423..." "41925assume !!(~v37~3 <= ~v36~3);call #t~ret4..." "41927assume !(~v37~3 <= ~v36~3);" "41935assume !!(2 <= ~v61~3);call #t~ret426 :=..." "41911assume !!(2 <= ~v61~3);call #t~ret426 :=..." "41918assume !!(~v37~3 <= ~v36~3);call #t~ret4..." "41889assume !!(-1 + ~v36~3 <= ~v37~3);call #t..." "41903assume #t~ret425 != 0;havoc #t~ret425;as..." "41900assume #t~ret423 != 0;havoc #t~ret423;~v..." "41878assume !!(~v80~3 <= ~v38~3);assume !!(~v..." "41872assume !!(~v79~3 <= ~v72~3);assume !!(~v..." "41875assume !!(~v79~3 <= ~v73~3);assume !!(~v..." "41860assume #t~ret420 != 0;havoc #t~ret420;~v..." "41863assume !!(~v38~3 <= 0);assume !!(0 <= ~v..." "41869assume !!(~v73~3 <= ~v72~3);assume !!(~v..." "41866assume !!(~v80~3 <= 0);assume !!(~v72~3 ..." "42503assume !!(0 <= ~v31~3);assume !!(0 <= ~v..." "42500assume !!(~v61~3 <= ~v42~3);call #t~ret3..." "40360assume !(#t~ret228 != 0);havoc #t~ret228..." "40361assume true;" "40364assume #t~ret228 != 0;havoc #t~ret228;" "41513assume !!(~v45~3 <= ~v44~3);call #t~ret3..." "40366assume !!(1 <= ~v61~3);" "40352assume !!(~v34~3 <= ~v72~3);call #t~ret2..." "40358assume #t~ret227 != 0;havoc #t~ret227;~v..." "41506assume !!(~v33~3 <= ~v32~3);call #t~ret3..." "42606assume !!(~v77~3 <= 0);assume !!(0 <= ~v..." "42609assume !!(0 <= ~v38~3);assume !!(~v38~3 ..." "41532assume !!(0 <= ~v77~3);assume !!(~v77~3 ..." "41529assume !!(0 <= ~v44~3);assume !!(0 <= ~v..." "42612assume !!(0 <= ~v80~3);assume !!(~v80~3 ..." "42615assume !!(1 <= ~v44~3);assume !!(~v44~3 ..." "40368assume !!(~v61~3 <= 1);" "41526call #t~ret120 := nondet_bool();havoc ~a..." "42618assume !!(~v72~3 <= ~v73~3);assume !!(~v..." "40370assume !!(0 <= ~v77~3);" "42621assume !!(~v72~3 <= ~v79~3);assume !!(~v..." "41520assume !!(~v45~3 <= ~v44~3);call #t~ret3..." "41487assume #t~ret362 != 0;havoc #t~ret362;~v..." "40334assume !!(0 <= ~v77~3);" "40332assume #t~ret214 != 0;havoc #t~ret214;~v..." "41476assume !!(~v33~3 <= -1 + ~v32~3);assume ..." "40346assume !!(~v72~3 <= ~v34~3);" "40344assume !!(~v61~3 <= 1);" "41498assume !!(2 <= ~v61~3);call #t~ret365 :=..." "40338assume !!(0 <= ~v63~3);" "40336assume !!(~v77~3 <= 0);" "41490assume #t~ret364 != 0;havoc #t~ret364;as..." "40342assume !!(1 <= ~v61~3);" "40340assume !!(~v63~3 <= 0);" "42669assume !!(~v38~3 <= ~v80~3);assume !(~v8..." "42671assume !(~v38~3 <= ~v80~3);" "42664assume !!(~v79~3 <= ~v75~3);assume !(~v7..." "42666assume !(~v79~3 <= ~v75~3);" "42661assume !(#t~ret396 != 0);havoc #t~ret396..." "42657assume !!(1 <= ~v61~3);assume !(2 <= ~v6..." "42659assume !(1 <= ~v61~3);" "42684assume !!(~v72~3 <= ~v79~3);assume !(~v7..." "42686assume !(~v72~3 <= ~v79~3);" "42681assume !(~v72~3 <= ~v75~3);" "41717assume #t~ret177 != 0;havoc #t~ret177;as..." "42676assume !(~v73~3 <= ~v79~3);" "42679assume !!(~v72~3 <= ~v75~3);assume !(~v7..." "42674assume !!(~v73~3 <= ~v79~3);assume !(~v7..." "42637assume !!(~v79~3 <= ~v75~3);assume !!(~v..." "43615call #t~ret0 := nondet();havoc ~a~1;#res..." "41670assume #t~ret340 != 0;havoc #t~ret340;~v..." "42630assume !!(~v38~3 <= ~v80~3);assume !!(~v..." "40270assume #t~ret213 != 0;havoc #t~ret213;~v..." "42627assume !!(~v73~3 <= ~v79~3);assume !!(~v..." "41677assume #t~ret340 != 0;havoc #t~ret340;~v..." "42624assume !!(~v72~3 <= ~v75~3);assume !!(~v..." "40264assume !!(~v46~3 <= ~v43~3);~v69~3 := ~v..." "42654assume !!(1 <= ~v61~3);assume !!(2 <= ~v..." "41680assume !!(1 <= ~v61~3);assume !!(2 <= ~v..." "42651assume #t~ret396 != 0;havoc #t~ret396;~v..." "41685call #t~ret177 := nondet_bool();havoc ~a..." "42644assume #t~ret396 != 0;havoc #t~ret396;~v..." "42728assume !!(~v72~3 <= ~v34~3);assume !(~v3..." "42730assume !(~v72~3 <= ~v34~3);" "41638assume !!(0 <= ~v38~3);assume !!(~v38~3 ..." "42733assume !!(0 <= ~v63~3);assume !(~v63~3 <..." "41635assume !!(0 <= ~v44~3);assume !!(0 <= ~v..." "42735assume !(0 <= ~v63~3);" "42721assume !!(1 <= ~v61~3);assume !(2 <= ~v6..." "41644assume !!(~v72~3 <= ~v73~3);assume !!(~v..." "41647assume !!(~v72~3 <= ~v79~3);assume !!(~v..." "42723assume !(1 <= ~v61~3);" "42725assume !(#t~ret288 != 0);havoc #t~ret288..." "41641assume !!(0 <= ~v80~3);assume !!(~v80~3 ..." "42744assume !(#t~ret274 != 0);havoc #t~ret274..." "41653assume !!(~v73~3 <= ~v79~3);assume !!(~v..." "41650assume !!(~v72~3 <= ~v75~3);assume !!(~v..." "41663assume !!(~v79~3 <= ~v75~3);assume !!(~v..." "41656assume !!(~v38~3 <= ~v80~3);assume !!(~v..." "42742assume #t~ret274 != 0;havoc #t~ret274;~v..." "42699assume !!(0 <= ~v80~3);assume !(~v80~3 <..." "42696assume !(1 <= ~v44~3);" "40198assume #t~ret194 != 0;havoc #t~ret194;ca..." "42701assume !(0 <= ~v80~3);" "42691assume !(~v72~3 <= ~v73~3);" "42689assume !!(~v72~3 <= ~v73~3);assume !(~v7..." "42694assume !!(1 <= ~v44~3);assume !(~v44~3 <..." "42714assume !!(0 <= ~v31~3);assume !(0 <= ~v7..." "42718assume !(~v61~3 <= ~v42~3);" "42716assume !(0 <= ~v31~3);" "42706assume !(0 <= ~v38~3);" "42704assume !!(0 <= ~v38~3);assume !(~v38~3 <..." "42711assume !(~v77~3 <= 0);" "42709assume !!(~v77~3 <= 0);assume !(0 <= ~v3..." "42256assume !!(0 <= ~v77~3);assume !(~v77~3 <..." "42258assume !(0 <= ~v77~3);" "42261assume !!(0 <= ~v44~3);assume !(0 <= ~v3..." "41304call #t~ret120 := nondet_bool();havoc ~a..." "42263assume !(0 <= ~v44~3);" "42265assume !(~v45~3 <= ~v44~3);" "42241assume !!(0 <= ~v80~3);assume !(~v80~3 <..." "41293assume !!(1 <= ~v61~3);assume !!(2 <= ~v..." "42243assume !(0 <= ~v80~3);" "42246assume !!(0 <= ~v38~3);assume !(~v38~3 <..." "41290assume #t~ret417 != 0;havoc #t~ret417;~v..." "42248assume !(0 <= ~v38~3);" "42251assume !!(0 <= ~v44~3);assume !(0 <= ~v3..." "42253assume !(0 <= ~v44~3);" "41283assume #t~ret417 != 0;havoc #t~ret417;~v..." "40699assume !(~v75~3 <= ~v80~3);" "42290assume !(#t~ret364 != 0);havoc #t~ret364..." "40697assume #t~ret273 != 0;havoc #t~ret273;~v..." "42288assume #t~ret364 != 0;havoc #t~ret364;as..." "40703assume !(~v61~3 <= 1);" "40701assume !(~v80~3 <= ~v75~3);" "42299assume !(#t~ret362 != 0);havoc #t~ret362..." "42297assume #t~ret362 != 0;havoc #t~ret362;~v..." "40695assume !(#t~ret273 != 0);havoc #t~ret273..." "42302assume !!(~v33~3 <= -1 + ~v32~3);assume ..." "40693assume !!(~v75~3 <= ~v80~3);call #t~ret2..." "42275assume !(~v33~3 <= ~v32~3);" "42273assume !!(~v33~3 <= ~v32~3);call #t~ret3..." "42283assume !!(2 <= ~v61~3);call #t~ret365 :=..." "41315call #t~ret120 := nondet_bool();havoc ~a..." "42285assume !(2 <= ~v61~3);" "40605assume !!(~v80~3 <= ~v38~3);call #t~ret2..." "42324assume !(0 <= ~v63~3);" "42327assume !!(0 <= ~v64~3);assume !(~v64~3 <..." "42322assume !!(0 <= ~v63~3);assume !(~v63~3 <..." "40597assume !!(~v79~3 <= ~v73~3);" "40599assume !!(~v38~3 <= ~v80~3);" "40593assume !!(~v66~3 <= ~v72~3);" "42329assume !(0 <= ~v64~3);" "40595assume !!(~v73~3 <= ~v79~3);" "40589assume !!(~v79~3 <= ~v72~3);" "42309assume !(~v77~3 <= ~v47~3);" "40591assume !!(~v72~3 <= ~v66~3);" "42304assume !(~v33~3 <= -1 + ~v32~3);" "40585assume !!(~v73~3 <= ~v72~3);" "40587assume !!(~v72~3 <= ~v79~3);" "42307assume !!(~v77~3 <= ~v47~3);assume !(~v4..." "42317assume !!(1 <= -1 * ~v44~3 + ~v45~3);ass..." "40581assume !!(~v61~3 <= 1);" "42319assume !(1 <= -1 * ~v44~3 + ~v45~3);" "40583assume !!(~v72~3 <= ~v73~3);" "42312assume !!(~v72~3 <= ~v34~3);assume !(~v3..." "40577assume !!(~v75~3 <= 0);" "42314assume !(~v72~3 <= ~v34~3);" "40579assume !!(1 <= ~v61~3);" "42359assume !(~v34~3 <= ~v72~3);" "42357assume !!(~v34~3 <= ~v72~3);call #t~ret4..." "41276assume !!(~v34~3 <= ~v72~3);call #t~ret4..." "40632assume !!(~v80~3 <= ~v75~3);" "42367assume !!(~v64~3 <= 0);assume !(0 <= ~v6..." "40630assume !!(~v61~3 <= 1);call #t~ret261 :=..." "39673havoc ~a~1;#res := ~a~1;assume true;" "41265assume !!(~v63~3 <= 0);assume !!(~v72~3 ..." "42364assume !(~v63~3 <= 0);" "42362assume !!(~v63~3 <= 0);assume !(~v72~3 <..." "41259assume #t~ret399 != 0;havoc #t~ret399;ca..." "40623assume !!(1 <= ~v61~3);" "42343assume !(0 <= ~v44~3);" "40621assume #t~ret260 != 0;havoc #t~ret260;" "42341assume !!(0 <= ~v44~3);assume !(0 <= ~v3..." "41262assume !!(~v64~3 <= 0);assume !!(0 <= ~v..." "42338assume !(#t~ret342 != 0);havoc #t~ret342..." "40619assume !(#t~ret260 != 0);havoc #t~ret260..." "42336assume #t~ret342 != 0;havoc #t~ret342;~v..." "40617assume #t~ret259 != 0;havoc #t~ret259;~v..." "42350assume !(#t~ret417 != 0);havoc #t~ret417..." "42348assume !(1 <= ~v61~3);" "42346assume !!(1 <= ~v61~3);assume !(2 <= ~v6..." "40611assume #t~ret258 != 0;havoc #t~ret258;~v..." "40512assume !!(~v75~3 <= ~v79~3);call #t~ret2..." "40518assume #t~ret249 != 0;havoc #t~ret249;~v..." "42369assume !(~v64~3 <= 0);" "40520assume !(#t~ret250 != 0);havoc #t~ret250..." "40522assume #t~ret250 != 0;havoc #t~ret250;" "40524assume !!(1 <= ~v61~3);" "41463assume !!(1 <= -1 * ~v44~3 + ~v45~3);ass..." "40563assume !(#t~ret257 != 0);havoc #t~ret257..." "41460assume !!(0 <= ~v63~3);assume !!(~v63~3 ..." "40561assume #t~ret256 != 0;havoc #t~ret256;~v..." "40567assume !!(0 <= ~v38~3);" "41457assume !!(0 <= ~v64~3);assume !!(~v64~3 ..." "40565assume #t~ret257 != 0;havoc #t~ret257;~v..." "40571assume !!(0 <= ~v80~3);" "40569assume !!(~v38~3 <= 0);" "41469assume !!(~v77~3 <= ~v47~3);assume !!(~v..." "41466assume !!(~v72~3 <= ~v34~3);assume !!(~v..." "40575assume !!(0 <= ~v75~3);" "40573assume !!(~v80~3 <= 0);" "40555assume !!(~v61~3 <= 1);call #t~ret251 :=..." "41454assume #t~ret342 != 0;havoc #t~ret342;~v..." "42452assume #t~ret399 != 0;havoc #t~ret399;ca..." "40476assume !!(~v38~3 <= 0);" "42454assume !(#t~ret399 != 0);havoc #t~ret399..." "40478assume !!(0 <= ~v80~3);" "40472assume !!(~v77~3 <= 0);call #t~ret229 :=..." "40474assume !!(0 <= ~v38~3);" "41357assume !!(0 <= ~v44~3);assume !!(0 <= ~v..." "40502assume !!(~v38~3 <= ~v80~3);" "40500assume !!(~v79~3 <= ~v73~3);" "42493assume !(0 <= ~v31~3);" "40498assume !!(~v73~3 <= ~v79~3);" "42491assume !!(0 <= ~v31~3);call #t~ret390 :=..." "40496assume !!(~v75~3 <= ~v72~3);" "40506assume !!(~v79~3 <= ~v75~3);" "40504assume !!(~v80~3 <= ~v38~3);" "40486assume !!(~v72~3 <= ~v73~3);" "40484assume !!(~v61~3 <= 1);" "40482assume !!(1 <= ~v61~3);" "40480assume !!(~v80~3 <= 0);" "40494assume !!(~v72~3 <= ~v75~3);" "40492assume !!(~v79~3 <= ~v72~3);" "40490assume !!(~v72~3 <= ~v79~3);" "40488assume !!(~v73~3 <= ~v72~3);" "41985assume !(~v80~3 <= 0);" "41990assume !(~v38~3 <= 0);" "41988assume !!(~v38~3 <= 0);assume !(0 <= ~v8..." "40896call #t~ret101 := nondet_bool();havoc ~a..." "41998assume #t~ret420 != 0;havoc #t~ret420;~v..." "43207assume #t~ret191 != 0;havoc #t~ret191;ca..." "42000assume !(#t~ret420 != 0);havoc #t~ret420..." "40920assume !!(~v41~3 <= -1 + ~v43~3);assume ..." "40927assume !!(1 + ~v41~3 <= ~v46~3);call #t~..." "40914assume !!(0 <= ~v43~3);call #t~ret117 :=..." "40917assume !!(~v43~3 <= 1 + ~v41~3);assume !..." "43209assume !(#t~ret191 != 0);havoc #t~ret191..." "40940call #t~ret101 := nondet_bool();havoc ~a..." "40934assume !!(1 + ~v41~3 <= ~v46~3);call #t~..." "41084assume #t~ret274 != 0;havoc #t~ret274;~v..." "41087assume !!(0 <= ~v63~3);assume !!(~v63~3 ..." "42037assume !!(0 <= ~v36~3);call #t~ret95 := ..." "42039assume !(0 <= ~v36~3);" "42041assume #t~ret81 != 0;havoc #t~ret81;" "43154assume !(~v75~3 <= 0);" "40844assume #t~ret208 != 0;havoc #t~ret208;ca..." "43152assume !(~v72~3 <= ~v73~3);" "43158assume !(~v80~3 <= 0);" "42050assume !!(~v80~3 <= ~v75~3);" "43156assume !(0 <= ~v75~3);" "42048assume !!(0 <= ~v36~3);call #t~ret82 := ..." "43162assume !(~v79~3 <= 0);" "43160assume !(0 <= ~v80~3);" "43166assume !(~v38~3 <= 0);" "43164assume !(0 <= ~v79~3);" "40863assume !!(~v60~3 <= ~v40~3);" "43138assume !(~v75~3 <= ~v79~3);" "40861assume !!(~v40~3 <= ~v60~3);" "43136assume !(~v61~3 <= 0);" "40859assume !!(~v46~3 <= ~v61~3);" "43142assume !(~v80~3 <= ~v38~3);" "40857assume !!(~v61~3 <= ~v46~3);" "43140assume !(~v79~3 <= ~v75~3);" "40855assume !!(~v43~3 <= 2);" "43146assume !(~v79~3 <= ~v73~3);" "40853assume !!(2 <= ~v43~3);" "43144assume !(~v38~3 <= ~v80~3);" "40851assume !!(1 + ~v43~3 <= ~v46~3);~v71~3 :..." "43150assume !(~v73~3 <= ~v72~3);" "43148assume !(~v73~3 <= ~v79~3);" "43184assume !(~v46~3 <= ~v61~3);" "43187assume !!(~v40~3 <= 0);assume !(~v61~3 <..." "43189assume !(~v40~3 <= 0);" "40874assume !!(1 <= ~v46~3);assume !!(2 <= ~v..." "43192assume !!(~v43~3 <= 0);assume !(0 <= ~v4..." "40869assume !!(~v60~3 <= ~v71~3);" "43194assume !(~v43~3 <= 0);" "40871assume !!(~v71~3 <= ~v60~3);" "40865assume !!(~v40~3 <= ~v71~3);" "40867assume !!(~v71~3 <= ~v40~3);" "41017assume !!(0 <= ~v43~3);call #t~ret102 :=..." "43168assume !(0 <= ~v38~3);" "43170assume !(~v73~3 <= 0);" "43172assume !(0 <= ~v73~3);" "43174assume !(~v72~3 <= 0);" "40885call #t~ret101 := nondet_bool();havoc ~a..." "42109assume !!(1 <= ~v61~3);" "43176assume !(0 <= ~v72~3);" "42111assume !!(2 <= ~v61~3);" "43178assume !(~v77~3 <= 0);" "43180assume !(0 <= ~v77~3);" "42107~v66~3 := #t~ret93;havoc #t~ret93;~v59~3..." "42106assume !!(~v75~3 <= ~v80~3);call #t~ret8..." "43182assume !(~v46~3 <= ~v43~3);" "40771assume !(~v79~3 <= ~v72~3);" "39695havoc ~a~2;#res := ~a~2;assume true;" "42121assume !(0 <= ~v36~3);" "40769assume !(~v72~3 <= ~v75~3);" "39692assume true;" "40775assume !(~v73~3 <= ~v72~3);" "42126assume !(-1 + ~v44~3 <= ~v35~3);" "40773assume !(~v72~3 <= ~v79~3);" "42124assume !!(-1 + ~v44~3 <= ~v35~3);assume ..." "40779assume !(~v61~3 <= 1);" "42115assume !(1 <= ~v61~3);" "40777assume !(~v72~3 <= ~v73~3);" "42113assume !(2 <= ~v61~3);" "42119assume !(~v80~3 <= ~v75~3);" "40783assume !(~v80~3 <= 0);" "42117assume !(~v75~3 <= ~v80~3);" "40781assume !(1 <= ~v61~3);" "39710assume true;" "40787assume !(~v38~3 <= 0);" "40785assume !(0 <= ~v80~3);" "39709call ULTIMATE.init();assume true;Return ..." "42142assume !(#t~ret186 != 0);havoc #t~ret186..." "40791assume !(~v77~3 <= 0);" "42140assume #t~ret186 != 0;havoc #t~ret186;~v..." "40789assume !(0 <= ~v38~3);" "40795assume !(~v61~3 <= 1);" "42131assume !(1 <= ~v61~3);" "42129assume !!(1 <= ~v61~3);assume !(2 <= ~v6..." "40793assume !(0 <= ~v77~3);" "40799assume !(#t~ret227 != 0);havoc #t~ret227..." "41176assume !!(0 <= ~v31~3);call #t~ret390 :=..." "40797assume !(1 <= ~v61~3);" "42133assume !(#t~ret188 != 0);havoc #t~ret188..." "40801assume !(~v34~3 <= ~v72~3);" "42152assume !(~v38~3 <= ~v80~3);" "43132assume !(~v75~3 <= ~v80~3);" "42155assume !!(~v73~3 <= ~v79~3);assume !(~v7..." "40803assume !(~v72~3 <= ~v34~3);" "43134assume !(~v80~3 <= ~v75~3);" "42157assume !(~v73~3 <= ~v79~3);" "40805assume !(~v61~3 <= 1);" "43128assume !!(~v61~3 <= 0);" "40807assume !(1 <= ~v61~3);" "43130assume !(~v61~3 <= 0);" "42145assume !!(~v35~3 <= ~v36~3);assume !(~v3..." "43125assume !!(~v75~3 <= ~v80~3);call #t~ret3..." "40809assume !(~v63~3 <= 0);" "42147assume !(~v35~3 <= ~v36~3);" "40811assume !(0 <= ~v63~3);" "43126~v66~3 := #t~ret335;havoc #t~ret335;~v59..." "40813assume !(~v77~3 <= 0);" "40815assume !(0 <= ~v77~3);" "42150assume !!(~v38~3 <= ~v80~3);assume !(~v8..." "40817assume !(#t~ret214 != 0);havoc #t~ret214..." "42170assume !!(~v72~3 <= ~v73~3);assume !(~v7..." "40819assume !(#t~ret213 != 0);havoc #t~ret213..." "42172assume !(~v72~3 <= ~v73~3);" "40821assume !(~v46~3 <= ~v43~3);" "42175assume !!(0 <= -1 * ~v35~3 + ~v36~3);ass..." "42160assume !!(~v72~3 <= ~v66~3);assume !(~v6..." "42162assume !(~v72~3 <= ~v66~3);" "40827assume !(#t~ret194 != 0);havoc #t~ret194..." "42165assume !!(~v72~3 <= ~v79~3);assume !(~v7..." "42167assume !(~v72~3 <= ~v79~3);" "40711assume !(~v80~3 <= ~v38~3);" "43034assume !!(0 <= ~v79~3);" "40709assume !(#t~ret258 != 0);havoc #t~ret258..." "43032assume !!(~v38~3 <= 0);" "40707assume !(#t~ret259 != 0);havoc #t~ret259..." "42187assume !(0 <= ~v38~3);" "41094assume !!(~v72~3 <= ~v34~3);assume !!(~v..." "43038assume !!(0 <= ~v80~3);" "40705assume !(1 <= ~v61~3);" "42185assume !!(0 <= ~v38~3);assume !(~v38~3 <..." "43036assume !!(~v79~3 <= 0);" "40719assume !(~v66~3 <= ~v72~3);" "43026assume !!(0 <= ~v73~3);" "42182assume !(0 <= ~v80~3);" "40717assume !(~v73~3 <= ~v79~3);" "43024assume !!(~v72~3 <= 0);" "42180assume !!(0 <= ~v80~3);assume !(~v80~3 <..." "40715assume !(~v79~3 <= ~v73~3);" "43030assume !!(0 <= ~v38~3);" "41101assume #t~ret288 != 0;havoc #t~ret288;~v..." "42177assume !(0 <= -1 * ~v35~3 + ~v36~3);" "40713assume !(~v38~3 <= ~v80~3);" "43028assume !!(~v73~3 <= 0);" "42206assume !(1 <= ~v61~3);" "40727assume !(~v73~3 <= ~v72~3);" "42204assume !!(1 <= ~v61~3);assume !(2 <= ~v6..." "40725assume !(~v72~3 <= ~v79~3);" "43022assume !!(0 <= ~v72~3);" "41111assume !!(1 <= ~v61~3);assume !!(2 <= ~v..." "40723assume !(~v79~3 <= ~v72~3);" "41108assume #t~ret288 != 0;havoc #t~ret288;~v..." "43020assume !!(~v77~3 <= 0);call #t~ret304 :=..." "42201assume !(#t~ret177 != 0);havoc #t~ret177..." "40721assume !(~v72~3 <= ~v66~3);" "42199assume #t~ret177 != 0;havoc #t~ret177;as..." "40735assume !(~v75~3 <= 0);" "42196assume !(#t~ret183 != 0);havoc #t~ret183..." "40733assume !(1 <= ~v61~3);" "42194assume #t~ret183 != 0;havoc #t~ret183;~v..." "40731assume !(~v61~3 <= 1);" "40729assume !(~v72~3 <= ~v73~3);" "42221assume !!(~v73~3 <= ~v79~3);assume !(~v7..." "40741assume !(0 <= ~v80~3);" "42223assume !(~v73~3 <= ~v79~3);" "43067assume !!(~v61~3 <= 0);call #t~ret324 :=..." "41123assume !!(~v61~3 <= ~v42~3);call #t~ret3..." "40743assume !(~v38~3 <= 0);" "40737assume !(0 <= ~v75~3);" "43069assume !!(~v80~3 <= ~v75~3);" "42216assume !!(~v38~3 <= ~v80~3);assume !(~v8..." "40739assume !(~v80~3 <= 0);" "42218assume !(~v38~3 <= ~v80~3);" "42213assume !(~v79~3 <= ~v75~3);" "40749assume !(~v61~3 <= 1);" "43056assume !!(~v80~3 <= ~v38~3);" "40751assume !(1 <= ~v61~3);" "43058assume !!(~v79~3 <= ~v75~3);" "40745assume !(0 <= ~v38~3);" "42208assume !(#t~ret340 != 0);havoc #t~ret340..." "43060assume !!(~v75~3 <= ~v79~3);" "41135assume !!(~v61~3 <= ~v42~3);call #t~ret3..." "40747assume !(#t~ret256 != 0);havoc #t~ret256..." "42211assume !!(~v79~3 <= ~v75~3);assume !(~v7..." "42236assume !!(~v72~3 <= ~v73~3);assume !(~v7..." "43048assume !!(~v73~3 <= ~v72~3);" "40757assume !(~v79~3 <= ~v75~3);" "42238assume !(~v72~3 <= ~v73~3);" "43050assume !!(~v73~3 <= ~v79~3);" "40759assume !(~v80~3 <= ~v38~3);" "43052assume !!(~v79~3 <= ~v73~3);" "40753assume !(#t~ret249 != 0);havoc #t~ret249..." "42233assume !(~v72~3 <= ~v79~3);" "43054assume !!(~v38~3 <= ~v80~3);" "40755assume !(~v75~3 <= ~v79~3);" "42228assume !(~v72~3 <= ~v75~3);" "43040assume !!(~v80~3 <= 0);" "40765assume !(~v73~3 <= ~v79~3);" "43042assume !!(0 <= ~v75~3);" "42231assume !!(~v72~3 <= ~v79~3);assume !(~v7..." "40767assume !(~v75~3 <= ~v72~3);" "43044assume !!(~v75~3 <= 0);" "40761assume !(~v38~3 <= ~v80~3);" "42226assume !!(~v72~3 <= ~v75~3);assume !(~v7..." "43046assume !!(~v72~3 <= ~v73~3);" "40763assume !(~v79~3 <= ~v73~3);" }, returnAlphabet = {"40362return call #t~ret428 := main();" "39691return call #t~ret168 := nondet();" "39690return call #t~ret167 := nondet();" "39689return call #t~ret166 := nondet();" "39688return call #t~ret165 := nondet();" "39687return call #t~ret164 := nondet();" "39686return call #t~ret162 := nondet();" "39685return call #t~ret161 := nondet();" "39684return call #t~ret160 := nondet();" "39683return call #t~ret159 := nondet();" "39682return call #t~ret158 := nondet();" "39681return call #t~ret157 := nondet();" "39680return call #t~ret156 := nondet();" "39704return call #t~ret175 := nondet_bool();" "39705return call #t~ret176 := nondet_bool();" "39702return call #t~ret173 := nondet_bool();" "39703return call #t~ret174 := nondet_bool();" "39700return call #t~ret171 := nondet_bool();" "39701return call #t~ret172 := nondet_bool();" "39698return call #t~ret169 := nondet_bool();" "39699return call #t~ret170 := nondet_bool();" "39696return call #t~ret149 := nondet_bool();" "39697return call #t~ret163 := nondet_bool();" "39675return call #t~ret151 := nondet();" "39674return call #t~ret150 := nondet();" "39679return call #t~ret155 := nondet();" "39678return call #t~ret154 := nondet();" "39677return call #t~ret153 := nondet();" "39676return call #t~ret152 := nondet();" }, states = {"14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))" "15201#(and (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "14783#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "12428#unseeded" "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "12434#(or unseeded (and (> oldRank (+ main_~v36~3 (- 3))) (>= oldRank 0)))" "14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "14365#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))) (<= main_~v37~3 (+ oldRank 2)))" "15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))" }, initialStates = {"12428#unseeded" }, finalStates = {"12434#(or unseeded (and (> oldRank (+ main_~v36~3 (- 3))) (>= oldRank 0)))" }, callTransitions = { ("12428#unseeded" "39711call #t~ret428 := main();" "12428#unseeded") }, internalTransitions = { ("14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))" "41863assume !!(~v38~3 <= 0);assume !!(0 <= ~v..." "14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))") ("14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))" "41878assume !!(~v80~3 <= ~v38~3);assume !!(~v..." "14783#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))" "41872assume !!(~v79~3 <= ~v72~3);assume !!(~v..." "14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))") ("14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))" "41875assume !!(~v79~3 <= ~v73~3);assume !!(~v..." "14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))") ("14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))" "41869assume !!(~v73~3 <= ~v72~3);assume !!(~v..." "14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))") ("14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))" "41866assume !!(~v80~3 <= 0);assume !!(~v72~3 ..." "14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))") ("15201#(and (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41911assume !!(2 <= ~v61~3);call #t~ret426 :=..." "15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("15201#(and (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41889assume !!(-1 + ~v36~3 <= ~v37~3);call #t..." "15201#(and (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("15201#(and (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41903assume #t~ret425 != 0;havoc #t~ret425;as..." "15201#(and (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("15201#(and (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41900assume #t~ret423 != 0;havoc #t~ret423;~v..." "15201#(and (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41801call #t~ret81 := nondet_bool();havoc ~a~..." "15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41925assume !!(~v37~3 <= ~v36~3);call #t~ret4..." "15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41807assume !(#t~ret81 != 0);havoc #t~ret81;c..." "15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41852assume !!(0 <= ~v36~3);call #t~ret95 := ..." "12434#(or unseeded (and (> oldRank (+ main_~v36~3 (- 3))) (>= oldRank 0)))") ("15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41811assume #t~ret94 != 0;havoc #t~ret94;" "15307#(and (<= main_~v36~3 oldRank) (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14783#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41911assume !!(2 <= ~v61~3);call #t~ret426 :=..." "14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14783#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41889assume !!(-1 + ~v36~3 <= ~v37~3);call #t..." "14783#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14783#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41903assume #t~ret425 != 0;havoc #t~ret425;as..." "14783#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14783#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41900assume #t~ret423 != 0;havoc #t~ret423;~v..." "14783#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("12428#unseeded" "40191assume !!(~v71~3 <= ~v60~3);assume !!(1 ..." "12428#unseeded") ("12428#unseeded" "40184assume !!(~v71~3 <= ~v40~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41852assume !!(0 <= ~v36~3);call #t~ret95 := ..." "12428#unseeded") ("12428#unseeded" "40181assume !!(~v60~3 <= ~v40~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "40896call #t~ret101 := nondet_bool();havoc ~a..." "12428#unseeded") ("12428#unseeded" "40178assume !!(~v46~3 <= ~v61~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41293assume !!(1 <= ~v61~3);assume !!(2 <= ~v..." "12428#unseeded") ("12428#unseeded" "40175assume !!(~v43~3 <= 1);assume !!(~v61~3 ..." "12428#unseeded") ("12428#unseeded" "40172assume !!(1 + ~v43~3 <= ~v46~3);~v71~3 :..." "12428#unseeded") ("12428#unseeded" "40920assume !!(~v41~3 <= -1 + ~v43~3);assume ..." "12428#unseeded") ("12428#unseeded" "41290assume #t~ret417 != 0;havoc #t~ret417;~v..." "12428#unseeded") ("12428#unseeded" "40914assume !!(0 <= ~v43~3);call #t~ret117 :=..." "12428#unseeded") ("12428#unseeded" "40164assume #t~ret336 != 0;havoc #t~ret336;ca..." "12428#unseeded") ("12428#unseeded" "40917assume !!(~v43~3 <= 1 + ~v41~3);assume !..." "12428#unseeded") ("12428#unseeded" "42503assume !!(0 <= ~v31~3);assume !!(0 <= ~v..." "12428#unseeded") ("12428#unseeded" "42500assume !!(~v61~3 <= ~v42~3);call #t~ret3..." "12428#unseeded") ("12428#unseeded" "40940call #t~ret101 := nondet_bool();havoc ~a..." "12428#unseeded") ("12428#unseeded" "40152assume !(#t~ret291 != 0);havoc #t~ret291..." "12428#unseeded") ("12428#unseeded" "41811assume #t~ret94 != 0;havoc #t~ret94;" "12428#unseeded") ("12428#unseeded" "40934assume !!(1 + ~v41~3 <= ~v46~3);call #t~..." "12428#unseeded") ("12428#unseeded" "40146assume !!(~v46~3 <= ~v61~3);call #t~ret2..." "12428#unseeded") ("12428#unseeded" "40140assume !!(~v40~3 <= 0);assume !!(~v61~3 ..." "12428#unseeded") ("12428#unseeded" "41801call #t~ret81 := nondet_bool();havoc ~a~..." "12428#unseeded") ("12428#unseeded" "41084assume #t~ret274 != 0;havoc #t~ret274;~v..." "12428#unseeded") ("12428#unseeded" "41087assume !!(0 <= ~v63~3);assume !!(~v63~3 ..." "12428#unseeded") ("12428#unseeded" "40137assume !!(~v43~3 <= 0);assume !!(0 <= ~v..." "12428#unseeded") ("12428#unseeded" "41807assume !(#t~ret81 != 0);havoc #t~ret81;c..." "12428#unseeded") ("12428#unseeded" "41793assume !!(1 <= ~v61~3);assume !!(2 <= ~v..." "12428#unseeded") ("12428#unseeded" "40134assume #t~ret191 != 0;havoc #t~ret191;ca..." "12428#unseeded") ("12428#unseeded" "41796assume !!(-1 + ~v44~3 <= ~v35~3);assume ..." "12428#unseeded") ("12428#unseeded" "41796assume !!(-1 + ~v44~3 <= ~v35~3);assume ..." "12434#(or unseeded (and (> oldRank (+ main_~v36~3 (- 3))) (>= oldRank 0)))") ("12428#unseeded" "41315call #t~ret120 := nondet_bool();havoc ~a..." "12428#unseeded") ("12428#unseeded" "40844assume #t~ret208 != 0;havoc #t~ret208;ca..." "12428#unseeded") ("12428#unseeded" "40121call #t~ret0 := nondet();havoc ~a~1;#res..." "12428#unseeded") ("12428#unseeded" "41785assume #t~ret188 != 0;havoc #t~ret188;~v..." "12428#unseeded") ("12428#unseeded" "41506assume !!(~v33~3 <= ~v32~3);call #t~ret3..." "12428#unseeded") ("12428#unseeded" "42606assume !!(~v77~3 <= 0);assume !!(0 <= ~v..." "12428#unseeded") ("12428#unseeded" "40863assume !!(~v60~3 <= ~v40~3);" "12428#unseeded") ("12428#unseeded" "42609assume !!(0 <= ~v38~3);assume !!(~v38~3 ..." "12428#unseeded") ("12428#unseeded" "41532assume !!(0 <= ~v77~3);assume !!(~v77~3 ..." "12428#unseeded") ("12428#unseeded" "40861assume !!(~v40~3 <= ~v60~3);" "12428#unseeded") ("12428#unseeded" "41529assume !!(0 <= ~v44~3);assume !!(0 <= ~v..." "12428#unseeded") ("12428#unseeded" "40859assume !!(~v46~3 <= ~v61~3);" "12428#unseeded") ("12428#unseeded" "42612assume !!(0 <= ~v80~3);assume !!(~v80~3 ..." "12428#unseeded") ("12428#unseeded" "41771assume #t~ret186 != 0;havoc #t~ret186;~v..." "12428#unseeded") ("12428#unseeded" "42615assume !!(1 <= ~v44~3);assume !!(~v44~3 ..." "12428#unseeded") ("12428#unseeded" "40857assume !!(~v61~3 <= ~v46~3);" "12428#unseeded") ("12428#unseeded" "40855assume !!(~v43~3 <= 2);" "12428#unseeded") ("12428#unseeded" "40853assume !!(2 <= ~v43~3);" "12428#unseeded") ("12428#unseeded" "42618assume !!(~v72~3 <= ~v73~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41526call #t~ret120 := nondet_bool();havoc ~a..." "12428#unseeded") ("12428#unseeded" "40851assume !!(1 + ~v43~3 <= ~v46~3);~v71~3 :..." "12428#unseeded") ("12428#unseeded" "42621assume !!(~v72~3 <= ~v79~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41520assume !!(~v45~3 <= ~v44~3);call #t~ret3..." "12428#unseeded") ("12428#unseeded" "41760assume !!(~v35~3 <= ~v36~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41487assume #t~ret362 != 0;havoc #t~ret362;~v..." "12428#unseeded") ("12428#unseeded" "41753assume !!(~v38~3 <= ~v80~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "40874assume !!(1 <= ~v46~3);assume !!(2 <= ~v..." "12428#unseeded") ("12428#unseeded" "41276assume !!(~v34~3 <= ~v72~3);call #t~ret4..." "12428#unseeded") ("12428#unseeded" "40869assume !!(~v60~3 <= ~v71~3);" "12428#unseeded") ("12428#unseeded" "41265assume !!(~v63~3 <= 0);assume !!(~v72~3 ..." "12428#unseeded") ("12428#unseeded" "41476assume !!(~v33~3 <= -1 + ~v32~3);assume ..." "12428#unseeded") ("12428#unseeded" "41750assume !!(~v73~3 <= ~v79~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "40871assume !!(~v71~3 <= ~v60~3);" "12428#unseeded") ("12428#unseeded" "40865assume !!(~v40~3 <= ~v71~3);" "12428#unseeded") ("12428#unseeded" "41744assume !!(~v72~3 <= ~v79~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41747assume !!(~v72~3 <= ~v66~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "40867assume !!(~v71~3 <= ~v40~3);" "12428#unseeded") ("12428#unseeded" "41017assume !!(0 <= ~v43~3);call #t~ret102 :=..." "12428#unseeded") ("12428#unseeded" "41259assume #t~ret399 != 0;havoc #t~ret399;ca..." "12428#unseeded") ("12428#unseeded" "41741assume !!(~v72~3 <= ~v73~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41262assume !!(~v64~3 <= 0);assume !!(0 <= ~v..." "12428#unseeded") ("12428#unseeded" "41498assume !!(2 <= ~v61~3);call #t~ret365 :=..." "12428#unseeded") ("12428#unseeded" "41738assume !!(0 <= -1 * ~v35~3 + ~v36~3);ass..." "12428#unseeded") ("12428#unseeded" "41732assume !!(0 <= ~v38~3);assume !!(~v38~3 ..." "12428#unseeded") ("12428#unseeded" "41735assume !!(0 <= ~v80~3);assume !!(~v80~3 ..." "12428#unseeded") ("12428#unseeded" "41729assume #t~ret183 != 0;havoc #t~ret183;~v..." "12428#unseeded") ("12428#unseeded" "41490assume #t~ret364 != 0;havoc #t~ret364;as..." "12428#unseeded") ("12428#unseeded" "39709call ULTIMATE.init();assume true;Return ..." "12428#unseeded") ("12428#unseeded" "41717assume #t~ret177 != 0;havoc #t~ret177;as..." "12428#unseeded") ("12428#unseeded" "41176assume !!(0 <= ~v31~3);call #t~ret390 :=..." "12428#unseeded") ("12428#unseeded" "41463assume !!(1 <= -1 * ~v44~3 + ~v45~3);ass..." "12428#unseeded") ("12428#unseeded" "42637assume !!(~v79~3 <= ~v75~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41460assume !!(0 <= ~v63~3);assume !!(~v63~3 ..." "12428#unseeded") ("12428#unseeded" "41457assume !!(0 <= ~v64~3);assume !!(~v64~3 ..." "12428#unseeded") ("12428#unseeded" "42630assume !!(~v38~3 <= ~v80~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41469assume !!(~v77~3 <= ~v47~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "42627assume !!(~v73~3 <= ~v79~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41466assume !!(~v72~3 <= ~v34~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41677assume #t~ret340 != 0;havoc #t~ret340;~v..." "12428#unseeded") ("12428#unseeded" "42624assume !!(~v72~3 <= ~v75~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "42654assume !!(1 <= ~v61~3);assume !!(2 <= ~v..." "12428#unseeded") ("12428#unseeded" "41680assume !!(1 <= ~v61~3);assume !!(2 <= ~v..." "12428#unseeded") ("12428#unseeded" "41925assume !!(~v37~3 <= ~v36~3);call #t~ret4..." "12428#unseeded") ("12428#unseeded" "42651assume #t~ret396 != 0;havoc #t~ret396;~v..." "12428#unseeded") ("12428#unseeded" "41685call #t~ret177 := nondet_bool();havoc ~a..." "12428#unseeded") ("12428#unseeded" "41454assume #t~ret342 != 0;havoc #t~ret342;~v..." "12428#unseeded") ("12428#unseeded" "40827assume !(#t~ret194 != 0);havoc #t~ret194..." "12428#unseeded") ("12428#unseeded" "41911assume !!(2 <= ~v61~3);call #t~ret426 :=..." "12428#unseeded") ("12428#unseeded" "41638assume !!(0 <= ~v38~3);assume !!(~v38~3 ..." "12428#unseeded") ("12428#unseeded" "41094assume !!(~v72~3 <= ~v34~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41635assume !!(0 <= ~v44~3);assume !!(0 <= ~v..." "12428#unseeded") ("12428#unseeded" "41644assume !!(~v72~3 <= ~v73~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41647assume !!(~v72~3 <= ~v79~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41641assume !!(0 <= ~v80~3);assume !!(~v80~3 ..." "12428#unseeded") ("12428#unseeded" "41653assume !!(~v73~3 <= ~v79~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41111assume !!(1 <= ~v61~3);assume !!(2 <= ~v..." "12428#unseeded") ("12428#unseeded" "41650assume !!(~v72~3 <= ~v75~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41108assume #t~ret288 != 0;havoc #t~ret288;~v..." "12428#unseeded") ("12428#unseeded" "41889assume !!(-1 + ~v36~3 <= ~v37~3);call #t..." "12428#unseeded") ("12428#unseeded" "41903assume #t~ret425 != 0;havoc #t~ret425;as..." "12428#unseeded") ("12428#unseeded" "41663assume !!(~v79~3 <= ~v75~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41900assume #t~ret423 != 0;havoc #t~ret423;~v..." "12428#unseeded") ("12428#unseeded" "41656assume !!(~v38~3 <= ~v80~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41357assume !!(0 <= ~v44~3);assume !!(0 <= ~v..." "12428#unseeded") ("12428#unseeded" "41878assume !!(~v80~3 <= ~v38~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41872assume !!(~v79~3 <= ~v72~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41875assume !!(~v79~3 <= ~v73~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41135assume !!(~v61~3 <= ~v42~3);call #t~ret3..." "12428#unseeded") ("12428#unseeded" "41860assume #t~ret420 != 0;havoc #t~ret420;~v..." "12428#unseeded") ("12428#unseeded" "41863assume !!(~v38~3 <= 0);assume !!(0 <= ~v..." "12428#unseeded") ("12428#unseeded" "41869assume !!(~v73~3 <= ~v72~3);assume !!(~v..." "12428#unseeded") ("12428#unseeded" "41866assume !!(~v80~3 <= 0);assume !!(~v72~3 ..." "12428#unseeded") ("14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "41860assume #t~ret420 != 0;havoc #t~ret420;~v..." "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "41863assume !!(~v38~3 <= 0);assume !!(0 <= ~v..." "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "41878assume !!(~v80~3 <= ~v38~3);assume !!(~v..." "14365#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))) (<= main_~v37~3 (+ oldRank 2)))") ("14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "41872assume !!(~v79~3 <= ~v72~3);assume !!(~v..." "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "41807assume !(#t~ret81 != 0);havoc #t~ret81;c..." "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "41852assume !!(0 <= ~v36~3);call #t~ret95 := ..." "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "41875assume !!(~v79~3 <= ~v73~3);assume !!(~v..." "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "41869assume !!(~v73~3 <= ~v72~3);assume !!(~v..." "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "41811assume #t~ret94 != 0;havoc #t~ret94;" "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))" "41866assume !!(~v80~3 <= 0);assume !!(~v72~3 ..." "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("12434#(or unseeded (and (> oldRank (+ main_~v36~3 (- 3))) (>= oldRank 0)))" "41801call #t~ret81 := nondet_bool();havoc ~a~..." "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("12434#(or unseeded (and (> oldRank (+ main_~v36~3 (- 3))) (>= oldRank 0)))" "41860assume #t~ret420 != 0;havoc #t~ret420;~v..." "14073#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))))") ("14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41801call #t~ret81 := nondet_bool();havoc ~a~..." "14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41860assume #t~ret420 != 0;havoc #t~ret420;~v..." "15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))") ("14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41925assume !!(~v37~3 <= ~v36~3);call #t~ret4..." "14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41807assume !(#t~ret81 != 0);havoc #t~ret81;c..." "14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41852assume !!(0 <= ~v36~3);call #t~ret95 := ..." "14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41811assume #t~ret94 != 0;havoc #t~ret94;" "14889#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41801call #t~ret81 := nondet_bool();havoc ~a~..." "14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41860assume #t~ret420 != 0;havoc #t~ret420;~v..." "14627#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)))") ("14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41925assume !!(~v37~3 <= ~v36~3);call #t~ret4..." "14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41807assume !(#t~ret81 != 0);havoc #t~ret81;c..." "14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41852assume !!(0 <= ~v36~3);call #t~ret95 := ..." "14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))" "41811assume #t~ret94 != 0;havoc #t~ret94;" "14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))" "41863assume !!(~v38~3 <= 0);assume !!(0 <= ~v..." "15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))") ("15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))" "41878assume !!(~v80~3 <= ~v38~3);assume !!(~v..." "15201#(and (<= main_~v37~3 oldRank) (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v37~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))" "41872assume !!(~v79~3 <= ~v72~3);assume !!(~v..." "15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))") ("15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))" "41875assume !!(~v79~3 <= ~v73~3);assume !!(~v..." "15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))") ("15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))" "41869assume !!(~v73~3 <= ~v72~3);assume !!(~v..." "15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))") ("15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))" "41866assume !!(~v80~3 <= 0);assume !!(~v72~3 ..." "15045#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 1)) (<= main_~v36~3 (+ oldRank 2)))") ("14365#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))) (<= main_~v37~3 (+ oldRank 2)))" "41911assume !!(2 <= ~v61~3);call #t~ret426 :=..." "14471#(and (<= main_~v36~3 (+ oldRank 3)) (<= main_~v36~3 (+ oldRank 2)) (<= main_~v37~3 (+ oldRank 2)))") ("14365#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))) (<= main_~v37~3 (+ oldRank 2)))" "41889assume !!(-1 + ~v36~3 <= ~v37~3);call #t..." "14365#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))) (<= main_~v37~3 (+ oldRank 2)))") ("14365#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))) (<= main_~v37~3 (+ oldRank 2)))" "41903assume #t~ret425 != 0;havoc #t~ret425;as..." "14365#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))) (<= main_~v37~3 (+ oldRank 2)))") ("14365#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))) (<= main_~v37~3 (+ oldRank 2)))" "41900assume #t~ret423 != 0;havoc #t~ret423;~v..." "14365#(and (<= main_~v36~3 (+ oldRank 3)) (= oldRank (+ main_~v36~3 (- 3))) (<= main_~v37~3 (+ oldRank 2)))") }, returnTransitions = { } );