NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: 1}> (~(1) + Count^0)}> 1}> (0 + undef1247), ret_nondet4146^0 -> undef1247}> (0 + undef1392), requestRescan___014^0 -> 0, ret_nondet3742^0 -> undef1392, ret_nondet3944^0 -> undef1393, tmp___018^0 -> (0 + undef1393)}> undef1587, tmp___119^0 -> (0 + undef1587)}> undef1880, tmp___220^0 -> (0 + undef1880)}> (0 + undef2122), ret_nondet2732^0 -> undef2122}> undef2317, tmp___322^0 -> (0 + undef2317)}> 20}> undef2610, tmp___423^0 -> (0 + undef2610)}> undef2662, ret_nondet3136^0 -> undef2663, status___011^0 -> (0 + undef2662), tmp15^0 -> (0 + undef2663)}> 5}> (0 + undef2951), ret_nondet2126^0 -> undef2951}> (0 + undef2999), PowerStateIsAC^0 -> (0 + undef3014), WarmPollPeriod^0 -> (0 + undef3001), polling^0 -> (0 + undef3013), ret_nondet1010^0 -> undef2999, ret_nondet22^0 -> undef3001, ret_nondet44^0 -> undef3012, ret_nondet66^0 -> undef3013, ret_nondet88^0 -> undef3014, status^0 -> (0 + undef3012)}> Fresh variables: undef1247, undef1392, undef1393, undef1587, undef1880, undef2122, undef2317, undef2610, undef2662, undef2663, undef2951, undef2999, undef3001, undef3012, undef3013, undef3014, Undef variables: undef1247, undef1392, undef1393, undef1587, undef1880, undef2122, undef2317, undef2610, undef2662, undef2663, undef2951, undef2999, undef3001, undef3012, undef3013, undef3014, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: (0 + undef2999)}> (0 + undef2999)}> (0 + undef2999)}> (0 + undef2122)}> (0 + undef2122)}> (0 + undef2999)}> (0 + undef2122)}> (0 + undef2122)}> (0 + undef2999)}> (0 + undef2999)}> (0 + undef2122)}> (0 + undef2122)}> (0 + undef2999)}> (0 + undef2122)}> (0 + undef2122)}> (0 + undef2999)}> (0 + undef2999)}> (0 + undef2122)}> (0 + undef2122)}> (0 + undef2999)}> (0 + undef2122)}> (0 + undef2122)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (0 + undef1587)}> (0 + undef1587)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0), requestRescan___014^0 -> 1}> (~(1) + Count^0), requestRescan___014^0 -> 1}> (~(1) + Count^0), requestRescan___014^0 -> 1}> (~(1) + Count^0), requestRescan___014^0 -> 1}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0), requestRescan___014^0 -> 1}> (~(1) + Count^0), requestRescan___014^0 -> 1}> (~(1) + Count^0), requestRescan___014^0 -> 1}> (~(1) + Count^0), requestRescan___014^0 -> 1}> (~(1) + Count^0)}> (~(1) + Count^0)}> (~(1) + Count^0), requestRescan___014^0 -> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> 0}> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> 0}> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> (~(1) + Count^0), requestRescan___014^0 -> 0}> Fresh variables: undef1247, undef1392, undef1393, undef1587, undef1880, undef2122, undef2317, undef2610, undef2662, undef2663, undef2951, undef2999, undef3001, undef3012, undef3013, undef3014, Undef variables: undef1247, undef1392, undef1393, undef1587, undef1880, undef2122, undef2317, undef2610, undef2662, undef2663, undef2951, undef2999, undef3001, undef3012, undef3013, undef3014, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> undef1587, rest remain the same}> undef1587, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> 0, rest remain the same}> 0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> 0, rest remain the same}> 0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> Variables: Count^0, x2833^0, x3035^0, x3237^0, tmp___119^0, x3439^0, mfg16^0, requestRescan___014^0, mdl17^0, x3641^0, x3843^0, x4045^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 undef2122, rest remain the same}> undef2122, rest remain the same}> undef2122, rest remain the same}> undef2122, rest remain the same}> undef2122, rest remain the same}> undef2122, rest remain the same}> undef2122, rest remain the same}> undef2122, rest remain the same}> undef2122, rest remain the same}> undef2122, rest remain the same}> undef2122, rest remain the same}> undef2122, rest remain the same}> Graph 2 undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 5 , 2 ) ( 7 , 1 ) ( 15 , 1 ) ( 20 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.309507 Some transition disabled by a set of invariant(s): Invariant at l15: requestRescan___014^0 <= 0 Invariant at l20: 1 + x2833^0 + x3439^0 <= tmp___119^0 + x3035^0 Strengthening and disabling transitions... > It's unfeasible. Removing transition: -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> Checking unfeasibility... Time used: 0.227479 Some transition disabled by a set of invariant(s): Invariant at l15: 0 <= requestRescan___014^0 Invariant at l20: tmp___119^0 <= x3439^0 Strengthening and disabling transitions... > It's unfeasible. Removing transition: -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + Count^0, requestRescan___014^0 -> 0, rest remain the same}> Checking unfeasibility... Time used: 0.245921 Checking conditional termination of SCC {l7, l15, l20}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.020534s Ranking function: -7 + Count^0 - 3*x2833^0 - 3*x3035^0 New Graphs: Transitions: -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> Variables: Count^0, mdl17^0, mfg16^0, requestRescan___014^0, tmp___119^0, x2833^0, x3035^0, x3237^0, x3439^0, x3641^0, x3843^0, x4045^0 Checking conditional termination of SCC {l7, l15}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.050818s Ranking function: 2 + Count^0 + x2833^0 - x3035^0 - 3*x3439^0 New Graphs: Transitions: -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> Variables: Count^0, mdl17^0, mfg16^0, requestRescan___014^0, tmp___119^0, x2833^0, x3035^0, x3237^0, x3439^0, x3641^0, x3843^0, x4045^0 Checking conditional termination of SCC {l7, l15}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.027783s Ranking function: -7 + Count^0 - 5*x2833^0 - x3035^0 - 7*x3237^0 New Graphs: Transitions: -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> Variables: Count^0, mdl17^0, mfg16^0, requestRescan___014^0, tmp___119^0, x2833^0, x3035^0, x3237^0, x3439^0, x3641^0, x3843^0, x4045^0 Checking conditional termination of SCC {l7, l15}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.019669s Ranking function: -2 + Count^0 + x2833^0 - x3035^0 New Graphs: Transitions: -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> Variables: Count^0, mdl17^0, mfg16^0, requestRescan___014^0, tmp___119^0, x2833^0, x3035^0, x3237^0, x3439^0, x3641^0, x3843^0, x4045^0 Checking conditional termination of SCC {l7, l15}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.016735s Ranking function: -7 + Count^0 - 3*x2833^0 - x3035^0 + x3237^0 + x3439^0 - 3*x3843^0 - 3*x4045^0 New Graphs: Transitions: 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> Variables: Count^0, mdl17^0, mfg16^0, requestRescan___014^0, tmp___119^0, x2833^0, x3035^0, x3237^0, x3439^0, x3641^0, x3843^0, x4045^0 Checking conditional termination of SCC {l7, l15}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.014974s Ranking function: -7 + Count^0 - 5*x2833^0 - x3035^0 + x3237^0 + x3439^0 + x3843^0 New Graphs: Transitions: 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> Variables: Count^0, mdl17^0, mfg16^0, requestRescan___014^0, tmp___119^0, x2833^0, x3035^0, x3237^0, x3439^0, x3641^0, x3843^0, x4045^0 Checking conditional termination of SCC {l7, l15}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.013656s Ranking function: -7 + Count^0 - 5*x2833^0 - x3035^0 + x3237^0 + x3439^0 - x3843^0 New Graphs: Transitions: 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, rest remain the same}> Variables: Count^0, mdl17^0, mfg16^0, requestRescan___014^0, tmp___119^0, x2833^0, x3035^0, x3237^0, x3439^0, x3641^0, x3843^0, x4045^0 Checking conditional termination of SCC {l7, l15}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011901s Ranking function: Count^0 - 7*mfg16^0 New Graphs: Transitions: -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 0, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> -1 + Count^0, requestRescan___014^0 -> 1, tmp___119^0 -> undef1587, rest remain the same}> Variables: Count^0, mdl17^0, mfg16^0, requestRescan___014^0, tmp___119^0, x2833^0, x3035^0, x3237^0, x3439^0, x3641^0, x3843^0, x4045^0 Checking conditional termination of SCC {l7}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.060960s Ranking function: -2 + Count^0 New Graphs: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.009228 > No variable changes in termination graph. Checking conditional unfeasibility... Termination failed. Trying to show unreachability... Proving unreachability of entry: undef2999, rest remain the same}> LOG: CALL check - Post:1 <= 0 - Process 1 * Exit transition: undef2999, rest remain the same}> * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002214s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002277s Cannot prove unreachability Proving non-termination of subgraph 2 Transitions: Variables: Checking conditional non-termination of SCC {l5}... > No exit transition to close. Calling reachability with... Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: Transition: undef2999, rest remain the same}> Conditions: OPEN EXITS: undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> undef2999, rest remain the same}> > Conditions are reachable! Program does NOT terminate