[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]: Motor30R.armc [runlim] start: Sat Nov 29 18:13:48 2014 [runlim] main pid: 17633 ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008) rybal@mpi-sws.mpg.de cmd line: [Motor30R.armc] reading input from Motor30R.armc...done. -------------------------------------------------- abstraction refinement iteration 0: predicates: pc(_5503): #0: lfp iteration 0 1 2 abstract_check at refinement step 0 completed in 410 msec counterexample is spurious refining abstraction... cex: 35 33 32 0 Refining 32 Pivot Node : 2 RevSuffix [2-33-3,1-32-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: _674537: #1: x_1-x_2>=5 lfp iteration 0 1 2 3 abstract_check at refinement step 1 completed in 720 msec counterexample is spurious refining abstraction... cex: 35 33 1 32 0 Refining 61 Pivot Node : 32 RevSuffix [32-35-61,3-33-32] 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: _606263: #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 860 msec counterexample is spurious refining abstraction... cex: 38 36 1 32 0 Refining 61 Pivot Node : 33 RevSuffix [33-38-61,3-36-33] 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: _327983: #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 910 msec counterexample is spurious refining abstraction... cex: 41 39 1 32 0 Refining 61 Pivot Node : 34 RevSuffix [34-41-61,3-39-34] 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: _361333: #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 950 msec counterexample is spurious refining abstraction... cex: 44 42 1 32 0 Refining 62 Pivot Node : 35 RevSuffix [35-44-62,3-42-35] 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: _700463: #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 990 msec counterexample is spurious refining abstraction... cex: 47 45 1 32 0 Refining 63 Pivot Node : 36 RevSuffix [36-47-63,3-45-36] [runlim] sample: 10.0 seconds, 18.7 MB 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: _735587: #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 1040 msec counterexample is spurious refining abstraction... cex: 50 48 1 32 0 Refining 64 Pivot Node : 37 RevSuffix [37-50-64,3-48-37] 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: _775388: #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 1090 msec counterexample is spurious refining abstraction... cex: 53 51 1 32 0 Refining 65 Pivot Node : 38 RevSuffix [38-53-65,3-51-38] 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: _814774: #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 1130 msec counterexample is spurious refining abstraction... cex: 56 54 1 32 0 Refining 66 Pivot Node : 39 RevSuffix [39-56-66,3-54-39] 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: _920505: #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 1160 msec counterexample is spurious refining abstraction... cex: 59 57 1 32 0 Refining 67 Pivot Node : 40 RevSuffix [40-59-67,3-57-40] 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: _878781: #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 [runlim] sample: 20.0 seconds, 18.7 MB abstract_check at refinement step 10 completed in 1200 msec counterexample is spurious refining abstraction... cex: 62 60 1 32 0 Refining 68 Pivot Node : 41 RevSuffix [41-62-68,3-60-41] LI at pc(v_11):x_10-x_11>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 11: predicates: _1061663: #11: 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, x_10-x_11>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 11 completed in 1250 msec counterexample is spurious refining abstraction... cex: 65 63 1 32 0 Refining 69 Pivot Node : 42 RevSuffix [42-65-69,3-63-42] LI at pc(v_12):x_11-x_12>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 12: predicates: _661597: #12: 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, x_10-x_11>=2, x_11-x_12>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 12 completed in 1280 msec counterexample is spurious refining abstraction... cex: 68 66 1 32 0 Refining 70 Pivot Node : 43 RevSuffix [43-68-70,3-66-43] LI at pc(v_13):x_12-x_13>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 13: predicates: _839706: #13: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 13 completed in 1320 msec counterexample is spurious refining abstraction... cex: 71 69 1 32 0 Refining 71 Pivot Node : 44 RevSuffix [44-71-71,3-69-44] LI at pc(v_14):x_13-x_14>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 14: predicates: _1040053: #14: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 14 completed in 1350 msec counterexample is spurious refining abstraction... cex: 74 72 1 32 0 Refining 72 Pivot Node : 45 RevSuffix [45-74-72,3-72-45] [runlim] sample: 30.0 seconds, 18.7 MB LI at pc(v_15):x_14-x_15>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 15: predicates: _1088724: #15: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 15 completed in 1400 msec counterexample is spurious refining abstraction... cex: 77 75 1 32 0 Refining 73 Pivot Node : 46 RevSuffix [46-77-73,3-75-46] LI at pc(v_16):x_15-x_16>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 16: predicates: _957666: #16: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 16 completed in 1430 msec counterexample is spurious refining abstraction... cex: 80 78 1 32 0 Refining 74 Pivot Node : 47 RevSuffix [47-80-74,3-78-47] LI at pc(v_17):x_16-x_17>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 17: predicates: _889703: #17: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 17 completed in 1460 msec counterexample is spurious refining abstraction... cex: 83 81 1 32 0 Refining 75 Pivot Node : 48 RevSuffix [48-83-75,3-81-48] LI at pc(v_18):x_17-x_18>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,_,_,_,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 18: predicates: _1183754: #18: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 18 completed in 1480 msec counterexample is spurious refining abstraction... cex: 86 84 1 32 0 Refining 76 Pivot Node : 49 RevSuffix [49-86-76,3-84-49] [runlim] sample: 40.0 seconds, 18.7 MB LI at pc(v_19):x_18-x_19>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,_,_,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 19: predicates: _1196936: #19: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 19 completed in 1520 msec counterexample is spurious refining abstraction... cex: 89 87 1 32 0 Refining 77 Pivot Node : 50 RevSuffix [50-89-77,3-87-50] LI at pc(v_20):x_19-x_20>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,_,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 20: predicates: _1029327: #20: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 20 completed in 1560 msec counterexample is spurious refining abstraction... cex: 92 90 1 32 0 Refining 78 Pivot Node : 51 RevSuffix [51-92-78,3-90-51] LI at pc(v_21):x_20-x_21>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,_,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 21: predicates: _1163211: #21: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 21 completed in 1590 msec counterexample is spurious refining abstraction... cex: 95 93 1 32 0 Refining 79 Pivot Node : 52 RevSuffix [52-95-79,3-93-52] LI at pc(v_22):x_21-x_22>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,_,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 22: predicates: _1328412: #22: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2 lfp iteration 0 1 2 3 [runlim] sample: 50.0 seconds, 26.9 MB abstract_check at refinement step 22 completed in 1620 msec counterexample is spurious refining abstraction... cex: 98 96 1 32 0 Refining 80 Pivot Node : 53 RevSuffix [53-98-80,3-96-53] LI at pc(v_23):x_22-x_23>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,_,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 23: predicates: _1244738: #23: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 23 completed in 1650 msec counterexample is spurious refining abstraction... cex: 101 99 1 32 0 Refining 81 Pivot Node : 54 RevSuffix [54-101-81,3-99-54] LI at pc(v_24):x_23-x_24>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,_,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 24: predicates: _1612388: #24: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 24 completed in 1680 msec counterexample is spurious refining abstraction... cex: 104 102 1 32 0 Refining 82 Pivot Node : 55 RevSuffix [55-104-82,3-102-55] LI at pc(v_25):x_24-x_25>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,_,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 25: predicates: _1565989: #25: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 25 completed in 1710 msec counterexample is spurious refining abstraction... cex: 107 105 1 32 0 Refining 83 Pivot Node : 56 RevSuffix [56-107-83,3-105-56] LI at pc(v_26):x_25-x_26>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,_,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 26: predicates: _1694748: #26: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2 lfp iteration 0 1 2 3 [runlim] sample: 60.0 seconds, 26.9 MB abstract_check at refinement step 26 completed in 1730 msec counterexample is spurious refining abstraction... cex: 110 108 1 32 0 Refining 84 Pivot Node : 57 RevSuffix [57-110-84,3-108-57] LI at pc(v_27):x_26-x_27>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,_,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 27: predicates: _1947692: #27: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 27 completed in 1730 msec counterexample is spurious refining abstraction... cex: 113 111 1 32 0 Refining 85 Pivot Node : 58 RevSuffix [58-113-85,3-111-58] LI at pc(v_28):x_27-x_28>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,_,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 28: predicates: _1904775: #28: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 28 completed in 1770 msec counterexample is spurious refining abstraction... cex: 116 114 1 32 0 Refining 86 Pivot Node : 59 RevSuffix [59-116-86,3-114-59] LI at pc(v_29):x_28-x_29>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,_,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 29: predicates: _1828262: #29: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 29 completed in 1800 msec counterexample is spurious refining abstraction... cex: 119 117 1 32 0 Refining 87 Pivot Node : 60 RevSuffix [60-119-87,3-117-60] [runlim] sample: 70.0 seconds, 26.9 MB LI at pc(v_30):x_29-x_30>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 30: predicates: _1440731: #30: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2 lfp iteration 0 1 2 3 4 5 Number of interpolation queries: 30. Number of entailment checks during fixpoint checking: 0. Number of entailment checks that could be saved: 0. Number of entailment checks for abstraction: 48,805. abstract_check at refinement step 30 completed in 5000 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,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]). abstract_state(59, pc(v_29), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]). abstract_state(60, pc(v_30), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]). abstract_state(61, pc(v_2), [2,3]). abstract_state(62, pc(v_3), [2,3,4]). abstract_state(63, pc(v_4), [2,3,4,5]). abstract_state(64, pc(v_5), [2,3,4,5,6]). abstract_state(65, pc(v_6), [2,3,4,5,6,7]). abstract_state(66, pc(v_7), [2,3,4,5,6,7,8]). abstract_state(67, pc(v_8), [2,3,4,5,6,7,8,9]). abstract_state(68, pc(v_9), [2,3,4,5,6,7,8,9,10]). abstract_state(69, pc(v_10), [2,3,4,5,6,7,8,9,10,11]). abstract_state(70, pc(v_11), [2,3,4,5,6,7,8,9,10,11,12]). abstract_state(71, pc(v_12), [2,3,4,5,6,7,8,9,10,11,12,13]). abstract_state(72, pc(v_13), [2,3,4,5,6,7,8,9,10,11,12,13,14]). abstract_state(73, pc(v_14), [2,3,4,5,6,7,8,9,10,11,12,13,14,15]). abstract_state(74, pc(v_15), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]). abstract_state(75, pc(v_16), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17]). abstract_state(76, pc(v_17), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18]). abstract_state(77, pc(v_18), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19]). abstract_state(78, pc(v_19), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]). abstract_state(79, pc(v_20), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21]). abstract_state(80, pc(v_21), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22]). abstract_state(81, pc(v_22), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23]). abstract_state(82, pc(v_23), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24]). abstract_state(83, pc(v_24), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25]). abstract_state(84, pc(v_25), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]). abstract_state(85, pc(v_26), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27]). abstract_state(86, pc(v_27), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28]). abstract_state(87, pc(v_28), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29]). 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2 frontier 3: 59 pc(v_29) from 3 by appying 114: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2 frontier 3: 60 pc(v_30) from 3 by appying 117: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2 frontier 4: 61 pc(v_2) from 32 by appying 2: x_1-x_2>=2, x_2-x_3>=2 frontier 4: 62 pc(v_3) from 33 by appying 3: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2 frontier 4: 63 pc(v_4) from 34 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: 64 pc(v_5) from 35 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: 65 pc(v_6) from 36 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: 66 pc(v_7) from 37 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: 67 pc(v_8) from 38 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 frontier 4: 68 pc(v_9) from 39 by appying 9: 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: 69 pc(v_10) from 40 by appying 10: 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, x_10-x_11>=2 frontier 4: 70 pc(v_11) from 41 by appying 11: 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, x_10-x_11>=2, x_11-x_12>=2 frontier 4: 71 pc(v_12) from 42 by appying 12: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2 frontier 4: 72 pc(v_13) from 43 by appying 13: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2 frontier 4: 73 pc(v_14) from 44 by appying 14: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2 frontier 4: 74 pc(v_15) from 45 by appying 15: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2 frontier 4: 75 pc(v_16) from 46 by appying 16: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2 frontier 4: 76 pc(v_17) from 47 by appying 17: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2 frontier 4: 77 pc(v_18) from 48 by appying 18: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2 frontier 4: 78 pc(v_19) from 49 by appying 19: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2 frontier 4: 79 pc(v_20) from 50 by appying 20: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2 frontier 4: 80 pc(v_21) from 51 by appying 21: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2 frontier 4: 81 pc(v_22) from 52 by appying 22: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2 frontier 4: 82 pc(v_23) from 53 by appying 23: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2 frontier 4: 83 pc(v_24) from 54 by appying 24: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2 frontier 4: 84 pc(v_25) from 55 by appying 25: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2 frontier 4: 85 pc(v_26) from 56 by appying 26: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2 frontier 4: 86 pc(v_27) from 57 by appying 27: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2 frontier 4: 87 pc(v_28) from 58 by appying 28: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2 _1251427: #30: 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, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2 ================================================== verifying fixpoint...done. pc(v_0): [[]] pc(v_1): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]] pc(v_10): [[2,3,4,5,6,7,8,9,10,11]] pc(v_11): [[2,3,4,5,6,7,8,9,10,11,12]] pc(v_12): [[2,3,4,5,6,7,8,9,10,11,12,13]] pc(v_13): [[2,3,4,5,6,7,8,9,10,11,12,13,14]] pc(v_14): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15]] pc(v_15): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]] pc(v_16): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17]] pc(v_17): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18]] pc(v_18): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19]] pc(v_19): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]] pc(v_2): [[2,3]] pc(v_20): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21]] pc(v_21): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22]] pc(v_22): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23]] pc(v_23): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24]] pc(v_24): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25]] pc(v_25): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]] pc(v_26): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27]] pc(v_27): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28]] pc(v_28): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29]] pc(v_29): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]] pc(v_3): [[2,3,4]] pc(v_30): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]] 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 14.84, wall 26.52 s. Time on cli constraint preparation: run 0.04, wall 0.09 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.03, wall 0.04 s. Time on refinement preprocessing cut: run 1.30, wall 1.28 s. Time on refinement cutting trace: run 16.24, wall 27.98 s. Time on refinement finding unsat subtrace: run 0.79, wall 0.84 s. Time on refinement: run 17.08, wall 28.84 s. Time on concrete postcondition operator: run 0.00, wall 0.00 s. Time on fixpoint abstraction: run 14.29, wall 14.17 s. Time on fixpoint test: run 0.09, wall 0.06 s. Time on abstract check: run 40.03, wall 41.30 s. Time on total including result checking: run 63.51, wall 76.80 s. Time on check result: run 1.18, wall 1.30 s. Time on total: run 62.33, wall 75.50 s. Number of interpolation queries: 30. Number of entailment checks during fixpoint checking: 31. Number of entailment checks that could be saved: 0. Number of entailment checks for abstraction: 48,805. ================================================== ARMC: program is correct preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,_)), [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),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1)]). System information Variables: 31 Transitions: 119 Locations: 32 Analysis information Predicates: 30 Reachable abstract states: 87 Abstraction refinement iterations: 30 [runlim] end: Sat Nov 29 18:15:05 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 77.53 seconds [runlim] time: 77.05 seconds [runlim] space: 26.9 MB [runlim] samples: 771