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 false(reach) 9.6  1500 false(reach) 450     330 witness unconfirmed .27 37 timeout 910   11000 false(reach) 24   820 false(reach) 12   540 false(reach) 11   390 unknown .27 45 false(reach) 12    210 witness unconfirmed .81 37 false(reach) 18   580 witness timeout 1.5  68 unknown 23   1400 witness unconfirmed 9.2 190 false(reach) 19    21   timeout 900 9200 timeout 40   670 unknown .66  22  
elevator_spec14_product24_false-unreach-call.cil.c false(reach) 15    2300 exception (gremlins) 1.9   53 witness unconfirmed .28 38 timeout 910   11000 false(reach) 25   860 false(reach) 13   570 false(reach) 11   390 unknown .21 41 false(reach) 13    210 witness unconfirmed 1.3  37 false(reach) 20   590 witness timeout 2.1  100 unknown 23   1500 witness unconfirmed 11   220 false(reach) 18    22   timeout 900 10000 timeout 38   660 unknown .80  37  
elevator_spec14_product28_false-unreach-call.cil.c false(reach) 10    1600 false(reach) 480     330 witness unconfirmed .26 38 timeout 910   10000 false(reach) 21   830 false(reach) 11   550 false(reach) 11   380 unknown .20 40 false(reach) 13    210 witness unconfirmed .99 36 false(reach) 19   580 witness timeout 1.6  68 unknown 23   1400 witness unconfirmed 9.8 210 false(reach) 19    22   timeout 910 9200 timeout 40   640 unknown .78  24  
elevator_spec14_product32_false-unreach-call.cil.c false(reach) 16    2400 exception (gremlins) 1.9   53 witness unconfirmed .33 38 timeout 910   11000 false(reach) 26   870 false(reach) 12   570 false(reach) 9.3 390 unknown .28 46 false(reach) 13    210 witness unconfirmed 1.2  38 false(reach) 21   650 witness timeout 2.3  100 unknown 21   1500 witness unconfirmed 11   230 false(reach) 18    22   timeout 900 9700 timeout 46   720 unknown .91  38  
elevator_spec14_productSimulator_false-unreach-call.cil.c false(reach) 54    7900 exception (gremlins) 140     330 witness unconfirmed 15    420 exception 34   900 false(reach) 150   3000 false(reach) 12   610 false(reach) 9.9 430 unknown .33 47 false(reach) 65    350 witness unconfirmed 1.7  39 false(reach) 130   1700 false(reach) 8.2  230 unknown 25   1400 witness unconfirmed 23   310 false(reach) 18    24   timeout 900 8500 timeout 49   790 unknown 1.9   58  
elevator_spec1_product18_false-unreach-call.cil.c witness unconfirmed 770    1800 timeout 670     450 witness unconfirmed .55 38 timeout 910   11000 false(reach) 120   4100 false(reach) 13   570 false(reach) 11   390 unknown .21 45 witness timeout 15    200 witness unconfirmed 1.1  37 false(reach) 71   1600 false(reach) 7.6  310 unknown 21   1400 witness unconfirmed 8.6 180 false(reach) 18    21   timeout 910 7400 timeout 38   760 unknown .45  18  
elevator_spec1_product20_false-unreach-call.cil.c timeout 900    1900 timeout 680     310 witness unconfirmed .54 38 timeout 910   8500 false(reach) 120   4000 false(reach) 14   580 false(reach) 11   420 unknown .18 41 witness timeout 15    210 witness unconfirmed 1.4  38 false(reach) 74   1700 false(reach) 6.7  330 unknown 22   1400 witness unconfirmed 9.1 200 false(reach) 19    21   timeout 900 8300 timeout 38   710 unknown .50  19  
elevator_spec1_product22_false-unreach-call.cil.c timeout 900    2200 exception (gremlins) 4.2   71 witness unconfirmed .59 38 timeout 910   11000 false(reach) 140   4400 false(reach) 12   600 false(reach) 9.4 410 witness timeout 820    7900 witness timeout 14    210 witness unconfirmed 1.4  37 timeout (false(reach)) 900   7500 false(reach) 12    530 unknown 22   1400 witness unconfirmed 10   200 false(reach) 18    22   timeout 910 9000 timeout 40   630 unknown .54  25  
elevator_spec1_product24_false-unreach-call.cil.c timeout 900    2200 exception (gremlins) 4.0   67 witness unconfirmed .58 39 timeout 910   11000 false(reach) 140   4400 false(reach) 14   620 false(reach) 9.5 430 witness timeout 820    8700 witness timeout 15    210 witness unconfirmed 1.6  38 timeout (false(reach)) 900   7600 false(reach) 12    540 unknown 21   1400 witness unconfirmed 10   220 false(reach) 18    22   timeout 900 8100 timeout 37   670 unknown .53  28  
elevator_spec1_product26_false-unreach-call.cil.c witness unconfirmed 780    1900 timeout 660     310 witness unconfirmed .52 38 timeout 910   11000 false(reach) 120   3700 false(reach) 13   560 false(reach) 9.5 400 unknown .20 40 witness timeout 14    210 witness unconfirmed 1.2  37 timeout (false(reach)) 900   6400 false(reach) 7.5  330 unknown 24   1400 witness unconfirmed 11   220 false(reach) 19    21   timeout 910 9200 timeout 39   650 unknown .41  16  
elevator_spec1_product28_false-unreach-call.cil.c timeout 900    2000 timeout 680     400 witness unconfirmed .55 38 timeout 910   11000 false(reach) 130   4200 false(reach) 14   590 false(reach) 11   430 witness timeout 820    7600 witness timeout 15    210 witness unconfirmed 1.1  38 timeout (false(reach)) 900   6500 false(reach) 7.6  340 unknown 22   1400 witness unconfirmed 9.7 220 false(reach) 18    22   timeout 910 9100 timeout 39   760 unknown .57  17  
elevator_spec1_product30_false-unreach-call.cil.c timeout 900    2200 exception (gremlins) 4.8   83 witness unconfirmed .53 38 timeout 910   11000 false(reach) 150   4400 false(reach) 14   590 false(reach) 11   420 unknown .29 49 witness timeout 14    210 witness unconfirmed 1.3  40 timeout (false(reach)) 900   7400 false(reach) 11    520 unknown 20   1400 witness unconfirmed 10   220 false(reach) 18    22   timeout 910 8800 timeout 41   800 unknown .64  24  
elevator_spec1_product32_false-unreach-call.cil.c timeout 900    2300 exception (gremlins) 5.0   73 witness unconfirmed .44 39 timeout 910   11000 false(reach) 150   4500 false(reach) 13   610 false(reach) 12   420 witness timeout 820    8000 witness timeout 15    210 witness unconfirmed 1.6  38 timeout (false(reach)) 900   7700 false(reach) 12    550 unknown 22   1400 witness unconfirmed 12   210 false(reach) 18    23   timeout 910 9400 timeout 37   740 unknown .71  27  
elevator_spec1_productSimulator_false-unreach-call.cil.c timeout 900    4200 timeout 690     990 witness unconfirmed 96    1100 exception 34   840 false(reach) 350   5800 false(reach) 15   640 false(reach) 11   470 witness timeout 800    5700 witness timeout 590    430 witness unconfirmed 41    58 timeout (false(reach)) 900   9500 false(reach) 35    310 unknown 23   1500 witness unconfirmed 13   230 witness timeout 18    25   timeout 900 11000 timeout 43   650 unknown 1.4   43  
elevator_spec2_product18_false-unreach-call.cil.c witness unconfirmed 650    1800 timeout 680     320 witness unconfirmed .54 38 timeout 900   11000 false(reach) 120   4200 false(reach) 13   540 false(reach) 11   400 unknown .22 44 false(reach) 13    210 witness unconfirmed 1.1  37 timeout (false(reach)) 900   6400 false(reach) 3.6  170 unknown 22   1400 witness unconfirmed 9.5 210 false(reach) 18    21   timeout 910 8500 timeout 69   1100 unknown .53  21  
elevator_spec2_product20_false-unreach-call.cil.c witness unconfirmed 900    2000 timeout 680     380 witness unconfirmed .53 38 timeout 910   11000 false(reach) 120   4200 false(reach) 14   580 false(reach) 9.3 420 timeout 910    9300 false(reach) 13    210 witness unconfirmed 1.3  37 timeout (false(reach)) 900   6500 false(reach) 3.9  160 unknown 22   1400 witness unconfirmed 10   210 false(reach) 18    21   timeout 910 9400 timeout 62   1000 unknown .49  21  
elevator_spec2_product22_false-unreach-call.cil.c timeout 900    2200 exception (gremlins) 3.1   67 witness unconfirmed .53 38 timeout 900   11000 false(reach) 140   4300 false(reach) 13   580 false(reach) 11   400 unknown .18 45 false(reach) 15    210 witness unconfirmed 1.3  38 timeout (false(reach)) 900   7400 false(reach) 6.4  310 unknown 22   1400 witness unconfirmed 9.7 200 false(reach) 18    22   timeout 910 10000 timeout 60   1400 unknown .59  25  
elevator_spec2_product24_false-unreach-call.cil.c timeout 900    2200 exception (gremlins) 3.9   64 witness unconfirmed .58 39 timeout 910   11000 false(reach) 140   4500 false(reach) 12   590 false(reach) 11   410 unknown .19 43 false(reach) 14    210 witness unconfirmed 1.3  38 false(reach) 80   1800 false(reach) 6.5  320 unknown 24   1500 witness unconfirmed 9.4 210 false(reach) 18    22   timeout 910 10000 timeout 68   1200 unknown .48  22  
elevator_spec2_product26_false-unreach-call.cil.c witness unconfirmed 750    1900 timeout 700     630 witness unconfirmed .58 38 timeout 910   11000 false(reach) 120   4100 false(reach) 12   560 false(reach) 11   380 unknown .23 41 false(reach) 15    210 witness unconfirmed 1.1  37 timeout (false(reach)) 900   6400 false(reach) 3.7  160 unknown 23   1400 witness unconfirmed 10   200 false(reach) 19    21   timeout 910 9700 timeout 76   1500 unknown .53  21  
elevator_spec2_product28_false-unreach-call.cil.c timeout 900    2000 timeout 680     450 witness unconfirmed .58 38 timeout 910   11000 false(reach) 130   4200 false(reach) 14   570 false(reach) 11   400 unknown .22 41 false(reach) 15    210 witness unconfirmed 1.3  37 timeout (false(reach)) 900   6500 false(reach) 4.3  160 unknown 23   1500 witness unconfirmed 9.0 230 false(reach) 19    22   timeout 910 10000 timeout 65   1200 unknown .55  19  
elevator_spec2_product30_false-unreach-call.cil.c timeout 900    2300 exception (gremlins) 4.1   76 witness unconfirmed .43 38 timeout 910   11000 false(reach) 150   4400 false(reach) 14   580 false(reach) 9.3 410 unknown .24 45 false(reach) 15    210 witness unconfirmed 1.3  38 timeout (false(reach)) 900   7400 false(reach) 6.5  310 unknown 22   1400 witness unconfirmed 10   220 false(reach) 19    22   timeout 910 9700 timeout 54   1100 unknown .68  24  
elevator_spec2_product32_false-unreach-call.cil.c timeout 900    2300 exception (gremlins) 5.1   69 witness unconfirmed .59 39 timeout 910   11000 false(reach) 150   4400 false(reach) 14   580 false(reach) 11   420 unknown .29 47 false(reach) 15    210 witness unconfirmed 1.7  38 timeout (false(reach)) 900   7700 false(reach) 6.5  320 unknown 22   1400 witness unconfirmed 10   230 false(reach) 18    23   timeout 910 11000 timeout 72   1400 unknown .70  27  
elevator_spec2_productSimulator_false-unreach-call.cil.c timeout 900    4200 timeout 710     740 witness unconfirmed 60    920 timeout 910   11000 false(reach) 350   6000 false(reach) 16   640 false(reach) 13   530 witness timeout 800    6300 witness timeout 590    430 witness unconfirmed 45    69 timeout (false(reach)) 900   9500 false(reach) 28    260 unknown 25   1400 witness unconfirmed 14   270 witness timeout 18    24   timeout 910 9100 timeout 48   810 unknown 1.4   43  
elevator_spec3_product03_false-unreach-call.cil.c false(reach) 5.0  760 false(reach) .65  58 witness unconfirmed .37 39 timeout 910   11000 false(reach) 26   760 false(reach) 16   610 false(reach) 10   460 unknown .21 47 false(reach) 13    210 witness unconfirmed 2.1  38 false(reach) 18   570 witness timeout .87 49 unknown 20   1200 witness unconfirmed 14   250 false(reach) 18    22   timeout 910 10000 timeout 39   720 unknown .44  17  
elevator_spec3_product11_false-unreach-call.cil.c false(reach) 5.3  800 false(reach) .73  62 witness unconfirmed .38 39 timeout 910   11000 false(reach) 25   760 false(reach) 15   620 false(reach) 12   460 unknown .22 48 false(reach) 13    210 witness unconfirmed 2.1  38 false(reach) 19   600 witness timeout 1.0  48 unknown 21   1100 witness unconfirmed 17   300 false(reach) 19    22   timeout 900 9900 timeout 39   690 unknown .54  19  
elevator_spec3_product19_false-unreach-call.cil.c false(reach) 5.5  840 false(reach) .81  64 witness unconfirmed .40 39 timeout 910   11000 false(reach) 25   770 false(reach) 15   630 false(reach) 11   460 unknown .24 47 false(reach) 13    210 witness unconfirmed 2.1  38 false(reach) 19   580 witness timeout .95 47 unknown 21   1400 witness unconfirmed 13   240 false(reach) 19    22   timeout 900 10000 timeout 64   960 unknown .51  17  
elevator_spec3_product20_false-unreach-call.cil.c false(reach) 10    1600 false(reach) .64  64 witness unconfirmed .40 39 timeout 900   6500 false(reach) 29   890 false(reach) 15   650 false(reach) 11   480 unknown .25 41 false(reach) 14    210 witness unconfirmed 2.4  38 false(reach) 22   650 witness timeout 1.2  75 unknown 21   1400 witness unconfirmed 12   240 false(reach) 18    22   timeout 900 9200 timeout 40   780 unknown .70  28  
elevator_spec3_product23_false-unreach-call.cil.c false(reach) 8.4  1300 exception (gremlins) 1.8   50 witness unconfirmed .38 40 timeout 910   11000 false(reach) 27   810 false(reach) 16   660 false(reach) 11   470 unknown .24 44 false(reach) 13    210 witness unconfirmed 2.5  39 false(reach) 22   630 witness timeout 1.1  66 unknown 21   1200 witness unconfirmed 15   250 false(reach) 18    23   timeout 910 9300 timeout 39   760 unknown .59  26  
elevator_spec3_product24_false-unreach-call.cil.c false(reach) 16    2400 exception (gremlins) 1.7   52 witness unconfirmed .41 40 timeout 900   9600 false(reach) 32   970 false(reach) 15   670 false(reach) 13   500 unknown .24 46 false(reach) 14    210 witness unconfirmed 2.7  39 false(reach) 24   810 witness timeout 1.6  89 unknown 22   1400 witness unconfirmed 15   260 false(reach) 18    23   timeout 910 10000 timeout 41   810 unknown .82  36  
elevator_spec3_product27_false-unreach-call.cil.c false(reach) 5.7  890 false(reach) .63  62 witness unconfirmed .28 39 timeout 910   11000 false(reach) 27   750 false(reach) 14   630 false(reach) 11   460 false(reach) 820    8800 false(reach) 13    210 witness unconfirmed 1.9  38 false(reach) 21   590 witness timeout .96 48 unknown 23   1500 witness unconfirmed 13   240 false(reach) 19    23   timeout 900 11000 timeout 38   730 unknown .53  22  
elevator_spec3_product28_false-unreach-call.cil.c false(reach) 11    1700 false(reach) .83  64 witness unconfirmed .38 39 timeout 900   8200 false(reach) 27   890 false(reach) 15   640 false(reach) 13   470 unknown .21 41 false(reach) 13    210 witness unconfirmed 2.4  38 false(reach) 20   630 witness timeout 1.5  78 unknown 23   1400 witness unconfirmed 14   260 false(reach) 18    23   timeout 900 10000 timeout 40   740 unknown .80  28  
elevator_spec3_product31_false-unreach-call.cil.c false(reach) 8.6  1300 exception (gremlins) 1.8   50 witness unconfirmed .30 40 timeout 910   11000 false(reach) 27   810 false(reach) 16   650 false(reach) 13   470 unknown .24 48 false(reach) 12    220 witness unconfirmed 2.4  39 false(reach) 20   620 witness timeout 1.2  59 unknown 20   1100 witness unconfirmed 15   260 false(reach) 19    23   timeout 910 10000 timeout 39   710 unknown .61  22  
elevator_spec3_product32_false-unreach-call.cil.c false(reach) 16    2600 exception (gremlins) 1.7   50 witness unconfirmed .39 40 timeout 910   11000 false(reach) 29   900 false(reach) 16   640 false(reach) 13   500 unknown .25 47 false(reach) 13    210 witness unconfirmed 2.7  39 false(reach) 22   710 witness timeout 2.0  91 unknown 20   1400 witness unconfirmed 17   250 false(reach) 18    24   timeout 900 11000 timeout 39   820 unknown .93  38  
elevator_spec3_productSimulator_false-unreach-call.cil.c witness timeout 60    8500 exception (gremlins) 430     300 witness unconfirmed 56    880 timeout 910   11000 timeout 900   5400 false(reach) 25   930 false(reach) 19   710 unknown .27 49 witness timeout 140    570 witness timeout 8.8  43 timeout 900   2600 false(reach) 9.4  230 unknown 24   1400 witness timeout 32   320 false(reach) 18    26   timeout 910 9500 timeout 42   750 unknown 1.9   54  
elevator_spec9_product26_false-unreach-call.cil.c witness unconfirmed 700    1900 timeout 670     580 witness unconfirmed .58 38 timeout 910   11000 false(reach) 120   4200 false(reach) 11   560 false(reach) 9.2 400 unknown .25 43 false(reach) 14    210 witness unconfirmed 1.3  37 timeout (false(reach)) 900   6400 false(reach) 3.9  160 unknown 19   1400 witness unconfirmed 9.4 200 false(reach) 18    21   timeout 910 10000 timeout 72   1100 unknown .50  21  
elevator_spec9_product28_false-unreach-call.cil.c timeout 900    2000 timeout 680     450 witness unconfirmed .60 38 timeout 900   8900 false(reach) 130   4300 false(reach) 14   590 false(reach) 11   420 unknown .21 41 false(reach) 15    210 witness unconfirmed 1.5  38 timeout (false(reach)) 900   6500 false(reach) 4.0  160 unknown 24   1500 witness unconfirmed 11   220 false(reach) 18    22   timeout 900 11000 timeout 74   1400 unknown .56  17  
elevator_spec9_product30_false-unreach-call.cil.c timeout 900    2200 exception (gremlins) 75     170 witness unconfirmed .59 38 timeout 910   11000 false(reach) 140   4300 false(reach) 14   580 false(reach) 11   420 unknown .24 45 false(reach) 15    210 witness unconfirmed 1.5  38 timeout (false(reach)) 900   7500 false(reach) 6.9  310 unknown 20   1400 witness unconfirmed 10   210 false(reach) 19    22   timeout 900 10000 timeout 66   1300 unknown .58  22  
elevator_spec9_product32_false-unreach-call.cil.c timeout 900    2300 exception (gremlins) 100     190 witness unconfirmed .59 39 timeout 910   11000 false(reach) 160   4500 false(reach) 13   600 false(reach) 9.5 430 unknown .19 44 false(reach) 13    210 witness unconfirmed 1.8  38 timeout (false(reach)) 900   8100 false(reach) 6.3  310 unknown 21   1400 witness unconfirmed 12   240 false(reach) 19    22   timeout 900 10000 timeout 62   1500 unknown .62  23  
elevator_spec9_productSimulator_false-unreach-call.cil.c timeout 900    4200 timeout 700     960 witness unconfirmed 60    920 timeout 910   11000 false(reach) 310   5600 false(reach) 15   640 false(reach) 11   470 unknown .34 49 false(reach) 570    410 witness unconfirmed 47    67 timeout (false(reach)) 900   9600 false(reach) 21    240 unknown 24   1500 witness timeout 14   250 witness timeout 19    25   timeout 900 10000 timeout 61   1000 unknown 1.3   45  
elevator_spec13_product21_true-unreach-call.cil.c error(signal 6) 7.0  1200 exception (gremlins) 2.2   53 true 6.2  71 timeout 910   10000 timeout 900   7500 true 7.2 280 true 5.3 240 unknown .20 43 true 1.7  55 true 3.8  36 timeout 910   12000 true 54    840 unknown 22   1200 true 72   370 timeout 850    15000   timeout 900 9200 timeout 59   1000 unknown .54  23  
elevator_spec13_product22_true-unreach-call.cil.c error(signal 6) 13    2300 exception (gremlins) 2.5   55 true 6.4  72 timeout 900   7800 timeout 900   8000 true 6.3 270 true 5.5 240 unknown .23 43 true 1.7  55 true 4.2  36 timeout 900   11000 true 130    1100 unknown 21   1400 true 100   380 timeout 870    15000   timeout 900 10000 timeout 58   1000 unknown .82  35  
elevator_spec13_product23_true-unreach-call.cil.c error(signal 6) 7.5  1300 exception (gremlins) 2.6   53 true 5.0  50 timeout 910   11000 timeout 910   8300 true 7.4 280 true 6.3 240 unknown .22 41 true 1.3  56 true 5.4  37 true 97   2600 true 160    930 unknown 22   1300 true 150   460 timeout 860    15000   timeout 900 9400 timeout 47   840 unknown .66  23  
elevator_spec13_product24_true-unreach-call.cil.c error(signal 6) 15    2500 exception (gremlins) 3.1   55 true 5.2  51 timeout 900   7100 timeout 900   7900 true 6.5 290 true 6.6 250 unknown .21 46 true 1.7  58 true 5.8  37 true 110   3200 true 88    980 unknown 22   1400 true 140   410 timeout 880    15000   timeout 910 8300 timeout 40   840 unknown .85  33  
elevator_spec13_product29_true-unreach-call.cil.c error(signal 6) 7.2  1300 exception (gremlins) 2.9   58 true 6.2  72 timeout 900   11000 timeout 900   8200 true 7.1 280 true 5.3 240 true .89 53 true 1.7  55 true 3.8  36 timeout 910   12000 true 78    920 unknown 21   1200 true 66   370 timeout 860    15000   timeout 910 9500 timeout 43   780 unknown .59  25  
elevator_spec13_product30_true-unreach-call.cil.c error(signal 6) 14    2400 exception (gremlins) 3.3   60 true 6.4  72 timeout 910   8200 timeout 910   7800 true 6.2 280 true 5.4 240 unknown .18 42 true 1.7  55 true 4.3  36 timeout 910   11000 true 130    1100 unknown 22   1400 true 67   370 timeout 860    15000   timeout 910 8200 timeout 49   870 unknown .90  34  
elevator_spec13_product31_true-unreach-call.cil.c error(signal 6) 7.7  1400 exception (gremlins) 3.1   60 true 5.0  53 timeout 900   11000 timeout 910   8200 true 7.4 280 true 6.7 240 unknown .20 43 true 1.8  56 true 5.3  38 true 99   2500 true 120    820 unknown 20   1300 true 140   450 timeout 860    15000   timeout 900 8600 timeout 43   780 unknown .58  28  
elevator_spec13_product32_true-unreach-call.cil.c error(signal 6) 15    2600 exception (gremlins) 2.5   58 true 5.0  51 timeout 910   8300 timeout 910   8000 true 6.4 290 true 6.8 250 unknown .24 41 true 1.3  56 true 6.0  37 true 110   2700 true 160    810 unknown 23   1500 true 160   440 timeout 860    15000   timeout 910 7900 timeout 47   840 unknown .73  38  
elevator_spec13_productSimulator_true-unreach-call.cil.c error(signal 6) 56    8500 exception (gremlins) 3.5   85 true 850    420 exception 610   6700 timeout 900   8700 true 9.8 430 true 9.3 320 unknown .32 49 unknown 900    7000 true 32    50 timeout 910   11000 true 620    1300 unknown 23   1400 true 630   580 timeout 860    15000   timeout 900 8100 timeout 48   810 unknown 1.9   56  
elevator_spec14_product03_true-unreach-call.cil.c true 750    1800 timeout 680     420 true 2.9  36 timeout 910   9900 true 250   5200 true 8.8 300 true 7.9 270 unknown .22 47 true 1.7  54 true 22    38 timeout 900   7000 true 2.0  140 unknown 21   1200 true 130   510 true 18    21   timeout 900 8500 timeout 42   650 unknown .42  20  
elevator_spec14_product11_true-unreach-call.cil.c true 820    1800 timeout 680     420 true 2.9  37 timeout 910   10000 true 200   5100 true 8.7 310 true 8.0 280 true .40 51 true 1.8  55 true 22    39 timeout 900   7200 true 2.2  150 unknown 21   1100 true 140   530 true 18    21   timeout 900 9000 timeout 42   770 unknown .36  18  
elevator_spec14_product19_true-unreach-call.cil.c timeout 900    1900 timeout 680     470 true 3.0  37 timeout 910   11000 true 470   6300 true 8.7 310 true 6.8 270 unknown .22 40 true 1.7  54 true 23    39 timeout 900   7200 true 2.1  150 unknown 20   1100 true 76   460 true 18    21   timeout 910 8600 timeout 44   760 unknown .48  20  
elevator_spec14_product23_true-unreach-call.cil.c true 350    1700 exception (gremlins) 1.9   53 true 3.3  37 timeout 910   10000 timeout 900   7200 true 9.1 330 true 8.3 290 unknown .18 47 true 1.7  55 true 37    39 timeout 900   8200 true 1.3  52 unknown 67   1300 true 95   470 true 18    22   timeout 900 8600 timeout 72   1200 unknown .53  21  
elevator_spec14_product27_true-unreach-call.cil.c timeout 900    1900 timeout 690     430 true 3.0  37 timeout 900   10000 true 490   6500 true 7.5 310 true 6.5 280 unknown .22 41 true 1.7  54 true 23    40 timeout 900   7200 true 2.3  150 unknown 20   1100 true 94   500 true 19    21   timeout 900 8400 timeout 42   700 unknown .48  19  
elevator_spec14_product31_true-unreach-call.cil.c true 450    1800 exception (gremlins) 1.9   53 true 3.3  37 timeout 910   11000 timeout 900   7400 true 9.2 330 true 8.2 290 unknown .24 46 true 1.7  55 true 36    39 timeout 900   8300 true 1.3  53 unknown 22   1400 true 110   510 true 18    22   timeout 900 8900 timeout 43   820 unknown .63  24  
elevator_spec1_product01_true-unreach-call.cil.c timeout 900    1800 timeout 660     300 true 2.6  37 timeout 910   11000 true 600   6800 true 8.3 300 true 7.0 260 unknown .21 40 true 2.4  55 true 14    37 timeout (true) 900   8900 true 15    190 unknown 23   1500 true 42   380 true 18    20   timeout 910 8600 timeout 35   620 unknown .41  17  
elevator_spec1_product03_true-unreach-call.cil.c timeout 900    1700 timeout 660     480 true 2.8  38 timeout 910   11000 true 660   7000 true 8.5 310 true 7.5 270 true .34 51 true 2.5  56 true 21    40 timeout (true) 900   9200 true 12    190 unknown 65   1300 true 54   470 true 18    21   timeout 900 9100 timeout 37   640 unknown .26  15  
elevator_spec1_product09_true-unreach-call.cil.c timeout 900    1800 timeout 650     430 true 2.7  38 timeout 910   11000 true 610   7000 true 7.9 300 true 7.1 260 unknown .27 47 true 2.4  55 true 14    37 timeout (true) 900   9000 true 14    190 unknown 20   1100 true 49   440 true 18    20   timeout 900 10000 timeout 38   790 unknown .34  17  
elevator_spec1_product11_true-unreach-call.cil.c timeout 900    1700 timeout 660     440 true 2.8  38 timeout 910   11000 true 790   7400 true 7.0 310 true 7.5 270 unknown .23 41 true 2.6  56 true 22    40 timeout (true) 900   9200 true 18    210 unknown 21   1200 true 70   520 true 18    21   timeout 900 10000 timeout 39   730 unknown .35  17  
elevator_spec1_product17_true-unreach-call.cil.c timeout 900    1700 timeout 670     450 true 2.6  37 timeout 910   11000 true 670   7000 true 6.9 310 true 6.1 270 unknown .25 45 true 2.5  55 true 15    37 timeout (true) 900   8700 true 15    190 unknown 19   1100 true 32   350 true 18    20   timeout 910 9100 timeout 37   830 unknown .30  14  
elevator_spec1_product19_true-unreach-call.cil.c timeout 900    1700 timeout 670     420 true 2.8  38 timeout 910   11000 true 830   7500 true 7.0 310 true 7.7 280 unknown .23 44 true 2.3  56 true 22    41 timeout (true) 900   8900 true 16    190 unknown 20   1100 true 73   460 true 18    21   timeout 900 8500 timeout 36   610 unknown .44  13  
elevator_spec1_product21_true-unreach-call.cil.c timeout 900    1800 exception (gremlins) 5.3   96 true 2.9  38 timeout 900   11000 timeout 900   7100 true 7.0 310 true 6.3 270 unknown .15 42 true 5.4  57 true 19    39 timeout (true) 900   8700 true 78    310 unknown 23   1400 true 96   490 true 18    21   timeout 900 9400 timeout 41   780 unknown .43  17  
elevator_spec1_product23_true-unreach-call.cil.c timeout 900    1700 exception (gremlins) 39     190 true 3.0  38 timeout 910   11000 timeout 900   7200 true 8.6 310 true 6.9 280 unknown .24 49 true 5.2  58 true 28    46 timeout (true) 900   9000 true 67    320 unknown 19   1100 true 110   520 true 18    22   timeout 910 9600 timeout 38   630 unknown .46  15  
elevator_spec1_product25_true-unreach-call.cil.c timeout 900    1800 timeout 670     430 true 2.3  38 timeout 910   11000 true 830   7800 true 6.9 290 true 5.9 260 unknown .23 47 true 2.5  55 true 15    37 timeout (true) 900   8900 true 14    200 unknown 20   1100 true 40   390 true 18    21   timeout 900 9900 timeout 35   620 unknown .40  13  
elevator_spec1_product27_true-unreach-call.cil.c timeout 900    1700 timeout 670     420 true 2.9  38 timeout 910   11000 true 730   7400 true 8.5 310 true 6.4 270 unknown .22 46 true 2.6  56 true 22    41 timeout (true) 900   9100 true 12    200 unknown 20   1300 true 61   460 true 19    21   timeout 910 8700 timeout 38   800 unknown .39  19  
elevator_spec1_product29_true-unreach-call.cil.c timeout 900    1700 exception (gremlins) 5.3   100 true 3.2  38 timeout 910   11000 timeout 900   7000 true 8.5 300 true 7.4 270 true .40 52 true 5.2  57 true 19    38 timeout (true) 900   8600 true 86    320 unknown 62   1100 true 70   470 true 18    22   timeout 910 9700 timeout 37   790 unknown .46  19  
elevator_spec1_product31_true-unreach-call.cil.c timeout 900    1700 exception (gremlins) 39     190 true 3.1  39 timeout 910   11000 timeout 900   7400 true 8.6 320 true 6.7 280 unknown .20 46 true 5.1  59 true 27    45 timeout (true) 900   9300 true 120    370 unknown 21   1300 true 110   510 true 18    22   timeout 900 8900 timeout 37   730 unknown .54  21  
elevator_spec2_product01_true-unreach-call.cil.c timeout 900    1800 timeout 650     440 true 2.3  37 timeout 910   9000 true 150   4500 true 7.5 280 true 5.3 240 unknown .24 46 true 3.2  55 true 4.1  36 timeout (true) 900   5700 true 3.6  110 unknown 21   1100 true 30   360 true 18    20   timeout 910 9100 timeout 54   1100 unknown .30  16  
elevator_spec2_product03_true-unreach-call.cil.c timeout 900    1700 timeout 670     560 true 2.3  38 timeout 900   11000 true 170   4600 true 7.5 280 true 6.6 240 unknown .25 44 true 2.7  56 true 5.6  36 timeout (true) 900   6000 true 3.5  110 unknown 22   1400 true 29   330 true 18    21   timeout 900 8800 timeout 49   1000 unknown .34  12  
elevator_spec2_product09_true-unreach-call.cil.c timeout 900    1700 timeout 650     440 true 2.1  38 timeout 910   11000 true 160   4500 true 7.4 280 true 5.5 240 unknown .24 43 true 3.1  55 true 4.3  36 timeout (true) 900   5800 true 3.6  110 unknown 21   1100 true 32   360 true 18    20   timeout 900 8500 timeout 55   920 unknown .28  14  
elevator_spec2_product11_true-unreach-call.cil.c timeout 900    1700 timeout 670     660 true 2.0  38 timeout 910   11000 true 170   4600 true 7.7 280 true 6.4 250 unknown .16 44 true 3.4  56 true 5.9  36 timeout (true) 900   6000 true 3.2  110 unknown 19   1100 true 37   350 true 19    21   timeout 900 8800 timeout 53   1100 unknown .48  13  
elevator_spec2_product17_true-unreach-call.cil.c timeout 900    1700 timeout 670     420 true 2.2  38 timeout 910   11000 true 140   4500 true 7.0 280 true 6.4 240 unknown .22 42 true 3.3  55 true 4.3  36 timeout (true) 900   5700 true 3.0  110 unknown 21   1100 true 28   340 true 18    20   timeout 910 9200 timeout 59   1100 unknown .34  12  
elevator_spec2_product19_true-unreach-call.cil.c timeout 900    1800 timeout 670     450 true 2.5  38 timeout 910   11000 true 160   4700 true 7.6 290 true 5.6 250 unknown .19 41 true 3.4  56 true 6.2  36 timeout (true) 900   6000 true 3.2  100 unknown 22   1100 true 36   370 true 18    21   timeout 900 8600 timeout 52   1000 unknown .39  17  
elevator_spec2_product21_true-unreach-call.cil.c timeout 900    1800 exception (gremlins) 5.6   89 true 2.3  38 timeout 910   11000 true 210   4700 true 7.4 280 true 6.5 240 unknown .22 46 true 3.4  56 true 4.9  38 timeout (true) 900   7900 true 7.6  180 unknown 19   1200 true 25   320 true 18    21   timeout 900 9500 timeout 66   1400 unknown .42  19  
elevator_spec2_product23_true-unreach-call.cil.c timeout 900    1800 exception (gremlins) 51     290 true 2.4  38 timeout 910   11000 true 260   5100 true 6.5 290 true 6.6 240 unknown .24 49 true 3.6  57 true 7.0  37 timeout (true) 900   7900 true 8.2  180 unknown 21   1200 true 36   380 true 18    22   timeout 910 10000 timeout 49   830 unknown .42  20  
elevator_spec2_product25_true-unreach-call.cil.c timeout 900    1700 timeout 670     450 true 2.2  38 timeout 910   11000 true 150   4700 true 7.3 290 true 6.3 240 true .35 51 true 2.5  55 true 4.4  36 timeout (true) 900   5800 true 3.5  110 unknown 20   1100 true 26   320 true 18    21   timeout 900 8900 timeout 57   900 unknown .36  15  
elevator_spec2_product27_true-unreach-call.cil.c timeout 900    1800 timeout 680     450 true 2.3  38 timeout 900   11000 true 190   4900 true 7.7 290 true 5.6 250 true .35 51 true 3.4  56 true 6.0  37 timeout (true) 900   5900 true 3.6  100 unknown 18   1100 true 30   350 true 18    21   timeout 900 8400 timeout 52   1000 unknown .36  15  
elevator_spec2_product29_true-unreach-call.cil.c timeout 900    1700 exception (gremlins) 5.1   90 true 2.2  38 timeout 910   11000 true 240   4900 true 7.6 280 true 6.5 240 true .37 51 true 3.3  56 true 5.0  37 timeout (true) 900   7700 true 6.5  180 unknown 21   1200 true 33   350 true 18    21   timeout 910 10000 timeout 64   1400 unknown .47  20  
elevator_spec2_product31_true-unreach-call.cil.c timeout 900    1800 exception (gremlins) 50     290 true 2.7  39 timeout 910   11000 true 280   5100 true 7.7 290 true 6.6 250 unknown .24 46 true 3.4  58 true 7.2  37 timeout (true) 900   8100 true 7.7  180 unknown 22   1300 true 28   330 true 19    22   timeout 900 9300 timeout 50   800 unknown .54  18  
elevator_spec3_product01_true-unreach-call.cil.c true 4.6  680 timeout 700     420 true 3.3  37 timeout 910   10000 true 110   3800 true 9.0 320 true 7.0 290 true .41 51 true 1.7  55 true 29    48 timeout (true) 900   5400 true 1.7  120 unknown 21   1100 true 23   330 true 18    21   timeout 900 8100 timeout 64   1100 unknown .40  17  
elevator_spec3_product09_true-unreach-call.cil.c true 5.0  730 timeout 690     420 true 3.3  37 timeout 910   11000 true 100   3600 true 7.8 320 true 7.9 290 unknown .20 43 true 1.6  55 true 26    46 timeout (true) 900   5000 true 1.8  120 unknown 21   1400 true 20   310 true 19    21   timeout 910 8200 timeout 43   690 unknown .48  19  
elevator_spec3_product17_true-unreach-call.cil.c true 5.1  770 timeout 700     420 true 3.4  37 timeout 900   11000 true 100   3600 true 8.9 320 true 8.3 280 unknown .20 44 true 1.7  55 true 27    48 timeout (true) 900   5000 true 1.7  130 unknown 19   1100 true 20   300 true 19    22   timeout 910 9500 timeout 41   770 unknown .33  15  
elevator_spec3_product18_true-unreach-call.cil.c true 9.7  1400 timeout 680     290 true 3.4  37 timeout 900   11000 true 140   4600 true 8.9 320 true 6.7 280 unknown .21 44 true 1.7  55 true 33    51 timeout (true) 900   7100 true 3.0  180 unknown 21   1400 true 22   330 true 18    22   timeout 910 8300 timeout 43   820 unknown .69  27  
elevator_spec3_product21_true-unreach-call.cil.c true 7.7  1200 exception (gremlins) 5.2   59 true 3.6  37 timeout 910   11000 true 120   4600 true 9.4 330 true 8.4 290 unknown .22 45 true 1.8  56 true 39    62 timeout (true) 900   7500 true 2.3  160 unknown 22   1400 true 24   310 true 19    22   timeout 900 8900 timeout 41   810 unknown .58  26  
elevator_spec3_product22_true-unreach-call.cil.c true 15    2200 exception (gremlins) 4.8   61 true 3.8  37 timeout 900   10000 true 180   4800 true 7.9 340 true 8.3 290 unknown .24 46 true 1.8  56 true 45    65 timeout (true) 900   7700 true 4.6  290 unknown 21   1400 true 25   280 true 18    23   timeout 900 8400 timeout 39   760 unknown .84  35  
elevator_spec3_product25_true-unreach-call.cil.c true 5.2  810 timeout 700     420 true 3.2  37 timeout 910   11000 true 100   3700 true 7.5 320 true 8.2 280 unknown .25 45 true 1.3  55 true 27    46 timeout (true) 900   5100 true 1.8  130 unknown 22   1400 true 24   330 true 19    22   timeout 910 8000 timeout 42   790 unknown .52  17  
elevator_spec3_product26_true-unreach-call.cil.c true 10    1500 timeout 680     290 true 3.4  37 timeout 910   11000 true 120   4500 true 7.8 320 true 6.9 290 true .30 52 true 1.4  55 true 30    49 timeout (true) 900   6700 true 3.2  180 unknown 23   1400 true 19   290 true 18    22   timeout 900 8600 timeout 37   780 unknown .77  25  
elevator_spec3_product29_true-unreach-call.cil.c true 8.0  1200 exception (gremlins) 5.3   56 true 3.7  37 timeout 910   11000 true 130   4600 true 9.7 330 true 7.2 300 true .40 52 true 1.8  56 true 37    57 timeout (true) 900   7400 true 2.4  170 unknown 20   1200 true 21   300 true 19    23   timeout 900 9500 timeout 42   770 unknown .59  26  
elevator_spec3_product30_true-unreach-call.cil.c true 16    2300 exception (gremlins) 5.4   59 true 3.8  37 timeout 900   11000 true 170   4900 true 9.5 330 true 8.4 300 true .43 53 true 1.8  56 true 38    62 timeout (true) 900   8800 true 4.8  310 unknown 21   1400 true 27   310 true 18    23   timeout 910 9500 timeout 39   660 unknown .96  37  
elevator_spec9_product09_true-unreach-call.cil.c timeout 900    1800 timeout 650     430 true 2.1  38 timeout 900   11000 true 170   4500 true 7.5 280 true 5.2 240 unknown .19 41 true 3.1  55 true 4.3  36 timeout (true) 900   5900 true 3.2  110 unknown 20   1100 true 32   370 true 18    20   timeout 910 8700 timeout 57   1000 unknown .28  17  
elevator_spec9_product11_true-unreach-call.cil.c timeout 900    1800 timeout 660     550 true 2.4  38 timeout 910   11000 true 160   4700 true 7.5 280 true 6.6 250 true .35 51 true 3.2  56 true 6.3  36 timeout (true) 900   6100 true 3.5  99 unknown 19   1200 true 31   360 true 19    21   timeout 900 9100 timeout 60   1100 unknown .39  17  
elevator_spec9_product25_true-unreach-call.cil.c timeout 900    1700 timeout 670     460 true 2.3  38 timeout 910   11000 true 150   4500 true 6.4 280 true 5.6 240 unknown .22 47 true 2.9  55 true 4.8  36 timeout (true) 900   5900 true 3.8  100 unknown 20   1100 true 34   360 true 18    21   timeout 910 11000 timeout 59   1300 unknown .39  17  
elevator_spec9_product27_true-unreach-call.cil.c timeout 900    1800 timeout 660     310 true 2.3  38 timeout 910   11000 true 180   4800 true 7.5 280 true 6.6 240 unknown .22 46 true 3.4  56 true 6.4  37 timeout (true) 900   6100 true 3.4  110 unknown 20   1100 true 44   400 true 18    21   timeout 910 11000 timeout 64   1300 unknown .39  17  
elevator_spec9_product29_true-unreach-call.cil.c timeout 900    1700 exception (gremlins) 22     130 true 2.4  38 timeout 910   11000 true 250   4700 true 6.5 290 true 6.6 250 unknown .27 46 true 2.6  56 true 5.3  36 timeout (true) 900   7800 true 7.1  170 unknown 21   1100 true 31   360 true 18    22   timeout 900 9800 timeout 60   980 unknown .44  16  
elevator_spec9_product31_true-unreach-call.cil.c timeout 900    1800 exception (gremlins) 43     300 true 2.7  39 timeout 910   11000 true 250   4800 true 7.5 280 true 6.7 250 unknown .20 45 true 3.7  58 true 7.3  37 timeout (true) 900   8300 true 8.5  190 unknown 19   1200 true 37   370 true 18    22   timeout 910 9900 timeout 36   750 unknown .57  17  
email_spec0_product16_false-unreach-call.cil.c false(reach) 180    610 false(reach) 400     280 witness unconfirmed 1.6  48 false(reach) 140   4000 timeout 900   6000 false(reach) 43   1300 false(reach) 53   1600 witness unconfirmed 230    5000 witness unconfirmed 16    200 false(reach) 74    130 timeout 900   4800 false(reach) 19    200 unknown 18   940 false(reach) 23   180 witness unconfirmed 71    18   timeout 900 8800 timeout 43   710 unknown .19  17  
email_spec0_product21_false-unreach-call.cil.c false(reach) 350    1000 timeout 670     300 witness unconfirmed 2.6  56 false(reach) 430   4900 timeout 900   6500 false(reach) 50   1800 false(reach) 58   1600 witness unconfirmed 230    5100 witness unconfirmed 19    210 false(reach) 240    240 timeout 900   5000 witness timeout 31    360 unknown 20   950 false(reach) 21   220 witness unconfirmed 71    21   timeout 910 8800 timeout 42   870 unknown .21  13  
email_spec0_product22_false-unreach-call.cil.c false(reach) 210    670 timeout 650     300 witness unconfirmed 1.7  49 false(reach) 180   4200 timeout 900   5700 false(reach) 49   1800 false(reach) 54   1600 witness unconfirmed 220    5000 witness unconfirmed 15    210 false(reach) 120    170 timeout 900   4800 false(reach) 27    320 unknown 20   950 false(reach) 13   170 false(reach) 36    19   timeout 910 8800 timeout 47   760 unknown .21  13  
email_spec0_product26_false-unreach-call.cil.c false(reach) 420    1100 timeout 660     420 witness unconfirmed 2.8  58 false(reach) 810   7300 timeout 900   7300 false(reach) 54   1800 false(reach) 50   1400 witness unconfirmed 230    5100 witness unconfirmed 18    210 false(reach) 250    270 timeout 900   5100 witness timeout 43    1200 unknown 18   960 false(reach) 25   230 false(reach) 36    22   timeout 910 8600 timeout 46   920 unknown .17  13  
email_spec0_product31_false-unreach-call.cil.c false(reach) 170    640 timeout 660     380 witness unconfirmed 2.1  52 false(reach) 680   5600 timeout 900   6100 false(reach) 50   1800 false(reach) 58   1600 witness unconfirmed 220    5000 witness unconfirmed 18    210 false(reach) 120    220 timeout 900   4900 witness timeout 31    390 unknown 19   990 false(reach) 20   200 false(reach) 53    20   timeout 910 8600 timeout 47   810 unknown .17  11  
email_spec0_product33_false-unreach-call.cil.c false(reach) 190    690 timeout 670     430 witness unconfirmed 2.0  51 timeout 900   6800 timeout 900   6400 false(reach) 61   1400 false(reach) 50   1600 witness unconfirmed 240    5300 witness unconfirmed 14    210 witness unconfirmed 140    180 timeout 900   4900 false(reach) 24    520 unknown 20   1000 false(reach) 19   200 false(reach) 53    23   timeout 900 9000 timeout 40   780 unknown .20  11  
email_spec0_product34_false-unreach-call.cil.c false(reach) 370    1100 timeout 660     440 witness unconfirmed 3.6  69 timeout 900   7300 timeout 900   7000 false(reach) 58   1800 false(reach) 69   1700 witness unconfirmed 230    5300 witness unconfirmed 22    210 false(reach) 290    320 timeout 900   5200 witness timeout 43    620 unknown 19   1000 false(reach) 29   260 false(reach) 54    23   timeout 900 9200 timeout 49   830 unknown .27  12  
email_spec0_product35_false-unreach-call.cil.c false(reach) 400    1200 timeout 670     430 witness unconfirmed 3.9  71 timeout 910   7300 timeout 900   7800 false(reach) 60   2000 false(reach) 82   1800 witness unconfirmed 220    5200 witness unconfirmed 23    210 segmentation fault 370    460 timeout 900   5400 false(reach) 41    160 unknown 20   1000 false(reach) 34   270 false(reach) 54    24   timeout 900 9000 timeout 53   830 unknown .23  16  
email_spec0_productSimulator_false-unreach-call.cil.c killed by signal 9 700    15000 timeout 790     5000 witness timeout 480    1500 exception 7.9 390 timeout 900   8100 false(reach) 140   3800 false(reach) 110   3300 witness unconfirmed 340    5000 witness unconfirmed 360    770 timeout 900    400 timeout 900   7100 witness timeout 140    730 unknown 22   1400 false(reach) 170   330 timeout 900    90   timeout 910 9700 timeout 45   690 unknown 1.4   60  
email_spec11_product15_false-unreach-call.cil.c false(reach) 160    600 timeout 650     290 witness unconfirmed 1.5  48 false(reach) 81   3900 timeout 900   5400 false(reach) 56   1300 false(reach) 46   1600 witness unconfirmed 220    5000 witness unconfirmed 14    200 false(reach) 68    130 timeout 900   4800 false(reach) 20    230 unknown 19   970 false(reach) 12   160 false(reach) 18    17   timeout 900 8500 timeout 41   880 unknown .18  13  
email_spec11_product20_false-unreach-call.cil.c false(reach) 330    950 timeout 670     290 witness unconfirmed 2.2  53 false(reach) 310   4500 timeout 900   6100 false(reach) 44   1800 false(reach) 58   1600 witness unconfirmed 220    5100 witness unconfirmed 16    210 false(reach) 270    280 timeout 900   5200 false(reach) 27    430 unknown 20   960 false(reach) 22   210 false(reach) 18    20   timeout 900 8900 timeout 46   790 unknown .21  15  
email_spec11_product22_false-unreach-call.cil.c false(reach) 220    660 timeout 650     420 witness unconfirmed 1.7  49 false(reach) 150   4100 timeout 900   5600 false(reach) 51   1800 false(reach) 52   1600 witness unconfirmed 220    5200 witness unconfirmed 15    210 false(reach) 160    180 timeout 900   4800 false(reach) 27    280 unknown 20   970 false(reach) 21   190 false(reach) 18    19   timeout 900 8800 timeout 45   800 unknown .20  15  
email_spec11_product26_false-unreach-call.cil.c false(reach) 400    1100 timeout 660     430 witness unconfirmed 2.8  59 false(reach) 780   5800 timeout 900   7000 false(reach) 75   1800 false(reach) 64   1700 witness unconfirmed 220    5000 witness unconfirmed 22    210 false(reach) 240    270 timeout 900   5000 false(reach) 37    1100 unknown 20   960 false(reach) 24   230 false(reach) 19    21   timeout 900 8600 timeout 55   900 unknown .23  15  
email_spec11_product30_false-unreach-call.cil.c false(reach) 190    620 timeout 670     420 witness unconfirmed 1.9  49 false(reach) 470   5000 timeout 900   5700 false(reach) 59   1800 false(reach) 69   1600 witness unconfirmed 220    5000 witness unconfirmed 14    210 segmentation fault 21    76 timeout 900   4800 false(reach) 19    310 unknown 19   960 false(reach) 14   170 false(reach) 18    19   timeout 900 9300 timeout 36   770 unknown .22  13  
email_spec11_product32_false-unreach-call.cil.c false(reach) 350    1000 timeout 670     440 witness unconfirmed 3.0  64 timeout 900   6300 timeout 900   6700 false(reach) 78   1800 false(reach) 64   1700 witness unconfirmed 240    5400 witness unconfirmed 18    210 false(reach) 310    310 timeout 900   5100 false(reach) 31    650 unknown 19   1100 false(reach) 23   230 false(reach) 19    21   timeout 900 8400 timeout 52   890 unknown .23  13  
email_spec11_product33_false-unreach-call.cil.c false(reach) 200    720 timeout 650     360 witness unconfirmed 1.9  51 false(reach) 380   4800 timeout 900   6500 false(reach) 59   1800 false(reach) 66   1700 witness unconfirmed 220    5000 witness unconfirmed 21    210 witness unconfirmed 170    200 timeout 900   5000 false(reach) 30    460 unknown 19   1000 false(reach) 19   200 false(reach) 19    21   timeout 900 9000 timeout 42   830 unknown .25  13  
email_spec11_product35_false-unreach-call.cil.c false(reach) 430    1200 timeout 650     410 witness unconfirmed 3.9  71 timeout 900   6800 timeout 900   7800 false(reach) 68   2000 false(reach) 59   1800 witness unconfirmed 230    5400 witness unconfirmed 23    210 segmentation fault 380    460 timeout 900   5400 false(reach) 46    150 unknown 20   1100 false(reach) 36   270 false(reach) 18    24   timeout 900 9800 timeout 52   940 unknown .25  16  
email_spec11_productSimulator_false-unreach-call.cil.c killed by signal 9 70    15000 timeout 760     4800 witness timeout 690    1700 exception 8.3 380 timeout 900   8300 false(reach) 150   3800 false(reach) 120   3400 witness unconfirmed 340    5200 witness unconfirmed 430    850 timeout 900    400 timeout 900   7400 witness timeout 600    890 unknown 21   1400 false(reach) 100   300 witness timeout 360    76   timeout 900 9200 timeout 48   820 unknown 1.8   59  
email_spec1_product14_false-unreach-call.cil.c witness unconfirmed 130    630 timeout 660     540 witness unconfirmed 1.6  48 false(reach) 100   3700 false(reach) 140   3800 false(reach) 28   960 false(reach) 21   820 witness unconfirmed 230    5300 witness unconfirmed 16    210 witness unconfirmed 120    150 exception 38   920 false(reach) 7.6  210 unknown 20   960 witness unconfirmed 10   160 witness unconfirmed 19    19   timeout 910 9100 timeout 53   790 unknown .32  11  
email_spec1_product15_false-unreach-call.cil.c witness unconfirmed 90    440 timeout 680     400 witness unconfirmed 1.5  48 false(reach) 71   3600 false(reach) 130   3200 false(reach) 31   990 false(reach) 20   810 witness unconfirmed 230    5100 witness unconfirmed 15    210 witness unconfirmed 9.3  41 false(reach) 110   3000 false(reach) 5.6  160 unknown 21   960 witness unconfirmed 8.1 140 false(reach) 650    43   timeout 910 10000 timeout 47   800 unknown .19  11  
email_spec1_product16_false-unreach-call.cil.c witness unconfirmed 75    450 timeout 660     410 witness unconfirmed 1.6  49 false(reach) 110   4000 false(reach) 130   3500 false(reach) 33   1000 false(reach) 20   820 witness unconfirmed 230    5100 witness unconfirmed 17    210 witness unconfirmed 12    48 false(reach) 110   3000 false(reach) 6.3  160 unknown 20   950 witness unconfirmed 7.3 150 witness unconfirmed 250    23   timeout 910 8300 timeout 46   830 unknown .19  11  
email_spec1_product20_false-unreach-call.cil.c witness unconfirmed 170    720 timeout 670     420 witness unconfirmed 2.3  53 false(reach) 120   4100 witness unconfirmed 440   3800 false(reach) 32   1000 false(reach) 21   800 witness unconfirmed 220    5200 witness unconfirmed 17    210 witness unconfirmed 140    160 witness unconfirmed 420   3100 false(reach) 18    340 unknown 21   950 witness unconfirmed 14   200 false(reach) 140    27   timeout 900 7900 timeout 52   1000 unknown .23  13  
email_spec1_product21_false-unreach-call.cil.c witness unconfirmed 170    770 timeout 680     410 witness unconfirmed 2.5  55 false(reach) 130   4100 witness unconfirmed 470   3900 false(reach) 30   970 false(reach) 21   810 witness unconfirmed 230    5100 witness unconfirmed 19    210 witness unconfirmed 130    160 false(reach) 440   3200 false(reach) 9.6  310 unknown 18   930 witness unconfirmed 12   190 witness unconfirmed 160    21   timeout 900 8800 timeout 48   790 unknown .27  13  
email_spec1_product22_false-unreach-call.cil.c witness unconfirmed 98    490 timeout 700     300 witness unconfirmed 1.6  47 false(reach) 100   4000 false(reach) 130   3500 false(reach) 31   1000 false(reach) 22   830 witness unconfirmed 230    5000 witness unconfirmed 17    210 witness unconfirmed 150    170 false(reach) 110   3000 false(reach) 7.1  180 unknown 21   980 witness unconfirmed 9.1 160 false(reach) 310    33   timeout 900 7800 timeout 50   1000 unknown .19  11  
email_spec1_product26_false-unreach-call.cil.c witness unconfirmed 210    840 timeout 670     430 witness unconfirmed 3.0  56 false(reach) 250   4200 witness unconfirmed 490   4000 false(reach) 28   960 false(reach) 21   820 witness unconfirmed 220    5100 witness unconfirmed 23    210 witness unconfirmed 210    210 false(reach) 470   3100 false(reach) 18    910 unknown 19   960 witness unconfirmed 14   210 false(reach) 140    38   timeout 900 8400 timeout 54   870 unknown .28  13  
email_spec1_product29_false-unreach-call.cil.c witness unconfirmed 150    710 timeout 670     540 witness unconfirmed 1.7  50 false(reach) 160   4300 false(reach) 140   3900 false(reach) 30   1000 false(reach) 21   820 witness unconfirmed 220    5200 witness unconfirmed 17    210 witness unconfirmed 320    290 exception 40   970 witness timeout 14    360 unknown 19   960 witness unconfirmed 11   180 false(reach) 190    25   timeout 900 9500 timeout 49   810 unknown .22  15  
email_spec1_product30_false-unreach-call.cil.c witness unconfirmed 90    470 timeout 660     430 witness unconfirmed 1.7  48 false(reach) 460   5300 false(reach) 140   3300 false(reach) 33   1100 false(reach) 23   850 witness unconfirmed 230    5400 witness unconfirmed 16    210 witness unconfirmed 12    50 false(reach) 120   3000 false(reach) 6.4  190 unknown 20   960 witness unconfirmed 9.5 160 false(reach) 650    65   timeout 900 9000 timeout 46   810 unknown .21  15  
email_spec1_product31_false-unreach-call.cil.c witness unconfirmed 81    490 timeout 680     420 witness unconfirmed 1.9  48 timeout 910   6600 false(reach) 140   3500 false(reach) 29   1000 false(reach) 22   850 witness unconfirmed 230    5100 witness unconfirmed 22    210 witness unconfirmed 20    64 false(reach) 120   2900 witness timeout 5.6  200 unknown 19   970 witness unconfirmed 11   180 false(reach) 390    40   timeout 900 9600 timeout 45   780 unknown .22  13  
email_spec1_product32_false-unreach-call.cil.c witness unconfirmed 190    800 timeout 660     570 witness unconfirmed 3.1  60 timeout 900   6400 false(reach) 500   4200 false(reach) 28   980 false(reach) 22   820 witness unconfirmed 230    5300 witness unconfirmed 19    210 witness unconfirmed 220    230 witness unconfirmed 480   3200 witness timeout 14    480 unknown 19   1000 witness unconfirmed 18   210 false(reach) 140    42   timeout 900 8400 timeout 53   1000 unknown .22  16  
email_spec1_product33_false-unreach-call.cil.c witness unconfirmed 110    550 timeout 690     540 witness unconfirmed 2.0  49 false(reach) 180   4100 false(reach) 150   3700 false(reach) 33   1100 false(reach) 23   850 witness unconfirmed 220    5200 witness unconfirmed 23    210 witness unconfirmed 170    190 false(reach) 130   2900 witness timeout 8.8  220 unknown 22   1100 witness unconfirmed 8.6 180 false(reach) 400    43   timeout 900 9500 timeout 44   710 unknown .28  11  
email_spec1_product34_false-unreach-call.cil.c witness unconfirmed 190    880 timeout 660     670 witness unconfirmed 3.6  66 false(reach) 680   6600 false(reach) 540   4900 false(reach) 30   980 false(reach) 22   820 witness unconfirmed 230    5100 witness unconfirmed 24    210 witness unconfirmed 320    340 false(reach) 510   3300 witness timeout 15    480 unknown 19   990 witness unconfirmed 18   240 false(reach) 280    26   timeout 900 9100 timeout 50   880 unknown .29  16  
email_spec1_product35_false-unreach-call.cil.c witness unconfirmed 240    960 timeout 650     670 witness unconfirmed 3.6  68 timeout 900   7300 false(reach) 560   4500 false(reach) 32   1000 false(reach) 22   830 witness unconfirmed 230    5400 witness unconfirmed 27    220 witness unconfirmed 66    110 witness unconfirmed 540   3300 witness timeout 29    1200 unknown 19   1100 witness unconfirmed 22   260 false(reach) 140    32   timeout 900 9300 timeout 51   780 unknown .30  16  
email_spec1_productSimulator_false-unreach-call.cil.c timeout 900    14000 timeout 730     1700 witness timeout 83    520 exception 10   610 timeout 900   7000 false(reach) 48   1700 false(reach) 37   1100 witness unconfirmed 250    5100 witness unconfirmed 230    390 timeout 900    510 timeout 900   5500 witness timeout 120    470 unknown 22   1400 witness timeout 27   270 timeout 900    110   timeout 900 8700 timeout 50   720 unknown 1.7   55  
email_spec27_product17_false-unreach-call.cil.c false(reach) 150    660 witness unconfirmed 61     120 witness unconfirmed 1.7  48 false(reach) 100   3800 false(reach) 280   3700 false(reach) 24   910 false(reach) 15   630 witness unconfirmed 220    5100 witness unconfirmed 16    210 witness unconfirmed 190    210 exception 44   1000 witness timeout 7.7  240 unknown 19   960 false(reach) 10   170 timeout 900    46   timeout 900 9400 timeout 57   870 unknown .21  11  
email_spec27_product18_false-unreach-call.cil.c witness unconfirmed 81    440 witness unconfirmed 7.8   87 witness unconfirmed 1.5  48 false(reach) 120   4100 false(reach) 210   3200 false(reach) 33   1000 false(reach) 23   820 witness unconfirmed 230    5300 witness unconfirmed 16    210 witness unconfirmed 14    52 false(reach) 180   2900 witness timeout 5.4  210 unknown 18   950 false(reach) 9.0 150 timeout 900    58   timeout 900 8200 timeout 41   970 unknown .19  15  
email_spec27_product19_false-unreach-call.cil.c witness unconfirmed 85    460 witness timeout 67     120 witness unconfirmed 1.7  50 timeout 900   4900 false(reach) 210   3600 false(reach) 29   990 false(reach) 22   810 witness unconfirmed 230    5200 witness unconfirmed 17    210 witness unconfirmed 16    55 exception 43   990 witness timeout 6.2  220 unknown 19   950 false(reach) 11   170 false(reach) 420    31   timeout 900 8900 timeout 58   1100 unknown .21  13  
email_spec27_product23_false-unreach-call.cil.c false(reach) 180    730 witness timeout 9.4   84 witness unconfirmed 2.5  54 timeout 910   8900 witness unconfirmed 630   4200 false(reach) 22   900 false(reach) 18   650 witness unconfirmed 220    5000 witness unconfirmed 18    210 witness unconfirmed 240    260 witness unconfirmed 600   3100 witness timeout 13    450 unknown 20   950 false(reach) 12   180 timeout 900    59   timeout 900 8700 timeout 60   1500 unknown .20  13  
email_spec27_product24_false-unreach-call.cil.c witness unconfirmed 99    500 witness timeout 8.6   88 witness unconfirmed 1.8  50 false(reach) 360   5000 false(reach) 210   3600 false(reach) 28   1000 false(reach) 19   820 witness unconfirmed 220    5100 witness unconfirmed 20    210 witness unconfirmed 230    270 false(reach) 190   2900 witness timeout 8.7  290 unknown 21   970 false(reach) 11   160 false(reach) 400    48   timeout 900 9600 timeout 57   970 unknown .29  15  
email_spec27_product25_false-unreach-call.cil.c witness unconfirmed 180    780 witness timeout 66     130 witness unconfirmed 2.6  58 timeout 900   9300 witness unconfirmed 650   4200 false(reach) 23   880 false(reach) 18   660 witness unconfirmed 230    5000 witness unconfirmed 24    210 witness unconfirmed 270    270 false(reach) 620   3200 witness timeout 12    380 unknown 19   960 false(reach) 16   200 false(reach) 460    42   timeout 900 8500 timeout 62   1000 unknown .29  13  
email_spec27_product27_false-unreach-call.cil.c witness unconfirmed 220    850 witness timeout 9.9   85 witness unconfirmed 3.1  61 false(reach) 500   5200 false(reach) 660   4300 false(reach) 23   890 false(reach) 15   660 witness unconfirmed 220    5200 witness unconfirmed 23    210 witness unconfirmed 75    120 witness unconfirmed 650   3300 witness timeout 24    970 unknown 19   960 false(reach) 15   220 false(reach) 420    55   timeout 900 8900 timeout 74   1100 unknown .35  13  
email_spec27_product29_false-unreach-call.cil.c witness unconfirmed 140    730 witness unconfirmed 150     300 witness unconfirmed 1.9  52 false(reach) 110   3900 false(reach) 310   4300 false(reach) 24   910 false(reach) 18   710 witness unconfirmed 230    5300 witness unconfirmed 18    210 witness unconfirmed 240    270 false(reach) 280   3100 witness timeout 14    400 unknown 21   1100 false(reach) 14   190 timeout 900    55   timeout 900 8000 timeout 43   760 unknown .22  12  
email_spec27_product30_false-unreach-call.cil.c witness unconfirmed 83    470 witness timeout 390     290 witness unconfirmed 1.8  51 false(reach) 360   4000 false(reach) 230   3500 false(reach) 36   1100 false(reach) 23   840 witness unconfirmed 230    5300 witness unconfirmed 16    210 witness unconfirmed 20    73 false(reach) 200   2900 witness timeout 7.0  320 unknown 19   960 false(reach) 14   180 timeout 900    60   timeout 910 9600 timeout 43   680 unknown .18  15  
email_spec27_product31_false-unreach-call.cil.c witness unconfirmed 96    500 witness timeout 580     450 witness unconfirmed 2.0  51 false(reach) 190   4100 false(reach) 230   3700 false(reach) 32   1100 false(reach) 22   840 witness unconfirmed 230    5100 witness unconfirmed 22    210 witness unconfirmed 29    83 false(reach) 210   2900 witness timeout 10    400 unknown 18   950 false(reach) 12   180 false(reach) 530    49   timeout 910 9400 timeout 41   760 unknown .19  11  
email_spec27_product32_false-unreach-call.cil.c witness unconfirmed 200    820 witness timeout 400     290 witness unconfirmed 3.5  66 false(reach) 560   5300 false(reach) 730   4700 false(reach) 27   950 false(reach) 18   710 witness unconfirmed 230    5100 witness unconfirmed 23    210 witness unconfirmed 240    230 false(reach) 710   3300 witness timeout 20    710 unknown 20   1000 false(reach) 16   220 timeout 900    85   timeout 900 9800 timeout 40   750 unknown .28  11  
email_spec27_product33_false-unreach-call.cil.c witness unconfirmed 91    540 witness timeout 280     220 witness unconfirmed 2.2  52 false(reach) 450   4100 false(reach) 230   3800 false(reach) 30   1100 false(reach) 24   850 witness unconfirmed 220    5100 witness unconfirmed 23    210 witness unconfirmed 140    190 exception 44   970 witness timeout 11    480 unknown 19   1000 false(reach) 12   170 false(reach) 440    62   timeout 910 10000 timeout 40   610 unknown .18  11  
email_spec27_product34_false-unreach-call.cil.c witness unconfirmed 210    900 witness timeout 630     450 witness unconfirmed 4.1  70 false(reach) 310   4300 false(reach) 760   4500 false(reach) 25   940 false(reach) 17   710 witness unconfirmed 230    5300 witness unconfirmed 22    210 witness unconfirmed 200    230 false(reach) 740   3300 witness timeout 24    730 unknown 20   1100 false(reach) 13   200 false(reach) 550    48   timeout 900 8700 timeout 46   1100 unknown .26  16  
email_spec27_product35_false-unreach-call.cil.c witness unconfirmed 250    980 witness timeout 280     230 witness unconfirmed 4.3  72 false(reach) 750   5500 witness unconfirmed 790   5600 false(reach) 24   950 false(reach) 20   720 witness unconfirmed 230    5000 witness unconfirmed 26    210 witness unconfirmed 86    140 witness unconfirmed 750   3300 witness timeout 30    170 unknown 21   1100 false(reach) 21   250 false(reach) 440    44   timeout 900 9700 timeout 53   1100 unknown .30  16  
email_spec27_productSimulator_false-unreach-call.cil.c killed by signal 9 65    15000 witness timeout 61     420 witness timeout 240    780 timeout 900   3600 timeout 900   7700 false(reach) 31   1000 false(reach) 24   820 witness unconfirmed 290    5300 witness unconfirmed 680    510 timeout 900    480 timeout 900   6900 witness timeout 890    1100 unknown 21   1400 false(reach) 55   270 timeout 900    93   timeout 910 10000 timeout 47   750 unknown 1.7   53  
email_spec3_product13_false-unreach-call.cil.c false(reach) 1.1  130 false(reach) 78     140 witness unconfirmed .59 41 false(reach) 24   910 false(reach) 21   600 false(reach) 12   490 false(reach) 10   350 witness unconfirmed 220    5000 witness unconfirmed 13    210 false(reach) .43 37 false(reach) 14   490 false(reach) 1.5  120 unknown 20   970 false(reach) 5.7 120 false(reach) 36    17   false(reach) 520 7400 false(reach) 29   580 unknown .17  17  
email_spec3_product17_false-unreach-call.cil.c false(reach) 1.8  250 false(reach) 79     150 witness unconfirmed .73 45 false(reach) 25   880 false(reach) 20   600 false(reach) 12   500 false(reach) 10   350 witness unconfirmed 220    5000 witness unconfirmed 13    200 false(reach) .54 38 false(reach) 15   530 false(reach) 1.6  140 unknown 18   960 false(reach) 5.9 130 false(reach) 36    20   false(reach) 520 7700 timeout 66   1300 unknown .19  13  
email_spec3_product18_false-unreach-call.cil.c false(reach) 1.2  150 false(reach) 5.5   91 witness unconfirmed .52 43 false(reach) 26   920 false(reach) 17   550 false(reach) 11   490 false(reach) 9.0 350 witness unconfirmed 220    5100 witness unconfirmed 14    210 false(reach) .58 37 false(reach) 16   510 false(reach) 1.5  130 unknown 19   950 false(reach) 6.0 130 false(reach) 18    18   false(reach) 500 7700 false(reach) 27   560 unknown .20  11  
email_spec3_product19_false-unreach-call.cil.c false(reach) 1.1  160 false(reach) 71     140 witness unconfirmed .76 43 false(reach) 23   870 false(reach) 21   580 false(reach) 10   490 false(reach) 9.4 350 witness unconfirmed 220    5000 witness unconfirmed 16    210 false(reach) .56 37 false(reach) 14   500 false(reach) 1.5  130 unknown 19   950 false(reach) 5.1 140 false(reach) 36    19   false(reach) 630 7900 false(reach) 25   480 unknown .23  15  
email_spec3_product23_false-unreach-call.cil.c false(reach) 2.0  290 false(reach) 7.6   89 witness unconfirmed 1.3  51 false(reach) 27   930 false(reach) 21   630 false(reach) 12   510 false(reach) 10   350 witness unconfirmed 220    5000 witness unconfirmed 14    210 false(reach) .59 37 false(reach) 16   530 false(reach) 2.5  210 unknown 20   960 false(reach) 6.2 140 false(reach) 19    21   false(reach) 580 8300 timeout 61   1000 unknown .21  13  
email_spec3_product24_false-unreach-call.cil.c false(reach) 1.4  180 false(reach) 5.6   89 witness unconfirmed .78 45 false(reach) 25   860 false(reach) 19   570 false(reach) 10   480 false(reach) 9.9 330 witness unconfirmed 230    5000 witness unconfirmed 17    210 false(reach) .59 37 false(reach) 14   490 false(reach) 1.5  120 unknown 20   980 false(reach) 6.2 130 false(reach) 19    20   false(reach) 500 7900 false(reach) 23   470 unknown .25  13  
email_spec3_product25_false-unreach-call.cil.c false(reach) 2.1  340 false(reach) 82     150 witness unconfirmed 1.4  53 false(reach) 26   920 false(reach) 20   610 false(reach) 12   490 false(reach) 11   350 witness unconfirmed 220    5000 witness unconfirmed 18    210 false(reach) .55 37 false(reach) 16   530 false(reach) 2.3  210 unknown 21   960 false(reach) 6.1 160 false(reach) 37    22   false(reach) 540 7300 timeout 68   1600 unknown .21  15  
email_spec3_product27_false-unreach-call.cil.c false(reach) 2.4  380 false(reach) 7.6   89 witness unconfirmed 1.5  53 false(reach) 26   940 false(reach) 18   590 false(reach) 10   490 false(reach) 10   360 witness unconfirmed 220    5000 witness unconfirmed 20    210 false(reach) .55 37 false(reach) 15   540 false(reach) 2.4  210 unknown 19   940 false(reach) 5.4 170 false(reach) 18    23   false(reach) 530 7600 timeout 60   1500 unknown .23  13  
email_spec3_product28_false-unreach-call.cil.c false(reach) 1.3  160 false(reach) 120     150 witness unconfirmed .58 43 false(reach) 38   1500 false(reach) 20   620 false(reach) 10   510 false(reach) 11   370 witness unconfirmed 220    5000 witness unconfirmed 13    210 false(reach) .63 37 false(reach) 15   520 false(reach) 1.5  130 unknown 20   950 false(reach) 5.7 130 false(reach) 35    19   timeout 910 9600 timeout 45   1100 unknown .22  13  
email_spec3_product29_false-unreach-call.cil.c false(reach) 2.2  330 false(reach) 130     150 witness unconfirmed .86 46 false(reach) 40   1500 false(reach) 23   650 false(reach) 12   500 false(reach) 10   370 witness unconfirmed 230    5100 witness unconfirmed 13    210 false(reach) .62 38 false(reach) 17   550 false(reach) 1.9  140 unknown 20   1000 false(reach) 6.4 150 false(reach) 36    21   timeout 910 9200 timeout 48   1000 unknown .22  14  
email_spec3_product30_false-unreach-call.cil.c false(reach) 1.4  180 false(reach) 7.2   83 witness unconfirmed .79 46 false(reach) 39   1500 false(reach) 22   650 false(reach) 12   520 false(reach) 11   370 witness unconfirmed 230    5000 witness unconfirmed 13    210 false(reach) .62 38 false(reach) 14   510 false(reach) 1.7  140 unknown 20   1000 false(reach) 6.5 130 false(reach) 18    19   timeout 910 9200 timeout 38   800 unknown .20  13  
email_spec3_product31_false-unreach-call.cil.c false(reach) 1.5  210 false(reach) 130     150 witness unconfirmed .88 47 false(reach) 42   1500 false(reach) 21   660 false(reach) 13   510 false(reach) 10   360 witness unconfirmed 240    5300 witness unconfirmed 16    210 false(reach) .61 37 false(reach) 15   520 false(reach) 1.5  130 unknown 19   1000 false(reach) 6.1 150 false(reach) 36    21   timeout 900 9700 timeout 41   700 unknown .21  11  
email_spec3_product32_false-unreach-call.cil.c false(reach) 2.5  380 false(reach) 7.9   86 witness unconfirmed 1.7  58 false(reach) 39   1300 false(reach) 20   610 false(reach) 12   520 false(reach) 9.2 370 witness unconfirmed 220    5000 witness unconfirmed 15    210 false(reach) .62 38 false(reach) 16   550 false(reach) 2.3  210 unknown 19   1000 false(reach) 6.5 160 false(reach) 19    22   timeout 900 9600 timeout 49   890 unknown .27  14  
email_spec3_product33_false-unreach-call.cil.c false(reach) 1.7  220 false(reach) 7.8   85 witness unconfirmed .70 46 false(reach) 38   1500 false(reach) 20   580 false(reach) 12   510 false(reach) 11   370 witness unconfirmed 220    5000 witness unconfirmed 19    210 false(reach) .61 37 false(reach) 15   510 false(reach) 1.6  130 unknown 20   1000 false(reach) 6.2 150 false(reach) 19    22   timeout 900 9100 timeout 44   770 unknown .26  13  
email_spec3_product34_false-unreach-call.cil.c false(reach) 2.8  460 false(reach) 140     150 witness unconfirmed 2.0  64 false(reach) 39   1600 false(reach) 21   680 false(reach) 12   510 false(reach) 9.0 370 witness unconfirmed 230    5000 witness unconfirmed 20    210 false(reach) .61 38 false(reach) 16   550 false(reach) 2.7  210 unknown 20   1000 false(reach) 6.8 170 false(reach) 36    24   timeout 900 10000 timeout 47   840 unknown .28  18  
email_spec3_product35_false-unreach-call.cil.c false(reach) 3.1  510 false(reach) 7.9   86 witness unconfirmed 1.7  66 false(reach) 39   1400 false(reach) 21   630 false(reach) 12   520 false(reach) 9.7 340 witness unconfirmed 290    6800 witness unconfirmed 20    210 false(reach) .61 38 false(reach) 17   560 false(reach) 2.2  130 unknown 20   1100 false(reach) 6.5 160 false(reach) 19    25   timeout 910 10000 timeout 50   1000 unknown .34  16  
email_spec3_productSimulator_false-unreach-call.cil.c false(reach) 86    14000 false(reach) 22     170 witness unconfirmed 47    570 exception 9.1 350 witness unconfirmed 58   1500 false(reach) 13   540 false(reach) 9.5 390 witness unconfirmed 250    5200 witness unconfirmed 48    420 witness timeout .82 39 witness unconfirmed 41   1200 false(reach) 4.0  290 unknown 65   1400 false(reach) 8.0 190 false(reach) 72    49   timeout 910 10000 timeout 57   1100 unknown 1.5   59  
email_spec4_product18_false-unreach-call.cil.c witness unconfirmed 89    440 timeout 660     570 witness unconfirmed 1.6  47 false(reach) 45   2100 false(reach) 180   3300 false(reach) 31   990 false(reach) 21   830 witness unconfirmed 220    5200 witness unconfirmed 15    210 witness unconfirmed 8.8  41 false(reach) 160   3000 false(reach) 5.5  140 unknown 20   970 false(reach) 6.7 130 false(reach) 19    18   timeout 900 8100 timeout 49   950 unknown .20  17  
email_spec4_product19_false-unreach-call.cil.c witness unconfirmed 80    450 timeout 680     440 witness unconfirmed 1.6  48 false(reach) 51   1600 false(reach) 190   3500 false(reach) 30   1000 false(reach) 20   810 witness unconfirmed 220    5300 witness unconfirmed 19    210 witness unconfirmed 14    51 false(reach) 160   2900 false(reach) 6.3  140 unknown 19   970 false(reach) 6.8 150 witness unconfirmed 89    19   timeout 910 9800 timeout 47   980 unknown .25  13  
email_spec4_product23_false-unreach-call.cil.c witness unconfirmed 170    720 timeout 660     380 witness unconfirmed 2.3  54 false(reach) 79   3900 false(reach) 540   4000 false(reach) 33   1100 false(reach) 23   850 witness unconfirmed 230    5300 witness unconfirmed 18    210 witness unconfirmed 220    230 false(reach) 510   3100 false(reach) 8.9  280 unknown 19   960 false(reach) 11   190 false(reach) 19    20   timeout 900 8000 timeout 52   1000 unknown .18  17  
email_spec4_product24_false-unreach-call.cil.c witness unconfirmed 92    490 timeout 670     430 witness unconfirmed 1.7  49 false(reach) 59   3800 false(reach) 190   3500 false(reach) 30   970 false(reach) 20   830 witness unconfirmed 230    5100 witness unconfirmed 20    210 witness unconfirmed 210    230 false(reach) 160   3000 false(reach) 6.6  150 unknown 19   940 false(reach) 7.0 150 false(reach) 18    19   timeout 900 8300 timeout 44   1000 unknown .17  11  
email_spec4_product25_false-unreach-call.cil.c witness unconfirmed 190    770 timeout 660     440 witness unconfirmed 2.6  54 false(reach) 62   3000 false(reach) 560   3900 false(reach) 30   1000 false(reach) 20   840 witness unconfirmed 220    5100 witness unconfirmed 22    210 witness unconfirmed 210    230 false(reach) 530   3200 false(reach) 9.9  250 unknown 19   980 false(reach) 9.8 190 witness unconfirmed 88    21   timeout 910 8700 timeout 58   910 unknown .28  17  
email_spec4_product27_false-unreach-call.cil.c witness unconfirmed 200    830 timeout 680     830 witness unconfirmed 2.9  57 false(reach) 110   4100 false(reach) 570   4000 false(reach) 32   1000 false(reach) 22   840 witness unconfirmed 230    5000 witness unconfirmed 22    210 witness unconfirmed 120    170 exception 46   1000 false(reach) 18    620 unknown 19   930 false(reach) 11   190 false(reach) 19    22   timeout 910 6600 timeout 54   870 unknown .23  13  
email_spec4_product30_false-unreach-call.cil.c witness unconfirmed 85    470 timeout 710     290 witness unconfirmed 1.7  49 false(reach) 87   4000 false(reach) 190   3300 false(reach) 35   1100 false(reach) 22   840 witness unconfirmed 230    5200 witness unconfirmed 16    200 witness unconfirmed 12    50 false(reach) 170   3000 false(reach) 7.0  190 unknown 20   990 false(reach) 6.7 150 false(reach) 19    19   timeout 910 8200 timeout 46   910 unknown .18  13  
email_spec4_product31_false-unreach-call.cil.c witness unconfirmed 87    490 timeout 670     420 witness unconfirmed 1.8  50 false(reach) 110   4100 false(reach) 200   3500 false(reach) 32   1100 false(reach) 20   820 witness unconfirmed 230    5100 witness unconfirmed 22    210 witness unconfirmed 25    73 false(reach) 170   2900 witness timeout 7.8  200 unknown 20   950 false(reach) 7.9 150 false(reach) 110    31   timeout 900 8100 timeout 41   940 unknown .22  15  
email_spec4_product32_false-unreach-call.cil.c witness unconfirmed 160    790 timeout 670     370 witness unconfirmed 3.2  62 timeout 900   5700 false(reach) 610   4500 false(reach) 34   1100 false(reach) 25   890 witness unconfirmed 270    6600 witness unconfirmed 21    210 witness unconfirmed 250    230 false(reach) 580   3200 false(reach) 14    480 unknown 21   1000 false(reach) 11   180 false(reach) 19    22   timeout 900 8300 timeout 54   860 unknown .28  14  
email_spec4_product33_false-unreach-call.cil.c witness unconfirmed 100    550 timeout 650     420 witness unconfirmed 1.9  49 false(reach) 93   4400 false(reach) 200   3700 false(reach) 32   1100 false(reach) 22   860 witness unconfirmed 220    5000 witness unconfirmed 23    210 witness unconfirmed 170    190 false(reach) 180   2900 false(reach) 7.4  220 unknown 21   1000 false(reach) 8.6 160 false(reach) 19    21   timeout 900 8300 timeout 42   700 unknown .23  17  
email_spec4_product34_false-unreach-call.cil.c witness unconfirmed 200    880 timeout 660     420 witness unconfirmed 3.6  66 false(reach) 770   6500 false(reach) 650   4500 false(reach) 33   1100 false(reach) 24   850 witness unconfirmed 230    5000 witness unconfirmed 23    210 witness unconfirmed 220    220 exception 54   1200 witness timeout 15    470 unknown 20   1000 false(reach) 15   210 false(reach) 110    23   timeout 900 8700 timeout 51   950 unknown .26  14  
email_spec4_product35_false-unreach-call.cil.c witness unconfirmed 230    950 timeout 670     290 witness unconfirmed 3.8  68 false(reach) 590   6900 false(reach) 660   4400 false(reach) 32   1100 false(reach) 22   860 witness unconfirmed 230    5200 witness unconfirmed 23    210 witness unconfirmed 170    230 false(reach) 640   3400 witness timeout 30    1200 unknown 20   1100 false(reach) 13   210 false(reach) 18    24   timeout 900 8500 timeout 65   1200 unknown .30  12  
email_spec4_productSimulator_false-unreach-call.cil.c timeout 900    14000 timeout 710     1600 witness timeout 81    520 exception 11   650 timeout 900   7000 false(reach) 52   1800 false(reach) 51   1600 witness unconfirmed 260    5300 witness unconfirmed 230    370 timeout 900    480 timeout 900   5200 witness timeout 99    460 unknown 22   1400 false(reach) 32   260 false(reach) 730    88   timeout 910 9400 timeout 58   940 unknown 1.7   58  
email_spec6_product12_false-unreach-call.cil.c false(reach) 65    400 timeout 660     650 witness unconfirmed 1.3  47 false(reach) 48   2600 false(reach) 120   3200 false(reach) 29   980 false(reach) 20   790 witness unconfirmed 220    5000 witness unconfirmed 15    210 false(reach) 8.8  39 false(reach) 100   2800 false(reach) 4.7  130 unknown 18   930 false(reach) 8.4 140 witness unconfirmed 19    16   timeout 900 9600 timeout 48   870 unknown .15  15  
email_spec6_product14_false-unreach-call.cil.c false(reach) 150    660 timeout 660     760 witness unconfirmed 1.7  48 false(reach) 71   3800 false(reach) 270   3800 false(reach) 27   970 false(reach) 21   820 witness unconfirmed 220    5000 witness unconfirmed 16    210 witness unconfirmed 120    150 false(reach) 250   3100 false(reach) 8.4  230 unknown 19   970 false(reach) 14   180 witness unconfirmed 18    19   timeout 910 9300 timeout 47   990 unknown .20  13  
email_spec6_product15_false-unreach-call.cil.c false(reach) 78    440 timeout 660     410 witness unconfirmed 1.6  49 false(reach) 61   3700 false(reach) 200   3400 false(reach) 31   1000 false(reach) 18   790 witness unconfirmed 220    5000 witness unconfirmed 16    210 false(reach) 8.8  39 false(reach) 170   2900 false(reach) 6.5  190 unknown 19   950 false(reach) 11   160 false(reach) 18    17   timeout 910 7600 timeout 50   980 unknown .20  13  
email_spec6_product16_false-unreach-call.cil.c false(reach) 80    450 timeout 650     590 witness unconfirmed 1.7  49 false(reach) 66   3300 false(reach) 200   3400 false(reach) 31   1000 false(reach) 19   810 witness unconfirmed 230    5300 witness unconfirmed 17    210 false(reach) 9.2  40 false(reach) 180   3000 witness timeout 9.6  200 unknown 20   940 false(reach) 12   170 witness unconfirmed 19    18   timeout 910 9600 timeout 43   780 unknown .24  13  
email_spec6_product20_false-unreach-call.cil.c false(reach) 170    730 timeout 660     350 witness unconfirmed 2.7  55 false(reach) 160   4200 false(reach) 600   4000 false(reach) 31   1000 false(reach) 21   800 witness unconfirmed 290    6900 witness unconfirmed 19    210 witness unconfirmed 140    170 false(reach) 590   3100 witness timeout 16    440 unknown 20   950 false(reach) 13   210 false(reach) 18    20   timeout 910 9000 timeout 44   670 unknown .19  13  
email_spec6_product21_false-unreach-call.cil.c false(reach) 170    790 timeout 660     750 witness unconfirmed 2.6  59 false(reach) 87   3900 false(reach) 630   4100 false(reach) 27   970 false(reach) 21   830 witness unconfirmed 230    5100 witness unconfirmed 24    210 witness unconfirmed 140    170 false(reach) 610   3200 false(reach) 17    380 unknown 20   950 false(reach) 19   210 witness unconfirmed 18    21   timeout 910 9100 timeout 44   830 unknown .20  15  
email_spec6_product22_false-unreach-call.cil.c false(reach) 93    490 timeout 650     500 witness unconfirmed 1.7  47 false(reach) 79   3900 false(reach) 200   3600 false(reach) 29   970 false(reach) 21   820 witness unconfirmed 220    5000 witness unconfirmed 21    210 false(reach) 140    170 false(reach) 180   3000 false(reach) 11    240 unknown 19   950 false(reach) 11   170 false(reach) 18    19   timeout 900 8700 timeout 47   880 unknown .13  17  
email_spec6_product26_false-unreach-call.cil.c false(reach) 210    870 false(reach) 650     440 witness unconfirmed 3.0  63 false(reach) 99   4000 false(reach) 650   4500 false(reach) 28   970 false(reach) 20   820 witness unconfirmed 230    5300 witness unconfirmed 26    210 witness unconfirmed 210    240 false(reach) 620   3200 witness timeout 19    1100 unknown 20   980 false(reach) 15   220 false(reach) 18    22   timeout 910 9300 timeout 48   960 unknown .27  13  
email_spec6_product28_false-unreach-call.cil.c false(reach) 90    440 timeout 660     290 witness unconfirmed 1.4  48 false(reach) 77   2700 false(reach) 120   3400 false(reach) 28   970 false(reach) 20   810 witness unconfirmed 220    5100 witness unconfirmed 16    210 false(reach) 12    45 false(reach) 100   2900 false(reach) 5.7  170 unknown 18   970 false(reach) 11   160 false(reach) 19    18   timeout 900 9400 timeout 47   830 unknown .24  11  
email_spec6_product29_false-unreach-call.cil.c false(reach) 160    740 timeout 660     350 witness unconfirmed 2.0  53 timeout 900   5000 false(reach) 280   3900 false(reach) 29   990 false(reach) 20   820 witness unconfirmed 220    5100 witness unconfirmed 17    210 false(reach) 220    220 false(reach) 250   3100 false(reach) 11    390 unknown 19   970 false(reach) 12   190 false(reach) 18    21   timeout 910 8800 timeout 45   770 unknown .19  13  
email_spec6_product30_false-unreach-call.cil.c false(reach) 80    470 false(reach) 580     260 witness unconfirmed 1.8  48 false(reach) 89   3800 false(reach) 200   3500 false(reach) 27   960 false(reach) 19   810 witness unconfirmed 220    5100 witness unconfirmed 16    210 false(reach) 11    48 false(reach) 180   2900 witness timeout 13    230 unknown 20   950 false(reach) 11   170 false(reach) 19    19   timeout 910 8600 timeout 47   840 unknown .24  11  
email_spec6_product31_false-unreach-call.cil.c false(reach) 91    500 timeout 660     310 witness unconfirmed 1.9  49 false(reach) 130   4000 false(reach) 210   3700 false(reach) 30   990 false(reach) 21   830 witness unconfirmed 230    5100 witness unconfirmed 17    210 false(reach) 15    51 false(reach) 190   3000 witness timeout 12    240 unknown 21   1000 false(reach) 11   180 false(reach) 18    20   timeout 900 8600 timeout 49   920 unknown .20  11  
email_spec6_product32_false-unreach-call.cil.c false(reach) 190    820 false(reach) 620     310 witness unconfirmed 3.0  65 false(reach) 410   5200 false(reach) 670   4500 false(reach) 30   970 false(reach) 22   830 witness unconfirmed 230    5300 witness unconfirmed 23    210 witness unconfirmed 260    280 false(reach) 650   3200 witness timeout 17    560 unknown 20   1100 false(reach) 20   230 false(reach) 19    22   timeout 910 8900 timeout 51   840 unknown .23  14  
email_spec6_product33_false-unreach-call.cil.c false(reach) 110    560 timeout 650     400 witness unconfirmed 2.0  49 false(reach) 180   4200 false(reach) 220   3700 false(reach) 33   970 false(reach) 23   840 witness unconfirmed 230    5300 witness unconfirmed 24    210 false(reach) 160    180 false(reach) 190   3000 false(reach) 9.7  260 unknown 20   1100 false(reach) 13   190 false(reach) 18    21   timeout 900 8800 timeout 50   840 unknown .28  15  
email_spec6_product34_false-unreach-call.cil.c false(reach) 210    910 timeout 660     440 witness unconfirmed 3.7  70 false(reach) 130   4000 false(reach) 700   5100 false(reach) 30   990 false(reach) 22   830 witness unconfirmed 230    5000 witness unconfirmed 29    210 false(reach) 340    350