YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: 0, arg2 -> 0, arg3 -> 0, arg4 -> undef4, arg5 -> undef5}> 0, arg4 -> 0, arg5 -> 0}> 19) /\ (1 = arg3) /\ (arg4 = arg5), par{arg2 -> (arg2 + 1), arg3 -> (arg2 + 1), arg4 -> undef14, arg5 -> undef15}> (arg2 + 1), arg3 -> (arg2 + 1), arg4 -> undef19, arg5 -> undef20}> undef27) /\ (arg4 < 20) /\ (0 = arg3) /\ (arg4 = arg5), par{arg3 -> 0, arg4 -> (arg4 + 1), arg5 -> (arg4 + 1)}> 0, arg4 -> (arg4 + 1), arg5 -> (arg4 + 1)}> 19) /\ (0 = arg3) /\ (arg4 = arg5), par{arg1 -> (arg1 + 1), arg2 -> (arg2 + 1), arg3 -> (arg2 + 1), arg4 -> undef38, arg5 -> undef39}> 1, arg5 -> arg4}> undef45, arg2 -> undef46, arg3 -> undef47, arg4 -> undef48, arg5 -> undef49}> Fresh variables: undef4, undef5, undef14, undef15, undef19, undef20, undef26, undef27, undef33, undef34, undef38, undef39, undef45, undef46, undef47, undef48, undef49, Undef variables: undef4, undef5, undef14, undef15, undef19, undef20, undef26, undef27, undef33, undef34, undef38, undef39, undef45, undef46, undef47, undef48, undef49, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 19) /\ (1 = arg3) /\ (arg4 = arg5) /\ ((arg2 + 1) < 20) /\ ((arg2 + 1) = (arg2 + 1)), par{arg2 -> (arg2 + 1), arg3 -> 0, arg4 -> 0, arg5 -> 0}> (arg2 + 1), arg3 -> 0, arg4 -> 0, arg5 -> 0}> undef27) /\ (arg4 < 20) /\ (0 = arg3) /\ (arg4 = arg5), par{arg3 -> 0, arg4 -> (arg4 + 1), arg5 -> (arg4 + 1)}> 0, arg4 -> (arg4 + 1), arg5 -> (arg4 + 1)}> 19) /\ (0 = arg3) /\ (arg4 = arg5) /\ ((arg2 + 1) < 20) /\ ((arg2 + 1) = (arg2 + 1)), par{arg1 -> (arg1 + 1), arg2 -> (arg2 + 1), arg3 -> 0, arg4 -> 0, arg5 -> 0}> 1, arg5 -> arg4}> Fresh variables: undef4, undef5, undef14, undef15, undef19, undef20, undef26, undef27, undef33, undef34, undef38, undef39, undef45, undef46, undef47, undef48, undef49, Undef variables: undef4, undef5, undef14, undef15, undef19, undef20, undef26, undef27, undef33, undef34, undef38, undef39, undef45, undef46, undef47, undef48, undef49, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: 1 + arg2, arg3 -> 0, arg4 -> 0, arg5 -> 0, rest remain the same}> 1 + arg2, arg3 -> 0, arg4 -> 0, arg5 -> 0, rest remain the same}> 0, arg4 -> 1 + arg4, arg5 -> 1 + arg4, rest remain the same}> 0, arg4 -> 1 + arg4, arg5 -> 1 + arg4, rest remain the same}> 1 + arg1, arg2 -> 1 + arg2, arg3 -> 0, arg4 -> 0, arg5 -> 0, rest remain the same}> 1, arg5 -> arg4, rest remain the same}> Variables: arg2, arg3, arg4, arg5, arg1 Precedence: Graph 0 Graph 1 Map Locations to Subgraph: ( 0 , 0 ) ( 3 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.061872 Some transition disabled by a set of invariant(s): Invariant at l3: arg3 + arg5 <= 20 Strengthening and disabling transitions... > It's unfeasible. Removing transition: 1 + arg2, arg3 -> 0, arg4 -> 0, arg5 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + arg2, arg3 -> 0, arg4 -> 0, arg5 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, arg4 -> 1 + arg4, arg5 -> 1 + arg4, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, arg4 -> 1 + arg4, arg5 -> 1 + arg4, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + arg1, arg2 -> 1 + arg2, arg3 -> 0, arg4 -> 0, arg5 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, arg5 -> arg4, rest remain the same}> Checking unfeasibility... Time used: 0.120657 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005209s Ranking function: 399 - 20*arg2 - arg3 - arg4 New Graphs: Transitions: 1 + arg2, arg3 -> 0, arg4 -> 0, arg5 -> 0, rest remain the same}> 1 + arg1, arg2 -> 1 + arg2, arg3 -> 0, arg4 -> 0, arg5 -> 0, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000967s Ranking function: 1405 - arg1 - 77*arg2 - 77*arg3 New Graphs: Transitions: 1 + arg2, arg3 -> 0, arg4 -> 0, arg5 -> 0, rest remain the same}> Variables: arg2, arg3, arg4, arg5 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000522s Ranking function: -1 + arg3 New Graphs: Program Terminates