[runlim] version: 1.7 [runlim] time limit: 3600 seconds [runlim] real time limit: 311040000 seconds [runlim] space limit: 4294967069 MB [runlim] argv[0]: /home/zhouyan/BACH/armc [runlim] argv[1]: live [runlim] argv[2]: /home/zhouyan/BACH/tmpFile20141130190959.armc [runlim] argv[3]: -straight [runlim] start: Sun Nov 30 19:22:30 2014 [runlim] main pid: 1440 ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008) rybal@mpi-sws.mpg.de cmd line: [live,/home/zhouyan/BACH/tmpFile20141130190959.armc,-straight] reading input from /home/zhouyan/BACH/tmpFile20141130190959.armc...done. creating straight line code between cutpoints...done. meta_transition(p(pc(v3),data(_,A,_)), p(pc(v4),data(B,C,D)), [], [C=A,B=0.0,A=5,A>=5,D>0,B=<2], [11]). meta_transition(p(pc(v1),data(A,B,_)), p(pc(v5),data(C,D,E)), [], [D=B,C=A,B=0,B=<10,E>0], [10]). meta_transition(p(pc(v4),data(A,B,_)), p(pc(v1),data(C,D,E)), [], [D=B,C=A,B>=0,A=2,A=<2,E>0,D=<10], [9]). meta_transition(p(pc(v2),data(A,B,_)), p(pc(v3),data(C,D,E)), [], [D=B,C=A,A=2,A=<2,E>0,D>=5], [8]). meta_transition(p(pc(v1),data(_,A,_)), p(pc(v2),data(B,C,D)), [], [C=A,B=0.0,A=10,A=<10,D>0,B=<2], [7]). meta_transition(p(pc(v5),data(A,B,C)), p(pc(v5),data(D,E,F)), [], [E=B,D=A,F>0,C>0], [5]). meta_transition(p(pc(v4),data(A,B,C)), p(pc(v4),data(D,E,F)), [], [E=B-4*C,D=A+C,F>0,C>0,D=<2,A=<2], [4]). meta_transition(p(pc(v3),data(A,B,C)), p(pc(v3),data(D,E,F)), [], [E=B-2*C,D=A+C,F>0,C>0,E>=5,B>=5], [3]). meta_transition(p(pc(v2),data(A,B,C)), p(pc(v2),data(D,E,F)), [], [E=B+C,D=A+C,F>0,C>0,D=<2,A=<2], [2]). meta_transition(p(pc(v1),data(A,B,C)), p(pc(v1),data(D,E,F)), [], [E=B+C,D=A+C,F>0,C>0,E=<10,B=<10], [1]). meta_transition(p(pc(v0),data(_,_,_)), p(pc(v1),data(A,B,C)), [], [B=1.0,A=0.0,C>0,B=<10], [6]). transition(p(pc(v3),data(_,A,_)), p(pc(v4),data(B,C,D)), {C=A,B=0.0,A=5,A>=5,D>0,B=<2}, [], [C=A,B=0.0,A=5,A>=5,D>0,B=<2], tid([11])). transition(p(pc(v1),data(A,B,_)), p(pc(v5),data(C,D,E)), {D=B,C=A,B=0,B=<10,E>0}, [], [D=B,C=A,B=0,B=<10,E>0], tid([10])). transition(p(pc(v4),data(A,B,_)), p(pc(v1),data(C,D,E)), {D=B,C=A,B>=0,A=2,A=<2,E>0,D=<10}, [], [D=B,C=A,B>=0,A=2,A=<2,E>0,D=<10], tid([9])). transition(p(pc(v2),data(A,B,_)), p(pc(v3),data(C,D,E)), {D=B,C=A,A=2,A=<2,E>0,D>=5}, [], [D=B,C=A,A=2,A=<2,E>0,D>=5], tid([8])). transition(p(pc(v1),data(_,A,_)), p(pc(v2),data(B,C,D)), {C=A,B=0.0,A=10,A=<10,D>0,B=<2}, [], [C=A,B=0.0,A=10,A=<10,D>0,B=<2], tid([7])). transition(p(pc(v5),data(A,B,C)), p(pc(v5),data(D,E,F)), {E=B,D=A,F>0,C>0}, [], [E=B,D=A,F>0,C>0], tid([5])). transition(p(pc(v4),data(A,B,C)), p(pc(v4),data(D,E,F)), {E=B-4*C,D=A+C,F>0,C>0,D=<2,A=<2}, [], [E=B-4*C,D=A+C,F>0,C>0,D=<2,A=<2], tid([4])). transition(p(pc(v3),data(A,B,C)), p(pc(v3),data(D,E,F)), {E=B-2*C,D=A+C,F>0,C>0,E>=5,B>=5}, [], [E=B-2*C,D=A+C,F>0,C>0,E>=5,B>=5], tid([3])). transition(p(pc(v2),data(A,B,C)), p(pc(v2),data(D,E,F)), {E=B+C,D=A+C,F>0,C>0,D=<2,A=<2}, [], [E=B+C,D=A+C,F>0,C>0,D=<2,A=<2], tid([2])). transition(p(pc(v1),data(A,B,C)), p(pc(v1),data(D,E,F)), {E=B+C,D=A+C,F>0,C>0,E=<10,B=<10}, [], [E=B+C,D=A+C,F>0,C>0,E=<10,B=<10], tid([1])). transition(p(pc(v0),data(_,_,_)), p(pc(v1),data(A,B,C)), {B=1.0,A=0.0,C>0,B=<10}, [], [B=1.0,A=0.0,C>0,B=<10], tid([6])). tid([11]): pc(v3) pc(v4) {y'=y,x'=0.0,y=5,y>=5,t'>0,x'=<2} [] [y'=y,x'=0.0,y=5,y>=5,t'>0,x'=<2] tid([10]): pc(v1) pc(v5) {y'=y,x'=x,y=0,y=<10,t'>0} [] [y'=y,x'=x,y=0,y=<10,t'>0] tid([9]): pc(v4) pc(v1) {y'=y,x'=x,y>=0,x=2,x=<2,t'>0,y'=<10} [] [y'=y,x'=x,y>=0,x=2,x=<2,t'>0,y'=<10] tid([8]): pc(v2) pc(v3) {y'=y,x'=x,x=2,x=<2,t'>0,y'>=5} [] [y'=y,x'=x,x=2,x=<2,t'>0,y'>=5] tid([7]): pc(v1) pc(v2) {y'=y,x'=0.0,y=10,y=<10,t'>0,x'=<2} [] [y'=y,x'=0.0,y=10,y=<10,t'>0,x'=<2] tid([5]): pc(v5) pc(v5) {y'=y,x'=x,t'>0,t>0} [] [y'=y,x'=x,t'>0,t>0] tid([4]): pc(v4) pc(v4) {y'=y-4*t,x'=x+t,t'>0,t>0,x'=<2,x=<2} [] [y'=y-4*t,x'=x+t,t'>0,t>0,x'=<2,x=<2] tid([3]): pc(v3) pc(v3) {y'=y-2*t,x'=x+t,t'>0,t>0,y'>=5,y>=5} [] [y'=y-2*t,x'=x+t,t'>0,t>0,y'>=5,y>=5] tid([2]): pc(v2) pc(v2) {y'=y+t,x'=x+t,t'>0,t>0,x'=<2,x=<2} [] [y'=y+t,x'=x+t,t'>0,t>0,x'=<2,x=<2] tid([1]): pc(v1) pc(v1) {y'=y+t,x'=x+t,t'>0,t>0,y'=<10,y=<10} [] [y'=y+t,x'=x+t,t'>0,t>0,y'=<10,y=<10] tid([6]): pc(v0) pc(v1) {y'=1.0,x'=0.0,t'>0,y'=<10} [] [y'=1.0,x'=0.0,t'>0,y'=<10] -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 abstract counterexample: stem [0,tid([6])], loop [tid([1])] trans preds: _9086->_9089: #0: y+t>=11 y+t-y'-t'>=0 refining loop cutting step 1 at pc(v1) LI at pc(v1): y+t-y'-t'<0 refining stem cutting step 2 at pc(v1) unsat suffix not yet reached cutting step 1 at pc(v1) LI at pc(v1): _8373+_8374-y'-t'<0 refining loop cutting step 1 at pc(v1) LI at pc(v1): y+t=<10 refining stem cutting step 2 at pc(v1) unsat suffix not yet reached cutting step 1 at pc(v1) LI at pc(v1): _8373+_8374=<10 -------------------------------------------------- abstraction refinement iteration 1: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([6]),tid([10])], loop [tid([5])] trans preds: _101638->_101641: #2: y+t=<10, y+t-y'-t'<0 projected loop infeasible: 1=1 1=1 refining stem cutting step 1 at pc(v1) LI at pc(v1): y'>=1 refining stem cutting step 1 at pc(v1) LI at pc(v1): y'>=1 -------------------------------------------------- abstraction refinement iteration 2: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([6]),tid([7])], loop [tid([2])] trans preds: _126007->_126010: #3: y'>=1, y+t=<10, y+t-y'-t'<0 x+t>=3 x+t-x'-t'>=0 refining stem cutting step 1 at pc(v1) LI at pc(v1): y'=<1 refining stem cutting step 1 at pc(v1) LI at pc(v1): y'=<1 -------------------------------------------------- abstraction refinement iteration 3: lfp iteration 0 1 2 3 abstract counterexample: stem [0,tid([6]),tid([1]),tid([7])], loop [tid([2])] trans preds: _176032->_176035: #4: y'=<1, y'>=1, y+t=<10, y+t-y'-t'<0 x+t>=3 x+t-x'-t'>=0 refining loop cutting step 1 at pc(v2) LI at pc(v2): x+t-x'-t'<0 refining stem cutting step 4 at pc(v1) unsat suffix not yet reached cutting step 3 at pc(v1) unsat suffix not yet reached cutting step 2 at pc(v2) unsat suffix not yet reached cutting step 1 at pc(v2) LI at pc(v2): _174992+_174994-x'-t'<0 refining loop cutting step 1 at pc(v2) LI at pc(v2): x+t=<2 refining stem cutting step 4 at pc(v1) unsat suffix not yet reached cutting step 3 at pc(v1) unsat suffix not yet reached cutting step 2 at pc(v2) unsat suffix not yet reached cutting step 1 at pc(v2) LI at pc(v2): _3332+_3334=<2 -------------------------------------------------- abstraction refinement iteration 4: lfp iteration 0 1 2 3 4 abstract counterexample: stem [0,tid([6]),tid([1]),tid([7]),tid([8])], loop [tid([3])] trans preds: _41841->_41844: #6: x+t=<2, x+t-x'-t'<0, y'=<1, y'>=1, y+t=<10, y+t-y'-t'<0 y=<4 y-y'=<0 refining stem cutting step 3 at pc(v1) unsat suffix not yet reached cutting step 2 at pc(v1) unsat suffix not yet reached cutting step 1 at pc(v2) LI at pc(v2): x'=<0 refining stem cutting step 3 at pc(v1) unsat suffix not yet reached cutting step 2 at pc(v1) unsat suffix not yet reached cutting step 1 at pc(v2) LI at pc(v2): x'=<0 -------------------------------------------------- abstraction refinement iteration 5: lfp iteration 0 1 2 3 4 5 abstract counterexample: stem [0,tid([6]),tid([1]),tid([7]),tid([2]),tid([8])], loop [tid([3])] trans preds: _130647->_130650: #7: x'=<0, x+t=<2, x+t-x'-t'<0, y'=<1, y'>=1, y+t=<10, y+t-y'-t'<0 y=<4 y-y'=<0 refining loop cutting step 1 at pc(v3) LI at pc(v3): y-y'>0 refining stem cutting step 6 at pc(v1) unsat suffix not yet reached cutting step 5 at pc(v1) unsat suffix not yet reached cutting step 4 at pc(v2) unsat suffix not yet reached cutting step 3 at pc(v2) unsat suffix not yet reached cutting step 2 at pc(v3) unsat suffix not yet reached cutting step 1 at pc(v3) LI at pc(v3): _129285-y'>0 refining loop cutting step 1 at pc(v3) LI at pc(v3): y>=12 refining stem cutting step 6 at pc(v1) unsat suffix not yet reached cutting step 5 at pc(v1) unsat suffix not yet reached cutting step 4 at pc(v2) unsat suffix not yet reached cutting step 3 at pc(v2) unsat suffix not yet reached cutting step 2 at pc(v3) unsat suffix not yet reached cutting step 1 at pc(v3) LI at pc(v3): _19833>=12 -------------------------------------------------- abstraction refinement iteration 6: lfp iteration 0 1 2 3 4 5 6 7 abstract counterexample: stem [0,tid([6]),tid([1])], loop [tid([7]),tid([2]),tid([8]),tid([11]),tid([4]),tid([9])] trans preds: _111692->_111695: #9: y>=12, y-y'>0, x'=<0, x+t=<2, x+t-x'-t'<0, y'=<1, y'>=1, y+t=<10, y+t-y'-t'<0 loop infeasible: 1=1 1=1 refining loop cutting step 3 at pc(v2) LI at pc(v2): y'>=10 cutting step 2 at pc(v2) LI at pc(v2): x'-1/6*y'=<0 cutting step 1 at pc(v3) LI at pc(v3): y'>=12 refining stem cutting step 5 at pc(v1) unsat suffix not yet reached cutting step 4 at pc(v1) unsat suffix not yet reached cutting step 3 at pc(v2) LI at pc(v2): y'>=10 cutting step 2 at pc(v2) LI at pc(v2): x'-1/6*y'=<0 cutting step 1 at pc(v3) LI at pc(v3): y'>=12 refining loop cutting step 3 at pc(v2) LI at pc(v2): y'>=10 cutting step 2 at pc(v2) LI at pc(v2): x'-1/6*y'=<0 cutting step 1 at pc(v3) LI at pc(v3): y'>=12 refining stem cutting step 5 at pc(v1) unsat suffix not yet reached cutting step 4 at pc(v1) unsat suffix not yet reached cutting step 3 at pc(v2) LI at pc(v2): y'>=10 cutting step 2 at pc(v2) LI at pc(v2): x'-1/6*y'=<0 cutting step 1 at pc(v3) LI at pc(v3): y'>=12 -------------------------------------------------- abstraction refinement iteration 7: lfp iteration 0 1 2 3 4 5 6 7 8 abstract counterexample: stem [0,tid([6]),tid([1])], loop [tid([7]),tid([2]),tid([8]),tid([3]),tid([11]),tid([4]),tid([9])] trans preds: _214483->_214486: #12: y'>=12, x'-1/6*y'=<0, y'>=10, y>=12, y-y'>0, x'=<0, x+t=<2, x+t-x'-t'<0, y'=<1, y'>=1, y+t=<10, y+t-y'-t'<0 loop infeasible: 1=1 1=1 refining loop cutting step 6 at pc(v2) unsat suffix not yet reached cutting step 5 at pc(v2) unsat suffix not yet reached cutting step 4 at pc(v3) unsat suffix not yet reached cutting step 3 at pc(v3) unsat suffix not yet reached cutting step 2 at pc(v4) LI at pc(v4): x'+1/4*y'=<5/4 cutting step 1 at pc(v4) LI at pc(v4): x'+1/4*y'=<5/4 refining stem cutting step 8 at pc(v1) unsat suffix not yet reached cutting step 7 at pc(v1) unsat suffix not yet reached cutting step 6 at pc(v2) unsat suffix not yet reached cutting step 5 at pc(v2) unsat suffix not yet reached cutting step 4 at pc(v3) unsat suffix not yet reached cutting step 3 at pc(v3) unsat suffix not yet reached cutting step 2 at pc(v4) LI at pc(v4): x'+1/4*y'=<5/4 cutting step 1 at pc(v4) LI at pc(v4): x'+1/4*y'=<5/4 refining loop cutting step 6 at pc(v2) unsat suffix not yet reached cutting step 5 at pc(v2) unsat suffix not yet reached cutting step 4 at pc(v3) unsat suffix not yet reached cutting step 3 at pc(v3) unsat suffix not yet reached cutting step 2 at pc(v4) LI at pc(v4): x'+1/4*y'=<5/4 cutting step 1 at pc(v4) LI at pc(v4): x'+1/4*y'=<5/4 refining stem cutting step 8 at pc(v1) unsat suffix not yet reached cutting step 7 at pc(v1) unsat suffix not yet reached cutting step 6 at pc(v2) unsat suffix not yet reached cutting step 5 at pc(v2) unsat suffix not yet reached cutting step 4 at pc(v3) unsat suffix not yet reached cutting step 3 at pc(v3) unsat suffix not yet reached cutting step 2 at pc(v4) LI at pc(v4): x'+1/4*y'=<5/4 cutting step 1 at pc(v4) LI at pc(v4): x'+1/4*y'=<5/4 -------------------------------------------------- abstraction refinement iteration 8: lfp iteration 0 1 2 3 4 5 6 7 8 9 10 ================================================== ARMC-LIVE: program is correct abstract trans fixpoint abstract_trans_state(0, pc(v0), pc(v0), [], stem, 1, (0,0)). abstract_trans_state(1, pc(v0), pc(v1), [1,3,7,10,11], stem, 2, (1,tid([6]))). abstract_trans_state(2, pc(v0), pc(v1), [11], stem, 3, (2,tid([1]))). abstract_trans_state(2, pc(v1), pc(v1), [9,11,12,13], loop, 4, (2,tid([1]))). abstract_trans_state(3, pc(v0), pc(v2), [3,4,7,11], stem, 5, (3,tid([7]))). abstract_trans_state(3, pc(v1), pc(v2), [3,4,7,11], loop, 6, (3,tid([7]))). abstract_trans_state(4, pc(v0), pc(v2), [3,4,11], stem, 7, (5,tid([2]))). abstract_trans_state(4, pc(v2), pc(v2), [3,4,8,9,11,13], loop, 8, (5,tid([2]))). abstract_trans_state(4, pc(v1), pc(v2), [3,4,11], loop, 9, (6,tid([2]))). abstract_trans_state(5, pc(v0), pc(v3), [2,3,4,11], stem, 10, (7,tid([8]))). abstract_trans_state(5, pc(v2), pc(v3), [2,3,4,5,11], loop, 11, (7,tid([8]))). abstract_trans_state(5, pc(v0), pc(v2), [4,11], stem, 12, (7,tid([2]))). abstract_trans_state(5, pc(v2), pc(v2), [4,8,9,11,13], loop, 13, (7,tid([2]))). abstract_trans_state(5, pc(v2), pc(v3), [2,3,4,8,9,11], loop, 14, (8,tid([8]))). abstract_trans_state(5, pc(v1), pc(v3), [2,3,4,11], loop, 15, (9,tid([8]))). abstract_trans_state(5, pc(v1), pc(v2), [4,11], loop, 16, (9,tid([2]))). abstract_trans_state(6, pc(v0), pc(v3), [11], stem, 17, (10,tid([3]))). abstract_trans_state(6, pc(v3), pc(v3), [5,6,9,11], loop, 18, (10,tid([3]))). abstract_trans_state(6, pc(v2), pc(v3), [5,11], loop, 19, (11,tid([3]))). abstract_trans_state(6, pc(v2), pc(v3), [4,11], loop, 20, (12,tid([8]))). abstract_trans_state(6, pc(v2), pc(v3), [8,9,11], loop, 21, (14,tid([3]))). abstract_trans_state(6, pc(v1), pc(v3), [11], loop, 22, (15,tid([3]))). abstract_trans_state(7, pc(v0), pc(v4), [1,3,7,11], stem, 23, (17,tid([11]))). abstract_trans_state(7, pc(v3), pc(v4), [1,3,7,11], loop, 24, (17,tid([11]))). abstract_trans_state(7, pc(v3), pc(v3), [6,9,11], loop, 25, (17,tid([3]))). abstract_trans_state(7, pc(v2), pc(v4), [1,3,5,6,7,11], loop, 26, (19,tid([11]))). abstract_trans_state(7, pc(v2), pc(v3), [11], loop, 27, (20,tid([3]))). abstract_trans_state(7, pc(v2), pc(v4), [1,3,7,8,11], loop, 28, (21,tid([11]))). abstract_trans_state(7, pc(v1), pc(v4), [1,3,7,11], loop, 29, (22,tid([11]))). abstract_trans_state(8, pc(v0), pc(v4), [1], stem, 30, (23,tid([4]))). abstract_trans_state(8, pc(v4), pc(v4), [1,6,8,9], loop, 31, (23,tid([4]))). abstract_trans_state(8, pc(v3), pc(v4), [1], loop, 32, (24,tid([4]))). abstract_trans_state(8, pc(v2), pc(v4), [1,5,6], loop, 33, (26,tid([4]))). abstract_trans_state(8, pc(v2), pc(v4), [1,3,7,11], loop, 34, (27,tid([11]))). abstract_trans_state(8, pc(v2), pc(v4), [1,8], loop, 35, (28,tid([4]))). abstract_trans_state(8, pc(v1), pc(v4), [1], loop, 36, (29,tid([4]))). abstract_trans_state(9, pc(v2), pc(v4), [1], loop, 37, (34,tid([4]))). frontier 0: stem 1 (pc(v0)->pc(v0)) from 0 by appying 0: T frontier 1: stem 2 (pc(v0)->pc(v1)) from 1 by appying tid([6]): x'+1/4*y'=<5/4, x'-1/6*y'=<0, x'=<0, y'=<1, y'>=1 frontier 2: stem 3 (pc(v0)->pc(v1)) from 2 by appying tid([1]): y'>=1 frontier 2: loop 4 (pc(v1)->pc(v1)) from 2 by appying tid([1]): x+t-x'-t'<0, y'>=1, y+t=<10, y+t-y'-t'<0 frontier 3: stem 5 (pc(v0)->pc(v2)) from 3 by appying tid([7]): x'-1/6*y'=<0, y'>=10, x'=<0, y'>=1 frontier 3: loop 6 (pc(v1)->pc(v2)) from 3 by appying tid([7]): x'-1/6*y'=<0, y'>=10, x'=<0, y'>=1 frontier 4: stem 7 (pc(v0)->pc(v2)) from 5 by appying tid([2]): x'-1/6*y'=<0, y'>=10, y'>=1 frontier 4: loop 8 (pc(v2)->pc(v2)) from 5 by appying tid([2]): x'-1/6*y'=<0, y'>=10, x+t=<2, x+t-x'-t'<0, y'>=1, y+t-y'-t'<0 frontier 4: loop 9 (pc(v1)->pc(v2)) from 6 by appying tid([2]): x'-1/6*y'=<0, y'>=10, y'>=1 frontier 5: stem 10 (pc(v0)->pc(v3)) from 7 by appying tid([8]): y'>=12, x'-1/6*y'=<0, y'>=10, y'>=1 frontier 5: loop 11 (pc(v2)->pc(v3)) from 7 by appying tid([8]): y'>=12, x'-1/6*y'=<0, y'>=10, y>=12, y'>=1 frontier 5: stem 12 (pc(v0)->pc(v2)) from 7 by appying tid([2]): y'>=10, y'>=1 frontier 5: loop 13 (pc(v2)->pc(v2)) from 7 by appying tid([2]): y'>=10, x+t=<2, x+t-x'-t'<0, y'>=1, y+t-y'-t'<0 frontier 5: loop 14 (pc(v2)->pc(v3)) from 8 by appying tid([8]): y'>=12, x'-1/6*y'=<0, y'>=10, x+t=<2, x+t-x'-t'<0, y'>=1 frontier 5: loop 15 (pc(v1)->pc(v3)) from 9 by appying tid([8]): y'>=12, x'-1/6*y'=<0, y'>=10, y'>=1 frontier 5: loop 16 (pc(v1)->pc(v2)) from 9 by appying tid([2]): y'>=10, y'>=1 frontier 6: stem 17 (pc(v0)->pc(v3)) from 10 by appying tid([3]): y'>=1 frontier 6: loop 18 (pc(v3)->pc(v3)) from 10 by appying tid([3]): y>=12, y-y'>0, x+t-x'-t'<0, y'>=1 frontier 6: loop 19 (pc(v2)->pc(v3)) from 11 by appying tid([3]): y>=12, y'>=1 frontier 6: loop 20 (pc(v2)->pc(v3)) from 12 by appying tid([8]): y'>=10, y'>=1 frontier 6: loop 21 (pc(v2)->pc(v3)) from 14 by appying tid([3]): x+t=<2, x+t-x'-t'<0, y'>=1 frontier 6: loop 22 (pc(v1)->pc(v3)) from 15 by appying tid([3]): y'>=1 frontier 7: stem 23 (pc(v0)->pc(v4)) from 17 by appying tid([11]): x'+1/4*y'=<5/4, x'-1/6*y'=<0, x'=<0, y'>=1 frontier 7: loop 24 (pc(v3)->pc(v4)) from 17 by appying tid([11]): x'+1/4*y'=<5/4, x'-1/6*y'=<0, x'=<0, y'>=1 frontier 7: loop 25 (pc(v3)->pc(v3)) from 17 by appying tid([3]): y-y'>0, x+t-x'-t'<0, y'>=1 frontier 7: loop 26 (pc(v2)->pc(v4)) from 19 by appying tid([11]): x'+1/4*y'=<5/4, x'-1/6*y'=<0, y>=12, y-y'>0, x'=<0, y'>=1 frontier 7: loop 27 (pc(v2)->pc(v3)) from 20 by appying tid([3]): y'>=1 frontier 7: loop 28 (pc(v2)->pc(v4)) from 21 by appying tid([11]): x'+1/4*y'=<5/4, x'-1/6*y'=<0, x'=<0, x+t=<2, y'>=1 frontier 7: loop 29 (pc(v1)->pc(v4)) from 22 by appying tid([11]): x'+1/4*y'=<5/4, x'-1/6*y'=<0, x'=<0, y'>=1 frontier 8: stem 30 (pc(v0)->pc(v4)) from 23 by appying tid([4]): x'+1/4*y'=<5/4 frontier 8: loop 31 (pc(v4)->pc(v4)) from 23 by appying tid([4]): x'+1/4*y'=<5/4, y-y'>0, x+t=<2, x+t-x'-t'<0 frontier 8: loop 32 (pc(v3)->pc(v4)) from 24 by appying tid([4]): x'+1/4*y'=<5/4 frontier 8: loop 33 (pc(v2)->pc(v4)) from 26 by appying tid([4]): x'+1/4*y'=<5/4, y>=12, y-y'>0 frontier 8: loop 34 (pc(v2)->pc(v4)) from 27 by appying tid([11]): x'+1/4*y'=<5/4, x'-1/6*y'=<0, x'=<0, y'>=1 frontier 8: loop 35 (pc(v2)->pc(v4)) from 28 by appying tid([4]): x'+1/4*y'=<5/4, x+t=<2 frontier 8: loop 36 (pc(v1)->pc(v4)) from 29 by appying tid([4]): x'+1/4*y'=<5/4 frontier 9: loop 37 (pc(v2)->pc(v4)) from 34 by appying tid([4]): x'+1/4*y'=<5/4 _222269->_222272: #13: x'+1/4*y'=<5/4, y'>=12, x'-1/6*y'=<0, y'>=10, y>=12, y-y'>0, x'=<0, x+t=<2, x+t-x'-t'<0, y'=<1, y'>=1, y+t=<10, y+t-y'-t'<0 Time on instantiating uf axioms: run 0.00, wall 0.00 s. Time on cli constraint solving: run 0.07, wall 0.12 s. Time on cli constraint preparation: run 0.00, wall 0.00 s. Time on cli matrix parsing: run 0.00, wall 0.00 s. Time on cli preprocessing: run 0.00, wall 0.00 s. Time on computing the subsumer subtree: run 0.00, wall 0.00 s. Time on finding the location of subsumer in queue: run 0.00, wall 0.00 s. Time on asserting thick transitions: run 0.00, wall 0.00 s. Time on path invariant generation: run 0.00, wall 0.00 s. Time on new predicate selection: run 0.01, wall 0.01 s. Time on refinement preprocessing cut: run 0.00, wall 0.00 s. Time on refinement cutting trace: run 0.21, wall 0.32 s. Time on refinement finding unsat subtrace: run 0.00, wall 0.00 s. Time on refinement: run 0.24, wall 0.40 s. Time on concrete postcondition operator: run 0.00, wall 0.00 s. Time on fixpoint abstraction: run 0.00, wall 0.00 s. Time on fixpoint test: run 0.00, wall 0.00 s. Time on abstract check: run 0.00, wall 0.00 s. Time on total including result checking: run 0.00, wall 0.00 s. Time on check result: run 0.00, wall 0.00 s. Time on total: run 0.00, wall 0.00 s. ================================================== ARMC-LIVE: program is correct [runlim] end: Sun Nov 30 19:22:31 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 1.60 seconds [runlim] time: 0.63 seconds [runlim] space: 8.4 MB [runlim] samples: 8