NO Solver Timeout: 4 Global Timeout: 300 Maximum number of concurrent processes: 900 ******************************************************************************************* *********************** UNPROCESSED TRANSITION SYSTEMS PER FUNCTION *********************** ******************************************************************************************* List of LLVMGraphs + assumeNodes + staticAssertNodes [1] : +++++++++++++++++++++++++++++++ main +++++++++++++++++++++++++++++++ + + Init Location: 0 Transitions: 0, main_i -> 0}> (main_i + 2), main_j -> 0}> ((main_i + main_j) + 3)}> = 0))> = 0)> (((main_i + main_j) + main_k) + 4), main_l -> 0}> ((((main_i + main_j) + main_k) + main_l) + 1000)}> = 0))> = 0)> (main_m - 0)}> (main_l + 1)}> (main_k - 1)}> (main_j + 1)}> (main_i + 1)}> 0}> Fresh variables: Undef variables: Abstraction variables: Exit nodes: Accepting locations: Asserts: + Assume Nodes [0]: ++++++++++++++++++++++++++++++++++++++++++++++++ + Static Assert Nodes [0]: +++++++++++++++++++++++++++++++++++++++++ + After preprocess (paralelization): ++++++++++++++++++++++++++++++ Init Location: 0 Transitions: 0, main_i -> 0}> (main_i + 2), main_j -> 0}> ((main_i + main_j) + 3)}> = 0)> = 0))> (((main_i + main_j) + main_k) + 4), main_l -> 0}> ((((main_i + main_j) + main_k) + main_l) + 1000)}> = 0)> = 0))> (main_m - 0)}> (main_l + 1)}> (main_k - 1)}> (main_j + 1)}> (main_i + 1)}> 0}> Fresh variables: Undef variables: Abstraction variables: Exit nodes: 26, Accepting locations: Asserts: + + +++++++++++++++++++++++++++++++ main +++++++++++++++++++++++++++++++ Function Return and Parameters Information [1 functions]: function name: main [1 return + 0 parameters] demangled: main main__func_return_ [function result] : int AST Ident Scanner Information [9 idents]: __VERIFIER_nondet_int | function | [integer, ()] | main | function | [integer, ()] | i | local variable | integer | | j | local variable | integer | | k | local variable | integer | | l | local variable | integer | | m | local variable | integer | | a | local variable | integer | | b | local variable | integer | | Main function: main Preprocessed LLVMGraph Init Location: 0 Transitions: 0, main_a -> (0 + 2)}> = 0), par{main_k -> ((main_i + main_j) + 3), main_l -> 0, main_b -> (((main_i + main_j) + ((main_i + main_j) + 3)) + 4)}> = 0)), par{main_j -> (main_j + 1), main_k -> ((main_i + main_j) + 3)}> (main_i + 1), main_j -> 0, main_a -> ((main_i + 1) + 2)}> (main_i + 1)}> ((((main_i + main_j) + main_k) + main_l) + 1000)}> = 0), par{main_k -> (main_k - 1), main_l -> 0, main_b -> (((main_i + main_j) + (main_k - 1)) + 4)}> = 0)), par{main_j -> (main_j + 1), main_k -> (main_k - 1)}> = 0), par{main_m -> (main_m - 0)}> = 0)), par{main_l -> (main_l + 1)}> Fresh variables: Undef variables: Abstraction variables: Exit nodes: 26, Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: 3 + main_i + main_j, main_l -> 0, main_b -> 7 + 2*main_i + 2*main_j, rest remain the same}> 1 + main_j, main_k -> 3 + main_i + main_j, rest remain the same}> 1 + main_i, main_j -> 0, main_a -> 3 + main_i, rest remain the same}> 1000 + main_i + main_j + main_k + main_l, rest remain the same}> -1 + main_k, main_l -> 0, main_b -> 3 + main_i + main_j + main_k, rest remain the same}> 1 + main_j, main_k -> -1 + main_k, rest remain the same}> 1 + main_l, rest remain the same}> Variables: main_i, main_j, main_k, main_a, main_b, main_l, main_m Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 0, main_a -> 2, rest remain the same}> Graph 2 1 + main_i, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 5 , 1 ) ( 11 , 1 ) ( 14 , 1 ) ( 26 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.369715 Some transition disabled by a set of invariant(s): Invariant at l11: main_b <= 4 + main_i + main_j + main_k + 2*main_l Invariant at l14: 0 <= main_m Strengthening and disabling transitions... > It's unfeasible. Removing transition: 1 + main_l, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1000 + main_i + main_j + main_k + main_l, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + main_k, main_l -> 0, main_b -> 3 + main_i + main_j + main_k, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + main_j, main_k -> -1 + main_k, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): Checking unfeasibility... Time used: 0.04372 Some transition disabled by a set of invariant(s): Invariant at l5: 1 + main_i <= main_j + main_a Invariant at l11: 1 + main_l <= main_b Strengthening and disabling transitions... > It's unfeasible. Removing transition: -1 + main_k, main_l -> 0, main_b -> 3 + main_i + main_j + main_k, rest remain the same}> > It's unfeasible. Removing transition: 1 + main_j, main_k -> -1 + main_k, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 3 + main_i + main_j, main_l -> 0, main_b -> 7 + 2*main_i + 2*main_j, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + main_j, main_k -> 3 + main_i + main_j, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + main_i, main_j -> 0, main_a -> 3 + main_i, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1000 + main_i + main_j + main_k + main_l, rest remain the same}> Checking unfeasibility... Time used: 0.137675 Some transition disabled by a set of invariant(s): Invariant at l5: main_a <= 2 + main_i Invariant at l11: main_l <= 1 + main_a + main_b Invariant at l14: main_l <= 1 + main_a + main_b Strengthening and disabling transitions... > It's unfeasible. Removing transition: 1 + main_j, main_k -> 3 + main_i + main_j, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 3 + main_i + main_j, main_l -> 0, main_b -> 7 + 2*main_i + 2*main_j, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + main_i, main_j -> 0, main_a -> 3 + main_i, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1000 + main_i + main_j + main_k + main_l, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): Checking unfeasibility... Time used: 0.01886 Some transition disabled by a set of invariant(s): Invariant at l5: 1 + main_j <= main_a Invariant at l14: 1 <= main_m Strengthening and disabling transitions... > It's unfeasible. Removing transition: 1 + main_i, main_j -> 0, main_a -> 3 + main_i, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 3 + main_i + main_j, main_l -> 0, main_b -> 7 + 2*main_i + 2*main_j, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): Checking unfeasibility... Time used: 4.10048 Analyzing SCC {l5}... No cycles found. Proving termination of subgraph 4 Analyzing SCC {l11}... No cycles found. Proving termination of subgraph 5 Checking unfeasibility... Time used: 0.002251 > No variable changes in termination graph. Checking conditional unfeasibility... Calling Safety with literal 1 + main_m <= 0 and entry LOG: CALL check - Post:1 + main_m <= 0 - Process 1 * Exit transition: * Postcondition : 1 + main_m <= 0 Postcodition moved up: 1 + main_m <= 0 LOG: Try proving POST LOG: CALL check - Post:1 + main_m <= 0 - Process 2 * Exit transition: 1000 + main_i + main_j + main_k + main_l, rest remain the same}> * Postcondition : 1 + main_m <= 0 Postcodition moved up: 1001 + main_i + main_j + main_k + main_l <= 0 LOG: Try proving POST LOG: CALL check - Post:1001 + main_i + main_j + main_k + main_l <= 0 - Process 3 * Exit transition: 3 + main_i + main_j, main_l -> 0, main_b -> 7 + 2*main_i + 2*main_j, rest remain the same}> * Postcondition : 1001 + main_i + main_j + main_k + main_l <= 0 Postcodition moved up: 502 + main_i + main_j <= 0 LOG: Try proving POST LOG: CALL check - Post:502 + main_i + main_j <= 0 - Process 4 * Exit transition: 0, main_a -> 2, rest remain the same}> * Postcondition : 502 + main_i + main_j <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000193s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000223s LOG: NarrowEntry size 1 ENTRIES: 0, main_a -> 2, rest remain the same}> END ENTRIES: GRAPH: END GRAPH: EXIT: 3 + main_i + main_j, main_l -> 0, main_b -> 7 + 2*main_i + 2*main_j, rest remain the same}> POST: 1001 + main_i + main_j + main_k + main_l <= 0 LOG: Try proving POST [10755 : 10757] [10755 : 10758] LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.045509s LOG: NarrowEntry size 1 ENTRIES: 3 + main_i + main_j, main_l -> 0, main_b -> 7 + 2*main_i + 2*main_j, rest remain the same}> END ENTRIES: GRAPH: END GRAPH: EXIT: 1000 + main_i + main_j + main_k + main_l, rest remain the same}> POST: 1 + main_m <= 0 LOG: Try proving POST [10755 : 10759] [10755 : 10760] [10755 : 10761] LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 4.156772s LOG: NarrowEntry size 1 Narrowing transition: LOG: Narrow transition size 1 ENTRIES: 1000 + main_i + main_j + main_k + main_l, rest remain the same}> END ENTRIES: GRAPH: END GRAPH: EXIT: POST: 1 + main_m <= 0 LOG: Try proving POST [10755 : 10762] [10755 : 10763] [10755 : 10764] LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 8.273406s [10755 : 10925] [10755 : 10929] Successful child: 10925 Program does NOT terminate