[runlim] version:		1.7
[runlim] time limit:		3600 seconds
[runlim] real time limit:	311040000 seconds
[runlim] space limit:		4294967069 MB
[runlim] argv[0]:		./armc
[runlim] argv[1]:		Motor10R.armc
[runlim] start:			Sat Nov 29 18:13:30 2014
[runlim] main pid:		10901
ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [Motor10R.armc]
reading input from Motor10R.armc...done.



--------------------------------------------------
abstraction refinement iteration 0:
predicates:
pc(_4763):	#0:	
lfp iteration 0 1 2 
abstract_check at refinement step 0 completed in 30 msec

counterexample is spurious
refining abstraction...
cex: 15 13 12 0 
Refining 12
Pivot Node : 2
RevSuffix [2-13-3,1-12-2]
LI at pc(v_1):x_1-x_2>=5
preds(p(_,data(A,B,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1)]).




--------------------------------------------------
abstraction refinement iteration 1:
predicates:
_131798:	#1:	x_1-x_2>=5
lfp iteration 0 1 2 3 
abstract_check at refinement step 1 completed in 60 msec

counterexample is spurious
refining abstraction...
cex: 15 13 1 12 0 
Refining 21
Pivot Node : 12
RevSuffix [12-15-21,3-13-12]
LI at pc(v_2):x_1-x_2>=2
preds(p(_,data(A,B,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1)]).




--------------------------------------------------
abstraction refinement iteration 2:
predicates:
_159677:	#2:	x_1-x_2>=5, x_1-x_2>=2
lfp iteration 0 1 2 3 
abstract_check at refinement step 2 completed in 70 msec

counterexample is spurious
refining abstraction...
cex: 18 16 1 12 0 
Refining 21
Pivot Node : 13
RevSuffix [13-18-21,3-16-13]
LI at pc(v_3):x_2-x_3>=2
preds(p(_,data(A,B,C,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1)]).




--------------------------------------------------
abstraction refinement iteration 3:
predicates:
_418812:	#3:	x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2
lfp iteration 0 1 2 3 
abstract_check at refinement step 3 completed in 70 msec

counterexample is spurious
refining abstraction...
cex: 21 19 1 12 0 
Refining 21
Pivot Node : 14
RevSuffix [14-21-21,3-19-14]
LI at pc(v_4):x_3-x_4>=2
preds(p(_,data(A,B,C,D,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1)]).




--------------------------------------------------
abstraction refinement iteration 4:
predicates:
_286494:	#4:	x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2
lfp iteration 0 1 2 3 
abstract_check at refinement step 4 completed in 80 msec

counterexample is spurious
refining abstraction...
cex: 24 22 1 12 0 
Refining 22
Pivot Node : 15
RevSuffix [15-24-22,3-22-15]
LI at pc(v_5):x_4-x_5>=2
preds(p(_,data(A,B,C,D,E,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1)]).




--------------------------------------------------
abstraction refinement iteration 5:
predicates:
_205349:	#5:	x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2
lfp iteration 0 1 2 3 
abstract_check at refinement step 5 completed in 80 msec

counterexample is spurious
refining abstraction...
cex: 27 25 1 12 0 
Refining 23
Pivot Node : 16
RevSuffix [16-27-23,3-25-16]
LI at pc(v_6):x_5-x_6>=2
preds(p(_,data(A,B,C,D,E,F,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1)]).




--------------------------------------------------
abstraction refinement iteration 6:
predicates:
_443320:	#6:	x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2
lfp iteration 0 1 2 3 
abstract_check at refinement step 6 completed in 70 msec

counterexample is spurious
refining abstraction...
cex: 30 28 1 12 0 
Refining 24
Pivot Node : 17
RevSuffix [17-30-24,3-28-17]
LI at pc(v_7):x_6-x_7>=2
preds(p(_,data(A,B,C,D,E,F,G,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1)]).




--------------------------------------------------
abstraction refinement iteration 7:
predicates:
_330699:	#7:	x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2
lfp iteration 0 1 2 3 
abstract_check at refinement step 7 completed in 90 msec

counterexample is spurious
refining abstraction...
cex: 33 31 1 12 0 
Refining 25
Pivot Node : 18
RevSuffix [18-33-25,3-31-18]
LI at pc(v_8):x_7-x_8>=2
preds(p(_,data(A,B,C,D,E,F,G,H,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1)]).




--------------------------------------------------
abstraction refinement iteration 8:
predicates:
_271147:	#8:	x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2
lfp iteration 0 1 2 3 
abstract_check at refinement step 8 completed in 100 msec

counterexample is spurious
refining abstraction...
cex: 36 34 1 12 0 
Refining 26
Pivot Node : 19
RevSuffix [19-36-26,3-34-19]
LI at pc(v_9):x_8-x_9>=2
preds(p(_,data(A,B,C,D,E,F,G,H,I,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1)]).




--------------------------------------------------
abstraction refinement iteration 9:
predicates:
_270185:	#9:	x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2
lfp iteration 0 1 2 3 
abstract_check at refinement step 9 completed in 90 msec

