[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]: TCSR.armc [runlim] start: Sat Nov 29 18:13:28 2014 [runlim] main pid: 5656 ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008) rybal@mpi-sws.mpg.de cmd line: [TCSR.armc] reading input from TCSR.armc...done. -------------------------------------------------- abstraction refinement iteration 0: predicates: pc(_4508): #0: lfp iteration 0 1 abstract_check at refinement step 0 completed in 0 msec counterexample is spurious refining abstraction... cex: 10 5 0 Refining 5 Pivot Node : 2 RevSuffix [2-10-5,1-5-2] LI at pc(v1):x2-2*th>=0 preds(p(_,data(_,A,B,_)), [A-rat(2,1)*B>=rat(0,1)]). -------------------------------------------------- abstraction refinement iteration 1: predicates: _19768: #1: x2-2*th>=0 lfp iteration 0 1 2 abstract_check at refinement step 1 completed in 0 msec counterexample is spurious refining abstraction... cex: 10 1 5 0 Refining 8 Pivot Node : 2 RevSuffix [3-10-8,2-1-3,1-5-2] LI at pc(v1):x2-10/11*th>=36/11 LI at pc(v1):x2-62/55*th>=0 preds(p(_,data(_,A,B,_)), [A-rat(2,1)*B>=rat(0,1),A-rat(10,11)*B>=rat(36,11),A-rat(62,55)*B>=rat(0,1)]). -------------------------------------------------- abstraction refinement iteration 2: predicates: _54351: #3: x2-2*th>=0, x2-10/11*th>=36/11, x2-62/55*th>=0 lfp iteration 0 1 2 3 4 abstract_check at refinement step 2 completed in 10 msec counterexample is spurious refining abstraction... cex: 10 9 8 1 5 0 Refining 11 Pivot Node : 7 RevSuffix [7-9-8,3-8-7] LI at pc(v3):th>=15 preds(p(_,data(_,A,B,_)), [A-rat(2,1)*B>=rat(0,1),A-rat(10,11)*B>=rat(36,11),A-rat(62,55)*B>=rat(0,1),B>=rat(15,1)]). -------------------------------------------------- abstraction refinement iteration 3: predicates: _70592: #4: x2-2*th>=0, x2-10/11*th>=36/11, x2-62/55*th>=0, th>=15 lfp iteration 0 1 2 3 4 5 abstract_check at refinement step 3 completed in 10 msec counterexample is spurious refining abstraction... cex: 10 9 3 8 1 5 0 Refining 13 Pivot Node : 10 RevSuffix [10-10-13,9-9-10] LI at pc(v1):th=<3 preds(p(_,data(_,A,B,_)), [A-rat(2,1)*B>=rat(0,1),A-rat(10,11)*B>=rat(36,11),A-rat(62,55)*B>=rat(0,1),B>=rat(15,1),B==0, x2-10/11*th>=36/11, x2-62/55*th>=0, th>=15, th=<3 lfp iteration 0 1 2 3 4 5 6 abstract_check at refinement step 4 completed in 10 msec counterexample is spurious refining abstraction... cex: 10 1 9 3 8 1 5 0 Refining 12 Pivot Node : 8 RevSuffix [9-10-12,8-1-9,7-9-8] LI at pc(v1):x2-10/11*th>= -30/11 LI at pc(v1):x2-10/11*th>= -30/11 preds(p(_,data(_,A,B,_)), [A-rat(2,1)*B>=rat(0,1),A-rat(10,11)*B>=rat(36,11),A-rat(62,55)*B>=rat(0,1),B>=rat(15,1),B==rat(-30,11)]). -------------------------------------------------- abstraction refinement iteration 5: predicates: _134840: #6: x2-2*th>=0, x2-10/11*th>=36/11, x2-62/55*th>=0, th>=15, th=<3, x2-10/11*th>= -30/11 lfp iteration 0 1 2 3 4 5 6 7 8 9 Number of interpolation queries: 7. Number of entailment checks during fixpoint checking: 0. Number of entailment checks that could be saved: 0. Number of entailment checks for abstraction: 327. abstract_check at refinement step 5 completed in 20 msec ================================================== ARMC: program is correct abstract fixpoint abstract_state(1, pc(v0), []). abstract_state(9, pc(v1), [6]). abstract_state(12, pc(v2), [6]). abstract_state(13, pc(v3), [6]). frontier 0: 1 pc(v0) from 0 by appying 0: T frontier 6: 9 pc(v1) from 8 by appying 1: x2-10/11*th>= -30/11 frontier 8: 12 pc(v2) from 10 by appying 2: x2-10/11*th>= -30/11 frontier 8: 13 pc(v3) from 11 by appying 3: x2-10/11*th>= -30/11 _137833: #6: x2-2*th>=0, x2-10/11*th>=36/11, x2-62/55*th>=0, th>=15, th=<3, x2-10/11*th>= -30/11 ================================================== verifying fixpoint...done. pc(v0): [[]] pc(v1): [[6]] pc(v2): [[6]] pc(v3): [[6]] Time on instantiating uf axioms: run 0.00, wall 0.00 s. Time on cli constraint solving: run 0.01, wall 0.00 s. Time on cli constraint preparation: run 0.01, 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.01, wall 0.01 s. Time on refinement cutting trace: run 0.03, wall 0.03 s. Time on refinement finding unsat subtrace: run 0.00, wall 0.01 s. Time on refinement: run 0.03, wall 0.04 s. Time on concrete postcondition operator: run 0.00, wall 0.00 s. Time on fixpoint abstraction: run 0.02, wall 0.00 s. Time on fixpoint test: run 0.00, wall 0.00 s. Time on abstract check: run 0.04, wall 0.03 s. Time on total including result checking: run 0.10, wall 0.16 s. Time on check result: run 0.00, wall 0.01 s. Time on total: run 0.10, wall 0.15 s. Number of interpolation queries: 7. Number of entailment checks during fixpoint checking: 4. Number of entailment checks that could be saved: 0. Number of entailment checks for abstraction: 327. ================================================== ARMC: program is correct preds(p(_,data(_,A,B,_)), [A-rat(2,1)*B>=rat(0,1),A-rat(10,11)*B>=rat(36,11),A-rat(62,55)*B>=rat(0,1),B>=rat(15,1),B==rat(-30,11)]). System information Variables: 4 Transitions: 10 Locations: 5 Analysis information Predicates: 6 Reachable abstract states: 13 Abstraction refinement iterations: 5 [runlim] end: Sat Nov 29 18:13:28 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 0.84 seconds [runlim] time: 0.19 seconds [runlim] space: 6.6 MB [runlim] samples: 2