Tool 2LS 0.3.4 BLAST 2.7.3 CBMC CPAchecker 1.4-svcomp16c CPAchecker 1.4-svn 18373 CPAchecker 1.4-svcomp16c ESBMC ESBMC version 2.0.0 64-bit x86_64 linux DepthK ESBMC+DepthK version 2.1 impara 0.45 CPAchecker 1.4-svn 18356M SeaHorn-F16 0.1.0 skink SMACK+Corral 1.5.2 symbiotic 3.0.1 ULTIMATE Automizer cfb9fd9e ULTIMATE Kojak fd30d3d8 VVT prerelease
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic Linux 4.2.0-23-generic Linux 4.2.0-22-generic Linux 4.2.0-23-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]] 2016-01-03 17:36:26 CET [[ 2016-01-15 08:15:11 CET ]] [[ 2016-01-15 21:49:51 CET ]] 2016-01-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]] 2016-01-04 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]] 2016-01-04 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]] 2016-01-04 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]] 2016-01-04 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]] 2016-01-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]] 2016-01-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 CET ]] 2016-01-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]] 2016-01-10 22:01:17 CET [[ 2016-01-15 09:16:15 CET ]] [[ 2016-01-15 22:26:01 CET ]] 2016-01-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]] 2016-01-15 22:52:00 CET [[ 2016-01-16 00:34:30 CET ]] [[ 2016-01-16 00:56:26 CET ]] 2016-01-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]] 2016-01-07 09:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 CET ]] 2016-01-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 CET ]] 2016-01-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 CET ]] 2016-01-17 23:14:00 CET [[ 2016-01-18 06:54:01 CET ]] [[ 2016-01-18 07:05:55 CET ]]
Run set 2ls.sv-comp16.ProductLines blast.sv-comp16.ProductLines cbmc.sv-comp16.ProductLines cpa-bam.sv-comp16.ProductLines cpa-kind.sv-comp16.ProductLines cpa-refsel.sv-comp16.ProductLines cpa-seq.sv-comp16.ProductLines esbmc.sv-comp16.ProductLines esbmcdepthk.sv-comp16.ProductLines impara.sv-comp16.ProductLines lpi.sv-comp16.ProductLines seahorn.sv-comp16.ProductLines skink.sv-comp16.ProductLines smack.sv-comp16.ProductLines symbiotic3.sv-comp16.ProductLines uautomizer.sv-comp16.ProductLines ukojak.sv-comp16.ProductLines vvt.sv-comp16.ProductLines
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--k-induction -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -lpi-svcomp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/skink.2016-01-15_2252.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/skink.2016-01-15_2252.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/vvt.2016-01-17_2314.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/vvt.2016-01-17_2314.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/product-lines/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
elevator_spec14_product20_false-unreach-call.cil.c 9.6  1500 450     330 .27 37 910   11000 24   820 12   540 11   390 .27 45 12    210 .81 37 18   580 1.5  68 23   1400 9.2 190 19    21   900 9200 40   670 .66  22  
elevator_spec14_product24_false-unreach-call.cil.c 15    2300 1.9   53 .28 38 910   11000 25   860 13   570 11   390 .21 41 13    210 1.3  37 20   590 2.1  100 23   1500 11   220 18    22   900 10000 38   660 .80  37  
elevator_spec14_product28_false-unreach-call.cil.c 10    1600 480     330 .26 38 910   10000 21   830 11   550 11   380 .20 40 13    210 .99 36 19   580 1.6  68 23   1400 9.8 210 19    22   910 9200 40   640 .78  24  
elevator_spec14_product32_false-unreach-call.cil.c 16    2400 1.9   53 .33 38 910   11000 26   870 12   570 9.3 390 .28 46 13    210 1.2  38 21   650 2.3  100 21   1500 11   230 18    22   900 9700 46   720 .91  38  
elevator_spec14_productSimulator_false-unreach-call.cil.c 54    7900 140     330 15    420 34   900 150   3000 12   610 9.9 430 .33 47 65    350 1.7  39 130   1700 8.2  230 25   1400 23   310 18    24   900 8500 49   790 1.9   58  
elevator_spec1_product18_false-unreach-call.cil.c 770    1800 670     450 .55 38 910   11000 120   4100 13   570 11   390 .21 45 15    200 1.1  37 71   1600 7.6  310 21   1400 8.6 180 18    21   910 7400 38   760 .45  18  
elevator_spec1_product20_false-unreach-call.cil.c 900    1900 680     310 .54 38 910   8500 120   4000 14   580 11   420 .18 41 15    210 1.4  38 74   1700 6.7  330 22   1400 9.1 200 19    21   900 8300 38   710 .50  19  
elevator_spec1_product22_false-unreach-call.cil.c 900    2200 4.2   71 .59 38 910   11000 140   4400 12   600 9.4 410 820    7900 14    210 1.4  37 900   7500 12    530 22   1400 10   200 18    22   910 9000 40   630 .54  25  
elevator_spec1_product24_false-unreach-call.cil.c 900    2200 4.0   67 .58 39 910   11000 140   4400 14   620 9.5 430 820    8700 15    210 1.6  38 900   7600 12    540 21   1400 10   220 18    22   900 8100 37   670 .53  28  
elevator_spec1_product26_false-unreach-call.cil.c 780    1900 660     310 .52 38 910   11000 120   3700 13   560 9.5 400 .20 40 14    210 1.2  37 900   6400 7.5  330 24   1400 11   220 19    21   910 9200 39   650 .41  16  
elevator_spec1_product28_false-unreach-call.cil.c 900    2000 680     400 .55 38 910   11000 130   4200 14   590 11   430 820    7600 15    210 1.1  38 900   6500 7.6  340 22   1400 9.7 220 18    22   910 9100 39   760 .57  17  
elevator_spec1_product30_false-unreach-call.cil.c 900    2200 4.8   83 .53 38 910   11000 150   4400 14   590 11   420 .29 49 14    210 1.3  40 900   7400 11    520 20   1400 10   220 18    22   910 8800 41   800 .64  24  
elevator_spec1_product32_false-unreach-call.cil.c 900    2300 5.0   73 .44 39 910   11000 150   4500 13   610 12   420 820    8000 15    210 1.6  38 900   7700 12    550 22   1400 12   210 18    23   910 9400 37   740 .71  27  
elevator_spec1_productSimulator_false-unreach-call.cil.c 900    4200 690     990 96    1100 34   840 350   5800 15   640 11   470 800    5700 590    430 41    58 900   9500 35    310 23   1500 13   230 18    25   900 11000 43   650 1.4   43  
elevator_spec2_product18_false-unreach-call.cil.c 650    1800 680     320 .54 38 900   11000 120   4200 13   540 11   400 .22 44 13    210 1.1  37 900   6400 3.6  170 22   1400 9.5 210 18    21   910 8500 69   1100 .53  21  
elevator_spec2_product20_false-unreach-call.cil.c 900    2000 680     380 .53 38 910   11000 120   4200 14   580 9.3 420 910    9300 13    210 1.3  37 900   6500 3.9  160 22   1400 10   210 18    21   910 9400 62   1000 .49  21  
elevator_spec2_product22_false-unreach-call.cil.c 900    2200 3.1   67 .53 38 900   11000 140   4300 13   580 11   400 .18 45 15    210 1.3  38 900   7400 6.4  310 22   1400 9.7 200 18    22   910 10000 60   1400 .59  25  
elevator_spec2_product24_false-unreach-call.cil.c 900    2200 3.9   64 .58 39 910   11000 140   4500 12   590 11   410 .19 43 14    210 1.3  38 80   1800 6.5  320 24   1500 9.4 210 18    22   910 10000 68   1200 .48  22  
elevator_spec2_product26_false-unreach-call.cil.c 750    1900 700     630 .58 38 910   11000 120   4100 12   560 11   380 .23 41 15    210 1.1  37 900   6400 3.7  160 23   1400 10   200 19    21   910 9700 76   1500 .53  21  
elevator_spec2_product28_false-unreach-call.cil.c 900    2000 680     450 .58 38 910   11000 130   4200 14   570 11   400 .22 41 15    210 1.3  37 900   6500 4.3  160 23   1500 9.0 230 19    22   910 10000 65   1200 .55  19  
elevator_spec2_product30_false-unreach-call.cil.c 900    2300 4.1   76 .43 38 910   11000 150   4400 14   580 9.3 410 .24 45 15    210 1.3  38 900   7400 6.5  310 22   1400 10   220 19    22   910 9700 54   1100 .68  24  
elevator_spec2_product32_false-unreach-call.cil.c 900    2300 5.1   69 .59 39 910   11000 150   4400 14   580 11   420 .29 47 15    210 1.7  38 900   7700 6.5  320 22   1400 10   230 18    23   910 11000 72   1400 .70  27  
elevator_spec2_productSimulator_false-unreach-call.cil.c 900    4200 710     740 60    920 910   11000 350   6000 16   640 13   530 800    6300 590    430 45    69 900   9500 28    260 25   1400 14   270 18    24   910 9100 48   810 1.4   43  
elevator_spec3_product03_false-unreach-call.cil.c 5.0  760 .65  58 .37 39 910   11000 26   760 16   610 10   460 .21 47 13    210 2.1  38 18   570 .87 49 20   1200 14   250 18    22   910 10000 39   720 .44  17  
elevator_spec3_product11_false-unreach-call.cil.c 5.3  800 .73  62 .38 39 910   11000 25   760 15   620 12   460 .22 48 13    210 2.1  38 19   600 1.0  48 21   1100 17   300 19    22   900 9900 39   690 .54  19  
elevator_spec3_product19_false-unreach-call.cil.c 5.5  840 .81  64 .40 39 910   11000 25   770 15   630 11   460 .24 47 13    210 2.1  38 19   580 .95 47 21   1400 13   240 19    22   900 10000 64   960 .51  17  
elevator_spec3_product20_false-unreach-call.cil.c 10    1600 .64  64 .40 39 900   6500 29   890 15   650 11   480 .25 41 14    210 2.4  38 22   650 1.2  75 21   1400 12   240 18    22   900 9200 40   780 .70  28  
elevator_spec3_product23_false-unreach-call.cil.c 8.4  1300 1.8   50 .38 40 910   11000 27   810 16   660 11   470 .24 44 13    210 2.5  39 22   630 1.1  66 21   1200 15   250 18    23   910 9300 39   760 .59  26  
elevator_spec3_product24_false-unreach-call.cil.c 16    2400 1.7   52 .41 40 900   9600 32   970 15   670 13   500 .24 46 14    210 2.7  39 24   810 1.6  89 22   1400 15   260 18    23   910 10000 41   810 .82  36  
elevator_spec3_product27_false-unreach-call.cil.c 5.7  890 .63  62 .28 39 910   11000 27   750 14   630 11   460 820    8800 13    210 1.9  38 21   590 .96 48 23   1500 13   240 19    23   900 11000 38   730 .53  22  
elevator_spec3_product28_false-unreach-call.cil.c 11    1700 .83  64 .38 39 900   8200 27   890 15   640 13   470 .21 41 13    210 2.4  38 20   630 1.5  78 23   1400 14   260 18    23   900 10000 40   740 .80  28  
elevator_spec3_product31_false-unreach-call.cil.c 8.6  1300 1.8   50 .30 40 910   11000 27   810 16   650 13   470 .24 48 12    220 2.4  39 20   620 1.2  59 20   1100 15   260 19    23   910 10000 39   710 .61  22  
elevator_spec3_product32_false-unreach-call.cil.c 16    2600 1.7   50 .39 40 910   11000 29   900 16   640 13   500 .25 47 13    210 2.7  39 22   710 2.0  91 20   1400 17   250 18    24   900 11000 39   820 .93  38  
elevator_spec3_productSimulator_false-unreach-call.cil.c 60    8500 430     300 56    880 910   11000 900   5400 25   930 19   710 .27 49 140    570 8.8  43 900   2600 9.4  230 24   1400 32   320 18    26   910 9500 42   750 1.9   54  
elevator_spec9_product26_false-unreach-call.cil.c 700    1900 670     580 .58 38 910   11000 120   4200 11   560 9.2 400 .25 43 14    210 1.3  37 900   6400 3.9  160 19   1400 9.4 200 18    21   910 10000 72   1100 .50  21  
elevator_spec9_product28_false-unreach-call.cil.c 900    2000 680     450 .60 38 900   8900 130   4300 14   590 11   420 .21 41 15    210 1.5  38 900   6500 4.0  160 24   1500 11   220 18    22   900 11000 74   1400 .56  17  
elevator_spec9_product30_false-unreach-call.cil.c 900    2200 75     170 .59 38 910   11000 140   4300 14   580 11   420 .24 45 15    210 1.5  38 900   7500 6.9  310 20   1400 10   210 19    22   900 10000 66   1300 .58  22  
elevator_spec9_product32_false-unreach-call.cil.c 900    2300 100     190 .59 39 910   11000 160   4500 13   600 9.5 430 .19 44 13    210 1.8  38 900   8100 6.3  310 21   1400 12   240 19    22   900 10000 62   1500 .62  23  
elevator_spec9_productSimulator_false-unreach-call.cil.c 900    4200 700     960 60    920 910   11000 310   5600 15   640 11   470 .34 49 570    410 47    67 900   9600 21    240 24   1500 14   250 19    25   900 10000 61   1000 1.3   45  
elevator_spec13_product21_true-unreach-call.cil.c 7.0  1200 2.2   53 6.2  71 910   10000 900   7500 7.2 280 5.3 240 .20 43 1.7  55 3.8  36 910   12000 54    840 22   1200 72   370 850    15000   900 9200 59   1000 .54  23  
elevator_spec13_product22_true-unreach-call.cil.c 13    2300 2.5   55 6.4  72 900   7800 900   8000 6.3 270 5.5 240 .23 43 1.7  55 4.2  36 900   11000 130    1100 21   1400 100   380 870    15000   900 10000 58   1000 .82  35  
elevator_spec13_product23_true-unreach-call.cil.c 7.5  1300 2.6   53 5.0  50 910   11000 910   8300 7.4 280 6.3 240 .22 41 1.3  56 5.4  37 97   2600 160    930 22   1300 150   460 860    15000   900 9400 47   840 .66  23  
elevator_spec13_product24_true-unreach-call.cil.c 15    2500 3.1   55 5.2  51 900   7100 900   7900 6.5 290 6.6 250 .21 46 1.7  58 5.8  37 110   3200 88    980 22   1400 140   410 880    15000   910 8300 40   840 .85  33  
elevator_spec13_product29_true-unreach-call.cil.c 7.2  1300 2.9   58 6.2  72 900   11000 900   8200 7.1 280 5.3 240 .89 53 1.7  55 3.8  36 910   12000 78    920 21   1200 66   370 860    15000   910 9500 43   780 .59  25  
elevator_spec13_product30_true-unreach-call.cil.c 14    2400 3.3   60 6.4  72 910   8200 910   7800 6.2 280 5.4 240 .18 42 1.7  55 4.3  36 910   11000 130    1100 22   1400 67   370 860    15000   910 8200 49   870 .90  34  
elevator_spec13_product31_true-unreach-call.cil.c 7.7  1400 3.1   60 5.0  53 900   11000 910   8200 7.4 280 6.7 240 .20 43 1.8  56 5.3  38 99   2500 120    820 20   1300 140   450 860    15000   900 8600 43   780 .58  28  
elevator_spec13_product32_true-unreach-call.cil.c 15    2600 2.5   58 5.0  51 910   8300 910   8000 6.4 290 6.8 250 .24 41 1.3  56 6.0  37 110   2700 160    810 23   1500 160   440 860    15000   910 7900 47   840 .73  38  
elevator_spec13_productSimulator_true-unreach-call.cil.c 56    8500 3.5   85 850    420 610   6700 900   8700 9.8 430 9.3 320 .32 49 900    7000 32    50 910   11000 620    1300 23   1400 630   580 860    15000   900 8100 48   810 1.9   56  
elevator_spec14_product03_true-unreach-call.cil.c 750    1800 680     420 2.9  36 910   9900 250   5200 8.8 300 7.9 270 .22 47 1.7  54 22    38 900   7000 2.0  140 21   1200 130   510 18    21   900 8500 42   650 .42  20  
elevator_spec14_product11_true-unreach-call.cil.c 820    1800 680     420 2.9  37 910   10000 200   5100 8.7 310 8.0 280 .40 51 1.8  55 22    39 900   7200 2.2  150 21   1100 140   530 18    21   900 9000 42   770 .36  18  
elevator_spec14_product19_true-unreach-call.cil.c 900    1900 680     470 3.0  37 910   11000 470   6300 8.7 310 6.8 270 .22 40 1.7  54 23    39 900   7200 2.1  150 20   1100 76   460 18    21   910 8600 44   760 .48  20  
elevator_spec14_product23_true-unreach-call.cil.c 350    1700 1.9   53 3.3  37 910   10000 900   7200 9.1 330 8.3 290 .18 47 1.7  55 37    39 900   8200 1.3  52 67   1300 95   470 18    22   900 8600 72   1200 .53  21  
elevator_spec14_product27_true-unreach-call.cil.c 900    1900 690     430 3.0  37 900   10000 490   6500 7.5 310 6.5 280 .22 41 1.7  54 23    40 900   7200 2.3  150 20   1100 94   500 19    21   900 8400 42   700 .48  19  
elevator_spec14_product31_true-unreach-call.cil.c 450    1800 1.9   53 3.3  37 910   11000 900   7400 9.2 330 8.2 290 .24 46 1.7  55 36    39 900   8300 1.3  53 22   1400 110   510 18    22   900 8900 43   820 .63  24  
elevator_spec1_product01_true-unreach-call.cil.c 900    1800 660     300 2.6  37 910   11000 600   6800 8.3 300 7.0 260 .21 40 2.4  55 14    37 900   8900 15    190 23   1500 42   380 18    20   910 8600 35   620 .41  17  
elevator_spec1_product03_true-unreach-call.cil.c 900    1700 660     480 2.8  38 910   11000 660   7000 8.5 310 7.5 270 .34 51 2.5  56 21    40 900   9200 12    190 65   1300 54   470 18    21   900 9100 37   640 .26  15  
elevator_spec1_product09_true-unreach-call.cil.c 900    1800 650     430 2.7  38 910   11000 610   7000 7.9 300 7.1 260 .27 47 2.4  55 14    37 900   9000 14    190 20   1100 49   440 18    20   900 10000 38   790 .34  17  
elevator_spec1_product11_true-unreach-call.cil.c 900    1700 660     440 2.8  38 910   11000 790   7400 7.0 310 7.5 270 .23 41 2.6  56 22    40 900   9200 18    210 21   1200 70   520 18    21   900 10000 39   730 .35  17  
elevator_spec1_product17_true-unreach-call.cil.c 900    1700 670     450 2.6  37 910   11000 670   7000 6.9 310 6.1 270 .25 45 2.5  55 15    37 900   8700 15    190 19   1100 32   350 18    20   910 9100 37   830 .30  14  
elevator_spec1_product19_true-unreach-call.cil.c 900    1700 670     420 2.8  38 910   11000 830   7500 7.0 310 7.7 280 .23 44 2.3  56 22    41 900   8900 16    190 20   1100 73   460 18    21   900 8500 36   610 .44  13  
elevator_spec1_product21_true-unreach-call.cil.c 900    1800 5.3   96 2.9  38 900   11000 900   7100 7.0 310 6.3 270 .15 42 5.4  57 19    39 900   8700 78    310 23   1400 96   490 18    21   900 9400 41   780 .43  17  
elevator_spec1_product23_true-unreach-call.cil.c 900    1700 39     190 3.0  38 910   11000 900   7200 8.6 310 6.9 280 .24 49 5.2  58 28    46 900   9000 67    320 19   1100 110   520 18    22   910 9600 38   630 .46  15  
elevator_spec1_product25_true-unreach-call.cil.c 900    1800 670     430 2.3  38 910   11000 830   7800 6.9 290 5.9 260 .23 47 2.5  55 15    37 900   8900 14    200 20   1100 40   390 18    21   900 9900 35   620 .40  13  
elevator_spec1_product27_true-unreach-call.cil.c 900    1700 670     420 2.9  38 910   11000 730   7400 8.5 310 6.4 270 .22 46 2.6  56 22    41 900   9100 12    200 20   1300 61   460 19    21   910 8700 38   800 .39  19  
elevator_spec1_product29_true-unreach-call.cil.c 900    1700 5.3   100 3.2  38 910   11000 900   7000 8.5 300 7.4 270 .40 52 5.2  57 19    38 900   8600 86    320 62   1100 70   470 18    22   910 9700 37   790 .46  19  
elevator_spec1_product31_true-unreach-call.cil.c 900    1700 39     190 3.1  39 910   11000 900   7400 8.6 320 6.7 280 .20 46 5.1  59 27    45 900   9300 120    370 21   1300 110   510 18    22   900 8900 37   730 .54  21  
elevator_spec2_product01_true-unreach-call.cil.c 900    1800 650     440 2.3  37 910   9000 150   4500 7.5 280 5.3 240 .24 46 3.2  55 4.1  36 900   5700 3.6  110 21   1100 30   360 18    20   910 9100 54   1100 .30  16  
elevator_spec2_product03_true-unreach-call.cil.c 900    1700 670     560 2.3  38 900   11000 170   4600 7.5 280 6.6 240 .25 44 2.7  56 5.6  36 900   6000 3.5  110 22   1400 29   330 18    21   900 8800 49   1000 .34  12  
elevator_spec2_product09_true-unreach-call.cil.c 900    1700 650     440 2.1  38 910   11000 160   4500 7.4 280 5.5 240 .24 43 3.1  55 4.3  36 900   5800 3.6  110 21   1100 32   360 18    20   900 8500 55   920 .28  14  
elevator_spec2_product11_true-unreach-call.cil.c 900    1700 670     660 2.0  38 910   11000 170   4600 7.7 280 6.4 250 .16 44 3.4  56 5.9  36 900   6000 3.2  110 19   1100 37   350 19    21   900 8800 53   1100 .48  13  
elevator_spec2_product17_true-unreach-call.cil.c 900    1700 670     420 2.2  38 910   11000 140   4500 7.0 280 6.4 240 .22 42 3.3  55 4.3  36 900   5700 3.0  110 21   1100 28   340 18    20   910 9200 59   1100 .34  12  
elevator_spec2_product19_true-unreach-call.cil.c 900    1800 670     450 2.5  38 910   11000 160   4700 7.6 290 5.6 250 .19 41 3.4  56 6.2  36 900   6000 3.2  100 22   1100 36   370 18    21   900 8600 52   1000 .39  17  
elevator_spec2_product21_true-unreach-call.cil.c 900    1800 5.6   89 2.3  38 910   11000 210   4700 7.4 280 6.5 240 .22 46 3.4  56 4.9  38 900   7900 7.6  180 19   1200 25   320 18    21   900 9500 66   1400 .42  19  
elevator_spec2_product23_true-unreach-call.cil.c 900    1800 51     290 2.4  38 910   11000 260   5100 6.5 290 6.6 240 .24 49 3.6  57 7.0  37 900   7900 8.2  180 21   1200 36   380 18    22   910 10000 49   830 .42  20  
elevator_spec2_product25_true-unreach-call.cil.c 900    1700 670     450 2.2  38 910   11000 150   4700 7.3 290 6.3 240 .35 51 2.5  55 4.4  36 900   5800 3.5  110 20   1100 26   320 18    21   900 8900 57   900 .36  15  
elevator_spec2_product27_true-unreach-call.cil.c 900    1800 680     450 2.3  38 900   11000 190   4900 7.7 290 5.6 250 .35 51 3.4  56 6.0  37 900   5900 3.6  100 18   1100 30   350 18    21   900 8400 52   1000 .36  15  
elevator_spec2_product29_true-unreach-call.cil.c 900    1700 5.1   90 2.2  38 910   11000 240   4900 7.6 280 6.5 240 .37 51 3.3  56 5.0  37 900   7700 6.5  180 21   1200 33   350 18    21   910 10000 64   1400 .47  20  
elevator_spec2_product31_true-unreach-call.cil.c 900    1800 50     290 2.7  39 910   11000 280   5100 7.7 290 6.6 250 .24 46 3.4  58 7.2  37 900   8100 7.7  180 22   1300 28   330 19    22   900 9300 50   800 .54  18  
elevator_spec3_product01_true-unreach-call.cil.c 4.6  680 700     420 3.3  37 910   10000 110   3800 9.0 320 7.0 290 .41 51 1.7  55 29    48 900   5400 1.7  120 21   1100 23   330 18    21   900 8100 64   1100 .40  17  
elevator_spec3_product09_true-unreach-call.cil.c 5.0  730 690     420 3.3  37 910   11000 100   3600 7.8 320 7.9 290 .20 43 1.6  55 26    46 900   5000 1.8  120 21   1400 20   310 19    21   910 8200 43   690 .48  19  
elevator_spec3_product17_true-unreach-call.cil.c 5.1  770 700     420 3.4  37 900   11000 100   3600 8.9 320 8.3 280 .20 44 1.7  55 27    48 900   5000 1.7  130 19   1100 20   300 19    22   910 9500 41   770 .33  15  
elevator_spec3_product18_true-unreach-call.cil.c 9.7  1400 680     290 3.4  37 900   11000 140   4600 8.9 320 6.7 280 .21 44 1.7  55 33    51 900   7100 3.0  180 21   1400 22   330 18    22   910 8300 43   820 .69  27  
elevator_spec3_product21_true-unreach-call.cil.c 7.7  1200 5.2   59 3.6  37 910   11000 120   4600 9.4 330 8.4 290 .22 45 1.8  56 39    62 900   7500 2.3  160 22   1400 24   310 19    22   900 8900 41   810 .58  26  
elevator_spec3_product22_true-unreach-call.cil.c 15    2200 4.8   61 3.8  37 900   10000 180   4800 7.9 340 8.3 290 .24 46 1.8  56 45    65 900   7700 4.6  290 21   1400 25   280 18    23   900 8400 39   760 .84  35  
elevator_spec3_product25_true-unreach-call.cil.c 5.2  810 700     420 3.2  37 910   11000 100   3700 7.5 320 8.2 280 .25 45 1.3  55 27    46 900   5100 1.8  130 22   1400 24   330 19    22   910 8000 42   790 .52  17  
elevator_spec3_product26_true-unreach-call.cil.c 10    1500 680     290 3.4  37 910   11000 120   4500 7.8 320 6.9 290 .30 52 1.4  55 30    49 900   6700 3.2  180 23   1400 19   290 18    22   900 8600 37   780 .77  25  
elevator_spec3_product29_true-unreach-call.cil.c 8.0  1200 5.3   56 3.7  37 910   11000 130   4600 9.7 330 7.2 300 .40 52 1.8  56 37    57 900   7400 2.4  170 20   1200 21   300 19    23   900 9500 42   770 .59  26  
elevator_spec3_product30_true-unreach-call.cil.c 16    2300 5.4   59 3.8  37 900   11000 170   4900 9.5 330 8.4 300 .43 53 1.8  56 38    62 900   8800 4.8  310 21   1400 27   310 18    23   910 9500 39   660 .96  37  
elevator_spec9_product09_true-unreach-call.cil.c 900    1800 650     430 2.1  38 900   11000 170   4500 7.5 280 5.2 240 .19 41 3.1  55 4.3  36 900   5900 3.2  110 20   1100 32   370 18    20   910 8700 57   1000 .28  17  
elevator_spec9_product11_true-unreach-call.cil.c 900    1800 660     550 2.4  38 910   11000 160   4700 7.5 280 6.6 250 .35 51 3.2  56 6.3  36 900   6100 3.5  99 19   1200 31   360 19    21   900 9100 60   1100 .39  17  
elevator_spec9_product25_true-unreach-call.cil.c 900    1700 670     460 2.3  38 910   11000 150   4500 6.4 280 5.6 240 .22 47 2.9  55 4.8  36 900   5900 3.8  100 20   1100 34   360 18    21   910 11000 59   1300 .39  17  
elevator_spec9_product27_true-unreach-call.cil.c 900    1800 660     310 2.3  38 910   11000 180   4800 7.5 280 6.6 240 .22 46 3.4  56 6.4  37 900   6100 3.4  110 20   1100 44   400 18    21   910 11000 64   1300 .39  17  
elevator_spec9_product29_true-unreach-call.cil.c 900    1700 22     130 2.4  38 910   11000 250   4700 6.5 290 6.6 250 .27 46 2.6  56 5.3  36 900   7800 7.1  170 21   1100 31   360 18    22   900 9800 60   980 .44  16  
elevator_spec9_product31_true-unreach-call.cil.c 900    1800 43     300 2.7  39 910   11000 250   4800 7.5 280 6.7 250 .20 45 3.7  58 7.3  37 900   8300 8.5  190 19   1200 37   370 18    22   910 9900 36   750 .57  17  
email_spec0_product16_false-unreach-call.cil.c 180    610 400     280 1.6  48 140   4000 900   6000 43   1300 53   1600 230    5000 16    200 74    130 900   4800 19    200 18   940 23   180 71    18   900 8800 43   710 .19  17  
email_spec0_product21_false-unreach-call.cil.c 350    1000 670     300 2.6  56 430   4900 900   6500 50   1800 58   1600 230    5100 19    210 240    240 900   5000 31    360 20   950 21   220 71    21   910 8800 42   870 .21  13  
email_spec0_product22_false-unreach-call.cil.c 210    670 650     300 1.7  49 180   4200 900   5700 49   1800 54   1600 220    5000 15    210 120    170 900   4800 27    320 20   950 13   170 36    19   910 8800 47   760 .21  13  
email_spec0_product26_false-unreach-call.cil.c 420    1100 660     420 2.8  58 810   7300 900   7300 54   1800 50   1400 230    5100 18    210 250    270 900   5100 43    1200 18   960 25   230 36    22   910 8600 46   920 .17  13  
email_spec0_product31_false-unreach-call.cil.c 170    640 660     380 2.1  52 680   5600 900   6100 50   1800 58   1600 220    5000 18    210 120    220 900   4900 31    390 19   990 20   200 53    20   910 8600 47   810 .17  11  
email_spec0_product33_false-unreach-call.cil.c 190    690 670     430 2.0  51 900   6800 900   6400 61   1400 50   1600 240    5300 14    210 140    180 900   4900 24    520 20   1000 19   200 53    23   900 9000 40   780 .20  11  
email_spec0_product34_false-unreach-call.cil.c 370    1100 660     440 3.6  69 900   7300 900   7000 58   1800 69   1700 230    5300 22    210 290    320 900   5200 43    620 19   1000 29   260 54    23   900 9200 49   830 .27  12  
email_spec0_product35_false-unreach-call.cil.c 400    1200 670     430 3.9  71 910   7300 900   7800 60   2000 82   1800 220    5200 23    210 370    460 900   5400 41    160 20   1000 34   270 54    24   900 9000 53   830 .23  16  
email_spec0_productSimulator_false-unreach-call.cil.c 700    15000 790     5000 480    1500 7.9 390 900   8100 140   3800 110   3300 340    5000 360    770 900    400 900   7100 140    730 22   1400 170   330 900    90   910 9700 45   690 1.4   60  
email_spec11_product15_false-unreach-call.cil.c 160    600 650     290 1.5  48 81   3900 900   5400 56   1300 46   1600 220    5000 14    200 68    130 900   4800 20    230 19   970 12   160 18    17   900 8500 41   880 .18  13  
email_spec11_product20_false-unreach-call.cil.c 330    950 670     290 2.2  53 310   4500 900   6100 44   1800 58   1600 220    5100 16    210 270    280 900   5200 27    430 20   960 22   210 18    20   900 8900 46   790 .21  15  
email_spec11_product22_false-unreach-call.cil.c 220    660 650     420 1.7  49 150   4100 900   5600 51   1800 52   1600 220    5200 15    210 160    180 900   4800 27    280 20   970 21   190 18    19   900 8800 45   800 .20  15  
email_spec11_product26_false-unreach-call.cil.c 400    1100 660     430 2.8  59 780   5800 900   7000 75   1800 64   1700 220    5000 22    210 240    270 900   5000 37    1100 20   960 24   230 19    21   900 8600 55   900 .23  15  
email_spec11_product30_false-unreach-call.cil.c 190    620 670     420 1.9  49 470   5000 900   5700 59   1800 69   1600 220    5000 14    210 21    76 900   4800 19    310 19   960 14   170 18    19   900 9300 36   770 .22  13  
email_spec11_product32_false-unreach-call.cil.c 350    1000 670     440 3.0  64 900   6300 900   6700 78   1800 64   1700 240    5400 18    210 310    310 900   5100 31    650 19   1100 23   230 19    21   900 8400 52   890 .23  13  
email_spec11_product33_false-unreach-call.cil.c 200    720 650     360 1.9  51 380   4800 900   6500 59   1800 66   1700 220    5000 21    210 170    200 900   5000 30    460 19   1000 19   200 19    21   900 9000 42   830 .25  13  
email_spec11_product35_false-unreach-call.cil.c 430    1200 650     410 3.9  71 900   6800 900   7800 68   2000 59   1800 230    5400 23    210 380    460 900   5400 46    150 20   1100 36   270 18    24   900 9800 52   940 .25  16  
email_spec11_productSimulator_false-unreach-call.cil.c 70    15000 760     4800 690    1700 8.3 380 900   8300 150   3800 120   3400 340    5200 430    850 900    400 900   7400 600    890 21   1400 100   300 360    76   900 9200 48   820 1.8   59  
email_spec1_product14_false-unreach-call.cil.c 130    630 660     540 1.6  48 100   3700 140   3800 28   960 21   820 230    5300 16    210 120    150 38   920 7.6  210 20   960 10   160 19    19   910 9100 53   790 .32  11  
email_spec1_product15_false-unreach-call.cil.c 90    440 680     400 1.5  48 71   3600 130   3200 31   990 20   810 230    5100 15    210 9.3  41 110   3000 5.6  160 21   960 8.1 140 650    43   910 10000 47   800 .19  11  
email_spec1_product16_false-unreach-call.cil.c 75    450 660     410 1.6  49 110   4000 130   3500 33   1000 20   820 230    5100 17    210 12    48 110   3000 6.3  160 20   950 7.3 150 250    23   910 8300 46   830 .19  11  
email_spec1_product20_false-unreach-call.cil.c 170    720 670     420 2.3  53 120   4100 440   3800 32   1000 21   800 220    5200 17    210 140    160 420   3100 18    340 21   950 14   200 140    27   900 7900 52   1000 .23  13  
email_spec1_product21_false-unreach-call.cil.c 170    770 680     410 2.5  55 130   4100 470   3900 30   970 21   810 230    5100 19    210 130    160 440   3200 9.6  310 18   930 12   190 160    21   900 8800 48   790 .27  13  
email_spec1_product22_false-unreach-call.cil.c 98    490 700     300 1.6  47 100   4000 130   3500 31   1000 22   830 230    5000 17    210 150    170 110   3000 7.1  180 21   980 9.1 160 310    33   900 7800 50   1000 .19  11  
email_spec1_product26_false-unreach-call.cil.c 210    840 670     430 3.0  56 250   4200 490   4000 28   960 21   820 220    5100 23    210 210    210 470   3100 18    910 19   960 14   210 140    38   900 8400 54   870 .28  13  
email_spec1_product29_false-unreach-call.cil.c 150    710 670     540 1.7  50 160   4300 140   3900 30   1000 21   820 220    5200 17    210 320    290 40   970 14    360 19   960 11   180 190    25   900 9500 49   810 .22  15  
email_spec1_product30_false-unreach-call.cil.c 90    470 660     430 1.7  48 460   5300 140   3300 33   1100 23   850 230    5400 16    210 12    50 120   3000 6.4  190 20   960 9.5 160 650    65   900 9000 46   810 .21  15  
email_spec1_product31_false-unreach-call.cil.c 81    490 680     420 1.9  48 910   6600 140   3500 29   1000 22   850 230    5100 22    210 20    64 120   2900 5.6  200 19   970 11   180 390    40   900 9600 45   780 .22  13  
email_spec1_product32_false-unreach-call.cil.c 190    800 660     570 3.1  60 900   6400 500   4200 28   980 22   820 230    5300 19    210 220    230 480   3200 14    480 19   1000 18   210 140    42   900 8400 53   1000 .22  16  
email_spec1_product33_false-unreach-call.cil.c 110    550 690     540 2.0  49 180   4100 150   3700 33   1100 23   850 220    5200 23    210 170    190 130   2900 8.8  220 22   1100 8.6 180 400    43   900 9500 44   710 .28  11  
email_spec1_product34_false-unreach-call.cil.c 190    880 660     670 3.6  66 680   6600 540   4900 30   980 22   820 230    5100 24    210 320    340 510   3300 15    480 19   990 18   240 280    26   900 9100 50   880 .29  16  
email_spec1_product35_false-unreach-call.cil.c 240    960 650     670 3.6  68 900   7300 560   4500 32   1000 22   830 230    5400 27    220 66    110 540   3300 29    1200 19   1100 22   260 140    32   900 9300 51   780 .30  16  
email_spec1_productSimulator_false-unreach-call.cil.c 900    14000 730     1700 83    520 10   610 900   7000 48   1700 37   1100 250    5100 230    390 900    510 900   5500 120    470 22   1400 27   270 900    110   900 8700 50   720 1.7   55  
email_spec27_product17_false-unreach-call.cil.c 150    660 61     120 1.7  48 100   3800 280   3700 24   910 15   630 220    5100 16    210 190    210 44   1000 7.7  240 19   960 10   170 900    46   900 9400 57   870 .21  11  
email_spec27_product18_false-unreach-call.cil.c 81    440 7.8   87 1.5  48 120   4100 210   3200 33   1000 23   820 230    5300 16    210 14    52 180   2900 5.4  210 18   950 9.0 150 900    58   900 8200 41   970 .19  15  
email_spec27_product19_false-unreach-call.cil.c 85    460 67     120 1.7  50 900   4900 210   3600 29   990 22   810 230    5200 17    210 16    55 43   990 6.2  220 19   950 11   170 420    31   900 8900 58   1100 .21  13  
email_spec27_product23_false-unreach-call.cil.c 180    730 9.4   84 2.5  54 910   8900 630   4200 22   900 18   650 220    5000 18    210 240    260 600   3100 13    450 20   950 12   180 900    59   900 8700 60   1500 .20  13  
email_spec27_product24_false-unreach-call.cil.c 99    500 8.6   88 1.8  50 360   5000 210   3600 28   1000 19   820 220    5100 20    210 230    270 190   2900 8.7  290 21   970 11   160 400    48   900 9600 57   970 .29  15  
email_spec27_product25_false-unreach-call.cil.c 180    780 66     130 2.6  58 900   9300 650   4200 23   880 18   660 230    5000 24    210 270    270 620   3200 12    380 19   960 16   200 460    42   900 8500 62   1000 .29  13  
email_spec27_product27_false-unreach-call.cil.c 220    850 9.9   85 3.1  61 500   5200 660   4300 23   890 15   660 220    5200 23    210 75    120 650   3300 24    970 19   960 15   220 420    55   900 8900 74   1100 .35  13  
email_spec27_product29_false-unreach-call.cil.c 140    730 150     300 1.9  52 110   3900 310   4300 24   910 18   710 230    5300 18    210 240    270 280   3100 14    400 21   1100 14   190 900    55   900 8000 43   760 .22  12  
email_spec27_product30_false-unreach-call.cil.c 83    470 390     290 1.8  51 360   4000 230   3500 36   1100 23   840 230    5300 16    210 20    73 200   2900 7.0  320 19   960 14   180 900    60   910 9600 43   680 .18  15  
email_spec27_product31_false-unreach-call.cil.c 96    500 580     450 2.0  51 190   4100 230   3700 32   1100 22   840 230    5100 22    210 29    83 210   2900 10    400 18   950 12   180 530    49   910 9400 41   760 .19  11  
email_spec27_product32_false-unreach-call.cil.c 200    820 400     290 3.5  66 560   5300 730   4700 27   950 18   710 230    5100 23    210 240    230 710   3300 20    710 20   1000 16   220 900    85   900 9800 40   750 .28  11  
email_spec27_product33_false-unreach-call.cil.c 91    540 280     220 2.2  52 450   4100 230   3800 30   1100 24   850 220    5100 23    210 140    190 44   970 11    480 19   1000 12   170 440    62   910 10000 40   610 .18  11  
email_spec27_product34_false-unreach-call.cil.c 210    900 630     450 4.1  70 310   4300 760   4500 25   940 17   710 230    5300 22    210 200    230 740   3300 24    730 20   1100 13   200 550    48   900 8700 46   1100 .26  16  
email_spec27_product35_false-unreach-call.cil.c 250    980 280     230 4.3  72 750   5500 790   5600 24   950 20   720 230    5000 26    210 86    140 750   3300 30    170 21   1100 21   250 440    44   900 9700 53   1100 .30  16  
email_spec27_productSimulator_false-unreach-call.cil.c 65    15000 61     420 240    780 900   3600 900   7700 31   1000 24   820 290    5300 680    510 900    480 900   6900 890    1100 21   1400 55   270 900    93   910 10000 47   750 1.7   53  
email_spec3_product13_false-unreach-call.cil.c 1.1  130 78     140 .59 41 24   910 21   600 12   490 10   350 220    5000 13    210 .43 37 14   490 1.5  120 20   970 5.7 120 36    17   520 7400 29   580 .17  17  
email_spec3_product17_false-unreach-call.cil.c 1.8  250 79     150 .73 45 25   880 20   600 12   500 10   350 220    5000 13    200 .54 38 15   530 1.6  140 18   960 5.9 130 36    20   520 7700 66   1300 .19  13  
email_spec3_product18_false-unreach-call.cil.c 1.2  150 5.5   91 .52 43 26   920 17   550 11   490 9.0 350 220    5100 14    210 .58 37 16   510 1.5  130 19   950 6.0 130 18    18   500 7700 27   560 .20  11  
email_spec3_product19_false-unreach-call.cil.c 1.1  160 71     140 .76 43 23   870 21   580 10   490 9.4 350 220    5000 16    210 .56 37 14   500 1.5  130 19   950 5.1 140 36    19   630 7900 25   480 .23  15  
email_spec3_product23_false-unreach-call.cil.c 2.0  290 7.6   89 1.3  51 27   930 21   630 12   510 10   350 220    5000 14    210 .59 37 16   530 2.5  210 20   960 6.2 140 19    21   580 8300 61   1000 .21  13  
email_spec3_product24_false-unreach-call.cil.c 1.4  180 5.6   89 .78 45 25   860 19   570 10   480 9.9 330 230    5000 17    210 .59 37 14   490 1.5  120 20   980 6.2 130 19    20   500 7900 23   470 .25  13  
email_spec3_product25_false-unreach-call.cil.c 2.1  340 82     150 1.4  53 26   920 20   610 12   490 11   350 220    5000 18    210 .55 37 16   530 2.3  210 21   960 6.1 160 37    22   540 7300 68   1600 .21  15  
email_spec3_product27_false-unreach-call.cil.c 2.4  380 7.6   89 1.5  53 26   940 18   590 10   490 10   360 220    5000 20    210 .55 37 15   540 2.4  210 19   940 5.4 170 18    23   530 7600 60   1500 .23  13  
email_spec3_product28_false-unreach-call.cil.c 1.3  160 120     150 .58 43 38   1500 20   620 10   510 11   370 220    5000 13    210 .63 37 15   520 1.5  130 20   950 5.7 130 35    19   910 9600 45   1100 .22  13  
email_spec3_product29_false-unreach-call.cil.c 2.2  330 130     150 .86 46 40   1500 23   650 12   500 10   370 230    5100 13    210 .62 38 17   550 1.9  140 20   1000 6.4 150 36    21   910 9200 48   1000 .22  14  
email_spec3_product30_false-unreach-call.cil.c 1.4  180 7.2   83 .79 46 39   1500 22   650 12   520 11   370 230    5000 13    210 .62 38 14   510 1.7  140 20   1000 6.5 130 18    19   910 9200 38   800 .20  13  
email_spec3_product31_false-unreach-call.cil.c 1.5  210 130     150 .88 47 42   1500 21   660 13   510 10   360 240    5300 16    210 .61 37 15   520 1.5  130 19   1000 6.1 150 36    21   900 9700 41   700 .21  11  
email_spec3_product32_false-unreach-call.cil.c 2.5  380 7.9   86 1.7  58 39   1300 20   610 12   520 9.2 370 220    5000 15    210 .62 38 16   550 2.3  210 19   1000 6.5 160 19    22   900 9600 49   890 .27  14  
email_spec3_product33_false-unreach-call.cil.c 1.7  220 7.8   85 .70 46 38   1500 20   580 12   510 11   370 220    5000 19    210 .61 37 15   510 1.6  130 20   1000 6.2 150 19    22   900 9100 44   770 .26  13  
email_spec3_product34_false-unreach-call.cil.c 2.8  460 140     150 2.0  64 39   1600 21   680 12   510 9.0 370 230    5000 20    210 .61 38 16   550 2.7  210 20   1000 6.8 170 36    24   900 10000 47   840 .28  18  
email_spec3_product35_false-unreach-call.cil.c 3.1  510 7.9   86 1.7  66 39   1400 21   630 12   520 9.7 340 290    6800 20    210 .61 38 17   560 2.2  130 20   1100 6.5 160 19    25   910 10000 50   1000 .34  16  
email_spec3_productSimulator_false-unreach-call.cil.c 86    14000 22     170 47    570 9.1 350 58   1500 13   540 9.5 390 250    5200 48    420 .82 39 41   1200 4.0  290 65   1400 8.0 190 72    49   910 10000 57   1100 1.5   59  
email_spec4_product18_false-unreach-call.cil.c 89    440 660     570 1.6  47 45   2100 180   3300 31   990 21   830 220    5200 15    210 8.8  41 160   3000 5.5  140 20   970 6.7 130 19    18   900 8100 49   950 .20  17  
email_spec4_product19_false-unreach-call.cil.c 80    450 680     440 1.6  48 51   1600 190   3500 30   1000 20   810 220    5300 19    210 14    51 160   2900 6.3  140 19   970 6.8 150 89    19   910 9800 47   980 .25  13  
email_spec4_product23_false-unreach-call.cil.c 170    720 660     380 2.3  54 79   3900 540   4000 33   1100 23   850 230    5300 18    210 220    230 510   3100 8.9  280 19   960 11   190 19    20   900 8000 52   1000 .18  17  
email_spec4_product24_false-unreach-call.cil.c 92    490 670     430 1.7  49 59   3800 190   3500 30   970 20   830 230    5100 20    210 210    230 160   3000 6.6  150 19   940 7.0 150 18    19   900 8300 44   1000 .17  11  
email_spec4_product25_false-unreach-call.cil.c 190    770 660     440 2.6  54 62   3000 560   3900 30   1000 20   840 220    5100 22    210 210    230 530   3200 9.9  250 19   980 9.8 190 88    21   910 8700 58   910 .28  17  
email_spec4_product27_false-unreach-call.cil.c 200    830 680     830 2.9  57 110   4100 570   4000 32   1000 22   840 230    5000 22    210 120    170 46   1000 18    620 19   930 11   190 19    22   910 6600 54   870 .23  13  
email_spec4_product30_false-unreach-call.cil.c 85    470 710     290 1.7  49 87   4000 190   3300 35   1100 22   840 230    5200 16    200 12    50 170   3000 7.0  190 20   990 6.7 150 19    19   910 8200 46   910 .18  13  
email_spec4_product31_false-unreach-call.cil.c 87    490 670     420 1.8  50 110   4100 200   3500 32   1100 20   820 230    5100 22    210 25    73 170   2900 7.8  200 20   950 7.9 150 110    31   900 8100 41   940 .22  15  
email_spec4_product32_false-unreach-call.cil.c 160    790 670     370 3.2  62 900   5700 610   4500 34   1100 25   890 270    6600 21    210 250    230 580   3200 14    480 21   1000 11   180 19    22   900 8300 54   860 .28  14  
email_spec4_product33_false-unreach-call.cil.c 100    550 650     420 1.9  49 93   4400 200   3700 32   1100 22   860 220    5000 23    210 170    190 180   2900 7.4  220 21   1000 8.6 160 19    21   900 8300 42   700 .23  17  
email_spec4_product34_false-unreach-call.cil.c 200    880 660     420 3.6  66 770   6500 650   4500 33   1100 24   850 230    5000 23    210 220    220 54   1200 15    470 20   1000 15   210 110    23   900 8700 51   950 .26  14  
email_spec4_product35_false-unreach-call.cil.c 230    950 670     290 3.8  68 590   6900 660   4400 32   1100 22   860 230    5200 23    210 170    230 640   3400 30    1200 20   1100 13   210 18    24   900 8500 65   1200 .30  12  
email_spec4_productSimulator_false-unreach-call.cil.c 900    14000 710     1600 81    520 11   650 900   7000 52   1800 51   1600 260    5300 230    370 900    480 900   5200 99    460 22   1400 32   260 730    88   910 9400 58   940 1.7   58  
email_spec6_product12_false-unreach-call.cil.c 65    400 660     650 1.3  47 48   2600 120   3200 29   980 20   790 220    5000 15    210 8.8  39 100   2800 4.7  130 18   930 8.4 140 19    16   900 9600 48   870 .15  15  
email_spec6_product14_false-unreach-call.cil.c 150    660 660     760 1.7  48 71   3800 270   3800 27   970 21   820 220    5000 16    210 120    150 250   3100 8.4  230 19   970 14   180 18    19   910 9300 47   990 .20  13  
email_spec6_product15_false-unreach-call.cil.c 78    440 660     410 1.6  49 61   3700 200   3400 31   1000 18   790 220    5000 16    210 8.8  39 170   2900 6.5  190 19   950 11   160 18    17   910 7600 50   980 .20  13  
email_spec6_product16_false-unreach-call.cil.c 80    450 650     590 1.7  49 66   3300 200   3400 31   1000 19   810 230    5300 17    210 9.2  40 180   3000 9.6  200 20   940 12   170 19    18   910 9600 43   780 .24  13  
email_spec6_product20_false-unreach-call.cil.c 170    730 660     350 2.7  55 160   4200 600   4000 31   1000 21   800 290    6900 19    210 140    170 590   3100 16    440 20   950 13   210 18    20   910 9000 44   670 .19  13  
email_spec6_product21_false-unreach-call.cil.c 170    790 660     750 2.6  59 87   3900 630   4100 27   970 21   830 230    5100 24    210 140    170 610   3200 17    380 20   950 19   210 18    21   910 9100 44   830 .20  15  
email_spec6_product22_false-unreach-call.cil.c 93    490 650     500 1.7  47 79   3900 200   3600 29   970 21   820 220    5000 21    210 140    170 180   3000 11    240 19   950 11   170 18    19   900 8700 47   880 .13  17  
email_spec6_product26_false-unreach-call.cil.c 210    870 650     440 3.0  63 99   4000 650   4500 28   970 20   820 230    5300 26    210 210    240 620   3200 19    1100 20   980 15   220 18    22   910 9300 48   960 .27  13  
email_spec6_product28_false-unreach-call.cil.c 90    440 660     290 1.4  48 77   2700 120   3400 28   970 20   810 220    5100 16    210 12    45 100   2900 5.7  170 18   970 11   160 19    18   900 9400 47   830 .24  11  
email_spec6_product29_false-unreach-call.cil.c 160    740 660     350 2.0  53 900   5000 280   3900 29   990 20   820 220    5100 17    210 220    220 250   3100 11    390 19   970 12   190 18    21   910 8800 45   770 .19  13  
email_spec6_product30_false-unreach-call.cil.c 80    470 580     260 1.8  48 89   3800 200   3500 27   960 19   810 220    5100 16    210 11    48 180   2900 13    230 20   950 11   170 19    19   910 8600 47   840 .24  11  
email_spec6_product31_false-unreach-call.cil.c 91    500 660     310 1.9  49 130   4000 210   3700 30   990 21   830 230    5100 17    210 15    51 190   3000 12    240 21   1000 11   180 18    20   900 8600 49   920 .20  11  
email_spec6_product32_false-unreach-call.cil.c 190    820 620     310 3.0  65 410   5200 670   4500 30   970 22   830 230    5300 23    210 260    280 650   3200 17    560 20   1100 20   230 19    22   910 8900 51   840 .23  14  
email_spec6_product33_false-unreach-call.cil.c 110    560 650     400 2.0  49 180   4200 220   3700 33   970 23   840 230    5300 24    210 160    180 190   3000 9.7  260 20   1100 13   190 18    21   900 8800 50   840 .28  15  
email_spec6_product34_false-unreach-call.cil.c 210    910 660     440 3.7  70 130   4000 700   5100 30   990 22   830 230    5000 29    210 340    350