counterexample is spurious
refining abstraction...
cex: 39 37 1 12 0 
Refining 27
Pivot Node : 20
RevSuffix [20-39-27,3-37-20]
LI at pc(v_10):x_9-x_10>=2
preds(p(_,data(A,B,C,D,E,F,G,H,I,J,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1)]).




--------------------------------------------------
abstraction refinement iteration 10:
predicates:
_502192:	#10:	x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2
lfp iteration 0 1 2 3 4 5 Number of interpolation queries:	10.
Number of entailment checks during fixpoint checking:	0.
Number of entailment checks that could be saved:	0.
Number of entailment checks for abstraction:	2,035.

abstract_check at refinement step 10 completed in 160 msec



==================================================
ARMC: program is correct

abstract fixpoint
abstract_state(1, pc(v_0), []).
abstract_state(3, pc(v_1), [2,3,4,5,6,7,8,9,10]).
abstract_state(19, pc(v_9), [2,3,4,5,6,7,8,9,10]).
abstract_state(20, pc(v_10), [2,3,4,5,6,7,8,9,10]).
abstract_state(21, pc(v_2), [2,3]).
abstract_state(22, pc(v_3), [2,3,4]).
abstract_state(23, pc(v_4), [2,3,4,5]).
abstract_state(24, pc(v_5), [2,3,4,5,6]).
abstract_state(25, pc(v_6), [2,3,4,5,6,7]).
abstract_state(26, pc(v_7), [2,3,4,5,6,7,8]).
abstract_state(27, pc(v_8), [2,3,4,5,6,7,8,9]).

frontier 0: 1 pc(v_0) from 0 by appying 0: 	T
frontier 2: 3 pc(v_1) from 2 by appying 1: 	x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2
frontier 3: 19 pc(v_9) from 3 by appying 34: 	x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2
frontier 3: 20 pc(v_10) from 3 by appying 37: 	x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2
frontier 4: 21 pc(v_2) from 12 by appying 2: 	x_1-x_2>=2, x_2-x_3>=2
frontier 4: 22 pc(v_3) from 13 by appying 3: 	x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2
frontier 4: 23 pc(v_4) from 14 by appying 4: 	x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2
frontier 4: 24 pc(v_5) from 15 by appying 5: 	x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2
frontier 4: 25 pc(v_6) from 16 by appying 6: 	x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2
frontier 4: 26 pc(v_7) from 17 by appying 7: 	x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2
frontier 4: 27 pc(v_8) from 18 by appying 8: 	x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2

_505232:	#10:	x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2

==================================================
verifying fixpoint...done.
pc(v_0): [[]]
pc(v_1): [[2,3,4,5,6,7,8,9,10]]
pc(v_10): [[2,3,4,5,6,7,8,9,10]]
pc(v_2): [[2,3]]
pc(v_3): [[2,3,4]]
pc(v_4): [[2,3,4,5]]
pc(v_5): [[2,3,4,5,6]]
pc(v_6): [[2,3,4,5,6,7]]
pc(v_7): [[2,3,4,5,6,7,8]]
pc(v_8): [[2,3,4,5,6,7,8,9]]
pc(v_9): [[2,3,4,5,6,7,8,9,10]]
Time on instantiating uf axioms:		run 0.00,	 wall 0.00 s.
Time on cli constraint solving:		run 0.22,	 wall 0.29 s.
Time on cli constraint preparation:		run 0.00,	 wall 0.01 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.01 s.
Time on refinement preprocessing cut:		run 0.10,	 wall 0.06 s.
Time on refinement cutting trace:		run 0.33,	 wall 0.37 s.
Time on refinement finding unsat subtrace:		run 0.07,	 wall 0.09 s.
Time on refinement:		run 0.40,	 wall 0.46 s.
Time on concrete postcondition operator:		run 0.00,	 wall 0.00 s.
Time on fixpoint abstraction:		run 0.17,	 wall 0.29 s.
Time on fixpoint test:		run 0.00,	 wall 0.02 s.
Time on abstract check:		run 0.75,	 wall 0.79 s.
Time on total including result checking:		run 1.39,	 wall 1.56 s.
Time on check result:		run 0.06,	 wall 0.09 s.
Time on total:		run 1.33,	 wall 1.47 s.
Number of interpolation queries:	10.
Number of entailment checks during fixpoint checking:	11.
Number of entailment checks that could be saved:	0.
Number of entailment checks for abstraction:	2,035.



==================================================
ARMC: program is correct

preds(p(_,data(A,B,C,D,E,F,G,H,I,J,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1)]).


System information
Variables: 11
Transitions: 39
Locations: 12

Analysis information
Predicates: 10
Reachable abstract states: 27
Abstraction refinement iterations: 10
[runlim] end:			Sat Nov 29 18:13:32 2014
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			2.05 seconds
[runlim] time:			1.59 seconds
[runlim] space:			13.0 MB
[runlim] samples:		16