YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef1, devExt_7^0 -> undef3, i_12^0 -> undef4, irp_11^0 -> undef5, loop_count_14^0 -> undef6, loop_max_13^0 -> undef7, lt_48^0 -> (0 + cnt_60^0), nPacketsOld_9^0 -> undef9, nPackets_10^0 -> undef10, request_8^0 -> undef11}> Fresh variables: undef1, undef3, undef4, undef5, undef6, undef7, undef9, undef10, undef11, Undef variables: undef1, undef3, undef4, undef5, undef6, undef7, undef9, undef10, undef11, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: Fresh variables: undef1, undef3, undef4, undef5, undef6, undef7, undef9, undef10, undef11, Undef variables: undef1, undef3, undef4, undef5, undef6, undef7, undef9, undef10, undef11, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: Variables: Precedence: Graph 0 Graph 1 Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Analyzing SCC {l2}... No cycles found. Program Terminates