// Testfile dumped by Ultimate at 2013/11/09 20:29:53 print(numberOfStates(nwa)); NestedWordAutomaton complement = buchiComplementFKV(nwa); print(numberOfStates(complement)); assert(numberOfStates(complement) == 41); // with MatthiasTightLevelRankingStateGenerator result was 41 and minimizeSevpa reduced it to 29 NestedWordAutomaton live = removeNonLiveStates(complement); print(numberOfStates(live)); assert(numberOfStates(live) == 41); minimizeSevpa(complement); NestedWordAutomaton nwa = ( callAlphabet = {"34422call #t~ret185 := main();" }, internalAlphabet = {"35200assume !!(~v18~3 <= ~v38~3);assume !!(~v..." "35207assume !!(~v14~3 <= ~v15~3);assume !!(~v..." "35745assume !!(~v20~3 <= -1 + ~v21~3);assume ..." "35759assume !!(1 + ~v20~3 <= ~v22~3);call #t~..." "35752assume !!(1 + ~v20~3 <= ~v22~3);call #t~..." "35764assume !!(~v20~3 <= -1 + ~v21~3);assume ..." "35218assume #t~ret158 != 0;havoc #t~ret158;~v..." "35766assume !(~v20~3 <= -1 + ~v21~3);" "35761assume !(1 + ~v20~3 <= ~v22~3);" "35221assume #t~ret160 != 0;havoc #t~ret160;as..." "35769assume !!(~v21~3 <= 1 + ~v20~3);assume !..." "35771assume !(~v21~3 <= 1 + ~v20~3);" "35229assume !!(2 <= ~v22~3);assume !!(~v22~3 ..." "34643assume true;" "34642assume !(#t~ret176 != 0);havoc #t~ret176..." "35232assume !!(-1 + ~v21~3 <= ~v14~3);assume ..." "34640assume !(#t~ret163 != 0);havoc #t~ret163..." "35237call #t~ret39 := nondet_bool();havoc ~a~..." "34646assume #t~ret176 != 0;havoc #t~ret176;" "35243assume !(#t~ret39 != 0);havoc #t~ret39;c..." "35245assume !(#t~ret52 != 0);havoc #t~ret52;" "35247assume #t~ret52 != 0;havoc #t~ret52;" "34625assume #t~ret110 != 0;havoc #t~ret110;~v..." "34628assume !!(~v21~3 <= 0);assume !!(0 <= ~v..." "34634assume !!(~v33~3 <= 0);call #t~ret163 :=..." "35742assume !!(~v21~3 <= 1 + ~v20~3);assume !..." "35739assume !!(0 <= ~v21~3);call #t~ret70 := ..." "35808assume !(~v32~3 <= ~v33~3);" "35811assume !!(~v21~3 <= 1);assume !(~v33~3 <..." "35813assume !(~v21~3 <= 1);" "36236call #t~ret0 := nondet();havoc ~a~1;#res..." "34622call #t~ret0 := nondet();havoc ~a~1;#res..." "35298assume !!(0 <= ~v15~3);call #t~ret53 := ..." "35309assume !!(~v18~3 <= 0);assume !!(0 <= ~v..." "35786assume !(0 <= ~v21~3);" "35784assume !!(0 <= ~v21~3);call #t~ret70 := ..." "35791assume !(1 <= ~v22~3);" "35789assume !!(1 <= ~v22~3);assume !(2 <= ~v2..." "35306assume #t~ret148 != 0;havoc #t~ret148;~v..." "35795assume !(~v33~3 <= ~v32~3);" "35318assume !!(~v37~3 <= ~v33~3);assume !!(~v..." "35793assume !(~v32~3 <= ~v33~3);" "35312assume !!(~v38~3 <= 0);assume !!(~v33~3 ..." "35799assume !(2 <= ~v21~3);" "35797assume !(~v21~3 <= 2);" "35315assume !!(~v34~3 <= ~v33~3);assume !!(~v..." "35324assume !!(~v37~3 <= ~v34~3);assume !!(~v..." "35803assume !(#t~ret120 != 0);havoc #t~ret120..." "35801assume !(1 + ~v21~3 <= ~v22~3);" "35327assume !!(~v38~3 <= ~v18~3);assume !!(~v..." "35806assume !!(~v32~3 <= ~v33~3);assume !(1 <..." "35321assume !!(~v32~3 <= ~v33~3);assume !!(~v..." "35628assume !!(~v33~3 <= ~v28~3);assume !(~v2..." "34809assume !!(~v18~3 <= 0);" "35630assume !(~v33~3 <= ~v28~3);" "34811assume !!(0 <= ~v38~3);" "35625assume !(~v33~3 <= ~v32~3);" "34813assume !!(~v38~3 <= 0);" "34815assume !!(0 <= ~v35~3);" "35620assume !(~v34~3 <= ~v37~3);" "34801assume #t~ret130 != 0;havoc #t~ret130;~v..." "34803assume !(#t~ret131 != 0);havoc #t~ret131..." "35623assume !!(~v33~3 <= ~v32~3);assume !(~v3..." "34805assume #t~ret131 != 0;havoc #t~ret131;~v..." "35618assume !!(~v34~3 <= ~v37~3);assume !(~v3..." "34807assume !!(0 <= ~v18~3);" "35645assume !(0 <= -1 * ~v14~3 + ~v15~3);" "34795assume !!(~v22~3 <= ~v21~3);call #t~ret1..." "35640assume !(~v33~3 <= ~v34~3);" "35102assume !!(2 <= ~v21~3);" "35643assume !!(0 <= -1 * ~v14~3 + ~v15~3);ass..." "35100assume !!(1 + ~v21~3 <= ~v22~3);~v17~3 :..." "35638assume !!(~v33~3 <= ~v34~3);assume !(~v3..." "35633assume !!(~v33~3 <= ~v37~3);assume !(~v3..." "35635assume !(~v33~3 <= ~v37~3);" "35596assume !(#t~ret160 != 0);havoc #t~ret160..." "35594assume #t~ret160 != 0;havoc #t~ret160;as..." "35116call #t~ret61 := nondet_bool();havoc ~a~..." "35119assume #t~ret61 != 0;havoc #t~ret61;assu..." "35104assume !!(~v21~3 <= 2);" "35591assume !(2 <= ~v22~3);" "35106assume !!(~v33~3 <= ~v32~3);" "35589assume !!(2 <= ~v22~3);assume !(~v22~3 <..." "35108assume !!(~v32~3 <= ~v33~3);" "35586assume !(-1 + ~v21~3 <= ~v14~3);" "35584assume !!(-1 + ~v21~3 <= ~v14~3);assume ..." "35111assume !!(1 <= ~v22~3);assume !!(2 <= ~v..." "35615assume !(~v18~3 <= ~v38~3);" "35613assume !!(~v18~3 <= ~v38~3);assume !(~v3..." "35610assume !(~v14~3 <= ~v15~3);" "35608assume !!(~v14~3 <= ~v15~3);assume !(~v1..." "34754assume !!(1 <= ~v22~3);" "35605assume !(#t~ret158 != 0);havoc #t~ret158..." "34752assume !!(~v35~3 <= ~v37~3);" "35603assume #t~ret158 != 0;havoc #t~ret158;~v..." "34748assume !!(~v38~3 <= ~v18~3);" "34750assume !!(~v37~3 <= ~v35~3);" "34744assume !!(~v37~3 <= ~v34~3);" "34746assume !!(~v18~3 <= ~v38~3);" "34740assume !!(~v32~3 <= ~v33~3);" "34742assume !!(~v34~3 <= ~v37~3);" "34736assume !!(~v35~3 <= ~v33~3);" "35686assume !(#t~ret61 != 0);havoc #t~ret61;c..." "34738assume !!(~v33~3 <= ~v32~3);" "34732assume !!(~v37~3 <= ~v33~3);" "34734assume !!(~v33~3 <= ~v35~3);" "34728assume !!(~v34~3 <= ~v33~3);" "35161assume !!(~v22~3 <= ~v21~3);~v34~3 := ~v..." "34730assume !!(~v33~3 <= ~v37~3);" "34724assume !!(~v22~3 <= 1);" "34726assume !!(~v33~3 <= ~v34~3);" "34720assume !!(~v21~3 <= 1);" "34722assume !!(1 <= ~v22~3);" "34718assume !!(1 <= ~v21~3);" "35182assume !!(0 <= -1 * ~v14~3 + ~v15~3);ass..." "34716assume !!(~v38~3 <= 0);" "35662assume #t~ret155 != 0;havoc #t~ret155;~v..." "35176assume !!(0 <= ~v18~3);assume !!(~v18~3 ..." "34714assume !!(0 <= ~v38~3);" "34712assume !!(~v18~3 <= 0);" "35179assume !!(0 <= ~v38~3);assume !!(~v38~3 ..." "35650assume !(0 <= ~v38~3);" "34710assume !!(0 <= ~v18~3);" "35173assume #t~ret155 != 0;havoc #t~ret155;~v..." "35648assume !!(0 <= ~v38~3);assume !(~v38~3 <..." "34708assume !!(~v22~3 <= ~v21~3);~v34~3 := ~v..." "34706assume #t~ret111 != 0;havoc #t~ret111;ca..." "35655assume !(0 <= ~v18~3);" "35653assume !!(0 <= ~v18~3);assume !(~v18~3 <..." "35197assume !!(~v34~3 <= ~v37~3);assume !!(~v..." "35672assume #t~ret61 != 0;havoc #t~ret61;assu..." "35679assume !(#t~ret61 != 0);havoc #t~ret61;c..." "34699assume !!(~v32~3 <= ~v33~3);assume !!(1 ..." "35194assume !!(~v33~3 <= ~v32~3);assume !!(~v..." "35667assume !!(~v22~3 <= ~v21~3);~v34~3 := ~v..." "35188assume !!(~v33~3 <= ~v37~3);assume !!(~v..." "35191assume !!(~v33~3 <= ~v28~3);assume !!(~v..." "35664assume !(#t~ret155 != 0);havoc #t~ret155..." "34692assume !!(~v21~3 <= 1);assume !!(~v33~3 ..." "35185assume !!(~v33~3 <= ~v34~3);assume !!(~v..." "35669assume !(~v22~3 <= ~v21~3);" "34689assume !!(1 + ~v21~3 <= ~v22~3);~v17~3 :..." "35510assume !!(~v38~3 <= ~v35~3);" "34961assume !(~v33~3 <= ~v32~3);" "35508assume !!(0 <= ~v15~3);call #t~ret40 := ..." "34963assume !(~v28~3 <= ~v33~3);" "34965assume !(~v33~3 <= ~v28~3);" "34407havoc ~a~2;#res := ~a~2;assume true;" "34404assume true;" "34967assume !(~v37~3 <= ~v33~3);" "34969assume !(~v33~3 <= ~v37~3);" "34971assume !(~v34~3 <= ~v33~3);" "34973assume !(~v33~3 <= ~v34~3);" "34975assume !(~v22~3 <= 1);" "34945assume !(~v22~3 <= ~v21~3);" "34947assume !(1 <= ~v22~3);" "34949assume !(#t~ret132 != 0);havoc #t~ret132..." "36040assume !(#t~ret110 != 0);havoc #t~ret110..." "34421assume true;" "34951assume !(~v38~3 <= ~v18~3);" "34420call ULTIMATE.init();assume true;Return ..." "34953assume !(~v18~3 <= ~v38~3);" "35501assume #t~ret39 != 0;havoc #t~ret39;" "34955assume !(~v37~3 <= ~v34~3);" "36038assume #t~ret110 != 0;havoc #t~ret110;~v..." "36033assume !!(~v21~3 <= 0);assume !(0 <= ~v3..." "35499assume !(0 <= ~v15~3);" "34957assume !(~v34~3 <= ~v37~3);" "36035assume !(~v21~3 <= 0);" "35497assume !!(0 <= ~v15~3);call #t~ret53 := ..." "34959assume !(~v32~3 <= ~v33~3);" "34995assume !(#t~ret130 != 0);havoc #t~ret130..." "34993assume !(0 <= ~v18~3);" "34999assume !(1 <= ~v22~3);" "34997assume !(~v22~3 <= ~v21~3);" "35003assume !(~v37~3 <= ~v35~3);" "35001assume !(~v35~3 <= ~v37~3);" "35007assume !(~v18~3 <= ~v38~3);" "34382havoc ~a~1;#res := ~a~1;assume true;" "35005assume !(~v38~3 <= ~v18~3);" "34979assume !(~v21~3 <= 1);" "34977assume !(1 <= ~v22~3);" "34983assume !(~v35~3 <= 0);" "34981assume !(1 <= ~v21~3);" "34987assume !(~v38~3 <= 0);" "34985assume !(0 <= ~v35~3);" "34991assume !(~v18~3 <= 0);" "34989assume !(0 <= ~v38~3);" "35992assume !(~v37~3 <= ~v34~3);" "35571assume !!(2 <= ~v22~3);" "35029assume !(~v22~3 <= 1);" "35994assume !(~v34~3 <= ~v37~3);" "35031assume !(1 <= ~v22~3);" "35569assume !!(1 <= ~v22~3);" "35996assume !(~v34~3 <= ~v33~3);" "35025assume !(~v34~3 <= ~v33~3);" "35575assume !(1 <= ~v22~3);" "35998assume !(~v33~3 <= ~v34~3);" "35027assume !(~v33~3 <= ~v34~3);" "35573assume !(2 <= ~v22~3);" "35984assume !(~v35~3 <= ~v37~3);" "35037assume !(~v38~3 <= 0);" "35579assume !(~v38~3 <= ~v35~3);" "35986assume !(~v37~3 <= ~v35~3);" "35039assume !(0 <= ~v38~3);" "35577assume !(~v35~3 <= ~v38~3);" "35988assume !(~v38~3 <= ~v18~3);" "35033assume !(~v21~3 <= 1);" "35990assume !(~v18~3 <= ~v38~3);" "35035assume !(1 <= ~v21~3);" "35581assume !(0 <= ~v15~3);" "35013assume !(~v32~3 <= ~v33~3);" "35976assume !(~v22~3 <= 0);" "35015assume !(~v33~3 <= ~v32~3);" "35978assume !(~v35~3 <= ~v38~3);" "35009assume !(~v37~3 <= ~v34~3);" "35980assume !(~v38~3 <= ~v35~3);" "35011assume !(~v34~3 <= ~v37~3);" "35982assume !(~v22~3 <= ~v21~3);" "35021assume !(~v37~3 <= ~v33~3);" "35023assume !(~v33~3 <= ~v37~3);" "35971assume !!(~v35~3 <= ~v38~3);call #t~ret1..." "35017assume !(~v35~3 <= ~v33~3);" "35567~v28~3 := #t~ret51;havoc #t~ret51;~v26~3..." "35972~v28~3 := #t~ret175;havoc #t~ret175;~v26..." "35566assume !!(~v35~3 <= ~v38~3);call #t~ret4..." "35019assume !(~v33~3 <= ~v35~3);" "35974assume !!(~v22~3 <= 0);" "36026assume !(0 <= ~v21~3);" "36024assume !(~v21~3 <= 0);" "35058assume #t~ret120 != 0;havoc #t~ret120;ca..." "36030assume !(~v33~3 <= 0);" "36028assume !(~v22~3 <= ~v21~3);" "36018assume !(0 <= ~v34~3);" "36016assume !(~v34~3 <= 0);" "36022assume !(0 <= ~v33~3);" "36020assume !(~v33~3 <= 0);" "36010assume !(0 <= ~v37~3);" "35045assume !(~v22~3 <= ~v21~3);" "36008assume !(~v37~3 <= 0);" "35043assume !(0 <= ~v18~3);" "36014assume !(0 <= ~v18~3);" "35041assume !(~v18~3 <= 0);" "36012assume !(~v18~3 <= 0);" "36002assume !(0 <= ~v35~3);" "36000assume !(~v35~3 <= 0);" "35051assume !(#t~ret111 != 0);havoc #t~ret111..." "36006assume !(0 <= ~v38~3);" "36004assume !(~v38~3 <= 0);" "34841assume !!(~v32~3 <= ~v33~3);" "34843assume !!(~v34~3 <= ~v37~3);" "35389assume !(~v22~3 <= ~v21~3);" "34845assume !!(~v37~3 <= ~v34~3);" "35387assume !!(~v22~3 <= ~v21~3);call #t~ret1..." "34847assume !!(~v18~3 <= ~v38~3);" "34833assume !!(~v37~3 <= ~v33~3);" "34835assume !!(~v33~3 <= ~v28~3);" "34837assume !!(~v28~3 <= ~v33~3);" "35379assume !(~v16~3 <= ~v15~3);" "34839assume !!(~v33~3 <= ~v32~3);" "35377assume !!(~v16~3 <= ~v15~3);call #t~ret1..." "34825assume !!(~v22~3 <= 1);" "34827assume !!(~v33~3 <= ~v34~3);" "35370assume !!(~v16~3 <= ~v15~3);call #t~ret1..." "35904assume !!(~v37~3 <= ~v35~3);" "34829assume !!(~v34~3 <= ~v33~3);" "35906assume !!(~v35~3 <= ~v37~3);" "34831assume !!(~v33~3 <= ~v37~3);" "34817assume !!(~v35~3 <= 0);" "34819assume !!(1 <= ~v21~3);" "34821assume !!(~v21~3 <= 1);" "35363assume !!(~v22~3 <= ~v21~3);call #t~ret1..." "35913assume !!(~v22~3 <= ~v21~3);call #t~ret1..." "34823assume !!(1 <= ~v22~3);" "35915assume !!(~v38~3 <= ~v35~3);" "34874assume !!(~v38~3 <= ~v35~3);" "34872assume !!(~v22~3 <= ~v21~3);call #t~ret1..." "35352assume #t~ret151 != 0;havoc #t~ret151;~v..." "35355assume !!(1 <= ~v22~3);assume !!(2 <= ~v..." "34865assume !!(1 <= ~v22~3);" "35345assume #t~ret151 != 0;havoc #t~ret151;~v..." "34859assume #t~ret132 != 0;havoc #t~ret132;~v..." "34863assume #t~ret133 != 0;havoc #t~ret133;" "35338assume !!(-1 + ~v15~3 <= ~v16~3);call #t..." "34861assume !(#t~ret133 != 0);havoc #t~ret133..." "34853assume !!(~v38~3 <= ~v18~3);call #t~ret1..." "35856assume !!(1 + ~v21~3 <= ~v22~3);~v17~3 :..." "35450assume !(#t~ret148 != 0);havoc #t~ret148..." "35858assume !(1 + ~v21~3 <= ~v22~3);" "35448assume #t~ret148 != 0;havoc #t~ret148;~v..." "35860assume #t~ret163 != 0;havoc #t~ret163;" "35862assume !!(~v22~3 <= ~v21~3);~v34~3 := ~v..." "35864assume !!(0 <= ~v21~3);" "35440assume !(~v18~3 <= 0);" "35866assume !!(~v21~3 <= 0);" "35868assume !!(0 <= ~v33~3);" "35870assume !!(~v33~3 <= 0);" "35435assume !(~v38~3 <= 0);" "35433assume !!(~v38~3 <= 0);assume !(~v33~3 <..." "35438assume !!(~v18~3 <= 0);assume !(0 <= ~v3..." "35425assume !(~v37~3 <= ~v33~3);" "35430assume !(~v34~3 <= ~v33~3);" "35428assume !!(~v34~3 <= ~v33~3);assume !(~v3..." "34943assume !(~v38~3 <= ~v35~3);" "35890assume !!(~v35~3 <= 0);" "34941assume !(~v35~3 <= ~v38~3);" "35888assume !!(0 <= ~v35~3);" "35418assume !!(~v32~3 <= ~v33~3);assume !(~v3..." "34939assume #t~ret146 != 0;havoc #t~ret146;~v..." "35420assume !(~v32~3 <= ~v33~3);" "35894assume !!(~v34~3 <= ~v33~3);" "35423assume !!(~v37~3 <= ~v33~3);assume !(~v3..." "34937assume !(#t~ret146 != 0);havoc #t~ret146..." "35892assume !!(~v33~3 <= ~v34~3);" "34935assume !!(~v35~3 <= ~v38~3);call #t~ret1..." "35898assume !!(~v37~3 <= ~v34~3);" "35408assume !!(~v38~3 <= ~v18~3);assume !(~v1..." "35410assume !(~v38~3 <= ~v18~3);" "35896assume !!(~v34~3 <= ~v37~3);" "35413assume !!(~v37~3 <= ~v34~3);assume !(~v1..." "35902assume !!(~v38~3 <= ~v18~3);" "35415assume !(~v37~3 <= ~v34~3);" "35900assume !!(~v18~3 <= ~v38~3);" "35874assume !!(~v34~3 <= 0);" "35872assume !!(0 <= ~v34~3);" "35403assume !!(-1 + ~v15~3 <= ~v16~3);call #t..." "35878assume !!(~v18~3 <= 0);" "35405assume !(-1 + ~v15~3 <= ~v16~3);" "35876assume !!(0 <= ~v18~3);" "35392assume !!(1 <= ~v22~3);assume !(2 <= ~v2..." "35882assume !!(~v37~3 <= 0);" "35394assume !(1 <= ~v22~3);" "35880assume !!(0 <= ~v37~3);" "35886assume !!(~v38~3 <= 0);" "35396assume !(#t~ret151 != 0);havoc #t~ret151..." "35884assume !!(0 <= ~v38~3);" }, returnAlphabet = {"34402return call #t~ret101 := nondet();" "34403return call #t~ret102 := nondet();" "34400return call #t~ret99 := nondet();" "34401return call #t~ret100 := nondet();" "34410return call #t~ret103 := nondet_bool();" "34411return call #t~ret104 := nondet_bool();" "34408return call #t~ret80 := nondet_bool();" "34409return call #t~ret95 := nondet_bool();" "34414return call #t~ret107 := nondet_bool();" "34415return call #t~ret108 := nondet_bool();" "34412return call #t~ret105 := nondet_bool();" "34413return call #t~ret106 := nondet_bool();" "34416return call #t~ret109 := nondet_bool();" "34644return call #t~ret185 := main();" "34383return call #t~ret81 := nondet();" "34385return call #t~ret83 := nondet();" "34384return call #t~ret82 := nondet();" "34387return call #t~ret85 := nondet();" "34386return call #t~ret84 := nondet();" "34389return call #t~ret87 := nondet();" "34388return call #t~ret86 := nondet();" "34391return call #t~ret89 := nondet();" "34390return call #t~ret88 := nondet();" "34393return call #t~ret91 := nondet();" "34392return call #t~ret90 := nondet();" "34395return call #t~ret93 := nondet();" "34394return call #t~ret92 := nondet();" "34397return call #t~ret96 := nondet();" "34396return call #t~ret94 := nondet();" "34399return call #t~ret98 := nondet();" "34398return call #t~ret97 := nondet();" }, states = {"2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "2598#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "1805#unseeded" "1811#(or unseeded (and (> oldRank (+ main_~v15~3 (- 1))) (>= oldRank 0)))" "2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))" }, initialStates = {"1805#unseeded" }, finalStates = {"1811#(or unseeded (and (> oldRank (+ main_~v15~3 (- 1))) (>= oldRank 0)))" }, callTransitions = { ("1805#unseeded" "34422call #t~ret185 := main();" "1805#unseeded") }, internalTransitions = { ("2598#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35352assume #t~ret151 != 0;havoc #t~ret151;~v..." "2598#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2598#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35338assume !!(-1 + ~v15~3 <= ~v16~3);call #t..." "2598#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2598#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35355assume !!(1 <= ~v22~3);assume !!(2 <= ~v..." "2598#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2598#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35363assume !!(~v22~3 <= ~v21~3);call #t~ret1..." "2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35318assume !!(~v37~3 <= ~v33~3);assume !!(~v..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35312assume !!(~v38~3 <= 0);assume !!(~v33~3 ..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35298assume !!(0 <= ~v15~3);call #t~ret53 := ..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35315assume !!(~v34~3 <= ~v33~3);assume !!(~v..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35309assume !!(~v18~3 <= 0);assume !!(0 <= ~v..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35324assume !!(~v37~3 <= ~v34~3);assume !!(~v..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35243assume !(#t~ret39 != 0);havoc #t~ret39;c..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35327assume !!(~v38~3 <= ~v18~3);assume !!(~v..." "2598#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35321assume !!(~v32~3 <= ~v33~3);assume !!(~v..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35247assume #t~ret52 != 0;havoc #t~ret52;" "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))" "35306assume #t~ret148 != 0;havoc #t~ret148;~v..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("1805#unseeded" "35200assume !!(~v18~3 <= ~v38~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "35745assume !!(~v20~3 <= -1 + ~v21~3);assume ..." "1805#unseeded") ("1805#unseeded" "35207assume !!(~v14~3 <= ~v15~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "35759assume !!(1 + ~v20~3 <= ~v22~3);call #t~..." "1805#unseeded") ("1805#unseeded" "35377assume !!(~v16~3 <= ~v15~3);call #t~ret1..." "1805#unseeded") ("1805#unseeded" "35218assume #t~ret158 != 0;havoc #t~ret158;~v..." "1805#unseeded") ("1805#unseeded" "35102assume !!(2 <= ~v21~3);" "1805#unseeded") ("1805#unseeded" "34420call ULTIMATE.init();assume true;Return ..." "1805#unseeded") ("1805#unseeded" "35100assume !!(1 + ~v21~3 <= ~v22~3);~v17~3 :..." "1805#unseeded") ("1805#unseeded" "35221assume #t~ret160 != 0;havoc #t~ret160;as..." "1805#unseeded") ("1805#unseeded" "35363assume !!(~v22~3 <= ~v21~3);call #t~ret1..." "1805#unseeded") ("1805#unseeded" "35229assume !!(2 <= ~v22~3);assume !!(~v22~3 ..." "1805#unseeded") ("1805#unseeded" "35232assume !!(-1 + ~v21~3 <= ~v14~3);assume ..." "1805#unseeded") ("1805#unseeded" "35232assume !!(-1 + ~v21~3 <= ~v14~3);assume ..." "1811#(or unseeded (and (> oldRank (+ main_~v15~3 (- 1))) (>= oldRank 0)))") ("1805#unseeded" "34640assume !(#t~ret163 != 0);havoc #t~ret163..." "1805#unseeded") ("1805#unseeded" "35237call #t~ret39 := nondet_bool();havoc ~a~..." "1805#unseeded") ("1805#unseeded" "35116call #t~ret61 := nondet_bool();havoc ~a~..." "1805#unseeded") ("1805#unseeded" "34646assume #t~ret176 != 0;havoc #t~ret176;" "1805#unseeded") ("1805#unseeded" "35352assume #t~ret151 != 0;havoc #t~ret151;~v..." "1805#unseeded") ("1805#unseeded" "35355assume !!(1 <= ~v22~3);assume !!(2 <= ~v..." "1805#unseeded") ("1805#unseeded" "35119assume #t~ret61 != 0;havoc #t~ret61;assu..." "1805#unseeded") ("1805#unseeded" "35104assume !!(~v21~3 <= 2);" "1805#unseeded") ("1805#unseeded" "35243assume !(#t~ret39 != 0);havoc #t~ret39;c..." "1805#unseeded") ("1805#unseeded" "35106assume !!(~v33~3 <= ~v32~3);" "1805#unseeded") ("1805#unseeded" "35108assume !!(~v32~3 <= ~v33~3);" "1805#unseeded") ("1805#unseeded" "35247assume #t~ret52 != 0;havoc #t~ret52;" "1805#unseeded") ("1805#unseeded" "35111assume !!(1 <= ~v22~3);assume !!(2 <= ~v..." "1805#unseeded") ("1805#unseeded" "34625assume #t~ret110 != 0;havoc #t~ret110;~v..." "1805#unseeded") ("1805#unseeded" "35338assume !!(-1 + ~v15~3 <= ~v16~3);call #t..." "1805#unseeded") ("1805#unseeded" "34628assume !!(~v21~3 <= 0);assume !!(0 <= ~v..." "1805#unseeded") ("1805#unseeded" "35742assume !!(~v21~3 <= 1 + ~v20~3);assume !..." "1805#unseeded") ("1805#unseeded" "34634assume !!(~v33~3 <= 0);call #t~ret163 :=..." "1805#unseeded") ("1805#unseeded" "35739assume !!(0 <= ~v21~3);call #t~ret70 := ..." "1805#unseeded") ("1805#unseeded" "34622call #t~ret0 := nondet();havoc ~a~1;#res..." "1805#unseeded") ("1805#unseeded" "35686assume !(#t~ret61 != 0);havoc #t~ret61;c..." "1805#unseeded") ("1805#unseeded" "35161assume !!(~v22~3 <= ~v21~3);~v34~3 := ~v..." "1805#unseeded") ("1805#unseeded" "35182assume !!(0 <= -1 * ~v14~3 + ~v15~3);ass..." "1805#unseeded") ("1805#unseeded" "35058assume #t~ret120 != 0;havoc #t~ret120;ca..." "1805#unseeded") ("1805#unseeded" "35176assume !!(0 <= ~v18~3);assume !!(~v18~3 ..." "1805#unseeded") ("1805#unseeded" "35179assume !!(0 <= ~v38~3);assume !!(~v38~3 ..." "1805#unseeded") ("1805#unseeded" "35298assume !!(0 <= ~v15~3);call #t~ret53 := ..." "1805#unseeded") ("1805#unseeded" "35309assume !!(~v18~3 <= 0);assume !!(0 <= ~v..." "1805#unseeded") ("1805#unseeded" "35173assume #t~ret155 != 0;havoc #t~ret155;~v..." "1805#unseeded") ("1805#unseeded" "35306assume #t~ret148 != 0;havoc #t~ret148;~v..." "1805#unseeded") ("1805#unseeded" "35197assume !!(~v34~3 <= ~v37~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "35318assume !!(~v37~3 <= ~v33~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "34699assume !!(~v32~3 <= ~v33~3);assume !!(1 ..." "1805#unseeded") ("1805#unseeded" "35312assume !!(~v38~3 <= 0);assume !!(~v33~3 ..." "1805#unseeded") ("1805#unseeded" "35194assume !!(~v33~3 <= ~v32~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "35315assume !!(~v34~3 <= ~v33~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "35324assume !!(~v37~3 <= ~v34~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "35188assume !!(~v33~3 <= ~v37~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "35191assume !!(~v33~3 <= ~v28~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "34692assume !!(~v21~3 <= 1);assume !!(~v33~3 ..." "1805#unseeded") ("1805#unseeded" "35327assume !!(~v38~3 <= ~v18~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "35185assume !!(~v33~3 <= ~v34~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "35051assume !(#t~ret111 != 0);havoc #t~ret111..." "1805#unseeded") ("1805#unseeded" "35321assume !!(~v32~3 <= ~v33~3);assume !!(~v..." "1805#unseeded") ("1805#unseeded" "34689assume !!(1 + ~v21~3 <= ~v22~3);~v17~3 :..." "1805#unseeded") ("2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))" "35237call #t~ret39 := nondet_bool();havoc ~a~..." "2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))") ("2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))" "35298assume !!(0 <= ~v15~3);call #t~ret53 := ..." "1811#(or unseeded (and (> oldRank (+ main_~v15~3 (- 1))) (>= oldRank 0)))") ("2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))" "35243assume !(#t~ret39 != 0);havoc #t~ret39;c..." "2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))") ("2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))" "35377assume !!(~v16~3 <= ~v15~3);call #t~ret1..." "2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))") ("2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))" "35247assume #t~ret52 != 0;havoc #t~ret52;" "2704#(and (<= main_~v15~3 oldRank) (<= main_~v16~3 oldRank) (<= main_~v15~3 (+ oldRank 1)))") ("1811#(or unseeded (and (> oldRank (+ main_~v15~3 (- 1))) (>= oldRank 0)))" "35237call #t~ret39 := nondet_bool();havoc ~a~..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") ("1811#(or unseeded (and (> oldRank (+ main_~v15~3 (- 1))) (>= oldRank 0)))" "35306assume #t~ret148 != 0;havoc #t~ret148;~v..." "2323#(and (<= main_~v15~3 (+ oldRank 1)) (= oldRank (+ main_~v15~3 (- 1))))") }, returnTransitions = { } );