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_x -> ¿functionCall(__VERIFIER_nondet_int), main_y -> ¿functionCall(__VERIFIER_nondet_int), main_z -> ¿functionCall(__VERIFIER_nondet_int)}> 0))> 0)> (main_x + main_y), main_y -> (main_y + main_z), main_z -> (main_z + 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}> ¿functionCall(__VERIFIER_nondet_int)}> varCall_1}> ¿functionCall(__VERIFIER_nondet_int)}> varCall_2}> ¿functionCall(__VERIFIER_nondet_int)}> varCall_3}> 0)> 0))> (main_x + main_y), main_y -> (main_y + main_z), main_z -> (main_z + 1)}> 0}> Fresh variables: Undef variables: Abstraction variables: Exit nodes: 6, Accepting locations: Asserts: + + +++++++++++++++++++++++++++++++ main +++++++++++++++++++++++++++++++ Function Return and Parameters Information [2 functions]: function name: __VERIFIER_nondet_int [1 return + 0 parameters] demangled: __VERIFIER_nondet_int __VERIFIER_nondet_int__func_return_ [function result] : int function name: main [1 return + 0 parameters] demangled: main main__func_return_ [function result] : int AST Ident Scanner Information [5 idents]: __VERIFIER_nondet_int | function | [integer, ()] | | main | function | [integer, ()] | x | local variable | integer | | y | local variable | integer | | z | local variable | integer | | Main function: main Preprocessed LLVMGraph Init Location: 0 Transitions: 0), par{main_x -> (main_x + main_y), main_y -> (main_y + main_z), main_z -> (main_z + 1)}> 0))> Fresh variables: undef4, undef5, undef6, Undef variables: undef4, undef5, undef6, Abstraction variables: Exit nodes: 6, Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ( 6 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.002241 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000570s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001352s [3884 : 3886] [3884 : 3887] Successful child: 3886 [ 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: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> New Graphs: LOG: CALL check - Post:1 + main_x <= 0 - Process 1 * Exit transition: * Postcondition : 1 + main_x <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000363s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000418s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 1 + main_x <= 0 , Narrowing transition: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000548s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001397s [3884 : 3891] [3884 : 3892] Successful child: 3891 [ 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: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, 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: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> New Graphs: LOG: CALL check - Post:main_x <= 0 - Process 2 * Exit transition: * Postcondition : main_x <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000398s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000455s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: main_x <= 0 , Narrowing transition: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000532s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001265s [3884 : 3896] [3884 : 3897] Successful child: 3896 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, 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): main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Ranking function: -main_y - main_z New Graphs: [3884 : 3901] [3884 : 3902] INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: main_x + main_y + main_z <= 0 , 0 <= main_z , Narrowing transition: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000796s Ranking function: -main_z New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000304s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001143s [3884 : 3903] [3884 : 3904] Successful child: 3903 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> New Graphs: LOG: CALL check - Post:main_x + main_y + main_z <= 0 - Process 3 * Exit transition: * Postcondition : main_x + main_y + main_z <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000228s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000283s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: main_x + main_y + main_z <= 0 , It's unfeasible. Removing transition: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Narrowing transition: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000328s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001160s [3884 : 3908] [3884 : 3909] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005213s Time used: 0.004953 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.008994s Time used: 0.008992 LOG: SAT solveNonLinear - Elapsed time: 0.014207s Cost: 1; Total time: 0.013945 Quasi-ranking function: 50000 - main_z New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000348s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001556s [3884 : 3913] [3884 : 3914] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018305s Time used: 0.017577 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.013192s Time used: 0.013189 LOG: SAT solveNonLinear - Elapsed time: 0.031497s Cost: 1; Total time: 0.030766 Quasi-ranking function: 50000 - main_y New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000539s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007360s [3884 : 3918] [3884 : 3919] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019896s Time used: 0.018974 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015352s Time used: 0.01535 LOG: SAT solveNonLinear - Elapsed time: 0.035248s Cost: 1; Total time: 0.034324 Quasi-ranking function: 50000 - main_x + main_z New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z 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.004237s [3884 : 4083] [3884 : 4084] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010099s Time used: 0.009693 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.012627s Time used: 0.012625 LOG: SAT solveNonLinear - Elapsed time: 0.022726s Cost: 1; Total time: 0.022318 Quasi-ranking function: 50000 - main_x New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000440s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002824s [3884 : 4088] [3884 : 4089] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006163s Time used: 0.005821 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.008516s Time used: 0.008514 LOG: SAT solveNonLinear - Elapsed time: 0.014679s Cost: 1; Total time: 0.014335 Quasi-ranking function: 50000 - main_x - main_y + main_z New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000472s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010582s [3884 : 4093] [3884 : 4094] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005530s Time used: 0.005188 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015040s Time used: 0.015038 LOG: SAT solveNonLinear - Elapsed time: 0.020570s Cost: 1; Total time: 0.020226 Quasi-ranking function: 50000 - main_x - main_y - main_z New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000480s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010123s [3884 : 4098] [3884 : 4099] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019674s Time used: 0.018538 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015345s Time used: 0.015343 LOG: SAT solveNonLinear - Elapsed time: 0.035018s Cost: 1; Total time: 0.033881 Quasi-ranking function: 50000 - main_x - main_z New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000694s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004544s [3884 : 4103] [3884 : 4104] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007212s Time used: 0.006848 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010494s Time used: 0.010493 LOG: SAT solveNonLinear - Elapsed time: 0.017706s Cost: 1; Total time: 0.017341 Quasi-ranking function: 50000 - main_y - main_z New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000554s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006027s [3884 : 4108] [3884 : 4109] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022834s Time used: 0.021716 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.014562s Time used: 0.01456 LOG: SAT solveNonLinear - Elapsed time: 0.037396s Cost: 1; Total time: 0.036276 Quasi-ranking function: 50000 - main_y + main_z New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000596s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.020162s [3884 : 4113] [3884 : 4114] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006914s Time used: 0.006506 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.008844s Time used: 0.008842 LOG: SAT solveNonLinear - Elapsed time: 0.015757s Cost: 1; Total time: 0.015348 Quasi-ranking function: 50000 - main_x + main_y + main_z New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000644s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011752s [3884 : 4118] [3884 : 4119] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025067s Time used: 0.023769 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.014978s Time used: 0.014976 LOG: SAT solveNonLinear - Elapsed time: 0.040045s Cost: 1; Total time: 0.038745 Quasi-ranking function: 50000 - main_x + main_y - main_z New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000809s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018349s [3884 : 4123] [3884 : 4124] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008555s Time used: 0.008125 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.012234s Time used: 0.012233 LOG: SAT solveNonLinear - Elapsed time: 0.020790s Cost: 1; Total time: 0.020358 Quasi-ranking function: 50000 - main_x + main_y New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000723s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.024053s [3884 : 4128] [3884 : 4129] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008691s Time used: 0.008251 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009833s Time used: 0.009832 LOG: SAT solveNonLinear - Elapsed time: 0.018524s Cost: 1; Total time: 0.018083 Quasi-ranking function: 50000 - main_x - main_y New Graphs: Transitions: main_x + main_y, main_y -> main_y + main_z, main_z -> 1 + main_z, rest remain the same}> Variables: main_x, main_y, main_z Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000795s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.016249s [3884 : 4133] [3884 : 4134] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007045s Time used: 0.006663 [3884 : 4138] [3884 : 4142] Successful child: 4138 Program does NOT terminate