// Testfile dumped by Ultimate at 2013/11/09 20:11:19 print(numberOfStates(nwa)); NestedWordAutomaton complement = buchiComplementFKV(nwa); print(numberOfStates(complement)); assert(numberOfStates(complement) == 65); // with MatthiasTightLevelRankingStateGenerator result was 71 NestedWordAutomaton live = removeNonLiveStates(complement); print(numberOfStates(live)); assert(numberOfStates(live) == 65); minimizeSevpa(complement); //reduced to 47 NestedWordAutomaton nwa = ( callAlphabet = {"2696call #t~ret189 := main();" }, internalAlphabet = {"3828call #t~ret40 := nondet_bool();havoc ~a~..." "3834assume !(#t~ret40 != 0);havoc #t~ret40;c..." "3809assume #t~ret158 != 0;havoc #t~ret158;~v..." "3265assume !!(~v37~3 <= ~v38~3);" "3267assume !!(1 <= ~v30~3);" "3812assume #t~ret160 != 0;havoc #t~ret160;as..." "3823assume !!(-1 + ~v19~3 <= ~v14~3);assume ..." "3820assume !!(2 <= ~v30~3);assume !!(~v30~3 ..." "3318assume !!(0 <= ~v37~3);" "3316assume !!(~v39~3 <= 0);" "3314assume !!(0 <= ~v39~3);" "3312assume !!(~v17~3 <= 0);" "3798assume !!(~v14~3 <= ~v15~3);assume !!(~v..." "3326assume !!(~v29~3 <= ~v36~3);" "3324assume !!(~v30~3 <= 1);" "3322assume !!(1 <= ~v30~3);" "3320assume !!(~v37~3 <= 0);" "3776assume !!(0 <= -1 * ~v14~3 + ~v15~3);ass..." "3779assume !!(~v29~3 <= ~v36~3);assume !!(~v..." "4359assume !(#t~ret80 != 0);havoc #t~ret80;" "3298assume !!(~v30~3 <= 1);call #t~ret128 :=..." "4357assume #t~ret80 != 0;havoc #t~ret80;call..." "3782assume !!(~v29~3 <= ~v38~3);assume !!(~v..." "3785assume !!(~v29~3 <= ~v31~3);assume !!(~v..." "3310assume !!(0 <= ~v17~3);" "2695assume true;" "2694call ULTIMATE.init();assume true;Return ..." "3308assume #t~ret139 != 0;havoc #t~ret139;~v..." "3306assume !(#t~ret139 != 0);havoc #t~ret139..." "3788assume !!(~v36~3 <= ~v38~3);assume !!(~v..." "3791assume !!(~v17~3 <= ~v39~3);assume !!(~v..." "3304assume #t~ret138 != 0;havoc #t~ret138;~v..." "3767assume #t~ret155 != 0;havoc #t~ret155;~v..." "3773assume !!(0 <= ~v39~3);assume !!(~v39~3 ..." "3770assume !!(0 <= ~v17~3);assume !!(~v17~3 ..." "3229assume !!(~v22~3 <= ~v20~3);~v33~3 := ~v..." "3231assume !!(0 <= ~v17~3);" "3755assume !!(~v30~3 <= ~v20~3);assume !!(0 ..." "3251assume !!(~v29~3 <= ~v37~3);" "3249assume !!(~v38~3 <= ~v29~3);" "3255assume !!(~v36~3 <= ~v38~3);" "3253assume !!(~v37~3 <= ~v29~3);" "3259assume !!(~v17~3 <= ~v39~3);" "3257assume !!(~v38~3 <= ~v36~3);" "3263assume !!(~v38~3 <= ~v37~3);" "3261assume !!(~v39~3 <= ~v17~3);" "3235assume !!(0 <= ~v39~3);" "3233assume !!(~v17~3 <= 0);" "3718assume !!(1 <= ~v30~3);assume !!(2 <= ~v..." "3239assume !!(1 <= ~v30~3);" "3712assume !!(~v17~3 <= ~v39~3);assume !!(~v..." "3237assume !!(~v39~3 <= 0);" "3715assume !!(~v38~3 <= ~v37~3);assume !!(~v..." "3243assume !!(~v29~3 <= ~v36~3);" "3241assume !!(~v30~3 <= 1);" "3247assume !!(~v29~3 <= ~v38~3);" "3245assume !!(~v36~3 <= ~v29~3);" "3164assume !!(~v20~3 <= 1);assume !!(~v30~3 ..." "3706assume !!(~v29~3 <= ~v37~3);assume !!(~v..." "3167assume !!(~v22~3 <= ~v30~3);assume !!(~v..." "3161assume !!(1 + ~v20~3 <= ~v22~3);~v35~3 :..." "3709assume !!(~v36~3 <= ~v38~3);assume !!(~v..." "3697assume !!(0 <= ~v39~3);assume !!(~v39~3 ..." "3703assume !!(~v29~3 <= ~v38~3);assume !!(~v..." "3153assume #t~ret185 != 0;havoc #t~ret185;ca..." "3700assume !!(~v29~3 <= ~v36~3);assume !!(~v..." "3691assume !!(0 <= ~v20~3);call #t~ret61 := ..." "3694assume !!(0 <= ~v17~3);assume !!(~v17~3 ..." "3141assume !(#t~ret163 != 0);havoc #t~ret163..." "3187assume #t~ret118 != 0;havoc #t~ret118;ca..." "3180assume !!(~v35~3 <= ~v28~3);assume !!(1 ..." "3173assume !!(~v35~3 <= ~v18~3);assume !!(~v..." "3170assume !!(~v28~3 <= ~v18~3);assume !!(~v..." "3097assume !(~v38~3 <= ~v37~3);" "3099assume !(~v39~3 <= ~v17~3);" "3101assume !(~v17~3 <= ~v39~3);" "3643call #t~ret60 := nondet_bool();havoc ~a~..." "2678assume true;" "3103assume !(~v38~3 <= ~v36~3);" "3089assume !(~v37~3 <= ~v39~3);" "3637assume !!(1 + ~v21~3 <= ~v22~3);call #t~..." "3091assume !(~v39~3 <= ~v37~3);" "2681havoc ~a~2;#res := ~a~2;assume true;" "3093assume !(~v30~3 <= 0);" "3095assume !(~v37~3 <= ~v38~3);" "3630assume !!(1 + ~v21~3 <= ~v22~3);call #t~..." "3080assume !!(~v37~3 <= ~v39~3);call #t~ret1..." "3081~v31~3 := #t~ret184;havoc #t~ret184;~v27..." "2659havoc ~a~1;#res := ~a~1;assume true;" "3083assume !!(~v30~3 <= 0);" "3084assume true;" "3087assume !(~v30~3 <= 0);" "3623assume !!(~v21~3 <= -1 + ~v20~3);assume ..." "3620assume !!(~v20~3 <= 1 + ~v21~3);assume !..." "3617assume !!(0 <= ~v20~3);call #t~ret77 := ..." "3131assume !(~v29~3 <= 0);" "3129assume !(0 <= ~v36~3);" "3135assume !(~v22~3 <= ~v20~3);" "3133assume !(0 <= ~v29~3);" "3123assume !(~v17~3 <= 0);" "3121assume !(0 <= ~v38~3);" "3127assume !(~v36~3 <= 0);" "3125assume !(0 <= ~v17~3);" "4560call #t~ret0 := nondet();havoc ~a~1;#res..." "3115assume !(~v39~3 <= 0);" "3599call #t~ret60 := nondet_bool();havoc ~a~..." "3113assume !(0 <= ~v37~3);" "3119assume !(~v38~3 <= 0);" "3117assume !(0 <= ~v39~3);" "3588call #t~ret60 := nondet_bool();havoc ~a~..." "3107assume !(~v36~3 <= ~v29~3);" "3105assume !(~v36~3 <= ~v38~3);" "3111assume !(~v37~3 <= 0);" "3109assume !(~v29~3 <= ~v36~3);" "2989assume !!(0 <= ~v38~3);" "4130assume !(~v14~3 <= ~v15~3);" "2991assume !!(~v38~3 <= 0);" "4128assume !!(~v14~3 <= ~v15~3);assume !(~v1..." "3524assume !(~v22~3 <= ~v20~3);" "2985assume !!(0 <= ~v17~3);" "4135assume !(~v17~3 <= ~v39~3);" "3522assume !(0 <= ~v17~3);" "2987assume !!(~v17~3 <= 0);" "4133assume !!(~v17~3 <= ~v39~3);assume !(~v3..." "3520assume !(~v17~3 <= 0);" "2981assume !!(0 <= ~v36~3);" "4138assume !!(~v36~3 <= ~v38~3);assume !(~v3..." "2983assume !!(~v36~3 <= 0);" "2977assume !!(0 <= ~v29~3);" "4143assume !!(~v29~3 <= ~v31~3);assume !(~v3..." "3530assume !(#t~ret118 != 0);havoc #t~ret118..." "2979assume !!(~v29~3 <= 0);" "4140assume !(~v36~3 <= ~v38~3);" "3005assume !!(~v36~3 <= ~v38~3);" "3007assume !!(~v38~3 <= ~v36~3);" "4145assume !(~v29~3 <= ~v31~3);" "4150assume !(~v29~3 <= ~v38~3);" "3001assume !!(~v29~3 <= ~v36~3);" "4148assume !!(~v29~3 <= ~v38~3);assume !(~v3..." "4086assume !!(~v37~3 <= ~v39~3);call #t~ret4..." "4087~v31~3 := #t~ret52;havoc #t~ret52;~v27~3..." "3003assume !!(~v36~3 <= ~v29~3);" "4155assume !(~v29~3 <= ~v36~3);" "4089assume !!(1 <= ~v30~3);" "2997assume !!(0 <= ~v37~3);" "4153assume !!(~v29~3 <= ~v36~3);assume !(~v3..." "4091assume !!(2 <= ~v30~3);" "2999assume !!(~v37~3 <= 0);" "4158assume !!(0 <= -1 * ~v14~3 + ~v15~3);ass..." "2993assume !!(0 <= ~v39~3);" "3547assume #t~ret133 != 0;havoc #t~ret133;ca..." "4093assume !(2 <= ~v30~3);" "2995assume !!(~v39~3 <= 0);" "4095assume !(1 <= ~v30~3);" "4097assume !(~v37~3 <= ~v39~3);" "3556assume !!(2 <= ~v20~3);" "4099assume !(~v39~3 <= ~v37~3);" "3558assume !!(~v20~3 <= 2);" "4101assume !(0 <= ~v15~3);" "3554assume !!(1 + ~v20~3 <= ~v22~3);~v35~3 :..." "4104assume !!(-1 + ~v19~3 <= ~v14~3);assume ..." "3564assume !!(~v18~3 <= ~v28~3);" "4106assume !(-1 + ~v19~3 <= ~v14~3);" "3566assume !!(~v28~3 <= ~v18~3);" "4109assume !!(2 <= ~v30~3);assume !(~v30~3 <..." "3560assume !!(~v30~3 <= ~v22~3);" "4111assume !(2 <= ~v30~3);" "3562assume !!(~v22~3 <= ~v30~3);" "3572assume !!(~v28~3 <= ~v35~3);" "2975assume !!(~v22~3 <= ~v20~3);~v33~3 := ~v..." "4114assume #t~ret160 != 0;havoc #t~ret160;as..." "3574assume !!(~v35~3 <= ~v28~3);" "4116assume !(#t~ret160 != 0);havoc #t~ret160..." "3568assume !!(~v18~3 <= ~v35~3);" "3570assume !!(~v35~3 <= ~v18~3);" "4123assume #t~ret158 != 0;havoc #t~ret158;~v..." "4125assume !(#t~ret158 != 0);havoc #t~ret158..." "3577assume !!(1 <= ~v22~3);assume !!(2 <= ~v..." "4199assume !(~v17~3 <= ~v39~3);" "4005assume !(0 <= ~v17~3);" "3458assume !(~v38~3 <= ~v29~3);" "4197assume !!(~v17~3 <= ~v39~3);assume !(~v3..." "3456assume !(~v29~3 <= ~v31~3);" "4194assume !(~v38~3 <= ~v37~3);" "3462assume !(~v36~3 <= ~v29~3);" "4000assume !(0 <= ~v39~3);" "4003assume !!(0 <= ~v17~3);assume !(~v17~3 <..." "4192assume !!(~v38~3 <= ~v37~3);assume !(~v3..." "3460assume !(~v29~3 <= ~v38~3);" "4207assume !!(~v29~3 <= ~v37~3);assume !(~v3..." "4012assume #t~ret83 != 0;havoc #t~ret83;~v1~..." "3466assume !(~v30~3 <= 1);" "3464assume !(~v29~3 <= ~v36~3);" "4014assume !(#t~ret83 != 0);havoc #t~ret83;" "4204assume !(~v36~3 <= ~v38~3);" "3470assume !(~v37~3 <= 0);" "4202assume !!(~v36~3 <= ~v38~3);assume !(~v3..." "3468assume !(1 <= ~v30~3);" "3474assume !(~v39~3 <= 0);" "4214assume !(~v29~3 <= ~v38~3);" "4021assume #t~ret40 != 0;havoc #t~ret40;" "3472assume !(0 <= ~v37~3);" "4212assume !!(~v29~3 <= ~v38~3);assume !(~v3..." "3478assume !(~v17~3 <= 0);" "4017assume #t~ret53 != 0;havoc #t~ret53;assu..." "3476assume !(0 <= ~v39~3);" "4019assume !(#t~ret53 != 0);havoc #t~ret53;" "4209assume !(~v29~3 <= ~v37~3);" "4222assume !!(0 <= ~v39~3);assume !(~v39~3 <..." "3482assume !(#t~ret138 != 0);havoc #t~ret138..." "4028assume !!(0 <= ~v15~3);call #t~ret41 := ..." "3480assume !(0 <= ~v17~3);" "4030assume !!(~v39~3 <= ~v37~3);" "3486assume !(1 <= ~v30~3);" "4219assume !(~v29~3 <= ~v36~3);" "3484assume !(~v30~3 <= 1);" "4217assume !!(~v29~3 <= ~v36~3);assume !(~v3..." "4165assume !(0 <= ~v39~3);" "3975assume !(~v16~3 <= -1 + ~v15~3);" "3488assume !(~v37~3 <= ~v38~3);" "3973assume !!(~v16~3 <= -1 + ~v15~3);assume ..." "3490assume !(~v38~3 <= ~v37~3);" "3022assume !!(~v30~3 <= 0);call #t~ret173 :=..." "3970assume !(#t~ret86 != 0);havoc #t~ret86;" "4160assume !(0 <= -1 * ~v14~3 + ~v15~3);" "3492assume !(~v39~3 <= ~v17~3);" "4163assume !!(0 <= ~v39~3);assume !(~v39~3 <..." "3968assume #t~ret86 != 0;havoc #t~ret86;~v2~..." "3494assume !(~v17~3 <= ~v39~3);" "3983assume !!(~v36~3 <= ~v38~3);assume !(~v3..." "3011assume !!(~v39~3 <= ~v17~3);" "3496assume !(~v38~3 <= ~v36~3);" "3009assume !!(~v17~3 <= ~v39~3);" "3498assume !(~v36~3 <= ~v38~3);" "3980assume !(~v17~3 <= ~v39~3);" "3015assume !!(~v37~3 <= ~v38~3);" "3500assume !(~v37~3 <= ~v29~3);" "4168assume !!(0 <= ~v17~3);assume !(~v17~3 <..." "3978assume !!(~v17~3 <= ~v39~3);assume !(~v3..." "3013assume !!(~v38~3 <= ~v37~3);" "3502assume !(~v29~3 <= ~v37~3);" "4170assume !(0 <= ~v17~3);" "3504assume !(~v38~3 <= ~v29~3);" "3990assume !(~v29~3 <= ~v38~3);" "3506assume !(~v29~3 <= ~v38~3);" "4182assume !!(~v30~3 <= ~v20~3);assume !(0 <..." "3988assume !!(~v29~3 <= ~v38~3);assume !(~v3..." "3508assume !(~v36~3 <= ~v29~3);" "4177assume #t~ret155 != 0;havoc #t~ret155;~v..." "3510assume !(~v29~3 <= ~v36~3);" "4179assume !(#t~ret155 != 0);havoc #t~ret155..." "3985assume !(~v36~3 <= ~v38~3);" "3512assume !(~v30~3 <= 1);" "3998assume !!(0 <= ~v39~3);assume !(~v39~3 <..." "4189assume !(1 <= ~v30~3);" "3514assume !(1 <= ~v30~3);" "3024assume !!(~v39~3 <= ~v37~3);" "4184assume !(~v30~3 <= ~v20~3);" "3516assume !(~v39~3 <= 0);" "3995assume !(~v29~3 <= ~v36~3);" "3518assume !(0 <= ~v39~3);" "3993assume !!(~v29~3 <= ~v36~3);assume !(~v3..." "4187assume !!(1 <= ~v30~3);assume !(2 <= ~v3..." "3944assume !!(~v16~3 <= ~v15~3);call #t~ret9..." "4266assume !(0 <= ~v20~3);" "3946assume !(~v16~3 <= ~v15~3);" "4264assume !!(0 <= ~v20~3);call #t~ret77 := ..." "4271assume !(1 <= ~v22~3);" "4269assume !!(1 <= ~v22~3);assume !(2 <= ~v2..." "3937assume !!(~v16~3 <= ~v15~3);call #t~ret9..." "4283assume !(~v18~3 <= ~v28~3);" "3961assume !(#t~ret88 != 0);havoc #t~ret88;" "4281assume !(~v28~3 <= ~v18~3);" "4287assume !(~v30~3 <= ~v22~3);" "4285assume !(~v22~3 <= ~v30~3);" "4275assume !(~v28~3 <= ~v35~3);" "4273assume !(~v35~3 <= ~v28~3);" "3954assume !!(2 <= ~v30~3);call #t~ret89 := ..." "4279assume !(~v18~3 <= ~v35~3);" "3956assume !(2 <= ~v30~3);" "4277assume !(~v35~3 <= ~v18~3);" "3959assume #t~ret88 != 0;havoc #t~ret88;assu..." "3436assume !(~v37~3 <= ~v39~3);" "3438assume !(~v39~3 <= ~v37~3);" "3432assume !(#t~ret154 != 0);havoc #t~ret154..." "3919assume #t~ret86 != 0;havoc #t~ret86;~v2~..." "4237assume !!(0 <= ~v20~3);call #t~ret61 := ..." "3434assume #t~ret154 != 0;havoc #t~ret154;~v..." "4239assume !(0 <= ~v20~3);" "4224assume !(0 <= ~v39~3);" "3430assume !!(~v37~3 <= ~v39~3);call #t~ret1..." "4227assume !!(0 <= ~v17~3);assume !(~v17~3 <..." "4229assume !(0 <= ~v17~3);" "3908assume !!(~v16~3 <= -1 + ~v15~3);assume ..." "4249assume !!(~v20~3 <= 1 + ~v21~3);assume !..." "3930assume !!(2 <= ~v30~3);call #t~ret89 := ..." "3452assume !(~v36~3 <= ~v38~3);" "4251assume !(~v20~3 <= 1 + ~v21~3);" "3454assume !(~v31~3 <= ~v29~3);" "3448assume !(~v17~3 <= ~v39~3);" "3450assume !(~v38~3 <= ~v36~3);" "4241assume !(1 + ~v21~3 <= ~v22~3);" "3444assume !(#t~ret140 != 0);havoc #t~ret140..." "3922assume #t~ret88 != 0;havoc #t~ret88;assu..." "3446assume !(~v39~3 <= ~v17~3);" "4244assume !!(~v21~3 <= -1 + ~v20~3);assume ..." "3440assume !(~v30~3 <= 1);" "3442assume !(1 <= ~v30~3);" "4246assume !(~v21~3 <= -1 + ~v20~3);" "4334assume !(~v22~3 <= ~v30~3);" "3338assume !!(~v36~3 <= ~v38~3);" "2914assume #t~ret80 != 0;havoc #t~ret80;call..." "3886assume !!(0 <= ~v17~3);assume !!(~v17~3 ..." "3336assume !!(~v31~3 <= ~v29~3);" "4332assume !(#t~ret185 != 0);havoc #t~ret185..." "4330assume !(1 + ~v20~3 <= ~v22~3);" "3342assume !!(~v17~3 <= ~v39~3);" "2917assume !!(~v20~3 <= 0);assume !!(0 <= ~v..." "4328assume !!(1 + ~v20~3 <= ~v22~3);~v35~3 :..." "3340assume !!(~v38~3 <= ~v36~3);" "3883assume #t~ret83 != 0;havoc #t~ret83;~v1~..." "3330assume !!(~v29~3 <= ~v38~3);" "2920assume !!(~v18~3 <= 0);assume !!(~v30~3 ..." "3328assume !!(~v36~3 <= ~v29~3);" "3334assume !!(~v29~3 <= ~v31~3);" "4320assume !(~v20~3 <= 1);" "3332assume !!(~v38~3 <= ~v29~3);" "2926assume !!(~v22~3 <= ~v30~3);call #t~ret1..." "3901assume !!(~v17~3 <= ~v39~3);assume !!(~v..." "3354assume #t~ret140 != 0;havoc #t~ret140;~v..." "2933assume #t~ret163 != 0;havoc #t~ret163;ca..." "3358assume #t~ret141 != 0;havoc #t~ret141;" "3356assume !(#t~ret141 != 0);havoc #t~ret141..." "3898assume !!(~v36~3 <= ~v38~3);assume !!(~v..." "4344assume !(~v20~3 <= 0);" "3892assume !!(~v29~3 <= ~v36~3);assume !!(~v..." "4342assume !!(~v20~3 <= 0);assume !(0 <= ~v1..." "3895assume !!(~v29~3 <= ~v38~3);assume !!(~v..." "3889assume !!(0 <= ~v39~3);assume !!(~v39~3 ..." "4339assume !(~v18~3 <= 0);" "4337assume !!(~v18~3 <= 0);assume !(~v30~3 <..." "3348assume !!(~v39~3 <= ~v17~3);call #t~ret1..." "4300assume !(~v35~3 <= ~v28~3);" "3369assume !!(~v39~3 <= ~v37~3);" "4303assume !!(~v35~3 <= ~v18~3);assume !(~v2..." "4298assume !!(~v35~3 <= ~v28~3);assume !(1 <..." "3360assume !!(1 <= ~v30~3);" "4293assume !(1 + ~v20~3 <= ~v22~3);" "4295assume !(#t~ret133 != 0);havoc #t~ret133..." "4289assume !(~v20~3 <= 2);" "3367assume !!(~v30~3 <= 1);call #t~ret142 :=..." "4291assume !(2 <= ~v20~3);" "3871assume #t~ret53 != 0;havoc #t~ret53;assu..." "4318assume !!(~v20~3 <= 1);assume !(~v30~3 <..." "4313assume !!(~v22~3 <= ~v30~3);assume !(~v1..." "2901call #t~ret0 := nondet();havoc ~a~1;#res..." "4315assume !(~v22~3 <= ~v30~3);" "4308assume !!(~v28~3 <= ~v18~3);assume !(~v1..." "4310assume !(~v28~3 <= ~v18~3);" "4305assume !(~v35~3 <= ~v18~3);" }, returnAlphabet = {"2675return call #t~ret108 := nondet();" "2674return call #t~ret107 := nondet();" "2673return call #t~ret106 := nondet();" "2672return call #t~ret104 := nondet();" "2677return call #t~ret110 := nondet();" "2676return call #t~ret109 := nondet();" "2683return call #t~ret105 := nondet_bool();" "2682return call #t~ret91 := nondet_bool();" "2687return call #t~ret114 := nondet_bool();" "2686return call #t~ret113 := nondet_bool();" "2685return call #t~ret112 := nondet_bool();" "2684return call #t~ret111 := nondet_bool();" "2662return call #t~ret94 := nondet();" "3085return call #t~ret189 := main();" "2663return call #t~ret95 := nondet();" "2660return call #t~ret92 := nondet();" "2661return call #t~ret93 := nondet();" "2666return call #t~ret98 := nondet();" "2667return call #t~ret99 := nondet();" "2664return call #t~ret96 := nondet();" "2665return call #t~ret97 := nondet();" "2670return call #t~ret102 := nondet();" "2671return call #t~ret103 := nondet();" "2668return call #t~ret100 := nondet();" "2669return call #t~ret101 := nondet();" "2689return call #t~ret116 := nondet_bool();" "2688return call #t~ret115 := nondet_bool();" "2690return call #t~ret117 := nondet_bool();" }, states = {"3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3689#(and (<= main_~v16~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "2298#(or unseeded (and (> oldRank (+ main_~v15~3 (- 2))) (>= oldRank 0)))" "3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3296#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "2292#unseeded" "3770#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" }, initialStates = {"2292#unseeded" }, finalStates = {"2298#(or unseeded (and (> oldRank (+ main_~v15~3 (- 2))) (>= oldRank 0)))" }, callTransitions = { ("2292#unseeded" "2696call #t~ret189 := main();" "2292#unseeded") }, internalTransitions = { ("3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3871assume #t~ret53 != 0;havoc #t~ret53;assu..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3901assume !!(~v17~3 <= ~v39~3);assume !!(~v..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3886assume !!(0 <= ~v17~3);assume !!(~v17~3 ..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3883assume #t~ret83 != 0;havoc #t~ret83;~v1~..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3898assume !!(~v36~3 <= ~v38~3);assume !!(~v..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3834assume !(#t~ret40 != 0);havoc #t~ret40;c..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3892assume !!(~v29~3 <= ~v36~3);assume !!(~v..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3895assume !!(~v29~3 <= ~v38~3);assume !!(~v..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3889assume !!(0 <= ~v39~3);assume !!(~v39~3 ..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3908assume !!(~v16~3 <= -1 + ~v15~3);assume ..." "3296#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3689#(and (<= main_~v16~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3922assume #t~ret88 != 0;havoc #t~ret88;assu..." "3689#(and (<= main_~v16~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3689#(and (<= main_~v16~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3919assume #t~ret86 != 0;havoc #t~ret86;~v2~..." "3689#(and (<= main_~v16~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3689#(and (<= main_~v16~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3930assume !!(2 <= ~v30~3);call #t~ret89 := ..." "3770#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3901assume !!(~v17~3 <= ~v39~3);assume !!(~v..." "3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3886assume !!(0 <= ~v17~3);assume !!(~v17~3 ..." "3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3898assume !!(~v36~3 <= ~v38~3);assume !!(~v..." "3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3892assume !!(~v29~3 <= ~v36~3);assume !!(~v..." "3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3895assume !!(~v29~3 <= ~v38~3);assume !!(~v..." "3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3889assume !!(0 <= ~v39~3);assume !!(~v39~3 ..." "3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3908assume !!(~v16~3 <= -1 + ~v15~3);assume ..." "3689#(and (<= main_~v16~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("2298#(or unseeded (and (> oldRank (+ main_~v15~3 (- 2))) (>= oldRank 0)))" "3828call #t~ret40 := nondet_bool();havoc ~a~..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("2298#(or unseeded (and (> oldRank (+ main_~v15~3 (- 2))) (>= oldRank 0)))" "3883assume #t~ret83 != 0;havoc #t~ret83;~v1~..." "3049#(and (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3296#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3922assume #t~ret88 != 0;havoc #t~ret88;assu..." "3296#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3296#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3919assume #t~ret86 != 0;havoc #t~ret86;~v2~..." "3296#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))") ("3296#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)) (= oldRank (+ main_~v15~3 (- 2))))" "3930assume !!(2 <= ~v30~3);call #t~ret89 := ..." "3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3944assume !!(~v16~3 <= ~v15~3);call #t~ret9..." "3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3871assume #t~ret53 != 0;havoc #t~ret53;assu..." "3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3828call #t~ret40 := nondet_bool();havoc ~a~..." "3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3883assume #t~ret83 != 0;havoc #t~ret83;~v1~..." "3508#(and (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3834assume !(#t~ret40 != 0);havoc #t~ret40;c..." "3377#(and (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("2292#unseeded" "3944assume !!(~v16~3 <= ~v15~3);call #t~ret9..." "2292#unseeded") ("2292#unseeded" "3164assume !!(~v20~3 <= 1);assume !!(~v30~3 ..." "2292#unseeded") ("2292#unseeded" "3706assume !!(~v29~3 <= ~v37~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3167assume !!(~v22~3 <= ~v30~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3161assume !!(1 + ~v20~3 <= ~v22~3);~v35~3 :..." "2292#unseeded") ("2292#unseeded" "3828call #t~ret40 := nondet_bool();havoc ~a~..." "2292#unseeded") ("2292#unseeded" "3709assume !!(~v36~3 <= ~v38~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3834assume !(#t~ret40 != 0);havoc #t~ret40;c..." "2292#unseeded") ("2292#unseeded" "3697assume !!(0 <= ~v39~3);assume !!(~v39~3 ..." "2292#unseeded") ("2292#unseeded" "3153assume #t~ret185 != 0;havoc #t~ret185;ca..." "2292#unseeded") ("2292#unseeded" "3703assume !!(~v29~3 <= ~v38~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3530assume !(#t~ret118 != 0);havoc #t~ret118..." "2292#unseeded") ("2292#unseeded" "3700assume !!(~v29~3 <= ~v36~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3691assume !!(0 <= ~v20~3);call #t~ret61 := ..." "2292#unseeded") ("2292#unseeded" "3809assume #t~ret158 != 0;havoc #t~ret158;~v..." "2292#unseeded") ("2292#unseeded" "3694assume !!(0 <= ~v17~3);assume !!(~v17~3 ..." "2292#unseeded") ("2292#unseeded" "3812assume #t~ret160 != 0;havoc #t~ret160;as..." "2292#unseeded") ("2292#unseeded" "3141assume !(#t~ret163 != 0);havoc #t~ret163..." "2292#unseeded") ("2292#unseeded" "3823assume !!(-1 + ~v19~3 <= ~v14~3);assume ..." "2298#(or unseeded (and (> oldRank (+ main_~v15~3 (- 2))) (>= oldRank 0)))") ("2292#unseeded" "3823assume !!(-1 + ~v19~3 <= ~v14~3);assume ..." "2292#unseeded") ("2292#unseeded" "3547assume #t~ret133 != 0;havoc #t~ret133;ca..." "2292#unseeded") ("2292#unseeded" "3820assume !!(2 <= ~v30~3);assume !!(~v30~3 ..." "2292#unseeded") ("2292#unseeded" "3556assume !!(2 <= ~v20~3);" "2292#unseeded") ("2292#unseeded" "3558assume !!(~v20~3 <= 2);" "2292#unseeded") ("2292#unseeded" "3919assume #t~ret86 != 0;havoc #t~ret86;~v2~..." "2292#unseeded") ("2292#unseeded" "3798assume !!(~v14~3 <= ~v15~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3554assume !!(1 + ~v20~3 <= ~v22~3);~v35~3 :..." "2292#unseeded") ("2292#unseeded" "3564assume !!(~v18~3 <= ~v28~3);" "2292#unseeded") ("2292#unseeded" "3566assume !!(~v28~3 <= ~v18~3);" "2292#unseeded") ("2292#unseeded" "3560assume !!(~v30~3 <= ~v22~3);" "2292#unseeded") ("2292#unseeded" "3908assume !!(~v16~3 <= -1 + ~v15~3);assume ..." "2292#unseeded") ("2292#unseeded" "3562assume !!(~v22~3 <= ~v30~3);" "2292#unseeded") ("2292#unseeded" "3572assume !!(~v28~3 <= ~v35~3);" "2292#unseeded") ("2292#unseeded" "3930assume !!(2 <= ~v30~3);call #t~ret89 := ..." "2292#unseeded") ("2292#unseeded" "3776assume !!(0 <= -1 * ~v14~3 + ~v15~3);ass..." "2292#unseeded") ("2292#unseeded" "3779assume !!(~v29~3 <= ~v36~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3180assume !!(~v35~3 <= ~v28~3);assume !!(1 ..." "2292#unseeded") ("2292#unseeded" "3574assume !!(~v35~3 <= ~v28~3);" "2292#unseeded") ("2292#unseeded" "3568assume !!(~v18~3 <= ~v35~3);" "2292#unseeded") ("2292#unseeded" "3570assume !!(~v35~3 <= ~v18~3);" "2292#unseeded") ("2292#unseeded" "3782assume !!(~v29~3 <= ~v38~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3785assume !!(~v29~3 <= ~v31~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3922assume #t~ret88 != 0;havoc #t~ret88;assu..." "2292#unseeded") ("2292#unseeded" "2694call ULTIMATE.init();assume true;Return ..." "2292#unseeded") ("2292#unseeded" "3173assume !!(~v35~3 <= ~v18~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3170assume !!(~v28~3 <= ~v18~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3788assume !!(~v36~3 <= ~v38~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3577assume !!(1 <= ~v22~3);assume !!(2 <= ~v..." "2292#unseeded") ("2292#unseeded" "3791assume !!(~v17~3 <= ~v39~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3767assume #t~ret155 != 0;havoc #t~ret155;~v..." "2292#unseeded") ("2292#unseeded" "2914assume #t~ret80 != 0;havoc #t~ret80;call..." "2292#unseeded") ("2292#unseeded" "3886assume !!(0 <= ~v17~3);assume !!(~v17~3 ..." "2292#unseeded") ("2292#unseeded" "3643call #t~ret60 := nondet_bool();havoc ~a~..." "2292#unseeded") ("2292#unseeded" "2917assume !!(~v20~3 <= 0);assume !!(0 <= ~v..." "2292#unseeded") ("2292#unseeded" "3883assume #t~ret83 != 0;havoc #t~ret83;~v1~..." "2292#unseeded") ("2292#unseeded" "2920assume !!(~v18~3 <= 0);assume !!(~v30~3 ..." "2292#unseeded") ("2292#unseeded" "3637assume !!(1 + ~v21~3 <= ~v22~3);call #t~..." "2292#unseeded") ("2292#unseeded" "3773assume !!(0 <= ~v39~3);assume !!(~v39~3 ..." "2292#unseeded") ("2292#unseeded" "3770assume !!(0 <= ~v17~3);assume !!(~v17~3 ..." "2292#unseeded") ("2292#unseeded" "2926assume !!(~v22~3 <= ~v30~3);call #t~ret1..." "2292#unseeded") ("2292#unseeded" "3901assume !!(~v17~3 <= ~v39~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3898assume !!(~v36~3 <= ~v38~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3623assume !!(~v21~3 <= -1 + ~v20~3);assume ..." "2292#unseeded") ("2292#unseeded" "3892assume !!(~v29~3 <= ~v36~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3620assume !!(~v20~3 <= 1 + ~v21~3);assume !..." "2292#unseeded") ("2292#unseeded" "3895assume !!(~v29~3 <= ~v38~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3755assume !!(~v30~3 <= ~v20~3);assume !!(0 ..." "2292#unseeded") ("2292#unseeded" "3889assume !!(0 <= ~v39~3);assume !!(~v39~3 ..." "2292#unseeded") ("2292#unseeded" "3617assume !!(0 <= ~v20~3);call #t~ret77 := ..." "2292#unseeded") ("2292#unseeded" "3871assume #t~ret53 != 0;havoc #t~ret53;assu..." "2292#unseeded") ("2292#unseeded" "3718assume !!(1 <= ~v30~3);assume !!(2 <= ~v..." "2292#unseeded") ("2292#unseeded" "3599call #t~ret60 := nondet_bool();havoc ~a~..." "2292#unseeded") ("2292#unseeded" "3712assume !!(~v17~3 <= ~v39~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "3715assume !!(~v38~3 <= ~v37~3);assume !!(~v..." "2292#unseeded") ("2292#unseeded" "2901call #t~ret0 := nondet();havoc ~a~1;#res..." "2292#unseeded") ("3770#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3944assume !!(~v16~3 <= ~v15~3);call #t~ret9..." "3770#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3770#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3871assume #t~ret53 != 0;havoc #t~ret53;assu..." "2298#(or unseeded (and (> oldRank (+ main_~v15~3 (- 2))) (>= oldRank 0)))") ("3770#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3828call #t~ret40 := nondet_bool();havoc ~a~..." "3770#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") ("3770#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))" "3834assume !(#t~ret40 != 0);havoc #t~ret40;c..." "3770#(and (<= main_~v16~3 oldRank) (<= main_~v15~3 oldRank) (<= main_~v16~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 1)) (<= main_~v15~3 (+ oldRank 2)))") }, returnTransitions = { } );