NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef1}> undef6, y_6^0 -> (1 + y_6^0)}> undef14}> (1 + x_5^0)}> Fresh variables: undef1, undef6, undef14, Undef variables: undef1, undef6, undef14, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: (1 + y_6^0)}> (1 + x_5^0)}> (1 + x_5^0)}> Fresh variables: undef1, undef6, undef14, Undef variables: undef1, undef6, undef14, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: 1 + y_6^0, rest remain the same}> 1 + x_5^0, rest remain the same}> 1 + x_5^0, rest remain the same}> Variables: x_5^0, y_6^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 Map Locations to Subgraph: ( 0 , 0 ) ( 1 , 1 ) ( 2 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.004348 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001037s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010586s Trying to remove transition: 1 + x_5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007003s Time used: 0.006853 Trying to remove transition: 1 + x_5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006380s Time used: 0.005966 Trying to remove transition: 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004352s Time used: 0.003973 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013265s Time used: 0.012829 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.028949s Time used: 0.028947 LOG: SAT solveNonLinear - Elapsed time: 0.042214s Cost: 1; Total time: 0.041776 Failed at location 1: 1 + y_6^0 <= x_5^0 Before Improving: Quasi-invariant at l1: 1 + y_6^0 <= x_5^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004511s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001113s Remaining time after improvement: 0.997597 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: y_6^0 <= x_5^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + y_6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + x_5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + x_5^0, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + y_6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + x_5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + x_5^0, rest remain the same}> New Graphs: Calling Safety with literal y_6^0 <= x_5^0 and entry LOG: CALL check - Post:y_6^0 <= x_5^0 - Process 1 * Exit transition: * Postcondition : y_6^0 <= x_5^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000214s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000242s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: y_6^0 <= x_5^0 , Narrowing transition: 1 + y_6^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + x_5^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + x_5^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: 1 + y_6^0, rest remain the same}> 1 + x_5^0, rest remain the same}> 1 + x_5^0, rest remain the same}> Variables: x_5^0, y_6^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000677s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008138s Trying to remove transition: 1 + x_5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006225s Time used: 0.00611 Trying to remove transition: 1 + x_5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006416s Time used: 0.005985 Trying to remove transition: 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004422s Time used: 0.004011 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002017s Time used: 4.0016 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.011813s Time used: 4.00096 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006398s Time used: 1.00044 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.020146s Time used: 0.011901 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.020927s Time used: 0.020925 LOG: SAT solveNonLinear - Elapsed time: 0.041073s Cost: 1; Total time: 0.032826 Quasi-ranking function: 50000 - x_5^0 New Graphs: Transitions: 1 + y_6^0, rest remain the same}> 1 + x_5^0, rest remain the same}> 1 + x_5^0, rest remain the same}> Variables: x_5^0, y_6^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000829s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009894s Trying to remove transition: 1 + x_5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007647s Time used: 0.007295 Trying to remove transition: 1 + x_5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008064s Time used: 0.007572 Trying to remove transition: 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005569s Time used: 0.005098 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.064823s Time used: 4.06436 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.018335s Time used: 4.0138 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005189s Time used: 1.00008 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022723s Time used: 0.01418 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.029333s Time used: 0.029331 LOG: SAT solveNonLinear - Elapsed time: 0.052057s Cost: 1; Total time: 0.043511 Termination implied by a set of invariant(s): Invariant at l1: x_5^0 <= 1 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + y_6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + x_5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + x_5^0, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + y_6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + x_5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + x_5^0, rest remain the same}> Quasi-ranking function: 50000 - y_6^0 New Graphs: Transitions: 1 + y_6^0, rest remain the same}> 1 + x_5^0, rest remain the same}> 1 + x_5^0, rest remain the same}> Variables: x_5^0, y_6^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000806s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.012408s Trying to remove transition: 1 + x_5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009602s Time used: 0.009276 Trying to remove transition: 1 + x_5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008721s Time used: 0.008131 Trying to remove transition: 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005554s Time used: 0.004994 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.016150s Time used: 4.01558 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.875586s Time used: 4.87157 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007632s Time used: 1.001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022540s Time used: 0.013978 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.021844s Time used: 0.021842 LOG: SAT solveNonLinear - Elapsed time: 0.044385s Cost: 1; Total time: 0.03582 Termination implied by a set of invariant(s): Invariant at l1: x_5^0 <= 1 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + y_6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + x_5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + x_5^0, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + y_6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + x_5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + x_5^0, rest remain the same}> Quasi-ranking function: 50000 - x_5^0 - y_6^0 New Graphs: Transitions: 1 + y_6^0, rest remain the same}> 1 + x_5^0, rest remain the same}> 1 + x_5^0, rest remain the same}> Variables: x_5^0, y_6^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001022s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.024572s Trying to remove transition: 1 + x_5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010950s Time used: 0.010433 Trying to remove transition: 1 + x_5^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010482s Time used: 0.009993 Trying to remove transition: 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006131s Time used: 0.005661 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006951s Time used: 4.00306 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.012935s Time used: 4.00175 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005483s Time used: 1.00057 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.023224s Time used: 0.014491 Proving non-termination of subgraph 1 Transitions: 1 + y_6^0, rest remain the same}> 1 + x_5^0, rest remain the same}> 1 + x_5^0, rest remain the same}> Variables: x_5^0, y_6^0 Checking conditional non-termination of SCC {l1}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.010180s Time used: 5.00106 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.017053s Time used: 5.0106 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.016610s Time used: 5.00113 > Checking if the negation of the conditions of every pending exit is quasi-invariant... NO Proving non-termination of subgraph 1 Transitions: 1 + y_6^0, rest remain the same}> 1 + x_5^0, rest remain the same}> 1 + x_5^0, rest remain the same}> Variables: x_5^0, y_6^0 Checking conditional non-termination of SCC {l1}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.026816s Time used: 0.026614 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000622s Time used: 1.0006 LOG: SAT solveNonLinear - Elapsed time: 1.027438s Cost: 5; Total time: 1.02722 Failed at location 1: x_5^0 <= 0 Before Improving: Quasi-invariant at l1: x_5^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.013442s Remaining time after improvement: 0.997609 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.004036s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: x_5^0 <= 0 Strengthening and disabling EXIT transitions... Closed exits from l1: 3 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + y_6^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + x_5^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + x_5^0, rest remain the same}> Checking conditional non-termination of SCC {l1}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006963s Time used: 0.006853 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002461s Time used: 1.00245 LOG: SAT solveNonLinear - Elapsed time: 1.009424s Cost: 2; Total time: 1.0093 Failed at location 1: 1 + x_5^0 <= y_6^0 Before Improving: Quasi-invariant at l1: 1 + x_5^0 <= y_6^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004358s Remaining time after improvement: 0.998546 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.002326s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 + x_5^0 <= y_6^0 Strengthening and disabling EXIT transitions... Closed exits from l1: 1 Strengthening exit transition (result): Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + y_6^0, rest remain the same}> Checking conditional non-termination of SCC {l1}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.042824s Time used: 5.04271 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.035640s Time used: 5.00481 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.009022s Time used: 5.00355 > Checking if the negation of the conditions of every pending exit is quasi-invariant... YES Calling reachability with... Transition: Conditions: 1 + x_5^0 <= y_6^0, x_5^0 <= 50000, 50001 <= x_5^0 + y_6^0, x_5^0 <= 0, OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: x_5^0 <= 0, 1 + x_5^0 <= y_6^0, 50001 <= x_5^0 + y_6^0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate