NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef75, y_18^0 -> (0 + undef75)}> (0 + undef114), ___cil_tmp5_10^0 -> undef114, k_110^0 -> (0 + undef122), len_87^0 -> undef122, lt_26^0 -> undef128, lt_27^0 -> undef129, lt_28^0 -> undef130, tmp_9^0 -> undef132, x_13^0 -> (0 + a_11^0), x_19^0 -> undef136, x_8^0 -> undef137, y_20^0 -> 0}> undef205, ___patmp2^0 -> undef206, k_145^0 -> (0 + undef206), len_165^0 -> (0 + undef205), lt_23^0 -> undef215, lt_24^0 -> undef216, x_13^0 -> (0 + undef231)}> undef233, lt_25^0 -> undef247, lt_26^0 -> undef248, x_17^0 -> (0 + undef261), y_18^0 -> (0 + w_15^0)}> undef336, y_18^0 -> (0 + undef336)}> undef420, y_18^0 -> (0 + undef420)}> (~(1) + k_145^0)}> undef516, ___patmp2^0 -> undef517, k_145^0 -> (0 + undef517), len_165^0 -> (0 + undef516), lt_21^0 -> undef524, lt_22^0 -> undef525, x_13^0 -> (0 + undef542)}> Fresh variables: undef75, undef114, undef122, undef128, undef129, undef130, undef132, undef136, undef137, undef141, undef142, undef143, undef144, undef145, undef146, undef205, undef206, undef215, undef216, undef231, undef232, undef233, undef247, undef248, undef261, undef336, undef420, undef516, undef517, undef524, undef525, undef542, undef543, Undef variables: undef75, undef114, undef122, undef128, undef129, undef130, undef132, undef136, undef137, undef141, undef142, undef143, undef144, undef145, undef146, undef205, undef206, undef215, undef216, undef231, undef232, undef233, undef247, undef248, undef261, undef336, undef420, undef516, undef517, undef524, undef525, undef542, undef543, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: (0 + undef261)}> (0 + undef261)}> (0 + undef517), len_165^0 -> (0 + undef516), x_13^0 -> (0 + undef542)}> (0 + undef517), len_165^0 -> (0 + undef516), x_13^0 -> (0 + undef542)}> Fresh variables: undef75, undef114, undef122, undef128, undef129, undef130, undef132, undef136, undef137, undef141, undef142, undef143, undef144, undef145, undef146, undef205, undef206, undef215, undef216, undef231, undef232, undef233, undef247, undef248, undef261, undef336, undef420, undef516, undef517, undef524, undef525, undef542, undef543, Undef variables: undef75, undef114, undef122, undef128, undef129, undef130, undef132, undef136, undef137, undef141, undef142, undef143, undef144, undef145, undef146, undef205, undef206, undef215, undef216, undef231, undef232, undef233, undef247, undef248, undef261, undef336, undef420, undef516, undef517, undef524, undef525, undef542, undef543, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef517, len_165^0 -> undef516, x_13^0 -> undef542, rest remain the same}> undef517, len_165^0 -> undef516, x_13^0 -> undef542, rest remain the same}> Variables: k_145^0, len_165^0, x_13^0, y_12^0 Graph 2: Transitions: Variables: w_15^0, x_17^0 Precedence: Graph 0 Graph 1 Graph 2 undef261, rest remain the same}> undef261, 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.004503 Checking conditional termination of SCC {l7}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001265s Ranking function: -1 + k_145^0 New Graphs: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.001801 > No variable changes in termination graph. Checking conditional unfeasibility... Calling Safety with literal x_17^0 <= w_15^0 and entry LOG: CALL check - Post:x_17^0 <= w_15^0 - Process 1 * Exit transition: * Postcondition : x_17^0 <= w_15^0 Postcodition moved up: x_17^0 <= w_15^0 LOG: Try proving POST Postcondition: x_17^0 <= w_15^0 LOG: CALL check - Post:x_17^0 <= w_15^0 - Process 2 * Exit transition: undef261, rest remain the same}> * Postcondition : x_17^0 <= w_15^0 Postcodition moved up: undef261 <= w_15^0 LOG: Try proving POST Postcondition: undef261 <= w_15^0 LOG: CALL check - Post:undef261 <= w_15^0 - Process 3 * Exit transition: * Postcondition : undef261 <= w_15^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000729s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000830s Postcondition: undef261 <= w_15^0 LOG: CALL check - Post:undef261 <= w_15^0 - Process 4 * Exit transition: * Postcondition : undef261 <= w_15^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000718s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000815s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 Narrowing transition: undef517, len_165^0 -> undef516, x_13^0 -> undef542, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef517, len_165^0 -> undef516, x_13^0 -> undef542, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: END ENTRIES: GRAPH: undef517, len_165^0 -> undef516, x_13^0 -> undef542, rest remain the same}> undef517, len_165^0 -> undef516, x_13^0 -> undef542, rest remain the same}> END GRAPH: EXIT: undef261, rest remain the same}> POST: x_17^0 <= w_15^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.015313s Time used: 0.015254 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.562984s Time used: 0.5623 Improving Solution with cost 54 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000242s Time used: 1.00024 LOG: SAT solveNonLinear - Elapsed time: 1.563227s Cost: 54; Total time: 1.56254 Failed at location 7: y_12^0 <= x_13^0 Failed at location 7: y_12^0 <= x_13^0 Failed at location 7: x_13^0 <= y_12^0 Failed at location 7: x_13^0 <= y_12^0 Before Improving: Quasi-invariant at l7: y_12^0 <= x_13^0 Quasi-invariant at l7: x_13^0 <= y_12^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006719s Remaining time after improvement: 0.998322 Some transition disabled by a set of quasi-invariant(s): Quasi-invariant at l7: y_12^0 <= x_13^0 Quasi-invariant at l7: x_13^0 <= y_12^0 LOG: NEXT CALL check - disable LOG: CALL check - Post:y_12^0 <= x_13^0 - Process 5 * Exit transition: * Postcondition : y_12^0 <= x_13^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001092s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001188s Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.000112s Time used: 1.00003 LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 2.600786s LOG: NarrowEntry size 1 Narrowing transition: LOG: Narrow transition size 1 It's unfeasible. Removing transition: ENTRIES: undef261, rest remain the same}> END ENTRIES: GRAPH: END GRAPH: EXIT: POST: x_17^0 <= w_15^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003227s Time used: 0.003171 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.000593s Time used: 4.00047 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.001761s Time used: 1.0003 LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 7.622240s Proving non-termination of subgraph 2 Transitions: Variables: w_15^0, x_17^0 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000800s Checking conditional non-termination of SCC {l1}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014335s Time used: 0.01412 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.034126s Time used: 0.034124 LOG: SAT solveNonLinear - Elapsed time: 0.048461s Cost: 1; Total time: 0.048244 Failed at location 1: 1 + x_17^0 <= w_15^0 Before Improving: Quasi-invariant at l1: 1 + x_17^0 <= w_15^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008857s Remaining time after improvement: 0.998692 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.002705s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 + x_17^0 <= w_15^0 Strengthening and disabling EXIT transitions... Closed exits from l1: 1 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 Strengthening transition (result): Calling reachability with... Transition: Conditions: 1 + x_17^0 <= w_15^0, Transition: Conditions: 1 + x_17^0 <= w_15^0, OPEN EXITS: (condsUp: 1 + x_17^0 <= w_15^0) (condsUp: 1 + x_17^0 <= w_15^0) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: undef261, rest remain the same}> Conditions: 1 + x_17^0 <= w_15^0, Transition: undef261, rest remain the same}> Conditions: 1 + x_17^0 <= w_15^0, Transition: undef261, rest remain the same}> Conditions: 1 + x_17^0 <= w_15^0, Transition: undef261, rest remain the same}> Conditions: 1 + x_17^0 <= w_15^0, OPEN EXITS: undef261, rest remain the same}> (condsUp: 1 + undef261 <= w_15^0, undef261 = undef336, undef261 = undef420, 1 + undef261 <= w_15^0) undef261, rest remain the same}> (condsUp: 1 + undef261 <= w_15^0, undef261 = undef336, undef261 = undef420, 1 + undef261 <= w_15^0) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 1 <= k_145^0, 0 <= len_165^0, x_13^0 = y_12^0, 1 + undef261 <= w_15^0, undef261 = undef336, undef261 = undef420, 1 + undef261 <= w_15^0, Transition: Conditions: 1 <= k_145^0, 0 <= len_165^0, x_13^0 = y_12^0, 1 + undef261 <= w_15^0, undef261 = undef336, undef261 = undef420, 1 + undef261 <= w_15^0, Transition: Conditions: 1 <= k_145^0, 0 <= len_165^0, x_13^0 = y_12^0, 1 + undef261 <= w_15^0, undef261 = undef336, undef261 = undef420, 1 + undef261 <= w_15^0, Transition: Conditions: 1 <= k_145^0, 0 <= len_165^0, x_13^0 = y_12^0, 1 + undef261 <= w_15^0, undef261 = undef336, undef261 = undef420, 1 + undef261 <= w_15^0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate