NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: (0 + i3^0)}> (~(1) + j5^0)}> undef104}> 1}> (~(1) + j5^0)}> (1 + i3^0)}> (~(1) + j5^0)}> (1 + i3^0)}> undef263, i3^0 -> (1 + l6^0), j5^0 -> (0 + ir4^0)}> undef286}> undef325}> undef351}> undef401, temp9^0 -> undef403}> 1}> undef442}> (0 + undef577), flag211^0 -> undef577, ir4^0 -> (0 + undef584), k1^0 -> (0 + __const_10^0), l6^0 -> 1, n2^0 -> undef584}> Fresh variables: undef104, undef263, undef286, undef325, undef351, undef401, undef403, undef442, undef577, undef584, Undef variables: undef104, undef263, undef286, undef325, undef351, undef401, undef403, undef442, undef577, undef584, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 1}> 1}> 1}> (~(1) + j5^0)}> (0 + i3^0)}> (~(1) + j5^0)}> (~(1) + j5^0), l6^0 -> (0 + i3^0)}> (0 + i3^0)}> (~(1) + j5^0)}> (~(1) + j5^0), l6^0 -> (0 + i3^0)}> (1 + i3^0)}> 1, l6^0 -> (0 + i3^0)}> 1, ir4^0 -> (~(1) + j5^0)}> 1, ir4^0 -> (~(1) + j5^0), l6^0 -> (0 + i3^0)}> (1 + i3^0)}> (~(1) + j5^0)}> (1 + l6^0), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + (1 + l6^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + (1 + l6^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + (1 + l6^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0)}> (1 + l6^0), ir4^0 -> (~(1) + (0 + ir4^0)), j5^0 -> (0 + ir4^0), l6^0 -> (0 + (1 + l6^0))}> (1 + (1 + l6^0)), j5^0 -> (0 + ir4^0)}> Fresh variables: undef104, undef263, undef286, undef325, undef351, undef401, undef403, undef442, undef577, undef584, Undef variables: undef104, undef263, undef286, undef325, undef351, undef401, undef403, undef442, undef577, undef584, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> -1 + j5^0, rest remain the same}> i3^0, rest remain the same}> -1 + j5^0, rest remain the same}> -1 + j5^0, l6^0 -> i3^0, rest remain the same}> i3^0, rest remain the same}> -1 + j5^0, rest remain the same}> -1 + j5^0, l6^0 -> i3^0, rest remain the same}> 1 + i3^0, rest remain the same}> 1, l6^0 -> i3^0, rest remain the same}> 1, ir4^0 -> -1 + j5^0, rest remain the same}> 1, ir4^0 -> -1 + j5^0, l6^0 -> i3^0, rest remain the same}> 1 + i3^0, rest remain the same}> -1 + j5^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> Variables: flag10^0, ir4^0, l6^0, j5^0, flag211^0, i3^0, k1^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ( 10 , 1 ) ( 12 , 1 ) ( 17 , 1 ) ( 24 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.895842 Some transition disabled by a set of invariant(s): Invariant at l2: 0 <= 1 + flag211^0 Invariant at l10: 0 <= flag211^0 Invariant at l12: 0 <= flag211^0 Invariant at l17: 0 <= 1 + flag211^0 Strengthening and disabling transitions... > It's unfeasible. Removing transition: i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + j5^0, l6^0 -> i3^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 + j5^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 + j5^0, l6^0 -> i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, l6^0 -> i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, ir4^0 -> -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, ir4^0 -> -1 + j5^0, l6^0 -> i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> Checking unfeasibility... Time used: 0.503702 Some transition disabled by a set of invariant(s): Invariant at l2: flag211^0 <= 1 Invariant at l10: flag211^0 <= 0 Invariant at l12: flag211^0 <= 0 Invariant at l17: flag211^0 <= 1 Strengthening and disabling transitions... > It's unfeasible. Removing transition: -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: i3^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 + j5^0, l6^0 -> i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, l6^0 -> i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, ir4^0 -> -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, ir4^0 -> -1 + j5^0, l6^0 -> i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> Checking unfeasibility... Time used: 0.693862 Some transition disabled by a set of invariant(s): Invariant at l2: 0 <= flag211^0 Invariant at l10: 1 + j5^0 <= flag211^0 + ir4^0 Invariant at l12: j5^0 <= ir4^0 Invariant at l17: 0 <= flag211^0 Strengthening and disabling transitions... > It's unfeasible. Removing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, l6^0 -> i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, ir4^0 -> -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, ir4^0 -> -1 + j5^0, l6^0 -> i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + j5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> Checking unfeasibility... Time used: 4.00161 Checking conditional termination of SCC {l2, l10, l12, l17}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.015288s Ranking function: 2 - flag211^0 + ir4^0 - k1^0 New Graphs: Transitions: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> -1 + j5^0, rest remain the same}> 1 + i3^0, rest remain the same}> 1, l6^0 -> i3^0, rest remain the same}> 1 + i3^0, rest remain the same}> -1 + j5^0, rest remain the same}> Variables: flag10^0, flag211^0, i3^0, ir4^0, j5^0, k1^0, l6^0 Checking conditional termination of SCC {l2, l10, l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009928s Ranking function: 1 - flag10^0 - flag211^0 New Graphs: Transitions: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> -1 + j5^0, rest remain the same}> 1 + i3^0, rest remain the same}> 1, l6^0 -> i3^0, rest remain the same}> 1 + i3^0, rest remain the same}> -1 + j5^0, rest remain the same}> Variables: flag10^0, flag211^0, i3^0, ir4^0, j5^0, k1^0, l6^0 Checking conditional termination of SCC {l2, l10, l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008797s Ranking function: 1 - flag211^0 New Graphs: Transitions: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> Variables: flag10^0, flag211^0, i3^0, ir4^0, j5^0, k1^0, l6^0 Transitions: -1 + j5^0, rest remain the same}> 1 + i3^0, rest remain the same}> 1 + i3^0, rest remain the same}> -1 + j5^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004154s Ranking function: -2 - flag10^0 - flag211^0 + (3 / 2)*ir4^0 + (~(3) / 2)*l6^0 New Graphs: Transitions: -1 + j5^0, rest remain the same}> 1 + i3^0, rest remain the same}> 1 + i3^0, rest remain the same}> -1 + j5^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l10, l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001704s Ranking function: -1 - flag211^0 - i3^0 + ir4^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Transitions: -1 + j5^0, rest remain the same}> Variables: flag211^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000465s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001157s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004551s Time used: 0.004462 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.318144s Time used: 0.31724 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001510s Time used: 1.0015 LOG: SAT solveNonLinear - Elapsed time: 1.319654s Cost: 1; Total time: 1.31874 Failed at location 2: flag211^0 + ir4^0 <= l6^0 Before Improving: Quasi-invariant at l2: flag211^0 + ir4^0 <= l6^0 Quasi-invariant at l10: ir4^0 <= flag211^0 + j5^0 Quasi-invariant at l12: 1 + ir4^0 <= j5^0 Quasi-invariant at l17: 1 + flag211^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011177s Remaining time after improvement: 0.995145 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: flag211^0 + ir4^0 <= l6^0 Quasi-invariant at l10: ir4^0 <= flag211^0 + j5^0 Quasi-invariant at l12: 1 + ir4^0 <= j5^0 Quasi-invariant at l17: 1 + flag211^0 <= 0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: -1 + j5^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 + i3^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, l6^0 -> i3^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, ir4^0 -> -1 + j5^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, ir4^0 -> -1 + j5^0, l6^0 -> i3^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 + i3^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 + j5^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: 1 + i3^0, rest remain the same}> New Graphs: Transitions: -1 + j5^0, rest remain the same}> Variables: flag211^0, ir4^0, j5^0 Checking conditional termination of SCC {l10}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000330s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001105s Trying to remove transition: -1 + j5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004660s Time used: 0.004577 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004487s Time used: 0.004131 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021652s Time used: 0.02137 LOG: SAT solveNonLinear - Elapsed time: 0.021652s Cost: 0; Total time: 0.02137 Termination implied by a set of invariant(s): Invariant at l2: flag211^0 <= l6^0 Invariant at l2: 1 + flag211^0 <= l6^0 Invariant at l10: 1 + flag211^0 <= 0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: -1 + j5^0, rest remain the same}> New Graphs: Calling Safety with literal flag211^0 + ir4^0 <= l6^0 and entry LOG: CALL check - Post:flag211^0 + ir4^0 <= l6^0 - Process 1 * Exit transition: * Postcondition : flag211^0 + ir4^0 <= l6^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001254s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001316s INVARIANTS: 2: 10: 12: 17: Quasi-INVARIANTS to narrow Graph: 2: flag211^0 + ir4^0 <= l6^0 , 10: ir4^0 <= flag211^0 + j5^0 , 12: 1 + ir4^0 <= j5^0 , 17: 1 + flag211^0 <= 0 , INVARIANTS: 2: 1 + flag211^0 <= l6^0 , flag211^0 <= l6^0 , 10: 1 + flag211^0 <= 0 , Quasi-INVARIANTS to narrow Graph: 2: 10: Narrowing transition: LOG: Narrow transition size 1 Narrowing transition: LOG: Narrow transition size 1 Narrowing transition: 1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, rest remain the same}> LOG: Narrow transition size 1 It's unfeasible. Removing transition: -1 + j5^0, rest remain the same}> It's unfeasible. Removing transition: 1 + i3^0, rest remain the same}> It's unfeasible. Removing transition: 1, l6^0 -> i3^0, rest remain the same}> It's unfeasible. Removing transition: 1, ir4^0 -> -1 + j5^0, rest remain the same}> It's unfeasible. Removing transition: 1, ir4^0 -> -1 + j5^0, l6^0 -> i3^0, rest remain the same}> Narrowing transition: 1 + i3^0, rest remain the same}> LOG: Narrow transition size 1 It's unfeasible. Removing transition: -1 + j5^0, rest remain the same}> Narrowing transition: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> 1 + i3^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> Variables: flag10^0, ir4^0, l6^0, j5^0, flag211^0, i3^0, k1^0 Checking conditional termination of SCC {l2, l17}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006346s Ranking function: -4 - flag10^0 - flag211^0 + 3*ir4^0 - 2*l6^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Transitions: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1, rest remain the same}> Variables: flag10^0, flag211^0, i3^0, ir4^0, j5^0, k1^0, l6^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000554s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001257s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004885s Time used: 0.0048 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.103243s Time used: 0.102387 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000941s Time used: 1.00093 LOG: SAT solveNonLinear - Elapsed time: 1.104184s Cost: 1; Total time: 1.10331 Failed at location 2: ir4^0 <= 1 + l6^0 Before Improving: Quasi-invariant at l2: ir4^0 <= 1 + l6^0 Quasi-invariant at l12: 1 + flag211^0 <= 0 Quasi-invariant at l17: 1 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010134s Remaining time after improvement: 0.99545 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: ir4^0 <= 1 + l6^0 Quasi-invariant at l12: 1 + flag211^0 <= 0 Quasi-invariant at l17: 1 <= 0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + i3^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 2 + l6^0, j5^0 -> ir4^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 It's unfeasible. Removing transition: 1 + i3^0, rest remain the same}> New Graphs: Transitions: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1, rest remain the same}> Variables: flag10^0, flag211^0, i3^0, ir4^0, j5^0, k1^0, l6^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018263s Ranking function: -3 - 4*flag211^0 + (7 / 2)*ir4^0 + (~(7) / 2)*l6^0 New Graphs: Transitions: 1, rest remain the same}> Variables: flag10^0, flag211^0, ir4^0, l6^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001442s Ranking function: -flag10^0 New Graphs: Calling Safety with literal ir4^0 <= 1 + l6^0 and entry LOG: CALL check - Post:ir4^0 <= 1 + l6^0 - Process 2 * Exit transition: * Postcondition : ir4^0 <= 1 + l6^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001074s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001136s INVARIANTS: 2: 12: 17: Quasi-INVARIANTS to narrow Graph: 2: ir4^0 <= 1 + l6^0 , 12: 1 + flag211^0 <= 0 , 17: 1 <= 0 , Narrowing transition: LOG: Narrow transition size 1 Narrowing transition: LOG: Narrow transition size 1 It's unfeasible. Removing transition: 1, rest remain the same}> It's unfeasible. Removing transition: 1, rest remain the same}> It's unfeasible. Removing transition: 1, rest remain the same}> Narrowing transition: 1 + i3^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: 1 + i3^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> Variables: flag10^0, ir4^0, l6^0, j5^0, flag211^0, i3^0, k1^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.023766s Ranking function: (~(9) / 2) - flag10^0 + (3 / 2)*flag211^0 + k1^0 - l6^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Transitions: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> Variables: flag10^0, flag211^0, i3^0, ir4^0, j5^0, k1^0, l6^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000634s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002929s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006911s Time used: 0.006818 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002964s Time used: 4.0025 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002912s Time used: 4.0002 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005511s Time used: 1.00013 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.183720s Time used: 0.166227 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002447s Time used: 1.00243 LOG: SAT solveNonLinear - Elapsed time: 1.186167s Cost: 1; Total time: 1.16866 Termination implied by a set of invariant(s): Invariant at l2: 0 <= flag211^0 Invariant at l12: 1 + flag211^0 <= l6^0 Invariant at l17: 1 <= l6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - i3^0 New Graphs: Transitions: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> Variables: flag10^0, flag211^0, i3^0, ir4^0, j5^0, k1^0, l6^0 Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.012614s Ranking function: -5 - flag10^0 - flag211^0 + 6*ir4^0 - 6*k1^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Transitions: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> Variables: flag10^0, flag211^0, i3^0, ir4^0, j5^0, k1^0, l6^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000585s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001798s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007485s Time used: 0.007368 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003581s Time used: 4.0031 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002905s Time used: 4.00009 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005456s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.211058s Time used: 0.190148 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002440s Time used: 1.00242 LOG: SAT solveNonLinear - Elapsed time: 1.213497s Cost: 1; Total time: 1.19257 Termination implied by a set of invariant(s): Invariant at l2: l6^0 <= 1 + flag211^0 + ir4^0 Invariant at l12: 1 + flag211^0 <= ir4^0 + j5^0 Invariant at l17: 1 + l6^0 <= ir4^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 + flag211^0 - i3^0 + 2*ir4^0 + j5^0 New Graphs: Transitions: 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> Variables: flag10^0, flag211^0, i3^0, ir4^0, j5^0, k1^0, l6^0 Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007116s Ranking function: -2 - flag10^0 + 2*flag211^0 + ir4^0 - k1^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000728s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003082s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012411s Time used: 0.012266 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006026s Time used: 4.0055 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003014s Time used: 4.00011 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005817s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.188737s Time used: 0.161662 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002735s Time used: 1.00272 LOG: SAT solveNonLinear - Elapsed time: 1.191473s Cost: 1; Total time: 1.16439 Termination implied by a set of invariant(s): Invariant at l12: ir4^0 <= i3^0 + j5^0 + l6^0 Invariant at l17: 1 <= flag211^0 + ir4^0 + l6^0 [ Invariant Graph ] Strengthening and disabling transitions... 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 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - flag211^0 - i3^0 + 3*ir4^0 + j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000907s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003847s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012928s Time used: 0.012742 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.023748s Time used: 4.02322 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002722s Time used: 4.00007 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005777s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.231122s Time used: 0.209062 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002805s Time used: 1.00279 LOG: SAT solveNonLinear - Elapsed time: 1.233927s Cost: 1; Total time: 1.21185 Termination implied by a set of invariant(s): Invariant at l2: l6^0 <= 1 + flag211^0 + ir4^0 Invariant at l12: 1 <= ir4^0 Invariant at l17: flag211^0 + l6^0 <= ir4^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 + flag211^0 - i3^0 - ir4^0 + j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001067s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004724s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.015250s Time used: 0.015056 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006078s Time used: 4.0055 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003074s Time used: 4.00005 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006017s Time used: 1.00005 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.284730s Time used: 0.262598 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.012177s Time used: 1.00313 LOG: SAT solveNonLinear - Elapsed time: 1.296907s Cost: 1; Total time: 1.26572 Termination implied by a set of invariant(s): Invariant at l2: l6^0 <= 1 + ir4^0 Invariant at l12: 1 <= flag211^0 + ir4^0 + l6^0 Invariant at l17: 0 <= l6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - flag211^0 - i3^0 - ir4^0 + j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001189s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005102s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.017217s Time used: 0.016889 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006576s Time used: 4.00588 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003064s Time used: 4.00005 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006740s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.294830s Time used: 0.272445 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003292s Time used: 1.00328 LOG: SAT solveNonLinear - Elapsed time: 1.298121s Cost: 1; Total time: 1.27572 Termination implied by a set of invariant(s): Invariant at l2: flag211^0 <= 1 Invariant at l12: l6^0 <= 1 + ir4^0 Invariant at l17: 0 <= 1 + flag10^0 + flag211^0 + l6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 + flag211^0 - i3^0 - ir4^0 - j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001353s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005818s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018804s Time used: 0.018396 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006911s Time used: 4.00639 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003090s Time used: 4.00001 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.013001s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.259516s Time used: 0.23431 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002862s Time used: 1.00285 LOG: SAT solveNonLinear - Elapsed time: 1.262378s Cost: 1; Total time: 1.23716 Termination implied by a set of invariant(s): Invariant at l2: l6^0 <= 1 + ir4^0 Invariant at l12: 1 + ir4^0 <= i3^0 + j5^0 Invariant at l17: 1 + flag211^0 + l6^0 <= ir4^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - flag211^0 - i3^0 - ir4^0 - 3*j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001495s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007982s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021445s Time used: 0.02102 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006766s Time used: 4.00614 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005965s Time used: 4.00007 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006052s Time used: 1.0001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.239606s Time used: 0.214889 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003187s Time used: 1.00317 LOG: SAT solveNonLinear - Elapsed time: 1.242793s Cost: 1; Total time: 1.21806 Termination implied by a set of invariant(s): Invariant at l2: 0 <= 1 + flag10^0 + flag211^0 + l6^0 Invariant at l12: 1 + ir4^0 + l6^0 <= flag10^0 + i3^0 + j5^0 Invariant at l17: 0 <= flag10^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 + flag211^0 - i3^0 + ir4^0 - j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001635s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007595s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025248s Time used: 0.024837 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006773s Time used: 4.00615 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003428s Time used: 4.00023 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005973s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.278905s Time used: 0.255177 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003357s Time used: 1.00334 LOG: SAT solveNonLinear - Elapsed time: 1.282262s Cost: 1; Total time: 1.25851 Termination implied by a set of invariant(s): Invariant at l2: l6^0 <= 1 Invariant at l12: 1 <= flag211^0 + l6^0 Invariant at l17: flag211^0 + l6^0 <= 1 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - flag211^0 - i3^0 + ir4^0 - j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001839s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007373s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.026770s Time used: 0.026172 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.007756s Time used: 4.00688 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.009798s Time used: 4.00071 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002975s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.139656s Time used: 0.128505 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004859s Time used: 1.00485 LOG: SAT solveNonLinear - Elapsed time: 1.144515s Cost: 1; Total time: 1.13335 Termination implied by a set of invariant(s): Invariant at l12: 0 <= flag211^0 + j5^0 + l6^0 Invariant at l17: l6^0 <= 1 + flag211^0 [ Invariant Graph ] Strengthening and disabling transitions... 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 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - i3^0 + 3*ir4^0 - j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001929s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009162s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.028081s Time used: 0.027429 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006826s Time used: 4.00611 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.008618s Time used: 4.00024 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002663s Time used: 1.00007 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.158828s Time used: 0.15008 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002853s Time used: 1.00284 LOG: SAT solveNonLinear - Elapsed time: 1.161681s Cost: 1; Total time: 1.15292 Termination implied by a set of invariant(s): Invariant at l2: flag10^0 <= 1 + ir4^0 + l6^0 Invariant at l12: j5^0 <= i3^0 + ir4^0 + l6^0 Invariant at l17: 0 <= 1 + flag211^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - i3^0 + ir4^0 + 3*j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001921s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007466s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.029389s Time used: 0.028946 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004496s Time used: 4.00376 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.008924s Time used: 4.00005 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002491s Time used: 1.00008 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.158503s Time used: 0.148851 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.037760s Time used: 1.03775 LOG: SAT solveNonLinear - Elapsed time: 1.196264s Cost: 1; Total time: 1.1866 Termination implied by a set of invariant(s): Invariant at l2: 1 <= flag10^0 + l6^0 Invariant at l12: 1 <= ir4^0 + j5^0 Invariant at l17: 1 + flag10^0 + l6^0 <= ir4^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - i3^0 - ir4^0 - j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001992s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.014236s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.033044s Time used: 0.032594 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004982s Time used: 4.00443 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.007332s Time used: 4.00007 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002549s Time used: 1.00006 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.151815s Time used: 0.141042 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002819s Time used: 1.00281 LOG: SAT solveNonLinear - Elapsed time: 1.154634s Cost: 1; Total time: 1.14385 Termination implied by a set of invariant(s): Invariant at l2: 1 <= flag10^0 + l6^0 Invariant at l12: flag211^0 + ir4^0 <= j5^0 Invariant at l17: flag10^0 <= flag211^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - i3^0 - j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002118s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011744s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.032098s Time used: 0.031591 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004970s Time used: 4.00423 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.014835s Time used: 1.00773 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.983653s Time used: 0.981261 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.147053s Time used: 0.138938 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.874028s Time used: 0.874016 LOG: SAT solveNonLinear - Elapsed time: 1.021081s Cost: 1; Total time: 1.01295 Termination implied by a set of invariant(s): Invariant at l2: flag10^0 + flag211^0 <= 1 Invariant at l12: l6^0 <= flag211^0 + j5^0 Invariant at l17: flag211^0 + l6^0 <= 1 + flag10^0 + ir4^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - i3^0 - ir4^0 + j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002243s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011413s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.033248s Time used: 0.032689 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.779658s Time used: 0.778931 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.993932s Time used: 0.987888 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.984556s Time used: 0.982241 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.137909s Time used: 0.12878 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.865301s Time used: 0.865287 LOG: SAT solveNonLinear - Elapsed time: 1.003210s Cost: 1; Total time: 0.994067 Termination implied by a set of invariant(s): Invariant at l2: 1 + flag10^0 + flag211^0 <= l6^0 Invariant at l12: flag211^0 + j5^0 <= ir4^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^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 LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - i3^0 + j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002331s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010505s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.033953s Time used: 0.03336 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.806295s Time used: 0.805525 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.981759s Time used: 0.975611 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.985633s Time used: 0.983318 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.146506s Time used: 0.136231 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.857597s Time used: 0.857584 LOG: SAT solveNonLinear - Elapsed time: 1.004102s Cost: 1; Total time: 0.993815 Termination implied by a set of invariant(s): Invariant at l2: flag10^0 <= 1 Invariant at l12: 1 + flag211^0 + l6^0 <= ir4^0 Invariant at l17: flag10^0 <= flag211^0 + l6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 + flag211^0 - i3^0 - j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002404s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.021425s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.039140s Time used: 0.038357 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.770611s Time used: 0.769872 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994334s Time used: 0.988225 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.985342s Time used: 0.982929 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.145302s Time used: 0.136352 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.857490s Time used: 0.857482 LOG: SAT solveNonLinear - Elapsed time: 1.002792s Cost: 1; Total time: 0.993834 Termination implied by a set of invariant(s): Invariant at l2: l6^0 <= 1 Invariant at l12: j5^0 <= flag211^0 + ir4^0 Invariant at l17: l6^0 <= 1 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - flag211^0 - i3^0 - j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002555s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010050s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.037884s Time used: 0.037245 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.781412s Time used: 0.780649 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994461s Time used: 0.988323 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.985018s Time used: 0.982614 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.160897s Time used: 0.152609 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.841502s Time used: 0.84149 LOG: SAT solveNonLinear - Elapsed time: 1.002399s Cost: 1; Total time: 0.994099 Termination implied by a set of invariant(s): Invariant at l2: flag10^0 <= 1 + l6^0 Invariant at l12: l6^0 <= 1 + flag211^0 + i3^0 + ir4^0 Invariant at l17: flag211^0 <= 1 + flag10^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 + flag211^0 - i3^0 + j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002578s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010012s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.036773s Time used: 0.035942 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.777719s Time used: 0.777107 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994312s Time used: 0.988147 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.985618s Time used: 0.982433 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.155316s Time used: 0.147027 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.846117s Time used: 0.84611 LOG: SAT solveNonLinear - Elapsed time: 1.001433s Cost: 1; Total time: 0.993137 Termination implied by a set of invariant(s): Invariant at l12: 0 <= j5^0 + l6^0 Invariant at l17: 1 <= flag211^0 + l6^0 [ Invariant Graph ] Strengthening and disabling transitions... 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 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - flag211^0 - i3^0 + j5^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002778s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011506s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.037668s Time used: 0.036805 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.770609s Time used: 0.769825 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994729s Time used: 0.988598 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.985173s Time used: 0.982875 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.165465s Time used: 0.157433 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.838197s Time used: 0.838185 LOG: SAT solveNonLinear - Elapsed time: 1.003662s Cost: 1; Total time: 0.995618 Termination implied by a set of invariant(s): Invariant at l2: 1 + flag211^0 <= flag10^0 + l6^0 Invariant at l12: 1 + l6^0 <= flag211^0 + i3^0 + ir4^0 + j5^0 Invariant at l17: 1 + flag10^0 <= flag211^0 + l6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 + flag211^0 - i3^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002893s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.013466s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.041887s Time used: 0.041008 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.747311s Time used: 0.746483 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994333s Time used: 0.988108 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.985367s Time used: 0.982978 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.202696s Time used: 0.194829 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.799147s Time used: 0.799134 LOG: SAT solveNonLinear - Elapsed time: 1.001843s Cost: 1; Total time: 0.993963 Termination implied by a set of invariant(s): Invariant at l2: flag10^0 + l6^0 <= 1 Invariant at l12: l6^0 <= 1 + ir4^0 + j5^0 Invariant at l17: 0 <= flag10^0 + flag211^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - flag211^0 - i3^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003059s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.022942s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.039808s Time used: 0.038917 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.746523s Time used: 0.745877 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994856s Time used: 0.988584 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.985961s Time used: 0.9836 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.162350s Time used: 0.154185 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.839671s Time used: 0.839664 LOG: SAT solveNonLinear - Elapsed time: 1.002021s Cost: 1; Total time: 0.993849 Termination implied by a set of invariant(s): Invariant at l2: 0 <= 1 + flag10^0 Invariant at l12: ir4^0 + l6^0 <= 1 + flag211^0 + j5^0 Invariant at l17: 0 <= flag10^0 + flag211^0 + ir4^0 + l6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 + flag211^0 - i3^0 - ir4^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003160s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.014562s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.043858s Time used: 0.042843 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.745998s Time used: 0.745358 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.995406s Time used: 0.989103 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.984699s Time used: 0.982393 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.168306s Time used: 0.160341 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.833875s Time used: 0.833868 LOG: SAT solveNonLinear - Elapsed time: 1.002180s Cost: 1; Total time: 0.994209 Termination implied by a set of invariant(s): Invariant at l2: 1 + flag10^0 <= flag211^0 + l6^0 Invariant at l12: j5^0 <= 1 + ir4^0 Invariant at l17: 0 <= flag10^0 + flag211^0 + ir4^0 + l6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 + flag211^0 - i3^0 + ir4^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003225s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.013018s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.043769s Time used: 0.042771 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.744413s Time used: 0.743749 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994545s Time used: 0.988186 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.988442s Time used: 0.982971 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.183601s Time used: 0.176104 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.815151s Time used: 0.815139 LOG: SAT solveNonLinear - Elapsed time: 0.998752s Cost: 1; Total time: 0.991243 Termination implied by a set of invariant(s): Invariant at l2: l6^0 <= 1 + flag211^0 + ir4^0 Invariant at l12: l6^0 <= 1 + i3^0 + ir4^0 Invariant at l17: 1 + flag10^0 + flag211^0 <= ir4^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - flag211^0 - i3^0 - ir4^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003353s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.016860s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.046528s Time used: 0.045726 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.734220s Time used: 0.733346 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994261s Time used: 0.987799 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.985063s Time used: 0.982683 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.163304s Time used: 0.153477 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.840303s Time used: 0.840292 LOG: SAT solveNonLinear - Elapsed time: 1.003608s Cost: 1; Total time: 0.993769 Termination implied by a set of invariant(s): Invariant at l2: 1 + flag211^0 <= flag10^0 + ir4^0 + l6^0 Invariant at l12: j5^0 <= ir4^0 + l6^0 Invariant at l17: 1 + l6^0 <= flag211^0 + ir4^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - flag211^0 - i3^0 + ir4^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003416s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.016131s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.047016s Time used: 0.045944 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.727441s Time used: 0.726738 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994774s Time used: 0.988355 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.984531s Time used: 0.982142 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.179013s Time used: 0.169206 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.824638s Time used: 0.824626 LOG: SAT solveNonLinear - Elapsed time: 1.003651s Cost: 1; Total time: 0.993832 Termination implied by a set of invariant(s): Invariant at l2: 1 <= flag10^0 + flag211^0 + l6^0 Invariant at l12: 0 <= 1 + l6^0 Invariant at l17: 0 <= flag10^0 + flag211^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - i3^0 - ir4^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003515s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.019791s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.049287s Time used: 0.048157 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.708913s Time used: 0.70821 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994868s Time used: 0.988395 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.984701s Time used: 0.982256 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.175616s Time used: 0.166819 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.827097s Time used: 0.827086 LOG: SAT solveNonLinear - Elapsed time: 1.002713s Cost: 1; Total time: 0.993905 Termination implied by a set of invariant(s): Invariant at l2: l6^0 <= 1 Invariant at l12: l6^0 <= j5^0 Invariant at l17: flag211^0 <= flag10^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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): 1 + i3^0, rest remain the same}> Quasi-ranking function: 50000 - i3^0 + ir4^0 New Graphs: Transitions: 1 + i3^0, rest remain the same}> Variables: flag211^0, i3^0, ir4^0, j5^0 Checking conditional termination of SCC {l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003601s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.016963s Trying to remove transition: 1 + i3^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.049714s Time used: 0.048599 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.733232s Time used: 0.73251 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.979018s Time used: 0.972587 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.985001s Time used: 0.98244 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.995147s Time used: 0.991054 Proving non-termination of subgraph 1 Transitions: 1 + i3^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> Variables: flag10^0, ir4^0, l6^0, j5^0, flag211^0, i3^0, k1^0 Checking conditional non-termination of SCC {l2, l12, l17}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.318128s Time used: 0.317348 Improving Solution with cost 4 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003542s Time used: 1.00353 LOG: SAT solveNonLinear - Elapsed time: 1.321670s Cost: 4; Total time: 1.32088 Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: flag10^0 + flag211^0 <= 0 Quasi-invariant at l17: flag10^0 + flag211^0 <= 0 Strengthening and disabling EXIT transitions... Closed exits from l2: 3 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> Checking conditional non-termination of SCC {l2, l12, l17}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.233717s Time used: 0.232978 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.325615s Time used: 0.32163 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.517225s Time used: 0.517219 LOG: SAT solveNonLinear - Elapsed time: 1.076558s Cost: 2; Total time: 1.07183 Failed at location 2: 2 + flag211^0 + l6^0 <= ir4^0 Before Improving: Quasi-invariant at l2: 2 + flag211^0 + l6^0 <= ir4^0 Quasi-invariant at l17: flag211^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010498s Remaining time after improvement: 0.99378 Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: 2 + flag211^0 + l6^0 <= ir4^0 Quasi-invariant at l17: flag211^0 <= 0 Strengthening and disabling EXIT transitions... Closed exits from l2: 2 Strengthening exit transition (result): Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^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 + l6^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^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 + l6^0, ir4^0 -> -1 + ir4^0, j5^0 -> ir4^0, l6^0 -> 1 + l6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> Checking conditional non-termination of SCC {l2, l12, l17}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.095203s Time used: 0.095105 LOG: SAT solveNonLinear - Elapsed time: 0.095203s Cost: 0; Total time: 0.095105 Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: flag211^0 <= flag10^0 Quasi-invariant at l12: 1 + flag10^0 + l6^0 <= flag211^0 + i3^0 Quasi-invariant at l17: 1 + flag10^0 <= flag211^0 + l6^0 Strengthening and disabling EXIT transitions... Closed exits from l2: 1 Unnecessary quasi-invariant at l17: 1 + flag10^0 <= flag211^0 + l6^0 Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i3^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 2 + l6^0, j5^0 -> ir4^0, rest remain the same}> Calling reachability with... Transition: Conditions: flag10^0 + flag211^0 <= 0, 2 + flag211^0 + l6^0 <= ir4^0, flag211^0 <= flag10^0, OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: flag10^0 + flag211^0 <= 0, flag211^0 <= flag10^0, 2 + flag211^0 + l6^0 <= ir4^0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate