NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef3}> undef57, y_18^0 -> (0 + undef57)}> (0 + undef101), __cil_tmp5_10^0 -> undef101, k_110^0 -> (0 + undef114), len_87^0 -> undef114, lt_26^0 -> undef120, lt_27^0 -> undef121, lt_28^0 -> undef122, tmp_9^0 -> undef124, x_13^0 -> (0 + a_11^0), x_19^0 -> undef128, x_8^0 -> undef129, y_20^0 -> 0}> undef142}> undef179, __patmp2^0 -> undef180, k_145^0 -> (0 + undef180), len_165^0 -> (0 + undef179), lt_23^0 -> undef189, lt_24^0 -> undef190, x_13^0 -> (0 + undef205)}> undef207, lt_25^0 -> undef226, lt_26^0 -> undef227, x_17^0 -> (0 + undef240), y_18^0 -> (0 + w_15^0)}> undef245}> undef297, y_18^0 -> (0 + undef297)}> undef312}> undef363, y_18^0 -> (0 + undef363)}> (~(1) + k_145^0)}> undef412}> undef446, __patmp2^0 -> undef447, k_145^0 -> (0 + undef447), len_165^0 -> (0 + undef446), lt_21^0 -> undef454, lt_22^0 -> undef455, x_13^0 -> (0 + undef472)}> Fresh variables: undef3, undef57, undef101, undef114, undef120, undef121, undef122, undef124, undef128, undef129, undef133, undef134, undef135, undef136, undef137, undef138, undef142, undef179, undef180, undef189, undef190, undef205, undef206, undef207, undef226, undef227, undef240, undef245, undef297, undef312, undef363, undef412, undef446, undef447, undef454, undef455, undef472, undef473, Undef variables: undef3, undef57, undef101, undef114, undef120, undef121, undef122, undef124, undef128, undef129, undef133, undef134, undef135, undef136, undef137, undef138, undef142, undef179, undef180, undef189, undef190, undef205, undef206, undef207, undef226, undef227, undef240, undef245, undef297, undef312, undef363, undef412, undef446, undef447, undef454, undef455, undef472, undef473, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: undef142}> undef3}> undef245, __disjvr_3^0 -> undef312, x_17^0 -> (0 + undef240)}> undef412, k_145^0 -> (0 + undef447), len_165^0 -> (0 + undef446), x_13^0 -> (0 + undef472)}> Fresh variables: undef3, undef57, undef101, undef114, undef120, undef121, undef122, undef124, undef128, undef129, undef133, undef134, undef135, undef136, undef137, undef138, undef142, undef179, undef180, undef189, undef190, undef205, undef206, undef207, undef226, undef227, undef240, undef245, undef297, undef312, undef363, undef412, undef446, undef447, undef454, undef455, undef472, undef473, Undef variables: undef3, undef57, undef101, undef114, undef120, undef121, undef122, undef124, undef128, undef129, undef133, undef134, undef135, undef136, undef137, undef138, undef142, undef179, undef180, undef189, undef190, undef205, undef206, undef207, undef226, undef227, undef240, undef245, undef297, undef312, undef363, undef412, undef446, undef447, undef454, undef455, undef472, undef473, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef412, k_145^0 -> undef447, len_165^0 -> undef446, x_13^0 -> undef472, rest remain the same}> Variables: __disjvr_4^0, k_145^0, len_165^0, x_13^0 Graph 2: Transitions: undef3, rest remain the same}> Variables: __disjvr_0^0, x_17^0 Precedence: Graph 0 Graph 1 undef142, rest remain the same}> Graph 2 undef245, __disjvr_3^0 -> undef312, x_17^0 -> undef240, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 1 , 2 ) ( 7 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.002475 Checking conditional termination of SCC {l7}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000892s Ranking function: -1 + k_145^0 New Graphs: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.001043 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000263s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000800s Trying to remove transition: undef3, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001970s Time used: 0.001885 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003500s Time used: 0.003352 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.000508s Time used: 4.00026 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007616s Time used: 1.0003 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004566s Time used: 0.002812 Termination failed. Trying to show unreachability... Proving unreachability of entry: undef245, __disjvr_3^0 -> undef312, x_17^0 -> undef240, rest remain the same}> LOG: CALL check - Post:1 <= 0 - Process 1 * Exit transition: undef245, __disjvr_3^0 -> undef312, x_17^0 -> undef240, rest remain the same}> * Postcondition : 1 <= 0 Postcodition moved up: 1 <= 0 LOG: Try proving POST Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 2 * Exit transition: undef142, rest remain the same}> * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000850s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000946s LOG: NarrowEntry size 1 Narrowing transition: undef412, k_145^0 -> undef447, len_165^0 -> undef446, x_13^0 -> undef472, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef142, rest remain the same}> END ENTRIES: GRAPH: undef412, k_145^0 -> undef447, len_165^0 -> undef446, x_13^0 -> undef472, rest remain the same}> END GRAPH: EXIT: undef245, __disjvr_3^0 -> undef312, x_17^0 -> undef240, rest remain the same}> POST: 1 <= 0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011341s Time used: 0.01128 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.000610s Time used: 4.00005 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002163s Time used: 1.00022 LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 5.024669s Cannot prove unreachability Proving non-termination of subgraph 2 Transitions: undef3, rest remain the same}> Variables: __disjvr_0^0, x_17^0 Checking conditional non-termination of SCC {l1}... > No exit transition to close. Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001345s Calling reachability with... Transition: Conditions: OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: undef245, __disjvr_3^0 -> undef312, x_17^0 -> undef240, rest remain the same}> Conditions: OPEN EXITS: undef245, __disjvr_3^0 -> undef312, x_17^0 -> undef240, rest remain the same}> (condsUp: __disjvr_2^0 = undef245, __disjvr_3^0 = undef312, undef240 = undef297, undef240 = undef363) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: undef142, rest remain the same}> Conditions: 0 <= len_165^0, 1 <= k_145^0, x_13^0 = y_12^0, __disjvr_2^0 = undef245, __disjvr_3^0 = undef312, undef240 = undef297, undef240 = undef363, OPEN EXITS: undef142, rest remain the same}> > Conditions are reachable! Program does NOT terminate