[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]: Motor5R.armc [runlim] start: Sat Nov 29 18:13:30 2014 [runlim] main pid: 9903 ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008) rybal@mpi-sws.mpg.de cmd line: [Motor5R.armc] reading input from Motor5R.armc...done. -------------------------------------------------- abstraction refinement iteration 0: predicates: pc(_4576): #0: lfp iteration 0 1 2 abstract_check at refinement step 0 completed in 20 msec counterexample is spurious refining abstraction... cex: 16 8 7 0 Refining 7 Pivot Node : 2 RevSuffix [2-8-3,1-7-2] LI at pc(v1):x3-x4>=5 preds(p(_,data(_,_,A,B,_,_)), [A-B>=rat(5,1)]). -------------------------------------------------- abstraction refinement iteration 1: predicates: _44945: #1: x3-x4>=5 lfp iteration 0 1 2 3 abstract_check at refinement step 1 completed in 10 msec counterexample is spurious refining abstraction... cex: 16 8 4 7 0 Refining 11 Pivot Node : 7 RevSuffix [7-16-11,3-8-7] LI at pc(v4):x3-x4>=2 preds(p(_,data(_,_,A,B,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 2: predicates: _113755: #2: x3-x4>=5, x3-x4>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 2 completed in 20 msec counterexample is spurious refining abstraction... cex: 15 10 4 7 0 Refining 11 Pivot Node : 8 RevSuffix [8-15-11,3-10-8] LI at pc(v3):x2-x3>=2 preds(p(_,data(_,A,B,C,_,_)), [B-C>=rat(5,1),B-C>=rat(2,1),A-B>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 3: predicates: _183141: #3: x3-x4>=5, x3-x4>=2, x2-x3>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 3 completed in 0 msec counterexample is spurious refining abstraction... cex: 14 12 4 7 0 Refining 12 Pivot Node : 9 RevSuffix [9-14-12,3-12-9] LI at pc(v2):x1-x2>=2 preds(p(_,data(A,B,C,D,_,_)), [C-D>=rat(5,1),C-D>=rat(2,1),B-C>=rat(2,1),A-B>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 4: predicates: _253679: #4: x3-x4>=5, x3-x4>=2, x2-x3>=2, x1-x2>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 4 completed in 20 msec counterexample is spurious refining abstraction... cex: 18 19 4 7 0 Refining 12 Pivot Node : 10 RevSuffix [10-18-12,3-19-10] LI at pc(v5):x4-x5>=2 preds(p(_,data(A,B,C,D,E,_)), [C-D>=rat(5,1),C-D>=rat(2,1),B-C>=rat(2,1),A-B>=rat(2,1),D-E>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 5: predicates: _58617: #5: x3-x4>=5, x3-x4>=2, x2-x3>=2, x1-x2>=2, x4-x5>=2 lfp iteration 0 1 2 3 4 5 Number of interpolation queries: 5. Number of entailment checks during fixpoint checking: 0. Number of entailment checks that could be saved: 0. Number of entailment checks for abstraction: 280. abstract_check at refinement step 5 completed in 30 msec ================================================== ARMC: program is correct abstract fixpoint abstract_state(1, pc(v0), []). abstract_state(3, pc(v1), [2,3,4,5]). abstract_state(7, pc(v4), [2,3,4,5]). abstract_state(10, pc(v5), [2,3,4,5]). abstract_state(11, pc(v3), [2,3,4]). abstract_state(12, pc(v2), [3,4]). frontier 0: 1 pc(v0) from 0 by appying 0: T frontier 2: 3 pc(v1) from 2 by appying 4: x3-x4>=2, x2-x3>=2, x1-x2>=2, x4-x5>=2 frontier 3: 7 pc(v4) from 3 by appying 8: x3-x4>=2, x2-x3>=2, x1-x2>=2, x4-x5>=2 frontier 3: 10 pc(v5) from 3 by appying 19: x3-x4>=2, x2-x3>=2, x1-x2>=2, x4-x5>=2 frontier 4: 11 pc(v3) from 8 by appying 5: x3-x4>=2, x2-x3>=2, x1-x2>=2 frontier 4: 12 pc(v2) from 9 by appying 2: x2-x3>=2, x1-x2>=2 _61497: #5: x3-x4>=5, x3-x4>=2, x2-x3>=2, x1-x2>=2, x4-x5>=2 ================================================== verifying fixpoint...done. pc(v0): [[]] pc(v1): [[2,3,4,5]] pc(v2): [[3,4]] pc(v3): [[2,3,4]] pc(v4): [[2,3,4,5]] pc(v5): [[2,3,4,5]] Time on instantiating uf axioms: run 0.00, wall 0.00 s. Time on cli constraint solving: run 0.02, wall 0.04 s. Time on cli constraint preparation: run 0.00, wall 0.00 s. Time on cli matrix parsing: run 0.00, wall 0.00 s. Time on cli preprocessing: run 0.00, wall 0.00 s. Time on computing the subsumer subtree: run 0.00, wall 0.00 s. Time on finding the location of subsumer in queue: run 0.00, wall 0.00 s. Time on asserting thick transitions: run 0.00, wall 0.00 s. Time on path invariant generation: run 0.00, wall 0.00 s. Time on new predicate selection: run 0.00, wall 0.00 s. Time on refinement preprocessing cut: run 0.02, wall 0.01 s. Time on refinement cutting trace: run 0.05, wall 0.05 s. Time on refinement finding unsat subtrace: run 0.01, wall 0.02 s. Time on refinement: run 0.06, wall 0.07 s. Time on concrete postcondition operator: run 0.00, wall 0.00 s. Time on fixpoint abstraction: run 0.01, wall 0.03 s. Time on fixpoint test: run 0.00, wall 0.00 s. Time on abstract check: run 0.09, wall 0.10 s. Time on total including result checking: run 0.22, wall 0.27 s. Time on check result: run 0.02, wall 0.03 s. Time on total: run 0.20, wall 0.24 s. Number of interpolation queries: 5. Number of entailment checks during fixpoint checking: 6. Number of entailment checks that could be saved: 0. Number of entailment checks for abstraction: 280. ================================================== ARMC: program is correct preds(p(_,data(A,B,C,D,E,_)), [C-D>=rat(5,1),C-D>=rat(2,1),B-C>=rat(2,1),A-B>=rat(2,1),D-E>=rat(2,1)]). System information Variables: 6 Transitions: 19 Locations: 7 Analysis information Predicates: 5 Reachable abstract states: 12 Abstraction refinement iterations: 5 [runlim] end: Sat Nov 29 18:13:30 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 0.42 seconds [runlim] time: 0.29 seconds [runlim] space: 7.4 MB [runlim] samples: 3