NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef5}> undef10, x_5^0 -> undef11}> Fresh variables: undef5, undef10, undef11, Undef variables: undef5, undef10, undef11, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: undef5}> undef11}> Fresh variables: undef5, undef10, undef11, Undef variables: undef5, undef10, undef11, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef5, rest remain the same}> Variables: x_5^0, y_6^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 undef11, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ( 4 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.00094 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000293s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000908s Trying to remove transition: undef5, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.002106s Time used: 0.002021 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003216s Time used: 0.00303 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.005183s Time used: 0.005181 LOG: SAT solveNonLinear - Elapsed time: 0.008399s Cost: 1; Total time: 0.008211 Failed at location 2: 1 + x_5^0 + y_6^0 <= 0 Before Improving: Quasi-invariant at l2: 1 + x_5^0 + y_6^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000967s Remaining time after improvement: 0.999557 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: 1 + x_5^0 + y_6^0 <= 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: undef5, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef5, rest remain the same}> New Graphs: Calling Safety with literal 1 + x_5^0 + y_6^0 <= 0 and entry LOG: CALL check - Post:1 + x_5^0 + y_6^0 <= 0 - Process 1 * Exit transition: * Postcondition : 1 + x_5^0 + y_6^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000164s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000192s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 1 + x_5^0 + y_6^0 <= 0 , Narrowing transition: undef5, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef5, rest remain the same}> Variables: x_5^0, y_6^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000273s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000920s Trying to remove transition: undef5, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001895s Time used: 0.001817 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003594s Time used: 0.003395 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.004879s Time used: 0.004877 LOG: SAT solveNonLinear - Elapsed time: 0.008473s Cost: 1; Total time: 0.008272 Failed at location 2: 1 + y_6^0 <= 0 Before Improving: Quasi-invariant at l2: 1 + y_6^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001054s Remaining time after improvement: 0.999441 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: 1 + y_6^0 <= 0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef5, 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): undef5, rest remain the same}> Ranking function: 2*x_5^0 + y_6^0 New Graphs: Calling Safety with literal 1 + y_6^0 <= 0 and entry LOG: CALL check - Post:1 + y_6^0 <= 0 - Process 2 * Exit transition: * Postcondition : 1 + y_6^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000155s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000182s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 1 + y_6^0 <= 0 , Narrowing transition: undef5, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef5, rest remain the same}> Variables: x_5^0, y_6^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000299s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001007s Trying to remove transition: undef5, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001937s Time used: 0.001856 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003422s Time used: 0.003269 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.000511s Time used: 4.00026 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003144s Time used: 1.00024 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004698s Time used: 0.002791 Proving non-termination of subgraph 1 Transitions: undef5, rest remain the same}> Variables: x_5^0, y_6^0 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000479s Checking conditional non-termination of SCC {l2}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007544s Time used: 0.007411 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.017165s Time used: 0.017163 LOG: SAT solveNonLinear - Elapsed time: 0.024709s Cost: 2; Total time: 0.024574 Failed at location 2: 0 <= x_5^0 + y_6^0 Before Improving: Quasi-invariant at l2: 0 <= x_5^0 + y_6^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004023s Remaining time after improvement: 0.999127 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.001566s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: 0 <= x_5^0 + y_6^0 Strengthening and disabling EXIT transitions... Closed exits from l2: 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): undef5, rest remain the same}> Checking conditional non-termination of SCC {l2}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008498s Time used: 0.008367 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010286s Time used: 0.010284 LOG: SAT solveNonLinear - Elapsed time: 0.018784s Cost: 1; Total time: 0.018651 Failed at location 2: 0 <= y_6^0 Before Improving: Quasi-invariant at l2: 0 <= y_6^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003768s Remaining time after improvement: 0.99917 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.001423s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: 0 <= y_6^0 Strengthening and disabling EXIT transitions... Closed exits from l2: 1 Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef5, rest remain the same}> Calling reachability with... Transition: Conditions: 0 <= x_5^0 + y_6^0, 0 <= y_6^0, OPEN EXITS: (condsUp: 0 <= y_6^0) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 0 <= x_5^0 + y_6^0, 0 <= y_6^0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate