YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: (1 + i2^0)}> 0}> (1 + i2^0)}> 0}> (1 + i2^0)}> 0, size1010^0 -> (0 + undef67), size1^0 -> undef67, size77^0 -> (0 + undef67), tmp1111^0 -> undef69, tmp88^0 -> undef70}> Fresh variables: undef67, undef69, undef70, Undef variables: undef67, undef69, undef70, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 0}> (1 + i2^0)}> (1 + i2^0)}> 0}> (1 + i2^0)}> Fresh variables: undef67, undef69, undef70, Undef variables: undef67, undef69, undef70, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: 1 + i2^0, rest remain the same}> Variables: i2^0, size1^0 Graph 2: Transitions: 1 + i2^0, rest remain the same}> Variables: i2^0, size1^0 Graph 3: Transitions: 1 + i2^0, rest remain the same}> Variables: i2^0, size1^0 Graph 4: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 0, rest remain the same}> Graph 3 0, rest remain the same}> Graph 4 Map Locations to Subgraph: ( 0 , 0 ) ( 1 , 1 ) ( 4 , 4 ) ( 5 , 3 ) ( 6 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.00147 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000615s Ranking function: -1 - i2^0 + size1^0 New Graphs: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.001222 Checking conditional termination of SCC {l6}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000600s Ranking function: -1 - i2^0 + size1^0 New Graphs: Proving termination of subgraph 3 Checking unfeasibility... Time used: 0.001223 Checking conditional termination of SCC {l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000615s Ranking function: -1 - i2^0 + size1^0 New Graphs: Proving termination of subgraph 4 Analyzing SCC {l4}... No cycles found. Program Terminates