YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l103, true>
<l1, l2, true, par{i3742^0 -> 1}>
<l3, l1, (17 <= (0 + n3540^0))>
<l3, l1, ((1 + n3540^0) <= 16)>
<l3, l4, ((0 + n3540^0) <= 16) /\ (16 <= (0 + n3540^0))>
<l5, l3, (10 <= (0 + n3540^0))>
<l5, l3, ((1 + n3540^0) <= 9)>
<l5, l4, ((0 + n3540^0) <= 9) /\ (9 <= (0 + n3540^0))>
<l6, l5, (3 <= (0 + n3540^0))>
<l6, l5, ((1 + n3540^0) <= 2)>
<l6, l4, ((0 + n3540^0) <= 2) /\ (2 <= (0 + n3540^0))>
<l7, l8, true>
<l4, l7, (undef1309 = 0), par{j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, tmp4146^0 -> (0 + undef1309), tmp___04247^0 -> undef1309}>
<l9, l6, (2 <= (0 + n3540^0))>
<l9, l6, ((1 + n3540^0) <= 1)>
<l9, l4, ((0 + n3540^0) <= 1) /\ (1 <= (0 + n3540^0))>
<l10, l11, (17 <= (0 + i12^0))>
<l10, l9, ((0 + i12^0) <= 16) /\ (undef1827 = undef1827), par{n3540^0 -> (0 + i12^0), pg18^0 -> undef1827}>
<l12, l13, true>
<l14, l15, true, par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0), tmp___020^0 -> (0 + ret_getbit3439^0)}>
<l16, l14, true, par{ret_getbit3439^0 -> (0 + tmp___03338^0)}>
<l17, l16, true, par{tmp___03338^0 -> 0}>
<l17, l16, true, par{tmp___03338^0 -> 1}>
<l18, l19, true>
<l20, l14, true, par{ret_getbit3439^0 -> (0 + tmp3237^0)}>
<l21, l20, true, par{tmp3237^0 -> 0}>
<l21, l20, true, par{tmp3237^0 -> 1}>
<l22, l17, ((1 + nbits3136^0) <= (0 + bitno3035^0))>
<l22, l21, ((0 + bitno3035^0) <= (0 + nbits3136^0))>
<l23, l24, true>
<l25, l22, (undef3223 = undef3223), par{bitno3035^0 -> undef3223, nbits3136^0 -> 32, source2934^0 -> (0 + key7^0), tmp19^0 -> (0 + ret_getbit2833^0)}>
<l26, l25, true, par{ret_getbit2833^0 -> (0 + tmp___02732^0)}>
<l27, l26, true, par{tmp___02732^0 -> 0}>
<l27, l26, true, par{tmp___02732^0 -> 1}>
<l28, l25, true, par{ret_getbit2833^0 -> (0 + tmp2631^0)}>
<l29, l30, true>
<l31, l28, true, par{tmp2631^0 -> 0}>
<l31, l28, true, par{tmp2631^0 -> 1}>
<l32, l27, ((1 + nbits2530^0) <= (0 + bitno2429^0))>
<l32, l31, ((0 + bitno2429^0) <= (0 + nbits2530^0))>
<l33, l34, ((1 + j13^0) <= 1), par{i12^0 -> 1}>
<l33, l32, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443), par{bitno2429^0 -> undef4443, nbits2530^0 -> 32, source2328^0 -> (0 + key7^0)}>
<l35, l36, true>
<l37, l15, true, par{j13^0 -> 28, k14^0 -> 56}>
<l38, l39, true, par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0), tmp___727^0 -> (0 + ret_getbit9398^0)}>
<l40, l38, true, par{ret_getbit9398^0 -> (0 + tmp___09297^0)}>
<l41, l40, true, par{tmp___09297^0 -> 0}>
<l41, l40, true, par{tmp___09297^0 -> 1}>
<l42, l38, true, par{ret_getbit9398^0 -> (0 + tmp9196^0)}>
<l43, l42, true, par{tmp9196^0 -> 0}>
<l43, l42, true, par{tmp9196^0 -> 1}>
<l44, l37, true>
<l44, l37, true>
<l44, l11, true>
<l45, l41, ((1 + nbits9095^0) <= (0 + bitno8994^0))>
<l45, l43, ((0 + bitno8994^0) <= (0 + nbits9095^0))>
<l46, l45, (undef6213 = undef6213) /\ (undef6113 = undef6113), par{bitno8994^0 -> undef6113, nbits9095^0 -> 32, source8893^0 -> (0 + itmp17^0), tmp___525^0 -> (0 + ret_getbit8792^0), tmp___626^0 -> undef6213}>
<l47, l46, true, par{ret_getbit8792^0 -> (0 + tmp___08691^0)}>
<l48, l47, true, par{tmp___08691^0 -> 0}>
<l48, l47, true, par{tmp___08691^0 -> 1}>
<l49, l46, true, par{ret_getbit8792^0 -> (0 + tmp8590^0)}>
<l50, l49, true, par{tmp8590^0 -> 0}>
<l50, l49, true, par{tmp8590^0 -> 1}>
<l51, l48, ((1 + nbits8489^0) <= (0 + bitno8388^0))>
<l51, l50, ((0 + bitno8388^0) <= (0 + nbits8489^0))>
<l52, l53, ((1 + j13^0) <= 1)>
<l52, l51, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222), par{bitno8388^0 -> undef7222, nbits8489^0 -> 32, source8287^0 -> (0 + itmp17^0), tmp___424^0 -> undef7319}>
<l54, l55, true>
<l56, l54, true, par{j7378^0 -> (~(1) + j7378^0)}>
<l57, l56, true, par{tmp___38186^0 -> 0}>
<l57, l56, true, par{tmp___38186^0 -> 1}>
<l58, l44, (33 <= (0 + j13^0))>
<l58, l59, ((0 + j13^0) <= 32) /\ (undef7942 = undef7942), par{j13^0 -> (1 + j13^0), shifter16^0 -> undef7942}>
<l55, l18, ((1 + j7378^0) <= 1) /\ (undef8004 = undef8004), par{i12^0 -> (1 + i12^0), ic15^0 -> undef8004}>
<l55, l57, (1 <= (0 + j7378^0)) /\ (undef8203 = undef8203), par{tmp___28085^0 -> undef8203}>
<l36, l54, ((1 + jj6974^0) <= 1), par{j7378^0 -> 32}>
<l36, l35, (1 <= (0 + jj6974^0)) /\ (undef8355 = undef8355) /\ (undef8347 = undef8347) /\ (undef8339 = undef8339) /\ (undef8348 = undef8348) /\ (undef8437 = undef8437) /\ (undef8352 = undef8352), par{icol7176^0 -> undef8339, irow7075^0 -> undef8347, iss7277^0 -> undef8348, itmp6570^0 -> undef8352, j7378^0 -> undef8355, jj6974^0 -> (~(1) + jj6974^0)}>
<l30, l35, (5 <= (0 + j7378^0)), par{itmp6570^0 -> 0, jj6974^0 -> 8}>
<l30, l29, ((0 + j7378^0) <= 4) /\ (undef8563 = undef8563) /\ (undef8564 = undef8564), par{ietmp16671^0 -> undef8563, ietmp26772^0 -> undef8564, j7378^0 -> (1 + j7378^0), m7580^0 -> (1 + m7580^0)}>
<l60, l23, true, par{j7378^0 -> (~(1) + j7378^0), l7479^0 -> (~(1) + l7479^0), m7580^0 -> (~(1) + m7580^0)}>
<l61, l60, true, par{tmp___17984^0 -> 0}>
<l61, l60, true, par{tmp___17984^0 -> 1}>
<l62, l59, true, par{initflag^0 -> 0, j13^0 -> 2, shifter16^0 -> 1}>
<l63, l61, true>
<l64, l63, true, par{tmp___07883^0 -> 0}>
<l64, l63, true, par{tmp___07883^0 -> 1}>
<l65, l64, true>
<l66, l65, true, par{tmp7782^0 -> 0}>
<l66, l65, true, par{tmp7782^0 -> 1}>
<l67, l44, ((0 + initflag^0) <= 0) /\ (0 <= (0 + initflag^0))>
<l67, l62, (1 <= (0 + initflag^0))>
<l67, l62, ((1 + initflag^0) <= 0)>
<l24, l29, ((1 + j7378^0) <= 1) /\ (undef10117 = undef10117) /\ (undef10118 = undef10118), par{ietmp16671^0 -> undef10117, ietmp26772^0 -> undef10118, j7378^0 -> 1, m7580^0 -> 5}>
<l24, l66, (1 <= (0 + j7378^0))>
<l68, l69, true, par{ii11^0 -> (0 + i12^0)}>
<l69, l23, (undef10456 = undef10456) /\ (undef10469 = undef10469), par{ir6166^0 -> undef10456, j7378^0 -> 16, k6267^0 -> undef10469, l7479^0 -> 32, m7580^0 -> 48}>
<l70, l68, (2 <= (0 + isw9^0))>
<l70, l68, ((1 + isw9^0) <= 1)>
<l70, l69, ((0 + isw9^0) <= 1) /\ (1 <= (0 + isw9^0)), par{ii11^0 -> (17 + (~(1) * i12^0))}>
<l19, l39, (17 <= (0 + i12^0)) /\ (undef10891 = undef10891), par{ic15^0 -> undef10891, j13^0 -> 32, k14^0 -> 64, tmp___323^0 -> 0}>
<l19, l70, ((0 + i12^0) <= 16)>
<l71, l12, true, par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0), tmp___222^0 -> (0 + ret_getbit6065^0)}>
<l72, l71, true, par{ret_getbit6065^0 -> (0 + tmp___05964^0)}>
<l73, l72, true, par{tmp___05964^0 -> 0}>
<l73, l72, true, par{tmp___05964^0 -> 1}>
<l74, l71, true, par{ret_getbit6065^0 -> (0 + tmp5863^0)}>
<l75, l74, true, par{tmp5863^0 -> 0}>
<l75, l74, true, par{tmp5863^0 -> 1}>
<l76, l73, ((1 + nbits5762^0) <= (0 + bitno5661^0))>
<l76, l75, ((0 + bitno5661^0) <= (0 + nbits5762^0))>
<l77, l76, (undef12106 = undef12106), par{bitno5661^0 -> undef12106, nbits5762^0 -> 32, source5560^0 -> (0 + inp6^0), tmp___121^0 -> (0 + ret_getbit5459^0)}>
<l39, l52, true>
<l78, l77, true, par{ret_getbit5459^0 -> (0 + tmp___05358^0)}>
<l79, l78, true, par{tmp___05358^0 -> 0}>
<l79, l78, true, par{tmp___05358^0 -> 1}>
<l80, l77, true, par{ret_getbit5459^0 -> (0 + tmp5257^0)}>
<l81, l80, true, par{tmp5257^0 -> 0}>
<l81, l80, true, par{tmp5257^0 -> 1}>
<l82, l79, ((1 + nbits5156^0) <= (0 + bitno5055^0))>
<l82, l81, ((0 + bitno5055^0) <= (0 + nbits5156^0))>
<l13, l18, ((1 + j13^0) <= 1), par{i12^0 -> 1}>
<l13, l82, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326), par{bitno5055^0 -> undef13326, nbits5156^0 -> 32, source4954^0 -> (0 + inp6^0)}>
<l11, l12, true, par{j13^0 -> 32, k14^0 -> 64}>
<l83, l7, true, par{j3843^0 -> (~(1) + j3843^0), k3944^0 -> (~(1) + k3944^0), l4045^0 -> (~(1) + l4045^0), tmp___64853^0 -> (0 + ret_getbit111116^0)}>
<l84, l83, true, par{ret_getbit111116^0 -> (0 + tmp___0110115^0)}>
<l85, l84, true, par{tmp___0110115^0 -> 0}>
<l85, l84, true, par{tmp___0110115^0 -> 1}>
<l86, l83, true, par{ret_getbit111116^0 -> (0 + tmp109114^0)}>
<l87, l86, true, par{tmp109114^0 -> 0}>
<l87, l86, true, par{tmp109114^0 -> 1}>
<l88, l85, ((1 + nbits108113^0) <= (0 + bitno107112^0))>
<l88, l87, ((0 + bitno107112^0) <= (0 + nbits108113^0))>
<l89, l88, (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28, source106111^0 -> (0 + icd^0), tmp___44651^0 -> (0 + ret_getbit105110^0), tmp___54752^0 -> undef14649}>
<l90, l89, true, par{ret_getbit105110^0 -> (0 + tmp___0104109^0)}>
<l91, l90, true, par{tmp___0104109^0 -> 0}>
<l91, l90, true, par{tmp___0104109^0 -> 1}>
<l92, l89, true, par{ret_getbit105110^0 -> (0 + tmp103108^0)}>
<l93, l92, true, par{tmp103108^0 -> 0}>
<l93, l92, true, par{tmp103108^0 -> 1}>
<l94, l91, ((1 + nbits102107^0) <= (0 + bitno101106^0))>
<l94, l93, ((0 + bitno101106^0) <= (0 + nbits102107^0))>
<l95, l94, (undef15643 = undef15643) /\ (undef15542 = undef15542), par{bitno101106^0 -> undef15542, nbits102107^0 -> 28, source100105^0 -> (0 + icd^0), tmp___24449^0 -> (0 + ret_getbit99104^0), tmp___34550^0 -> undef15643}>
<l59, l58, true>
<l96, l95, true, par{ret_getbit99104^0 -> (0 + tmp___098103^0)}>
<l97, l96, true, par{tmp___098103^0 -> 0}>
<l97, l96, true, par{tmp___098103^0 -> 1}>
<l98, l95, true, par{ret_getbit99104^0 -> (0 + tmp97102^0)}>
<l99, l98, true, par{tmp97102^0 -> 0}>
<l99, l98, true, par{tmp97102^0 -> 1}>
<l100, l97, ((1 + nbits96101^0) <= (0 + bitno95100^0))>
<l100, l99, ((0 + bitno95100^0) <= (0 + nbits96101^0))>
<l15, l33, true>
<l8, l34, ((1 + j3843^0) <= 1), par{i12^0 -> (1 + i12^0)}>
<l8, l100, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882), par{bitno95100^0 -> undef16882, nbits96101^0 -> 28, source9499^0 -> (0 + icd^0), tmp___14348^0 -> undef16969}>
<l34, l10, true>
<l101, l4, (3 <= (0 + i3742^0))>
<l101, l2, ((0 + i3742^0) <= 2), par{i3742^0 -> (1 + i3742^0)}>
<l2, l101, true>
<l102, l67, (undef17453 = (0 + value^0)), par{inp6^0 -> (0 + inp^0), isw9^0 -> (0 + undef17453), isw^0 -> undef17453, key7^0 -> (0 + key^0), newkey_promoted_2^0 -> (0 + value^0)}>
<l103, l102, true>

