YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef2, z^0 -> ((0 + undef2) + z^0)}> (~(1) + x^0), y^0 -> (~(1) + y^0)}> Fresh variables: undef2, Undef variables: undef2, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: undef2, z^0 -> ((0 + undef2) + z^0)}> (~(1) + x^0), y^0 -> (~(1) + y^0)}> Fresh variables: undef2, Undef variables: undef2, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef2, z^0 -> z^0 + undef2, rest remain the same}> -1 + x^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Precedence: Graph 0 Graph 1 Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.003188 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001167s Ranking function: x^0 New Graphs: Transitions: undef2, z^0 -> z^0 + undef2, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000567s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002011s Trying to remove transition: undef2, z^0 -> z^0 + undef2, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004353s Time used: 0.00419 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006559s Time used: 0.006233 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009129s Time used: 0.009126 LOG: SAT solveNonLinear - Elapsed time: 0.015688s Cost: 1; Total time: 0.015359 Failed at location 2: 1 + x^0 + z^0 <= 0 Before Improving: Quasi-invariant at l2: 1 + x^0 + z^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001582s Remaining time after improvement: 0.999368 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: 1 + x^0 + z^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): undef2, z^0 -> z^0 + undef2, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + x^0, y^0 -> -1 + y^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): undef2, z^0 -> z^0 + undef2, rest remain the same}> Ranking function: -3*y^0 + 2*z^0 New Graphs: Calling Safety with literal 1 + x^0 + z^0 <= 0 and entry LOG: CALL check - Post:1 + x^0 + z^0 <= 0 - Process 1 * Exit transition: * Postcondition : 1 + x^0 + z^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000159s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000186s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 1 + x^0 + z^0 <= 0 , Narrowing transition: undef2, z^0 -> z^0 + undef2, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: -1 + x^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef2, z^0 -> z^0 + undef2, rest remain the same}> -1 + x^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000734s Ranking function: x^0 New Graphs: Transitions: undef2, z^0 -> z^0 + undef2, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000354s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001406s Trying to remove transition: undef2, z^0 -> z^0 + undef2, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003275s Time used: 0.003186 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005759s Time used: 0.005484 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.007795s Time used: 0.007792 LOG: SAT solveNonLinear - Elapsed time: 0.013554s Cost: 1; Total time: 0.013276 Failed at location 2: 1 + x^0 + z^0 <= y^0 Before Improving: Quasi-invariant at l2: 1 + x^0 + z^0 <= y^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001694s Remaining time after improvement: 0.999249 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: 1 + x^0 + z^0 <= y^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: undef2, z^0 -> z^0 + undef2, 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^0, y^0 -> -1 + y^0, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef2, z^0 -> z^0 + undef2, rest remain the same}> New Graphs: Calling Safety with literal 1 + x^0 + z^0 <= y^0 and entry LOG: CALL check - Post:1 + x^0 + z^0 <= y^0 - Process 2 * Exit transition: * Postcondition : 1 + x^0 + z^0 <= y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000240s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000274s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 1 + x^0 + z^0 <= y^0 , Narrowing transition: undef2, z^0 -> z^0 + undef2, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: -1 + x^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef2, z^0 -> z^0 + undef2, rest remain the same}> -1 + x^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000874s Ranking function: x^0 New Graphs: Transitions: undef2, z^0 -> z^0 + undef2, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000405s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001570s Trying to remove transition: undef2, z^0 -> z^0 + undef2, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004620s Time used: 0.004527 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006371s Time used: 0.006054 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010724s Time used: 0.010723 LOG: SAT solveNonLinear - Elapsed time: 0.017096s Cost: 1; Total time: 0.016777 Failed at location 2: 1 + x^0 <= 0 Before Improving: Quasi-invariant at l2: 1 + x^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001828s Remaining time after improvement: 0.999143 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: 1 + 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: undef2, z^0 -> z^0 + undef2, 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^0, y^0 -> -1 + y^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: undef2, z^0 -> z^0 + undef2, rest remain the same}> New Graphs: Calling Safety with literal 1 + x^0 <= 0 and entry LOG: CALL check - Post:1 + x^0 <= 0 - Process 3 * Exit transition: * Postcondition : 1 + x^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000277s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000315s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 1 + x^0 <= 0 , Narrowing transition: undef2, z^0 -> z^0 + undef2, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: -1 + x^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef2, z^0 -> z^0 + undef2, rest remain the same}> -1 + x^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000923s Ranking function: x^0 New Graphs: Transitions: undef2, z^0 -> z^0 + undef2, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000412s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001590s Trying to remove transition: undef2, z^0 -> z^0 + undef2, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004569s Time used: 0.004476 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006940s Time used: 0.006599 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009328s Time used: 0.009326 LOG: SAT solveNonLinear - Elapsed time: 0.016268s Cost: 1; Total time: 0.015925 Failed at location 2: 1 + x^0 + y^0 <= 0 Before Improving: Quasi-invariant at l2: 1 + x^0 + y^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002350s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001019s Remaining time after improvement: 0.997765 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: x^0 + y^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): undef2, z^0 -> z^0 + undef2, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + x^0, y^0 -> -1 + y^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): undef2, z^0 -> z^0 + undef2, rest remain the same}> Ranking function: x^0 + z^0 New Graphs: Calling Safety with literal x^0 + y^0 <= 0 and entry LOG: CALL check - Post:x^0 + y^0 <= 0 - Process 4 * Exit transition: * Postcondition : x^0 + y^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000244s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000290s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: x^0 + y^0 <= 0 , Narrowing transition: undef2, z^0 -> z^0 + undef2, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: -1 + x^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef2, z^0 -> z^0 + undef2, rest remain the same}> -1 + x^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001018s Ranking function: x^0 + y^0 New Graphs: Program Terminates