Tool 2LS 0.7.2-sv-comp19 AProVE 84fce4cdfd CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux PeSCo 1.7-svn b8d6131600+ Pinaka 0.1 SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-04 22:41:51 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:44:04 CET 2018-12-06 20:14:43 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET
Run set 2ls.sv-comp19_prop-termination.Termination-Other aprove.sv-comp19_prop-termination.Termination-Other cbmc.sv-comp19_prop-termination.Termination-Other cbmc-path.sv-comp19_prop-termination.Termination-Other cpa-seq.sv-comp19_prop-termination.Termination-Other depthk.sv-comp19_prop-termination.Termination-Other divine-explicit.sv-comp19_prop-termination.Termination-Other divine-smt.sv-comp19_prop-termination.Termination-Other esbmc-kind.sv-comp19_prop-termination.Termination-Other pesco.sv-comp19_prop-termination.Termination-Other pinaka.sv-comp19_prop-termination.Termination-Other smack.sv-comp19_prop-termination.Termination-Other symbiotic.sv-comp19_prop-termination.Termination-Other uautomizer.sv-comp19_prop-termination.Termination-Other ukojak.sv-comp19_prop-termination.Termination-Other utaipan.sv-comp19_prop-termination.Termination-Other
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s --graphml-witness witness.graphml -w error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i error (134) .093 24 .80 0 true 16   1300 150 2 true 130     4200   1600    2 true 130     2900   1500    2 unknown 3.3 270 29 0 unknown 900    2700 9100   0 unknown .030 4.6 .16  0 unknown .036 4.6 .25  0 timeout 900     12000 11000    0 error 3.3 270 32 0 true 130    2900 1800   2 disqualified .051 9.4 .33 0 true 1.0   96 16    2 true 11   500 100 2 error (5) .025 5.5 .13  0 error (5) .024 5.6 .17  0
array-examples/sanfoundry_24_true-unreach-call_true-termination.i error (134) .12  24 .73 0 true 200   8000 1200 2 error (42) 880     4000   9800    0 out of memory 170     15000   2500    0 unknown 3.3 270 32 0 unknown .79 67 8.6 0 unknown .030 4.6 .23  0 unknown .037 4.8 .20  0 timeout 900     1000 9700    0 error 3.3 270 29 0 out of memory 42    15000 450   0 disqualified .046 9.3 .37 0 timeout (verification) 900     1200 13000    0 true 16   530 140 2 error (5) .024 5.6 .099 0 error (5) .025 5.6 .11  0
array-examples/standard_sentinel_true-unreach-call_true-termination.i error (134) .097 24 .69 0 error (1) 25   1400 220 0 error (42) 880     2500   12000    0 error (42) 880     2600   13000    0 unknown 3.3 270 31 0 unknown 61    44 730   0 unknown .036 4.6 .24  0 unknown .031 4.8 .15  0 timeout 900     1200 14000    0 error 3.2 270 29 0 timeout 900    930 6800   0 disqualified .077 9.1 .44 0 timeout (verification) 900     2600 5500    0 true 9.7 380 79 2 error (5) .031 5.7 .11  0 error (5) .027 5.5 .15  0
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i error (134) .088 23 .79 0 error (1) 27   1400 250 0 error (42) 880     5000   5700    0 out of memory 170     15000   1900    0 unknown 3.3 270 31 0 unknown 63    51 870   0 unknown .040 4.7 .20  0 unknown .032 4.6 .17  0 timeout 900     970 12000    0 error 3.4 270 28 0 out of memory 350    15000 5500   0 disqualified .049 9.4 .49 0 true .15  16 1.6  2 true 11   470 84 2 error (5) .020 5.6 .15  0 error (5) .024 5.6 .15  0
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i error (134) .086 24 .91 0 true 9.0 570 68 2 out of memory 87     15000   1300    0 out of memory 120     15000   1500    0 unknown 3.1 270 32 0 unknown 1.2  66 12   0 unknown .047 4.6 .16  0 unknown .032 4.7 .16  0 timeout 900     7100 11000    0 error 3.3 270 28 0 true 43    830 530   2 disqualified .047 9.4 .41 0 true .43  33 5.7  2 true 13   500 100 2 error (5) .025 5.6 .12  0 error (5) .024 5.6 .14  0
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i error (134) .12  24 .75 0 true 72   3000 710 2 out of memory 68     15000   930    0 out of memory 160     15000   2600    0 unknown 3.2 270 32 0 unknown 170    58 2000   0 unknown .032 4.5 .32  0 unknown .035 4.6 .18  0 timeout 900     3200 12000    0 error 3.3 270 32 0 out of memory 320    15000 4100   0 disqualified .055 9.0 .46 0 timeout (verification) 900     2700 10000    0 timeout 900   810 10000 0 error (5) .038 5.7 .15  0 error (5) .024 5.6 .11  0
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i error (134) .091 24 .86 0 error (1) 42   2300 440 0 out of memory 68     15000   980    0 out of memory 190     15000   2800    0 unknown 3.4 270 29 0 unknown 900    340 11000   0 unknown .045 4.6 .17  0 unknown .027 4.6 .20  0 timeout 900     4300 9500    0 error 3.2 270 33 0 out of memory 440    15000 5100   0 disqualified .045 9.6 .39 0 timeout (verification) 900     3200 11000    0 timeout 900   810 11000 0 error (5) .023 5.7 .15  0 error (5) .024 5.6 .12  0
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i error (134) .086 24 .79 0 timeout 910   13000 6900 0 out of memory 68     15000   880    0 out of memory 190     15000   2500    0 unknown 3.4 270 30 0 unknown 230    67 3000   0 unknown .028 4.6 .18  0 unknown .031 4.6 .16  0 timeout 900     3900 10000    0 error 3.3 270 29 0 out of memory 320    15000 4300   0 disqualified .051 9.4 .45 0 timeout (verification) 900     3300 12000    0 true 11   470 98 2 error (5) .022 5.5 .16  0 error (5) .027 5.7 .16  0
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i true .33  49 3.0  2 true 26   2300 210 2 error (42) 880     14000   5800    0 out of memory 400     15000   5900    0 timeout 900   4300 11000 0 unknown 900    83 13000   0 unknown .055 4.6 .13  0 unknown .026 4.6 .24  0 timeout 900     910 13000    0 timeout 910   4300 12000 0 timeout 900    9800 5600   0 disqualified .048 9.3 .35 0 timeout (verification) 900     630 11000    0 true 11   490 93 2 error (5) .032 5.6 .13  0 error (5) .030 5.6 .20  0
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i error (134) .12  23 .74 0 timeout 910   13000 6500 0 out of memory 68     15000   940    0 out of memory 190     15000   2800    0 unknown 3.3 270 32 0 unknown 180    81 2100   0 unknown .030 4.7 .23  0 unknown .028 4.6 .24  0 timeout 900     3900 9900    0 error 3.3 270 30 0 out of memory 310    15000 4300   0 disqualified .042 9.2 .57 0 timeout (verification) 900     3300 11000    0 true 10   460 90 2 error (5) .029 5.6 .16  0 error (5) .024 5.6 .17  0
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i false(termination) .15  24 .90 1 false(termination) 4.3 290 33 1 error (42) 880     650   3800    0 out of memory 110     15000   1500    0 false(termination) 4.0 280 35 1 unknown 900    310 12000   0 unknown .032 4.7 .19  0 unknown .028 4.6 .14  0 timeout 900     1000 9700    0 false(termination) 3.8 280 35 1 out of memory 33    15000 440   0 disqualified .047 9.2 .39 0 timeout (verification) 900     300 9800    0 false(termination) 7.7 370 57 1 error (5) .027 5.6 .14  0 error (5) .048 5.6 .098 0
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i false(termination) .16  24 1.1  1 false(termination) 8.3 490 67 0 error (42) 880     950   3700    0 out of memory 120     15000   1400    0 false(termination) 4.1 280 37 1 unknown 900    290 11000   0 unknown .043 4.5 .20  0 unknown .053 4.6 .18  0 timeout 900     700 9600    0 false(termination) 3.9 280 38 1 out of memory 32    15000 440   0 disqualified .045 9.1 .40 0 timeout (verification) 900     400 11000    0 false(termination) 7.9 380 67 1 error (5) .024 5.6 .13  0 error (5) .026 5.6 .19  0
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i false(termination) .17  24 1.0  1 error (1) 3.6 260 33 0 error (42) 880     1300   4500    0 out of memory 120     15000   1600    0 false(termination) 4.1 280 38 1 unknown 900    260 11000   0 unknown .030 4.6 .28  0 unknown .027 4.6 .20  0 timeout 900     660 8500    0 false(termination) 4.1 290 38 1 out of memory 31    15000 420   0 disqualified .045 9.4 .42 0 error(unknown, verification-finished) 49     2300 650    0 false(termination) 7.9 360 62 1 error (5) .023 5.6 .21  0 error (5) .027 5.7 .10  0
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i false(termination) .14  24 1.0  1 error (1) 4.2 270 38 0 error (42) 880     1400   4900    0 out of memory 130     15000   1500    0 false(termination) 4.1 280 38 1 unknown 900    300 12000   0 unknown .031 4.7 .16  0 unknown .035 4.7 .19  0 timeout 900     660 9900    0 false(termination) 4.2 280 36 1 out of memory 32    15000 380   0 disqualified .043 9.5 .44 0 error(unknown, verification-finished) 49     2300 690    0 false(termination) 8.2 370 57 1 error (5) .032 5.6 .17  0 error (5) .028 5.6 .27  0
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i false(termination) .14  23 1.0  1 error (1) 25   1400 190 0 error (42) 880     1300   4500    0 out of memory 130     15000   1700    0 false(termination) 4.1 280 39 1 unknown 900    280 12000   0 unknown .033 4.5 .26  0 unknown .028 4.5 .27  0 timeout 900     930 9800    0 false(termination) 4.0 280 34 1 out of memory 39    15000 480   0 disqualified .045 9.5 .48 0 error(unknown, verification-finished) 49     2300 640    0 false(termination) 8.0 360 58 1 error (5) .031 5.6 .24  0 error (5) .028 5.6 .16  0
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i error (134) 1.7   170 16    0 error (1) 3.9 270 36 0 true .10  6.1 .99 2 true .24  12   2.2  2 timeout 900   8700 12000 0 unknown 2.3  67 31   0 unknown .032 4.5 .17  0 unknown .028 4.6 .15  0 true .11  27 1.4  2 timeout 930   7400 10000 0 true .53 59 6.7 2 disqualified .049 9.3 .40 0 true .38  18 5.1  2 error (7) 130   1600 1400 0 error (5) .047 5.5 .15  0 error (5) .047 5.6 .10  0
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i error (134) 1.8   160 15    0 error (1) 4.0 280 32 0 true .11  6.2 .87 2 true .20  12   2.4  2 timeout 920   8800 11000 0 unknown 2.4  68 29   0 unknown .028 4.6 .22  0 unknown .028 4.7 .18  0 true .12  27 1.2  2 timeout 930   7400 9900 0 true .51 60 7.0 2 disqualified .050 9.3 .46 0 true .36  18 4.9  2 true 110   940 1300 2 error (5) .037 5.6 .092 0 error (5) .026 5.6 .22  0
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i error (134) 1.8   160 16    0 error (1) 4.2 270 34 0 true .12  6.2 .93 2 true .81  38   9.9  2 timeout 900   4000 11000 0 unknown 1.2  67 13   0 unknown .039 4.6 .17  0 unknown .027 4.6 .21  0 true .13  27 1.8  2 timeout 910   3900 11000 0 true 1.2  95 16   2 disqualified .059 9.2 .46 0 true 1.2   19 15    2 true 66   930 660 2 error (5) .042 5.5 .10  0 error (5) .024 5.6 .15  0
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .30  31 3.5  2 error (1) 13   940 110 0 true .079 6.3 .35 2 true .088 5.7 .33 2 true 77   530 870 2 unknown 3.8  67 49   0 unknown .052 4.6 .16  0 unknown .028 4.6 .21  0 true .081 26 .88 2 true 77   500 990 2 true .38 58 3.0 2 disqualified .069 9.2 .37 0 true .16  16 2.1  2 true 15   570 130 2 error (5) .022 5.7 .082 0 error (5) .023 5.7 .11  0
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c false(termination) .71  90 6.4  1 error (1) 13   690 120 0 error (42) 880     400   4700    0 out of memory 370     15000   3500    0 false(termination) 57   2200 540 1 unknown 900    350 11000   0 unknown .031 4.6 .14  0 unknown .028 4.6 .19  0 timeout 900     2000 9500    0 false(termination) 45   1200 420 1 out of memory 49    15000 570   0 disqualified .044 9.2 .67 0 timeout (verification) 900     610 11000    0 false(termination) 15   560 130 1 error (5) .022 5.6 .24  0 error (5) .033 5.5 .18  0
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c false(termination) .68  91 5.8  1 error (1) 13   710 110 0 error (42) 880     400   5200    0 out of memory 370     15000   3900    0 false(termination) 35   1100 320 1 unknown 900    350 12000   0 unknown .033 4.7 .24  0 unknown .031 4.7 .19  0 timeout 900     2000 11000    0 false(termination) 50   2200 440 1 out of memory 48    15000 780   0 disqualified .068 9.4 .40 0 timeout (verification) 900     120 11000    0 false(termination) 14   560 120 1 error (5) .024 5.6 .17  0 error (5) .044 5.6 .11  0
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true .91  100 8.4  2 timeout 900   160 11000 0 true 3.5   27   41    2 error (42) 880     6600   11000    0 true 9.1 450 81 2 unknown 1.4  66 17   0 unknown .032 4.6 .19  0 unknown .029 4.6 .16  0 true .91  27 12    2 true 8.8 460 77 2 out of memory 57    15000 790   0 disqualified .055 8.7 .35 0 timeout (verification) 900     150 13000    0 true 13   490 95 2 error (5) .027 5.6 .10  0 error (5) .030 5.5 .23  0
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1.4   150 16    2 timeout 900   160 9600 0 true 2.5   27   38    2 error (42) 880     1600   10000    0 exception 8.2 460 73 0 unknown 1.2  67 16   0 unknown .029 4.7 .22  0 unknown .030 4.8 .20  0 true .21  27 2.6  2 exception 9.3 480 78 0 out of memory 64    15000 840   0 disqualified .045 9.6 .47 0 true 530     120 7900    2 true 13   550 110 2 error (5) .023 5.6 .15  0 error (5) .025 5.6 .091 0
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1.3   150 14    2 timeout 900   160 12000 0 true 2.5   27   29    2 error (42) 880     2200   11000    0 exception 8.8 360 66 0 unknown 1.0  66 11   0 unknown .048 4.8 .20  0 unknown .030 4.6 .20  0 true .24  27 2.5  2 exception 9.3 350 88 0 out of memory 59    15000 870   0 disqualified .055 9.3 .34 0 true 800     140 12000    2 true 13   520 120 2 error (5) .029 5.6 .14  0 error (5) .035 5.7 .19  0
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true .89  97 8.1  2 timeout 900   160 12000 0 true 3.3   28   47    2 error (42) 880     10000   10000    0 true 9.0 470 75 2 unknown 4.7  67 57   0 unknown .030 4.6 .26  0 unknown .029 4.6 .22  0 true .92  27 11    2 true 9.0 480 78 2 out of memory 96    15000 1400   0 disqualified .060 9.4 .43 0 timeout (verification) 900     1500 11000    0 true 12   480 97 2 error (5) .027 5.6 .080 0 error (5) .031 5.6 .10  0
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1.2   130 11    2 timeout 900   160 11000 0 true 2.5   27   34    2 error (42) 880     1600   12000    0 exception 8.2 340 75 0 unknown 1.2  66 15   0 unknown .046 4.6 .13  0 unknown .033 4.6 .23  0 true .23  27 2.4  2 exception 9.0 460 75 0 out of memory 64    15000 940   0 disqualified .045 9.3 .37 0 true 540     120 7100    2 true 12   490 120 2 error (5) .028 5.5 .20  0 error (5) .023 5.5 .21  0
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c true .10  24 .82 2 error (1) 2.4 210 23 0 true .049 7.8 .42 2 true .040 6.7 .26 2 true 3.2 270 35 2 unknown .60 66 5.8 0 unknown .028 4.7 .17  0 unknown .038 4.6 .19  0 true .077 26 .74 2 true 3.2 270 29 2 true .36 59 3.9 2 disqualified .048 9.2 .52 0 true .17  16 1.6  2 true 6.8 330 53 2 error (5) .022 5.5 .12  0 error (5) .026 5.6 .13  0
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c true .11  24 .75 2 error (1) 2.3 210 20 0 true .092 6.6 .31 2 true .040 6.6 .34 2 true 3.3 280 30 2 unknown .62 65 6.0 0 unknown .032 4.6 .20  0 unknown .052 4.6 .25  0 true .079 26 .96 2 true 3.3 260 30 2 true .36 58 2.9 2 disqualified .070 9.2 .41 0 true .15  15 1.7  2 true 6.9 340 53 2 error (5) .024 5.6 .15  0 error (5) .024 5.6 .15  0
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true .11  24 .63 2 error (1) 2.4 210 25 0 true .052 6.9 .41 2 true .047 6.4 .33 2 true 3.4 270 30 2 unknown .77 67 8.1 0 unknown .034 4.7 .25  0 unknown .028 4.7 .21  0 true .075 26 .93 2 true 3.3 270 31 2 true .37 59 2.7 2 disqualified .089 9.2 .47 0 true .14  16 1.6  2 true 7.9 350 63 2 error (5) .030 5.6 .078 0 error (5) .044 5.5 .13  0
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c true .10  24 .81 2 error (1) 2.0 190 21 0 true .040 7.0 .47 2 true .043 6.3 .26 2 true 3.3 270 28 2 unknown .59 65 5.8 0 unknown .033 4.6 .32  0 unknown .027 4.5 .17  0 true .094 26 .77 2 true 3.3 270 29 2 true .36 59 2.4 2 disqualified .049 9.4 .38 0 true .15  16 1.8  2 true 7.8 360 55 2 error (5) .035 5.6 .084 0 error (5) .054 5.5 .17  0
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true .10  24 .98 2 error (1) 2.0 190 19 0 true .055 6.7 .34 2 true .093 5.9 .18 2 true 3.3 270 30 2 unknown .80 68 9.1 0 unknown .032 4.8 .21  0 unknown .027 4.6 .22  0 true .075 26 .93 2 true 3.2 270 31 2 true .39 59 2.3 2 disqualified .049 9.2 .35 0 true .18  16 1.8  2 true 7.4 360 64 2 error (5) .049 5.6 .12  0 error (5) .021 5.6 .11  0
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c error (5) .098 24 .79 0 error (1) 4.4 310 41 0 out of memory 690     15000   4200    0 error (42) 880     780   9700    0 true 4.4 290 40 2 unknown .87 66 9.0 0 unknown .031 4.7 .21  0 unknown .026 4.6 .15  0 timeout 900     1500 8900    0 error (recursion) 3.2 260 31 0 out of memory 180    15000 2600   0 disqualified .042 9.1 .46 0 timeout (verification) 900     710 11000    0 true 9.8 390 79 2 error (5) .030 5.6 .15  0 error (5) .025 5.5 .12  0
bitvector-regression/signextension2_false-unreach-call_true-termination.c true .11  24 .79 2 true 2.9 230 25 2 true .098 6.3 .26 2 true .038 6.7 .33 2 true 3.3 270 32 2 unknown .57 65 5.7 0 unknown .052 4.6 .15  0 unknown .032 4.6 .19  0 true .085 26 .85 2 true 3.2 270 32 2 true .36 59 3.9 2 disqualified .045 9.9 .49 0 true .16  17 1.6  2 true 7.4 360 64 2 error (5) .034 5.7 .18  0 error (5) .021 5.6 .19  0
bitvector-regression/signextension2_true-unreach-call_true-termination.c true .097 24 1.1  2 true 2.9 220 25 2 true .050 6.5 .36 2 true .040 6.6 .41 2 true 3.1 270 28 2 unknown .82 66 8.6 0 unknown .031 4.5 .14  0 unknown .029 4.5 .15  0 true .074 26 .86 2 true 3.3 270 29 2 true .34 59 3.3 2 disqualified .072 9.5 .35 0 true .16  16 1.9  2 true 7.9 370 60 2 error (5) .032 5.6 .17  0 error (5) .037 5.6 .14  0
bitvector-regression/signextension_false-unreach-call_true-termination.c true .14  24 .89 2 true 3.3 260 31 2 true .046 6.5 .42 2 true .041 7.0 .34 2 true 3.2 270 29 2 unknown .62 65 6.4 0 unknown .029 4.6 .21  0 unknown .029 4.6 .20  0 true .077 26 1.1  2 true 3.4 270 32 2 true .34 59 4.1 2 disqualified .048 9.2 .38 0 true .15  16 1.6  2 true 7.4 360 52 2 error (5) .032 5.6 .19  0 error (5) .050 5.4 .17  0
bitvector-regression/signextension_true-unreach-call_true-termination.c true .10  24 1.0  2 true 3.1 260 26 2 true .052 6.5 .51 2 true .041 6.2 .32 2 true 3.3 270 27 2 unknown .80 67 8.2 0 unknown .031 4.7 .25  0 unknown .054 4.7 .19  0 true .076 26 .96 2 true 3.3 270 31 2 true .37 59 2.9 2 disqualified .044 8.9 .42 0 true .16  16 1.7  2 true 7.9 350 65 2 error (5) .027 5.7 .16  0 error (5) .030 5.7 .13  0
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i out of memory 640     15000 6800    0 error (1) 32   2300 320 0 true .13  6.8 .61 2 true .12  7.0 1.4  2 timeout 910   4400 12000 0 unknown 4.0  67 61   0 unknown .028 4.6 .33  0 unknown .031 4.6 .24  0 true .084 26 .92 2 timeout 910   4300 14000 0 true .53 61 5.7 2 disqualified .047 9.1 .39 0 true .51  18 5.8  2 true 23   510 220 2 error (5) .023 5.6 .11  0 error (5) .027 5.6 .15  0
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2.8   810 25    2 timeout 900   1700 11000 0 true .90  31   9.9  2 true 7.3   140   90    2 true 7.0 300 70 2 unknown .91 65 11   0 unknown .033 4.6 .22  0 unknown .035 4.6 .15  0 true .34  40 4.5  2 true 6.4 320 56 2 true 5.8  1200 70   2 disqualified .047 9.5 .46 0 true .85  22 13    2 true 18   550 150 2 error (5) .027 5.5 .15  0 error (5) .033 5.6 .18  0
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2.7   810 24    2 timeout 900   2300 11000 0 true .90  31   13    2 true 7.3   140   91    2 true 6.7 300 60 2 unknown 2.0  67 22   0 unknown .034 4.5 .25  0 unknown .026 4.6 .14  0 true .33  40 5.3  2 true 6.9 310 59 2 true 5.8  1200 70   2 disqualified .069 8.9 .41 0 true .84  22 13    2 true 17   590 130 2 error (5) .022 5.5 .087 0 error (5) .027 5.5 .091 0
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.1   230 9.7  2 timeout 900   2400 13000 0 error (42) 880     5800   4200    0 error (42) 870     690   9700    0 true 18   650 140 2 unknown 1.2  67 15   0 unknown .037 4.5 .14  0 unknown .036 4.6 .30  0 timeout 900     1100 11000    0 true 18   640 170 2 timeout 900    590 6400   0 disqualified .060 9.2 .40 0 true .57  20 7.8  2 true 13   480 95 2 error (5) .025 5.6 .15  0 error (5) .024 5.6 .17  0
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .73  160 6.4  2 timeout 900   920 14000 0 true .22  9.4 3.0  2 true 2.5   100   31    2 true 5.5 300 49 2 unknown .70 65 7.9 0 unknown .030 4.6 .18  0 unknown .025 4.6 .20  0 true .15  31 1.6  2 true 5.7 300 50 2 true 4.7  740 55   2 disqualified .044 9.1 .50 0 true .51  19 5.3  2 true 15   520 110 2 error (5) .027 5.6 .11  0 error (5) .029 5.6 .14  0
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .69  150 7.3  2 timeout 900   1800 13000 0 true .22  9.9 2.5  2 true 2.5   100   38    2 true 5.8 310 47 2 unknown 1.2  66 15   0 unknown .032 4.7 .23  0 unknown .030 4.8 .21  0 true .15  31 1.7  2 true 5.6 300 57 2 true 4.8  740 63   2 disqualified .044 9.7 .47 0 true .47  18 5.2  2 true 15   610 110 2 error (5) .028 5.6 .11  0 error (5) .025 5.7 .14  0
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.1   280 9.6  2 timeout 900   1300 10000 0 true .46  16   6.2  2 true 5.4   170   71    2 true 5.8 310 51 2 unknown .78 66 8.7 0 unknown .030 4.6 .24  0 unknown .052 4.6 .26  0 true .21  33 2.6  2 true 5.9 290 50 2 true 6.8  1200 75   2 disqualified .048 9.9 .41 0 true .68  21 11    2 true 16   590 130 2 error (5) .025 5.5 .14  0 error (5) .026 5.6 .14  0
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.1   280 11    2 timeout 900   1700 12000 0 true .46  16   5.8  2 true 5.4   170   81    2 true 6.1 320 52 2 unknown 1.5  66 17   0 unknown .027 4.6 .23  0 unknown .042 4.5 .20  0 true .21  33 3.4  2 true 5.8 310 48 2 true 6.9  1200 82   2 disqualified .063 9.2 .41 0 true .69  21 9.9  2 true 16   590 120 2 error (5) .024 5.7 .081 0 error (5) .026 5.6 .099 0
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .23  36 2.0  2 timeout 900   2100 10000 0 true .14  6.9 1.0  2 true .49  15   6.6  2 true 3.8 260 34 2 unknown .90 67 8.0 0 unknown .045 4.6 .16  0 unknown .027 4.6 .19  0 true .10  28 1.3  2 true 4.1 260 36 2 true .81 89 9.0 2 disqualified .044 9.3 .51 0 true .24  18 2.8  2 true 9.3 360 70 2 error (5) .049 5.5 .12  0 error (5) .048 5.6 .11  0
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .38  88 3.8  2 timeout 900   1900 8700 0 true .18  8.6 1.9  2 true 1.0   22   14    2 true 4.3 260 37 2 unknown .66 67 6.3 0 unknown .045 4.8 .44  0 unknown .032 4.7 .15  0 true .15  30 2.0  2 true 4.2 260 42 2 true 1.5  160 18   2 disqualified .045 9.2 .40 0 true .35  19 4.3  2 true 10   380 81 2 error (5) .031 5.6 .19  0 error (5) .023 5.7 .14  0
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .39  87 3.9  2 timeout 900   1600 11000 0 true .18  8.5 2.6  2 true .99  21   11    2 true 4.4 260 46 2 unknown 1.0  67 12   0 unknown .029 4.6 .20  0 unknown .036 4.6 .24  0 true .12  30 1.4  2 true 4.3 260 38 2 true 1.5  160 20   2 disqualified .047 9.0 .38 0 true .36  19 3.7  2 true 10   390 76 2 error (5) .043 5.5 .14  0 error (5) .026 5.6 .13  0
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(termination) 3.2   290 20    0 error (1) 16   1200 140 0 error (42) 880     770   6400    0 out of memory 160     15000   2000    0 timeout 900   4200 10000 0 unknown .60 64 5.6 0 unknown .031 4.5 .23  0 unknown .041 4.6 .19  0 timeout 900     2500 10000    0 timeout 900   4500 11000 0 out of memory 48    15000 730   0 disqualified .050 9.6 .40 0 timeout (verification) 900     170 11000    0 false(termination) 66   1200 680 1 error (5) .025 5.7 .21  0 error (5) .043 5.5 .091 0
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(termination) 3.0   290 20    0 error (1) 17   1000 180 0 error (42) 880     630   6600    0 out of memory 110     15000   1300    0 timeout 900   4400 12000 0 unknown 9.6  80 120   0 unknown .029 4.5 .21  0 unknown .041 4.7 .22  0 timeout 900     2200 10000    0 timeout 900   4600 11000 0 out of memory 51    15000 580   0 disqualified .044 9.6 .53 0 timeout (verification) 900     2800 8200    0 false(termination) 45   1100 390 1 error (5) .026 5.6 .17  0 error (5) .024 5.6 .15  0
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(termination) 4.9   320 37    0 error (1) 15   1200 140 0 error (42) 880     590   7700    0 out of memory 110     15000   1200    0 timeout 900   4600 8700 0 unknown 8.6  82 120   0 unknown .029 4.6 .18  0 unknown .030 4.6 .22  0 timeout 900     2100 10000    0 false(termination) 800   4700 8800 1 out of memory 75    15000 990   0 disqualified .046 9.6 .44 0 timeout (verification) 900     2800 11000    0 false(termination) 48   1400 420 1 error (5) .047 5.5 .12  0 error (5) .028 5.7 .18  0
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(termination) 3.2   300 20    0 error (1) 15   900 150 0 error (42) 880     630   5200    0 out of memory 110     15000   1400    0 timeout 900   5400 11000 0 unknown 3.5  66 43   0 unknown .030 4.7 .27  0 unknown .031 4.7 .26  0 timeout 900     2300 10000    0 timeout 900   5300 10000 0 out of memory 76    15000 1000   0 disqualified .046 9.5 .39 0 timeout (verification) 900     2800 9000    0 false(termination) 42   1100 360 1 error (5) .031 5.5 .26  0 error (5) .026 5.6 .14  0
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(termination) 2.8   270 21    0 error (1) 19   1200 160 0 error (42) 880     650   5800    0 out of memory 110     15000   1200    0 false(termination) 700   4200 7700 1 unknown 1.2  67 13   0 unknown .048 4.7 .19  0 unknown .037 4.6 .20  0 timeout 900     2300 10000    0 timeout 900   4000 13000 0 out of memory 45    15000 660   0 disqualified .044 9.2 .37 0 timeout (verification) 900     690 10000    0 false(termination) 55   1600 450 1 error (5) .030 5.6 .11  0 error (5) .044 5.5 .13  0
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(termination) 3.3   300 22    0 error (1) 14   940 140 0 error (42) 880     670   6300    0 out of memory 110     15000   1400    0 timeout 900   4200 10000 0 unknown 3.1  67 35   0 unknown .030 4.7 .20  0 unknown .033 4.6 .23  0 timeout 900     2500 9600    0 timeout 900   4200 9700 0 out of memory 50    15000 650   0 disqualified .047 9.2 .43 0 timeout (verification) 900     440 10000    0 false(termination) 36   870 310 1 error (5) .026 5.8 .13  0 error (5) .023 5.7 .13  0
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c false(termination) 3.1   290 19    0 error (1) 15   940 140 0 error (42) 880     690   5300    0 out of memory 110     15000   1500    0 timeout 900   4000 11000 0 unknown 900    390 12000   0 unknown .052 4.7 .17  0 unknown .030 4.5 .17  0 timeout 900     2400 12000    0 timeout 900   4900 9700 0 out of memory 50    15000 680   0 disqualified .050 9.5 .44 0 timeout (verification) 900     410 9300    0 false(termination) 38   1100 330 1 error (5) .020 5.7 .23  0 error (5) .029 5.7 .15  0
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c false(termination) .28  27 2.5  1 false(termination) 52   4300 410 1 error (42) 880     300   10000    0 out of memory 160     15000   2200    0 false(termination) 22   700 190 1 unknown 280    120 3700   0 unknown .058 4.7 .16  0 unknown .026 4.6 .24  0 timeout 900     1900 11000    0 false(termination) 21   680 180 1 timeout 900    6000 6400   0 disqualified .040 9.6 .56 0 timeout (verification) 900     63 12000    0 false(termination) 18   690 150 1 error (5) .040 5.5 .13  0 error (5) .030 5.7 .13  0
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c false(termination) .17  23 2.0  1 false(termination) 8.8 470 67 0 error (42) 880     400   9100    0 error (42) 880     430   8900    0 false(termination) 9.2 370 78 1 unknown 120    78 1700   0 unknown .026 4.6 .33  0 unknown .028 4.7 .17  0 timeout 900     2300 9900    0 false(termination) 11   400 110 1 out of memory 51    15000 700   0 disqualified .053 9.6 .45 0 timeout (verification) 900     54 12000    0 false(termination) 11   470 82 1 error (5) .028 5.8 .065 0 error (5) .038 5.5 .13  0
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(termination) 2.8   270 17    0 error (1) 16   850 130 0 error (42) 880     690   5600    0 out of memory 110     15000   1500    0 timeout 900   4100 11000 0 unknown 3.1  68 40   0 unknown .055 4.6 .15  0 unknown .030 4.7 .22  0 timeout 900     2400 10000    0 timeout 900   920 9200 0 out of memory 48    15000 660   0 disqualified .043 8.8 .68 0 timeout (verification) 900     720 8300    0 false(termination) 37   940 310 1 error (5) .029 5.7 .088 0 error (5) .031 5.5 .21  0
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c false(termination) 2.8   270 18    0 error (1) 16   1200 150 0 error (42) 880     690   6200    0 out of memory 110     15000   1200    0 false(termination) 740   4500 9300 1 unknown 900    380 12000   0 unknown .036 4.6 .26  0 unknown .029 4.6 .19  0 timeout 900     2300 11000    0 timeout 900   4100 11000 0 out of memory 49    15000 650   0 disqualified .046 8.9 .42 0 timeout (verification) 900     730 9800    0 false(termination) 48   1500 440 1 error (5) .024 5.6 .094 0 error (5) .023 5.6 .10  0
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c false(termination) 2.8   270 17    0 error (1) 16   1200 140 0 error (42) 880     670   5500    0 out of memory 110     15000   1600    0 timeout 900   4600 11000 0 unknown 900    390 11000   0 unknown .035 4.7 .23  0 unknown .030 4.6 .16  0 timeout 900     2300 8800    0 timeout 900   4300 12000 0 out of memory 49    15000 680   0 disqualified .049 9.6 .34 0 timeout (verification) 900     750 10000    0 false(termination) 41   1100 320 1 error (5) .025 5.8 .17  0 error (5) .023 5.6 .14  0
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c false(termination) 2.9   270 20    0 error (1) 15   1200 160 0 error (42) 880     680   5300    0 out of memory 110     15000   1600    0 timeout 900   4800 10000 0 unknown 900    390 10000   0 unknown .034 4.6 .19  0 unknown .068 4.8 .15  0 timeout 900     2300 10000    0 timeout 900   4400 11000 0 out of memory 48    15000 650   0 disqualified .048 9.3 .42 0 timeout (verification) 900     690 9500    0 false(termination) 41   1300 350 1 error (5) .030 5.6 .12  0 error (5) .028 5.6 .12  0
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(termination) 3.1   280 20    0 error (1) 15   910 160 0 error (42) 870     610   4700    0 out of memory 110     15000   1500    0 timeout 900   4600 11000 0 unknown .62 66 5.5 0 unknown .035 4.9 .26  0 unknown .026 4.8 .21  0 timeout 900     2300 8900    0 timeout 900   4600 14000 0 out of memory 47    15000 630   0 disqualified .071 9.7 .36 0 timeout (verification) 900     760 10000    0 false(termination) 47   1300 360 1 error (5) .023 5.7 .21  0 error (5) .022 5.6 .12  0
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c false(termination) 3.2   280 21    0 error (1) 15   1200 130 0 error (42) 880     640   7900    0 out of memory 110     15000   1300    0 timeout 900   3300 11000 0 unknown 900    420 13000   0 unknown .059 4.7 .23  0 unknown .033 4.6 .27  0 timeout 900     2300 11000    0 timeout 900   4400 13000 0 out of memory 49    15000 680   0 disqualified .071 9.6 .36 0 timeout (verification) 900     660 11000    0 false(termination) 45   1300 390 1 error (5) .023 5.6 .23  0 error (5) .024 5.6 .15  0
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c false(termination) 2.9   270 20    0 error (1) 16   940 130 0 error (42) 880     680   5700    0 out of memory 110     15000   1300    0 timeout 900   5000 9400 0 unknown 900    400 11000   0 unknown .029 4.7 .26  0 unknown .033 4.7 .21  0 timeout 900     2300 8900    0 timeout 900   4700 12000 0 out of memory 49    15000 720   0 disqualified .071 9.2 .33 0 timeout (verification) 900     710 9500    0 false(termination) 38   1200 320 1 error (5) .028 5.6 .19  0 error (5) .022 5.5 .19  0
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c false(termination) 2.8   270 16    0 error (1) 16   1200 170 0 error (42) 870     650   4000    0 out of memory 110     15000   1500    0 false(termination) 160   4200 1900 1 unknown 900    390 11000   0 unknown .030 4.7 .16  0 unknown .032 4.5 .30  0 timeout 900     2300 9800    0 timeout 900   1100 11000 0 out of memory 49    15000 640   0 disqualified .048 9.3 .45 0 timeout (verification) 900     660 12000    0 false(termination) 44   1100 390 1 error (5) .031 5.6 .15  0 error (5) .025 5.6 .17  0
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c out of memory 130     15000 870    0 out of memory 790   15000 4000 0 true 16     130   210    2 out of memory 160     15000   2200    0 timeout 900   4700 9900 0 unknown 5.5  67 68   0 unknown .035 4.7 .17  0 unknown .031 4.6 .13  0 true 5.5   130 72    2 timeout 900   4700 12000 0 out of memory 43    15000 630   0 disqualified .049 9.5 .45 0 true .99  18 15    2 true 29   900 240 2 error (5) .026 5.5 .18  0 error (5) .026 5.6 .20  0
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c out of memory 330     15000 1500    0 out of memory 780   15000 4900 0 true 16     130   210    2 out of memory 160     15000   2000    0 timeout 900   4700 12000 0 unknown 37    170 450   0 unknown .029 4.6 .25  0 unknown .028 4.6 .19  0 true 5.4   130 69    2 timeout 900   4100 11000 0 out of memory 44    15000 690   0 disqualified .043 9.2 .50 0 true 1.0   18 12    2 true 28   810 220 2 error (5) .023 5.6 .13  0 error (5) .024 5.7 .11  0
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c out of memory 110     15000 700    0 timeout 900   15000 5200 0 true 16     130   210    2 out of memory 160     15000   2000    0 timeout 900   4300 11000 0 unknown 5.6  67 65   0 unknown .031 4.6 .20  0 unknown .029 4.6 .20  0 true 5.5   140 80    2 timeout 900   4600 11000 0 out of memory 44    15000 520   0 disqualified .065 9.3 .34 0 true 1.0   18 13    2 true 35   1000 290 2 error (5) .031 5.5 .24  0 error (5) .030 5.7 .19  0
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c out of memory 120     15000 830    0 timeout 910   14000 4700 0 true 16     130   200    2 out of memory 160     15000   1900    0 timeout 900   4400 11000 0 unknown 37    180 450   0 unknown .039 4.6 .16  0 unknown .045 4.6 .19  0 true 5.6   140 74    2 timeout 900   4300 11000 0 out of memory 44    15000 670   0 disqualified .062 9.4 .39 0 true 1.0   18 15    2 true 35   1000 280 2 error (5) .029 5.6 .15  0 error (5) .025 5.6 .18  0
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c out of memory 110     15000 720    0 out of memory 820   15000 4800 0 true 19     150   270    2 out of memory 160     15000   2300    0 timeout 900   4300 13000 0 unknown 6.2  72 81   0 unknown .056 4.6 .18  0 unknown .048 4.8 .19  0 true 6.6   160 77    2 timeout 900   4300 11000 0 out of memory 43    15000 520   0 disqualified .055 9.4 .39 0 true 1.4   19 17    2 true 36   880 300 2 error (5) .028 5.6 .14  0 error (5) .024 5.6 .22  0
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c out of memory 110     15000 670    0 out of memory 860   15000 5400 0 true 18     150   250    2 out of memory 160     15000   1900    0 timeout 900   4300 13000 0 unknown 42    200 520   0 unknown .028 4.6 .27  0 unknown .055 4.5 .14  0 true 6.4   160 83    2 timeout 900   4200 11000 0 out of memory 44    15000 730   0 disqualified .046 9.6 .35 0 true 1.0   18 13    2 true 60   1200 490 2 error (5) .048 5.6 .11  0 error (5) .028 5.6 .25  0
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c out of memory 110     15000 900    0 out of memory 810   15000 4900 0 true 16     140   220    2 out of memory 160     15000   1900    0 timeout 900   4900 11000 0 unknown 5.7  67 74   0 unknown .032 4.6 .22  0 unknown .031 4.5 .18  0 true 5.6   140 62    2 timeout 900   4200 11000 0 out of memory 43    15000 540   0 disqualified .048 9.9 .41 0 true 1.4   19 19    2 true 36   920 290 2 error (5) .025 5.6 .15  0 error (5) .024 5.6 .085 0
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c out of memory 110     15000 980    0 out of memory 850   15000 4800 0 true 17     140   220    2 out of memory 160     15000   1900    0 timeout 900   4000 13000 0 unknown 38    180 460   0 unknown .055 4.7 .16  0 unknown .029 4.7 .26  0 true 5.6   140 64    2 timeout 900   4300 11000 0 out of memory 44    15000 540   0 disqualified .050 9.6 .41 0 true 1.0   18 16    2 true 36   900 280 2 error (5) .027 5.6 .13  0 error (5) .025 5.6 .12  0
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .18  24 1.6  0 timeout 900   2600 13000 0 error (42) 880     870   8300    0 out of memory 140     15000   1700    0 false(termination) 12   490 110 1 unknown .96 66 11   0 unknown .031 4.6 .16  0 unknown .030 4.6 .17  0 timeout 900     2500 10000    0 false(termination) 13   580 110 1 timeout 900    1700 11000   0 disqualified .071 9.4 .39 0 timeout (verification) 900     59 10000    0 false(termination) 13   500 120 1 error (5) .032 5.6 .12  0 error (5) .025 5.5 .17  0
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .18  25 1.5  1 timeout 900   2200 11000 0 error (42) 880     1000   9800    0 out of memory 130     15000   1900    0 false(termination) 18   1000 140 1 unknown 1.0  68 12   0 unknown .031 4.6 .21  0 unknown .028 4.6 .14  0 timeout 900     2600 8300    0 false(termination) 15   770 160 1 timeout 900    1900 13000   0 disqualified .042 9.4 .50 0 timeout (verification) 900     59 11000    0 false(termination) 13   590 110 1 error (5) .022 5.6 .21  0 error (5) .028 5.6 .16  0
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .19  25 1.4  0 timeout 900   3500 8900 0 error (42) 880     1200   8600    0 out of memory 130     15000   1600    0 false(termination) 22   1400 200 1 unknown 1.1  67 13   0 unknown .027 4.7 .30  0 unknown .038 4.6 .23  0 timeout 900     2700 8800    0 false(termination) 22   1100 200 1 timeout 900    1900 11000   0 disqualified .068 9.3 .40 0 timeout (verification) 900     59 9600    0 false(termination) 16   790 120 1 error (5) .027 5.6 .23  0 error (5) .025 5.6 .18  0
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .20  25 1.5  1 timeout 900   2500 9900 0 error (42) 880     1400   9700    0 out of memory 120     15000   1600    0 false(termination) 32   2100 340 1 unknown 1.1  66 11   0 unknown .032 4.6 .18  0 unknown .031 4.6 .20  0 timeout 900     2900 11000    0 false(termination) 35   1900 340 1 timeout 900    2000 12000   0 disqualified .047 9.2 .41 0 timeout (verification) 900     60 11000    0 false(termination) 18   1000 160 1 error (5) .021 5.6 .15  0 error (5) .026 5.6 .12  0
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(termination) .21  25 1.6  0 timeout 900   2500 12000 0 error (42) 880     460   8700    0 out of memory 230     15000   3100    0 false(termination) 6.2 310 55 1 unknown .63 66 6.1 0 unknown .043 4.6 .18  0 unknown .027 4.7 .27  0 timeout 900     2900 7200    0 false(termination) 6.2 350 50 1 timeout 900    2100 11000   0 disqualified .049 9.6 .42 0 timeout (verification) 900     60 10000    0 false(termination) 16   830 130 1 error (5) .024 5.6 .11  0 error (5) .023 5.9 .11  0
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .19  25 1.8  0 timeout 900   2500 13000 0 error (42) 880     1400   9600    0 out of memory 100     15000   1100    0 false(termination) 55   3300 550 1 unknown 1.1  68 13   0 unknown .025 4.6 .17  0 unknown .032 4.6 .28  0 timeout 900     2900 7800    0 false(termination) 61   3600 660 1 timeout 900    2100 12000   0 disqualified .047 9.4 .34 0 timeout (verification) 900     59 9500    0 false(termination) 28   2300 220 1 error (5) .045 5.6 .14  0 error (5) .023 5.7 .13  0
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(termination) .24  25 2.1  0 timeout 900   2500 12000 0 error (42) 880     520   11000    0 out of memory 83     15000   1100    0 false(termination) 31   1900 320 1 unknown .62 65 5.8 0 unknown .032 4.6 .17  0 unknown .037 4.6 .13  0 timeout 900     3100 8300    0 false(termination) 37   2200 370 1 timeout 900    2200 12000   0 disqualified .044 9.4 .41 0 timeout (verification) 900     60 11000    0 false(termination) 20   1300 160 1 error (5) .038 5.5 .15  0 error (5) .027 5.6 .15  0
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .25  25 1.6  0 timeout 900   2500 11000 0 error (42) 880     460   8400    0 out of memory 84     15000   1200    0 false(termination) 110   4900 940 1 unknown 1.2  74 13   0 unknown .061 4.7 .23  0 unknown .033 4.6 .18  0 timeout 900     3000 9400    0 false(termination) 130   5200 1200 1 timeout 900    2200 14000   0 disqualified .047 9.3 .33 0 timeout (verification) 900     58 11000    0 false(termination) 49   3600 300 1 error (5) .028 5.6 .15  0 error (5) .023 5.7 .15  0
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .15  24 1.4  1 false(termination) 130   4000 830 0 error (42) 880     950   8500    0 out of memory 130     15000   1800    0 false(termination) 5.0 290 42 1 unknown .86 67 9.1 0 unknown .030 4.6 .17  0 unknown .028 4.6 .17  0 timeout 900     1900 8500    0 false(termination) 5.1 290 40 1 timeout 900    1200 11000   0 disqualified .048 9.6 .40 0 timeout (verification) 900     60 10000    0 false(termination) 9.3 360 73 1 error (5) .031 5.6 .14  0 error (5) .030 5.6 .098 0
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .15  24 2.2  0 false(termination) 330   7300 1900 0 error (42) 880     1300   8900    0 out of memory 83     15000   1000    0 false(termination) 5.4 320 54 1 unknown .89 68 9.8 0 unknown .030 4.6 .24  0 unknown .032 4.6 .20  0 timeout 900     2000 8200    0 false(termination) 5.7 330 45 1 timeout 900    1300 10000   0 disqualified .049 9.1 .47 0 timeout (verification) 900     60 13000    0 false(termination) 9.1 380 69 1 error (5) .039 5.5 .093 0 error (5) .024 5.6 .15  0
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .17  24 1.4  1 false(termination) 600   7000 4500 0 error (42) 880     1500   12000    0 out of memory 89     15000   1100    0 false(termination) 6.4 420 59 1 unknown .90 66 9.7 0 unknown .030 4.7 .17  0 unknown .030 4.6 .24  0 timeout 900     2200 8400    0 false(termination) 6.5 420 63 1 timeout 900    1400 11000   0 disqualified .053 9.1 .43 0 timeout (verification) 900     58 9700    0 false(termination) 9.8 380 75 1 error (5) .030 5.6 .099 0 error (5) .024 5.6 .14  0
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .18  24 1.1  0 timeout 910   9100 8200 0 error (42) 880     580   10000    0 out of memory 100     15000   1300    0 false(termination) 7.5 330 66 1 unknown .92 66 11   0 unknown .029 4.6 .25  0 unknown .036 4.5 .23  0 timeout 900     2300 8600    0 false(termination) 8.1 360 71 1 timeout 900    1500 14000   0 disqualified .045 9.4 .50 0 timeout (verification) 900     60 12000    0 false(termination) 11   440 90 1 error (5) .030 5.7 .20  0 error (5) .046 5.5 .11  0
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) .17  24 1.3  1 timeout 900   2300 11000 0 error (42) 880     710   9000    0 out of memory 160     15000   2500    0 false(termination) 9.7 480 85 1 unknown .95 66 12   0 unknown .033 4.7 .16  0 unknown .036 4.6 .27  0 timeout 900     2400 11000    0 false(termination) 11   540 100 1 timeout 900    1600 12000   0 disqualified .044 9.0 .39 0 timeout (verification) 900     60 10000    0 false(termination) 11   510 100 1 error (5) .026 5.7 .14  0 error (5) .021 5.6 .13  0
ssh-simplified/s3_clnt_3.cil_true-unreach-call_true-termination.c out of memory 110     15000 1000    0 out of memory 580   15000 3100 0 true 14     100   190    2 out of memory 160     15000   1800    0 true 130   4000 1100 2 unknown 31    130 430   0 unknown .033 4.6 .16  0 unknown .053 4.6 .17  0 true 4.1   100 52    2 true 720   4100 8900 2 out of memory 47    15000 650   0 disqualified .043 9.4 .48 0 true .21  20 1.9  2 true 38   960 300 2 error (5) .023 5.6 .10  0 error (5) .020 5.5 .25  0
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c error (134) 18     1400 90    0 timeout 3.3 160 1100 0 error (42) 880     3600   11000    0 out of memory 540     15000   4300    0 timeout 900   4600 11000 0 unknown 900    1100 13000   0 unknown .032 4.6 .21  0 unknown .033 4.6 .20  0 timeout 900     8400 8000    0 timeout 900   4800 12000 0 error (8) 4.8  440 54   0 disqualified .049 9.4 .42 0 error(unknown, verification-finished) 1.2   35 16    0 true 75   1100 870 2 error (5) .024 5.7 .099 0 error (5) .028 5.6 .23  0
eca-rers2012/Problem01_label00_true-unreach-call_false-termination.c false(termination) .86  88 6.7  1 timeout 900   8100 8400 0 error (42) 880     1300   7400    0 out of memory 380     15000   5500    0 false(termination) 29   740 230 1 unknown 3.9  150 43   0 unknown .029 4.7 .17  0 unknown .029 4.6 .23  0 timeout 900     2900 11000    0 false(termination) 22   690 180 1 out of memory 330    15000 4300   0 disqualified .041 9.0 .48 0 timeout (verification) 900     6400 5400    0 timeout 910   13000 4300 0 error (5) .031 5.6 .16  0 error (5) .031 5.6 .21  0
eca-rers2012/Problem01_label01_true-unreach-call_false-termination.c false(termination) .80  88 7.4  1 timeout 900   8100 7400 0 error (42) 880     1300   7200    0 out of memory 380     15000   5100    0 false(termination) 29   950 240 1 unknown 3.9  140 49   0 unknown .029 4.7 .18  0 unknown .026 4.5 .24  0 timeout 900     2700 9600    0 false(termination) 23   700 180 1 out of memory 320    15000 4300   0 disqualified .045 9.0 .44 0 timeout (verification) 900     6400 5400    0 timeout 910   14000 4300 0 error (5) .024 5.6 .17  0 error (5) .027 5.6 .10  0
eca-rers2012/Problem01_label02_true-unreach-call_false-termination.c false(termination) .78  88 8.3  1 timeout 900   7800 8500 0 error (42) 880     1300   7800    0 out of memory 380     15000   4700    0 false(termination) 30   800 260 1 unknown 4.0  150 45   0 unknown .051 4.5 .17  0 unknown .039 4.7 .27  0 timeout 900     2800 9000    0 false(termination) 23   700 170 1 out of memory 320    15000 4100   0 disqualified .048 9.1 .39 0 timeout (verification) 900     6400 4700    0 timeout 910   14000 4000 0 error (5) .023 5.7 .19  0 error (5) .049 5.5 .11  0
eca-rers2012/Problem01_label03_true-unreach-call_false-termination.c false(termination) .81  88 7.2  1 timeout 900   8300 8400 0 error (42) 880     1300   8000    0 out of memory 380     15000   4900    0 false(termination) 30   770 250 1 unknown 3.8  150 48   0 unknown .028 4.6 .25  0 unknown .045 4.5 .18  0 timeout 900     2800 9800    0 false(termination) 23   700 190 1 out of memory 320    15000 3800   0 disqualified .064 9.2 .46 0 timeout (verification) 900     6700 6900    0 timeout 910   14000 4300 0 error (5) .021 5.7 .13  0 error (5) .025 5.6 .094 0
eca-rers2012/Problem01_label04_true-unreach-call_false-termination.c false(termination) .81  88 6.9  1 timeout 900   8100 7600 0 error (42) 880     1300   7500    0 out of memory 390     15000   5100    0 false(termination) 28   870 230 1 unknown 4.1  150 42   0 unknown .033 4.8 .26  0 unknown .034 4.5 .26  0 timeout 900     2800 8700    0 false(termination) 23   690 200 1 out of memory 320    15000 3900   0 disqualified .050 9.4 .42 0 timeout (verification) 900     6500 5700    0 timeout 910   13000 4300 0 error (5) .034 5.7 .16  0 error (5) .024 5.5 .14  0
eca-rers2012/Problem01_label05_true-unreach-call_false-termination.c false(termination) .81  88 7.4  1 timeout 900   8200 7600 0 error (42) 880     1300   7800    0 out of memory 380     15000   5400    0 false(termination) 30   780 230 1 unknown 4.9  150 49   0 unknown .028 4.6 .26  0 unknown .035 4.6 .22  0 timeout 900     2800 10000    0 false(termination) 22   680 180 1 out of memory 320    15000 4100   0 disqualified .049 9.3 .44 0 timeout (verification) 900     6500 6600    0 timeout 910   13000 4400 0 error (5) .051 5.7 .13  0 error (5) .027 5.5 .20  0
eca-rers2012/Problem01_label06_true-unreach-call_false-termination.c false(termination) .80  87 7.3  1 timeout 900   8100 7200 0 error (42) 880     1300   7300    0 out of memory 380     15000   5600    0 false(termination) 29   970 240 1 unknown 4.2  150 53   0 unknown .038 4.6 .26  0 unknown .046 4.6 .20  0 timeout 900     2800 9700    0 false(termination) 23   690 190 1 out of memory 320    15000 4000   0 disqualified .073 9.1 .54 0 timeout (verification) 900     6600 5100    0 timeout 910   14000 4800 0 error (5) .023 5.6 .16  0 error (5) .026 5.6 .17  0
eca-rers2012/Problem01_label07_true-unreach-call_false-termination.c false(termination) .85  88 6.7  1 timeout 900   8100 7900 0 error (42) 880     1300   10000    0 out of memory 380     15000   4400    0 false(termination) 30   760 250 1 unknown 4.3  150 50   0 unknown .027 4.6 .20  0 unknown .054 4.5 .16  0 timeout 900     2800 9700    0 false(termination) 23   710 210 1 out of memory 320    15000 3600   0 disqualified .042 9.6 .42 0 timeout (verification) 900     6400 6300    0 timeout 910   14000 4200 0 error (5) .026 5.5 .18  0 error (5) .031 5.7 .18  0
eca-rers2012/Problem01_label08_true-unreach-call_false-termination.c false(termination) .78  88 9.1  1 timeout 900   8200 8400 0 error (42) 880     1300   7300    0 out of memory 380     15000   4700    0 false(termination) 30   770 260 1 unknown 4.2  150 63   0 unknown .028 4.7 .25  0 unknown .028 4.6 .20  0 timeout 900     2800 8700    0 false(termination) 22   710 190 1 out of memory 320    15000 4200   0 disqualified .046 9.3 .44 0 timeout (verification) 900     6500 5700    0 timeout 910   14000 4900 0 error (5) .024 5.6 .15  0 error (5) .025 5.7 .14  0
eca-rers2012/Problem01_label09_true-unreach-call_false-termination.c false(termination) .84  88 6.7  1 timeout 900   8500 8800 0 error (42) 880     1300   8200    0 out of memory 380     15000   5300    0 false(termination) 30   770 250 1 unknown 4.1  140 45   0 unknown .030 4.7 .22  0 unknown .051 4.6 .15  0 timeout 900     2800 11000    0 false(termination) 22   680 180 1 out of memory 320    15000 4400   0 disqualified .046 9.7 .48 0 timeout (verification) 900     6600 6800    0 timeout 910   13000 4300 0 error (5) .028 5.7 .14  0 error (5) .026 5.6 .14  0
eca-rers2012/Problem01_label10_true-unreach-call_false-termination.c false(termination) .88  88 6.8  1 timeout 900   8600 8700 0 error (42) 880     1300   9000    0 out of memory 380     15000   6200    0 false(termination) 30   770 250 1 unknown 4.2  140 64   0 unknown .052 4.7 .12  0 unknown .031 4.7 .16  0 timeout 900     2700 9600    0 false(termination) 23   690 210 1 out of memory 320    15000 4400   0 disqualified .046 9.2 .36 0 timeout (verification) 900     6500 6000    0 timeout 910   14000 4100 0 error (5) .028 5.5 .13  0 error (5) .039 5.7 .12  0
eca-rers2012/Problem01_label11_true-unreach-call_false-termination.c false(termination) .88  88 6.5  1 timeout 900   8100 8500 0 error (42) 880     1300   6800    0 out of memory 380     15000   5000    0 false(termination) 29   760 260 1 unknown 4.4  150 61   0 unknown .026 4.6 .25  0 unknown .035 4.6 .23  0 timeout 900     2900 10000    0 false(termination) 22   680 210 1 out of memory 320    15000 3600   0 disqualified .046 9.4 .46 0 timeout (verification) 900     6500 5200    0 timeout 910   14000 4200 0 error (5) .060 5.7 .14  0 error (5) .028 5.5 .17  0
eca-rers2012/Problem01_label12_true-unreach-call_false-termination.c false(termination) .82  88 6.9  1 timeout 900   8100 7500 0 error (42) 880     1300   7900    0 out of memory 380     15000   5200    0 false(termination) 31   740 280 1 unknown 4.2  150 58   0 unknown .030 4.7 .21  0 unknown .028 4.7 .40  0 timeout 900     2800 10000    0 false(termination) 23   700 180 1 out of memory 320    15000 4100   0 disqualified .042 9.5 .44 0 timeout (verification) 900     6600 6300    0 timeout 900   13000 4200 0 error (5) .020 5.6 .26  0 error (5) .037 5.5 .15  0
eca-rers2012/Problem01_label13_true-unreach-call_false-termination.c false(termination) .80  88 7.4  1 timeout 900   8200 7300 0 error (42) 880     1300   7300    0 out of memory 380     15000   4600    0 false(termination) 32   910 240 1 unknown 4.0  150 51   0 unknown .028 4.6 .18  0 unknown .033 4.6 .27  0 timeout 900     2700 8700    0 false(termination) 22   710 200 1 out of memory 320    15000 4200   0 disqualified .054 9.2 .40 0 timeout (verification) 900     6600 5900    0 timeout 910   14000 4700 0 error (5) .025 5.6 .25  0 error (5) .031 5.6 .095 0
eca-rers2012/Problem01_label14_true-unreach-call_false-termination.c false(termination) .87  88 6.2  1 timeout 900   7900 8900 0 error (42) 880     1300   9700    0 out of memory 380     15000   5200    0 false(termination) 29   780 230 1 unknown 4.1  150 45   0 unknown .029 4.6 .23  0 unknown .033 4.6 .19  0 timeout 900     2800 8200    0 false(termination) 22   710 180 1 out of memory 320    15000 4200   0 disqualified .043 9.6 .49 0 timeout (verification) 900     6500 5900    0 timeout 910   13000 4800 0 error (5) .027 5.7 .14  0 error (5) .021 5.6 .16  0
eca-rers2012/Problem01_label15_false-unreach-call_false-termination.c false(termination) .82  88 7.0  1 timeout 900   8100 8100 0 error (42) 880     1300   8600    0 out of memory 380     15000   5400    0 false(termination) 30   910 240 1 unknown 6.5  90 87   0 unknown .057 4.7 .17  0 unknown .028 4.6 .22  0 timeout 900     2800 9100    0 false(termination) 23   700 210 1 out of memory 320    15000 4300   0 disqualified .062 9.2 .34 0 timeout (verification) 900     6500 5300    0 timeout 910   13000 4400 0 error (5) .024 5.6 .13  0 error (5) .023 5.6 .20  0
eca-rers2012/Problem01_label16_true-unreach-call_false-termination.c false(termination) .80  88 8.0  1 timeout 900   8100 7700 0 error (42) 870     1300   7600    0 out of memory 380     15000   5300    0 false(termination) 29   760 250 1 unknown 4.6  140 60   0 unknown .031 4.6 .17  0 unknown .029 4.7 .20  0 timeout 900     2900 10000    0 false(termination) 23   700 180 1 out of memory 320    15000 4200   0 disqualified .051 9.7 .51 0 timeout (verification) 900     6600 7700    0 timeout 910   14000 4400 0 error (5) .024 5.6 .13  0 error (5) .034 5.5 .082 0
eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c false(termination) .82  88 8.5  1 timeout 900   8100 9000 0 error (42) 880     1300   8000    0 out of memory 380     15000   5700    0 false(termination) 29   740 230 1 unknown 4.2  150 46   0 unknown .035 4.6 .22  0 unknown .058 4.5 .20  0 timeout 900     2900 11000    0 false(termination) 22   710 170 1 out of memory 320    15000 4000   0 disqualified .061 9.5 .47 0 timeout (verification) 900     6500 6200    0 timeout 910   13000 4900 0 error (5) .026 5.6 .14  0 error (5) .025 5.6 .12  0
eca-rers2012/Problem01_label18_true-unreach-call_false-termination.c false(termination) .82  88 6.9  1 timeout 900   8100 7600 0 error (42) 880     1300   8100    0 out of memory 380     15000   5600    0 false(termination) 29   790 270 1 unknown 4.5  150 58   0 unknown .030 4.5 .19  0 unknown .032 4.6 .19  0 timeout 900     2900 9400    0 false(termination) 22   690 200 1 out of memory 320    15000 4000   0 disqualified .073 9.0 .39 0 timeout (verification) 900     6600 6400    0 timeout 910   14000 4200 0 error (5) .027 5.6 .17  0 error (5) .026 5.5 .24  0
eca-rers2012/Problem01_label19_true-unreach-call_false-termination.c false(termination) .83  88 7.3  1 timeout 900   8200 8200 0 error (42) 880     1300   7800    0 out of memory 380     15000   5500    0 false(termination) 30   750 250 1 unknown 4.0  150 46   0 unknown .053 4.6 .19  0 unknown .036 4.6 .26  0 timeout 900     2700 9700    0 false(termination) 23   710 170 1 out of memory 320    15000 4100   0 disqualified .046 9.1 .41 0 timeout (verification) 900     6500 5400    0 timeout 900   14000 4800 0 error (5) .025 5.7 .14  0 error (5) .029 5.5 .091 0
eca-rers2012/Problem01_label20_false-unreach-call_false-termination.c false(termination) .80  88 7.2  1 timeout 900   8100 7100 0 error (42) 880     1300   9500    0 out of memory 380     15000   5600    0 false(termination) 30   760 260 1 unknown 12    110 170   0 unknown .031 4.6 .20  0 unknown .026 4.6 .19  0 timeout 900     2900 9200    0 false(termination) 22   700 200 1 out of memory 320    15000 4800   0 disqualified .052 9.5 .46 0 timeout (verification) 900     6500 4900    0 timeout 900   13000 4100 0 error (5) .026 5.6 .083 0 error (5) .025 5.6 .18  0
eca-rers2012/Problem01_label21_false-unreach-call_false-termination.c false(termination) .80  88 8.3  1 timeout 900   8500 8400 0 error (42) 880     1300   7600    0 out of memory 390     15000   5100    0 false(termination) 28   760 240 1 unknown 6.4  89 70   0 unknown .028 4.6 .27  0 unknown .029 4.8 .23  0 timeout 900     2800 9200    0 false(termination) 23   660 180 1 out of memory 320    15000 4500   0 disqualified .043 9.7 .45 0 timeout (verification) 900     6500 5300    0 timeout 910   13000 4200 0 error (5) .025 5.6 .16  0 error (5) .033 5.6 .13  0
eca-rers2012/Problem01_label22_true-unreach-call_false-termination.c false(termination) .79  88 8.8  1 timeout 900   7900 8000 0 error (42) 880     1300   11000    0 out of memory 380     15000   5500    0 false(termination) 29   920 270 1 unknown 4.3  150 51   0 unknown .029 4.8 .17  0 unknown .028 4.6 .17  0 timeout 900     2800 9500    0 false(termination) 22   700 190 1 out of memory 320    15000 4300   0 disqualified .050 9.4 .39 0 timeout (verification) 900     6500 5700    0 timeout 910   14000 4600 0 error (5) .027 5.6 .21  0 error (5) .026 5.6 .10  0
eca-rers2012/Problem01_label23_true-unreach-call_false-termination.c false(termination) .85  88 6.6  1 timeout 900   8100 8500 0 error (42) 880     1300   7900    0 out of memory 380     15000   4700    0 false(termination) 30   750 260 1 unknown 4.6  150 61   0 unknown .028 4.7 .17  0 unknown .029 4.5 .22  0 timeout 900     2900 9800    0 false(termination) 23   680 210 1 out of memory 320    15000 4100   0 disqualified .062 9.4 .35 0 timeout (verification) 900     6500 5000    0 timeout 910   14000 4500 0 error (5) .025 5.6 .13  0 error (5) .024 5.6 .091 0
eca-rers2012/Problem01_label24_true-unreach-call_false-termination.c false(termination) .86  88 6.2  1 timeout 900   8100 8600 0 error (42) 880     1300   8400    0 out of memory 380     15000   5000    0 false(termination) 30   940 250 1 unknown 4.1  150 45   0 unknown .028 4.8 .25  0 unknown .030 4.7 .14  0 timeout 900     2800 10000    0 false(termination) 22   700 190 1 out of memory 320    15000 4300   0 disqualified .072 9.6 .40 0 timeout (verification) 900     6500 6000    0 timeout 910   14000 4000 0 error (5) .044 5.5 .11  0 error (5) .032 5.7 .12  0
eca-rers2012/Problem01_label25_true-unreach-call_false-termination.c false(termination) .79  88 7.1  1 timeout 900   8100 8100 0 error (42) 880     1300   7200    0 out of memory 380     15000   5700    0 false(termination) 30   890 270 1 unknown 4.0  140 46   0 unknown .039 4.7 .20  0 unknown .029 4.8 .21  0 timeout 900     2700 10000    0 false(termination) 22   710 170 1 out of memory 320    15000 5200   0 disqualified .064 9.2 .37 0 timeout (verification) 900     6400 6500    0 timeout 910   13000 4200 0 error (5) .022 5.6 .10  0 error (5) .036 5.5 .17  0
eca-rers2012/Problem01_label26_true-unreach-call_false-termination.c false(termination) .83  88 6.7  1 timeout 900   8100 6900 0 error (42) 870     1300   7600    0 out of memory 380     15000   5100    0 false(termination) 31   920 280 1 unknown 4.2  150 49   0 unknown .055 4.5 .14  0 unknown .030 4.6 .23  0 timeout 900     2800 8900    0 false(termination) 22   690 190 1 out of memory 320    15000 4600   0 disqualified .045 9.5 .41 0 timeout (verification) 900     6500 6400    0 timeout 910   14000 4500 0 error (5) .023 5.6 .18  0 error (5) .027 5.6 .31  0
eca-rers2012/Problem01_label27_true-unreach-call_false-termination.c false(termination) .82  88 6.8  1 timeout 900   8100 8200 0 error (42) 880     1300   6800    0 out of memory 380     15000   5000    0 false(termination) 30   940 280 1 unknown 3.8  150 51   0 unknown .029 4.5 .23  0 unknown .028 4.6 .27  0 timeout 900     2800 9000    0 false(termination) 22   720 190 1 out of memory 320    15000 4200   0 disqualified .051 9.1 .40 0 timeout (verification) 900     6500 5400    0 timeout 910   13000 4300 0 error (5) .024 5.6 .13  0 error (5) .031 5.6 .13  0
eca-rers2012/Problem01_label28_true-unreach-call_false-termination.c false(termination) .82  88 7.5  1 timeout 900   7900 6900 0 error (42) 880     1300   7700    0 out of memory 380     15000   6200    0 false(termination) 31   750 260 1 unknown 4.0  150 51   0 unknown .049 4.5 .27  0 unknown .031 4.5 .35  0 timeout 900     2800 10000    0 false(termination) 22   710 180 1 out of memory 320    15000 4300   0 disqualified .048 9.3 .43 0 timeout (verification) 900     6500 4900    0 timeout 910   14000 4300 0 error (5) .043 5.7 .18  0 error (5) .026 5.6 .095 0
eca-rers2012/Problem01_label29_true-unreach-call_false-termination.c false(termination) .80  88 9.4  1 timeout 900   8100 7500 0 error (42) 880     1300   7700    0 out of memory 380     15000   5600    0 false(termination) 30   920 250 1 unknown 4.2  150 54   0 unknown .030 4.6 .19  0 unknown .032 4.6 .21  0 timeout 900     2800 9500    0 false(termination) 23   680 200 1 out of memory 320    15000 4300   0 disqualified .053 9.5 .36 0 timeout (verification) 900     6500 7800    0 timeout 910   14000 4400 0 error (5) .031 5.6 .19  0 error (5) .025 5.6 .13  0
eca-rers2012/Problem01_label30_true-unreach-call_false-termination.c false(termination) .85  88 7.0  1 timeout 900   8100 8400 0 error (42) 880     1300   7700    0 out of memory 380     15000   5100    0 false(termination) 30   750 260 1 unknown 4.0  150 48   0 unknown .031 4.6 .15  0 unknown .028 4.6 .23  0 timeout 900     2900 12000    0 false(termination) 22   690 190 1 out of memory 320    15000 5000   0 disqualified .046 9.3 .42 0 timeout (verification) 900     6600 5700    0 timeout 910   14000 4500 0 error (5) .027 5.5 .26  0 error (5) .030 5.6 .20  0
eca-rers2012/Problem01_label31_true-unreach-call_false-termination.c false(termination) .85  88 7.1  1 timeout 900   8100 8000 0 error (42) 880     1300   7600    0 out of memory 380     15000   5200    0 false(termination) 31   750 270 1 unknown 3.7  150 48   0 unknown .027 4.5 .19  0 unknown .027 4.6 .17  0 timeout 900     2800 8500    0 false(termination) 23   700 200 1 out of memory 320    15000 3900   0 disqualified .051 9.2 .41 0 timeout (verification) 900     6500 5600    0 timeout 910   14000 4800 0 error (5) .032 5.7 .21  0 error (5) .030 5.6 .21  0
eca-rers2012/Problem01_label32_false-unreach-call_false-termination.c false(termination) .82  88 7.1  1 timeout 900   8100 7800 0 error (42) 880     1300   8300    0 out of memory 380     15000   5400    0 false(termination) 29   770 270 1 unknown 12    110 180   0 unknown .027 4.6 .13  0 unknown .033 4.7 .20  0 timeout 900     2800 9500    0 false(termination) 22   660 180 1 out of memory 320    15000 3900   0 disqualified .046 9.2 .42 0 timeout (verification) 900     6500 5400    0 timeout 910   14000 4200 0 error (5) .026 5.6 .15  0 error (5) .048 5.5 .094 0
eca-rers2012/Problem01_label33_false-unreach-call_false-termination.c false(termination) .82  88 6.9  1 timeout 900   8100 7200 0 error (42) 880     1300   7800    0 out of memory 380     15000   4800    0 false(termination) 31   760 250 1 unknown 9.3  98 110   0 unknown .027 4.8 .25  0 unknown .037 4.7 .27  0 timeout 900     2900 12000    0 false(termination) 22   700 190 1 out of memory 320    15000 4700   0 disqualified .044 9.6 .42 0 timeout (verification) 900     6600 5600    0 timeout 910   14000 4500 0 error (5) .049 5.8 .10  0 error (5) .024 5.6 .14  0
eca-rers2012/Problem01_label34_true-unreach-call_false-termination.c false(termination) .85  88 6.9  1 timeout 900   7900 8400 0 error (42) 880     1300   7200    0 out of memory 380     15000   5000    0 false(termination) 28   740 270 1 unknown 4.3  150 52   0 unknown .029 4.6 .23  0 unknown .029 4.7 .20  0 timeout 900     2800 11000    0 false(termination) 22   700 200 1 out of memory 320    15000 3800   0 disqualified .048 9.0 .42 0 timeout (verification) 900     6500 6200    0 timeout 910   13000 4100 0 error (5) .025 5.7 .11  0 error (5) .021 5.7 .18  0
eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c false(termination) .81  88 7.0  1 timeout 900   8100 8800 0 error (42) 880     1300   7800    0 out of memory 380     15000   5600    0 false(termination) 29   760 250 1 unknown 6.8  88 96   0 unknown .055 4.6 .15  0 unknown .031 4.6 .28  0 timeout 900     2900 9200    0 false(termination) 22   700 170 1 out of memory 320    15000 4600   0 disqualified .045 9.5 .39 0 timeout (verification) 900     6600 5700    0 timeout 910   13000 4500 0 error (5) .048 5.5 .23  0 error (5) .022 5.6 .13  0
eca-rers2012/Problem01_label36_true-unreach-call_false-termination.c false(termination) .77  88 8.3  1 timeout 900   8100 8900 0 error (42) 880     1300   7900    0 out of memory 390     15000   5000    0 false(termination) 29   740 240 1 unknown 4.2  140 55   0 unknown .038 4.6 .15  0 unknown .032 4.6 .18  0 timeout 900     2900 11000    0 false(termination) 23   660 190 1 out of memory 320    15000 4600   0 disqualified .048 9.1 .39 0 timeout (verification) 900     6600 5800    0 timeout 910   13000 4900 0 error (5) .037 5.4 .15  0 error (5) .022 5.6 .17  0
eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c false(termination) .83  88 7.0  1 timeout 900   8000 8200 0 error (42) 880     1300   7200    0 out of memory 380     15000   5400    0 false(termination) 32   920 250 1 unknown 8.8  96 100   0 unknown .029 4.6 .21  0 unknown .027 4.5 .25  0 timeout 900     2800 11000    0 false(termination) 23   720 200 1 out of memory 320    15000 3600   0 disqualified .044 9.6 .39 0 timeout (verification) 900     6500 6000    0 timeout 910   14000 4700 0 error (5) .024 5.7 .15  0 error (5) .029 5.7 .15  0
eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c false(termination) .86  88 6.6  1 timeout 900   8100 7800 0 error (42) 880     1300   7900    0 out of memory 380     15000   5600    0 false(termination) 29   760 230 1 unknown 6.6  90 84   0 unknown .029 4.6 .18  0 unknown .033 4.6 .16  0 timeout 900     2800 10000    0 false(termination) 23   700 190 1 out of memory 320    15000 4100   0 disqualified .046 9.5 .38 0 timeout (verification) 900     6600 5700    0 timeout 910   13000 4800 0 error (5) .038 5.5 .081 0 error (5) .025 5.6 .16  0
eca-rers2012/Problem01_label39_true-unreach-call_false-termination.c false(termination) .83  88 8.2  1 timeout 900   8000 6900 0 error (42) 880     1300   7200    0 out of memory 380     15000   5600    0 false(termination) 30   760 250 1 unknown 3.9  140 47   0 unknown .030 4.7 .24  0 unknown .033 4.7 .13  0 timeout 900     2700 10000    0 false(termination) 24   680 180 1 out of memory 320    15000 4300   0 disqualified .048 9.2 .37 0 timeout (verification) 900     6500 5600    0 timeout 910   14000 4900 0 error (5) .027 5.6 .17  0 error (5) .051 5.6 .16  0
eca-rers2012/Problem01_label40_true-unreach-call_false-termination.c false(termination) .79  88 8.0  1 timeout 900   8100 7300 0 error (42) 880     1300   7700    0 out of memory 380     15000   4800    0 false(termination) 30   740 240 1 unknown 4.3  150 50   0 unknown .055 4.6 .14  0 unknown .028 4.5 .19  0 timeout 900     2800 9500    0 false(termination) 22   710 180 1 out of memory 320    15000 4600   0 disqualified .047 9.3 .42 0 timeout (verification) 900     6500 6100    0 timeout 910   14000 4500 0 error (5) .018 5.6 .085 0 error (5) .026 5.6 .15  0
eca-rers2012/Problem01_label41_true-unreach-call_false-termination.c false(termination) .80  88 7.2  1 timeout 900   8200 7600 0 error (42) 880     1300   8300    0 out of memory 380     15000   5000    0 false(termination) 28   740 230 1 unknown 3.9  150 43   0 unknown .031 4.6 .30  0 unknown .048 4.6 .17  0 timeout 900     2900 9600    0 false(termination) 23   690 190 1 out of memory 320    15000 4000   0 disqualified .046 9.3 .54 0 timeout (verification) 900     6600 7000    0 timeout 910   14000 4200 0 error (5) .047 5.5 .081 0 error (5) .026 5.6 .12  0
eca-rers2012/Problem01_label42_true-unreach-call_false-termination.c false(termination) .80  88 7.1  1 timeout 900   8100 7500 0 error (42) 880     1300   9500    0 out of memory 380     15000   4500    0 false(termination) 30   730 260 1 unknown 4.0  140 45   0 unknown .030 4.6 .22  0 unknown .045 4.5 .16  0 timeout 900     2900 12000    0 false(termination) 23   720 190 1 out of memory 320    15000 4600   0 disqualified .063 9.1 .48 0 timeout (verification) 900     6600 7000    0 timeout 910   13000 4300 0 error (5) .028 5.5 .17  0 error (5) .032 5.5 .13  0
eca-rers2012/Problem01_label43_true-unreach-call_false-termination.c false(termination) .80  88 7.0  1 timeout 900   8200 7500 0 error (42) 880     1300   7700    0 out of memory 380     15000   5800    0 false(termination) 30   770 240 1 unknown 4.1  150 53   0 unknown .030 4.8 .18  0 unknown .028 4.6 .20  0 timeout 900     2800 9200    0 false(termination) 22   690 190 1 out of memory 320    15000 3600   0 disqualified .048 9.2 .42 0 timeout (verification) 900     6400 5200    0 timeout 910   14000 4800 0 error (5) .023 5.6 .17  0 error (5) .025 5.6 .14  0
eca-rers2012/Problem01_label44_false-unreach-call_false-termination.c false(termination) .84  88 7.4  1 timeout 900   8100 7100 0 error (42) 880     1300   7300    0 out of memory 380     15000   5800    0 false(termination) 28   920 270 1 unknown 4.5  80 56   0 unknown .031 4.6 .24  0 unknown .029 4.6 .21  0 timeout 900     2900 12000    0 false(termination) 23   680 180 1 out of memory 320    15000 4600   0 disqualified .044 9.1 .52 0 timeout (verification) 900     6600 7300    0 timeout 910   14000 5100 0 error (5) .023 5.7 .14  0 error (5) .024 5.6 .11  0
eca-rers2012/Problem01_label45_true-unreach-call_false-termination.c false(termination) .78  88 8.6  1 timeout 900   8100 6900 0 error (42) 880     1300   8600    0 out of memory 390     15000   5600    0 false(termination) 31   920 250 1 unknown 3.9  150 54   0 unknown .058 4.5 .20  0 unknown .052 4.5 .15  0 timeout 900     2800 11000    0 false(termination) 23   670 190 1 out of memory 320    15000 4400   0 disqualified .047 9.2 .47 0 timeout (verification) 900     6500 6200    0 timeout 910   14000 4500 0 error (5) .027 5.6 .14  0 error (5) .024 5.6 .19  0
eca-rers2012/Problem01_label46_true-unreach-call_false-termination.c false(termination) .81  88 7.4  1 timeout 900   8100 7500 0 error (42) 880     1300   7900    0 out of memory 380     15000   5500    0 false(termination) 30   760 250 1 unknown 4.1  150 50   0 unknown .028 4.7 .31  0 unknown .035 4.6 .13  0 timeout 900     2700 9000    0 false(termination) 22   720 190 1 out of memory 320    15000 4100   0 disqualified .051 9.2 .39 0 timeout (verification) 900     6600 6200    0 timeout 910   14000 4300 0 error (5) .025 5.6 .12  0 error (5) .025 5.6 .19  0
eca-rers2012/Problem01_label47_false-unreach-call_false-termination.c false(termination) .81  88 7.7  1 timeout 900   8500 8300 0 error (42) 880     1300   7900    0 out of memory 380     15000   5200    0 false(termination) 30   770 260 1 unknown 12    110 160   0 unknown .033 4.6 .23  0 unknown .030 4.7 .23  0 timeout 900     2800 9900    0 false(termination) 23   710 200 1 out of memory 320    15000 4600   0 disqualified .049 9.2 .41 0 timeout (verification) 900     6600 6000    0 timeout 910   14000 4100 0 error (5) .041 5.5 .14  0 error (5) .024 5.6 .11  0
eca-rers2012/Problem01_label48_true-unreach-call_false-termination.c false(termination) .77  88 7.0  1 timeout 900   8100 7500 0 error (42) 880     1300   7000    0 out of memory 380     15000   5500    0 false(termination) 31   760 250 1 unknown 3.7  150 43   0 unknown .035 4.6 .16  0 unknown .029 4.7 .24  0 timeout 900     2700 10000    0 false(termination) 23   690 190 1 out of memory 320    15000 4100   0 disqualified .043 9.5 .42 0 timeout (verification) 900     6500 6200    0 timeout 910   13000 4500 0 error (5) .047 5.5 .17  0 error (5) .025 5.6 .17  0
eca-rers2012/Problem01_label49_true-unreach-call_false-termination.c false(termination) .81  88 7.6  1 timeout 900   8600 7100 0 error (42) 880     1300   8300    0 out of memory 380     15000   5000    0 false(termination) 30   770 250 1 unknown 3.7  150 47   0 unknown .028 4.6 .21  0 unknown .031 4.6 .16  0 timeout 900     2800 9100    0 false(termination) 22   700 190 1 out of memory 320    15000 3900   0 disqualified .047 8.8 .40 0 timeout (verification) 900     6500 5900    0 timeout 910   13000 4200 0 error (5) .026 5.6 .17  0 error (5) .022 5.5 .10  0
eca-rers2012/Problem01_label50_false-unreach-call_false-termination.c false(termination) .80  88 9.1  1 timeout 900   8200 7300 0 error (42) 880     1300   7600    0 out of memory 380     15000   5000    0 false(termination) 30   800 260 1 unknown 6.7  85 83   0 unknown .074 4.7 .16  0 unknown .031 4.6 .32  0 timeout 900     2800 11000    0 false(termination) 22   690 180 1 out of memory 320    15000 3700   0 disqualified .044 9.9 .51 0 timeout (verification) 900     6500 5900    0 timeout 910   14000 4200 0 error (5) .032 5.5 .20  0 error (5) .025 5.7 .11  0
eca-rers2012/Problem01_label51_true-unreach-call_false-termination.c false(termination) .82  88 7.4  1 timeout 900   8400 7700 0 error (42) 880     1300   7200    0 out of memory 380     15000   5100    0 false(termination) 31   900 280 1 unknown 3.9  150 47   0 unknown .028 4.7 .17  0 unknown .029 4.6 .16  0 timeout 900     2800 11000    0 false(termination) 23   710 180 1 out of memory 320    15000 4400   0 disqualified .052 9.3 .37 0 timeout (verification) 900     6500 5800    0 timeout 910   13000 4400 0 error (5) .026 5.6 .14  0 error (5) .035 5.7 .18  0
eca-rers2012/Problem01_label52_true-unreach-call_false-termination.c false(termination) .81  88 7.2  1 timeout 900   8100 8400 0 error (42) 880     1300   8000    0 out of memory 390     15000   4500    0 false(termination) 29   770 280 1 unknown 4.0  150 44   0 unknown .047 4.5 .15  0 unknown .030 4.6 .26  0 timeout 900     2800 11000    0 false(termination) 23   700 200 1 out of memory 320    15000 4300   0 disqualified .047 9.2 .38 0 timeout (verification) 900     6500 5500    0 timeout 910   13000 4700 0 error (5) .027 5.6 .11  0 error (5) .025 5.6 .14  0
eca-rers2012/Problem01_label53_true-unreach-call_false-termination.c false(termination) .83  87 7.4  1 timeout 900   8100 7400 0 error (42) 880     1300   7300    0 out of memory 380     15000   4700    0 false(termination) 30   760 250 1 unknown 3.9  140 51   0 unknown .035 4.7 .23  0 unknown .030 4.5 .28  0 timeout 900     2800 9700    0 false(termination) 23   700 180 1 out of memory 330    15000 4900   0 disqualified .041 8.9 .42 0 timeout (verification) 900     6600 8700    0 timeout 910   14000 4000 0 error (5) .024 5.6 .12  0 error (5) .023 5.6 .13  0
eca-rers2012/Problem01_label54_true-unreach-call_false-termination.c false(termination) .83  88 7.9  1 timeout 900   8400 6800 0 error (42) 880     1300   7900    0 out of memory 390     15000   5100    0 false(termination) 30   930 240 1 unknown 4.0  150 47   0 unknown .036 4.6 .17  0 unknown .031 4.5 .18  0 timeout 900     2900 9700    0 false(termination) 23   700 190 1 out of memory 320    15000 5100   0 disqualified .045 9.4 .42 0 timeout (verification) 900     6500 6600    0 timeout 910   14000 4400 0 error (5) .025 5.7 .16  0 error (5) .031 5.7 .10  0
eca-rers2012/Problem01_label55_true-unreach-call_false-termination.c false(termination) .80  88 8.2  1 timeout 900   8100 8400 0 error (42) 880     1300   6900    0 out of memory 380     15000   4800    0 false(termination) 29   760 240 1 unknown 3.8  150 44   0 unknown .027 4.5 .23  0 unknown .035 4.6 .25  0 timeout 900     2700 9000    0 false(termination) 22   670 190 1 out of memory 320    15000 4200   0 disqualified .048 9.1 .51 0 timeout (verification) 900     6500 6600    0 timeout 910   14000 4800 0 error (5) .029 5.6 .15  0 error (5) .027 5.6 .12  0
eca-rers2012/Problem01_label56_false-unreach-call_false-termination.c false(termination) .84  88 6.7  1 timeout 900   8100 7900 0 error (42) 880     1300   7300    0 out of memory 380     15000   4900    0 false(termination) 31   760 240 1 unknown 9.1  98 130   0 unknown .052 4.5 .15  0 unknown .025 4.6 .22  0 timeout 900     2700 9400    0 false(termination) 23   700 190 1 out of memory 320    15000 3900   0 disqualified .043 9.7 .43 0 timeout (verification) 900     6500 5800    0 timeout 910   14000 5000 0 error (5) .019 5.5 .11  0 error (5) .034 5.5 .060 0
eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c false(termination) .80  88 7.3  1 timeout 900   8100 8000 0 error (42) 880     1300   7600    0 out of memory 380     15000   5000    0 false(termination) 30   750 270 1 unknown 9.1  98 110   0 unknown .053 4.6 .13  0 unknown .027 4.6 .23  0 timeout 900     2800 11000    0 false(termination) 23   690 210 1 out of memory 320    15000 4000   0 disqualified .046 9.4 .50 0 timeout (verification) 900     6400 5800    0 timeout 910   14000 4900 0 error (5) .049 5.5 .10  0 error (5) .050 5.7 .11  0
eca-rers2012/Problem01_label58_true-unreach-call_false-termination.c false(termination) .80  88 7.0  1 timeout 900   8100 8600 0 error (42) 880     1300   8200    0 out of memory 380     15000   4700    0 false(termination) 30   880 250 1 unknown 3.9  150 48   0 unknown .032 4.7 .24  0 unknown .049 4.6 .16  0 timeout 900     2800 9200    0 false(termination) 22   700 190 1 out of memory 320    15000 4800   0 disqualified .039 8.8 .43 0 timeout (verification) 900     6500 5900    0 timeout 910   13000 4500 0 error (5) .025 5.7 .097 0 error (5) .024 5.6 .18  0
eca-rers2012/Problem01_label59_true-unreach-call_false-termination.c false(termination) .78  88 7.5  1 timeout 900   8000 7100 0 error (42) 880     1300   7300    0 out of memory 380     15000   4600    0 false(termination) 30   780 270 1 unknown 3.9  150 42   0 unknown .029 4.7 .19  0 unknown .023 4.6 .15  0 timeout 900     2800 9500    0 false(termination) 22   710 190 1 out of memory 320    15000 4300   0 disqualified .045 9.4 .41 0 timeout (verification) 900     6500 6400    0 timeout 910   14000 4200 0 error (5) .026 5.5 .21  0 error (5) .025 5.6 .082 0
eca-rers2012/Problem02_label00_true-unreach-call_false-termination.c false(termination) .83  88 7.8  0 false(termination) 170   6200 1500 0 error (42) 880     1400   7800    0 out of memory 380     15000   5700    0 false(termination) 24   670 210 1 unknown 4.6  150 57   0 unknown .036 4.5 .15  0 unknown .033 4.5 .31  0 timeout 900     2700 9700    0 false(termination) 24   710 200 1 out of memory 260    15000 3200   0 disqualified .062 9.2 .40 0 timeout (verification) 900     5300 7700    0 false(termination) 32   850 280 1 error (5) .025 5.6 .14  0 error (5) .027 5.7 .17  0
eca-rers2012/Problem02_label01_true-unreach-call_false-termination.c false(termination) .85  88 6.9  0 false(termination) 180   6200 1500 0 error (42) 880     1400   8300    0 out of memory 380     15000   4600    0 false(termination) 24   710 220 1 unknown 4.4  150 58   0 unknown .029 4.7 .22  0 unknown .059 4.6 .20  0 timeout 900     2700 9500    0 false(termination) 25   750 210 1 out of memory 260    15000 3100   0 disqualified .046 9.4 .45 0 timeout (verification) 900     5200 6300    0 false(termination) 33   850 270 1 error (5) .037 5.7 .15  0 error (5) .023 5.6 .11  0
eca-rers2012/Problem02_label02_true-unreach-call_false-termination.c false(termination) .81  88 8.1  0 false(termination) 180   6100 1500 0 error (42) 880     1400   7400    0 out of memory 380     15000   4800    0 false(termination) 25   700 220 1 unknown 5.5  150 75   0 unknown .030 4.6 .13  0 unknown .043 4.6 .15  0 timeout 900     2700 11000    0 false(termination) 25   710 210 1 out of memory 260    15000 3600   0 disqualified .046 9.3 .49 0 timeout (verification) 900     5300 8000    0 false(termination) 32   770 290 1 error (5) .027 5.5 .23  0 error (5) .025 5.6 .13  0
eca-rers2012/Problem02_label03_true-unreach-call_false-termination.c false(termination) .83  88 6.9  0 false(termination) 180   6200 1800 0 error (42) 880     1400   7700    0 out of memory 380     15000   4800    0 false(termination) 25   740 190 1 unknown 4.0  150 49   0 unknown .026 4.6 .17  0 unknown .033 4.5 .30  0 timeout 900     2700 9500    0 false(termination) 24   710 200 1 out of memory 260    15000 3600   0 disqualified .046 9.3 .38 0 timeout (verification) 900     5200 6400    0 false(termination) 32   840 260 1 error (5) .023 5.7 .16  0 error (5) .037 5.6 .13  0
eca-rers2012/Problem02_label04_true-unreach-call_false-termination.c false(termination) .85  87 6.8  0 false(termination) 180   6200 1700 0 error (42) 880     1400   7800    0 out of memory 380     15000   5300    0 false(termination) 26   710 240 1 unknown 4.1  150 44   0 unknown .029 4.6 .15  0 unknown .049 4.7 .15  0 timeout 900     2700 11000    0 false(termination) 25   720 230 1 out of memory 260    15000 3500   0 disqualified .045 9.3 .41 0 timeout (verification) 900     5300 7700    0 false(termination) 33   850 250 1 error (5) .036 5.6 .11  0 error (5) .032 5.6 .12  0
eca-rers2012/Problem02_label05_true-unreach-call_false-termination.c false(termination) .83  87 7.4  0 false(termination) 180   6300 1800 0 error (42) 880     1400   8300    0 out of memory 380     15000   4400    0 false(termination) 25   730 200 1 unknown 4.4  150 51   0 unknown .035 4.5 .26  0 unknown .032 4.7 .31  0 timeout 900     2700 8900    0 false(termination) 25   740 210 1 out of memory 260    15000 3400   0 disqualified .044 9.5 .48 0 timeout (verification) 900     5300 7200    0 false(termination) 32   760 270 1 error (5) .021 5.5 .15  0 error (5) .027 5.6 .25  0
eca-rers2012/Problem02_label06_true-unreach-call_false-termination.c false(termination) .89  88 7.3  0 false(termination) 190   6200 1600 0 error (42) 880     1400   7200    0 out of memory 380     15000   4300    0 false(termination) 26   730 240 1 unknown 10    150 130   0 unknown .029 4.6 .18  0 unknown .028 4.5 .22  0 timeout 900     2700 9800    0 false(termination) 26   740 220 1 out of memory 260    15000 4200   0 disqualified .045 9.1 .59 0 timeout (verification) 900     5300 7600    0 false(termination) 33   830 260 1 error (5) .024 5.7 .11  0 error (5) .043 5.5 .12  0
eca-rers2012/Problem02_label07_true-unreach-call_false-termination.c false(termination) .85  87 8.5  0 false(termination) 190   6200 1500 0 error (42) 880     1400   7900    0 out of memory 380     15000   4400    0 false(termination) 24   720 200 1 unknown 4.1  150 48   0 unknown .027 4.7 .19  0 unknown .056 4.7 .17  0 timeout 900     2700 8800    0 false(termination) 26   750 220 1 out of memory 260    15000 3400   0 disqualified .043 9.1 .56 0 timeout (verification) 900     5300 7100    0 false(termination) 32   850 230 1 error (5) .024 5.6 .13  0 error (5) .024 5.7 .095 0
eca-rers2012/Problem02_label08_true-unreach-call_false-termination.c false(termination) .85  88 7.3  0 false(termination) 180   6200 1600 0 error (42) 880     1400   7700    0 out of memory 380     15000   4800    0 false(termination) 26   700 200 1 unknown 5.5  150 73   0 unknown .053 4.6 .17  0 unknown .030 4.6 .20  0 timeout 900     2900 9400    0 false(termination) 25   740 230 1 out of memory 260    15000 3000   0 disqualified .065 9.2 .34 0 timeout (verification) 900     5500 11000    0 false(termination) 32   790 270 1 error (5) .025 5.6 .15  0 error (5) .024 5.6 .14  0
eca-rers2012/Problem02_label09_true-unreach-call_false-termination.c false(termination) .83  88 7.2  0 false(termination) 170   6200 1600 0 error (42) 880     1400   7000    0 out of memory 380     15000   4600    0 false(termination) 25   710 210 1