Fresh variables:
undef1309, undef1827, undef3223, undef4443, undef6113, undef6213, undef7222, undef7319, undef7942, undef8004, undef8203, undef8339, undef8347, undef8348, undef8352, undef8355, undef8437, undef8563, undef8564, undef10117, undef10118, undef10456, undef10469, undef10891, undef12106, undef13326, undef14544, undef14649, undef15542, undef15643, undef16882, undef16969, undef17453, 

Undef variables:
undef1309, undef1827, undef3223, undef4443, undef6113, undef6213, undef7222, undef7319, undef7942, undef8004, undef8203, undef8339, undef8347, undef8348, undef8352, undef8355, undef8437, undef8563, undef8564, undef10117, undef10118, undef10456, undef10469, undef10891, undef12106, undef13326, undef14544, undef14649, undef15542, undef15643, undef16882, undef16969, undef17453, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l15, (inp^0 = (0 + inp^0)) /\ (isw9^0 = (0 + undef17453)) /\ (key^0 = (0 + key^0)) /\ (undef17453 = (0 + value^0)) /\ ((0 + initflag^0) <= 0) /\ (0 <= (0 + initflag^0)), par{j13^0 -> 28, k14^0 -> 56}>
<l0, l15, (inp^0 = (0 + inp^0)) /\ (isw9^0 = (0 + undef17453)) /\ (key^0 = (0 + key^0)) /\ (undef17453 = (0 + value^0)) /\ ((0 + initflag^0) <= 0) /\ (0 <= (0 + initflag^0)), par{j13^0 -> 28, k14^0 -> 56}>
<l0, l12, (inp^0 = (0 + inp^0)) /\ (isw9^0 = (0 + undef17453)) /\ (key^0 = (0 + key^0)) /\ (undef17453 = (0 + value^0)) /\ ((0 + initflag^0) <= 0) /\ (0 <= (0 + initflag^0)), par{j13^0 -> 32, k14^0 -> 64}>
<l0, l59, (inp^0 = (0 + inp^0)) /\ (isw9^0 = (0 + undef17453)) /\ (key^0 = (0 + key^0)) /\ (undef17453 = (0 + value^0)) /\ (1 <= (0 + initflag^0)), par{initflag^0 -> 0, j13^0 -> 2}>
<l0, l59, (inp^0 = (0 + inp^0)) /\ (isw9^0 = (0 + undef17453)) /\ (key^0 = (0 + key^0)) /\ (undef17453 = (0 + value^0)) /\ ((1 + initflag^0) <= 0), par{initflag^0 -> 0, j13^0 -> 2}>
<l2, l7, (3 <= (0 + i3742^0)) /\ (undef1309 = 0), par{j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48}>
<l2, l2, ((0 + i3742^0) <= 2), par{i3742^0 -> (1 + i3742^0)}>
<l5, l2, (10 <= (0 + n3540^0)) /\ (17 <= (0 + n3540^0)), par{i3742^0 -> 1}>
<l5, l2, (10 <= (0 + n3540^0)) /\ ((1 + n3540^0) <= 16), par{i3742^0 -> 1}>
<l5, l7, (10 <= (0 + n3540^0)) /\ ((0 + n3540^0) <= 16) /\ (16 <= (0 + n3540^0)) /\ (undef1309 = 0), par{j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48}>
<l5, l2, ((1 + n3540^0) <= 9) /\ ((1 + n3540^0) <= 16), par{i3742^0 -> 1}>
<l5, l7, ((0 + n3540^0) <= 9) /\ (9 <= (0 + n3540^0)) /\ (undef1309 = 0), par{j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48}>
<l7, l12, ((1 + j3843^0) <= 1) /\ (17 <= (0 + (1 + i12^0))), par{i12^0 -> (1 + i12^0), j13^0 -> 32, k14^0 -> 64}>
<l7, l5, ((1 + j3843^0) <= 1) /\ ((0 + (1 + i12^0)) <= 16) /\ (undef1827 = undef1827) /\ (2 <= (0 + (0 + (1 + i12^0)))) /\ (3 <= (0 + (0 + (1 + i12^0)))), par{i12^0 -> (1 + i12^0), n3540^0 -> (0 + (1 + i12^0))}>
<l7, l7, ((1 + j3843^0) <= 1) /\ ((0 + (1 + i12^0)) <= 16) /\ (undef1827 = undef1827) /\ (2 <= (0 + (0 + (1 + i12^0)))) /\ ((0 + (0 + (1 + i12^0))) <= 2) /\ (2 <= (0 + (0 + (1 + i12^0)))) /\ (undef1309 = 0), par{i12^0 -> (1 + i12^0), j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, n3540^0 -> (0 + (1 + i12^0))}>
<l7, l5, ((1 + j3843^0) <= 1) /\ ((0 + (1 + i12^0)) <= 16) /\ (undef1827 = undef1827) /\ ((1 + (0 + (1 + i12^0))) <= 1) /\ ((1 + (0 + (1 + i12^0))) <= 2), par{i12^0 -> (1 + i12^0), n3540^0 -> (0 + (1 + i12^0))}>
<l7, l7, ((1 + j3843^0) <= 1) /\ ((0 + (1 + i12^0)) <= 16) /\ (undef1827 = undef1827) /\ ((0 + (0 + (1 + i12^0))) <= 1) /\ (1 <= (0 + (0 + (1 + i12^0)))) /\ (undef1309 = 0), par{i12^0 -> (1 + i12^0), j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, n3540^0 -> (0 + (1 + i12^0))}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((1 + 28) <= (0 + undef16882)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((1 + 28) <= (0 + undef15542)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((1 + 28) <= (0 + undef16882)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((1 + 28) <= (0 + undef15542)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((1 + 28) <= (0 + undef16882)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((0 + undef15542) <= (0 + 28)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((1 + 28) <= (0 + undef16882)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((0 + undef15542) <= (0 + 28)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((1 + 28) <= (0 + undef16882)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((1 + 28) <= (0 + undef15542)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((1 + 28) <= (0 + undef16882)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((1 + 28) <= (0 + undef15542)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((1 + 28) <= (0 + undef16882)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((0 + undef15542) <= (0 + 28)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((1 + 28) <= (0 + undef16882)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((0 + undef15542) <= (0 + 28)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((0 + undef16882) <= (0 + 28)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((1 + 28) <= (0 + undef15542)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((0 + undef16882) <= (0 + 28)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((1 + 28) <= (0 + undef15542)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((0 + undef16882) <= (0 + 28)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((0 + undef15542) <= (0 + 28)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((0 + undef16882) <= (0 + 28)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((0 + undef15542) <= (0 + 28)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((0 + undef16882) <= (0 + 28)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((1 + 28) <= (0 + undef15542)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((0 + undef16882) <= (0 + 28)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((1 + 28) <= (0 + undef15542)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((0 + undef16882) <= (0 + 28)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((0 + undef15542) <= (0 + 28)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l7, l88, (1 <= (0 + j3843^0)) /\ (undef16969 = undef16969) /\ (undef16882 = undef16882) /\ ((0 + undef16882) <= (0 + 28)) /\ (undef15643 = undef15643) /\ (undef15542 = undef15542) /\ ((0 + undef15542) <= (0 + 28)) /\ (undef14649 = undef14649) /\ (undef14544 = undef14544), par{bitno107112^0 -> undef14544, nbits108113^0 -> 28}>
<l12, l23, ((1 + j13^0) <= 1) /\ ((0 + 1) <= 16) /\ (2 <= (0 + isw9^0)) /\ (undef10456 = undef10456) /\ (undef10469 = undef10469), par{i12^0 -> 1, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48}>
<l12, l23, ((1 + j13^0) <= 1) /\ ((0 + 1) <= 16) /\ ((1 + isw9^0) <= 1) /\ (undef10456 = undef10456) /\ (undef10469 = undef10469), par{i12^0 -> 1, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48}>
<l12, l23, ((1 + j13^0) <= 1) /\ ((0 + 1) <= 16) /\ ((0 + isw9^0) <= 1) /\ (1 <= (0 + isw9^0)) /\ (undef10456 = undef10456) /\ (undef10469 = undef10469), par{i12^0 -> 1, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((1 + 32) <= (0 + undef13326)) /\ (undef12106 = undef12106) /\ ((1 + 32) <= (0 + undef12106)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((1 + 32) <= (0 + undef13326)) /\ (undef12106 = undef12106) /\ ((1 + 32) <= (0 + undef12106)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((1 + 32) <= (0 + undef13326)) /\ (undef12106 = undef12106) /\ ((0 + undef12106) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((1 + 32) <= (0 + undef13326)) /\ (undef12106 = undef12106) /\ ((0 + undef12106) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((1 + 32) <= (0 + undef13326)) /\ (undef12106 = undef12106) /\ ((1 + 32) <= (0 + undef12106)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((1 + 32) <= (0 + undef13326)) /\ (undef12106 = undef12106) /\ ((1 + 32) <= (0 + undef12106)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((1 + 32) <= (0 + undef13326)) /\ (undef12106 = undef12106) /\ ((0 + undef12106) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((1 + 32) <= (0 + undef13326)) /\ (undef12106 = undef12106) /\ ((0 + undef12106) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((0 + undef13326) <= (0 + 32)) /\ (undef12106 = undef12106) /\ ((1 + 32) <= (0 + undef12106)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((0 + undef13326) <= (0 + 32)) /\ (undef12106 = undef12106) /\ ((1 + 32) <= (0 + undef12106)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((0 + undef13326) <= (0 + 32)) /\ (undef12106 = undef12106) /\ ((0 + undef12106) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((0 + undef13326) <= (0 + 32)) /\ (undef12106 = undef12106) /\ ((0 + undef12106) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((0 + undef13326) <= (0 + 32)) /\ (undef12106 = undef12106) /\ ((1 + 32) <= (0 + undef12106)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((0 + undef13326) <= (0 + 32)) /\ (undef12106 = undef12106) /\ ((1 + 32) <= (0 + undef12106)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((0 + undef13326) <= (0 + 32)) /\ (undef12106 = undef12106) /\ ((0 + undef12106) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l12, l12, (1 <= (0 + j13^0)) /\ (undef13326 = undef13326) /\ ((0 + undef13326) <= (0 + 32)) /\ (undef12106 = undef12106) /\ ((0 + undef12106) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l7, ((1 + j13^0) <= 1) /\ ((0 + 1) <= 16) /\ (undef1827 = undef1827) /\ ((0 + (0 + 1)) <= 1) /\ (1 <= (0 + (0 + 1))) /\ (undef1309 = 0), par{i12^0 -> 1, j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, n3540^0 -> (0 + 1)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((1 + 32) <= (0 + undef4443)) /\ (undef3223 = undef3223) /\ ((1 + 32) <= (0 + undef3223)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((1 + 32) <= (0 + undef4443)) /\ (undef3223 = undef3223) /\ ((1 + 32) <= (0 + undef3223)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((1 + 32) <= (0 + undef4443)) /\ (undef3223 = undef3223) /\ ((0 + undef3223) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((1 + 32) <= (0 + undef4443)) /\ (undef3223 = undef3223) /\ ((0 + undef3223) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((1 + 32) <= (0 + undef4443)) /\ (undef3223 = undef3223) /\ ((1 + 32) <= (0 + undef3223)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((1 + 32) <= (0 + undef4443)) /\ (undef3223 = undef3223) /\ ((1 + 32) <= (0 + undef3223)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((1 + 32) <= (0 + undef4443)) /\ (undef3223 = undef3223) /\ ((0 + undef3223) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((1 + 32) <= (0 + undef4443)) /\ (undef3223 = undef3223) /\ ((0 + undef3223) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((0 + undef4443) <= (0 + 32)) /\ (undef3223 = undef3223) /\ ((1 + 32) <= (0 + undef3223)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((0 + undef4443) <= (0 + 32)) /\ (undef3223 = undef3223) /\ ((1 + 32) <= (0 + undef3223)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((0 + undef4443) <= (0 + 32)) /\ (undef3223 = undef3223) /\ ((0 + undef3223) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((0 + undef4443) <= (0 + 32)) /\ (undef3223 = undef3223) /\ ((0 + undef3223) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((0 + undef4443) <= (0 + 32)) /\ (undef3223 = undef3223) /\ ((1 + 32) <= (0 + undef3223)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((0 + undef4443) <= (0 + 32)) /\ (undef3223 = undef3223) /\ ((1 + 32) <= (0 + undef3223)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((0 + undef4443) <= (0 + 32)) /\ (undef3223 = undef3223) /\ ((0 + undef3223) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l15, l15, (1 <= (0 + j13^0)) /\ (undef4443 = undef4443) /\ ((0 + undef4443) <= (0 + 32)) /\ (undef3223 = undef3223) /\ ((0 + undef3223) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l23, l29, ((1 + j7378^0) <= 1) /\ (undef10117 = undef10117) /\ (undef10118 = undef10118), par{j7378^0 -> 1, m7580^0 -> 5}>
<l23, l23, (1 <= (0 + j7378^0)), par{j7378^0 -> (~(1) + j7378^0), l7479^0 -> (~(1) + l7479^0), m7580^0 -> (~(1) + m7580^0)}>
<l23, l23, (1 <= (0 + j7378^0)), par{j7378^0 -> (~(1) + j7378^0), l7479^0 -> (~(1) + l7479^0), m7580^0 -> (~(1) + m7580^0)}>
<l23, l23, (1 <= (0 + j7378^0)), par{j7378^0 -> (~(1) + j7378^0), l7479^0 -> (~(1) + l7479^0), m7580^0 -> (~(1) + m7580^0)}>
<l23, l23, (1 <= (0 + j7378^0)), par{j7378^0 -> (~(1) + j7378^0), l7479^0 -> (~(1) + l7479^0), m7580^0 -> (~(1) + m7580^0)}>
<l23, l23, (1 <= (0 + j7378^0)), par{j7378^0 -> (~(1) + j7378^0), l7479^0 -> (~(1) + l7479^0), m7580^0 -> (~(1) + m7580^0)}>
<l23, l23, (1 <= (0 + j7378^0)), par{j7378^0 -> (~(1) + j7378^0), l7479^0 -> (~(1) + l7479^0), m7580^0 -> (~(1) + m7580^0)}>
<l23, l23, (1 <= (0 + j7378^0)), par{j7378^0 -> (~(1) + j7378^0), l7479^0 -> (~(1) + l7479^0), m7580^0 -> (~(1) + m7580^0)}>
<l23, l23, (1 <= (0 + j7378^0)), par{j7378^0 -> (~(1) + j7378^0), l7479^0 -> (~(1) + l7479^0), m7580^0 -> (~(1) + m7580^0)}>
<l29, l35, (5 <= (0 + j7378^0)), par{jj6974^0 -> 8}>
<l29, l29, ((0 + j7378^0) <= 4) /\ (undef8563 = undef8563) /\ (undef8564 = undef8564), par{j7378^0 -> (1 + j7378^0), m7580^0 -> (1 + m7580^0)}>
<l35, l54, ((1 + jj6974^0) <= 1), par{j7378^0 -> 32}>
<l35, l35, (1 <= (0 + jj6974^0)) /\ (undef8355 = undef8355) /\ (undef8347 = undef8347) /\ (undef8339 = undef8339) /\ (undef8348 = undef8348) /\ (undef8437 = undef8437) /\ (undef8352 = undef8352), par{j7378^0 -> undef8355, jj6974^0 -> (~(1) + jj6974^0)}>
<l39, l53, ((1 + j13^0) <= 1)>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((1 + 32) <= (0 + undef7222)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((1 + 32) <= (0 + undef6113)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((1 + 32) <= (0 + undef7222)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((1 + 32) <= (0 + undef6113)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((1 + 32) <= (0 + undef7222)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((0 + undef6113) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((1 + 32) <= (0 + undef7222)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((0 + undef6113) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((1 + 32) <= (0 + undef7222)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((1 + 32) <= (0 + undef6113)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((1 + 32) <= (0 + undef7222)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((1 + 32) <= (0 + undef6113)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((1 + 32) <= (0 + undef7222)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((0 + undef6113) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((1 + 32) <= (0 + undef7222)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((0 + undef6113) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((0 + undef7222) <= (0 + 32)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((1 + 32) <= (0 + undef6113)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((0 + undef7222) <= (0 + 32)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((1 + 32) <= (0 + undef6113)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((0 + undef7222) <= (0 + 32)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((0 + undef6113) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((0 + undef7222) <= (0 + 32)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((0 + undef6113) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((0 + undef7222) <= (0 + 32)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((1 + 32) <= (0 + undef6113)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((0 + undef7222) <= (0 + 32)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((1 + 32) <= (0 + undef6113)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((0 + undef7222) <= (0 + 32)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((0 + undef6113) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l39, l39, (1 <= (0 + j13^0)) /\ (undef7319 = undef7319) /\ (undef7222 = undef7222) /\ ((0 + undef7222) <= (0 + 32)) /\ (undef6213 = undef6213) /\ (undef6113 = undef6113) /\ ((0 + undef6113) <= (0 + 32)), par{j13^0 -> (~(1) + j13^0), k14^0 -> (~(1) + k14^0)}>
<l54, l39, ((1 + j7378^0) <= 1) /\ (undef8004 = undef8004) /\ (17 <= (0 + (1 + i12^0))) /\ (undef10891 = undef10891), par{i12^0 -> (1 + i12^0), j13^0 -> 32, k14^0 -> 64}>
<l54, l23, ((1 + j7378^0) <= 1) /\ (undef8004 = undef8004) /\ ((0 + (1 + i12^0)) <= 16) /\ (2 <= (0 + isw9^0)) /\ (undef10456 = undef10456) /\ (undef10469 = undef10469), par{i12^0 -> (1 + i12^0), j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48}>
<l54, l23, ((1 + j7378^0) <= 1) /\ (undef8004 = undef8004) /\ ((0 + (1 + i12^0)) <= 16) /\ ((1 + isw9^0) <= 1) /\ (undef10456 = undef10456) /\ (undef10469 = undef10469), par{i12^0 -> (1 + i12^0), j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48}>
<l54, l23, ((1 + j7378^0) <= 1) /\ (undef8004 = undef8004) /\ ((0 + (1 + i12^0)) <= 16) /\ ((0 + isw9^0) <= 1) /\ (1 <= (0 + isw9^0)) /\ (undef10456 = undef10456) /\ (undef10469 = undef10469), par{i12^0 -> (1 + i12^0), j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48}>
<l54, l54, (1 <= (0 + j7378^0)) /\ (undef8203 = undef8203), par{j7378^0 -> (~(1) + j7378^0)}>
<l54, l54, (1 <= (0 + j7378^0)) /\ (undef8203 = undef8203), par{j7378^0 -> (~(1) + j7378^0)}>
<l59, l15, (33 <= (0 + j13^0)), par{j13^0 -> 28, k14^0 -> 56}>
<l59, l15, (33 <= (0 + j13^0)), par{j13^0 -> 28, k14^0 -> 56}>
<l59, l12, (33 <= (0 + j13^0)), par{j13^0 -> 32, k14^0 -> 64}>
<l59, l59, ((0 + j13^0) <= 32) /\ (undef7942 = undef7942), par{j13^0 -> (1 + j13^0)}>
<l88, l7, ((1 + nbits108113^0) <= (0 + bitno107112^0)), par{j3843^0 -> (~(1) + j3843^0), k3944^0 -> (~(1) + k3944^0), l4045^0 -> (~(1) + l4045^0)}>
<l88, l7, ((1 + nbits108113^0) <= (0 + bitno107112^0)), par{j3843^0 -> (~(1) + j3843^0), k3944^0 -> (~(1) + k3944^0), l4045^0 -> (~(1) + l4045^0)}>
<l88, l7, ((0 + bitno107112^0) <= (0 + nbits108113^0)), par{j3843^0 -> (~(1) + j3843^0), k3944^0 -> (~(1) + k3944^0), l4045^0 -> (~(1) + l4045^0)}>
<l88, l7, ((0 + bitno107112^0) <= (0 + nbits108113^0)), par{j3843^0 -> (~(1) + j3843^0), k3944^0 -> (~(1) + k3944^0), l4045^0 -> (~(1) + l4045^0)}>

Fresh variables:
undef1309, undef1827, undef3223, undef4443, undef6113, undef6213, undef7222, undef7319, undef7942, undef8004, undef8203, undef8339, undef8347, undef8348, undef8352, undef8355, undef8437, undef8563, undef8564, undef10117, undef10118, undef10456, undef10469, undef10891, undef12106, undef13326, undef14544, undef14649, undef15542, undef15643, undef16882, undef16969, undef17453, 

Undef variables:
undef1309, undef1827, undef3223, undef4443, undef6113, undef6213, undef7222, undef7319, undef7942, undef8004, undef8203, undef8339, undef8347, undef8348, undef8352, undef8355, undef8437, undef8563, undef8564, undef10117, undef10118, undef10456, undef10469, undef10891, undef12106, undef13326, undef14544, undef14649, undef15542, undef15643, undef16882, undef16969, undef17453, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

*************************************************************
*******************************************************************************************
***********************       WORKING TRANSITION SYSTEM (DAG)       ***********************
*******************************************************************************************

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l59, l59, j13^0 <= 32, {j13^0 -> 1 + j13^0, rest remain the same}>
Variables:
j13^0

Graph 2:
Transitions:
<l15, l15, 1 <= j13^0 /\ 33 <= undef3223 /\ 33 <= undef4443, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef3223 /\ 33 <= undef4443, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef4443 /\ undef3223 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef4443 /\ undef3223 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef3223 /\ 33 <= undef4443, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef3223 /\ 33 <= undef4443, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef4443 /\ undef3223 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef4443 /\ undef3223 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef3223 /\ undef4443 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef3223 /\ undef4443 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ undef3223 <= 32 /\ undef4443 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ undef3223 <= 32 /\ undef4443 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef3223 /\ undef4443 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ 33 <= undef3223 /\ undef4443 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ undef3223 <= 32 /\ undef4443 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l15, l15, 1 <= j13^0 /\ undef3223 <= 32 /\ undef4443 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
Variables:
j13^0, k14^0

Graph 3:
Transitions:
<l2, l7, 3 <= i3742^0 /\ undef1309 = 0, {j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, rest remain the same}>
<l2, l2, i3742^0 <= 2, {i3742^0 -> 1 + i3742^0, rest remain the same}>
<l5, l2, 17 <= n3540^0, {i3742^0 -> 1, rest remain the same}>
<l5, l2, 10 <= n3540^0 /\ n3540^0 <= 15, {i3742^0 -> 1, rest remain the same}>
<l5, l7, undef1309 = 0 /\ n3540^0 = 16, {j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, rest remain the same}>
<l5, l2, n3540^0 <= 8, {i3742^0 -> 1, rest remain the same}>
<l5, l7, undef1309 = 0 /\ n3540^0 = 9, {j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, rest remain the same}>
<l7, l5, j3843^0 <= 0 /\ 2 <= i12^0 /\ i12^0 <= 15, {i12^0 -> 1 + i12^0, n3540^0 -> 1 + i12^0, rest remain the same}>
<l7, l7, j3843^0 <= 0 /\ undef1309 = 0 /\ i12^0 = 1, {i12^0 -> 1 + i12^0, j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, n3540^0 -> 1 + i12^0, rest remain the same}>
<l7, l5, 1 + i12^0 <= 0 /\ j3843^0 <= 0, {i12^0 -> 1 + i12^0, n3540^0 -> 1 + i12^0, rest remain the same}>
<l7, l7, j3843^0 <= 0 /\ i12^0 = 0 /\ undef1309 = 0, {i12^0 -> 1 + i12^0, j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, n3540^0 -> 1 + i12^0, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l88, l7, 1 + nbits108113^0 <= bitno107112^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
<l88, l7, 1 + nbits108113^0 <= bitno107112^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
<l88, l7, bitno107112^0 <= nbits108113^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
<l88, l7, bitno107112^0 <= nbits108113^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
Variables:
i3742^0, n3540^0, i12^0, j3843^0, bitno107112^0, k3944^0, l4045^0, nbits108113^0

Graph 4:
Transitions:
<l12, l12, 1 <= j13^0 /\ 33 <= undef12106 /\ 33 <= undef13326, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef12106 /\ 33 <= undef13326, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef13326 /\ undef12106 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef13326 /\ undef12106 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef12106 /\ 33 <= undef13326, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef12106 /\ 33 <= undef13326, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef13326 /\ undef12106 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef13326 /\ undef12106 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef12106 /\ undef13326 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef12106 /\ undef13326 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ undef12106 <= 32 /\ undef13326 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ undef12106 <= 32 /\ undef13326 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef12106 /\ undef13326 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ 33 <= undef12106 /\ undef13326 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ undef12106 <= 32 /\ undef13326 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l12, l12, 1 <= j13^0 /\ undef12106 <= 32 /\ undef13326 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
Variables:
j13^0, k14^0

Graph 5:
Transitions:
<l23, l29, j7378^0 <= 0, {j7378^0 -> 1, m7580^0 -> 5, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l29, l35, 5 <= j7378^0, {jj6974^0 -> 8, rest remain the same}>
<l29, l29, j7378^0 <= 4, {j7378^0 -> 1 + j7378^0, m7580^0 -> 1 + m7580^0, rest remain the same}>
<l35, l54, jj6974^0 <= 0, {j7378^0 -> 32, rest remain the same}>
<l35, l35, 1 <= jj6974^0, {j7378^0 -> undef8355, jj6974^0 -> -1 + jj6974^0, rest remain the same}>
<l54, l23, j7378^0 <= 0 /\ 2 <= isw9^0 /\ i12^0 <= 15, {i12^0 -> 1 + i12^0, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48, rest remain the same}>
<l54, l23, isw9^0 <= 0 /\ j7378^0 <= 0 /\ i12^0 <= 15, {i12^0 -> 1 + i12^0, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48, rest remain the same}>
<l54, l23, j7378^0 <= 0 /\ i12^0 <= 15 /\ isw9^0 = 1, {i12^0 -> 1 + i12^0, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48, rest remain the same}>
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
Variables:
j7378^0, l7479^0, m7580^0, jj6974^0, i12^0, isw9^0

Graph 6:
Transitions:
<l39, l39, 1 <= j13^0 /\ 33 <= undef6113 /\ 33 <= undef7222, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef6113 /\ 33 <= undef7222, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef7222 /\ undef6113 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef7222 /\ undef6113 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef6113 /\ 33 <= undef7222, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef6113 /\ 33 <= undef7222, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef7222 /\ undef6113 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef7222 /\ undef6113 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef6113 /\ undef7222 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef6113 /\ undef7222 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ undef6113 <= 32 /\ undef7222 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ undef6113 <= 32 /\ undef7222 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef6113 /\ undef7222 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ 33 <= undef6113 /\ undef7222 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ undef6113 <= 32 /\ undef7222 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
<l39, l39, 1 <= j13^0 /\ undef6113 <= 32 /\ undef7222 <= 32, {j13^0 -> -1 + j13^0, k14^0 -> -1 + k14^0, rest remain the same}>
Variables:
j13^0, k14^0

Graph 7:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l59, 1 <= initflag^0 /\ isw9^0 = undef17453 /\ value^0 = undef17453, {initflag^0 -> 0, j13^0 -> 2, rest remain the same}>
<l0, l59, 1 + initflag^0 <= 0 /\ isw9^0 = undef17453 /\ value^0 = undef17453, {initflag^0 -> 0, j13^0 -> 2, rest remain the same}>

Graph 2
<l0, l15, initflag^0 = 0 /\ isw9^0 = undef17453 /\ value^0 = undef17453, {j13^0 -> 28, k14^0 -> 56, rest remain the same}>
<l0, l15, initflag^0 = 0 /\ isw9^0 = undef17453 /\ value^0 = undef17453, {j13^0 -> 28, k14^0 -> 56, rest remain the same}>
<l59, l15, 33 <= j13^0, {j13^0 -> 28, k14^0 -> 56, rest remain the same}>
<l59, l15, 33 <= j13^0, {j13^0 -> 28, k14^0 -> 56, rest remain the same}>

Graph 3
<l15, l7, j13^0 <= 0 /\ undef1309 = 0, {i12^0 -> 1, j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, n3540^0 -> 1, rest remain the same}>

Graph 4
<l0, l12, initflag^0 = 0 /\ isw9^0 = undef17453 /\ value^0 = undef17453, {j13^0 -> 32, k14^0 -> 64, rest remain the same}>
<l7, l12, j3843^0 <= 0 /\ 16 <= i12^0, {i12^0 -> 1 + i12^0, j13^0 -> 32, k14^0 -> 64, rest remain the same}>
<l59, l12, 33 <= j13^0, {j13^0 -> 32, k14^0 -> 64, rest remain the same}>

Graph 5
<l12, l23, j13^0 <= 0 /\ 2 <= isw9^0, {i12^0 -> 1, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48, rest remain the same}>
<l12, l23, isw9^0 <= 0 /\ j13^0 <= 0, {i12^0 -> 1, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48, rest remain the same}>
<l12, l23, j13^0 <= 0 /\ isw9^0 = 1, {i12^0 -> 1, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48, rest remain the same}>

Graph 6
<l54, l39, j7378^0 <= 0 /\ 16 <= i12^0, {i12^0 -> 1 + i12^0, j13^0 -> 32, k14^0 -> 64, rest remain the same}>

Graph 7
<l39, l53, j13^0 <= 0, {all remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 2 , 3 )
( 5 , 3 )
( 7 , 3 )
( 12 , 4 )
( 15 , 2 )
( 23 , 5 )
( 29 , 5 )
( 35 , 5 )
( 39 , 6 )
( 53 , 7 )
( 54 , 5 )
( 59 , 1 )
( 88 , 3 )

*******************************************************************************************
********************************    CHECKING ASSERTIONS    ********************************
*******************************************************************************************

Proving termination of subgraph 0
Proving termination of subgraph 1
Checking unfeasibility...
Time used: 0.007151

Checking conditional termination of SCC {l59}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005007s
Ranking function: 32 - j13^0
New Graphs: 
Proving termination of subgraph 2
Checking unfeasibility...
Time used: 0.044893

Checking conditional termination of SCC {l15}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010453s
Ranking function: -1 + j13^0
New Graphs: 
Proving termination of subgraph 3
Checking unfeasibility...
Time used: 0.412724
Some transition disabled by a set of invariant(s):
Invariant at l2: 1 <= i12^0
Invariant at l5: 1 <= i12^0
Invariant at l7: 1 <= i12^0
Invariant at l88: 1 <= i12^0

Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l7, l7, j3843^0 <= 0 /\ i12^0 = 0 /\ undef1309 = 0, {i12^0 -> 1 + i12^0, j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, n3540^0 -> 1 + i12^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l2, l7, 1 <= i12^0 /\ 3 <= i3742^0 /\ undef1309 = 0, {j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l2, l2, 1 <= i12^0 /\ i3742^0 <= 2, {i3742^0 -> 1 + i3742^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l2, 1 <= i12^0 /\ 17 <= n3540^0, {i3742^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l2, 1 <= i12^0 /\ 10 <= n3540^0 /\ n3540^0 <= 15, {i3742^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l7, 1 <= i12^0 /\ undef1309 = 0 /\ n3540^0 = 16, {j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l2, 1 <= i12^0 /\ n3540^0 <= 8, {i3742^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l7, 1 <= i12^0 /\ undef1309 = 0 /\ n3540^0 = 9, {j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l5, j3843^0 <= 0 /\ 2 <= i12^0 /\ i12^0 <= 15, {i12^0 -> 1 + i12^0, n3540^0 -> 1 + i12^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l7, j3843^0 <= 0 /\ undef1309 = 0 /\ i12^0 = 1, {i12^0 -> 1 + i12^0, j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, n3540^0 -> 1 + i12^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l7, l5, 1 + i12^0 <= 0 /\ j3843^0 <= 0, {i12^0 -> 1 + i12^0, n3540^0 -> 1 + i12^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
Checking unfeasibility...
Time used: 4.00203

Checking conditional termination of SCC {l2, l5, l7, l88}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.022665s
Ranking function: 30 - 2*i12^0
New Graphs: 
Transitions:
<l2, l2, 1 <= i12^0 /\ i3742^0 <= 2, {i3742^0 -> 1 + i3742^0, rest remain the same}>
Variables:
i12^0, i3742^0
Transitions:
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
<l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
<l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
<l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
Variables:
bitno107112^0, i12^0, j3843^0, k3944^0, l4045^0, nbits108113^0
Checking conditional termination of SCC {l2}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003863s
Ranking function: 2 - i3742^0
New Graphs: 
Transitions:
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
<l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
<l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
<l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
<l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
Variables:
bitno107112^0, i12^0, j3843^0, k3944^0, l4045^0, nbits108113^0
Checking conditional termination of SCC {l7, l88}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008036s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.078423s
Trying to remove transition: <l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.053243s
Time used: 0.050019
Trying to remove transition: <l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.058669s
Time used: 0.056796
Trying to remove transition: <l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.059187s
Time used: 0.057345
Trying to remove transition: <l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.059365s
Time used: 0.05757
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.057297s
Time used: 0.05558
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051285s
Time used: 0.049847
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.054176s
Time used: 0.052675
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.049042s
Time used: 0.047647
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051664s
Time used: 0.050297
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.058223s
Time used: 0.056899
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050566s
Time used: 0.049189
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050257s
Time used: 0.04895
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.052863s
Time used: 0.051584
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050665s
Time used: 0.049326
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050595s
Time used: 0.049299
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.054479s
Time used: 0.053195
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.048997s
Time used: 0.047679
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.054061s
Time used: 0.052786
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.053266s
Time used: 0.051947
Trying to remove transition: <l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051415s
Time used: 0.050091
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.004532s
Time used: 1.00317

LOG: SAT solveNonLinear - Elapsed time: 1.004532s
Cost: 0; Total time: 1.00317
Termination implied by a set of invariant(s):
Invariant at l2: 1 <= i3742^0
Invariant at l5: n3540^0 <= i12^0
Invariant at l7: 0 <= 1 + i12^0
Invariant at l88: 0 <= 1 + i12^0 + j3843^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l2, l7, 1 <= i12^0 /\ 3 <= i3742^0 /\ undef1309 = 0, {j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l2, l2, 1 <= i12^0 /\ 1 <= i3742^0 /\ i3742^0 <= 2, {i3742^0 -> 1 + i3742^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l2, 1 <= i12^0 /\ 17 <= n3540^0 /\ n3540^0 <= i12^0, {i3742^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l2, 1 <= i12^0 /\ n3540^0 <= i12^0 /\ 10 <= n3540^0 /\ n3540^0 <= 15, {i3742^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l7, 1 <= i12^0 /\ n3540^0 <= i12^0 /\ undef1309 = 0 /\ n3540^0 = 16, {j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l2, 1 <= i12^0 /\ n3540^0 <= i12^0 /\ n3540^0 <= 8, {i3742^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l5, l7, 1 <= i12^0 /\ n3540^0 <= i12^0 /\ undef1309 = 0 /\ n3540^0 = 9, {j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l5, j3843^0 <= 0 /\ 2 <= i12^0 /\ i12^0 <= 15, {i12^0 -> 1 + i12^0, n3540^0 -> 1 + i12^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l7, j3843^0 <= 0 /\ undef1309 = 0 /\ i12^0 = 1, {i12^0 -> 1 + i12^0, j3843^0 -> 16, k3944^0 -> 32, l4045^0 -> 48, n3540^0 -> 1 + i12^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0 /\ 0 <= 1 + i12^0 + j3843^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0 /\ 0 <= 1 + i12^0 + j3843^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0 /\ 0 <= 1 + i12^0 + j3843^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0 /\ 0 <= 1 + i12^0 + j3843^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ 29 <= undef16882, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef16882 /\ undef15542 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ 29 <= undef15542 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l7, l88, 1 <= i12^0 /\ 1 <= j3843^0 /\ undef15542 <= 28 /\ undef16882 <= 28, {bitno107112^0 -> undef14544, nbits108113^0 -> 28, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0 /\ 0 <= 1 + i12^0 + j3843^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 + nbits108113^0 <= bitno107112^0 /\ 1 <= i12^0 /\ 0 <= 1 + i12^0 + j3843^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0 /\ 0 <= 1 + i12^0 + j3843^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l88, l7, 1 <= i12^0 /\ bitno107112^0 <= nbits108113^0 /\ 0 <= 1 + i12^0 + j3843^0, {j3843^0 -> -1 + j3843^0, k3944^0 -> -1 + k3944^0, l4045^0 -> -1 + l4045^0, rest remain the same}>
Ranking function: 1 + i12^0 + j3843^0
New Graphs: 
INVARIANTS: 
2: 1 <= i3742^0 , 
5: n3540^0 <= i12^0 , 
7: 0 <= 1 + i12^0 , 
88: 0 <= 1 + i12^0 + j3843^0 , 
Quasi-INVARIANTS to narrow Graph: 
2: 
5: 
7: 
88: 
Proving termination of subgraph 4
Checking unfeasibility...
Time used: 0.045515

Checking conditional termination of SCC {l12}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.012365s
Ranking function: -1 + j13^0
New Graphs: 
Proving termination of subgraph 5
Checking unfeasibility...
Time used: 4.00457

Checking conditional termination of SCC {l23, l29, l35, l54}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.030530s
Ranking function: -49 - i12^0 + 32*isw9^0
New Graphs: 
Transitions:
<l23, l29, j7378^0 <= 0, {j7378^0 -> 1, m7580^0 -> 5, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l29, l35, 5 <= j7378^0, {jj6974^0 -> 8, rest remain the same}>
<l29, l29, j7378^0 <= 4, {j7378^0 -> 1 + j7378^0, m7580^0 -> 1 + m7580^0, rest remain the same}>
<l35, l54, jj6974^0 <= 0, {j7378^0 -> 32, rest remain the same}>
<l35, l35, 1 <= jj6974^0, {j7378^0 -> undef8355, jj6974^0 -> -1 + jj6974^0, rest remain the same}>
<l54, l23, isw9^0 <= 0 /\ j7378^0 <= 0 /\ i12^0 <= 15, {i12^0 -> 1 + i12^0, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48, rest remain the same}>
<l54, l23, j7378^0 <= 0 /\ i12^0 <= 15 /\ isw9^0 = 1, {i12^0 -> 1 + i12^0, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48, rest remain the same}>
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
Variables:
i12^0, isw9^0, j7378^0, jj6974^0, l7479^0, m7580^0
Checking conditional termination of SCC {l23, l29, l35, l54}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009178s
Ranking function: 15 - i12^0 - 32*isw9^0
New Graphs: 
Transitions:
<l23, l29, j7378^0 <= 0, {j7378^0 -> 1, m7580^0 -> 5, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l29, l35, 5 <= j7378^0, {jj6974^0 -> 8, rest remain the same}>
<l29, l29, j7378^0 <= 4, {j7378^0 -> 1 + j7378^0, m7580^0 -> 1 + m7580^0, rest remain the same}>
<l35, l54, jj6974^0 <= 0, {j7378^0 -> 32, rest remain the same}>
<l35, l35, 1 <= jj6974^0, {j7378^0 -> undef8355, jj6974^0 -> -1 + jj6974^0, rest remain the same}>
<l54, l23, j7378^0 <= 0 /\ i12^0 <= 15 /\ isw9^0 = 1, {i12^0 -> 1 + i12^0, j7378^0 -> 16, l7479^0 -> 32, m7580^0 -> 48, rest remain the same}>
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
Variables:
i12^0, isw9^0, j7378^0, jj6974^0, l7479^0, m7580^0
Checking conditional termination of SCC {l23, l29, l35, l54}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009146s
Ranking function: -2 - i12^0 + 17*isw9^0
New Graphs: 
Transitions:
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
<l23, l23, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, l7479^0 -> -1 + l7479^0, m7580^0 -> -1 + m7580^0, rest remain the same}>
Variables:
j7378^0, l7479^0, m7580^0
Transitions:
<l29, l29, j7378^0 <= 4, {j7378^0 -> 1 + j7378^0, m7580^0 -> 1 + m7580^0, rest remain the same}>
Variables:
j7378^0, m7580^0
Transitions:
<l35, l35, 1 <= jj6974^0, {j7378^0 -> undef8355, jj6974^0 -> -1 + jj6974^0, rest remain the same}>
Variables:
j7378^0, jj6974^0
Transitions:
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
Variables:
j7378^0
Checking conditional termination of SCC {l23}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006577s
Ranking function: -1 + j7378^0
New Graphs: 
Transitions:
<l29, l29, j7378^0 <= 4, {j7378^0 -> 1 + j7378^0, m7580^0 -> 1 + m7580^0, rest remain the same}>
Variables:
j7378^0, m7580^0
Transitions:
<l35, l35, 1 <= jj6974^0, {j7378^0 -> undef8355, jj6974^0 -> -1 + jj6974^0, rest remain the same}>
Variables:
j7378^0, jj6974^0
Transitions:
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
Variables:
j7378^0
Checking conditional termination of SCC {l29}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005036s
Ranking function: 4 - j7378^0
New Graphs: 
Transitions:
<l35, l35, 1 <= jj6974^0, {j7378^0 -> undef8355, jj6974^0 -> -1 + jj6974^0, rest remain the same}>
Variables:
j7378^0, jj6974^0
Transitions:
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
Variables:
j7378^0
Checking conditional termination of SCC {l35}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004908s
Ranking function: -1 + jj6974^0
New Graphs: 
Transitions:
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
<l54, l54, 1 <= j7378^0, {j7378^0 -> -1 + j7378^0, rest remain the same}>
Variables:
j7378^0
Checking conditional termination of SCC {l54}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005261s
Ranking function: -1 + j7378^0
New Graphs: 
Proving termination of subgraph 6
Checking unfeasibility...
Time used: 0.039392

Checking conditional termination of SCC {l39}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013368s
Ranking function: -1 + j13^0
New Graphs: 
Proving termination of subgraph 7
Analyzing SCC {l53}...
No cycles found.

Program Terminates