YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: (~(2) + i^0)}> (1 + i^0)}> (1 + j10^0)}> (0 + undef78), ret_check12^0 -> undef78}> (0 + j^0)}> (1 + j6^0)}> (0 + undef183), ret_check8^0 -> undef183, tmp^0 -> undef184}> (0 + j^0)}> 0}> Fresh variables: undef78, undef183, undef184, Undef variables: undef78, undef183, undef184, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: (0 + (~(2) + i^0))}> (1 + i^0)}> (1 + j10^0)}> (1 + j10^0)}> (0 + (0 + undef183))}> (0 + (0 + undef183))}> (1 + j6^0)}> (1 + j6^0)}> Fresh variables: undef78, undef183, undef184, Undef variables: undef78, undef183, undef184, 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}> Variables: __const_100^0, i^0 Graph 2: Transitions: 1 + j6^0, rest remain the same}> 1 + j6^0, rest remain the same}> Variables: j6^0 Graph 3: Transitions: 1 + j10^0, rest remain the same}> 1 + j10^0, rest remain the same}> Variables: j10^0 Graph 4: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 -2 + i^0, rest remain the same}> Graph 3 undef183, rest remain the same}> undef183, rest remain the same}> Graph 4 Map Locations to Subgraph: ( 0 , 0 ) ( 3 , 1 ) ( 5 , 4 ) ( 7 , 3 ) ( 11 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.001178 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000563s Ranking function: -1 + __const_100^0 - i^0 New Graphs: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.002608 Checking conditional termination of SCC {l11}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000440s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000770s Trying to remove transition: 1 + j6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.002941s Time used: 0.002859 Trying to remove transition: 1 + j6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.002555s Time used: 0.002344 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001637s Time used: 4.00111 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006873s Time used: 4.00163 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.004858s Time used: 1.00082 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013283s Time used: 0.00594 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000987s Time used: 1.00096 LOG: SAT solveNonLinear - Elapsed time: 1.014269s Cost: 1; Total time: 1.0069 Quasi-ranking function: 50000 - j6^0 New Graphs: Transitions: 1 + j6^0, rest remain the same}> 1 + j6^0, rest remain the same}> Variables: j6^0 Checking conditional termination of SCC {l11}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000347s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001564s Trying to remove transition: 1 + j6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003743s Time used: 0.003664 Trying to remove transition: 1 + j6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003980s Time used: 0.003641 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002905s Time used: 4.00228 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.008725s Time used: 4.00252 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006317s Time used: 1.00116 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.011401s Time used: 4.0045 Termination failed. Trying to show unreachability... Proving unreachability of entry: -2 + i^0, rest remain the same}> LOG: CALL check - Post:1 <= 0 - Process 1 * Exit transition: -2 + i^0, rest remain the same}> * Postcondition : 1 <= 0 Postcodition moved up: 1 <= 0 LOG: Try proving POST Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 2 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000250s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000281s LOG: NarrowEntry size 1 Narrowing transition: 1 + i^0, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: END ENTRIES: GRAPH: 1 + i^0, rest remain the same}> END GRAPH: EXIT: -2 + i^0, rest remain the same}> POST: 1 <= 0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.002913s Time used: 0.002854 LOG: SAT solveNonLinear - Elapsed time: 0.002913s Cost: 0; Total time: 0.002854 Postcondition implied by a set of invariant(s): Invariant at l3: 0 <= i^0 LOG: Postcondition implied > Postcondition implied! LOG: RETURN check - Elapsed time: 0.014467s It is unreachable Location 11 unreachable! > It's unfeasible. Removing transition: undef183, rest remain the same}> > It's unfeasible. Removing transition: undef183, rest remain the same}> Location 7 unreachable! > It's unfeasible. Removing transition: > It's unfeasible. Removing transition: Proving termination of subgraph 4 Analyzing SCC {l5}... No cycles found. Program Terminates