NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef1}> Fresh variables: undef1, Undef variables: undef1, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: undef1}> Fresh variables: undef1, Undef variables: undef1, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef1, rest remain the same}> Variables: x^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.001324 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000535s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001775s Trying to remove transition: undef1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003326s Time used: 0.003165 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.617278s Time used: 2.61702 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.200119s Time used: 0.200115 LOG: SAT solveNonLinear - Elapsed time: 2.817397s Cost: 1; Total time: 2.81714 Failed at location 1: 859 + x^0 <= 0 Before Improving: Quasi-invariant at l1: 859 + x^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006573s Remaining time after improvement: 0.998732 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 859 + x^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: undef1, 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: undef1, rest remain the same}> New Graphs: Calling Safety with literal 859 + x^0 <= 0 and entry LOG: CALL check - Post:859 + x^0 <= 0 - Process 1 * Exit transition: * Postcondition : 859 + x^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000764s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000792s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 859 + x^0 <= 0 , Narrowing transition: undef1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef1, rest remain the same}> Variables: x^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000289s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001080s Trying to remove transition: undef1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001773s Time used: 0.001694 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.397767s Time used: 2.39758 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.076358s Time used: 0.076354 LOG: SAT solveNonLinear - Elapsed time: 2.474125s Cost: 1; Total time: 2.47393 Failed at location 1: 808 + x^0 <= 0 Before Improving: Quasi-invariant at l1: 808 + x^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006428s Remaining time after improvement: 0.99843 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 808 + x^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: undef1, 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: undef1, rest remain the same}> New Graphs: Calling Safety with literal 808 + x^0 <= 0 and entry LOG: CALL check - Post:808 + x^0 <= 0 - Process 2 * Exit transition: * Postcondition : 808 + x^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000906s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000936s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 808 + x^0 <= 0 , Narrowing transition: undef1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef1, rest remain the same}> Variables: x^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000308s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001115s Trying to remove transition: undef1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001818s Time used: 0.001737 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.388156s Time used: 2.38797 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.076657s Time used: 0.076655 LOG: SAT solveNonLinear - Elapsed time: 2.464813s Cost: 1; Total time: 2.46462 Failed at location 1: 803 + x^0 <= 0 Before Improving: Quasi-invariant at l1: 803 + x^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006959s Remaining time after improvement: 0.998361 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 803 + x^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: undef1, 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: undef1, rest remain the same}> New Graphs: Calling Safety with literal 803 + x^0 <= 0 and entry LOG: CALL check - Post:803 + x^0 <= 0 - Process 3 * Exit transition: * Postcondition : 803 + x^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000950s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000981s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 803 + x^0 <= 0 , Narrowing transition: undef1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef1, rest remain the same}> Variables: x^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000312s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001155s Trying to remove transition: undef1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001910s Time used: 0.001829 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.383445s Time used: 2.38325 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.077111s Time used: 0.077108 LOG: SAT solveNonLinear - Elapsed time: 2.460556s Cost: 1; Total time: 2.46035 Failed at location 1: 802 + x^0 <= 0 Before Improving: Quasi-invariant at l1: 802 + x^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007240s Remaining time after improvement: 0.998258 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 802 + x^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: undef1, 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: undef1, rest remain the same}> New Graphs: Calling Safety with literal 802 + x^0 <= 0 and entry LOG: CALL check - Post:802 + x^0 <= 0 - Process 4 * Exit transition: * Postcondition : 802 + x^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001000s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001031s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 802 + x^0 <= 0 , Narrowing transition: undef1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef1, rest remain the same}> Variables: x^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000317s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001176s Trying to remove transition: undef1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001953s Time used: 0.001868 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.390291s Time used: 2.39009 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.077340s Time used: 0.077337 LOG: SAT solveNonLinear - Elapsed time: 2.467631s Cost: 1; Total time: 2.46742 Failed at location 1: 801 + x^0 <= 0 Before Improving: Quasi-invariant at l1: 801 + x^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007378s Remaining time after improvement: 0.998251 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 801 + x^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: undef1, 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: undef1, rest remain the same}> New Graphs: Calling Safety with literal 801 + x^0 <= 0 and entry LOG: CALL check - Post:801 + x^0 <= 0 - Process 5 * Exit transition: * Postcondition : 801 + x^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001011s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001042s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 801 + x^0 <= 0 , Narrowing transition: undef1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef1, rest remain the same}> Variables: x^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000315s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001167s Trying to remove transition: undef1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001969s Time used: 0.001886 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.425149s Time used: 2.42495 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.077345s Time used: 0.077343 LOG: SAT solveNonLinear - Elapsed time: 2.502494s Cost: 1; Total time: 2.50229 Failed at location 1: 800 + x^0 <= 0 Before Improving: Quasi-invariant at l1: 800 + x^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007447s Remaining time after improvement: 0.998196 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 800 + x^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: undef1, 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: undef1, rest remain the same}> New Graphs: Calling Safety with literal 800 + x^0 <= 0 and entry LOG: CALL check - Post:800 + x^0 <= 0 - Process 6 * Exit transition: * Postcondition : 800 + x^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001032s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001062s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 800 + x^0 <= 0 , Narrowing transition: undef1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef1, rest remain the same}> Variables: x^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000314s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001069s Trying to remove transition: undef1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001972s Time used: 0.001889 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003018s Time used: 4.00288 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.008669s Time used: 4.00155 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.008368s Time used: 1.00073 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005015s Time used: 0.00291 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.004790s Time used: 0.004789 LOG: SAT solveNonLinear - Elapsed time: 0.009805s Cost: 1; Total time: 0.007699 Quasi-ranking function: 50000 - x^0 New Graphs: Transitions: undef1, rest remain the same}> Variables: x^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000313s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001150s Trying to remove transition: undef1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.002093s Time used: 0.002011 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002472s Time used: 4.00234 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006409s Time used: 4.00157 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.015562s Time used: 1.00083 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004179s Time used: 0.002221 Proving non-termination of subgraph 1 Transitions: undef1, rest remain the same}> Variables: x^0 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000600s Checking conditional non-termination of SCC {l1}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006184s Time used: 0.006054 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.008218s Time used: 0.008216 LOG: SAT solveNonLinear - Elapsed time: 0.014403s Cost: 1; Total time: 0.01427 Failed at location 1: 1 <= x^0 Before Improving: Quasi-invariant at l1: 1 <= x^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003530s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001220s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000696s Remaining time after improvement: 0.99695 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.001348s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 0 <= 399 + x^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): undef1, rest remain the same}> Calling reachability with... Transition: Conditions: 0 <= 399 + x^0, OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 0 <= 399 + x^0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate