NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: (1 + num^0)}> 0, i^0 -> (1 + i^0), status^0 -> 1}> 0, Pdo^0 -> 0, conditional^0 -> undef37}> 1, num^0 -> 0}> 1, conditional^0 -> undef67}> 0}> undef81, PPBlockInits^0 -> 1, status^0 -> 0}> 0, PPBlockInits^0 -> 1, PPBunlockInits^0 -> 0, Pdolen^0 -> undef96, i^0 -> undef98, status^0 -> 0}> Fresh variables: undef37, undef67, undef81, undef96, undef98, Undef variables: undef37, undef67, undef81, undef96, undef98, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 0}> 0}> (1 + i^0)}> 0}> (1 + num^0)}> Fresh variables: undef37, undef67, undef81, undef96, undef98, Undef variables: undef37, undef67, undef81, undef96, undef98, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: 1 + i^0, rest remain the same}> 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 0, rest remain the same}> 0, rest remain the same}> 0, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 3 , 1 ) ( 5 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.003048 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001074s Ranking function: -6 + 6*Pdolen^0 - 6*i^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000466s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001826s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004004s Time used: 0.003864 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006028s Time used: 0.00571 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.008420s Time used: 0.008418 LOG: SAT solveNonLinear - Elapsed time: 0.014448s Cost: 1; Total time: 0.014128 Failed at location 3: 1 + Pdolen^0 <= i^0 Before Improving: Quasi-invariant at l3: 1 + Pdolen^0 <= i^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002034s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000879s Remaining time after improvement: 0.99821 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: Pdolen^0 <= i^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 + i^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 + num^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 + num^0, rest remain the same}> New Graphs: Calling Safety with literal Pdolen^0 <= i^0 and entry LOG: CALL check - Post:Pdolen^0 <= i^0 - Process 1 * Exit transition: * Postcondition : Pdolen^0 <= i^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000275s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000312s INVARIANTS: 3: Quasi-INVARIANTS to narrow Graph: 3: Pdolen^0 <= i^0 , Narrowing transition: 1 + i^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + num^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: 1 + i^0, rest remain the same}> 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000745s Ranking function: -6 + 6*Pdolen^0 - 6*i^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000332s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001305s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003256s Time used: 0.003178 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001630s Time used: 4.00136 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005255s Time used: 4.00056 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003237s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010254s Time used: 0.005939 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.008124s Time used: 0.008122 LOG: SAT solveNonLinear - Elapsed time: 0.018378s Cost: 1; Total time: 0.014061 Termination implied by a set of invariant(s): Invariant at l3: i^0 <= 1 + Pdolen^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 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + num^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 + num^0, rest remain the same}> Quasi-ranking function: 50000 - num^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000392s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001529s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004271s Time used: 0.004176 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001882s Time used: 4.0015 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004220s Time used: 4.00054 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003047s Time used: 1.00009 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011818s Time used: 0.007154 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010707s Time used: 0.010705 LOG: SAT solveNonLinear - Elapsed time: 0.022525s Cost: 1; Total time: 0.017859 Termination implied by a set of invariant(s): Invariant at l3: i^0 <= Pdolen^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 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + num^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 + num^0, rest remain the same}> Quasi-ranking function: 50000 + 2*Pdolen^0 - 2*i^0 - num^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000461s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002052s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004753s Time used: 0.004641 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002312s Time used: 4.00196 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.009540s Time used: 4.00496 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003071s Time used: 1.00005 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012098s Time used: 0.007872 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.007131s Time used: 0.00713 LOG: SAT solveNonLinear - Elapsed time: 0.019229s Cost: 1; Total time: 0.015002 Termination implied by a set of invariant(s): Invariant at l3: i^0 <= Pdolen^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 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + num^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 + num^0, rest remain the same}> Quasi-ranking function: 50000 - Pdolen^0 + i^0 - num^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000510s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002128s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004745s Time used: 0.004633 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002722s Time used: 4.00234 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005603s Time used: 4.00072 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003265s Time used: 1.00009 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012927s Time used: 0.008308 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009425s Time used: 0.009423 LOG: SAT solveNonLinear - Elapsed time: 0.022352s Cost: 1; Total time: 0.017731 Quasi-ranking function: 50000 + Pdolen^0 + i^0 - num^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000576s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002539s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006010s Time used: 0.005895 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002886s Time used: 4.00246 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005342s Time used: 4.00082 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003148s Time used: 1.00004 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012920s Time used: 0.008717 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009466s Time used: 0.009464 LOG: SAT solveNonLinear - Elapsed time: 0.022386s Cost: 1; Total time: 0.018181 Quasi-ranking function: 50000 - Pdolen^0 - i^0 - num^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000633s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003298s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005823s Time used: 0.005691 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002958s Time used: 4.00253 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005827s Time used: 4.00097 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003305s Time used: 1.00002 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013378s Time used: 0.008825 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009211s Time used: 0.00921 LOG: SAT solveNonLinear - Elapsed time: 0.022590s Cost: 1; Total time: 0.018035 Quasi-ranking function: 50000 - i^0 - num^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000679s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003485s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006617s Time used: 0.006491 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002697s Time used: 4.00233 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004583s Time used: 4.00112 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003651s Time used: 1.0001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013748s Time used: 0.009099 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009019s Time used: 0.009018 LOG: SAT solveNonLinear - Elapsed time: 0.022767s Cost: 1; Total time: 0.018117 Quasi-ranking function: 50000 + 100004*i^0 - num^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000737s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003956s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006397s Time used: 0.006264 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002781s Time used: 4.0024 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005501s Time used: 4.00103 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003669s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014524s Time used: 0.009924 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.008925s Time used: 0.008924 LOG: SAT solveNonLinear - Elapsed time: 0.023449s Cost: 1; Total time: 0.018848 Termination implied by a set of invariant(s): Invariant at l3: i^0 <= Pdolen^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 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + num^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 + num^0, rest remain the same}> Quasi-ranking function: 50000 + Pdolen^0 - num^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000800s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004821s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007459s Time used: 0.007138 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003194s Time used: 4.00277 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006304s Time used: 4.00113 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003325s Time used: 1.00011 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.015115s Time used: 0.010833 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009822s Time used: 0.009819 LOG: SAT solveNonLinear - Elapsed time: 0.024937s Cost: 1; Total time: 0.020652 Quasi-ranking function: 50000 - Pdolen^0 - num^0 New Graphs: Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000826s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005559s Trying to remove transition: 1 + num^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007021s Time used: 0.006644 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003330s Time used: 4.00293 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006219s Time used: 4.0014 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003660s Time used: 1.00009 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013980s Time used: 0.009543 Proving non-termination of subgraph 1 Transitions: 1 + i^0, rest remain the same}> 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional non-termination of SCC {l3}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.002766s Time used: 5.00261 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.005415s Time used: 5.00152 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.007371s Time used: 5.00098 > Checking if the negation of the conditions of every pending exit is quasi-invariant... NO Proving non-termination of subgraph 1 Transitions: 1 + num^0, rest remain the same}> Variables: Pdolen^0, i^0, num^0 Checking conditional non-termination of SCC {l3}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.675108s Time used: 0.674237 Improving Solution with cost 37 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000593s Time used: 1.00059 LOG: SAT solveNonLinear - Elapsed time: 1.675702s Cost: 37; Total time: 1.67483 Failed at location 3: 1 + i^0 <= Pdolen^0 Before Improving: Quasi-invariant at l3: 1 + i^0 <= Pdolen^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011590s Remaining time after improvement: 0.990914 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.020176s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: 1 + i^0 <= Pdolen^0 Strengthening and disabling EXIT transitions... Closed exits from l3: 23 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 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 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): 1 + num^0, rest remain the same}> Checking conditional non-termination of SCC {l3}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.240450s Time used: 0.239821 Improving Solution with cost 15 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000517s Time used: 1.00051 LOG: SAT solveNonLinear - Elapsed time: 1.240966s Cost: 15; Total time: 1.24033 Failed at location 3: 1 + Pdolen^0 <= 0 Before Improving: Quasi-invariant at l3: 1 + Pdolen^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009299s Remaining time after improvement: 0.993888 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.012483s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: 1 + Pdolen^0 <= 0 Strengthening and disabling EXIT transitions... Closed exits from l3: 14 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): 1 + num^0, rest remain the same}> Checking conditional non-termination of SCC {l3}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.053928s Time used: 0.05364 Improving Solution with cost 12 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.108550s Time used: 0.108547 Improving Solution with cost 10 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000856s Time used: 1.00084 LOG: SAT solveNonLinear - Elapsed time: 1.163334s Cost: 10; Total time: 1.16303 Failed at location 3: 0 <= 3 + Pdolen^0 + i^0 Before Improving: Quasi-invariant at l3: 0 <= 3 + Pdolen^0 + i^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.021756s Remaining time after improvement: 0.996293 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.006760s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: 0 <= 3 + Pdolen^0 + i^0 Strengthening and disabling EXIT transitions... Closed exits from l3: 4 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): 1 + num^0, rest remain the same}> Checking conditional non-termination of SCC {l3}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.005986s Time used: 5.00588 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.008313s Time used: 5.0021 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.006494s Time used: 5.00203 > Checking if the negation of the conditions of every pending exit is quasi-invariant... YES Calling reachability with... Transition: Conditions: 1 + i^0 <= Pdolen^0, 50001 <= Pdolen^0 + i^0 + num^0, 50001 + i^0 <= Pdolen^0 + num^0, 50001 <= Pdolen^0 + num^0, 50001 + Pdolen^0 + i^0 <= num^0, 50001 + Pdolen^0 <= num^0, 50001 + 2*Pdolen^0 <= 2*i^0 + num^0, 50001 <= i^0 + num^0, 50001 <= num^0, 50001 + 100004*i^0 <= num^0, 1 + Pdolen^0 <= 0, 0 <= 3 + Pdolen^0 + i^0, OPEN EXITS: (condsUp: 1 + Pdolen^0 <= 0) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 1 + i^0 <= Pdolen^0, 50001 + Pdolen^0 + i^0 <= num^0, 50001 + Pdolen^0 <= num^0, 50001 + 2*Pdolen^0 <= 2*i^0 + num^0, 50001 + i^0 <= Pdolen^0 + num^0, 50001 <= Pdolen^0 + i^0 + num^0, 50001 <= Pdolen^0 + num^0, 50001 <= i^0 + num^0, 50001 + 100004*i^0 <= num^0, 50001 <= num^0, 0 <= 3 + Pdolen^0 + i^0, 1 + Pdolen^0 <= 0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate