[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]: WLMR.armc [runlim] start: Sat Nov 29 18:13:28 2014 [runlim] main pid: 4353 ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008) rybal@mpi-sws.mpg.de cmd line: [WLMR.armc] reading input from WLMR.armc...done. -------------------------------------------------- abstraction refinement iteration 0: predicates: pc(_4481): #0: lfp iteration 0 1 abstract_check at refinement step 0 completed in 0 msec counterexample is spurious refining abstraction... cex: 10 6 0 Refining 4 Pivot Node : 2 RevSuffix [2-10-4,1-6-2] LI at pc(v1):y>=1 preds(p(_,data(_,A,_)), [A>=rat(1,1)]). -------------------------------------------------- abstraction refinement iteration 1: predicates: _15319: #1: y>=1 lfp iteration 0 1 2 3 4 5 6 abstract_check at refinement step 1 completed in 0 msec counterexample is spurious refining abstraction... cex: 10 9 4 11 8 7 6 0 Refining 8 Pivot Node : 2 RevSuffix [2-7-3,1-6-2] LI at pc(v1):y=<1 preds(p(_,data(_,A,_)), [A>=rat(1,1),A==1, y=<1 lfp iteration 0 1 2 3 4 5 6 7 abstract_check at refinement step 2 completed in 0 msec counterexample is spurious refining abstraction... cex: 10 9 4 11 8 7 1 6 0 Refining 9 Pivot Node : 4 RevSuffix [4-8-5,3-7-4] LI at pc(v2):x=<0 preds(p(_,data(A,B,_)), [B>=rat(1,1),B==1, y=<1, x=<0 lfp iteration 0 1 2 3 4 5 6 7 8 abstract_check at refinement step 3 completed in 10 msec counterexample is spurious refining abstraction... cex: 10 9 4 11 8 2 7 1 6 0 Refining 10 Pivot Node : 4 RevSuffix [6-11-7,5-8-6,4-2-5,3-7-4] LI at pc(v2):y>=10 LI at pc(v2):x-1/5*y=<0 LI at pc(v3):y>=10 preds(p(_,data(A,B,_)), [B>=rat(1,1),B==rat(10,1),A-rat(1,5)*B==1, y=<1, x=<0, y>=10, x-1/5*y=<0 lfp iteration 0 1 2 3 4 5 6 7 8 9 abstract_check at refinement step 4 completed in 0 msec counterexample is spurious refining abstraction... cex: 10 9 4 11 3 8 2 7 1 6 0 Refining 11 Pivot Node : 8 RevSuffix [10-10-11,9-9-10,8-4-9,7-11-8] LI at pc(v4):x+1/2*y>=5/2 LI at pc(v4):x-2*y=<0 LI at pc(v1):y>=1 preds(p(_,data(A,B,_)), [B>=rat(1,1),B==rat(10,1),A-rat(1,5)*B==rat(5,2),A-rat(2,1)*B==1, y=<1, x=<0, y>=10, x-1/5*y=<0, x+1/2*y>=5/2, x-2*y=<0 lfp iteration 0 1 2 3 4 5 6 7 8 9 Number of interpolation queries: 9. Number of entailment checks during fixpoint checking: 0. Number of entailment checks that could be saved: 0. Number of entailment checks for abstraction: 260. abstract_check at refinement step 5 completed in 10 msec ================================================== ARMC: program is correct abstract fixpoint abstract_state(1, pc(v0), []). abstract_state(3, pc(v1), [1,7]). abstract_state(5, pc(v2), [1,4,5,6,7]). abstract_state(7, pc(v3), [1,6]). abstract_state(9, pc(v4), [1,6,7]). frontier 0: 1 pc(v0) from 0 by appying 0: T frontier 2: 3 pc(v1) from 2 by appying 1: y>=1, x-2*y=<0 frontier 4: 5 pc(v2) from 4 by appying 2: y>=1, y>=10, x-1/5*y=<0, x+1/2*y>=5/2, x-2*y=<0 frontier 6: 7 pc(v3) from 6 by appying 3: y>=1, x+1/2*y>=5/2 frontier 8: 9 pc(v4) from 8 by appying 4: y>=1, x+1/2*y>=5/2, x-2*y=<0 _123072: #7: y>=1, y=<1, x=<0, y>=10, x-1/5*y=<0, x+1/2*y>=5/2, x-2*y=<0 ================================================== verifying fixpoint...done. pc(v0): [[]] pc(v1): [[1,7]] pc(v2): [[1,4,5,6,7]] pc(v3): [[1,6]] pc(v4): [[1,6,7]] Time on instantiating uf axioms: run 0.00, wall 0.00 s. Time on cli constraint solving: run 0.00, wall 0.02 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.00, wall 0.01 s. Time on refinement cutting trace: run 0.02, wall 0.03 s. Time on refinement finding unsat subtrace: run 0.00, wall 0.00 s. Time on refinement: run 0.02, wall 0.03 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.01, wall 0.00 s. Time on abstract check: run 0.01, wall 0.04 s. Time on total including result checking: run 0.07, wall 0.13 s. Time on check result: run 0.00, wall 0.02 s. Time on total: run 0.07, wall 0.11 s. Number of interpolation queries: 9. Number of entailment checks during fixpoint checking: 5. Number of entailment checks that could be saved: 0. Number of entailment checks for abstraction: 260. ================================================== ARMC: program is correct preds(p(_,data(A,B,_)), [B>=rat(1,1),B==rat(10,1),A-rat(1,5)*B==rat(5,2),A-rat(2,1)*B=