WARNING: Excluded non-linear constraints:[B*B*B>=0,0>=B*B*B] WARNING: Excluded non-linear constraints:[B*B*B>=1,B*B*B>=2*O,1+2*O>=B*B*B] WARNING: Excluded non-linear constraints:[0>=B*B*B+1,2*O>=B*B*B,1+B*B*B>=2*O] WARNING: Excluded non-linear constraints:[B*B*B>=0,0>=B*B*B] WARNING: Excluded non-linear constraints:[B*B*B>=1,B*B*B>=2*F,1+2*F>=B*B*B] WARNING: Excluded non-linear constraints:[0>=B*B*B+1,2*F>=B*B*B,1+B*B*B>=2*F] warning: Ignored call to evalfstop/4 in equation evalfreturnin/4 Inferred cost of evalfbb3in(A,B,C,D,E,F,G,H,I): evalfbb3in(A,B,C,D,E,F,G,H,I):[26]: 1 with precondition: [D=0,E=0,I=0,F=A,B=G,C=H,0>=C,B>=C+1] evalfbb3in(A,B,C,D,E,F,G,H,I):[[25],26]: 1+it1*(2) Such that:it1=<1*C,it1=<1*H,it1=<1*I,it1=<1*B+ -1,it1=<1*G+ -1,it1=<1*I+ -1*D,it1=<1*B+ -1*D+ -1,it1=<1*G+ -1*D+ -1 with precondition: [E=0,I=C,A=F,B=G,I=H,D>=0,I>=D+1,B>=I+1] Inferred cost of evalfbb5in(A,B,C,D,E,F,G,H,I): evalfbb5in(A,B,C,D,E,F,G,H,I):[30]: 1 with precondition: [C=0,E=0,H=0,F=A,I=D,B=G,0>=B] evalfbb5in(A,B,C,D,E,F,G,H,I):[[28],[29],30]: 1+it1*(3+it2*(2))+it3*(3) Such that:it1=<1*I,it1=<1*B+ -1,it1=<1*G+ -1,it1=<1*H+ -1,it3=<1,it3=<1*B,it3=<1*G,it3=<1*H,it3=<1*I+1 it2=<1*B+ -1 with precondition: [C=0,E=0,A=F,B=G,B=H,B=I+1,B>=2] evalfbb5in(A,B,C,D,E,F,G,H,I):[[28],30]: 1+it1*(3) Such that:it1=<1 with precondition: [B=1,C=0,E=0,G=1,H=1,I=0,A=F] Inferred cost of evalfbb7in(A,B,C,D,E,F,G,H,I): evalfbb7in(A,B,C,D,E,F,G,H,I):[41]: 1 with precondition: [A=0,E=0,F=0,G=B,H=C,I=D] evalfbb7in(A,B,C,D,E,F,G,H,I):[42]: 0 with precondition: [A=0,E=1,F=0,G=B,H=C,I=D] evalfbb7in(A,B,C,D,E,F,G,H,I):[43]: 1 with precondition: [A=0,E=0,F=0,G=B,H=C,I=D] evalfbb7in(A,B,C,D,E,F,G,H,I):[44]: 1 with precondition: [A=0,E=0,F=0,G=B,H=C,I=D] evalfbb7in(A,B,C,D,E,F,G,H,I):[[32,35,38],41]: inf with precondition: [E=0,H=0,B=G,D=I,0>=B,A>=0,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[32,35,38],42]: inf with precondition: [E=1,H=0,B=G,D=I,0>=B,A>=0,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[32,35,38],43]: inf with precondition: [E=0,H=0,B=G,D=I,0>=B,A>=0,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[32,35,38],44]: inf with precondition: [E=0,H=0,B=G,D=I,0>=B,A>=0,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[32,35,38],45]...: inf with precondition: [0>=B,1>=E,A>=0,E>=0] evalfbb7in(A,B,C,D,E,F,G,H,I):[[33,36,39],41]: inf with precondition: [E=0,B=G,B=H,B=I+1,A>=0,B>=2,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[33,36,39],42]: inf with precondition: [E=1,B=G,B=H,B=I+1,A>=0,B>=2,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[33,36,39],43]: inf with precondition: [E=0,B=G,B=H,B=I+1,A>=0,B>=2,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[33,36,39],44]: inf with precondition: [E=0,B=G,B=H,B=I+1,A>=0,B>=2,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[33,36,39],45]...: inf with precondition: [1>=E,A>=0,B>=2,E>=0] evalfbb7in(A,B,C,D,E,F,G,H,I):[[34,37,40],41]: inf with precondition: [B=1,E=0,G=1,H=1,I=0,A>=0,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[34,37,40],42]: inf with precondition: [B=1,E=1,G=1,H=1,I=0,A>=0,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[34,37,40],43]: inf with precondition: [B=1,E=0,G=1,H=1,I=0,A>=0,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[34,37,40],44]: inf with precondition: [B=1,E=0,G=1,H=1,I=0,A>=0,F>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I):[[34,37,40],45]...: inf with precondition: [B=1,1>=E,A>=0,E>=0] Inferred cost of evalfreturnin(A,B,C,D): evalfreturnin(A,B,C,D):[46]: 1 with precondition: [] Inferred cost of loop_cont_evalfbb7in(A,B,C,D): loop_cont_evalfbb7in(A,B,C,D):[48]: 1 with precondition: [] Inferred cost of evalfentryin(A,B,C,D): evalfentryin(A,B,C,D):[50]: 3 with precondition: [] evalfentryin(A,B,C,D):[51]: 3 with precondition: [] evalfentryin(A,B,C,D):[52]: 3 with precondition: [] evalfentryin(A,B,C,D):[53]: inf with precondition: [0>=B] evalfentryin(A,B,C,D):[54]: inf with precondition: [0>=B] evalfentryin(A,B,C,D):[55]: inf with precondition: [0>=B] evalfentryin(A,B,C,D):[56]: inf with precondition: [B>=2] evalfentryin(A,B,C,D):[57]: inf with precondition: [B>=2] evalfentryin(A,B,C,D):[58]: inf with precondition: [B>=2] evalfentryin(A,B,C,D):[59]: inf with precondition: [B=1] evalfentryin(A,B,C,D):[60]: inf with precondition: [B=1] evalfentryin(A,B,C,D):[61]: inf with precondition: [B=1] evalfentryin(A,B,C,D):[62]: 1 with precondition: [] evalfentryin(A,B,C,D):[63]: inf with precondition: [0>=B] evalfentryin(A,B,C,D):[64]: inf with precondition: [B>=2] evalfentryin(A,B,C,D):[65]: inf with precondition: [B=1] evalfentryin(A,B,C,D):[66]...: inf with precondition: [0>=B] evalfentryin(A,B,C,D):[67]...: inf with precondition: [B>=2] evalfentryin(A,B,C,D):[68]...: inf with precondition: [B=1] evalfentryin(A,B,C,D):[69]...: inf with precondition: [0>=B] evalfentryin(A,B,C,D):[70]...: inf with precondition: [B>=2] evalfentryin(A,B,C,D):[71]...: inf with precondition: [B=1] Inferred cost of evalfstart(A,B,C,D): evalfstart(A,B,C,D):[73]: 4 with precondition: [] evalfstart(A,B,C,D):[74]: 4 with precondition: [] evalfstart(A,B,C,D):[75]: 4 with precondition: [] evalfstart(A,B,C,D):[76]: inf with precondition: [0>=B] evalfstart(A,B,C,D):[77]: inf with precondition: [0>=B] evalfstart(A,B,C,D):[78]: inf with precondition: [0>=B] evalfstart(A,B,C,D):[79]: inf with precondition: [B>=2] evalfstart(A,B,C,D):[80]: inf with precondition: [B>=2] evalfstart(A,B,C,D):[81]: inf with precondition: [B>=2] evalfstart(A,B,C,D):[82]: inf with precondition: [B=1] evalfstart(A,B,C,D):[83]: inf with precondition: [B=1] evalfstart(A,B,C,D):[84]: inf with precondition: [B=1] evalfstart(A,B,C,D):[85]: 2 with precondition: [] evalfstart(A,B,C,D):[86]: inf with precondition: [0>=B] evalfstart(A,B,C,D):[87]: inf with precondition: [B>=2] evalfstart(A,B,C,D):[88]: inf with precondition: [B=1] evalfstart(A,B,C,D):[89]...: inf with precondition: [0>=B] evalfstart(A,B,C,D):[90]...: inf with precondition: [B>=2] evalfstart(A,B,C,D):[91]...: inf with precondition: [B=1] evalfstart(A,B,C,D):[92]...: inf with precondition: [0>=B] evalfstart(A,B,C,D):[93]...: inf with precondition: [B>=2] evalfstart(A,B,C,D):[94]...: inf with precondition: [B=1] Solved cost expressions of evalfstart(A,B,C,D): evalfstart(A,B,C,D):[73]: 4 with precondition: [] evalfstart(A,B,C,D):[74]: 4 with precondition: [] evalfstart(A,B,C,D):[75]: 4 with precondition: [] evalfstart(A,B,C,D):[76]: inf with precondition: [0>=B] evalfstart(A,B,C,D):[77]: inf with precondition: [0>=B] evalfstart(A,B,C,D):[78]: inf with precondition: [0>=B] evalfstart(A,B,C,D):[79]: inf with precondition: [B>=2] evalfstart(A,B,C,D):[80]: inf with precondition: [B>=2] evalfstart(A,B,C,D):[81]: inf with precondition: [B>=2] evalfstart(A,B,C,D):[82]: inf with precondition: [B=1] evalfstart(A,B,C,D):[83]: inf with precondition: [B=1] evalfstart(A,B,C,D):[84]: inf with precondition: [B=1] evalfstart(A,B,C,D):[85]: 2 with precondition: [] evalfstart(A,B,C,D):[86]: inf with precondition: [0>=B] evalfstart(A,B,C,D):[87]: inf with precondition: [B>=2] evalfstart(A,B,C,D):[88]: inf with precondition: [B=1] evalfstart(A,B,C,D):[89]...: inf with precondition: [0>=B] evalfstart(A,B,C,D):[90]...: inf with precondition: [B>=2] evalfstart(A,B,C,D):[91]...: inf with precondition: [B=1] evalfstart(A,B,C,D):[92]...: inf with precondition: [0>=B] evalfstart(A,B,C,D):[93]...: inf with precondition: [B>=2] evalfstart(A,B,C,D):[94]...: inf with precondition: [B=1] Maximum cost of evalfstart(A,B,C,D): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 25 ms. Invariants computed in 148 ms. ----Backward Invariants 87 ms. ----Transitive Invariants 11 ms. Refinement performed in 109 ms. Termination proved in 29 ms. Upper bounds computed in 232 ms. ----Phase cost structures 85 ms. --------Equation cost structures 67 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 136 ms. ----Solving cost expressions 0 ms. Compressed phase information: 21 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 577 ms.