YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> undef3, oldX3^0 -> undef4, x0^0 -> (0 + undef3), x1^0 -> (0 + undef4)}> undef7, oldX1^0 -> undef8, x0^0 -> (0 + undef7), x1^0 -> (~(1) + undef8)}> undef13, oldX1^0 -> undef14, x0^0 -> (0 + undef13), x1^0 -> (0 + undef14)}> undef19, oldX1^0 -> undef20, x0^0 -> (0 + undef19), x1^0 -> (0 + undef20)}> undef25, oldX1^0 -> (0 + x1^0), oldX2^0 -> undef27, x0^0 -> (~(1) + undef25), x1^0 -> (0 + undef27)}> undef31, oldX1^0 -> (0 + x1^0), x0^0 -> (0 + undef31), x1^0 -> 7}> undef37, oldX1^0 -> (0 + x1^0), oldX2^0 -> undef39, x0^0 -> (0 + undef37), x1^0 -> (0 + undef39)}> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> undef45, x0^0 -> 7, x1^0 -> (0 + undef45)}> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> undef51, oldX3^0 -> undef52, x0^0 -> (0 + undef51), x1^0 -> (0 + undef52)}> undef55, oldX1^0 -> (0 + x1^0), oldX2^0 -> undef57, x0^0 -> (1 + undef55), x1^0 -> (0 + undef57)}> undef61, oldX1^0 -> undef62, x0^0 -> (0 + undef61), x1^0 -> (0 + undef62)}> undef67, oldX1^0 -> undef68, x0^0 -> (0 + undef67), x1^0 -> (0 + undef68)}> (0 + x0^0), oldX1^0 -> (0 + x1^0), x0^0 -> 0, x1^0 -> 0}> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> undef81, oldX3^0 -> undef82, x0^0 -> (0 + undef81), x1^0 -> (0 + undef82)}> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> undef87, oldX3^0 -> undef88, x0^0 -> (0 + undef87), x1^0 -> (0 + undef88)}> Fresh variables: undef3, undef4, undef7, undef8, undef13, undef14, undef19, undef20, undef25, undef27, undef31, undef37, undef39, undef45, undef51, undef52, undef55, undef57, undef61, undef62, undef67, undef68, undef81, undef82, undef87, undef88, Undef variables: undef3, undef4, undef7, undef8, undef13, undef14, undef19, undef20, undef25, undef27, undef31, undef37, undef39, undef45, undef51, undef52, undef55, undef57, undef61, undef62, undef67, undef68, undef81, undef82, undef87, undef88, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: (0 + undef67), x1^0 -> (0 + undef68)}> (0 + undef37), x1^0 -> (0 + undef39)}> (0 + undef3), x1^0 -> (0 + undef4)}> (0 + undef3), x1^0 -> (0 + undef4)}> (0 + undef19), x1^0 -> (0 + undef20)}> (0 + undef19), x1^0 -> (0 + undef20)}> (0 + undef37), x1^0 -> (0 + undef39)}> (0 + undef37), x1^0 -> (0 + undef39)}> (0 + undef51), x1^0 -> (0 + undef52)}> (0 + undef51), x1^0 -> (0 + undef52)}> (0 + undef67), x1^0 -> (0 + undef68)}> (0 + undef67), x1^0 -> (0 + undef68)}> (0 + undef3), x1^0 -> (0 + undef4)}> (0 + undef19), x1^0 -> (0 + undef20)}> (0 + undef19), x1^0 -> (0 + undef20)}> (0 + undef37), x1^0 -> (0 + undef39)}> (0 + undef51), x1^0 -> (0 + undef52)}> (0 + undef67), x1^0 -> (0 + undef68)}> Fresh variables: undef3, undef4, undef7, undef8, undef13, undef14, undef19, undef20, undef25, undef27, undef31, undef37, undef39, undef45, undef51, undef52, undef55, undef57, undef61, undef62, undef67, undef68, undef81, undef82, undef87, undef88, Undef variables: undef3, undef4, undef7, undef8, undef13, undef14, undef19, undef20, undef25, undef27, undef31, undef37, undef39, undef45, undef51, undef52, undef55, undef57, undef61, undef62, undef67, undef68, undef81, undef82, undef87, undef88, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef37, x1^0 -> undef39, rest remain the same}> Variables: x0^0, x1^0 Graph 2: Transitions: undef19, x1^0 -> undef20, rest remain the same}> Variables: x0^0, x1^0 Graph 3: Transitions: Variables: Graph 4: Transitions: undef67, x1^0 -> undef68, rest remain the same}> Variables: x0^0, x1^0 Graph 5: Transitions: Variables: Precedence: Graph 0 Graph 1 undef37, x1^0 -> undef39, rest remain the same}> undef37, x1^0 -> undef39, rest remain the same}> undef37, x1^0 -> undef39, rest remain the same}> Graph 2 undef19, x1^0 -> undef20, rest remain the same}> undef19, x1^0 -> undef20, rest remain the same}> undef19, x1^0 -> undef20, rest remain the same}> Graph 3 undef3, x1^0 -> undef4, rest remain the same}> undef3, x1^0 -> undef4, rest remain the same}> undef3, x1^0 -> undef4, rest remain the same}> Graph 4 undef67, x1^0 -> undef68, rest remain the same}> undef67, x1^0 -> undef68, rest remain the same}> undef67, x1^0 -> undef68, rest remain the same}> Graph 5 undef51, x1^0 -> undef52, rest remain the same}> undef51, x1^0 -> undef52, rest remain the same}> undef51, x1^0 -> undef52, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 3 ) ( 3 , 2 ) ( 5 , 1 ) ( 9 , 5 ) ( 10 , 4 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.001053 Checking conditional termination of SCC {l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000432s Ranking function: -1 + x0^0 New Graphs: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.001276 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000543s Ranking function: -1 + x1^0 New Graphs: Proving termination of subgraph 3 Analyzing SCC {l2}... No cycles found. Proving termination of subgraph 4 Checking unfeasibility... Time used: 0.00112 Checking conditional termination of SCC {l10}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000518s Ranking function: 62 - x0^0 New Graphs: Proving termination of subgraph 5 Analyzing SCC {l9}... No cycles found. Program Terminates