[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/tmpFile20141130191046.armc [runlim] argv[3]: -straight [runlim] start: Sun Nov 30 19:22:31 2014 [runlim] main pid: 5144 ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008) rybal@mpi-sws.mpg.de cmd line: [live,/home/zhouyan/BACH/tmpFile20141130191046.armc,-straight] reading input from /home/zhouyan/BACH/tmpFile20141130191046.armc...done. creating straight line code between cutpoints...done. meta_transition(p(pc(v1),data(A,B,C,_)), p(pc(v4),data(D,E,F,G)), [], [F=C,E=B,D=A,C=15,B<6,A<6,C=<15,G>0], [10]). meta_transition(p(pc(v3),data(A,_,B,_)), p(pc(v1),data(C,D,E,F)), [], [E=B,C=A,D=0.0,B=3,B>=3,F>0,E=<15], [9]). meta_transition(p(pc(v1),data(A,B,C,_)), p(pc(v3),data(D,E,F,G)), [], [F=C,E=B,D=A,C=15,B>=6,C=<15,G>0,F>=3], [8]). meta_transition(p(pc(v2),data(_,A,B,_)), p(pc(v1),data(C,D,E,F)), [], [E=B,D=A,C=0.0,B=3,B>=3,F>0,E=<15], [7]). meta_transition(p(pc(v1),data(A,B,C,_)), p(pc(v2),data(D,E,F,G)), [], [F=C,E=B,D=A,A>=6,C=15,C=<15,G>0,F>=3], [6]). meta_transition(p(pc(v4),data(A,B,C,D)), p(pc(v4),data(E,F,G,H)), [], [G=C,F=B,E=A,H>0,D>0], [4]). meta_transition(p(pc(v3),data(A,B,C,D)), p(pc(v3),data(E,F,G,H)), [], [G==C-3.1*D,F=B+D,E=A+D,H>0,D>0,G>=3,C>=3], [3]). meta_transition(p(pc(v2),data(A,B,C,D)), p(pc(v2),data(E,F,G,H)), [], [G==C-4.1*D,F=B+D,E=A+D,H>0,D>0,G>=3,C>=3], [2]). meta_transition(p(pc(v1),data(A,B,C,D)), p(pc(v1),data(E,F,G,H)), [], [G==C+0.9*D,F=B+D,E=A+D,H>0,D>0,G=<15,C=<15], [1]). meta_transition(p(pc(v0),data(_,_,_,_)), p(pc(v1),data(A,B,C,D)), [], [C=3.0,B=6.0,A=6.0,D>0,C=<15], [5]). transition(p(pc(v1),data(A,B,C,_)), p(pc(v4),data(D,E,F,G)), {F=C,E=B,D=A,C=15,B<6,A<6,C=<15,G>0}, [], [F=C,E=B,D=A,C=15,B<6,A<6,C=<15,G>0], tid([10])). transition(p(pc(v3),data(A,_,B,_)), p(pc(v1),data(C,D,E,F)), {E=B,C=A,D=0.0,B=3,B>=3,F>0,E=<15}, [], [E=B,C=A,D=0.0,B=3,B>=3,F>0,E=<15], tid([9])). transition(p(pc(v1),data(A,B,C,_)), p(pc(v3),data(D,E,F,G)), {F=C,E=B,D=A,C=15,B>=6,C=<15,G>0,F>=3}, [], [F=C,E=B,D=A,C=15,B>=6,C=<15,G>0,F>=3], tid([8])). transition(p(pc(v2),data(_,A,B,_)), p(pc(v1),data(C,D,E,F)), {E=B,D=A,C=0.0,B=3,B>=3,F>0,E=<15}, [], [E=B,D=A,C=0.0,B=3,B>=3,F>0,E=<15], tid([7])). transition(p(pc(v1),data(A,B,C,_)), p(pc(v2),data(D,E,F,G)), {F=C,E=B,D=A,A>=6,C=15,C=<15,G>0,F>=3}, [], [F=C,E=B,D=A,A>=6,C=15,C=<15,G>0,F>=3], tid([6])). transition(p(pc(v4),data(A,B,C,D)), p(pc(v4),data(E,F,G,H)), {G=C,F=B,E=A,H>0,D>0}, [], [G=C,F=B,E=A,H>0,D>0], tid([4])). transition(p(pc(v3),data(A,B,C,D)), p(pc(v3),data(E,F,G,H)), {G==C-3.1*D,F=B+D,E=A+D,H>0,D>0,G>=3,C>=3}, [], [G==C-3.1*D,F=B+D,E=A+D,H>0,D>0,G>=3,C>=3], tid([3])). transition(p(pc(v2),data(A,B,C,D)), p(pc(v2),data(E,F,G,H)), {G==C-4.1*D,F=B+D,E=A+D,H>0,D>0,G>=3,C>=3}, [], [G==C-4.1*D,F=B+D,E=A+D,H>0,D>0,G>=3,C>=3], tid([2])). transition(p(pc(v1),data(A,B,C,D)), p(pc(v1),data(E,F,G,H)), {G==C+0.9*D,F=B+D,E=A+D,H>0,D>0,G=<15,C=<15}, [], [G==C+0.9*D,F=B+D,E=A+D,H>0,D>0,G=<15,C=<15], tid([1])). transition(p(pc(v0),data(_,_,_,_)), p(pc(v1),data(A,B,C,D)), {C=3.0,B=6.0,A=6.0,D>0,C=<15}, [], [C=3.0,B=6.0,A=6.0,D>0,C=<15], tid([5])). tid([10]): pc(v1) pc(v4) {th'=th,x2'=x2,x1'=x1,th=15,x2<6,x1<6,th=<15,t'>0} [] [th'=th,x2'=x2,x1'=x1,th=15,x2<6,x1<6,th=<15,t'>0] tid([9]): pc(v3) pc(v1) {th'=th,x1'=x1,x2'=0.0,th=3,th>=3,t'>0,th'=<15} [] [th'=th,x1'=x1,x2'=0.0,th=3,th>=3,t'>0,th'=<15] tid([8]): pc(v1) pc(v3) {th'=th,x2'=x2,x1'=x1,th=15,x2>=6,th=<15,t'>0,th'>=3} [] [th'=th,x2'=x2,x1'=x1,th=15,x2>=6,th=<15,t'>0,th'>=3] tid([7]): pc(v2) pc(v1) {th'=th,x2'=x2,x1'=0.0,th=3,th>=3,t'>0,th'=<15} [] [th'=th,x2'=x2,x1'=0.0,th=3,th>=3,t'>0,th'=<15] tid([6]): pc(v1) pc(v2) {th'=th,x2'=x2,x1'=x1,x1>=6,th=15,th=<15,t'>0,th'>=3} [] [th'=th,x2'=x2,x1'=x1,x1>=6,th=15,th=<15,t'>0,th'>=3] tid([4]): pc(v4) pc(v4) {th'=th,x2'=x2,x1'=x1,t'>0,t>0} [] [th'=th,x2'=x2,x1'=x1,t'>0,t>0] tid([3]): pc(v3) pc(v3) {th'==th-3.1*t,x2'=x2+t,x1'=x1+t,t'>0,t>0,th'>=3,th>=3} [] [th'==th-3.1*t,x2'=x2+t,x1'=x1+t,t'>0,t>0,th'>=3,th>=3] tid([2]): pc(v2) pc(v2) {th'==th-4.1*t,x2'=x2+t,x1'=x1+t,t'>0,t>0,th'>=3,th>=3} [] [th'==th-4.1*t,x2'=x2+t,x1'=x1+t,t'>0,t>0,th'>=3,th>=3] tid([1]): pc(v1) pc(v1) {th'==th+0.9*t,x2'=x2+t,x1'=x1+t,t'>0,t>0,th'=<15,th=<15} [] [th'==th+0.9*t,x2'=x2+t,x1'=x1+t,t'>0,t>0,th'=<15,th=<15] tid([5]): pc(v0) pc(v1) {th'=3.0,x2'=6.0,x1'=6.0,t'>0,th'=<15} [] [th'=3.0,x2'=6.0,x1'=6.0,t'>0,th'=<15] -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 abstract counterexample: stem [0,tid([5])], loop [tid([1])] trans preds: _9417->_9420: #0: th+9/10*t>=151/10 th+9/10*t-th'-9/10*t'>= -4/5 path is sat -------------------------------------------------- abstraction refinement iteration 0: lfp iteration 0 1 2 abstract counterexample: stem [0,tid([5])], loop [] trans preds: _9218->_9221: #0: projected loop: x1'=x1, x2'=x2, th'=th, t'=t, x1=6, x1'=x1, x2'=x2, th'=th, t'=t, x2=6, x1'=x1, x2'=x2, th'=th, t'=t, th=3, x1'=x1, x2'=x2, th'=th, t'=t, t>0 ================================================== ARMC-Live: feasible counterexample: stem [0,tid([5])] loop [] Stem: 0: unknown 5: unknown Loop: halt Time on instantiating uf axioms: run 0.00, wall 0.00 s. Time on cli constraint solving: run 0.00, wall 0.00 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.00, wall 0.00 s. Time on refinement preprocessing cut: run 0.00, wall 0.00 s. Time on refinement cutting trace: run 0.00, wall 0.00 s. Time on refinement finding unsat subtrace: run 0.00, wall 0.00 s. Time on refinement: run 0.00, wall 0.00 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. [runlim] end: Sun Nov 30 19:22:31 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 0.69 seconds [runlim] time: 0.00 seconds [runlim] space: 0.0 MB [runlim] samples: 0