NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef1, l_11^0 -> (0 + x_12^0), len_98^0 -> undef3}> Fresh variables: undef1, undef3, undef5, Undef variables: undef1, undef3, undef5, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: (0 + x_12^0), len_98^0 -> undef3}> Fresh variables: undef1, undef3, undef5, Undef variables: undef1, undef3, undef5, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: x_12^0, len_98^0 -> undef3, rest remain the same}> Variables: l_11^0, len_98^0, x_12^0 Precedence: Graph 0 Graph 1 Map Locations to Subgraph: ( 0 , 0 ) ( 1 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.002165 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000716s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002454s Trying to remove transition: x_12^0, len_98^0 -> undef3, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004207s Time used: 0.003994 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005301s Time used: 0.00492 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.006847s Time used: 0.006846 LOG: SAT solveNonLinear - Elapsed time: 0.012148s Cost: 1; Total time: 0.011766 Failed at location 1: 1 + len_98^0 <= l_11^0 Before Improving: Quasi-invariant at l1: 1 + len_98^0 <= l_11^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001199s Remaining time after improvement: 0.999426 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 + len_98^0 <= l_11^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: x_12^0, len_98^0 -> undef3, 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: x_12^0, len_98^0 -> undef3, rest remain the same}> New Graphs: Calling Safety with literal 1 + len_98^0 <= l_11^0 and entry LOG: CALL check - Post:1 + len_98^0 <= l_11^0 - Process 1 * Exit transition: * Postcondition : 1 + len_98^0 <= l_11^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000193s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000221s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 1 + len_98^0 <= l_11^0 , Narrowing transition: x_12^0, len_98^0 -> undef3, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: x_12^0, len_98^0 -> undef3, rest remain the same}> Variables: l_11^0, len_98^0, x_12^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000352s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001275s Trying to remove transition: x_12^0, len_98^0 -> undef3, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.002845s Time used: 0.002755 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003900s Time used: 0.003602 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.005443s Time used: 0.005441 LOG: SAT solveNonLinear - Elapsed time: 0.009343s Cost: 1; Total time: 0.009043 Failed at location 1: 1 + l_11^0 <= 0 Before Improving: Quasi-invariant at l1: 1 + l_11^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001260s Remaining time after improvement: 0.999357 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 + l_11^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: x_12^0, len_98^0 -> undef3, 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: x_12^0, len_98^0 -> undef3, rest remain the same}> New Graphs: Calling Safety with literal 1 + l_11^0 <= 0 and entry LOG: CALL check - Post:1 + l_11^0 <= 0 - Process 2 * Exit transition: * Postcondition : 1 + l_11^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000220s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000247s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 1 + l_11^0 <= 0 , Narrowing transition: x_12^0, len_98^0 -> undef3, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: x_12^0, len_98^0 -> undef3, rest remain the same}> Variables: l_11^0, len_98^0, x_12^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000381s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001373s Trying to remove transition: x_12^0, len_98^0 -> undef3, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003058s Time used: 0.002968 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004242s Time used: 0.00394 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.004778s Time used: 0.004777 LOG: SAT solveNonLinear - Elapsed time: 0.009021s Cost: 1; Total time: 0.008717 Failed at location 1: 1 <= l_11^0 Before Improving: Quasi-invariant at l1: 1 <= l_11^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001328s Remaining time after improvement: 0.99929 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 <= l_11^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: x_12^0, len_98^0 -> undef3, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: x_12^0, len_98^0 -> undef3, rest remain the same}> New Graphs: Calling Safety with literal 1 <= l_11^0 and entry LOG: CALL check - Post:1 <= l_11^0 - Process 3 * Exit transition: * Postcondition : 1 <= l_11^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000257s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000289s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 1 <= l_11^0 , Narrowing transition: x_12^0, len_98^0 -> undef3, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: x_12^0, len_98^0 -> undef3, rest remain the same}> Variables: l_11^0, len_98^0, x_12^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000372s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001310s Trying to remove transition: x_12^0, len_98^0 -> undef3, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.002934s Time used: 0.002843 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004300s Time used: 0.00399 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.005268s Time used: 0.005243 LOG: SAT solveNonLinear - Elapsed time: 0.009568s Cost: 1; Total time: 0.009233 Failed at location 1: l_11^0 + len_98^0 <= 0 Before Improving: Quasi-invariant at l1: l_11^0 + len_98^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001385s Remaining time after improvement: 0.99928 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: l_11^0 + len_98^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: x_12^0, len_98^0 -> undef3, 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: x_12^0, len_98^0 -> undef3, rest remain the same}> New Graphs: Calling Safety with literal l_11^0 + len_98^0 <= 0 and entry LOG: CALL check - Post:l_11^0 + len_98^0 <= 0 - Process 4 * Exit transition: * Postcondition : l_11^0 + len_98^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000271s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000307s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: l_11^0 + len_98^0 <= 0 , Narrowing transition: x_12^0, len_98^0 -> undef3, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: x_12^0, len_98^0 -> undef3, rest remain the same}> Variables: l_11^0, len_98^0, x_12^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000407s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001466s Trying to remove transition: x_12^0, len_98^0 -> undef3, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003151s Time used: 0.003056 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005448s Time used: 0.005114 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.005121s Time used: 0.005115 LOG: SAT solveNonLinear - Elapsed time: 0.010569s Cost: 1; Total time: 0.010229 Failed at location 1: 1 + x_12^0 <= 0 Before Improving: Quasi-invariant at l1: 1 + x_12^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001396s Remaining time after improvement: 0.999231 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 + x_12^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): x_12^0, len_98^0 -> undef3, 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): x_12^0, len_98^0 -> undef3, rest remain the same}> Ranking function: l_11^0 New Graphs: Calling Safety with literal 1 + x_12^0 <= 0 and entry LOG: CALL check - Post:1 + x_12^0 <= 0 - Process 5 * Exit transition: * Postcondition : 1 + x_12^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000226s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000262s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 1 + x_12^0 <= 0 , Narrowing transition: x_12^0, len_98^0 -> undef3, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: x_12^0, len_98^0 -> undef3, rest remain the same}> Variables: l_11^0, len_98^0, x_12^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000444s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001614s Trying to remove transition: x_12^0, len_98^0 -> undef3, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003128s Time used: 0.003023 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005036s Time used: 0.004688 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.004919s Time used: 0.004918 LOG: SAT solveNonLinear - Elapsed time: 0.009956s Cost: 1; Total time: 0.009606 Failed at location 1: 1 <= l_11^0 + x_12^0 Before Improving: Quasi-invariant at l1: 1 <= l_11^0 + x_12^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001528s Remaining time after improvement: 0.999136 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 <= l_11^0 + x_12^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x_12^0, len_98^0 -> undef3, 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): x_12^0, len_98^0 -> undef3, rest remain the same}> Ranking function: -l_11^0 New Graphs: Calling Safety with literal 1 <= l_11^0 + x_12^0 and entry LOG: CALL check - Post:1 <= l_11^0 + x_12^0 - Process 6 * Exit transition: * Postcondition : 1 <= l_11^0 + x_12^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000258s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000309s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 1 <= l_11^0 + x_12^0 , Narrowing transition: x_12^0, len_98^0 -> undef3, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: x_12^0, len_98^0 -> undef3, rest remain the same}> Variables: l_11^0, len_98^0, x_12^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000473s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001724s Trying to remove transition: x_12^0, len_98^0 -> undef3, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003361s Time used: 0.003253 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004520s Time used: 0.004244 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.000900s Time used: 4.00053 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.004251s Time used: 1.00058 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008201s Time used: 0.004977 Proving non-termination of subgraph 1 Transitions: x_12^0, len_98^0 -> undef3, rest remain the same}> Variables: l_11^0, len_98^0, x_12^0 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000955s Checking conditional non-termination of SCC {l1}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.064231s Time used: 0.063798 Improving Solution with cost 13 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.167915s Time used: 0.167912 LOG: SAT solveNonLinear - Elapsed time: 0.232146s Cost: 13; Total time: 0.23171 Failed at location 1: 1 <= l_11^0 + len_98^0 Before Improving: Quasi-invariant at l1: 1 <= l_11^0 + len_98^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.022621s Remaining time after improvement: 0.996163 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.006589s Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 <= l_11^0 + len_98^0 Constraint over undef '1 + len_98^0 <= undef3' in transition: x_12^0, len_98^0 -> undef3, rest remain the same}> Strengthening and disabling EXIT transitions... Closed exits from l1: 10 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): 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): x_12^0, len_98^0 -> undef3, 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.036014s Time used: 0.035645 Improving Solution with cost 4 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.061537s Time used: 0.061535 LOG: SAT solveNonLinear - Elapsed time: 0.097551s Cost: 4; Total time: 0.09718 Failed at location 1: l_11^0 <= 0 Before Improving: Quasi-invariant at l1: l_11^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.017642s Remaining time after improvement: 0.996238 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.005260s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: l_11^0 <= 0 Strengthening and disabling EXIT transitions... Closed exits from l1: 7 Strengthening exit transition (result): 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): x_12^0, len_98^0 -> undef3, 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.016647s Time used: 0.01638 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.040399s Time used: 0.040397 LOG: SAT solveNonLinear - Elapsed time: 0.057046s Cost: 2; Total time: 0.056777 Failed at location 1: x_12^0 <= l_11^0 Before Improving: Quasi-invariant at l1: x_12^0 <= l_11^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.012242s Remaining time after improvement: 0.997823 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.003604s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: x_12^0 <= l_11^0 Strengthening and disabling EXIT transitions... Closed exits from l1: 2 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): x_12^0, len_98^0 -> undef3, 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.000619s Time used: 5.00053 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.105365s Time used: 5.00275 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.134746s Time used: 0.036755 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.037908s Time used: 0.037905 LOG: SAT solveNonLinear - Elapsed time: 0.172653s Cost: 1; Total time: 0.07466 Failed at location 1: 0 <= x_12^0 Before Improving: Quasi-invariant at l1: 0 <= x_12^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004701s Remaining time after improvement: 0.997791 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.004750s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 0 <= x_12^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 Strengthening transition (result): x_12^0, len_98^0 -> undef3, rest remain the same}> Calling reachability with... Transition: Conditions: 1 <= l_11^0 + len_98^0, l_11^0 <= 0, x_12^0 <= l_11^0, 0 <= x_12^0, OPEN EXITS: (condsUp: 0 <= x_12^0) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 1 <= l_11^0 + len_98^0, l_11^0 <= 0, x_12^0 <= l_11^0, 0 <= x_12^0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate