[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/tmpFile20141130191410.armc
[runlim] argv[3]:		-straight
[runlim] start:			Sun Nov 30 19:22:32 2014
[runlim] main pid:		8583
ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [live,/home/zhouyan/BACH/tmpFile20141130191410.armc,-straight]
reading input from /home/zhouyan/BACH/tmpFile20141130191410.armc...done.
creating straight line code between cutpoints...done.
meta_transition(p(pc(v1),data(A,B,C,D,E,_)), p(pc(v5),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,D-E<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0], [19]).
meta_transition(p(pc(v5),data(A,B,C,D,E,_)), p(pc(v6),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,D-E<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0], [18]).
meta_transition(p(pc(v5),data(A,B,C,D,E,_)), p(pc(v1),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,D-E>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2], [17]).
meta_transition(p(pc(v4),data(A,B,C,D,E,_)), p(pc(v6),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,C-D<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0], [16]).
meta_transition(p(pc(v3),data(A,B,C,D,E,_)), p(pc(v6),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,B-C<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0], [15]).
meta_transition(p(pc(v2),data(A,B,C,D,E,_)), p(pc(v6),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,A-B<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0], [14]).
meta_transition(p(pc(v2),data(A,B,C,D,E,_)), p(pc(v1),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,A-B>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2], [13]).
meta_transition(p(pc(v1),data(A,B,C,D,E,_)), p(pc(v2),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,A-B<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0], [12]).
meta_transition(p(pc(v3),data(A,B,C,D,E,_)), p(pc(v1),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,B-C>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2], [11]).
meta_transition(p(pc(v1),data(A,B,C,D,E,_)), p(pc(v3),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,B-C<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0], [10]).
meta_transition(p(pc(v4),data(A,B,C,D,E,_)), p(pc(v1),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,C-D>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2], [9]).
meta_transition(p(pc(v1),data(A,B,C,D,E,_)), p(pc(v4),data(F,G,H,I,J,K)), [], [J=E,I=D,H=C,G=B,F=A,C-D<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0], [8]).
meta_transition(p(pc(v5),data(A,B,C,D,E,F)), p(pc(v5),data(G,H,I,J,K,L)), [], [K=E+10*F,J=D+12*F,I=C+12*F,H=B+12*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0], [6]).
meta_transition(p(pc(v3),data(A,B,C,D,E,F)), p(pc(v3),data(G,H,I,J,K,L)), [], [K=<E+10*F,K>=E+8*F,J=<D+10*F,J>=D+8*F,I=C+10*F,H=B+12*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0], [5]).
meta_transition(p(pc(v1),data(A,B,C,D,E,F)), p(pc(v1),data(G,H,I,J,K,L)), [], [K=<E+10*F,K>=E+8*F,J=<D+10*F,J>=D+8*F,I=<C+10*F,I>=C+8*F,H=<B+10*F,H>=B+8*F,G=<A+10*F,G>=A+8*F,L>0,F>0,J-K<10,D-E<10,J-K>2,D-E>2,I-J<10,C-D<10,I-J>2,C-D>2,H-I<10,B-C<10,H-I>2,B-C>2,G-H<10,A-B<10,G-H>2,A-B>2], [4]).
meta_transition(p(pc(v4),data(A,B,C,D,E,F)), p(pc(v4),data(G,H,I,J,K,L)), [], [K=<E+10*F,K>=E+8*F,J=D+10*F,I=C+12*F,H=B+12*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0], [3]).
meta_transition(p(pc(v2),data(A,B,C,D,E,F)), p(pc(v2),data(G,H,I,J,K,L)), [], [K=<E+10*F,K>=E+8*F,J=<D+10*F,J>=D+8*F,I=<C+10*F,I>=C+8*F,H=B+10*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0], [2]).
meta_transition(p(pc(v6),data(A,B,C,D,E,F)), p(pc(v6),data(G,H,I,J,K,L)), [], [K=E+12*F,J=D+12*F,I=C+12*F,H=B+12*F,G=A+12*F,L>0,F>0], [1]).
meta_transition(p(pc(v0),data(_,_,_,_,_,_)), p(pc(v1),data(A,B,C,D,E,F)), [], [E=40.0,D=45.0,C=50.0,B=55.0,A=60.0,F>0,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2], [7]).


transition(p(pc(v1),data(A,B,C,D,E,_)), p(pc(v5),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,D-E<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0}, [], [J=E,I=D,H=C,G=B,F=A,D-E<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0], tid([19])).
transition(p(pc(v5),data(A,B,C,D,E,_)), p(pc(v6),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,D-E<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0}, [], [J=E,I=D,H=C,G=B,F=A,D-E<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0], tid([18])).
transition(p(pc(v5),data(A,B,C,D,E,_)), p(pc(v1),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,D-E>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2}, [], [J=E,I=D,H=C,G=B,F=A,D-E>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2], tid([17])).
transition(p(pc(v4),data(A,B,C,D,E,_)), p(pc(v6),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,C-D<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0}, [], [J=E,I=D,H=C,G=B,F=A,C-D<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0], tid([16])).
transition(p(pc(v3),data(A,B,C,D,E,_)), p(pc(v6),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,B-C<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0}, [], [J=E,I=D,H=C,G=B,F=A,B-C<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0], tid([15])).
transition(p(pc(v2),data(A,B,C,D,E,_)), p(pc(v6),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,A-B<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0}, [], [J=E,I=D,H=C,G=B,F=A,A-B<1,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0], tid([14])).
transition(p(pc(v2),data(A,B,C,D,E,_)), p(pc(v1),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,A-B>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2}, [], [J=E,I=D,H=C,G=B,F=A,A-B>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2], tid([13])).
transition(p(pc(v1),data(A,B,C,D,E,_)), p(pc(v2),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,A-B<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0}, [], [J=E,I=D,H=C,G=B,F=A,A-B<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0], tid([12])).
transition(p(pc(v3),data(A,B,C,D,E,_)), p(pc(v1),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,B-C>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2}, [], [J=E,I=D,H=C,G=B,F=A,B-C>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2], tid([11])).
transition(p(pc(v1),data(A,B,C,D,E,_)), p(pc(v3),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,B-C<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0}, [], [J=E,I=D,H=C,G=B,F=A,B-C<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0], tid([10])).
transition(p(pc(v4),data(A,B,C,D,E,_)), p(pc(v1),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,C-D>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2}, [], [J=E,I=D,H=C,G=B,F=A,C-D>4,D-E<10,D-E>0,C-D<10,C-D>0,B-C<10,B-C>0,A-B<10,A-B>0,K>0,I-J<10,I-J>2,H-I<10,H-I>2,G-H<10,G-H>2,F-G<10,F-G>2], tid([9])).
transition(p(pc(v1),data(A,B,C,D,E,_)), p(pc(v4),data(F,G,H,I,J,K)), {J=E,I=D,H=C,G=B,F=A,C-D<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0}, [], [J=E,I=D,H=C,G=B,F=A,C-D<4,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2,K>0,I-J<10,I-J>0,H-I<10,H-I>0,G-H<10,G-H>0,F-G<10,F-G>0], tid([8])).
transition(p(pc(v5),data(A,B,C,D,E,F)), p(pc(v5),data(G,H,I,J,K,L)), {K=E+10*F,J=D+12*F,I=C+12*F,H=B+12*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0}, [], [K=E+10*F,J=D+12*F,I=C+12*F,H=B+12*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0], tid([6])).
transition(p(pc(v3),data(A,B,C,D,E,F)), p(pc(v3),data(G,H,I,J,K,L)), {K=<E+10*F,K>=E+8*F,J=<D+10*F,J>=D+8*F,I=C+10*F,H=B+12*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0}, [], [K=<E+10*F,K>=E+8*F,J=<D+10*F,J>=D+8*F,I=C+10*F,H=B+12*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0], tid([5])).
transition(p(pc(v1),data(A,B,C,D,E,F)), p(pc(v1),data(G,H,I,J,K,L)), {K=<E+10*F,K>=E+8*F,J=<D+10*F,J>=D+8*F,I=<C+10*F,I>=C+8*F,H=<B+10*F,H>=B+8*F,G=<A+10*F,G>=A+8*F,L>0,F>0,J-K<10,D-E<10,J-K>2,D-E>2,I-J<10,C-D<10,I-J>2,C-D>2,H-I<10,B-C<10,H-I>2,B-C>2,G-H<10,A-B<10,G-H>2,A-B>2}, [], [K=<E+10*F,K>=E+8*F,J=<D+10*F,J>=D+8*F,I=<C+10*F,I>=C+8*F,H=<B+10*F,H>=B+8*F,G=<A+10*F,G>=A+8*F,L>0,F>0,J-K<10,D-E<10,J-K>2,D-E>2,I-J<10,C-D<10,I-J>2,C-D>2,H-I<10,B-C<10,H-I>2,B-C>2,G-H<10,A-B<10,G-H>2,A-B>2], tid([4])).
transition(p(pc(v4),data(A,B,C,D,E,F)), p(pc(v4),data(G,H,I,J,K,L)), {K=<E+10*F,K>=E+8*F,J=D+10*F,I=C+12*F,H=B+12*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0}, [], [K=<E+10*F,K>=E+8*F,J=D+10*F,I=C+12*F,H=B+12*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0], tid([3])).
transition(p(pc(v2),data(A,B,C,D,E,F)), p(pc(v2),data(G,H,I,J,K,L)), {K=<E+10*F,K>=E+8*F,J=<D+10*F,J>=D+8*F,I=<C+10*F,I>=C+8*F,H=B+10*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0}, [], [K=<E+10*F,K>=E+8*F,J=<D+10*F,J>=D+8*F,I=<C+10*F,I>=C+8*F,H=B+10*F,G=A+12*F,L>0,F>0,J-K<10,D-E<10,J-K>0,D-E>0,I-J<10,C-D<10,I-J>0,C-D>0,H-I<10,B-C<10,H-I>0,B-C>0,G-H<10,A-B<10,G-H>0,A-B>0], tid([2])).
transition(p(pc(v6),data(A,B,C,D,E,F)), p(pc(v6),data(G,H,I,J,K,L)), {K=E+12*F,J=D+12*F,I=C+12*F,H=B+12*F,G=A+12*F,L>0,F>0}, [], [K=E+12*F,J=D+12*F,I=C+12*F,H=B+12*F,G=A+12*F,L>0,F>0], tid([1])).
transition(p(pc(v0),data(_,_,_,_,_,_)), p(pc(v1),data(A,B,C,D,E,F)), {E=40.0,D=45.0,C=50.0,B=55.0,A=60.0,F>0,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2}, [], [E=40.0,D=45.0,C=50.0,B=55.0,A=60.0,F>0,D-E<10,D-E>2,C-D<10,C-D>2,B-C<10,B-C>2,A-B<10,A-B>2], tid([7])).

tid([19]): pc(v1) pc(v5) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5<4,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x4'-x5'<10,x4'-x5'>0,x3'-x4'<10,x3'-x4'>0,x2'-x3'<10,x2'-x3'>0,x1'-x2'<10,x1'-x2'>0}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5<4,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x4'-x5'<10,x4'-x5'>0,x3'-x4'<10,x3'-x4'>0,x2'-x3'<10,x2'-x3'>0,x1'-x2'<10,x1'-x2'>0]
tid([18]): pc(v5) pc(v6) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5<1,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5<1,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0]
tid([17]): pc(v5) pc(v1) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5>4,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x4-x5>4,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2]
tid([16]): pc(v4) pc(v6) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4<1,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4<1,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0]
tid([15]): pc(v3) pc(v6) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3<1,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3<1,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0]
tid([14]): pc(v2) pc(v6) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2<1,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2<1,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0]
tid([13]): pc(v2) pc(v1) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2>4,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2>4,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2]
tid([12]): pc(v1) pc(v2) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2<4,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x4'-x5'<10,x4'-x5'>0,x3'-x4'<10,x3'-x4'>0,x2'-x3'<10,x2'-x3'>0,x1'-x2'<10,x1'-x2'>0}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x1-x2<4,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x4'-x5'<10,x4'-x5'>0,x3'-x4'<10,x3'-x4'>0,x2'-x3'<10,x2'-x3'>0,x1'-x2'<10,x1'-x2'>0]
tid([11]): pc(v3) pc(v1) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3>4,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3>4,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2]
tid([10]): pc(v1) pc(v3) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3<4,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x4'-x5'<10,x4'-x5'>0,x3'-x4'<10,x3'-x4'>0,x2'-x3'<10,x2'-x3'>0,x1'-x2'<10,x1'-x2'>0}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x2-x3<4,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x4'-x5'<10,x4'-x5'>0,x3'-x4'<10,x3'-x4'>0,x2'-x3'<10,x2'-x3'>0,x1'-x2'<10,x1'-x2'>0]
tid([9]): pc(v4) pc(v1) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4>4,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4>4,x4-x5<10,x4-x5>0,x3-x4<10,x3-x4>0,x2-x3<10,x2-x3>0,x1-x2<10,x1-x2>0,t'>0,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2]
tid([8]): pc(v1) pc(v4) {x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4<4,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x4'-x5'<10,x4'-x5'>0,x3'-x4'<10,x3'-x4'>0,x2'-x3'<10,x2'-x3'>0,x1'-x2'<10,x1'-x2'>0}
[] [x5'=x5,x4'=x4,x3'=x3,x2'=x2,x1'=x1,x3-x4<4,x4-x5<10,x4-x5>2,x3-x4<10,x3-x4>2,x2-x3<10,x2-x3>2,x1-x2<10,x1-x2>2,t'>0,x4'-x5'<10,x4'-x5'>0,x3'-x4'<10,x3'-x4'>0,x2'-x3'<10,x2'-x3'>0,x1'-x2'<10,x1'-x2'>0]
tid([6]): pc(v5) pc(v5) {x5'=x5+10*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0}
[] [x5'=x5+10*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0]
tid([5]): pc(v3) pc(v3) {x5'=<x5+10*t,x5'>=x5+8*t,x4'=<x4+10*t,x4'>=x4+8*t,x3'=x3+10*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0}
[] [x5'=<x5+10*t,x5'>=x5+8*t,x4'=<x4+10*t,x4'>=x4+8*t,x3'=x3+10*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0]
tid([4]): pc(v1) pc(v1) {x5'=<x5+10*t,x5'>=x5+8*t,x4'=<x4+10*t,x4'>=x4+8*t,x3'=<x3+10*t,x3'>=x3+8*t,x2'=<x2+10*t,x2'>=x2+8*t,x1'=<x1+10*t,x1'>=x1+8*t,t'>0,t>0,x4'-x5'<10,x4-x5<10,x4'-x5'>2,x4-x5>2,x3'-x4'<10,x3-x4<10,x3'-x4'>2,x3-x4>2,x2'-x3'<10,x2-x3<10,x2'-x3'>2,x2-x3>2,x1'-x2'<10,x1-x2<10,x1'-x2'>2,x1-x2>2}
[] [x5'=<x5+10*t,x5'>=x5+8*t,x4'=<x4+10*t,x4'>=x4+8*t,x3'=<x3+10*t,x3'>=x3+8*t,x2'=<x2+10*t,x2'>=x2+8*t,x1'=<x1+10*t,x1'>=x1+8*t,t'>0,t>0,x4'-x5'<10,x4-x5<10,x4'-x5'>2,x4-x5>2,x3'-x4'<10,x3-x4<10,x3'-x4'>2,x3-x4>2,x2'-x3'<10,x2-x3<10,x2'-x3'>2,x2-x3>2,x1'-x2'<10,x1-x2<10,x1'-x2'>2,x1-x2>2]
tid([3]): pc(v4) pc(v4) {x5'=<x5+10*t,x5'>=x5+8*t,x4'=x4+10*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0}
[] [x5'=<x5+10*t,x5'>=x5+8*t,x4'=x4+10*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0]
tid([2]): pc(v2) pc(v2) {x5'=<x5+10*t,x5'>=x5+8*t,x4'=<x4+10*t,x4'>=x4+8*t,x3'=<x3+10*t,x3'>=x3+8*t,x2'=x2+10*t,x1'=x1+12*t,t'>0,t>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0}
[] [x5'=<x5+10*t,x5'>=x5+8*t,x4'=<x4+10*t,x4'>=x4+8*t,x3'=<x3+10*t,x3'>=x3+8*t,x2'=x2+10*t,x1'=x1+12*t,t'>0,t>0,x4'-x5'<10,x4-x5<10,x4'-x5'>0,x4-x5>0,x3'-x4'<10,x3-x4<10,x3'-x4'>0,x3-x4>0,x2'-x3'<10,x2-x3<10,x2'-x3'>0,x2-x3>0,x1'-x2'<10,x1-x2<10,x1'-x2'>0,x1-x2>0]
tid([1]): pc(v6) pc(v6) {x5'=x5+12*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0}
[] [x5'=x5+12*t,x4'=x4+12*t,x3'=x3+12*t,x2'=x2+12*t,x1'=x1+12*t,t'>0,t>0]
tid([7]): pc(v0) pc(v1) {x5'=40.0,x4'=45.0,x3'=50.0,x2'=55.0,x1'=60.0,t'>0,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2}
[] [x5'=40.0,x4'=45.0,x3'=50.0,x2'=55.0,x1'=60.0,t'>0,x4'-x5'<10,x4'-x5'>2,x3'-x4'<10,x3'-x4'>2,x2'-x3'<10,x2'-x3'>2,x1'-x2'<10,x1'-x2'>2]



--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 
abstract counterexample: stem [0,tid([7])], loop [tid([4])]
trans preds: _18171->_18174:	#0:	
projected loop:
x1=60, x2=55, x3=50, x4=45, x5=40, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t>0, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0
x1>=61
x1-x1'>= -7
path is sat



--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 
abstract counterexample: stem [0,tid([7]),tid([12])], loop []
trans preds: _7827->_7830:	#0:	
projected loop infeasible:
x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, 1=1
x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, 1=1
refining stem

cutting step 1 at pc(v1)
LI at pc(v1): x1'-x2'>=5

refining stem

cutting step 1 at pc(v1)
LI at pc(v1): x1'-x2'>=5




--------------------------------------------------
abstraction refinement iteration 1:
lfp iteration 0 1 
abstract counterexample: stem [0,tid([7])], loop [tid([4])]
trans preds: _198494->_198497:	#1:	x1'-x2'>=5
projected loop:
x1=60, x2=55, x3=50, x4=45, x5=40, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t>0, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0
x1>=61
x1-x1'>= -7
path is sat



--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 
abstract counterexample: stem [0,tid([7]),tid([10])], loop []
trans preds: _7654->_7657:	#1:	x1'-x2'>=5
projected loop infeasible:
x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, 1=1
x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, 1=1
refining stem

cutting step 1 at pc(v1)
LI at pc(v1): x2'-x3'>=5

refining stem

cutting step 1 at pc(v1)
LI at pc(v1): x2'-x3'>=5




--------------------------------------------------
abstraction refinement iteration 1:
lfp iteration 0 1 
abstract counterexample: stem [0,tid([7])], loop [tid([4])]
trans preds: _193762->_193765:	#2:	x2'-x3'>=5, x1'-x2'>=5
projected loop:
x1=60, x2=55, x3=50, x4=45, x5=40, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t>0, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0
x1>=61
x1-x1'>= -7
path is sat



--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 
abstract counterexample: stem [0,tid([7]),tid([8])], loop []
trans preds: _7305->_7308:	#2:	x2'-x3'>=5, x1'-x2'>=5
projected loop infeasible:
x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, 1=1
x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, 1=1
refining stem

cutting step 1 at pc(v1)
LI at pc(v1): x3'-x4'>=5

refining stem

cutting step 1 at pc(v1)
LI at pc(v1): x3'-x4'>=5




--------------------------------------------------
abstraction refinement iteration 1:
lfp iteration 0 1 
abstract counterexample: stem [0,tid([7])], loop [tid([4])]
trans preds: _195440->_195443:	#3:	x3'-x4'>=5, x2'-x3'>=5, x1'-x2'>=5
projected loop:
x1=60, x2=55, x3=50, x4=45, x5=40, x1'-x2'>2, x1'-x2'<10, x2'-x3'>2, x2'-x3'<10, x3'-x4'>2, x3'-x4'<10, x4'-x5'>2, x4'-x5'<10, t-1/8*x1'=< -15/2, t-1/8*x2'=< -55/8, t-1/8*x3'=< -25/4, t-1/8*x4'=< -45/8, t-1/8*x5'=< -5, t>0, t-1/10*x5'>= -4, t-1/10*x4'>= -9/2, t-1/10*x3'>= -5, t-1/10*x2'>= -11/2, t-1/10*x1'>= -6, t'>0
x1>=61
x1-x1'>= -7
path is sat



--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 
abstract counterexample: stem [0,tid([7]),tid([4])], loop []
trans preds: _7148->_7151:	#3:	x3'-x4'>=5, x2'-x3'>=5, x1'-x2'>=5
projected loop:
x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1-5/4*x5=<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x2-5/4*x5=<5, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x3-5/4*x5=<0, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x4-5/4*x5=< -5, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1-5/4*x4=<15/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x2-5/4*x4=< -5/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x3-5/4*x4=< -25/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x4-4/5*x5>=13, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1-5/4*x3=< -5/2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x2-5/4*x3=< -15/2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x3-4/5*x4>=14, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x3-4/5*x5>=18, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1-5/4*x2=< -35/4, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x2-4/5*x3>=15, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x2-4/5*x4>=19, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x2-4/5*x5>=23, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1-4/5*x2>=16, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1-4/5*x3>=20, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1-4/5*x4>=24, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1-4/5*x5>=28, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1>60, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1-x2>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x1-x2<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x2-x3>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x2-x3<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x3-x4>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x3-x4<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x4-x5>2, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, x4-x5<10, x1'=x1, x2'=x2, x3'=x3, x4'=x4, x5'=x5, t'=t, t>0



==================================================
ARMC-Live: feasible counterexample:
	stem [0,tid([7]),tid([4])]
	loop []
Stem:
0:	unknown
7:	unknown
4:	unknown
Loop:
halt
Time on instantiating uf axioms:		run 0.00,	 wall 0.00 s.
Time on cli constraint solving:		run 0.05,	 wall 0.06 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.00 s.
Time on refinement preprocessing cut:		run 0.00,	 wall 0.00 s.
Time on refinement cutting trace:		run 0.07,	 wall 0.09 s.
Time on refinement finding unsat subtrace:		run 0.00,	 wall 0.00 s.
Time on refinement:		run 0.08,	 wall 0.12 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:33 2014
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			1.45 seconds
[runlim] time:			0.98 seconds
[runlim] space:			7.9 MB
[runlim] samples:		11