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)}> (main_x + main_z), main_z -> (~(2) * main_y), main_y -> (main_y + 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}> (main_x + main_z), main_z -> (~(2) * main_y), main_y -> (main_y + 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: (main_x + main_z), main_y -> (main_y + 1), main_z -> (~(2) * main_y)}> 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.00131 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000424s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001002s [6967 : 6969] [6967 : 6970] Successful child: 6969 [ 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> New Graphs: LOG: CALL check - Post:1 <= main_x - Process 1 * Exit transition: * Postcondition : 1 <= main_x LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000270s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000311s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 1 <= main_x , Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000393s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001012s [6967 : 6974] [6967 : 6975] Successful child: 6974 [ 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> New Graphs: LOG: CALL check - Post:0 <= main_x - Process 2 * Exit transition: * Postcondition : 0 <= main_x LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000355s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000403s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 0 <= main_x , Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000459s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001160s [6967 : 6979] [6967 : 6980] Successful child: 6979 [ 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> Ranking function: -main_x New Graphs: [6967 : 6984] [6967 : 6985] INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 0 <= main_x + main_z , main_y <= 1 + main_x , Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000750s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004909s Piecewise ranking function: min(2,1 - main_x) New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000352s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001171s [6967 : 6986] [6967 : 6987] Successful child: 6986 [ 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> Ranking function: -main_y New Graphs: [6967 : 6991] [6967 : 6992] INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 2*main_y <= 2*main_x + main_z , Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000760s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.012538s Piecewise ranking function: min(1,-main_x) New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000369s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001283s [6967 : 6993] [6967 : 6994] Successful child: 6993 [ 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> Ranking function: 2 - main_y New Graphs: [6967 : 6998] [6967 : 6999] [6967 : 7000] INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 1 + main_x <= 0 , 1 <= main_z , main_y <= 1 + main_x , Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 3 invGraph after Narrowing: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001357s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.156545s Piecewise ranking function: min((1 / 2),(~(1) / 2) - main_x) New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000750s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008008s [6967 : 7001] [6967 : 7002] Successful child: 7001 [ 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> Ranking function: main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000605s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002763s [6967 : 7006] [6967 : 7007] Successful child: 7006 [ 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> New Graphs: [6967 : 7011] [6967 : 7012] INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 1 <= 2*main_y + main_z , [6967 : 7013] [6967 : 7014] [6967 : 7015] INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 2*main_y <= 1 + main_x , Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.003604s Ranking function: 2 - 7*main_y New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001877s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.306463s Piecewise ranking function: min(2,-4 - 12*main_x) New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001297s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.044840s [6967 : 7016] [6967 : 7017] Successful child: 7017 Ranking function: -2*main_y - main_z Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001381s Ranking function: main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000497s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002586s [6967 : 7021] [6967 : 7022] Successful child: 7021 [ 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> New Graphs: [6967 : 7026] [6967 : 7027] [6967 : 7028] [6967 : 7029] [6967 : 7030] [6967 : 7031] [6967 : 7032] INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 0 <= main_x + main_z , 2*main_y + main_z <= 2 , Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.003293s Ranking function: 2 - 7*main_y New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001886s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.339981s Piecewise ranking function: min(0,-1 - 3*main_x) New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001296s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.044754s [6967 : 7033] [6967 : 7034] Successful child: 7034 Ranking function: -2*main_y - main_z Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001394s Ranking function: main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000491s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002564s [6967 : 7038] [6967 : 7039] Successful child: 7038 [ 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> New Graphs: [6967 : 7178] [6967 : 7179] [6967 : 7180] [6967 : 7181] [6967 : 7182] [6967 : 7183] INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: 2*main_y + main_z <= 2 , 1 + main_y <= main_x + main_z , Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.005064s Ranking function: 7 - 14*main_y New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.003632s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.474824s Piecewise ranking function: min(0,-1 - 8*main_x) New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.002606s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.164432s [6967 : 7208] [6967 : 7209] Successful child: 7209 Ranking function: -2*main_y - main_z Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.002424s Ranking function: -1 + main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, rest remain the same}> main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001094s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011358s [6967 : 7213] [6967 : 7214] Successful child: 7214 Ranking function: 2*main_y + main_z Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000630s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003537s [6967 : 7218] [6967 : 7219] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025822s Time used: 0.025248 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.046328s Time used: 0.046326 LOG: SAT solveNonLinear - Elapsed time: 0.072150s Cost: 1; Total time: 0.071574 Quasi-ranking function: 50000 + main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000653s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009550s [6967 : 7223] [6967 : 7224] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024503s Time used: 0.023794 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.044080s Time used: 0.044078 LOG: SAT solveNonLinear - Elapsed time: 0.068583s Cost: 1; Total time: 0.067872 Quasi-ranking function: 50000 + main_x + main_y + main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000725s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007451s [6967 : 7228] [6967 : 7229] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.027971s Time used: 0.027191 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.041888s Time used: 0.041886 LOG: SAT solveNonLinear - Elapsed time: 0.069858s Cost: 1; Total time: 0.069077 Quasi-ranking function: 50000 + main_x - main_y + main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.000742s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.034088s [6967 : 7233] [6967 : 7234] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.046035s Time used: 0.044511 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.038448s Time used: 0.038445 LOG: SAT solveNonLinear - Elapsed time: 0.084483s Cost: 1; Total time: 0.082956 Quasi-ranking function: 50000 + 2*main_x + main_y - 25000*main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001508s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.063369s [6967 : 7238] [6967 : 7239] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.028756s Time used: 0.027749 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.037159s Time used: 0.037157 LOG: SAT solveNonLinear - Elapsed time: 0.065915s Cost: 1; Total time: 0.064906 Quasi-ranking function: 50000 + main_y + 2*main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001213s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.076438s [6967 : 7243] [6967 : 7244] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.049832s Time used: 0.047881 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.048809s Time used: 0.048806 LOG: SAT solveNonLinear - Elapsed time: 0.098641s Cost: 1; Total time: 0.096687 Quasi-ranking function: 50000 - main_y + main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001314s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.051266s [6967 : 7248] [6967 : 7249] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.031573s Time used: 0.03034 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.049455s Time used: 0.049453 LOG: SAT solveNonLinear - Elapsed time: 0.081028s Cost: 1; Total time: 0.079793 Quasi-ranking function: 50000 + main_x + main_y New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001408s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.069464s [6967 : 7253] [6967 : 7254] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.032357s Time used: 0.030925 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.048235s Time used: 0.048232 LOG: SAT solveNonLinear - Elapsed time: 0.080592s Cost: 1; Total time: 0.079157 Quasi-ranking function: 50000 + main_x - main_y - 16668*main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001481s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.114640s [6967 : 7260] [6967 : 7261] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.035766s Time used: 0.034487 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.043283s Time used: 0.043281 LOG: SAT solveNonLinear - Elapsed time: 0.079050s Cost: 1; Total time: 0.077768 Quasi-ranking function: 50000 - 3*main_y - main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001669s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.055887s [6967 : 7265] [6967 : 7266] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.031475s Time used: 0.02994 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.039026s Time used: 0.039024 LOG: SAT solveNonLinear - Elapsed time: 0.070501s Cost: 1; Total time: 0.068964 Quasi-ranking function: 50000 + main_x - main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001753s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.020166s [6967 : 7270] [6967 : 7271] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.055307s Time used: 0.051373 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.042666s Time used: 0.042663 LOG: SAT solveNonLinear - Elapsed time: 0.097973s Cost: 1; Total time: 0.094036 Quasi-ranking function: 50000 - main_y New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001559s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.059476s [6967 : 7275] [6967 : 7276] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.035723s Time used: 0.033921 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.042529s Time used: 0.042527 LOG: SAT solveNonLinear - Elapsed time: 0.078252s Cost: 1; Total time: 0.076448 Quasi-ranking function: 50000 + main_x + main_z New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.003817s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.084049s [6967 : 7280] [6967 : 7281] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.033771s Time used: 0.03181 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.034937s Time used: 0.034934 LOG: SAT solveNonLinear - Elapsed time: 0.068707s Cost: 1; Total time: 0.066744 Quasi-ranking function: 50000 + main_x New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.003590s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.091176s [6967 : 7285] [6967 : 7286] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.033116s Time used: 0.031154 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.049195s Time used: 0.049036 LOG: SAT solveNonLinear - Elapsed time: 0.082310s Cost: 1; Total time: 0.08019 Quasi-ranking function: 50000 + main_x - main_y New Graphs: Transitions: main_x + main_z, main_y -> 1 + main_y, main_z -> -2*main_y, 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.001173s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.050890s [6967 : 7449] [6967 : 7450] Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.034002s Time used: 0.032299 [6967 : 7454] [6967 : 7458] Successful child: 7454 Program does NOT terminate