[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/tmpFile20141130190930.armc
[runlim] argv[3]:		-straight
[runlim] start:			Sun Nov 30 19:22:26 2014
[runlim] main pid:		28786
ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [live,/home/zhouyan/BACH/tmpFile20141130190930.armc,-straight]
reading input from /home/zhouyan/BACH/tmpFile20141130190930.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,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-2*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,A=2,A=<2,E>0,D=<10}, [], [D=B,C=A,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-2*C,D=A+C,F>0,C>0,D=<2,A=<2}, [], [E=B-2*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,x=2,x=<2,t'>0,y'=<10}
[] [y'=y,x'=x,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-2*t,x'=x+t,t'>0,t>0,x'=<2,x=<2}
[] [y'=y-2*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: _9070->_9073:	#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): _8357+_8358-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): _8357+_8358=<10




--------------------------------------------------
abstraction refinement iteration 1:
lfp iteration 0 1 2 
abstract counterexample: stem [0,tid([6]),tid([10])], loop [tid([5])]
trans preds: _101622->_101625:	#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: _125991->_125994:	#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: _176016->_176019:	#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): _174976+_174978-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): _3324+_3326=<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: _41784->_41787:	#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: _130590->_130593:	#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): _129228-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): _19824>=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: _111572->_111575:	#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: _214464->_214467:	#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
y=<9
y'-y>= -8
refining loop
cutting step 7 at pc(v2)
LI at pc(v2): y>=10
cutting step 6 at pc(v2)
LI at pc(v2): x'-1/5*y=<0
cutting step 5 at pc(v3)
LI at pc(v3): y>=10
cutting step 4 at pc(v3)
LI at pc(v3): y>=10
cutting step 3 at pc(v4)
LI at pc(v4): x'+1/2*y'-1/2*y=< -5/2
cutting step 2 at pc(v4)
LI at pc(v4): x'+2/9*y'-2/9*y=<0
cutting step 1 at pc(v1)
LI at pc(v1): y'-y=< -9

refining stem

cutting step 9 at pc(v1)
unsat suffix not yet reached
cutting step 8 at pc(v1)
unsat suffix not yet reached
cutting step 7 at pc(v2)
LI at pc(v2): _132199>=10
cutting step 6 at pc(v2)
cutting step 5 at pc(v3)
cutting step 4 at pc(v3)
cutting step 3 at pc(v4)
cutting step 2 at pc(v4)
cutting step 1 at pc(v1)

refining loop
cutting step 7 at pc(v2)
LI at pc(v2): y>=10
cutting step 6 at pc(v2)
LI at pc(v2): x'-1/5*y=<0
cutting step 5 at pc(v3)
LI at pc(v3): y>=10
cutting step 4 at pc(v3)
LI at pc(v3): y>=10
cutting step 3 at pc(v4)
LI at pc(v4): y>=10
cutting step 2 at pc(v4)
LI at pc(v4): x'-1/5*y=<0
cutting step 1 at pc(v1)
LI at pc(v1): y>=10

refining stem

cutting step 9 at pc(v1)
unsat suffix not yet reached
cutting step 8 at pc(v1)
unsat suffix not yet reached
cutting step 7 at pc(v2)
LI at pc(v2): _132199>=10
cutting step 6 at pc(v2)
cutting step 5 at pc(v3)
cutting step 4 at pc(v3)
cutting step 3 at pc(v4)
cutting step 2 at pc(v4)
cutting step 1 at pc(v1)




--------------------------------------------------
abstraction refinement iteration 8:
lfp iteration 0 1 2 3 4 5 6 7 8 
abstract counterexample: stem [0,tid([6])], loop [tid([1]),tid([7]),tid([2]),tid([8]),tid([3]),tid([11]),tid([4]),tid([9])]
trans preds: _301180->_301183:	#17:	y'-y=< -9, x'+2/9*y'-2/9*y=<0, x'+1/2*y'-1/2*y=< -5/2, x'-1/5*y=<0, y>=10, 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
projected loop:
x'=2, y'=1, x=0, y=1, t=9, t'>0
x>=1
x'-x=<1
refining loop
cutting step 8 at pc(v1)
LI at pc(v1): x=<0
cutting step 7 at pc(v2)
LI at pc(v2): x=<0
cutting step 6 at pc(v2)
LI at pc(v2): x=<0
cutting step 5 at pc(v3)
LI at pc(v3): x=<0
cutting step 4 at pc(v3)
LI at pc(v3): x=<0
cutting step 3 at pc(v4)
LI at pc(v4): x=<0
cutting step 2 at pc(v4)
LI at pc(v4): x=<0
cutting step 1 at pc(v1)
LI at pc(v1): x'-x>=2

refining stem

cutting step 9 at pc(v1)
LI at pc(v1): x'=<0
cutting step 8 at pc(v1)
LI at pc(v1): _294937=<0
cutting step 7 at pc(v2)
cutting step 6 at pc(v2)
cutting step 5 at pc(v3)
cutting step 4 at pc(v3)
cutting step 3 at pc(v4)
cutting step 2 at pc(v4)
cutting step 1 at pc(v1)

refining loop
cutting step 8 at pc(v1)
LI at pc(v1): x=<0
cutting step 7 at pc(v2)
LI at pc(v2): x=<0
cutting step 6 at pc(v2)
LI at pc(v2): x=<0
cutting step 5 at pc(v3)
LI at pc(v3): x=<0
cutting step 4 at pc(v3)
LI at pc(v3): x=<0
cutting step 3 at pc(v4)
LI at pc(v4): x=<0
cutting step 2 at pc(v4)
LI at pc(v4): x=<0
cutting step 1 at pc(v1)
LI at pc(v1): x=<0

refining stem

cutting step 9 at pc(v1)
LI at pc(v1): x'=<0
cutting step 8 at pc(v1)
LI at pc(v1): _294908=<0
cutting step 7 at pc(v2)
cutting step 6 at pc(v2)
cutting step 5 at pc(v3)
cutting step 4 at pc(v3)
cutting step 3 at pc(v4)
cutting step 2 at pc(v4)
cutting step 1 at pc(v1)




--------------------------------------------------
abstraction refinement iteration 9:
lfp iteration 0 1 2 3 4 5 6 7 8 9 
abstract counterexample: stem [0,tid([6]),tid([1])], loop [tid([7]),tid([2]),tid([8]),tid([3]),tid([11]),tid([4]),tid([9]),tid([1])]
trans preds: _663218->_663221:	#19:	x'-x>=2, x=<0, y'-y=< -9, x'+2/9*y'-2/9*y=<0, x'+1/2*y'-1/2*y=< -5/2, x'-1/5*y=<0, y>=10, 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
projected loop:
x=9, y=10, t'>0, x'=1+y', y'>1, y'=<10, t>0
x-y>=0
x'-y'-x+y=<1
refining loop
cutting step 8 at pc(v2)
LI at pc(v2): x'-y'-10*x+10*y>=0
cutting step 7 at pc(v2)
LI at pc(v2): y'+12*x-12*y=<0
cutting step 6 at pc(v3)
LI at pc(v3): y'+12*x-12*y=<0
cutting step 5 at pc(v3)
LI at pc(v3): y'+12*x-12*y=<0
cutting step 4 at pc(v4)
LI at pc(v4): x'+1/2*y'+1/2*x-1/2*y=<2
cutting step 3 at pc(v4)
LI at pc(v4): x'+1/2*y'+1/2*x-1/2*y=<2
cutting step 2 at pc(v1)
LI at pc(v1): x'-y'-x+y>=2
cutting step 1 at pc(v1)
LI at pc(v1): x'-y'-x+y>=2

refining stem

cutting step 10 at pc(v1)
LI at pc(v1): x'-y'=< -1
cutting step 9 at pc(v1)
LI at pc(v1): x'-9/10*y'=<0
cutting step 8 at pc(v2)
LI at pc(v2): x'-y'-10*_500051+10*_500052>=0
cutting step 7 at pc(v2)
cutting step 6 at pc(v3)
cutting step 5 at pc(v3)
cutting step 4 at pc(v4)
cutting step 3 at pc(v4)
cutting step 2 at pc(v1)
cutting step 1 at pc(v1)

refining loop
cutting step 8 at pc(v2)
LI at pc(v2): x'-y'-10*x+10*y>=0
cutting step 7 at pc(v2)
LI at pc(v2): y'+12*x-12*y=<0
cutting step 6 at pc(v3)
LI at pc(v3): y'+12*x-12*y=<0
cutting step 5 at pc(v3)
LI at pc(v3): y'+12*x-12*y=<0
cutting step 4 at pc(v4)
LI at pc(v4): x-y=< -1
cutting step 3 at pc(v4)
LI at pc(v4): x'+2*x-2*y=<0
cutting step 2 at pc(v1)
LI at pc(v1): x-y=< -1
cutting step 1 at pc(v1)
LI at pc(v1): x-y=< -1

refining stem

cutting step 10 at pc(v1)
LI at pc(v1): x'-y'=< -1
cutting step 9 at pc(v1)
LI at pc(v1): x'-9/10*y'=<0
cutting step 8 at pc(v2)
LI at pc(v2): x'-y'-10*_500022+10*_500023>=0
cutting step 7 at pc(v2)
cutting step 6 at pc(v3)
cutting step 5 at pc(v3)
cutting step 4 at pc(v4)
cutting step 3 at pc(v4)
cutting step 2 at pc(v1)
cutting step 1 at pc(v1)




--------------------------------------------------
abstraction refinement iteration 10:
lfp iteration 0 1 2 3 4 5 6 7 8 9 10 
abstract counterexample: stem [0,tid([6]),tid([1]),tid([7]),tid([2]),tid([8]),tid([3]),tid([11]),tid([4]),tid([9]),tid([10])], loop [tid([5])]
trans preds: _1029573->_1029576:	#27:	x'+2*x-2*y=<0, x-y=< -1, x'-9/10*y'=<0, x'-y'=< -1, x'-y'-x+y>=2, x'+1/2*y'+1/2*x-1/2*y=<2, y'+12*x-12*y=<0, x'-y'-10*x+10*y>=0, x'-x>=2, x=<0, y'-y=< -9, x'+2/9*y'-2/9*y=<0, x'+1/2*y'-1/2*y=< -5/2, x'-1/5*y=<0, y>=10, 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
projected loop infeasible:
1=1
1=1
refining stem

cutting step 9 at pc(v1)
unsat suffix not yet reached
cutting step 8 at pc(v1)
unsat suffix not yet reached
cutting step 7 at pc(v2)
unsat suffix not yet reached
cutting step 6 at pc(v2)
unsat suffix not yet reached
cutting step 5 at pc(v3)
unsat suffix not yet reached
cutting step 4 at pc(v3)
unsat suffix not yet reached
cutting step 3 at pc(v4)
LI at pc(v4): x'+1/2*y'>=5/2
cutting step 2 at pc(v4)
LI at pc(v4): x'-2*y'=<0
cutting step 1 at pc(v1)
LI at pc(v1): y'>=1

refining stem

cutting step 9 at pc(v1)
unsat suffix not yet reached
cutting step 8 at pc(v1)
unsat suffix not yet reached
cutting step 7 at pc(v2)
unsat suffix not yet reached
cutting step 6 at pc(v2)
unsat suffix not yet reached
cutting step 5 at pc(v3)
unsat suffix not yet reached
cutting step 4 at pc(v3)
unsat suffix not yet reached
cutting step 3 at pc(v4)
LI at pc(v4): x'+1/2*y'>=5/2
cutting step 2 at pc(v4)
LI at pc(v4): x'-2*y'=<0
cutting step 1 at pc(v1)
LI at pc(v1): y'>=1




--------------------------------------------------
abstraction refinement iteration 11:
lfp iteration 0 1 2 3 4 5 6 7 8 9 10 
abstract counterexample: stem [0,tid([6]),tid([1]),tid([7]),tid([2])], loop [tid([8]),tid([3]),tid([11]),tid([4]),tid([9]),tid([7]),tid([2])]
trans preds: _928648->_928651:	#29:	x'-2*y'=<0, x'+1/2*y'>=5/2, x'+2*x-2*y=<0, x-y=< -1, x'-9/10*y'=<0, x'-y'=< -1, x'-y'-x+y>=2, x'+1/2*y'+1/2*x-1/2*y=<2, y'+12*x-12*y=<0, x'-y'-10*x+10*y>=0, x'-x>=2, x=<0, y'-y=< -9, x'+2/9*y'-2/9*y=<0, x'+1/2*y'-1/2*y=< -5/2, x'-1/5*y=<0, y>=10, 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 5 at pc(v3)
unsat suffix not yet reached
cutting step 4 at pc(v3)
unsat suffix not yet reached
cutting step 3 at pc(v4)
LI at pc(v4): y'=<5
cutting step 2 at pc(v4)
LI at pc(v4): y'=<5
cutting step 1 at pc(v1)
LI at pc(v1): y'=<1

refining stem

cutting step 9 at pc(v1)
unsat suffix not yet reached
cutting step 8 at pc(v1)
unsat suffix not yet reached
cutting step 7 at pc(v2)
unsat suffix not yet reached
cutting step 6 at pc(v2)
unsat suffix not yet reached
cutting step 5 at pc(v3)
unsat suffix not yet reached
cutting step 4 at pc(v3)
unsat suffix not yet reached
cutting step 3 at pc(v4)
LI at pc(v4): y'=<5
cutting step 2 at pc(v4)
LI at pc(v4): y'=<5
cutting step 1 at pc(v1)
LI at pc(v1): y'=<1

refining loop
cutting step 5 at pc(v3)
unsat suffix not yet reached
cutting step 4 at pc(v3)
unsat suffix not yet reached
cutting step 3 at pc(v4)
LI at pc(v4): y'=<5
cutting step 2 at pc(v4)
LI at pc(v4): y'=<5
cutting step 1 at pc(v1)
LI at pc(v1): y'=<1

refining stem

cutting step 9 at pc(v1)
unsat suffix not yet reached
cutting step 8 at pc(v1)
unsat suffix not yet reached
cutting step 7 at pc(v2)
unsat suffix not yet reached
cutting step 6 at pc(v2)
unsat suffix not yet reached
cutting step 5 at pc(v3)
unsat suffix not yet reached
cutting step 4 at pc(v3)
unsat suffix not yet reached
cutting step 3 at pc(v4)
LI at pc(v4): y'=<5
cutting step 2 at pc(v4)
LI at pc(v4): y'=<5
cutting step 1 at pc(v1)
LI at pc(v1): y'=<1




--------------------------------------------------
abstraction refinement iteration 12:
lfp iteration 0 1 2 3 4 5 6 7 8 9 10 
abstract counterexample: stem [0,tid([6]),tid([1]),tid([7])], loop [tid([2]),tid([8]),tid([3]),tid([11]),tid([4]),tid([9]),tid([1]),tid([7])]
trans preds: _1092654->_1092657:	#30:	y'=<5, x'-2*y'=<0, x'+1/2*y'>=5/2, x'+2*x-2*y=<0, x-y=< -1, x'-9/10*y'=<0, x'-y'=< -1, x'-y'-x+y>=2, x'+1/2*y'+1/2*x-1/2*y=<2, y'+12*x-12*y=<0, x'-y'-10*x+10*y>=0, x'-x>=2, x=<0, y'-y=< -9, x'+2/9*y'-2/9*y=<0, x'+1/2*y'-1/2*y=< -5/2, x'-1/5*y=<0, y>=10, 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
projected loop:
x'=0, y'=10, x=0, y=10, t=2, t'>0



==================================================
ARMC-Live: cannot find rank:
	stem [0,tid([6]),tid([1]),tid([7])]
	loop [tid([2]),tid([8]),tid([3]),tid([11]),tid([4]),tid([9]),tid([1]),tid([7])]
Stem:
0:	unknown
6:	unknown
1:	unknown
7:	unknown
Loop:
2:	unknown
8:	unknown
3:	unknown
11:	unknown
4:	unknown
9:	unknown
1:	unknown
7:	unknown
halt
Time on instantiating uf axioms:		run 0.00,	 wall 0.00 s.
Time on cli constraint solving:		run 0.38,	 wall 1.01 s.
Time on cli constraint preparation:		run 0.07,	 wall 0.12 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.07,	 wall 0.05 s.
Time on refinement preprocessing cut:		run 0.00,	 wall 0.00 s.
Time on refinement cutting trace:		run 1.07,	 wall 1.84 s.
Time on refinement finding unsat subtrace:		run 0.00,	 wall 0.00 s.
Time on refinement:		run 1.17,	 wall 2.05 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.15,	 wall 0.15 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:30 2014
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			4.74 seconds
[runlim] time:			3.43 seconds
[runlim] space:			16.7 MB
[runlim] samples:		39