NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: ((0 + x^0) + y^0), y^0 -> (~(2) + y^0)}> ((0 + x^0) + z^0), y^0 -> (1 + y^0), z^0 -> (~(2) + z^0)}> Fresh variables: Undef variables: Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: ((0 + x^0) + y^0), y^0 -> (~(2) + y^0)}> ((0 + x^0) + z^0), y^0 -> (1 + y^0), z^0 -> (~(2) + z^0)}> Fresh variables: Undef variables: Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: x^0 + y^0, y^0 -> -2 + y^0, rest remain the same}> x^0 + z^0, y^0 -> 1 + y^0, z^0 -> -2 + z^0, rest remain the same}> Variables: x^0, y^0, z^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.004207 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000923s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001924s Trying to remove transition: x^0 + z^0, y^0 -> 1 + y^0, z^0 -> -2 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007340s Time used: 0.007249 Trying to remove transition: x^0 + y^0, y^0 -> -2 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003790s Time used: 0.003238 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001754s Time used: 4.00141 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005654s Time used: 4.00065 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006130s Time used: 1.00048 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018968s Time used: 0.009804 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015098s Time used: 0.015096 LOG: SAT solveNonLinear - Elapsed time: 0.034066s Cost: 1; Total time: 0.0249 Quasi-ranking function: 50000 + y^0 + z^0 New Graphs: Transitions: x^0 + y^0, y^0 -> -2 + y^0, rest remain the same}> x^0 + z^0, y^0 -> 1 + y^0, z^0 -> -2 + z^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000449s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002973s Trying to remove transition: x^0 + z^0, y^0 -> 1 + y^0, z^0 -> -2 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010019s Time used: 0.009916 Trying to remove transition: x^0 + y^0, y^0 -> -2 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007487s Time used: 0.006824 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002021s Time used: 4.00147 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005726s Time used: 4.00085 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006314s Time used: 1.00002 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019645s Time used: 0.009724 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.012699s Time used: 0.012696 LOG: SAT solveNonLinear - Elapsed time: 0.032344s Cost: 1; Total time: 0.02242 Quasi-ranking function: 50000 + z^0 New Graphs: Transitions: x^0 + y^0, y^0 -> -2 + y^0, rest remain the same}> x^0 + z^0, y^0 -> 1 + y^0, z^0 -> -2 + z^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000521s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003185s Trying to remove transition: x^0 + z^0, y^0 -> 1 + y^0, z^0 -> -2 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011330s Time used: 0.011222 Trying to remove transition: x^0 + y^0, y^0 -> -2 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007375s Time used: 0.006795 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002330s Time used: 4.00178 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004792s Time used: 4.0008 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006701s Time used: 1.00009 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.020785s Time used: 0.011525 Termination failed. Trying to show unreachability... Proving unreachability of entry: LOG: CALL check - Post:1 <= 0 - Process 1 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001513s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001544s Cannot prove unreachability Proving non-termination of subgraph 1 Transitions: x^0 + y^0, y^0 -> -2 + y^0, rest remain the same}> x^0 + z^0, y^0 -> 1 + y^0, z^0 -> -2 + z^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional non-termination of SCC {l1}... > No exit transition to close. Calling reachability with... Transition: Conditions: OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: OPEN EXITS: > Conditions are reachable! Program does NOT terminate