Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741 VeriAbs
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-11-30 11:20:26 CET 2017-11-30 16:01:31 CET 2017-12-01 08:49:27 CET 2017-12-01 12:59:33 CET 2017-12-01 19:00:34 CET 2017-12-01 22:41:19 CET 2017-12-02 01:06:24 CET 2017-12-02 02:33:02 CET 2017-12-02 17:23:13 CET 2017-12-02 18:04:04 CET
Run set 2ls.sv-comp18.ReachSafety-ProductLines cbmc.sv-comp18.ReachSafety-ProductLines cpa-bam-bnb.sv-comp18.ReachSafety-ProductLines cpa-bam-slicing.sv-comp18.ReachSafety-ProductLines cpa-seq.sv-comp18.ReachSafety-ProductLines depthk.sv-comp18.ReachSafety-ProductLines esbmc-incr.sv-comp18.ReachSafety-ProductLines esbmc-kind.sv-comp18.ReachSafety-ProductLines interpchecker.sv-comp18.ReachSafety-ProductLines symbiotic.sv-comp18.ReachSafety-ProductLines uautomizer.sv-comp18.ReachSafety-ProductLines ukojak.sv-comp18.ReachSafety-ProductLines utaipan.sv-comp18.ReachSafety-ProductLines veriabs.sv-comp18.ReachSafety-ProductLines
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/product-lines/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
elevator_spec14_product20_false-unreach-call_true-termination.cil.c 6.0  1200 56    1 .45 42 4.5 1 92   4600 710 1 480   9700 3000 1 7.4 310 53 1 480    380 4200   1 .20 38 1.9 1 .17  39 2.0  1 910   4200 11000 0 .38 18 4.6 1 900   13000 8000 0 900   3300 11000 0 900   4700 12000 0 380 1200 2800 0
elevator_spec14_product24_false-unreach-call_true-termination.cil.c 9.9  2000 81    1 .51 42 4.9 1 130   5700 910 1 910   11000 5200 0 7.2 310 66 1 480    520 4200   1 .17 39 1.6 1 .20  39 2.2  1 900   4000 11000 0 .38 19 3.8 1 910   13000 7300 0 900   2800 11000 0 900   4600 9600 0 400 1400 3800 0
elevator_spec14_product28_false-unreach-call_true-termination.cil.c 6.2  1300 60    1 .47 42 4.3 1 93   4800 670 1 900   11000 4600 0 7.3 320 66 1 480    420 5600   1 .19 39 1.7 1 .19  39 1.9  1 920   4400 12000 0 .38 19 4.6 1 900   13000 6100 0 900   2800 15000 0 900   4600 12000 0 400 1200 2800 0
elevator_spec14_product32_false-unreach-call_true-termination.cil.c 11    2100 100    1 .47 42 4.6 1 140   6000 980 1 900   11000 4700 0 7.1 310 57 1 6.3  540 64   1 .16 39 1.9 1 .18  39 1.9  1 900   4000 13000 0 .39 19 4.9 1 910   12000 7800 0 900   2800 12000 0 900   4700 11000 0 400 1400 3500 0
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c 36    7000 320    1 11    450 110   1 910   11000 5000 0 910   11000 5000 0 8.4 360 75 1 530    1400 5600   1 4.7  160 49   1 6.1   200 63    1 900   4200 13000 0 .41 23 6.1 1 910   13000 6500 0 900   2500 15000 0 900   4700 11000 0 900 5900 6900 0
elevator_spec1_product18_false-unreach-call_true-termination.cil.c 41    850 490    1 1.2  42 13   1 910   11000 5600 0 900   11000 4700 0 7.5 330 58 1 490    180 6300   1 .23 39 2.4 1 1.4   61 16    1 970   9200 10000 0 .37 18 4.8 1 900   13000 8800 0 900   3300 13000 0 900   5400 11000 0 210 750 2000 0
elevator_spec1_product20_false-unreach-call_true-termination.cil.c 43    900 360    1 1.2  42 13   1 910   11000 5200 0 900   11000 4600 0 7.7 330 64 1 490    200 6900   1 .22 39 2.4 1 1.5   63 18    1 950   8800 8100 0 .38 19 4.6 1 900   14000 6900 0 900   3200 13000 0 900   4600 10000 0 210 770 2000 0
elevator_spec1_product22_false-unreach-call_true-termination.cil.c 43    1200 450    1 1.2  42 12   1 900   11000 5200 0 910   11000 5700 0 7.4 330 68 1 500    240 6800   1 .22 39 2.1 1 1.9   76 21    1 970   8200 9200 0 .37 19 4.4 1 900   13000 7400 0 900   3100 12000 0 900   4700 11000 0 210 760 2200 0
elevator_spec1_product24_false-unreach-call_true-termination.cil.c 49    1300 380    1 1.3  43 16   1 910   11000 5700 0 900   11000 4300 0 7.6 340 58 1 500    330 5800   1 .23 39 2.2 1 2.0   79 27    1 970   9400 9800 0 .37 19 5.1 1 900   13000 6600 0 900   3100 11000 0 900   4600 10000 0 210 760 2300 0
elevator_spec1_product26_false-unreach-call_true-termination.cil.c 43    890 370    1 1.2  42 14   1 900   11000 5600 0 900   11000 4800 0 7.3 320 58 1 490    210 6000   1 .20 39 2.2 1 1.6   65 18    1 920   8400 10000 0 .39 19 3.8 1 910   13000 6000 0 900   2900 14000 0 900   8200 10000 0 210 760 2400 0
elevator_spec1_product28_false-unreach-call_true-termination.cil.c 45    950 560    1 1.2  42 13   1 910   11000 6100 0 910   11000 4700 0 7.6 330 59 1 490    210 7200   1 .23 39 2.2 1 1.6   68 21    1 960   9300 9200 0 .37 19 4.9 1 900   12000 7000 0 900   4600 11000 0 900   4600 10000 0 220 780 1900 0
elevator_spec1_product30_false-unreach-call_true-termination.cil.c 53    1200 420    1 1.2  42 12   1 910   11000 5100 0 910   11000 4800 0 7.6 330 64 1 500    320 6000   1 .24 40 2.3 1 2.0   80 24    1 970   9300 9100 0 .39 20 4.6 1 900   13000 7200 0 900   3700 14000 0 900   4600 11000 0 210 780 2100 0
elevator_spec1_product32_false-unreach-call_true-termination.cil.c 62    1300 440    1 1.3  43 16   1 900   11000 6100 0 910   11000 5000 0 7.8 340 52 1 500    340 5500   1 .22 40 3.2 1 2.3   84 28    1 970   8600 8400 0 .38 20 4.5 1 910   13000 6500 0 900   3100 12000 0 900   4600 10000 0 210 760 2400 0
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c 140    3700 1100    1 85    1200 760   1 900   11000 5700 0 910   11000 4500 0 9.8 380 83 1 700    790 9100   1 7.3  190 110   1 20     300 220    1 950   7400 10000 0 .44 24 6.5 1 910   13000 7000 0 900   4300 13000 0 900   4400 11000 0 690 6800 4800 0
elevator_spec2_product18_false-unreach-call_true-termination.cil.c 36    870 380    1 1.2  42 12   1 910   11000 5800 0 910   11000 4600 0 7.1 320 59 1 490    190 5100   1 .23 39 2.1 1 1.7   68 24    1 900   3500 12000 0 .38 18 4.3 1 910   14000 5900 0 900   5400 12000 0 900   6100 11000 0 210 850 2500 0
elevator_spec2_product20_false-unreach-call_true-termination.cil.c 37    930 330    1 1.2  42 12   1 900   11000 5600 0 910   11000 5000 0 7.9 320 62 1 490    200 5800   1 .20 39 2.4 1 1.8   70 21    1 900   3700 14000 0 .36 19 4.9 1 900   14000 5200 0 900   5700 12000 0 900   13000 7600 0 210 810 2100 0
elevator_spec2_product22_false-unreach-call_true-termination.cil.c 46    1200 540    1 1.2  42 12   1 910   11000 5700 0 910   11000 5100 0 7.3 320 61 1 500    240 5700   1 .23 39 2.2 1 2.2   83 28    1 900   3700 13000 0 .37 19 4.7 1 900   13000 6200 0 900   3400 15000 0 900   6500 10000 0 210 790 1900 0
elevator_spec2_product24_false-unreach-call_true-termination.cil.c 44    1300 340    1 1.3  43 13   1 910   11000 5500 0 900   11000 4300 0 7.5 330 59 1 500    330 5800   1 .21 40 2.2 1 2.4   85 28    1 900   3900 11000 0 .37 20 5.1 1 900   13000 7800 0 900   3700 13000 0 900   4600 11000 0 210 820 2300 0
elevator_spec2_product26_false-unreach-call_true-termination.cil.c 32    900 310    1 1.2  42 11   1 910   11000 5300 0 910   11000 5200 0 7.3 310 57 1 490    200 5800   1 .19 39 2.5 1 1.8   71 22    1 900   3200 11000 0 .36 19 4.4 1 900   14000 5200 0 900   4700 14000 0 900   6200 10000 0 210 760 2000 0
elevator_spec2_product28_false-unreach-call_true-termination.cil.c 36    970 290    1 1.2  42 13   1 900   11000 5400 0 910   11000 5300 0 7.7 330 57 1 490    220 6100   1 .23 39 2.2 1 1.9   74 22    1 900   3700 13000 0 .38 19 4.9 1 900   13000 7700 0 900   4400 13000 0 900   4700 11000 0 210 760 2200 0
elevator_spec2_product30_false-unreach-call_true-termination.cil.c 40    1200 380    1 1.2  42 14   1 910   11000 5600 0 910   11000 4500 0 7.4 330 58 1 500    320 6000   1 .21 40 2.3 1 2.2   86 35    1 900   3500 12000 0 .39 20 5.3 1 910   14000 6600 0 900   4800 12000 0 900   5600 11000 0 210 840 2600 0
elevator_spec2_product32_false-unreach-call_true-termination.cil.c 46    1300 430    1 1.2  43 14   1 910   11000 5900 0 910   11000 4600 0 7.5 330 65 1 500    340 5900   1 .24 40 2.3 1 2.5   91 28    1 900   3600 12000 0 .38 20 4.8 1 900   13000 7100 0 900   3700 15000 0 900   4600 11000 0 210 830 2300 0
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c 130    3800 1200    1 48    930 380   1 900   11000 5500 0 900   11000 4800 0 9.7 370 85 1 700    730 8800   1 7.4  190 84   1 20     300 210    1 960   7800 10000 0 .45 24 6.1 1 910   14000 5200 0 900   1500 16000 0 900   6500 10000 0 890 7900 6000 0
elevator_spec3_product03_false-unreach-call_true-termination.cil.c 2.9  580 31    1 .65 43 6.4 1 900   8300 9100 0 910   11000 5100 0 8.2 350 76 1 480    250 5100   1 .20 39 1.9 1 .17  39 1.9  1 950   6400 11000 0 .38 19 4.3 1 900   13000 6300 0 900   1600 10000 0 900   5400 10000 0 220 790 1400 0
elevator_spec3_product11_false-unreach-call_true-termination.cil.c 3.1  620 29    1 .61 43 5.7 1 900   8800 8400 0 910   11000 6200 0 8.3 350 71 1 480    270 5500   1 .17 39 2.0 1 .20  39 2.1  1 960   6300 12000 0 .39 20 4.5 1 910   13000 5900 0 900   2900 11000 0 900   5500 11000 0 210 770 1600 0
elevator_spec3_product19_false-unreach-call_true-termination.cil.c 3.2  660 32    1 .66 43 7.3 1 900   8600 6900 0 900   11000 4900 0 8.2 350 57 1 480    420 5500   1 .21 39 2.0 1 .17  39 1.9  1 940   7000 9900 0 .39 20 4.9 1 910   13000 6500 0 900   2900 14000 0 900   4600 11000 0 210 760 1900 0
elevator_spec3_product20_false-unreach-call_true-termination.cil.c 6.1  1200 61    1 .67 43 7.1 1 900   8700 8600 0 910   9300 7800 0 8.3 390 72 1 480    390 6100   1 .18 39 2.2 1 .20  39 1.9  1 930   6400 12000 0 .37 21 4.1 1 900   13000 6400 0 900   5400 12000 0 900   5400 11000 0 220 770 1400 0
elevator_spec3_product23_false-unreach-call_true-termination.cil.c 5.4  1000 53    1 .68 44 6.4 1 900   9000 7800 0 900   11000 4800 0 8.8 380 69 1 480    320 5900   1 .19 40 2.0 1 .23  39 2.1  1 960   7600 12000 0 .37 21 4.9 1 910   13000 6900 0 900   2500 12000 0 900   4600 13000 0 220 780 1500 0
elevator_spec3_product24_false-unreach-call_true-termination.cil.c 11    2000 99    1 .69 44 8.0 1 900   8600 9100 0 900   9300 8100 0 8.8 380 74 1 480    540 3800   1 .18 40 2.0 1 .19  40 2.7  1 940   6900 11000 0 .38 22 5.5 1 910   14000 6100 0 900   5400 13000 0 900   4600 11000 0 210 770 1400 0
elevator_spec3_product27_false-unreach-call_true-termination.cil.c 3.6  700 34    1 .64 43 6.4 1 900   8700 7800 0 910   11000 6600 0 8.0 360 64 1 480    430 5200   1 .21 39 2.0 1 .21  39 1.8  1 930   7400 10000 0 .40 21 4.6 1 900   13000 5700 0 900   2900 11000 0 900   5400 11000 0 220 760 1500 0
elevator_spec3_product28_false-unreach-call_true-termination.cil.c 6.6  1300 63    1 .64 43 7.5 1 900   8600 7800 0 900   9800 7900 0 8.2 370 68 1 480    420 5600   1 .20 39 1.8 1 .23  40 1.6  1 960   6100 11000 0 .38 22 4.5 1 900   14000 5600 0 900   5400 14000 0 900   4600 12000 0 220 760 1600 0
elevator_spec3_product31_false-unreach-call_true-termination.cil.c 5.5  1100 64    1 .68 44 7.2 1 900   8500 7600 0 900   11000 5800 0 8.6 370 72 1 480    330 5100   1 .18 40 2.1 1 .18  40 2.0  1 940   6600 12000 0 .39 22 5.6 1 910   13000 5600 0 900   2500 12000 0 900   4600 10000 0 210 750 1600 0
elevator_spec3_product32_false-unreach-call_true-termination.cil.c 11    2100 120    1 .65 44 8.1 1 900   8700 9400 0 910   9900 8400 0 8.2 400 65 1 480    560 4400   1 .19 40 2.1 1 .22  40 2.1  1 930   6600 11000 0 .41 22 4.7 1 910   13000 7200 0 900   5400 14000 0 900   4600 11000 0 220 810 1500 0
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c 38    7000 400    1 43    950 410   1 900   8500 8900 0 910   11000 5300 0 11   480 80 1 610    1400 4500   1 11    260 100   1 12     330 160    1 910   6200 12000 0 .44 26 6.2 1 910   13000 6600 0 900   3100 12000 0 900   4700 12000 0 810 7900 6400 0
elevator_spec9_product26_false-unreach-call_true-termination.cil.c 39    900 390    1 1.2  44 13   1 900   11000 5800 0 910   11000 4900 0 7.5 330 63 1 490    200 5100   1 .23 39 2.2 1 1.8   71 22    1 910   4300 12000 0 .36 19 4.6 1 910   14000 4900 0 900   4500 15000 0 910   14000 5000 0 440 1400 3200 0
elevator_spec9_product28_false-unreach-call_true-termination.cil.c 39    950 400    1 1.3  42 14   1 900   11000 6200 0 900   11000 4900 0 7.7 340 72 1 490    220 6000   1 .22 39 2.3 1 1.8   77 26    1 920   5000 11000 0 .39 20 4.7 1 910   14000 5000 0 900   5200 11000 0 910   14000 5400 0 440 1600 3700 0
elevator_spec9_product30_false-unreach-call_true-termination.cil.c 46    1300 360    1 1.2  42 13   1 910   11000 5900 0 910   11000 4300 0 7.6 330 60 1 500    320 6800   1 .22 39 2.6 1 2.3   88 27    1 920   4500 11000 0 .37 20 4.6 1 910   14000 5000 0 900   4900 13000 0 910   14000 5200 0 440 1400 2900 0
elevator_spec9_product32_false-unreach-call_true-termination.cil.c 47    1300 340    1 1.3  42 13   1 900   11000 5300 0 900   11000 4600 0 7.6 340 62 1 500    340 6300   1 .20 40 3.1 1 2.3   91 26    1 970   6800 13000 0 .39 20 4.8 1 910   14000 5600 0 900   2600 12000 0 910   14000 5000 0 440 1500 3100 0
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c 93    3700 870    1 47    930 450   0 910   11000 5800 0 900   11000 5500 0 9.5 400 84 1 690    730 7500   1 7.8  190 80   1 20     290 250    1 970   7300 11000 0 .45 24 5.8 1 910   14000 5200 0 900   1500 13000 0 910   14000 4900 0 900 3100 6700 0
elevator_spec13_product21_true-unreach-call_false-termination.cil.c 5.4  1000 48    0 870    12000 11000   0 900   8300 7100 0 900   11000 5100 0 5.2 280 44 1 890    1500 12000   0 900    1500 12000   0 900     1500 11000    0 900   4000 12000 0 900    15000 12000   0 910   14000 5300 0 900   2600 15000 0 900   5400 10000 0 480 1600 2900 0
elevator_spec13_product22_true-unreach-call_false-termination.cil.c 11    1900 100    0 870    12000 14000   0 910   11000 7200 0 910   11000 5700 0 5.6 280 52 1 900    2100 10000   0 900    1400 11000   0 900     1400 12000    0 900   4000 13000 0 900    15000 12000   0 910   14000 5700 0 900   2000 14000 0 900   4700 12000 0 470 1600 3800 0
elevator_spec13_product23_true-unreach-call_false-termination.cil.c 5.9  1100 50    0 750    15000 10000   0 900   8100 7400 0 900   11000 5500 0 5.2 280 40 1 890    660 10000   0 900    1900 13000   0 900     1900 11000    0 900   4000 12000 0 900    15000 13000   0 910   14000 6000 0 900   2500 11000 0 900   4600 11000 0 460 2100 2500 0
elevator_spec13_product24_true-unreach-call_false-termination.cil.c 11    2100 98    0 760    15000 11000   0 900   8200 7400 0 910   11000 5400 0 5.3 280 44 1 890    2400 11000   0 900    1900 14000   0 900     1900 11000    0 900   4000 11000 0 900    15000 12000   0 910   14000 6300 0 900   2300 11000 0 900   4900 11000 0 460 2000 2700 0
elevator_spec13_product29_true-unreach-call_false-termination.cil.c 5.6  1100 44    0 880    12000 11000   0 900   8600 8100 0 900   11000 5800 0 5.3 280 43 1 890    1700 10000   0 900    1500 11000   0 900     1500 14000    0 900   4000 11000 0 900    15000 12000   0 910   13000 5800 0 900   2500 11000 0 900   5400 11000 0 480 1600 2900 0
elevator_spec13_product30_true-unreach-call_false-termination.cil.c 11    2000 91    0 880    12000 11000   0 910   11000 7500 0 910   11000 5300 0 5.5 280 43 1 890    740 11000   0 900    1400 11000   0 900     1500 11000    0 900   4000 12000 0 900    15000 13000   0 910   14000 5700 0 900   2200 11000 0 900   5300 12000 0 480 1600 3100 0
elevator_spec13_product31_true-unreach-call_false-termination.cil.c 5.8  1200 60    0 750    15000 9700   0 900   8600 8000 0 910   11000 4900 0 5.4 280 44 1 900    660 11000   0 900    1900 13000   0 900     2000 11000    0 900   4100 14000 0 900    15000 12000   0 910   13000 6000 0 900   2500 13000 0 900   4700 11000 0 460 2100 2600 0
elevator_spec13_product32_true-unreach-call_false-termination.cil.c 11    2200 140    0 750    15000 9800   0 900   8000 7600 0 910   11000 5300 0 5.3 290 42 1 900    750 12000   0 900    2000 14000   0 900     1900 13000    0 900   4000 13000 0 900    15000 13000   0 910   14000 6100 0 900   2300 9900 0 900   5400 13000 0 470 2000 3300 0
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c 47    7300 380    0 870    460 9900   0 900   8100 8100 0 910   11000 4600 0 7.2 300 60 1 900    1400 8500   0 900    3300 9400   0 900     3700 7000    0 900   4300 12000 0 900    15000 11000   0 900   11000 7800 0 900   2400 11000 0 900   5000 10000 0 900 2500 8000 0
elevator_spec14_product03_true-unreach-call_true-termination.cil.c 20    860 210    2 3.3  47 37   1 120   5500 870 2 99   4000 770 2 6.1 290 49 2 540    300 6500   2 .64 36 8.6 2 1.6   51 21    2 900   3900 13000 0 .37 17 3.9 2 900   13000 7300 0 900   3100 12000 0 900   4600 10000 0 120 1000 1300 2
elevator_spec14_product11_true-unreach-call_true-termination.cil.c 20    910 180    2 3.3  47 42   1 120   5300 830 2 900   11000 4900 0 6.2 290 52 2 550    290 7300   2 .67 37 8.2 2 1.7   54 23    2 900   3700 12000 0 .37 18 4.7 2 900   13000 6400 0 900   1500 14000 0 900   4600 11000 0 120 1000 1100 2
elevator_spec14_product19_true-unreach-call_true-termination.cil.c 24    1000 240    2 3.4  47 37   1 120   5500 960 2 110   4100 680 2 5.8 290 51 2 550    290 7000   2 .75 37 8.1 2 1.8   52 23    2 900   3300 13000 0 .37 17 4.7 2 900   13000 7700 0 900   2400 13000 0 900   4600 12000 0 120 1100 1100 2
elevator_spec14_product23_true-unreach-call_true-termination.cil.c 10    1300 100    2 3.5  47 44   1 190   6500 1200 2 910   11000 5200 0 6.1 290 52 2 660    310 7700   2 1.1  37 15   2 2.3   61 34    2 900   4000 12000 0 .36 22 5.0 2 900   12000 8000 0 900   2600 12000 0 900   4600 11000 0 160 1300 1600 2
elevator_spec14_product27_true-unreach-call_true-termination.cil.c 24    1100 220    2 3.5  47 40   1 140   5500 890 2 910   11000 4900 0 6.6 290 53 2 550    290 6500   2 .76 37 9.1 2 1.9   54 23    2 900   2900 12000 0 .37 18 4.4 2 910   13000 7500 0 900   1800 12000 0 900   4700 12000 0 130 1100 1100 2
elevator_spec14_product31_true-unreach-call_true-termination.cil.c 11    1400 110    2 3.4  47 44   1 180   6500 1100 2 900   11000 5600 0 6.1 290 52 2 660    330 7700   2 1.1  37 12   2 2.4   64 35    2 900   4000 13000 0 .36 19 4.5 2 900   12000 8800 0 900   2600 11000 0 900   4600 10000 0 160 1300 1500 2
elevator_spec1_product01_true-unreach-call_true-termination.cil.c 28    1000 240    2 2.8  45 27   1 900   11000 5700 0 910   11000 5000 0 5.7 290 51 2 520    290 6900   2 .54 37 6.4 2 1.2   46 14    2 970   8400 9500 0 .36 17 5.5 2 900   11000 8300 0 900   3200 12000 0 900   4600 10000 0 160 1500 1100 2
elevator_spec1_product03_true-unreach-call_true-termination.cil.c 30    1100 300    2 3.0  45 34   1 900   11000 4700 0 900   11000 4800 0 5.7 280 50 2 540    290 6500   2 .62 37 8.7 2 1.4   48 19    2 970   8200 9100 0 .35 18 4.9 2 910   13000 6400 0 900   2500 14000 0 900   4700 11000 0 170 1700 1400 2
elevator_spec1_product09_true-unreach-call_true-termination.cil.c 29    1000 270    2 2.8  45 36   1 910   11000 5300 0 910   11000 5600 0 5.8 290 48 2 540    290 6300   2 .54 37 6.6 2 1.3   50 16    2 970   8200 9700 0 .35 18 4.2 2 910   12000 7800 0 900   2500 13000 0 900   4600 11000 0 170 1700 1400 2
elevator_spec1_product11_true-unreach-call_true-termination.cil.c 31    1100 300    2 3.1  45 33   1 900   11000 5200 0 910   11000 3900 0 6.0 290 47 2 550    290 7300   2 .60 37 6.9 2 1.5   51 20    2 970   8500 8000 0 .38 18 4.2 2 900   13000 7100 0 900   2900 10000 0 900   4200 9500 0 170 1700 1100 2
elevator_spec1_product17_true-unreach-call_true-termination.cil.c 33    1100 300    2 2.9  45 30   1 900   11000 5800 0 910   11000 5000 0 5.8 290 47 2 530    290 6300   2 .51 37 6.9 2 1.2   46 13    2 960   10000 10000 0 .34 18 5.4 2 910   11000 9800 0 900   2100 12000 0 900   5400 10000 0 160 1600 1200 2
elevator_spec1_product19_true-unreach-call_true-termination.cil.c 31    1100 280    2 3.1  46 45   1 910   11000 4500 0 910   11000 4700 0 6.1 290 51 2 550    300 7300   2 .54 37 6.8 2 1.3   49 15    2 970   8400 9600 0 .36 18 4.5 2 900   13000 8000 0 900   2900 11000 0 900   4500 10000 0 170 1700 1200 2
elevator_spec1_product21_true-unreach-call_true-termination.cil.c 39    1500 350    2 3.0  45 39   1 900   11000 4700 0 900   11000 5100 0 6.0 290 49 2 570    290 6800   2 .61 37 7.1 2 1.7   56 21    2 960   10000 8700 0 .36 18 5.0 2 900   13000 7400 0 900   2200 14000 0 900   4600 9900 0 170 1700 1200 2
elevator_spec1_product23_true-unreach-call_true-termination.cil.c 39    1600 420    2 3.2  47 39   1 900   11000 5100 0 900   11000 5200 0 6.4 290 51 2 580    300 7300   2 .70 38 9.7 2 1.9   58 27    2 970   8300 8200 0 .37 19 4.5 2 910   13000 6600 0 900   2700 14000 0 900   4600 11000 0 160 1700 1200 2
elevator_spec1_product25_true-unreach-call_true-termination.cil.c 29    1100 330    2 3.0  45 33   1 900   11000 5200 0 900   11000 5100 0 6.2 290 52 2 550    290 8100   2 .54 37 6.0 2 1.4   50 18    2 920   8900 8900 0 .36 19 4.9 2 900   13000 7400 0 900   3600 13000 0 900   6200 12000 0 160 1700 1200 2
elevator_spec1_product27_true-unreach-call_true-termination.cil.c 34    1200 320    2 3.1  46 37   1 900   11000 5200 0 910   11000 4800 0 5.8 290 43 2 550    300 7600   2 .60 38 7.3 2 1.5   52 16    2 950   8800 8800 0 .37 19 5.0 2 910   12000 7800 0 900   3300 11000 0 900   4700 11000 0 170 1700 1300 2
elevator_spec1_product29_true-unreach-call_true-termination.cil.c 37    1600 350    2 3.1  46 39   1 900   11000 5000 0 910   11000 4300 0 6.0 290 48 1 580    290 7200   2 .54 38 5.9 2 1.7   60 21    2 970   8400 9000 0 .38 19 5.3 2 910   14000 5700 0 900   3000 13000 0 900   4600 10000 0 170 1500 1300 2
elevator_spec1_product31_true-unreach-call_true-termination.cil.c 37    1600 420    2 3.3  47 41   1 900   11000 5100 0 910   11000 4500 0 6.0 300 44 2 590    300 7800   2 .74 38 11   2 2.0   61 26    2 960   8300 10000 0 .40 20 4.7 2 910   14000 6900 0 900   2700 12000 0 900   4600 12000 0 160 1800 1400 2
elevator_spec2_product01_true-unreach-call_true-termination.cil.c 21    710 180    2 1.6  42 18   1 900   11000 5000 0 900   11000 5900 0 5.3 280 43 2 440    280 5700   2 .29 37 3.3 2 1.2   52 13    2 910   3900 11000 0 .37 17 4.2 2 900   13000 5100 0 900   2900 12000 0 910   13000 6000 0 110 980 800 2
elevator_spec2_product03_true-unreach-call_true-termination.cil.c 21    750 220    2 1.6  42 22   1 910   11000 5300 0 900   11000 5400 0 5.6 290 51 2 500    280 6200   2 .30 37 3.4 2 1.3   54 14    2 920   5100 12000 0 .37 17 4.0 2 900   13000 5900 0 900   4500 13000 0 900   6700 13000 0 120 1000 890 2
elevator_spec2_product09_true-unreach-call_true-termination.cil.c 22    750 200    2 1.5  42 16   1 910   11000 5700 0 900   11000 5600 0 5.3 280 42 2 500    280 6700   2 .31 37 3.1 2 1.3   56 16    2 900   3700 12000 0 .35 18 4.3 2 900   14000 4700 0 900   3400 9600 0 910   13000 5500 0 110 1000 720 2
elevator_spec2_product11_true-unreach-call_true-termination.cil.c 22    790 240    2 1.7  43 18   1 900   11000 5500 0 900   11000 4900 0 5.3 290 39 2 500    280 5900   2 .35 37 3.4 2 1.4   56 15    2 920   5000 12000 0 .36 18 4.5 2 900   13000 5600 0 900   3700 12000 0 900   6300 12000 0 120 1100 930 2
elevator_spec2_product17_true-unreach-call_true-termination.cil.c 23    780 260    2 1.6  42 16   1 900   11000 5300 0 910   11000 5800 0 5.8 280 45 2 480    270 6400   2 .30 37 3.0 2 1.2   53 15    2 900   3600 13000 0 .35 18 4.8 2 900   14000 5200 0 900   3200 11000 0 910   14000 6000 0 110 1000 810 2
elevator_spec2_product19_true-unreach-call_true-termination.cil.c 26    830 250    2 1.6  43 20   1 900   11000 5500 0 910   11000 5000 0 5.2 280 50 2 500    290 7000   2 .32 37 3.3 2 1.3   55 17    2 900   3600 11000 0 .36 18 4.3 2 910   12000 6300 0 900   5300 11000 0 900   5900 11000 0 120 1100 790 2
elevator_spec2_product21_true-unreach-call_true-termination.cil.c 24    1100 280    2 1.6  43 18   1 900   11000 5000 0 910   11000 4700 0 5.3 280 45 2 510    280 6800   2 .31 37 3.0 2 1.6   59 18    2 900   3700 14000 0 .37 18 4.3 2 910   14000 5600 0 900   3400 11000 0 900   8600 8500 0 130 1200 1000 2
elevator_spec2_product23_true-unreach-call_true-termination.cil.c 29    1100 240    2 1.7  43 16   1 900   11000 5700 0 900   11000 5800 0 5.5 280 44 2 510    280 6300   2 .32 38 3.5 2 1.7   61 19    2 900   3700 12000 0 .39 19 3.9 2 910   13000 6800 0 900   2400 11000 0 900   4700 11000 0 120 1200 910 2
elevator_spec2_product25_true-unreach-call_true-termination.cil.c 25    810 220    2 1.6  42 18   1 900   11000 5100 0 900   11000 4500 0 5.3 280 40 2 500    280 5200   2 .29 37 3.5 2 1.4   56 15    2 900   3500 11000 0 .37 18 4.4 2 910   14000 5000 0 900   3700 13000 0 900   13000 5500 0 110 1000 860 2
elevator_spec2_product27_true-unreach-call_true-termination.cil.c 27    860 230    2 1.7  43 17   1 900   11000 5900 0 910   11000 4800 0 5.9 290 43 2 510    290 6600   2 .34 37 3.7 2 1.5   58 18    2 900   3400 12000 0 .38 19 4.4 2 910   13000 6200 0 900   3100 14000 0 900   6200 11000 0 120 1100 910 2
elevator_spec2_product29_true-unreach-call_true-termination.cil.c 28    1100 220    2 1.7  43 17   1 900   11000 5100 0 900   11000 5000 0 5.6 280 38 2 510    280 6300   2 .31 38 3.3 2 1.7   62 20    2 900   3700 13000 0 .39 19 5.1 2 900   14000 5100 0 900   3000 14000 0 900   12000 7500 0 130 1200 890 2
elevator_spec2_product31_true-unreach-call_true-termination.cil.c 30    1200 260    2 1.8  43 18   1 900   11000 5100 0 910   11000 6000 0 5.6 280 46 2 510    290 5400   2 .31 38 3.9 2 1.8   64 21    2 900   3700 14000 0 .40 19 4.5 2 900   12000 6400 0 900   5300 13000 0 900   6000 12000 0 130 1300 940 2
elevator_spec3_product01_true-unreach-call_true-termination.cil.c 3.1  630 31    2 3.5  47 40   1 910   9800 7600 0 910   11000 5300 0 5.9 290 48 2 490    300 5900   2 .97 37 11   2 .81  45 10    2 910   6900 10000 0 .38 19 4.2 2 910   14000 5900 0 900   2700 10000 0 900   6500 11000 0 93 750 640 2
elevator_spec3_product09_true-unreach-call_true-termination.cil.c 3.3  680 31    2 3.5  47 40   1 910   9400 7500 0 910   11000 5100 0 5.9 290 45 2 490    330 6000   2 .89 37 12   2 .90  49 9.9  2 910   6900 11000 0 .36 20 4.5 2 900   13000 4800 0 900   2800 12000 0 900   13000 5600 0 100 770 780 2
elevator_spec3_product17_true-unreach-call_true-termination.cil.c 3.4  730 34    2 3.5  47 37   1 900   9400 8100 0 910   11000 4900 0 6.2 290 50 2 490    300 6300   2 .97 37 11   2 .87  47 11    2 910   7400 11000 0 .39 20 4.2 2 900   14000 5300 0 900   1900 10000 0 900   6600 11000 0 95 780 700 2
elevator_spec3_product18_true-unreach-call_true-termination.cil.c 6.4  1400 61    2 3.6  47 41   1 900   9200 8100 0 900   11000 7700 0 6.1 290 53 2 490    360 5000   2 1.1  37 13   2 1.4   60 17    2 940   7000 9900 0 .39 20 4.3 2 900   13000 5900 0 900   5300 13000 0 910   13000 6600 0 100 860 800 2
elevator_spec3_product21_true-unreach-call_true-termination.cil.c 5.5  1200 50    2 3.9  50 42   1 900   8300 8600 0 910   11000 6700 0 6.2 290 49 2 490    610 6300   2 1.1  38 15   2 1.2   55 13    2 960   7300 12000 0 .36 20 4.9 2 910   13000 4800 0 900   2600 12000 0 900   8400 11000 0 110 840 780 2
elevator_spec3_product22_true-unreach-call_true-termination.cil.c 11    2300 120    2 4.0  49 46   1 910   9300 7600 0 910   11000 7600 0 6.2 290 55 2 500    460 4300   2 1.3  38 14   2 2.0   75 24    2 910   6900 9300 0 .37 21 4.5 2 910   14000 6200 0 900   2300 13000 0 900   9600 8900 0 110 1000 790 2
elevator_spec3_product25_true-unreach-call_true-termination.cil.c 3.6  770 34    2 3.6  47 44   1 910   9400 8400 0 900   11000 6800 0 6.0 290 51 2 490    330 5900   2 1.0  37 13   2 .93  50 9.8  2 960   8400 11000 0 .36 20 4.5 2 910   14000 6800 0 900   3300 12000 0 900   7000 11000 0 95 770 700 2
elevator_spec3_product26_true-unreach-call_true-termination.cil.c 6.8  1500 63    2 3.6  48 50   1 910   9200 8900 0 900   11000 7100 0 6.1 290 55 2 490    400 5700   2 1.1  38 13   2 1.6   65 20    2 940   6900 9700 0 .39 21 4.4 2 900   13000 6200 0 900   5200 14000 0 900   6400 10000 0 110 920 740 2
elevator_spec3_product29_true-unreach-call_true-termination.cil.c 5.7  1200 57    2 3.9  50 47   1 900   8300 7900 0 900   11000 6200 0 6.4 290 48 2 490    320 6300   2 1.1  38 14   2 1.4   58 16    2 910   6800 10000 0 .39 21 5.0 2 910   13000 5300 0 900   3600 13000 0 900   8400 9800 0 100 830 810 2
elevator_spec3_product30_true-unreach-call_true-termination.cil.c 12    2400 120    2 4.0  50 52   1 900   9300 8200 0 910   11000 6500 0 6.6 290 57 2 500    520 5400   2 1.2  38 19   2 2.2   79 29    2 940   6900 11000 0 .38 22 4.6 2 910   13000 6800 0 900   5300 11000 0 900   4600 11000 0 110 1000 830 2
elevator_spec9_product09_true-unreach-call_true-termination.cil.c 22    750 220    2 1.5  42 18   1 910   11000 5800 0 900   11000 5100 0 5.4 280 40 2 500    280 7400   2 .29 37 2.9 2 1.3   55 16    2 900   3900 12000 0 .38 18 4.1 2 910   13000 5400 0 900   3500 13000 0 910   13000 5800 0 350 1000 2000 2
elevator_spec9_product11_true-unreach-call_true-termination.cil.c 22    780 190    2 1.7  44 17   1 900   11000 6700 0 910   11000 5100 0 5.6 280 46 2 500    280 7300   2 .35 37 3.5 2 1.5   56 17    2 920   4900 12000 0 .38 19 4.1 2 910   14000 5400 0 900   2800 11000 0 910   14000 5200 0 340 1100 2000 2
elevator_spec9_product25_true-unreach-call_true-termination.cil.c 22    810 320    2 1.6  42 19   1 900   11000 6200 0 910   11000 5500 0 5.3 280 44 2 500    280 6200   2 .31 37 3.5 2 1.3   55 16    2 910   3800 12000 0 .38 18 4.1 2 910   14000 5300 0 900   2900 12000 0 910   13000 6900 0 350 1100 2300 2
elevator_spec9_product27_true-unreach-call_true-termination.cil.c 24    860 210    2 1.7  43 18   1 910   11000 6000 0 910   11000 5000 0 5.6 280 49 2 510    290 6100   2 .37 37 3.9 2 1.5   57 19    2 920   5000 11000 0 .39 19 4.2 2 910   14000 5300 0 900   3200 14000 0 910   14000 5300 0 360 1100 2000 2
elevator_spec9_product29_true-unreach-call_true-termination.cil.c 28    1100 280    2 1.7  43 16   1 900   11000 5100 0 910   11000 5100 0 5.4 290 40 2 510    280 6800   2 .29 38 3.1 2 1.7   64 19    2 910   4600 12000 0 .36 19 4.2 2 900   14000 6500 0 900   3700 11000 0 910   13000 6000 0 350 1200 2200 2
elevator_spec9_product31_true-unreach-call_true-termination.cil.c 33    1200 320    2 1.8  43 17   1 900   11000 6700 0 910   11000 4300 0 5.4 280 51 2 510    280 6800   2 .31 38 3.7 2 1.8   65 22    2 960   6100 12000 0 .39 20 4.8 2 910   14000 5300 0 900   2300 14000 0 910   14000 5300 0 360 1300 2200 2
email_spec0_product16_false-unreach-call_true-termination.cil.c 21    290 190    1 3.1  55 25   0 130   5500 1100 1 900   5300 7000 0 14   510 110 1 490    170 6100   0 2.7  41 24   1 2.8   41 27    1 900   4800 10000 0 .39 15 4.5 1 900   10000 7300 0 900   4400 12000 0 900   6000 11000 0 500 3800 5500 0
email_spec0_product21_false-unreach-call_true-termination.cil.c 37    500 300    1 4.5  64 70   0 900   11000 5200 0 900   6600 8700 0 12   490 97 1 500    300 6300   0 3.8  50 44   1 4.3   52 43    1 900   4800 11000 0 .40 17 4.6 1 900   11000 6900 0 900   4200 13000 0 900   5400 12000 0 530 3900 5900 0
email_spec0_product22_false-unreach-call_true-termination.cil.c 26    310 190    1 3.1  56 32   1 210   6600 1500 1 900   9200 8000 0 14   510 130 1 490    190 4700   0 2.6  43 28   1 3.2   43 34    1 900   4600 11000 0 .39 16 4.7 1 900   12000 6100 0 900   6200 11000 0 910   13000 5700 0 500 3900 5900 0
email_spec0_product26_false-unreach-call_true-termination.cil.c 42    540 550    1 5.0  65 57   0 910   11000 6300 0 900   9000 8300 0 14   520 120 1 500    490 5600   0 5.0  54 46   1 4.6   54 46    1 900   4700 13000 0 .42 18 4.8 1 900   13000 7300 0 900   5400 13000 0 910   12000 7500 0 520 4000 5500 0
email_spec0_product31_false-unreach-call_true-termination.cil.c 20    320 210    1 3.4  57 37   0 910   11000 5200 0 900   6200 9900 0 15   530 140 1 490    180 5300   0 2.7  43 29   1 3.0   43 30    1 900   5600 11000 0 .41 17 4.6 1 910   14000 6800 0 900   4100 12000 0 900   6200 12000 0 510 3800 5800 0
email_spec0_product33_false-unreach-call_true-termination.cil.c 25    350 210    1 3.6  60 41   0 910   11000 5900 0 900   10000 7500 0 14   520 130 1 490    160 4900   0 2.8  45 29   1 3.5   45 37    1 900   5500 11000 0 .42 18 5.3 1 900   14000 6500 0 900   5500 12000 0 900   5400 12000 0 510 3800 5800 0
email_spec0_product34_false-unreach-call_true-termination.cil.c 37    590 430    1 6.0  76 64   0 900   11000 6100 0 900   8400 7600 0 15   530 140 1 500    230 6400   0 4.1  56 45   1 4.3   57 59    1 900   5500 9900 0 .40 19 4.8 1 900   13000 6700 0 900   4500 12000 0 900   5800 12000 0 540 3900 5600 0
email_spec0_product35_false-unreach-call_true-termination.cil.c 48    670 450    1 6.4  77 73   1 910   11000 6000 0 910   10000 6800 0 18   800 140 1 500    220 4800   0 4.8  58 49   1 5.2   59 54    1 900   5500 12000 0 .45 20 5.0 1 900   13000 7300 0 900   5000 11000 0 900   4800 13000 0 550 4000 6200 0
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c 200    8000 1300    1 870    1800 5200   0 900   11000 8200 0 900   10000 7600 0 560   6200 6800 1 890    1600 12000   0 48    440 560   1 65     470 730    1 900   5700 11000 0 1.2  38 15   1 900   13000 5000 0 910   6500 13000 0 900   4600 11000 0 900 2500 6300 0
email_spec11_product15_false-unreach-call_true-termination.cil.c 19    270 240    1 3.0  56 34   0 900   11000 5600 0 900   8200 8800 0 12   480 110 1 490    140 5700   0 2.4  41 23   1 2.5   40 31    1 900   4400 11000 0 .37 15 3.9 1 900   12000 7300 0 900   6200 12000 0 900   6600 9600 0 500 3800 6100 0
email_spec11_product20_false-unreach-call_true-termination.cil.c 41    460 400    1 4.1  63 42   1 910   11000 6200 0 900   7400 11000 0 11   430 99 1 490    320 5700   0 4.0  49 45   1 3.4   51 35    1 900   4400 14000 0 .37 17 5.2 1 900   13000 6800 0 900   4500 14000 0 900   5400 12000 0 510 3900 6800 0
email_spec11_product22_false-unreach-call_true-termination.cil.c 21    310 210    1 3.1  56 31   0 580   9900 4200 1 900   8900 9300 0 12   480 98 1 490    270 6300   0 2.6  43 28   1 3.0   43 30    1 900   4600 13000 0 .39 16 4.5 1 900   12000 7400 0 900   3500 13000 0 900   6000 11000 0 500 3900 5300 0
email_spec11_product26_false-unreach-call_true-termination.cil.c 43    540 370    1 4.9  65 54   1 900   11000 5400 0 910   11000 9500 0 13   490 100 1 500    190 5900   0 3.9  53 40   1 4.3   54 62    1 900   4400 12000 0 .38 18 4.4 1 900   12000 8200 0 900   3400 14000 0 900   5300 13000 0 530 3900 5700 0
email_spec11_product30_false-unreach-call_true-termination.cil.c 23    300 190    1 3.2  57 41   0 240   6900 1700 1 900   6700 12000 0 12   480 100 1 490    200 6200   0 2.6  43 24   1 2.8   43 24    1 900   4400 12000 0 .37 16 4.7 1 900   11000 8100 0 900   6300 12000 0 900   7600 11000 0 510 3800 5700 0
email_spec11_product32_false-unreach-call_true-termination.cil.c 39    520 370    1 5.3  70 62   1 900   11000 5300 0 900   8600 11000 0 13   510 100 1 500    210 5400   0 4.6  54 46   1 3.7   55 42    1 900   4600 13000 0 .39 18 5.4 1 900   14000 6500 0 900   4500 11000 0 900   6700 9900 0 540 3900 5100 0
email_spec11_product33_false-unreach-call_true-termination.cil.c 22    350 210    1 3.5  58 38   1 910   11000 5200 0 900   8600 8500 0 12   480 110 1 490    180 5600   0 2.8  45 28   1 3.0   45 33    1 900   4800 12000 0 .38 18 5.2 1 910   14000 6200 0 900   4400 13000 0 900   6800 12000 0 510 3900 5400 0
email_spec11_product35_false-unreach-call_true-termination.cil.c 46    640 420    1 6.5  77 77   0 910   11000 5300 0 900   10000 8800 0 12   480 99 1 500    310 5100   0 4.3  58 48   1 5.0   59 67    1 900   4900 11000 0 .41 20 5.3 1 910   13000 7100 0 900   6000 14000 0 900   6000 9700 0 550 3900 6600 0
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c 280    8500 1400    1 870    2200 5000   0 910   8600 10000 0 910   11000 6800 0 550   6300 5500 1 890    1600 8700   0 56    490 630   1 75     520 830    1 910   6100 11000 0 .72 25 9.0 1 910   14000 6800 0 900   6600 11000 0 900   13000 6200 0 900 2500 5700 0
email_spec1_product14_false-unreach-call_true-termination.cil.c 31    390 290    1 2.8  55 37   0 900   8000 9100 0 910   7300 9500 0 14   530 110 1 490    200 5400   0 2.9  39 26   1 3.6   42 35    1 900   4900 10000 0 .39 16 5.4 1 900   13000 5600 0 900   6200 12000 0 900   9900 8600 0 500 3900 4900 0
email_spec1_product15_false-unreach-call_true-termination.cil.c 23    250 180    1 2.8  54 29   0 83   4200 640 1 900   9800 7600 0 12   450 100 1 490    210 5800   0 2.6  37 29   1 3.5   40 29    1 900   4900 12000 0 .49 17 5.4 1 910   12000 8000 0 900   7000 12000 0 900   5700 12000 0 510 3800 5800 0
email_spec1_product16_false-unreach-call_true-termination.cil.c 23    270 180    1 3.0  54 35   0 900   11000 5900 0 900   9900 6700 0 13   480 110 1 490    160 5400   0 2.9  37 27   1 3.6   41 34    1 900   5600 11000 0 .42 15 5.0 1 910   13000 9400 0 900   6600 11000 0 900   5700 12000 0 500 3800 5200 0
email_spec1_product20_false-unreach-call_true-termination.cil.c 41    440 320    1 4.1  61 46   0 430   9500 3300 1 900   6400 10000 0 14   510 100 1 490    180 6300   0 2.9  45 25   1 4.6   49 42    1 900   4900 10000 0 .44 17 4.8 1 900   11000 7400 0 900   6100 13000 0 900   8400 10000 0 520 3900 6600 0
email_spec1_product21_false-unreach-call_true-termination.cil.c 42    480 350    1 4.6  63 50   1 910   11000 5600 0 900   6100 11000 0 17   790 160 1 490    170 5400   0 3.1  46 32   1 4.6   52 44    1 900   5500 11000 0 .40 17 4.7 1 900   11000 7800 0 900   6400 13000 0 900   9200 11000 0 530 3900 6100 0
email_spec1_product22_false-unreach-call_true-termination.cil.c 25    290 210    1 3.1  56 32   1 900   8200 9200 0 900   10000 7100 0 12   490 110 1 490    300 5400   0 3.0  39 25   1 3.9   43 36    1 900   4800 11000 0 .45 16 4.9 1 900   12000 8400 0 900   6800 10000 0 900   5500 11000 0 500 3900 6200 0
email_spec1_product26_false-unreach-call_true-termination.cil.c 44    520 400    1 4.9  64 62   1 910   11000 4700 0 900   5500 10000 0 14   530 130 1 490    320 5000   0 3.4  48 31   1 5.4   54 55    1 900   4900 13000 0 .43 18 5.3 1 900   12000 7300 0 900   6200 13000 0 900   9700 8000 0 520 3900 6500 0
email_spec1_product29_false-unreach-call_true-termination.cil.c 33    460 280    1 3.3  56 42   1 900   8200 9500 0 900   6000 9600 0 17   740 150 1 490    200 5500   0 2.8  41 24   1 3.1   45 44    1 910   5700 10000 0 .43 17 5.2 1 910   13000 7000 0 900   6300 12000 0 900   9300 9600 0 510 3900 5700 0
email_spec1_product30_false-unreach-call_true-termination.cil.c 21    300 240    1 3.2  54 33   1 160   5700 1300 1 900   8800 9800 0 17   800 150 1 490    210 5600   0 2.6  39 21   1 3.5   43 33    1 910   5600 11000 0 .48 17 6.4 1 900   11000 7800 0 900   6400 12000 0 900   7400 11000 0 500 3800 5300 0
email_spec1_product31_false-unreach-call_true-termination.cil.c 22    310 260    1 3.4  56 41   0 240   6800 1700 1 900   9400 7900 0 22   900 230 1 490    140 5800   0 2.9  39 25   1 3.6   43 36    1 920   5800 11000 0 .44 17 4.5 1 900   11000 6900 0 900   6200 15000 0 910   10000 9700 0 510 3800 5400 0
email_spec1_product32_false-unreach-call_true-termination.cil.c 39    500 330    1 5.2  67 60   0 910   8300 9400 0 900   7200 9200 0 15   540 120 1 490    320 5500   0 2.9  48 31   1 5.0   55 51    1 900   5500 10000 0 .44 18 5.5 1 900   11000 7400 0 900   6100 13000 0 900   10000 10000 0 530 3900 5700 0
email_spec1_product33_false-unreach-call_true-termination.cil.c 25    340 270    1 3.6  56 41   1 320   8000 2400 1 910   9800 6600 0 19   810 170 1 490    360 6700   0 2.9  41 29   1 4.0   45 37    1 910   5700 12000 0 .48 18 5.0 1 910   13000 5700 0 900   6600 12000 0 900   12000 9000 0 510 3900 5800 0
email_spec1_product34_false-unreach-call_true-termination.cil.c 40    570 340    1 6.0  72 66   0 910   11000 6500 0 900   8900 8500 0 16   580 160 1 490    220 5600   0 3.3  49 33   1 4.9   55 48    1 910   5600 10000 0 .43 19 4.9 1 900   13000 7800 0 900   6100 13000 0 900   9800 9100 0 540 3900 5800 0
email_spec1_product35_false-unreach-call_true-termination.cil.c 45    620 360    1 6.4  74 94   0 900   11000 5600 0 900   7200 9200 0 16   580 150 1 490    240 6100   0 3.3  52 39   1 6.0   59 57    1 910   5800 12000 0 .47 20 7.1 1 910   14000 5800 0 900   6100 14000 0 900   11000 9000 0 550 4000 6500 0
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c 140    7600 1100    1 130    640 1700   1 900   8900 8300 0 900   7800 9900 0 17   730 140 1 620    1600 6400   0 9.8  170 120   1 28     210 300    1 920   6100 13000 0 1.3  41 15   1 910   13000 6100 0 900   6300 11000 0 900   5100 13000 0 900 4500 8100 0
email_spec27_product17_false-unreach-call_true-termination.cil.c 32    400 280    1 3.1  57 34   1 350   8300 2500 1 900   8000 8800 0 18   800 160 1 490    350 5700   0 3.6  40 31   1 4.2   43 45    1 900   4400 11000 0 .55 19 6.3 1 910   13000 5700 0 900   3500 13000 0 900   5200 11000 0 510 3900 5500 0
email_spec27_product18_false-unreach-call_true-termination.cil.c 23    260 180    1 3.0  55 34   1 350   7800 2400 1 900   7000 8800 0 15   540 130 1 490    170 5000   0 3.0  38 37   1 4.0   41 45    1 900   4300 11000 0 .57 20 6.8 1 900   13000 8800 0 900   5500 12000 0 900   6200 11000 0 500 3800 6200 0
email_spec27_product19_false-unreach-call_true-termination.cil.c 19    280 190    1 3.1  57 34   1 320   8200 2500 1 910   11000 8800 0 18   810 170 1 490    170 5500   0 3.9  38 32   1 4.3   41 38    1 900   4800 11000 0 .43 16 5.2 1 910   13000 8300 0 900   3500 13000 0 900   5400 11000 0 510 3800 5300 0
email_spec27_product23_false-unreach-call_true-termination.cil.c 44    450 370    1 4.4  63 46   0 910   11000 5500 0 900   8100 9600 0 14   520 120 1 490    300 6200   0 3.8  46 39   1 5.3   51 49    1 900   4400 13000 0 .58 20 8.1 1 900   12000 8500 0 900   2700 12000 0 900   5400 12000 0 520 3900 5600 0
email_spec27_product24_false-unreach-call_true-termination.cil.c 23    300 200    1 3.2  57 35   1 910   11000 5100 0 900   11000 8400 0 16   550 110 1 490    230 4700   0 3.7  40 38   1 4.6   44 42    1 900   4400 14000 0 .44 17 5.8 1 900   12000 8100 0 900   4700 12000 0 900   5900 12000 0 510 3800 5500 0
email_spec27_product25_false-unreach-call_true-termination.cil.c 33    480 330    1 4.9  66 59   1 910   11000 4800 0 900   5400 11000 0 17   810 150 1 490    230 5400   0 3.9  47 47   1 5.1   52 54    1 900   4600 11000 0 .43 18 5.1 1 910   13000 4900 0 900   4800 12000 0 900   6200 10000 0 530 3900 5500 0
email_spec27_product27_false-unreach-call_true-termination.cil.c 48    530 360    1 5.3  68 57   0 900   11000 5400 0 900   8900 10000 0 14   510 110 1 490    180 5900   0 4.3  49 37   1 6.1   55 62    1 900   4400 12000 0 .47 18 5.6 1 910   13000 6000 0 900   3200 14000 0 900   4600 10000 0 540 4000 6500 0
email_spec27_product29_false-unreach-call_true-termination.cil.c 34    470 310    1 3.4  59 42   0 160   5600 1300 1 900   9400 8500 0 22   900 220 1 490    330 5400   0 4.4  42 50   1 6.5   46 49    1 900   4500 11000 0 .63 20 8.4 1 900   12000 8200 0 900   3500 14000 0 900   4700 11000 0 510 3900 5300 0
email_spec27_product30_false-unreach-call_true-termination.cil.c 20    290 190    1 3.4  58 36   0 240   6800 1500 1 910   7500 11000 0 21   880 190 1 490    390 5200   0 4.7  40 41   1 6.0   44 42    1 900   4400 12000 0 .63 22 7.1 1 910   13000 6700 0 900   6200 13000 0 900   6000 11000 0 510 3800 6300 0
email_spec27_product31_false-unreach-call_true-termination.cil.c 23    310 190    1 3.5  58 44   0 200   6600 1600 1 900   7500 10000 0 27   1500 250 1 490    150 5900   0 4.6  40 38   1 6.2   44 42    1 900   4500 13000 0 .43 17 5.9 1 900   13000 6900 0 900   6100 13000 0 900   6000 10000 0 510 3800 5400 0
email_spec27_product32_false-unreach-call_true-termination.cil.c 40    520 350    1 5.6  72 62   0 520   10000 4200 1 900   6400 11000 0 16   610 150 1 490    320 5400   0 5.4  50 48   1 6.8   58 70    1 900   4600 11000 0 .65 23 8.6 1 900   13000 7600 0 900   5600 14000 0 900   4600 10000 0 530 3900 7400 0
email_spec27_product33_false-unreach-call_true-termination.cil.c 24    330 240    1 3.7  59 43   0 330   8700 2500 1 900   9800 8200 0 22   910 200 1 490    150 5700   0 4.7  42 42   1 5.5   46 46    1 930   5300 11000 0 .48 18 6.9 1 910   13000 6900 0 900   5500 13000 0 900   6100 11000 0 510 3900 5000 0
email_spec27_product34_false-unreach-call_true-termination.cil.c 41    590 390    1 6.4  76 71   1 910   11000 5800 0 900   7400 8700 0 20   820 160 1 490    230 5500   0 5.0  53 45   1 7.5   60 73    1 900   4600 11000 0 .49 19 5.3 1 910   11000 6900 0 900   4900 14000 0 900   4600 12000 0 540 3900 6600 0
email_spec27_product35_false-unreach-call_true-termination.cil.c 44    640 370    1 6.9  79 80   0 910   11000 5500 0 900   8200 8600 0 19   830 190 1 500    220 5700   0 5.2  54 49   1 8.0   65 81    1 900   5200 10000 0 .50 20 5.5 1 900   13000 6700 0 900   4500 12000 0 900   4600 12000 0 560 3900 5700 0
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c 440    11000 2500    1 340    920 2600   0 900   8400 9100 0 900   9700 9400 0 22   920 190 1 740    1500 8300   0 15    260 160   1 47     320 500    1 900   4600 11000 0 1.7  54 21   1 900   13000 6400 0 900   6300 11000 0 900   4700 12000 0 900 2500 5700 0
email_spec3_product13_false-unreach-call_true-termination.cil.c .65 110 5.8  1 .84 45 8.4 1 160   5700 1200 1 12   500 110 0 7.5 330 65 1 480    260 5800   0 .74 36 6.1 1 1.1   37 13    1 900   8000 13000 0 .39 15 4.3 1 900   13000 7000 0 75   1200 870 0 900   6700 11000 0 500 3800 5500 0
email_spec3_product17_false-unreach-call_true-termination.cil.c 1.0  210 9.7  1 1.0  50 12   1 540   9600 4600 1 15   650 110 0 7.8 340 59 1 480    220 6700   0 .86 37 7.3 1 1.5   40 17    1 910   5800 9900 0 .38 16 4.5 1 910   13000 6400 0 84   1200 830 0 900   6300 12000 0 510 3900 5300 0
email_spec3_product18_false-unreach-call_true-termination.cil.c .73 120 6.7  1 .98 48 10   1 150   5600 1200 1 12   500 93 1 7.9 340 61 1 480    410 6200   0 .69 36 9.7 1 1.3   38 12    1 900   5500 10000 0 .39 16 4.4 1 910   13000 7300 0 82   1200 790 0 900   6800 10000 0 510 3800 6000 0
email_spec3_product19_false-unreach-call_true-termination.cil.c .76 140 7.9  1 .99 49 10   1 150   5600 1200 1 12   500 84 0 7.4 330 62 1 480    140 6200   0 .74 36 9.0 1 1.3   38 13    1 900   5800 12000 0 .39 16 4.3 1 910   8300 9100 0 85   1200 850 0 900   6300 10000 0 510 3800 5700 0
email_spec3_product23_false-unreach-call_true-termination.cil.c 1.1  230 11    1 1.5  60 18   1 570   9700 4800 1 18   640 130 1 7.5 330 69 1 480    200 4600   0 .75 37 6.9 1 1.8   45 18    1 910   5800 11000 0 .40 17 4.1 1 900   9200 8000 0 79   1100 810 0 900   6700 10000 0 530 3900 5400 0
email_spec3_product24_false-unreach-call_true-termination.cil.c .80 150 8.3  1 1.1  49 11   1 180   5800 1200 1 12   480 95 1 7.3 330 57 1 480    150 5500   0 .76 37 8.6 1 1.3   39 12    1 940   6100 12000 0 .38 17 4.8 1 910   13000 6900 0 85   1200 900 0 900   7100 10000 0 520 3900 6700 0
email_spec3_product25_false-unreach-call_true-termination.cil.c 1.3  280 13    1 1.6  60 22   1 670   10000 5100 1 17   670 130 0 7.7 340 60 1 480    170 5600   0 .77 37 7.8 1 1.6   46 21    1 910   6300 12000 0 .38 18 4.8 1 910   14000 7300 0 87   1200 980 0 900   5500 11000 0 540 3900 6100 0
email_spec3_product27_false-unreach-call_true-termination.cil.c 1.4  310 15    1 1.7  60 19   1 600   9700 5000 1 16   640 140 1 7.3 330 60 1 480    220 4600   0 .73 38 7.7 1 1.9   49 21    1 930   6000 11000 0 .42 19 4.7 1 900   13000 7000 0 85   1100 930 0 900   5700 12000 0 540 4000 6900 0
email_spec3_product28_false-unreach-call_true-termination.cil.c .77 130 7.2  1 .90 47 8.3 1 470   9200 3200 1 12   500 98 0 7.7 340 60 1 480    170 5100   0 .80 36 6.7 1 1.2   38 11    1 910   5800 11000 0 .40 16 5.0 1 900   13000 7800 0 900   4700 12000 0 900   5200 12000 0 500 3800 5400 0
email_spec3_product29_false-unreach-call_true-termination.cil.c 1.2  270 13    1 1.1  54 13   1 150   5700 1100 1 16   650 120 0 7.9 340 65 1 480    400 5200   0 .79 38 8.2 1 1.5   41 14    1 930   6000 11000 0 .40 18 4.9 1 900   14000 5700 0 900   4500 12000 0 900   5000 11000 0 510 3900 6200 0
email_spec3_product30_false-unreach-call_true-termination.cil.c .81 150 7.4  1 1.1  51 13   1 560   11000 3700 1 13   500 100 1 7.9 340 58 1 480    190 5400   0 .71 37 8.2 1 1.3   39 13    1 910   5800 9200 0 .41 17 4.5 1 910   13000 7900 0 900   4500 11000 0 900   5800 11000 0 510 3800 6200 0
email_spec3_product31_false-unreach-call_true-termination.cil.c .89 170 9.2  1 1.1  50 13   1 410   8800 2700 1 13   510 100 0 8.0 340 70 1 480    280 4600   0 .76 37 8.0 1 1.3   39 13    1 910   5800 11000 0 .40 17 4.5 1 910   14000 7600 0 900   4000 14000 0 900   6000 11000 0 510 3800 5400 0
email_spec3_product32_false-unreach-call_true-termination.cil.c 1.4  310 12    1 1.8  63 21   1 170   5600 1300 1 16   650 130 1 8.3 350 65 1 480    230 5500   0 .73 38 7.3 1 1.9   48 18    1 950   5800 13000 0 .40 19 5.4 1 910   13000 6100 0 900   4600 13000 0 900   4600 9500 0 540 3900 5700 0
email_spec3_product33_false-unreach-call_true-termination.cil.c .93 180 8.5  1 1.2  52 13   1 420   8800 2900 1 13   510 110 1 7.9 340 73 1 480    280 5100   0 .73 37 8.9 1 1.3   41 15    1 910   5900 11000 0 .42 18 4.8 1 900   12000 7100 0 900   4400 13000 0 900   6100 11000 0 520 3900 5800 0
email_spec3_product34_false-unreach-call_true-termination.cil.c 1.6  380 17    1 2.1  68 26   1 170   5600 1300 1 19   630 120 0 8.0 340 69 1 480    200 5000   0 .73 38 7.8 1 1.7   50 19    1 910   6000 13000 0 .40 20 4.6 1 910   13000 7500 0 900   4900 14000 0 900   4600 11000 0 550 3900 5700 0
email_spec3_product35_false-unreach-call_true-termination.cil.c 1.8  410 18    1 2.2  69 30   1 180   5800 1400 1 17   660 150 1 8.3 350 74 1 480    220 6600   0 .76 38 8.7 1 2.0   52 20    1 910   5700 11000 0 .41 21 5.7 1 910   13000 6700 0 900   4300 12000 0 900   4700 10000 0 560 3900 6900 0
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c 56    7900 400    1 47    670 390   0 780   11000 4300 1 20   690 140 0 8.0 350 72 1 510    1600 5400   0 2.9  45 26   1 7.8   180 84    1 970   7200 13000 0 .60 25 7.8 1 900   9900 9700 0 900   5000 12000 0 900   4600 12000 0 900 10000 8100 0
email_spec4_product18_false-unreach-call_true-termination.cil.c 20    260 190    1 3.0  54 30   0 470   9300 3000 1 21   740 150 1 11   480 99 1 490    220 5600   0 2.0  37 31   1 2.9   40 32    1 900   4900 11000 0 .37 15 4.0 1 910   12000 7000 0 900   3700 12000 0 900   6200 11000 0 500 3900 6300 0
email_spec4_product19_false-unreach-call_true-termination.cil.c 23    280 150    1 3.0  55 33   1 910   11000 6200 0 40   1300 340 0 12   490 110 1 490    200 5500   0 2.6  37 25   1 3.2   41 32    1 930   5700 8600 0 .38 15 4.0 1 900   12000 9000 0 900   4400 13000 0 900   5300 11000 0 510 3800 5500 0
email_spec4_product23_false-unreach-call_true-termination.cil.c 38    430 400    1 4.2  61 51   0 910   11000 6400 0 220   4400 2300 1 12   480 100 1 490    250 5500   0 2.9  44 25   1 4.0   49 37    1 900   5100 11000 0 .37 17 4.2 1 910   11000 9600 0 900   6100 12000 0 900   6000 10000 0 530 3900 6700 0
email_spec4_product24_false-unreach-call_true-termination.cil.c 21    290 280    1 3.1  54 32   0 910   11000 6000 0 41   1500 310 1 12   480 98 1 490    290 5400   0 2.7  39 26   1 3.5   43 34    1 900   4900 11000 0 .38 16 4.9 1 900   13000 7000 0 900   3800 13000 0 900   5500 10000 0 510 3900 5500 0
email_spec4_product25_false-unreach-call_true-termination.cil.c 41    480 360    1 4.5  63 65   0 910   11000 7300 0 900   6100 9900 0 13   480 110 1 490    260 5400   0 2.7  45 33   1 4.3   49 43    1 910   5900 11000 0 .39 17 4.5 1 900   12000 10000 0 900   5000 12000 0 900   5300 12000 0 530 3900 6400 0
email_spec4_product27_false-unreach-call_true-termination.cil.c 40    510 360    1 4.9  64 51   0 910   11000 7100 0 900   8200 7300 0 12   490 120 1 490    210 5500   0 3.0  47 34   1 4.3   52 51    1 900   5300 11000 0 .40 19 4.5 1 900   10000 6600 0 900   3200 11000 0 900   6100 12000 0 540 4000 6300 0
email_spec4_product30_false-unreach-call_true-termination.cil.c 21    280 180    1 3.2  55 33   0 180   6500 1200 1 21   810 170 1 16   620 130 1 490    250 6400   0 2.3  39 23   1 2.9   42 26    1 910   5900 12000 0 .39 16 5.0 1 910   10000 8500 0 900   6400 11000 0 900   4600 10000 0 500 3800 5600 0
email_spec4_product31_false-unreach-call_true-termination.cil.c 22    310 210    1 3.4  56 41   1 910   11000 6100 0 44   1600 340 0 20   840 170 1 490    230 5600   0 2.6  39 23   1 3.3   43 35    1 910   6100 10000 0 .37 17 4.3 1 900   13000 7500 0 900   6400 11000 0 900   5700 12000 0 510 3800 5800 0
email_spec4_product32_false-unreach-call_true-termination.cil.c 42    510 400    1 5.2  67 59   0 910   11000 5600 0 330   4600 4000 1 13   510 110 1 490    240 5400   0 2.7  47 33   1 4.3   53 40    1 910   5800 11000 0 .38 18 4.9 1 900   13000 8400 0 900   3500 12000 0 900   4600 9600 0 530 3900 6000 0
email_spec4_product33_false-unreach-call_true-termination.cil.c 28    330 210    1 3.5  57 36   0 270   7600 1800 1 43   1700 370 1 13   490 120 1 490    150 5600   0 2.7  41 30   1 3.4   45 35    1 900   6100 9800 0 .37 18 4.8 1 900   13000 7100 0 900   4900 11000 0 900   4700 10000 0 520 3800 6200 0
email_spec4_product34_false-unreach-call_true-termination.cil.c 46    580 360    1 6.0  71 90   1 910   11000 5600 0 900   7100 11000 0 17   720 150 1 490    280 5800   0 3.1  48 29   1 4.5   54 54    1 900   5900 12000 0 .39 19 4.7 1 900   13000 7300 0 900   6400 12000 0 900   5400 9900 0 540 3900 5500 0
email_spec4_product35_false-unreach-call_true-termination.cil.c 40    620 330    1 6.4  76 81   0 900   11000 6500 0 900   6200 11000 0 12   480 120 1 490    380 6300   0 3.1  51 41   1 4.9   57 50    1 910   6200 12000 0 .39 20 4.8 1 900   13000 8100 0 900   4000 11000 0 900   5200 12000 0 550 4000 6000 0
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c 130    7600 1300    1 130    640 1300   0 900   11000 5400 0 900   9100 8200 0 17   570 150 1 620    1500 6500   0 9.4  170 96   1 27     210 300    1 930   6500 9900 0 .76 25 11   1 900   12000 6900 0 900   4500 12000 0 900   4600 12000 0 900 4800 9600 0
email_spec6_product12_false-unreach-call_true-termination.cil.c 20    240 210    1 2.6  53 27   0 39   1400 320 1 39   1300 290 1 10   400 87 1 490    160 5400   0 1.8  37 19   1 2.3   38 23    1 900   4400 12000 0 .35 14 4.3 1 900   9200 7700 0 900   6500 12000 0 900   6200 12000 0 500 3800 5200 0
email_spec6_product14_false-unreach-call_true-termination.cil.c 39    410 300    1 3.0  56 39   1 900   7900 9700 0 900   9300 8400 0 9.9 400 80 1 490    170 5400   0 2.2  40 22   1 2.8   45 32    1 900   4400 11000 0 .37 16 4.0 1 900   11000 6300 0 900   6200 12000 0 900   13000 6800 0 500 3900 5400 0
email_spec6_product15_false-unreach-call_true-termination.cil.c 22    260 180    1 2.9  56 31   0 160   5500 1300 1 900   6900 9200 0 10   400 81 1 490    180 5500   0 1.9  39 21   1 2.5   42 19    1 920   6300 11000 0 .36 15 4.2 1 910   13000 6600 0 900   4100 12000 0 900   7000 11000 0 500 3800 5700 0
email_spec6_product16_false-unreach-call_true-termination.cil.c 20    270 210    1 3.1  54 36   0 77   3700 540 1 900   11000 7700 0 11   400 83 1 490    330 5200   0 2.0  39 18   1 2.7   42 26    1 910   6000 12000 0 .36 16 4.6 1 900   9300 7700 0 900   6500 13000 0 900   7000 10000 0 500 3800 5700 0
email_spec6_product20_false-unreach-call_true-termination.cil.c 41    460 390    1 4.5  64 51   0 910   11000 5600 0 900   8900 7800 0 11   400 86 1 490    200 6400   0 2.6  46 25   1 4.4   52 42    1 900   5700 10000 0 .39 17 4.6 1 900   11000 8400 0 900   6200 14000 0 900   9900 9500 0 520 3900 5400 0
email_spec6_product21_false-unreach-call_true-termination.cil.c 39    500 330    1 4.8  66 54   1 910   11000 5900 0 910   8400 9500 0 11   410 93 1 490    340 5000   0 2.4  48 26   1 4.1   54 40    1 960   6400 11000 0 .40 18 4.7 1 900   13000 6500 0 900   6200 15000 0 900   9700 9700 0 530 3900 5800 0
email_spec6_product22_false-unreach-call_true-termination.cil.c 26    300 210    1 3.2  56 35   1 900   11000 6200 0 900   9900 10000 0 10   390 76 1 490    180 6100   0 2.1  41 19   1 3.0   44 36    1 960   6300 12000 0 .37 17 4.6 1 900   13000 5500 0 910   6500 13000 0 900   8700 9500 0 500 3900 5200 0
email_spec6_product26_false-unreach-call_true-termination.cil.c 43    540 390    1 5.3  68 65   0 900   11000 7200 0 900   8900 8800 0 11   420 85 1 490    210 6100   0 2.8  51 28   1 5.1   58 58    1 960   6100 12000 0 .38 18 5.1 1 900   14000 6600 0 900   6000 12000 0 900   10000 8300 0 530 3900 5200 0
email_spec6_product28_false-unreach-call_true-termination.cil.c 19    270 150    1 2.6  53 27   0 62   2200 430 1 39   1400 300 1 10   410 82 1 490    310 5000   0 1.9  38 18   1 2.5   40 26    1 940   6200 12000 0 .39 16 5.2 1 910   13000 7200 0 900   6400 10000 0 900   6000 11000 0 500 3800 5200 0
email_spec6_product29_false-unreach-call_true-termination.cil.c 36    480 330    1 3.5  59 41   0 910   8400 9300 0 910   8700 10000 0 11   410 94 1 490    180 5600   0 2.4  42 24   1 3.0   47 32    1 940   6300 11000 0 .40 18 4.7 1 900   12000 7800 0 900   6000 14000 0 900   6600 10000 0 510 3900 5500 0
email_spec6_product30_false-unreach-call_true-termination.cil.c 24    290 230    1 3.2  58 30