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-05 07:52:24 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 900   3900 13000 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   4200 13000 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 910   4300 11000 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 11000 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 12000 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 960   8100 9500 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 970   9200 9400 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   8900 10000 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 960   10000 9500 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 970   8100 8600 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 970   9600 8900 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 960   8200 9600 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 920   8800 9400 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 970   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 13000 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   3600 12000 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   3600 11000 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   3800 14000 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   3100 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   3900 12000 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   3800 13000 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   3700 11000 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 950   8000 8900 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 940   6500 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 940   6700 11000 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   7300 11000 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 940   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 940   6900 10000 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 930   6300 10000 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 940   7100 11000 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 930   6500 9800 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   6700 11000 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 940   7300 9600 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   6500 10000 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 900   4200 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 14000 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 910   4600 13000 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   6100 11000 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   9000 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 11000 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 11000 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   4100 13000 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   3900 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   4000 11000 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 14000 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   4400 13000 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   4000 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 11000 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   4000 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 11000 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   3400 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 11000 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 960   8600 9600 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   8100 9400 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 960   8400 8800 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   8200 9800 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 9000 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   8300 8700 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 920   8900 10000 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   8400 9500 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 960   9400 10000 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 970   8300 9100 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 960   8700 8100 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 970   8600 9100 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   3800 12000 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   5000 14000 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 910   3800 13000 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 14000 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   3800 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   3400 11000 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 13000 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   3700 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   3100 14000 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 14000 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 11000 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 940   7000 11000 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 940   6900 10000 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 970   7200 9800 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 930   7600 10000 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 940   6800 9800 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 940   6900 9500 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 940   7900 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   7000 10000 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 960   7300 12000 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   4000 11000 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 910   4600 10000 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   4100 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 930   4900 13000 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   4500 10000 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   7000 11000 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 9600 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 12000 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 12000 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 11000 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 9200 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   5400 12000 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   5600 11000 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 910   5900 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   4300 13000 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   4500 10000 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   4500 12000 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   4500 11000 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   4700 9900 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 11000 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 10000 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   5900 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   5000 11000 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 10000 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 11000 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 910   5700 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   4900 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   4800 12000 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 900   5500 11000 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 930   5700 12000 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 910   5900 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 11000 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 900   5600 13000 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   5900 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 930   5900 10000 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 910   6400 10000 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   4500 14000 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 13000 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   4700 13000 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 12000 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 12000 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   4500 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 11000 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 11000 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 900   5200 10000 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   4500 13000 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 12000 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   4700 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 890   8100 10000 1 .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 900   5600 12000 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 910   5600 11000 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 9800 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   5700 10000 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 950   6800 11000 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 940   6200 11000 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 910   6000 9600 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   5600 10000 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   6300 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   5700 11000 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   6000 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 960   5900 11000 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   6000 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   5900 10000 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   6000 12000 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 900   6400 11000 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   4800 12000 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 900   5600 10000 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 9900 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   5000 9800 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 930   5900 9800 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 910   5400 12000 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 900   5800 11000 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   6300 12000 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   5700 10000 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 930   6100 12000 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 910   5800 13000 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 10000 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 910   6900 11000 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 11000 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 14000 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 910   5700 10000 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   6100 9700 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 12000 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 910   6100 12000 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 910   6100 9600 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 910   6200 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 970   6600 10000 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   6100 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   1 180   6500 1300 1 900   7600 8800 0 10   400 81 1 490    170 5200   0 2.1  41 17   1 2.5   44 31    1 910   6200 10000 0 .38 17 4.9 1 910   11000 8100 0 900   6300 12000 0 900   7700 11000 0 510 3800 5700 0
email_spec6_product31_false-unreach-call_true-termination.cil.c 23    310 190    1 3.5  59 32   1 170   5900 1300 1 900   10000 7900 0 11   400 76 1 490    150 5600   0 2.1  41 19   1 3.1   45 42    1 940   6600 10000 0 .39 17 5.1 1 900   11000 7800 0 900   6600 12000 0 900   6000 12000 0 510 3800 5300 0
email_spec6_product32_false-unreach-call_true-termination.cil.c 36    520 330    1 5.4  69 71   0 360   8100 3300 1 900   6900 8900 0 11   410 85 1 490    210 6000   0 2.3  50 24   1 5.7   56 61    1 900   6100 10000 0 .39 18 4.3 1 910   14000 5800 0 900   5900 11000 0 900   7200 12000 0 530 3900 6000 0
email_spec6_product33_false-unreach-call_true-termination.cil.c 25    340 170    1 3.5  58 39   0 910   11000 5000 0 900   6400 10000 0 11   410 92 1 490    290 5000   0 1.8  43 23   1 3.1   46 31    1 910   7300 10000 0 .38 18 5.2 1 900   13000 8700 0 900   6300 13000 0 900   7900 11000 0 510 3900 5800 0
email_spec6_product34_false-unreach-call_true-termination.cil.c 39    600 510    1 6.3  75 73   0 340   7800 2500 1 900   11000 10000 0 11   410 100 1 490    300 5500   0 2.6  52 24   1 4.2   58 65    1 910   6600 10000 0 .40 20 4.7 1 900   14000 6300 0 900   5900 15000 0 900   7000 9200 0 540 3900 5400 0
email_spec6_product35_false-unreach-call_true-termination.cil.c 45    640 390    1 6.7  77 73   0 910   11000 4800 0 910   9500 7800 0 11   420 81 1 500    390 4900   0 2.9  55 28   1 5.9   63 67    1 910   6900 9500 0 .42 21 4.2 1 910   13000 6900 0 900   6100 12000 0 900   6100 11000 0 560 4000 5800 0
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c 140    7800 1200    1 120    650 1500   0 900   8100 9000 0 910   11000 8400 0 15   610 130 1 630    1600 5700   0 9.1  180 110   1 30     220 330    1 970   7900 10000 0 .53 25 6.1 1 900   11000 8200 0 900   6300 13000 0 910   14000 5000 0 900 4600 11000 0
email_spec7_product28_false-unreach-call_true-termination.cil.c 19    250 170    1 2.6  54 37   0 52   2300 390 1 390   5200 4400 1 11   480 100 1 490    260 5500   0 1.9  37 18   1 2.3   38 22    1 900   4800 10000 0 .36 15 4.2 1 900   13000 5800 0 900   4800 12000 0 910   9400 9800 0 500 3800 5100 0
email_spec7_product29_false-unreach-call_true-termination.cil.c 33    450 270    1 3.3  57 36   0 910   7600 9400 0 70   2600 610 1 11   450 90 1 490    390 5400   0 2.2  40 21   1 3.2   43 30    1 900   4800 12000 0 .39 17 5.3 1 910   14000 6600 0 900   4300 14000 0 900   6500 10000 0 500 3900 5700 0
email_spec7_product30_false-unreach-call_true-termination.cil.c 21    280 180    1 3.2  56 35   0 120   5200 1000 1 900   7200 9200 0 11   400 85 1 490    240 5300   0 1.7  38 23   1 2.4   42 23    1 900   5000 12000 0 .39 16 4.4 1 910   14000 6000 0 900   4900 14000 0 900   7300 9700 0 500 3800 5400 0
email_spec7_product31_false-unreach-call_true-termination.cil.c 19    300 230    1 3.4  57 37   0 160   5600 1100 1 900   7700 11000 0 10   400 77 1 490    280 5600   0 1.9  39 18   1 2.7   42 30    1 900   5700 11000 0 .39 17 4.3 1 900   13000 6200 0 900   6200 15000 0 900   6800 10000 0 510 3800 6700 0
email_spec7_product32_false-unreach-call_true-termination.cil.c 42    500 530    1 5.1  67 76   0 900   11000 5900 0 900   8500 8900 0 11   410 81 1 490    420 5400   0 2.5  47 23   1 4.1   53 43    1 900   5100 11000 0 .38 18 4.9 1 910   13000 6400 0 900   5000 12000 0 900   6100 11000 0 530 3900 6000 0
email_spec7_product33_false-unreach-call_true-termination.cil.c 25    330 190    1 3.5  57 41   0 900   11000 4900 0 900   10000 8300 0 11   400 84 1 490    180 5100   0 2.2  40 19   1 2.6   44 28    1 900   5700 12000 0 .40 18 4.3 1 910   13000 7500 0 900   4800 11000 0 900   6800 11000 0 510 3900 5400 0
email_spec7_product34_false-unreach-call_true-termination.cil.c 41    570 320    1 6.0  72 78   1 180   6300 1300 1 900   6100 9700 0 11   410 93 1 490    320 5700   0 2.5  49 21   1 5.1   55 56    1 900   5800 11000 0 .38 19 5.1 1 910   14000 6500 0 900   6200 12000 0 900   5900 9800 0 550 3900 5900 0
email_spec7_product35_false-unreach-call_true-termination.cil.c 40    610 500    1 6.3  75 92   0 900   11000 5600 0 900   10000 8500 0 11   410 94 1 490    230 5100   0 2.6  52 21   1 5.0   58 51    1 900   5700 10000 0 .41 20 4.9 1 910   13000 6700 0 900   6200 12000 0 900   5700 10000 0 550 3900 6800 0
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c 150    7700 1100    1 150    740 1200   0 900   8800 11000 0 900   6600 12000 0 34   1600 300 1 640    1600 6300   0 8.7  190 91   1 31     240 330    1 920   5700 11000 0 .56 25 6.1 1 900   12000 6000 0 900   6200 10000 0 900   5600 9900 0 900 9100 9700 0
email_spec8_product15_false-unreach-call_true-termination.cil.c 20    250 160    1 2.9  53 32   0 910   8100 9600 0 130   4700 1000 0 11   430 92 1 490    250 5200   0 2.4  38 21   1 3.3   41 29    1 900   5600 11000 0 .46 16 6.2 1 900   13000 8400 0 900   6900 11000 0 900   7600 11000 0 510 3800 6300 0
email_spec8_product16_false-unreach-call_true-termination.cil.c 21    270 220    1 3.0  55 34   0 900   8200 7900 0 92   4200 760 0 13   490 98 1 490    210 5300   0 2.9  39 27   1 3.4   42 32    1 900   5700 10000 0 .40 15 4.7 1 900   11000 8100 0 900   6500 11000 0 900   5800 13000 0 500 3800 5600 0
email_spec8_product20_false-unreach-call_true-termination.cil.c 43    450 390    1 4.2  61 49   0 350   8500 2900 1 900   8100 8700 0 13   490 120 1 490    250 5500   0 3.2  46 28   1 4.6   51 49    1 910   6100 11000 0 .48 17 5.5 1 900   12000 7200 0 900   6500 14000 0 900   8300 10000 0 520 3900 6200 0
email_spec8_product21_false-unreach-call_true-termination.cil.c 40    490 340    1 4.7  64 52   0 900   11000 5800 0 900   7600 10000 0 17   740 130 1 490    320 5200   0 3.5  47 33   1 6.1   52 66    1 910   5900 11000 0 .44 18 4.7 1 900   13000 7300 0 900   6400 12000 0 900   9600 8600 0 520 3900 6100 0
email_spec8_product22_false-unreach-call_true-termination.cil.c 23    290 270    1 3.1  55 36   0 900   8800 9800 0 340   5900 3200 0 13   490 110 1 490    230 4700   0 3.0  40 35   1 4.0   44 36    1 910   6000 11000 0 .45 16 5.8 1 900   11000 7800 0 900   6900 11000 0 900   5900 11000 0 510 3800 6200 0
email_spec8_product26_false-unreach-call_true-termination.cil.c 42    530 420    1 5.0  65 54   0 900   11000 6000 0 910   11000 8100 0 13   500 110 1 490    230 6700   0 3.3  51 31   1 5.8   57 44    1 950   6700 10000 0 .48 18 6.5 1 900   13000 7300 0 900   6500 14000 0 900   5400 10000 0 530 4000 6700 0
email_spec8_product30_false-unreach-call_true-termination.cil.c 21    280 200    1 3.2  56 34   0 900   7800 9700 0 150   4500 1300 0 16   640 160 1 490    170 4500   0 2.6  40 26   1 3.6   44 36    1 950   7500 9700 0 .51 17 5.7 1 900   13000 7600 0 900   6600 11000 0 900   5400 11000 0 500 3800 5200 0
email_spec8_product31_false-unreach-call_true-termination.cil.c 19    310 190    1 3.4  58 41   0 230   6900 1500 1 100   4100 860 0 20   830 190 1 490    250 5800   0 2.8  41 27   1 3.6   44 43    1 970   9200 8600 0 .43 17 5.2 1 910   13000 7600 0 900   6900 14000 0 900   6700 11000 0 510 3800 5700 0
email_spec8_product32_false-unreach-call_true-termination.cil.c 39    510 410    1 5.3  68 51   0 900   8100 10000 0 900   9700 8800 0 17   750 150 1 490    280 5800   0 3.2  49 30   1 4.8   55 46    1 910   8700 9800 0 .50 19 5.9 1 910   13000 7200 0 900   6600 10000 0 900   12000 8400 0 530 3900 6700 0
email_spec8_product33_false-unreach-call_true-termination.cil.c 25    330 200    1 3.5  55 38   0 250   7800 1800 1 590   7600 5600 0 18   810 150 1 490    160 5200   0 3.1  43 28   1 3.9   46 49    1 970   9500 9300 0 .47 18 6.4 1 910   14000 6500 0 900   6600 11000 0 900   5600 11000 0 510 3800 5800 0
email_spec8_product34_false-unreach-call_true-termination.cil.c 40    580 350    1 6.1  72 68   0 910   11000 6700 0 900   8600 9400 0 17   780 160 1 490    250 4800   0 3.2  51 40   1 6.5   57 74    1 920   9100 9700 0 .46 19 5.8 1 910   13000 7200 0 900   6700 11000 0 900   8900 11000 0 540 3900 6100 0
email_spec8_product35_false-unreach-call_true-termination.cil.c 46    630 380    1 6.4  75 90   0 900   11000 4700 0 900   10000 7200 0 15   560 130 1 500    330 6100   0 3.4  54 35   1 6.0   62 66    1 960   9500 10000 0 .49 20 5.0 1 900   12000 8000 0 900   6000 11000 0 900   11000 8600 0 560 4000 7200 0
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c 150    7700 1200    1 130    640 1200   0 900   9600 8300 0 900   10000 8700 0 17   720 150 1 630    1500 6600   0 10    180 110   1 31     220 340    1 960   8400 10000 0 1.6  50 20   1 900   13000 6600 0 900   6200 12000 0 900   5800 11000 0 900 4500 7300 0
email_spec9_product15_false-unreach-call_true-termination.cil.c 20    260 180    1 2.8  53 36   0 900   8000 9200 0 130   4700 1100 0 11   440 91 1 490    240 5600   0 2.7  38 24   1 3.2   42 32    1 900   5600 11000 0 .46 16 5.8 1 910   11000 7800 0 900   6400 12000 0 900   7700 13000 0 500 3800 5800 0
email_spec9_product16_false-unreach-call_true-termination.cil.c 18    270 150    1 3.0  54 31   0 900   8300 8100 0 98   4200 730 0 13   490 120 1 490    190 5000   0 3.1  39 27   1 3.5   42 38    1 930   5900 11000 0 .43 16 5.2 1 900   12000 7600 0 900   6700 13000 0 900   5800 13000 0 500 3800 6200 0
email_spec9_product20_false-unreach-call_true-termination.cil.c 40    440 300    1 4.2  62 44   0 470   9100 3100 1 900   8100 9400 0 13   480 97 1 490    300 5700   0 3.1  46 28   1 4.7   51 49    1 900   5900 11000 0 .52 17 6.4 1 900   11000 7300 0 900   6400 12000 0 900   7900 11000 0 520 3900 5500 0
email_spec9_product21_false-unreach-call_true-termination.cil.c 36    490 420    1 4.6  63 63   0 910   11000 5900 0 900   7500 9100 0 17   810 170 1 490    260 5600   0 3.2  47 31   1 6.1   52 60    1 910   5800 12000 0 .43 17 5.2 1 900   11000 8500 0 900   6400 13000 0 900   8700 9500 0 520 3900 5700 0
email_spec9_product22_false-unreach-call_true-termination.cil.c 25    300 270    1 3.0  55 43   0 910   8500 9100 0 350   5900 3100 0 11   460 87 1 490    330 5400   0 3.3  40 27   1 3.7   43 37    1 910   6000 11000 0 .43 16 5.2 1 900   11000 8900 0 900   6400 12000 0 900   5900 11000 0 510 3900 5600 0
email_spec9_product26_false-unreach-call_true-termination.cil.c 40    520 320    1 5.0  64 56   0 910   11000 5500 0 910   11000 9700 0 15   530 130 1 490    260 5500   0 3.3  51 38   1 5.6   57 57    1 930   7000 10000 0 .45 18 5.5 1 900   10000 7200 0 900   6800 11000 0 900   9700 8700 0 530 4000 6000 0
email_spec9_product30_false-unreach-call_true-termination.cil.c 19    280 150    1 3.2  55 35   0 910   7900 9400 0 140   4500 1200 0 20   840 190 1 490    450 5400   0 2.4  40 25   1 3.2   44 42    1 950   7900 9700 0 .48 17 6.2 1 910   13000 7600 0 900   6600 12000 0 900   7300 11000 0 500 3800 5800 0
email_spec9_product31_false-unreach-call_true-termination.cil.c 19    310 210    1 3.5  55 43   0 230   7400 1600 1 100   4100 830 0 22   910 240 1 490    190 5800   0 2.7  41 27   1 3.7   44 36    1 970   9400 10000 0 .42 17 5.8 1 910   14000 6500 0 900   6800 11000 0 900   7200 12000 0 510 3800 5800 0
email_spec9_product32_false-unreach-call_true-termination.cil.c 43    510 380    1 5.2  67 65   0 900   8000 9700 0 900   9700 7800 0 14   550 120 1 490    190 6200   0 3.0  49 30   1 4.8   55 54    1 960   9600 9900 0 .50 18 6.3 1 900   13000 7000 0 900   6200 13000 0 900   8100 11000 0 530 3900 6000 0
email_spec9_product33_false-unreach-call_true-termination.cil.c 27    330 200    1 3.5  57 42   0 250   7800 1700 1 600   7600 6300 0 17   780 150 1 490    250 5300   0 3.1  42 34   1 4.2   46 41    1 970   9700 11000 0 .45 18 6.0 1 910   13000 7100 0 900   6900 11000 0 900   6000 9700 0 520 3900 5700 0
email_spec9_product34_false-unreach-call_true-termination.cil.c 37    580 330    1 6.1  72 78   0 910   11000 6200 0 900   7800 9600 0 16   630 150 1 490    230 6000   0 3.7  51 34   1 6.4   57 76    1 940   8700 8800 0 .46 19 5.1 1 900   12000 7300 0 900   6800 10000 0 900   4600 12000 0 540 3900 6500 0
email_spec9_product35_false-unreach-call_true-termination.cil.c 45    620 430    1 6.5  75 78   0 910   11000 5400 0 900   8900 8600 0 17   570 140 1 500    200 5300   0 3.4  54 34   1 5.8   62 75    1 940   9800 10000 0 .47 20 5.3 1 900   12000 7500 0 900   6900 13000 0 900   5100 11000 0 550 4000 5600 0
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c 140    7700 1000    1 130    640 1100   0 900   9800 8800 0 900   10000 8400 0 21   900 190 1 620    1600 5600   0 9.6  180 90   1 29     220 400    1 970   8400 8400 0 1.6  50 19   1 900   13000 5900 0 900   6100 12000 0 900   4600 10000 0 900 4500 8100 0
email_spec0_product05_true-unreach-call_true-termination.cil.c .45 54 3.7  2 2.7  42 28   2 6.1 300 47 2 3.9 280 36 2 31   790 310 2 520    630 5700   2 .58 32 8.2 2 .38  32 4.7  2 31   1500 260 2 .26 13 3.1 2 8.4 400 70 2 8.9 420 71 2 8.3 400 72 2 330 1800 3900 2
email_spec0_product09_true-unreach-call_true-termination.cil.c .66 120 5.9  2 3.5  42 39   2 7.2 340 57 2 4.5 280 43 2 30   1400 310 2 520    1500 5600   2 1.0  36 14   2 .72  36 8.7  2 260   6100 2700 2 .28 13 3.5 2 9.6 430 71 2 10   510 74 2 9.1 440 75 2 340 2500 3100 1
email_spec0_product10_true-unreach-call_true-termination.cil.c .46 62 4.1  2 2.8  42 30   2 6.3 320 60 2 5.3 290 45 2 32   1300 340 2 520    910 5400   2 .70 34 8.5 2 .44  34 5.3  2 45   2700 360 2 .29 13 3.3 2 9.2 440 74 2 9.2 440 80 2 9.4 430 75 2 330 1800 3600 2
email_spec0_product11_true-unreach-call_true-termination.cil.c .58 98 5.1  2 3.3  44 34   2 7.3 340 58 2 4.0 280 33 2 31   1600 250 2 520    1600 5600   2 .97 35 13   2 .54  35 5.7  2 52   3700 470 2 .30 13 3.8 2 10   550 86 2 11   500 88 2 11   560 86 2 350 3800 3600 2
email_spec0_product19_true-unreach-call_true-termination.cil.c .74 130 6.9  2 3.8  45 38   2 8.1 460 61 2 4.0 280 38 2 40   2400 380 2 520    2700 6600   2 1.0  36 12   2 .61  36 7.6  2 970   8500 8700 0 .29 13 3.6 2 16   760 120 2 13   520 88 2 900   6200 11000 0 360 3800 4400 2
email_spec0_product24_true-unreach-call_true-termination.cil.c .76 150 7.3  2 3.8  46 43   2 8.5 450 77 2 5.4 290 52 2 45   2800 510 2 530    2700 6600   2 1.2  38 15   2 .71  38 8.4  2 970   7900 11000 0 .29 13 4.0 2 26   880 210 2 13   510 90 2 900   6700 11000 0 360 3800 4400 2
email_spec0_product25_true-unreach-call_true-termination.cil.c 1.2  260 12    2 5.6  45 59   2 8.8 450 66 2 4.6 280 44 2 46   2800 530 2 530    2800 6700   2 1.8  44 19   2 1.1   42 14    2 970   8300 10000 0 .32 13 3.6 2 18   730 140 2 14   520 110 2 900   5900 12000 0 370 3900 4100 2
email_spec0_product27_true-unreach-call_true-termination.cil.c 1.3  290 12    2 6.0  47 63   2 9.4 470 69 2 6.2 320 61 2 52   2900 510 2 530    2900 5800   2 2.0  47 25   2 1.3   46 16    2 970   7600 10000 0 .32 13 3.5 2 30   980 220 2 13   510 99 2 900   5400 10000 0 370 3900 4100 2
email_spec0_product36_true-unreach-call_true-termination.cil.c .80 150 7.3  2 4.0  44 46   2 7.3 360 61 2 6.3 330 45 2 32   1500 340 2 520    1500 5100   2 1.3  38 17   2 .86  37 9.9  2 760   11000 7800 2 .29 13 3.4 2 9.9 490 70 2 10   510 78 2 10   500 82 2 340 2400 4400 2
email_spec0_product37_true-unreach-call_true-termination.cil.c .62 110 5.5  2 3.4  44 34   2 7.6 370 69 2 5.5 290 46 2 35   1700 350 2 520    1800 6100   2 1.0  36 13   2 .63  37 8.3  2 81   4200 860 2 .31 13 3.4 2 20   820 170 2 11   520 79 2 18   720 140 2 350 3900 4400 2
email_spec0_product38_true-unreach-call_true-termination.cil.c .88 170 8.5  2 4.3  47 45   2 7.9 380 63 2 4.8 310 47 2 36   1700 380 2 520    2000 6100   2 1.4  40 21   2 .89  38 9.8  2 810   12000 7600 2 .28 13 3.4 2 11   560 79 2 13   530 100 2 11   610 89 2 360 3900 3900 2
email_spec0_product40_true-unreach-call_true-termination.cil.c .96 200 9.6  2 4.6  45 62   2 8.0 410 66 2 6.5 330 57 2 40   2400 470 2 520    2700 5500   2 1.6  43 20   2 1.0   41 14    2 970   8800 11000 0 .31 13 3.8 2 24   840 200 2 12   530 92 2 22   810 170 2 360 3900 4200 2
email_spec11_product03_true-unreach-call_true-termination.cil.c .42 49 3.5  2 2.5  42 24   2 6.5 300 50 2 5.1 300 52 2 30   780 330 2 520    510 5400   2 .56 32 6.8 2 .38  32 3.7  2 23   840 180 2 .26 13 3.2 2 9.7 490 82 2 8.0 400 56 2 9.7 520 75 2 330 1800 4300 2
email_spec11_product07_true-unreach-call_true-termination.cil.c .60 110 6.3  2 3.4  42 40   2 6.8 340 63 2 6.0 300 50 2 30   1400 340 2 510    1400 5400   2 .96 36 11   2 .65  35 8.0  2 77   4200 810 2 .26 13 3.6 2 9.5 430 72 2 9.8 520 79 2 9.7 410 72 2 340 2500 3900 2
email_spec11_product08_true-unreach-call_true-termination.cil.c .59 90 5.3  2 3.3  46 35   2 7.0 340 56 2 5.4 290 49 2 31   1500 310 2 510    1600 5500   2 .92 35 12   2 .51  35 6.6  2 36   2000 300 2 .28 13 3.2 2 12   580 100 2 11   500 94 2 13   610 99 2 350 3800 4000 2
email_spec11_product10_true-unreach-call_true-termination.cil.c .49 63 3.8  2 2.7  43 34   2 6.4 310 55 2 5.3 300 48 2 33   1300 360 2 520    850 5500   2 .68 34 8.5 2 .48  34 4.7  2 45   3100 370 2 .27 13 3.9 2 8.9 400 76 2 9.0 430 64 2 8.7 400 68 2 330 1800 3500 2
email_spec11_product18_true-unreach-call_true-termination.cil.c .71 120 6.8  2 3.6  46 42   2 8.2 460 65 2 5.2 290 54 2 40   2100 430 2 520    2400 5800   2 1.1  36 15   2 .63  36 7.4  2 960   12000 8500 0 .28 13 3.4 2 19   780 140 2 12   520 97 2 900   5800 11000 0 360 3800 3600 2
email_spec11_product23_true-unreach-call_true-termination.cil.c 1.0  220 13    2 5.0  45 57   2 9.6 460 75 2 6.1 310 49 2 44   2800 450 2 530    2700 5700   2 1.7  43 23   2 1.0   41 12    2 970   8300 9700 0 .29 13 3.7 2 20   800 150 2 13   520 94 2 900   6000 9400 0 370 3900 4100 2
email_spec11_product24_true-unreach-call_true-termination.cil.c .78 150 6.4  2 3.9  45 38   2 8.8 460 72 2 5.3 290 49 2 45   2800 460 2 520    2800 5800   2 1.2  38 14   2 .71  37 8.4  2 970   8800 11000 0 .29 13 3.5 2 19   730 130 2 13   510 100 2 900   6000 11000 0 360 3800 3900 2
email_spec11_product27_true-unreach-call_true-termination.cil.c 1.2  300 12    2 6.0  45 68   2 9.1 450 74 2 6.4 320 58 2 53   2900 490 2 530    2900 6100   2 1.9  47 21   2 1.3   45 16    2 960   8500 12000 0 .32 13 3.5 2 19   810 150 2 14   550 99 2 900   5800 12000 0 370 4000 4000 2
email_spec11_product36_true-unreach-call_true-termination.cil.c .79 150 6.6  2 3.9  42 53   2 7.1 350 59 2 6.4 310 52 2 32   1500 370 2 520    1500 6100   2 1.2  38 16   2 .83  37 10    2 960   15000 8600 0 .27 13 3.5 2 9.7 470 68 2 10   510 84 2 10   490 88 2 340 2400 3700 2
email_spec11_product37_true-unreach-call_true-termination.cil.c .66 110 6.6  2 3.5  45 42   2 7.2 350 56 2 5.4 290 50 2 35   1700 370 2 520    1800 6800   2 1.1  36 14   2 .65  36 9.0  2 87   4400 870 2 .30 13 3.7 2 14   700 100 2 11   510 86 2 13   620 100 2 360 3900 3900 2
email_spec11_product39_true-unreach-call_true-termination.cil.c .85 160 7.7  2 4.1  45 43   2 7.8 380 65 2 6.1 300 52 2 35   1600 340 2 520    1900 5700   2 1.3  39 19   2 .84  38 9.8  2 190   5400 1900 2 .29 14 3.8 2 13   640 110 2 11   510 88 2 14   690 110 2 360 3900 4300 2
email_spec11_product40_true-unreach-call_true-termination.cil.c .96 200 11    2 4.7  45 52   2 7.6 370 65 2 6.0 310 50 2 40   2400 420 2 520    2700 6500   2 1.6  44 20   2 1.1   41 13    2 970   9100 9800 0 .31 13 3.5 2 13   680 110 2 12   510 99 2 13   570 97 2 360 4000 3900 2
email_spec1_product12_true-unreach-call_true-termination.cil.c .65 100 5.8  2 3.2  46 34   1 12   500 100 2 6.9 390 61 2 34   1600 340 2 520    1600 5600   2 .86 34 11   2 .48  34 6.4  2 970   7900 11000 0 3.6  44 45   2 900   13000 8200 0 900   6600 11000 0 900   5400 11000 0 370 3800 4200 1
email_spec1_product28_true-unreach-call_true-termination.cil.c .72 130 6.3  2 3.4  45 31   1 17   900 130 2 7.5 390 59 2 41   2400 450 2 520    2500 6500   2 .93 35 9.9 2 .52  35 5.9  2 940   6500 12000 0 3.9  51 38   2 900   11000 7100 0 900   6900 13000 0 900   6000 12000 0 370 3800 3800 2
email_spec27_product13_true-unreach-call_true-termination.cil.c .67 110 6.2  2 3.4  52 30   1 270   7400 1900 2 98   4200 900 2 36   1700 360 2 520    1800 6000   2 .96 35 11   2 .50  34 6.6  2 900   4400 11000 0 3.8  50 45   2 910   13000 7000 0 900   3600 13000 0 900   6600 8400 0 370 3800 4500 2
email_spec27_product28_true-unreach-call_true-termination.cil.c .75 140 7.1  2 3.5  53 34   1 110   5200 840 2 900   5800 11000 0 41   2400 450 2 520    2600 6000   2 1.0  35 12   2 .56  35 6.6  2 900   4400 10000 0 4.2  60 48   2 910   13000 7100 0 900   4100 13000 0 900   5600 12000 0 380 3800 4500 2
email_spec4_product13_true-unreach-call_true-termination.cil.c .65 110 5.7  2 3.3  50 38   2 12   490 99 2 6.5 370 54 2 36   1700 350 2 520    1800 5700   2 .92 34 12   2 .48  34 5.7  2 900   4700 12000 0 3.2  36 37   2 830   7200 12000 2 900   6600 12000 0 900   5200 10000 0 370 3800 4000 2
email_spec4_product17_true-unreach-call_true-termination.cil.c .95 200 9.9  2 3.8  53 43   1 420   8600 3600 2 27   870 200 2 40   2600 390 2 520    2700 6600   2 1.1  38 13   2 .70  38 8.0  2 900   4800 10000 0 3.3  42 43   2 900   9500 8500 0 900   3600 12000 0 900   5900 11000 0 390 3900 4200 1
email_spec4_product28_true-unreach-call_true-termination.cil.c .73 130 7.7  2 3.4  50 45   2 48   2100 340 2 7.1 390 55 2 42   2500 480 2 520    2700 5600   2 .95 35 11   2 .51  35 6.1  2 910   5900 12000 0 3.2  37 41   2 110   4400 1200 2 900   4500 11000 0 900   4500 11000 0 370 3800 3900 2
email_spec4_product29_true-unreach-call_true-termination.cil.c 1.1  270 16    2 4.4  55 48   1 900   11000 5400 0 26   850 210 2 48   2800 460 2 530    2800 6900   2 1.3  41 16   2 .78  39 11    2 900   5700 11000 0 3.4  42 38   2 900   8300 11000 0 900   4800 13000 0 900   6100 11000 0 390 3900 4900 2
email_spec7_product13_true-unreach-call_true-termination.cil.c .63 100 5.8  2 3.1  44 40   2 7.8 360 66 2 3.4 270 35 2 35   1600 340 2 520    1700 5700   2 .84 34 9.1 2 .45  34 5.7  2 940   6800 8800 0 .29 13 4.3 2 11   570 81 2 11   520 100 2 10   560 87 2 350 3800 3800 2
email_spec7_product17_true-unreach-call_true-termination.cil.c .88 180 9.4  2 3.6  45 41   2 8.4 400 65 2 3.8 280 40 2 39   2300 420 2 520    2600 6000   2 1.1  37 14   2 .60  37 9.1  2 970   6400 9900 0 .31 13 3.5 2 12   570 94 2 13   530 99 2 11   580 98 2 360 3900 4100 2
email_spec7_product18_true-unreach-call_true-termination.cil.c .66 120 6.6  2 3.6  47 34   2 8.0 360 71 2 5.3 290 47 2 40   2300 390 2 520    2500 5900   2 .98 35 12   2 .60  34 7.0  2 420   8600 3700 2 .31 13 3.3 2 13   590 100 2 11   510 99 2 13   600 97 2 360 3800 3900 2
email_spec7_product19_true-unreach-call_true-termination.cil.c .75 130 7.3  2 3.7  45 40   2 7.5 370 65 2 4.1 280 40 2 40   2600 360 2 520    2700 6500   2 1.1  35 15   2 .59  34 7.3  2 970   8700 10000 0 .28 13 3.5 2 11   570 80 2 11   520 82 2 12   560 82 2 360 3800 3800 2
email_spec7_product23_true-unreach-call_true-termination.cil.c 1.1  210 10    2 5.0  45 54   2 8.2 400 64 2 5.9 290 56 2 46   2800 490 2 530    2800 5600   2 1.5  42 18   2 .96  40 11    2 970   8900 9600 0 .32 13 3.7 2 14   600 110 2 12   530 100 2 14   610 110 2 360 3900 3700 2
email_spec7_product24_true-unreach-call_true-termination.cil.c .75 140 7.5  2 4.0  45 42   2 7.7 370 69 2 5.3 290 46 2 47   2800 480 2 530    2800 5400   2 1.1  37 13   2 .66  36 8.5  2 960   8900 10000 0 .29 13 3.6 2 12   580 93 2 12   520 100 2 14   650 110 2 360 3800 3900 2
email_spec7_product25_true-unreach-call_true-termination.cil.c 1.1  260 11    2 5.4  47 75   2 8.6 420 70 2 4.7 290 40 2 47   2800 530 2 530    2800 6000   2 1.6  43 23   2 1.1   40 13    2 970   8900 10000 0 .29 13 3.5 2 13   600 110 2 12   520 100 2 12   570 95 2 370 3900 3900 2
email_spec7_product27_true-unreach-call_true-termination.cil.c 1.2  290 13    2 6.0  50 70   2 8.8 420 74 2 6.3 300 53 2 54   2900 620 2 530    2900 6400   2 1.9  45 23   2 1.2   43 14    2 970   8600 9500 0 .29 13 4.3 2 14   640 110 2 13   520 99 2 14   650 110 2 370 4000 5000 2
email_spec8_product12_true-unreach-call_true-termination.cil.c .60 110 6.0  2 3.1  45 31   2 12   520 100 2 7.0 390 60 2 34   1600 320 2 520    1600 5200   2 1.0  36 12   2 .55  35 6.7  2 960   7800 11000 0 3.6  45 44   2 610   6600 7800 2 900   6600 11000 0 900   5500 10000 0 370 3800 4800 2
email_spec8_product14_true-unreach-call_true-termination.cil.c 39    480 320    2 4.0  55 42   1 900   7500 8900 0 900   7400 8900 0 38   2100 380 2 530    2400 5500   2 1.4  40 19   2 2.2   44 27    2 920   5800 11000 0 4.0  55 48   2 910   13000 6900 0 900   6100 14000 0 900   5400 11000 0 390 3900 5000 1
email_spec8_product28_true-unreach-call_true-termination.cil.c .80 140 6.8  2 3.4  45 27   1 17   890 160 2 7.3 390 57 2 40   2500 430 2 520    2700 6800   2 1.1  37 13   2 .55  36 7.2  2 940   8300 9500 0 3.9  51 55   2 900   8800 9900 0 900   6700 12000 0 900   7000 9800 0 380 3800 3700 2
email_spec8_product29_true-unreach-call_true-termination.cil.c 36    550 330    2 4.4  57 44   1 900   10000 7900 0 900   7900 9300 0 48   2800 570 2 540    2800 7100   2 1.5  42 21   2 2.5   46 31    2 920   7300 9400 0 4.4  62 60   2 900   13000 7600 0 900   6700 10000 0 900   9600 9500 0 400 3900 4200 2
email_spec9_product12_true-unreach-call_true-termination.cil.c .63 110 6.0  2 3.1  45 35   2 12   550 91 2 7.7 400 61 2 34   1600 350 2 110    1600 1300   2 1.0  36 14   2 .51  36 6.3  2 960   7400 10000 0 3.6  44 41   2 620   6500 9000 2 900   7000 11000 0 900   6500 12000 0 370 3800 4000 2
email_spec9_product14_true-unreach-call_true-termination.cil.c 32    480 260    2 4.0  55 42   1 900   8100 9900 0 900   7200 9200 0 38   2100 360 2 530    2400 5200   2 1.4  40 17   2 2.2   44 28    2 940   5700 11000 0 4.0  54 51   2 900   11000 7800 0 900   6900 11000 0 900   12000 8800 0 390 3900 4700 1
email_spec9_product28_true-unreach-call_true-termination.cil.c .72 140 7.6  2 3.4  45 36   1 20   850 140 2 7.2 400 58 2 41   2400 400 2 520    2600 6400   2 1.1  37 13   2 .55  37 6.0  2 930   9100 9600 0 4.0  51 50   2 900   13000 6300 0 900   6600 13000 0 910   13000 7700 0 370 3800 3800 2
email_spec9_product29_true-unreach-call_true-termination.cil.c 38    550 290    2 4.5  57 56   1 900   10000 8200 0 910   8400 9400 0 48   2800 560 2 540    2800 6400   2 1.6  42 18   2 2.5   46 31    2 920   7300 10000 0 4.4  61 47   2 900   13000 6500 0 900   6500 11000 0 900   4500 11000 0 400 3900 4000 2
minepump_spec1_product33_false-unreach-call_false-termination.cil.c .16 27 1.3  1 .29 35 2.4 1 5.5 310 50 1 5.2 300 44 1 4.2 280 37 1 .56 77 6.2 1 .42 30 5.1 1 .81  30 6.5  1 5.7 300 50 1 .23 11 2.4 1 9.9 530 83 1 6.2 310 49 1 9.7 550 79 1 900 870 9700 0
minepump_spec1_product34_false-unreach-call_false-termination.cil.c .18 27 1.3  1 .31 35 2.7 1 5.5 310 53 1 5.0 300 45 1 4.2 270 35 1 .57 77 6.7 1 .51 30 4.7 1 .69  30 11    1 5.7 300 49 1 .23 11 2.4 1 10   540 83 1 6.5 320 52 1 10   530 86 1 900 900 7100 0
minepump_spec1_product35_false-unreach-call_false-termination.cil.c .16 27 1.5  1 .32 36 3.0 1 5.7 310 51 1 5.1 300 45 1 4.1 270 36 1 .70 78 7.9 1 .55 30 3.8 1 .60  30 4.3  1 5.6 300 48 1 .22 12 2.9 1 9.5 540 80 1 7.2 340 51 1 10   550 85 1 900 980 8800 0
minepump_spec1_product36_false-unreach-call_false-termination.cil.c .16 27 1.4  1 .31 35 2.8 1 5.6 310 47 1 5.0 300 42 1 4.2 280 33 1 .75 78 11   1 .50 30 4.3 1 .53  30 5.3  1 5.6 300 44 1 .22 12 2.9 1 9.8 530 89 1 6.8 370 56 1 10   530 76 1 900 1000 11000 0
minepump_spec1_product37_false-unreach-call_false-termination.cil.c .17 28 1.2  1 .34 36 3.1 1 5.7 310 43 1 5.0 290 46 1 4.2 280 38 1 .67 78 7.9 1 .47 30 3.7 1 .49  30 4.3  1 5.7 300 53 1 .20 11 2.7 1 10   530 81 1 7.1 340 58 1 10   550 79 1 900 870 8700 0
minepump_spec1_product38_false-unreach-call_false-termination.cil.c .18 28 1.3  1 .34 36 3.7 1 5.8 330 49 1 5.3 300 44 1 4.3 280 36 1 .67 79 7.4 1 .41 30 5.6 1 .46  30 5.7  1 5.8 300 47 1 .21 11 2.5 1 11   550 97 1 7.3 350 50 1 10   520 85 1 900 880 8900 0
minepump_spec1_product39_false-unreach-call_false-termination.cil.c .18 28 1.5  1 .32 36 3.5 1 5.7 330 50 1 5.3 300 52 1 4.3 280 35 1 .83 79 9.8 1 .50 30 4.2 1 .51  30 4.2  1 5.9 300 48 1 .21 11 2.5 1 9.9 530 79 1 7.5 410 53 1 10   530 71 1 900 930 8600 0
minepump_spec1_product40_false-unreach-call_false-termination.cil.c .20 28 1.4  1 .34 38 3.1 1 5.6 330 45 1 5.5 300 45 1 4.5 280 41 1 .78 79 11   1 .49 30 4.5 1 .55  30 4.6  1 6.3 300 50 1 .23 11 2.5 1 11   560 80 1 7.5 380 62 1 10   580 79 1 900 940 8100 0
minepump_spec1_product41_false-unreach-call_false-termination.cil.c .31 32 3.1  1 .31 35 2.8 1 7.0 380 53 1 6.0 330 53 1 5.6 290 44 1 1.3  77 18   1 1.0  30 9.2 1 .77  30 7.5  1 8.0 430 66 1 .23 11 2.3 1 11   530 88 1 11   530 79 1 11   540 95 1 900 1000 11000 0
minepump_spec1_product42_false-unreach-call_false-termination.cil.c .46 33 4.7  1 .33 35 2.4 1 7.2 380 63 1 6.0 330 53 1 5.6 290 50 1 1.3  78 17   1 1.3  31 9.5 1 .87  30 8.8  1 8.6 450 78 1 .23 11 2.6 1 15   650 110 1 13   580 110 1 39   1100 340 1 900 1000 8900 0
minepump_spec1_product43_false-unreach-call_false-termination.cil.c .42 35 4.7  1 .31 36 2.9 1 7.2 400 61 1 6.1 310 49 1 5.4 300 43 1 1.5  78 19   1 1.2  30 10   1 .95  30 7.6  1 8.0 440 71 1 .23 12 2.3 1 10   540 87 1 14   660 120 1 10   530 77 1 900 1100 7800 0
minepump_spec1_product44_false-unreach-call_false-termination.cil.c .44 34 4.3  1 .29 36 3.6 1 6.8 380 61 1 6.3 350 52 1 5.5 290 50 1 1.6  78 20   1 1.4  30 11   1 .88  30 8.5  1 8.3 440 72 1 .23 11 2.3 1 15   670 130 1 900   1700 11000 0 48   1200 400 1 900 1100 9600 0
minepump_spec1_product49_false-unreach-call_false-termination.cil.c .17 28 1.6  1 .32 36 3.1 1 5.8 320 47 1 5.2 300 48 1 4.2 280 34 1 .55 78 7.1 1 .49 30 3.8 1 .79  30 6.4  1 6.0 300 58 1 .21 11 2.3 1 10   530 82 1 6.9 350 53 1 9.9 530 78 1 900 950 9500 0
minepump_spec1_product50_false-unreach-call_false-termination.cil.c .16 28 1.9  1 .32 36 3.4 1 5.5 320 49 1 5.0 290 43 1 4.1 280 36 1 .55 78 7.3 1 .43 30 5.0 1 .90  30 7.6  1 6.3 300 48 1 .22 11 2.6 1 11   540 93 1 9.1 370 60 1 11   570 95 1 900 970 8200 0
minepump_spec1_product51_false-unreach-call_false-termination.cil.c .20 28 1.4  1 .34 36 2.9 1 5.7 320 49 1 5.5 300 51 1 4.4 270 38 1 .59 80 7.7 1 .52 30 4.3 1 .51  30 5.1  1 5.8 300 49 1 .21 11 2.7 1 11   540 84 1 7.7 370 65 1 9.9 520 76 1 900 800 7900 0
minepump_spec1_product52_false-unreach-call_false-termination.cil.c .19 28 1.5  1 .34 36 3.0 1 5.6 310 51 1 5.1 300 48 1 4.6 270 39 1 .61 78 6.9 1 .49 30 5.3 1 .56  30 4.3  1 5.8 310 52 1 .21 11 2.4 1 10   540 81 1 7.9 390 66 1 11   560 84 1 900 700 7800 0
minepump_spec1_product53_false-unreach-call_false-termination.cil.c .21 30 1.8  1 .37 39 3.6 1 5.7 330 44 1 5.5 300 50 1 4.1 280 35 1 .57 79 7.7 1 .49 30 4.6 1 .83  30 6.4  1 5.9 300 49 1 .24 11 2.3 1 11   530 81 1 7.8 350 57 1 10   540 81 1 900 820 8300 0
minepump_spec1_product54_false-unreach-call_false-termination.cil.c .22 29 1.8  1 .40 37 3.7 1 5.8 320 55 1 5.5 290 41 1 4.2 280 36 1 .56 79 8.1 1 .49 30 4.0 1 .82  30 7.8  1 6.1 300 58 1 .21 12 2.5 1 12   660 95 1 9.3 370 61 1 13   640 97 1 900 830 7800 0
minepump_spec1_product55_false-unreach-call_false-termination.cil.c .20 28 2.2  1 .40 37 4.2 1 5.8 320 53 1 5.3 300 42 1 4.3 280 39 1 .62 80 9.3 1 .50 30 4.1 1 .50  30 4.0  1 5.9 310 50 1 .22 12 2.9 1 10   560 73 1 7.9 400 61 1 10   580 80 1 900 870 8100 0
minepump_spec1_product56_false-unreach-call_false-termination.cil.c .22 29 1.7  1 .37 39 3.6 1 5.6 320 49 1 6.0 300 51 1 4.6 280 42 1 .63 79 9.1 1 .48 30 4.5 1 .50  30 5.0  1 6.0 300 48 1 .21 11 2.4 1 11   540 78 1 8.4 390 73 1 10   540 77 1 900 870 9800 0
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c .33 49 3.6  1 .67 51 8.2 0 7.5 400 60 1 7.6 420 69 1 7.6 330 65 1 1.5  90 23   1 1.2  31 12   1 1.6   31 17    1 36   1500 300 0 .27 12 2.7 1 13   690 110 1 900   1600 12000 0 13   650 100 1 900 930 7700 0
minepump_spec2_product33_false-unreach-call_false-termination.cil.c .42 33 4.7  1 .30 36 3.3 1 6.8 380 61 1 6.4 320 53 1 5.7 290 53 1 1.3  78 18   1 1.1  30 9.7 1 .71  30 8.1  1 22   950 180 1 .21 11 2.7 1 12   550 99 1 12   540 100 1 31   1000 270 1 900 1000 8600 0
minepump_spec2_product34_false-unreach-call_false-termination.cil.c .46 36 5.9  1 .32 36 2.9 1 7.3 390 62 1 6.1 330 51 1 5.7 290 46 1 1.3  78 17   1 1.3  30 12   1 .79  30 7.3  1 23   1300 210 1 .23 12 2.4 1 12   560 92 1 13   620 110 1 40   1100 360 1 900 1000 11000 0
minepump_spec2_product35_false-unreach-call_false-termination.cil.c .52 34 5.5  1 .30 36 2.9 0 7.8 480 66 1 7.0 360 51 1 6.0 290 52 1 1.5  78 19   1 1.2  30 14   1 .87  30 7.4  1 37   1900 330 1 .26 12 2.5 1 12   560 100 1 13   560 100 1 12   560 110 1 900 1100 7100 0
minepump_spec2_product36_false-unreach-call_false-termination.cil.c .52 36 5.7  1 .30 36 2.7 1 6.9 390 56 1 6.5 340 52 1 5.8 290 47 1 1.6  78 20   1 1.3  30 10   1 .85  30 7.5  1 69   3000 710 1 .25 12 2.4 1 12   590 96 1 13   610 110 1 13   590 100 1 900 1100 9400 0
minepump_spec2_product41_false-unreach-call_false-termination.cil.c .78 41 8.6  1 .87 38 8.0 1 8.8 480 74 1 8.1 450 72 1 6.2 290 52 1 2.1  78 26   1 1.0  30 12   1 1.2   30 13    1 52   2400 430 1 .23 11 2.6 1 14   620 110 1 11   540 100 1 12   540 99 1 900 1100 8800 0
minepump_spec2_product42_false-unreach-call_false-termination.cil.c .82 44 8.0  1 .88 37 8.3 1 8.6 450 70 1 7.9 440 68 1 6.4 300 48 1 2.2  78 26   1 1.3  30 11   1 1.4   30 13    1 55   2600 530 1 .30 13 3.7 1 18   770 150 1 900   1400 11000 0 61   1500 540 1 900 660 8600 0
minepump_spec2_product43_false-unreach-call_false-termination.cil.c .82 43 9.0  1 .85 37 9.5 0 10   490 83 1 8.3 460 63 1 6.3 300 58 1 2.4  79 33   1 1.4  30 11   1 1.8   30 13    1 67   3100 750 1 .34 15 4.1 1 10   550 72 1 34   910 350 1 39   2300 340 1 900 720 8300 0
minepump_spec2_product44_false-unreach-call_false-termination.cil.c .80 41 7.3  1 .90 37 8.4 1 9.3 460 79 1 8.7 450 75 1 6.4 300 49 1 2.5  93 33   1 1.3  30 11   1 1.9   30 15    1 65   3000 610 1 .33 16 3.9 1 15   640 120 1 23   800 210 1 120   1800 1200 1 900 730 8400 0
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c .81 70 8.9  1 .69 51 8.6 0 17   680 120 1 16   740 140 1 15   800 120 1 2.7  88 35   1 1.8  31 12   1 1.5   31 14    1 960   8100 12000 0 1.3  46 18   1 17   790 120 1 140   2500 1600 1 59   4600 670 1 900 960 7400 0
minepump_spec3_product01_false-unreach-call_false-termination.cil.c .14 26 1.1  1 .28 35 2.4 1 4.9 320 43 1 4.1 290 39 1 3.8 270 36 1 .51 77 5.9 1 .41 30 2.8 1 .40  30 3.1  1 6.5 320 54 1 .20 11 2.7 1 7.1 330 54 1 6.1 310 48 1 6.9 320 58 1 780 1900 7800 0
minepump_spec3_product02_false-unreach-call_false-termination.cil.c .17 26 1.1  1 .28 35 2.8 1 5.2 320 48 1 4.1 290 36 1 3.5 260 30 1 .53 77 5.8 1 .39 30 3.0 1 .37  30 3.5  1 6.9 320 58 1 .21 11 2.7 1 8.2 440 66 1 6.3 300 46 1 8.5 430 70 1 790 2000 8000 0
minepump_spec3_product03_false-unreach-call_false-termination.cil.c .16 29 1.2  1 .29 35 2.5 1 5.2 310 42 1 4.0 290 36 1 3.6 270 32 1 .54 77 6.4 1 .32 30 4.6 1 .30  30 4.3  1 6.3 320 50 1 .22 11 3.0 1 8.2 410 69 1 5.9 310 45 1 8.1 420 71 1 810 2000 8000 0
minepump_spec3_product04_false-unreach-call_false-termination.cil.c .15 27 1.1  1 .27 35 2.7 1 5.1 320 44 1 4.2 290 41 1 3.8 270 31 1 .56 77 6.6 1 .37 30 3.0 1 .41  30 3.1  1 6.6 320 54 1 .22 11 2.7 1 8.0 410 69 1 6.0 310 47 1 8.0 380 58 1 810 1800 9700 0
minepump_spec3_product05_false-unreach-call_false-termination.cil.c .18 29 1.1  1 .29 35 2.5 1 5.3 310 42 1 4.3 290 40 1 3.6 270 34 1 .53 77 6.3 1 .35 30 3.5 1 .36  30 3.5  1 6.8 340 62 1 .22 11 2.2 1 7.0 330 52 1 6.0 330 51 1 7.1 320 51 1 880 2000 10000 0
minepump_spec3_product06_false-unreach-call_false-termination.cil.c .15 27 1.4  1 .29 35 2.5 1 5.5 330 49 1 4.4 290 39 1 3.7 280 37 1 .53 77 6.2 1 .34 30 3.6 1 .39  30 3.3  1 6.8 340 59 1 .20 11 2.5 1 7.8 380 59 1 6.3 330 49 1 7.8 390 57 1 890 2000 9600 0
minepump_spec3_product07_false-unreach-call_false-termination.cil.c .16 27 1.1  1 .28 35 2.5 1 5.6 320 50 1 4.4 290 35 1 3.9 270 31 1 .58 77 7.5 1 .42 30 3.1 1 .38  30 3.3  1 6.6 340 58 1 .20 12 2.7 1 8.4 410 66 1 6.6 320 57 1 8.2 410 69 1 900 1700 9600 0
minepump_spec3_product08_false-unreach-call_false-termination.cil.c .16 27 1.2  1 .31 35 2.4 1 5.3 320 53 1 4.5 280 41 1 3.8 270 33 1 .57 77 6.2 1 .39 30 3.2 1 .33  30 3.9  1 6.7 340 61 1 .22 11 2.3 1 8.0 410 61 1 6.7 320 54 1 8.3 410 68 1 900 1200 7400 0
minepump_spec3_product09_false-unreach-call_false-termination.cil.c .17 26 1.3  1 .30 35 2.7 1 5.2 310 43 1 4.0 290 35 1 3.5 260 33 1 .51 77 5.8 1 .39 30 3.3 1 .34  30 3.5  1 6.5 320 62 1 .22 11 2.3 1 7.1 310 53 1 6.0 310 48 1 6.9 310 57 1 790 1900 8100 0
minepump_spec3_product10_false-unreach-call_false-termination.cil.c .17 26 1.2  1 .26 35 3.5 1 5.1 310 41 1 4.1 280 36 1 3.8 270 31 1 .50 77 7.8 1 .40 30 3.0 1 .41  30 3.3  1 6.5 330 53 1 .20 11 2.5 1 8.5 440 62 1 6.3 310 52 1 8.4 440 70 1 790 2000 11000 0
minepump_spec3_product11_false-unreach-call_false-termination.cil.c .15 27 1.3  1 .31 35 2.4 1 5.4 310 46 1 4.3 280 37 1 3.8 270 31 1 .54 77 7.7 1 .40 30 3.2 1 .35  30 3.2  1 6.6 320 51 1 .23 11 2.1 1 7.8 360 65 1 6.0 310 44 1 7.7 370 56 1 810 2000 8500 0
minepump_spec3_product12_false-unreach-call_false-termination.cil.c .14 27 1.4  1 .32 35 2.4 1 5.1 310 45 1 4.3 290 38 1 3.9 280 32 1 .55 77 6.5 1 .36 30 3.4 1 .34  30 4.0  1 6.6 330 58 1 .23 11 2.4 1 8.1 370 65 1 6.0 310 48 1 7.7 360 62 1 820 1300 8700 0
minepump_spec3_product13_false-unreach-call_false-termination.cil.c .17 27 1.3  1 .29 35 2.4 1 5.2 310 42 1 4.3 290 40 1 3.8 270 32 1 .51 77 5.6 1 .39 30 3.0 1 .34  30 3.1  1 6.9 350 52 1 .20 11 3.0 1 7.1 320 53 1 6.1 320 46 1 6.9 330 59 1 880 2000 9600 0
minepump_spec3_product14_false-unreach-call_false-termination.cil.c .16 29 1.1  1 .32 35 2.6 1 5.5 310 41 1 4.5 290 38 1 3.9 270 27 1 .53 77 5.7 1 .39 30 2.7 1 .34  30 3.7  1 6.8 350 60 1 .21 11 2.7 1 7.8 370 59 1 6.8 330 54 1 8.1 370 65 1 890 2000 9100 0
minepump_spec3_product15_false-unreach-call_false-termination.cil.c .15 27 1.5  1 .30 35 2.5 1 5.6 330 48 1 4.4 290 45 1 3.7 270 31 1 .56 77 7.4 1 .37 30 3.4 1 .39  30 3.2  1 7.0 340 58 1 .22 11 2.5 1 8.1 400 66 1 6.5 330 48 1 8.1 400 64 1 900 1800 9600 0
minepump_spec3_product16_false-unreach-call_false-termination.cil.c .17 27 1.2  1 .27 37 2.7 1 5.4 320 42 1 4.7 290 43 1 3.9 280 32 1 .55 77 6.6 1 .37 30 3.2 1 .38  30 3.2  1 6.9 340 57 1 .21 11 2.8 1 8.2 410 62 1 6.4 320 48 1 8.1 410 63 1 900 1100 9100 0
minepump_spec3_product17_false-unreach-call_false-termination.cil.c .18 27 1.2  1 .30 36 2.5 1 5.2 330 42 1 4.5 290 40 1 3.8 270 33 1 .51 77 5.9 1 .35 30 3.4 1 .34  30 3.6  1 7.2 350 59 1 .21 11 2.4 1 8.3 410 66 1 7.6 390 68 1 8.6 420 71 1 900 2000 9500 0
minepump_spec3_product18_false-unreach-call_false-termination.cil.c .16 27 1.1  1 .28 36 3.1 1 5.5 320 53 1 4.6 290 43 1 3.8 270 32 1 .53 77 7.1 1 .36 30 3.2 1 .37  30 3.5  1 7.1 350 67 1 .20 11 2.5 1 7.7 380 67 1 7.9 420 58 1 7.8 380 66 1 900 2000 11000 0
minepump_spec3_product19_false-unreach-call_false-termination.cil.c .16 27 1.1  1 .29 37 2.4 1 5.4 320 49 1 4.4 290 37 1 4.0 280 34 1 .57 78 7.1 1 .37 30 3.2 1 .37  30 4.2  1 6.8 350 60 1 .21 12 2.4 1 8.1 390 59 1 6.5 330 51 1 8.2 400 68 1 900 1500 9200 0
minepump_spec3_product20_false-unreach-call_false-termination.cil.c .17 29 1.2  1 .28 36 2.5 1 5.3 300 42 1 4.7 290 44 1 3.9 270 31 1 .56 78 7.2 1 .35 30 3.9 1 .34  30 3.2  1 6.9 340 55 1 .22 11 2.6 1 7.9 390 65 1 6.7 350 53 1 8.1 380 57 1 900 1100 9100 0
minepump_spec3_product21_false-unreach-call_false-termination.cil.c .19 27 1.5  1 .29 35 2.7 1 5.1 320 45 1 4.8 290 46 1 3.9 280 34 1 .55 78 6.0 1 .34 30 3.0 1 .35  30 4.4  1 6.9 340 53 1 .21 11 2.3 1 8.4 430 67 1 6.7 340 53 1 8.5 430 76 1 900 2000 9100 0
minepump_spec3_product22_false-unreach-call_false-termination.cil.c .17 27 1.4  1 .30 35 2.5 1 5.2 310 41 1 4.6 290 39 1 4.2 280 35 1 .51 78 5.9 1 .36 30 3.6 1 .32  30 4.3  1 7.0 350 50 1 .23 11 2.3 1 8.1 400 71 1 6.6 330 54 1 8.1 400 64 1 900 2000 10000 0
minepump_spec3_product23_false-unreach-call_false-termination.cil.c .18 28 1.3  1 .31 35 2.4 1 5.3 310 42 1 4.7 290 37 1 3.9 280 34 1 .58 78 8.3 1 .42 30 2.6 1 .39  30 2.5  1 6.7 350 56 1 .21 11 2.4 1 8.0 390 69 1 6.6 320 51 1 7.8 400 58 1 900 1200 9600 0
minepump_spec3_product24_false-unreach-call_false-termination.cil.c .15 27 1.3  1 .29 36 2.5 1 5.3 310 50 1 4.9 300 41 1 3.8 270 33 1 .57 78 6.4 1 .35 30 2.9 1 .35  30 3.3  1 6.7 350 51 1 .22 11 2.4 1 8.2 400 63 1 6.5 330 59 1 8.0 400 73 1 900 920 9700 0
minepump_spec3_product25_false-unreach-call_false-termination.cil.c .16 27 1.3  1 .29 35 2.7 1 5.4 320 43 1 4.5 290 45 1 3.7 270 35 1 .53 77 7.0 1 .38 30 3.4 1 .37  30 3.4  1 6.9 340 58 1 .22 12 2.1 1 7.4 320 56 1 7.6 420 62 1 7.3 330 61 1 900 1900 9600 0
minepump_spec3_product26_false-unreach-call_false-termination.cil.c .17 27 1.4  1 .32 35 2.5 1 5.5 330 45 1 4.5 290 37 1 3.8 280 34 1 .53 77 7.1 1 .35 30 3.5 1 .34  30 3.7  1 6.9 350 54 1 .21 11 2.5 1 7.9 380 63 1 7.4 420 60 1 8.1 380 63 1 900 2000 12000 0
minepump_spec3_product27_false-unreach-call_false-termination.cil.c .15 27 1.5  1 .31 35 2.5 1 5.6 320 48 1 4.4 290 42 1 3.7 270 31 1 .56 78 6.4 1 .38 30 3.7 1 .39  30 3.2  1 6.8 340 57 1 .22 11 2.6 1 7.9 390 64 1 6.2 330 56 1 8.0 380 65 1 900 1200 9300 0
minepump_spec3_product28_false-unreach-call_false-termination.cil.c .16 27 1.3  1 .27 36 3.6 1 5.4 320 42 1 4.8 290 39 1 3.9 280 33 1 .57 77 7.6 1 .41 30 3.7 1 .41  30 2.9  1 6.8 350 51 1 .24 11 2.8 1 8.1 390 64 1 6.8 350 53 1 7.6 390 66 1 900 1200 9000 0
minepump_spec3_product29_false-unreach-call_false-termination.cil.c .16 27 1.5  1 .28 36 2.6 1 5.6 310 50 1 4.7 300 37 1 3.9 270 33 1 .55 78 7.4 1 .37 30 3.2 1 .38  30 3.2  1 6.7 350 56 1 .21 11 2.2 1 7.0 340 56 1 6.4 330 52 1 7.2 330 57 1 900 2000 9300 0
minepump_spec3_product30_false-unreach-call_false-termination.cil.c .17 29 1.3  1 .29 35 2.4 1 5.6 310 49 1 4.7 290 45 1 3.8 280 32 1 .55 78 6.4 1 .38 30 3.0 1 .37  30 3.4  1 7.3 360 60 1 .22 11 2.6 1 9.4 510 78 1 6.4 340 54 1 8.9 490 65 1 900 2000 9800 0
minepump_spec3_product31_false-unreach-call_false-termination.cil.c .17 27 1.2  1 .30 36 2.4 1 5.6 320 52 1 4.6 290 40 1 4.0 280 36 1 .60 78 7.0 1 .34 30 3.6 1 .39  30 3.1  1 6.9 340 56 1 .24 11 2.4 1 8.6 430 70 1 6.7 330 53 1 8.2 420 65 1 900 1200 11000 0
minepump_spec3_product32_false-unreach-call_false-termination.cil.c .17 28 1.2  1 .30 36 2.6 1 5.2 300 48 1 4.9 300 47 1 3.9 270 33 1 .60 78 7.7 1 .36 30 2.9 1 .38  30 3.3  1 6.7 350 61 1 .23 11 2.4 1 8.2 430 64 1 6.7 330 57 1 8.2 420 62 1 900 920 8200 0
minepump_spec3_product35_false-unreach-call_false-termination.cil.c .19 27 1.2  1 .33 35 2.7 1 6.3 340 48 1 4.8 300 41 1 3.9 270 37 1 .80 78 8.3 1 .57 30 4.9 1 .55  30 5.6  1 13   640 110 1 .24 11 2.3 1 8.1 390 59 1 5.9 310 56 1 8.1 390 72 1 900 1000 8300 0
minepump_spec3_product36_false-unreach-call_false-termination.cil.c .18 28 1.2  1 .32 38 2.8 1 6.2 350 54 1 5.9 300 43 1 3.8 270 35 1 .83 79 12   1 .59 30 4.7 1 .96  30 7.6  1 29   920 230 1 .21 11 2.5 1 8.0 390 65 1 6.2 320 46 1 10   410 66 1 900 730 8700 0
minepump_spec3_product39_false-unreach-call_false-termination.cil.c .18 30 1.5  1 .32 38 3.1 1 6.2 350 51 1 4.8 290 41 1 4.0 270 31 1 .91 79 10   1 .55 30 4.5 1 .56  30 5.1  1 20   920 160 1 .24 11 2.4 1 8.3 400 67 1 6.9 330 60 1 8.4 410 69 1 900 700 8600 0
minepump_spec3_product40_false-unreach-call_false-termination.cil.c .19 28 1.4  1 .32 38 3.9 1 6.3 350 62 1 5.6 310 53 1 3.8 270 33 1 .86 79 12   1 .52 30 6.0 1 .51  30 5.0  1 45   1700 430 1 .23 11 2.6 1 8.1 400 59 1 6.7 330 57 1 8.5 410 66 1 900 710 7900 0
minepump_spec3_product43_false-unreach-call_false-termination.cil.c .18 30 1.5  1 .32 36 3.2 1 6.2 350 55 1 4.6 290 44 1 4.2 270 36 1 .78 79 11   1 .55 30 4.0 1 .52  30 5.5  1 24   960 170 1 .21 12 2.7 1 7.8 390 61 1 6.8 340 61 1 7.9 390 62 1 900 770 11000 0
minepump_spec3_product44_false-unreach-call_false-termination.cil.c .16 28 1.3  1 .31 36 3.5 1 5.9 330 51 1 6.8 370 54 1 4.1 280 35 1 .90 79 11   1 .51 30 5.5 1 1.2   30 13    1 99   2500 1200 1 .24 11 2.5 1 8.0 390 64 1 6.1 320 47 1 7.8 390 62 1 900 780 8000 0
minepump_spec3_product47_false-unreach-call_false-termination.cil.c .17 28 1.4  1 .35 37 3.5 1 6.1 350 57 1 4.6 290 38 1 3.9 280 31 1 .87 80 10   1 .50 30 5.4 1 .59  30 4.8  1 26   960 210 1 .23 11 2.3 1 8.1 410 63 1 6.7 320 60 1 7.8 400 64 1 900 840 9700 0
minepump_spec3_product48_false-unreach-call_false-termination.cil.c .21 29 1.4  1 .35 37 4.2 1 5.9 340 53 1 6.8 380 61 1 3.9 280 31 1 .83 79 9.4 1 .51 30 4.6 1 1.2   30 11    1 31   1400 230 1 .24 11 2.3 1 8.1 410 67 1 7.0 350 57 1 8.2 400 68 1 900 850 8100 0
minepump_spec3_product51_false-unreach-call_false-termination.cil.c .20 28 1.5  1 .35 38 2.9 1 6.1 350 53 1 4.7 300 43 1 4.0 270 32 1 .63 78 7.4 1 .43 30 6.9 1 .55  30 4.6  1 30   1400 220 1 .21 11 2.3 1 7.9 390 73 1 6.7 320 54 1 7.8 400 61 1 900 720 9300 0
minepump_spec3_product52_false-unreach-call_false-termination.cil.c .19 30 1.5  1 .36 36 2.9 1 6.4 340 54 1 5.7 300 49 1 3.9 270 33 1 .64 78 7.6 1 .58 30 4.8 1 .59  30 5.3  1 42   2000 310 1 .22 12 3.3 1 11   440 84 1 6.7 340 54 1 8.4 410 65 1 900 730 10000 0
minepump_spec3_product55_false-unreach-call_false-termination.cil.c .21 30 1.8  1 .37 38 4.0 1 6.2 350 51 1 5.1 300 46 1 4.0 280 32 1 .64 80 7.9 1 .55 30 5.1 1 .77  30 7.5  1 25   1300 210 1 .23 11 2.9 1 8.3 410 70 1 6.9 330 54 1 8.2 410 71 1 900 900 7800 0
minepump_spec3_product56_false-unreach-call_false-termination.cil.c .22 29 1.8  1 .40 38 3.7 1 6.4 350 53 1 5.9 310 54 1 3.8 270 35 1 .67 80 8.1 1 .57 30 5.0 1 .53  30 5.0  1 33   1100 290 1 .21 11 2.4 1 8.4 420 72 1 7.1 340 57 1 8.2 410 65 1 900 900 9700 0
minepump_spec3_product59_false-unreach-call_false-termination.cil.c .19 29 1.7  1 .33 36 3.3 1 6.5 360 57 1 5.0 300 46 1 3.8 270 32 1 .65 79 7.5 1 .60 30 4.7 1 .51  30 6.1  1 34   1600 300 1 .21 11 2.9 1 8.0 410 63 1 8.0 440 70 1 8.1 400 70 1 900 650 7300 0
minepump_spec3_product60_false-unreach-call_false-termination.cil.c .19 28 1.5  1 .35 37 3.7 1 6.2 330 55 1 6.7 380 61 1 4.2 280 36 1 .62 79 7.7 1 .54 30 5.0 1 .58  30 5.4  1 35   1700 300 1 .24 11 2.3 1 8.3 400 70 1 6.6 340 55 1 8.4 420 74 1 900 660 7500 0
minepump_spec3_product63_false-unreach-call_false-termination.cil.c .25 31 1.8  1 .39 39 4.0 1 6.5 350 48 1 5.0 300 42 1 3.9 280 33 1 .68 80 7.9 1 .57 30 4.8 1 .55  30 6.1  1 28   940 230 1 .21 11 2.8 1 8.2 420 63 1 6.8 340 53 1 8.1 410 60 1 900 820 7300 0
minepump_spec3_product64_false-unreach-call_false-termination.cil.c .22 29 1.7  1 .41 39 5.0 1 6.2 340 56 1 7.1 410 65 1 3.9 270 36 1 .69 81 9.1 1 .56 30 5.2 1 .61  30 3.7  1 31   1400 280 1 .21 12 2.7 1 8.2 430 66 1 7.2 360 64 1 8.2 420 73 1 900 820 9000 0
minepump_spec3_productSimulator_false-unreach-call_false-termination.cil.c .35 49 2.9  1 .69 52 7.7 1 6.7 370 57 1 6.4 340 54 1 5.6 290 50 1 1.6  88 23   1 1.4  31 13   1 1.3   31 14    1 42   2200 380 1 .23 12 2.9 1 9.6 530 80 1 7.8 350 59 1 9.8 530 82 1 900 940 7300 0
minepump_spec4_product33_false-unreach-call_false-termination.cil.c .55 37 5.9  1 .81 38 9.1 1 7.0 380 60 1 5.5 300 45 1 5.7 290 48 1 2.1  77 27   1 .75 30 7.0 1 .90  30 6.6  1 10   470 84 1 .23 11 2.4 1 17   660 120 1 15   720 130 1 28   870 230 1 900 970 9900 0
minepump_spec4_product34_false-unreach-call_false-termination.cil.c .73 43 9.5  1 .78 36 8.1 1 7.0 380 57 1 5.4 290 45 1 6.0 290 54 1 2.0  79 29   1 .93 30 7.2 1 1.0   30 7.9  1 11   460 89 1 .24 11 2.5 1 19   720 150 1 23   850 240 1 31   1000 260 1 900 990 9700 0
minepump_spec4_product35_false-unreach-call_false-termination.cil.c .67 40 7.2  1 .81 38 11   1 7.6 330 68 1 6.0 320 51 1 5.9 290 42 1 2.1  78 27   1 1.0  30 11   1 1.2   30 10    1 12   460 98 1 .24 11 2.4 1 15   630 120 1 31   1000 320 1 20   800 160 1 900 1100 9000 0
minepump_spec4_product36_false-unreach-call_false-termination.cil.c .76 43 7.9  1 .85 38 7.8 1 7.7 390 62 1 5.6 300 47 1 6.3 290 47 1 2.1  78 31   1 .90 30 10   1 1.1   30 8.8  1 11   460 93 1 .25 11 2.9 1 21   740 180 1 26   880 240 1 25   810 180 1 900 1100 8800 0
minepump_spec4_product37_false-unreach-call_false-termination.cil.c .68 40 8.2  1 .90 39 9.2 1 8.2 470 68 1 6.1 340 49 1 5.9 300 47 1 2.2  79 33   1 1.2  30 9.7 1 1.2   30 12    1 45   2000 350 1 .23 11 2.3 1 19   750 150 1 22   860 220 1 27   940 250 1 900 920 8600 0
minepump_spec4_product38_false-unreach-call_false-termination.cil.c .83 41 9.9  1 .91 37 9.4 1 9.6 480 78 1 6.7 350 55 1 6.5 300 55 1 2.2  79 31   1 1.3  30 14   1 1.5   30 13    1 44   2000 420 1 .28 13 3.1 1 19   750 160 1 24   820 270 1 23   810 180 1 900 930 8300 0
minepump_spec4_product39_false-unreach-call_false-termination.cil.c .90 44 9.8  1 .91 38 10   0 9.2 460 72 1 6.9 380 59 1 6.3 290 53 1 2.3  79 29   1 1.4  30 11   1 2.3   30 15    1 49   2200 450 1 .29 14 4.6 1 21   750 170 1 51   1200 620 1 58   1200 500 1 900 990 7600 0
minepump_spec4_product40_false-unreach-call_false-termination.cil.c .77 42 7.4  1 .91 40 9.8 1 10   470 85 1 6.5 350 57 1 6.2 300 51 1 2.4  79 26   1 1.3  30 12   1 2.0   30 16    1 66   3600 650 1 .30 14 3.4 1 18   740 140 1 900   1900 11000 0 23   830 180 1 900 1000 9100 0
minepump_spec4_product41_false-unreach-call_false-termination.cil.c .57 37 6.0  1 .84 36 8.2 1 8.6 470 70 1 6.4 350 57 1 5.7 290 54 1 2.1  78 27   1 1.1  30 8.7 1 1.1   30 10    1 12   570 91 1 .23 12 2.5 1 15   670 130 1 19   750 180 1 44   1000 450 1 900 1100 8000 0
minepump_spec4_product42_false-unreach-call_false-termination.cil.c .62 38 6.6  1 .83 38 11   1 8.4 480 72 1 6.7 340 60 1 6.1 300 53 1 2.1  78 27   1 1.2  30 11   1 1.2   30 12    1 13   620 110 1 .28 13 3.4 1 16   700 140 1 14   620 120 1 59   1500 510 1 900 1500 11000 0
minepump_spec4_product43_false-unreach-call_false-termination.cil.c .74 43 9.0  1 .84 38 7.7 1 8.6 480 76 1 7.2 410 54 1 5.8 290 49 1 2.3  78 28   1 1.2  30 10   1 1.6   30 16    1 12   550 99 1 .27 13 3.1 1 19   750 160 1 48   1200 590 1 44   1100 370 1 900 940 8200 0
minepump_spec4_product44_false-unreach-call_false-termination.cil.c .72 42 8.1  1 .88 38 7.7 1 8.3 490 72 1 7.1 380 52 1 6.3 290 48 1 2.3  78 26   1 1.3  30 9.5 1 1.8   30 14    1 15   610 97 1 .31 14 3.4 1 17   690 130 1 24   850 250 1 35   1000 310 1 900 730 9700 0
minepump_spec4_product45_false-unreach-call_false-termination.cil.c .60 40 7.3  1 .93 39 10   1 9.2 480 79 1 7.0 390 59 1 5.5 290 53 1 2.2  79 34   1 1.3  30 11   1 1.4   30 14    1 73   3300 690 1 .22 11 2.5 1 16   690 120 1 900   1700 11000 0 21   880 150 1 900 740 9200 0
minepump_spec4_product46_false-unreach-call_false-termination.cil.c .84 42 11    1 .94 40 10   1 9.1 490 64 1 7.6 430 59 1 6.0 290 43 1 2.3  79 29   1 1.5  30 14   1 1.6   30 14    1 74   3300 810 1 .31 14 3.6 1 17   750 130 1 32   890 390 1 15   610 99 1 900 740 9000 0
minepump_spec4_product47_false-unreach-call_false-termination.cil.c .75 42 9.7  1 .94 42 9.9 0 8.8 480 77 1 7.9 450 63 1 6.3 300 52 1 2.4  79 27   1 1.6  30 13   1 1.6   30 18    1 90   3800 1100 1 .39 17 4.6 1 21   760 180 1 900   1600 11000 0 25   940 200 1 900 810 8500 0
minepump_spec4_product48_false-unreach-call_false-termination.cil.c .77 43 7.5  1 .97 40 12   1 10   480 71 1 7.8 410 57 1 5.9 300 49 1 2.5  81 32   1 1.5  30 17   1 1.5   30 16    1 100   3600 1000 1 .40 17 4.3 1 18   750 140 1 35   950 350 1 140   2100 1500 1 900 820 8700 0
minepump_spec4_productSimulator_false-unreach-call_false-termination.cil.c 1.3  81 17    1 2.2  83 25   0 17   690 120 1 16   630 130 1 15   790 130 1 3.9  87 51   1 2.2  31 18   1 3.1   31 26    1 330   5700 3700 1 9.8  260 130   1 26   820 210 1 320   4700 4800 1 900   4700 11000 0 900 930 7300 0
minepump_spec1_product01_true-unreach-call_false-termination.cil.c .16 26 .96 2 870    890 4700   0 4.0 300 31 2 3.1 270 31 2 4.3 260 34 2 5.1  280 51   2 900    7400 12000   0 .12  28 .88 2 6.2 320 50 2 900    3200 9700   0 6.9 320 55 2 6.8 340 54 2 7.0 320 51 2 17 290 160 2
minepump_spec1_product02_true-unreach-call_false-termination.cil.c .15 27 1.1  2 870    930 4700   0 4.0 310 32 2 3.3 270 24 2 4.2 270 34 2 5.2  280 47   2 900    7700 13000   0 .096 28 .95 2 6.1 320 42 2 900    3200 8300   0 8.4 470 74 2 6.5 340 50 2 8.3 470 66 2 17 280 130 2
minepump_spec1_product03_true-unreach-call_false-termination.cil.c .14 27 1.2  2 870    990 6500   0 4.5 310 38 2 3.3 270 30 2 4.6 280 40 2 420    160 5000   0 900    7200 10000   0 900     7400 12000    0 6.1 330 53 2 900    2300 9400   0 7.7 380 70 2 7.0 350 53 2 8.1 400 61 2 17 290 150 2
minepump_spec1_product04_true-unreach-call_false-termination.cil.c .14 27 1.1  2 870    940 6500   0 3.9 310 34 2 3.3 270 32 2 4.6 270 33 2 430    160 6700   0 900    6500 11000   0 900     6500 11000    0 6.2 330 51 2 900    2300 9800   0 7.7 370 55 2 6.5 350 50 2 8.1 370 64 2 17 280 140 2
minepump_spec1_product05_true-unreach-call_false-termination.cil.c .16 27 1.1  2 870    790 4100   0 4.4 290 37 2 3.6 270 32 2 4.0 260 36 2 5.3  280 57   2 900    7200 12000   0 .096 28 1.2  2 6.2 330 49 2 900    3700 8900   0 7.7 380 63 2 10   540 89 2 7.7 370 64 2 17 290 120 2
minepump_spec1_product06_true-unreach-call_false-termination.cil.c .14 27 1.0  2 870    950 4500   0 4.3 290 42 2 3.5 270 34 2 4.4 270 42 2 400    150 5200   0 900    5300 13000   0 900     5300 11000    0 6.3 340 52 2 900    3300 11000   0 8.1 440 71 2 8.2 450 69 2 7.8 450 63 2 17 290 120 2
minepump_spec1_product07_true-unreach-call_false-termination.cil.c .14 27 1.3  2 870    980 6200   0 4.6 310 41 2 3.8 280 34 2 4.9 270 35 2 510    170 6200   0 900    7600 13000   0 900     7500 12000    0 6.3 340 55 2 900    2900 9700   0 7.9 430 70 2 12   530 100 2 8.2 420 69 2 18 290 160 2
minepump_spec1_product08_true-unreach-call_false-termination.cil.c .15 27 .99 2 870    890 5300   0 4.2 300 36 2 3.7 280 32 2 4.9 270 35 2 490    180 6000   0 900    6200 10000   0 900     6200 11000    0 6.4 340 56 2 900    2800 11000   0 11   480 100 2 900   1400 10000 0 8.3 420 65 2 18 320 150 2
minepump_spec1_product09_true-unreach-call_false-termination.cil.c .12 26 1.3  2 870    890 4500   0 4.0 310 34 2 3.2 270 31 2 4.0 260 30 2 5.0  280 48   2 900    5500 11000   0 .097 28 .99 2 6.1 320 53 2 900    3200 8000   0 8.4 460 64 2 6.4 340 47 2 8.7 460 76 2 17 290 140 2
minepump_spec1_product10_true-unreach-call_false-termination.cil.c .14 27 1.0  2 870    1000 7300   0 4.0 290 36 2 3.2 270 29 2 4.2 260 35 2 5.2  270 44   2 900    6200 12000   0 .13  28 .87 2 6.3 320 56 2 900    3200 9700   0 8.5 480 75 2 6.3 340 52 2 8.5 480 70 2 18 290 120 2
minepump_spec1_product11_true-unreach-call_false-termination.cil.c .14 27 1.1  2 870    950 4700   0 4.3 310 43 2 3.3 270 31 2 4.6 280 41 2 420    150 5800   0 900    7200 12000   0 900     7200 11000    0 6.1 320 47 2 900    2300 8600   0 8.1 390 65 2 6.5 350 50 2 7.6 390 61 2 17 290 140 2
minepump_spec1_product12_true-unreach-call_false-termination.cil.c .14 27 1.0  2 870    940 5800   0 4.1 290 31 2 3.3 280 33 2 4.5 270 35 2 430    160 6000   0 900    7500 12000   0 900     7500 11000    0 6.3 330 52 2 900    2300 11000   0 7.6 380 59 2 6.9 350 54 2 7.5 370 55 2 18 290 120 2
minepump_spec1_product13_true-unreach-call_false-termination.cil.c .14 27 1.3  2 870    800 5200   0 4.4 290 36 2 3.4 280 32 2 4.3 270 33 2 5.4  280 49   2 900    5200 11000   0 .10  28 1.1  2 6.3 340 48 2 900    3700 11000   0 7.7 370 60 2 11   460 94 2 7.5 370 55 2 18 290 120 2
minepump_spec1_product14_true-unreach-call_false-termination.cil.c .17 27 .95 2 870    950 5400   0 4.4 310 37 2 3.5 280 36 2 4.2 270 36 2 400    150 5000   0 900    6000 13000   0 900     6000 10000    0 6.5 340 53 2 900    3300 8800   0 8.0 450 63 2 11   570 95 2 8.0 440 69 2 18 290 130 2
minepump_spec1_product15_true-unreach-call_false-termination.cil.c .17 27 1.3  2 870    950 4800   0 4.5 290 40 2 3.6 270 32 2 4.6 280 36 2 500    180 6100   0 900    7200 9800   0 900     7200 9300    0 6.3 340 55 2 900    2800 9900   0 8.1 430 59 2 13   580 120 2 8.1 430 65 2 18 280 130 2
minepump_spec1_product16_true-unreach-call_false-termination.cil.c .16 27 1.2  2 870    890 5300   0 4.1 310 36 2 3.8 270 32 2 4.5 270 38 2 490    180 5900   0 900    6100 12000   0 900     6100 11000    0 6.5 350 53 2 900    2900 11000   0 8.1 430 70 2 11   510 110 2 7.8 420 66 2 18 290 140 2
minepump_spec1_product17_true-unreach-call_false-termination.cil.c .16 27 1.2  2 870    820 5500   0 4.3 290 41 2 3.8 280 33 2 4.5 270 38 2 250    130 3300   0 900    5400 11000   0 900     5400 11000    0 6.7 340 53 2 900    3600 8800   0 7.5 380 57 2 900   1700 12000 0 7.6 360 70 2 17 290 160 2
minepump_spec1_product18_true-unreach-call_false-termination.cil.c .15 27 1.1  2 870    940 5100   0 4.4 290 43 2 3.9 280 37 2 4.2 270 32 2 410    160 5600   0 900    6300 11000   0 900     6400 10000    0 6.7 340 53 2 900    3500 10000   0 8.3 450 70 2 7.7 370 59 2 8.0 440 69 2 18 290 130 2
minepump_spec1_product19_true-unreach-call_false-termination.cil.c .17 29 1.3  2 870    950 4800   0 4.7 310 39 2 4.0 280 35 2 4.8 270 40 2 460    190 5600   0 900    6000 10000   0 900     5900 10000    0 6.3 340 53 2 900    2900 10000   0 8.0 420 69 2 9.3 490 84 2 7.9 430 62 2 18 290 140 2
minepump_spec1_product20_true-unreach-call_false-termination.cil.c .16 27 1.2  2 870    900 5400   0 4.4 290 37 2 4.0 280 35 2 4.8 270 37 2 480    200 6100   0 900    6700 10000   0 900     6800 9700    0 6.5 350 56 2 900    3000 9300   0 8.4 440 71 2 12   540 110 2 8.2 440 66 2 18 280 130 2
minepump_spec1_product21_true-unreach-call_false-termination.cil.c .18 28 1.1  2 870    800 5200   0 4.3 290 35 2 3.9 280 32 2 4.4 270 36 2 5.3  280 53   2 900    4900 10000   0 .20  28 2.1  2 6.7 340 49 2 900    2800 9700   0 8.1 400 65 2 8.7 410 81 2 7.6 400 58 2 18 290 140 2
minepump_spec1_product22_true-unreach-call_false-termination.cil.c .18 30 1.1  2 870    960 4400   0 4.6 300 36 2 4.0 280 38 2 4.3 270 37 2 440    210 5700   0 900    5500 12000   0 900     5400 12000    0 6.2 350 55 2 900    2900 9200   0 8.3 460 75 2 12   520 77 2 8.3 480 74 2 18 290 150 2
minepump_spec1_product23_true-unreach-call_false-termination.cil.c .16 28 1.3  2 870    1000 6800   0 4.7 310 42 2 4.9 290 38 2 5.0 280 43 2 630    240 9400   0 900    5200 10000   0 900     5300 12000    0 6.4 350 58 2 900    2500 12000   0 8.1 450 70 2 12   520 99 2 8.4 470 68 2 19 290 150 2
minepump_spec1_product24_true-unreach-call_false-termination.cil.c .16 28 1.6  2 870    900 5700   0 4.2 290 37 2 5.5 300 52 2 4.8 270 36 2 550    240 7700   0 900    5100 10000   0 900     5100 9300    0 6.6 350 53 2 900    2600 9600   0 8.2 450 73 2 19   670 160 2 8.0 460 60 2 18 320 160 2
minepump_spec1_product25_true-unreach-call_false-termination.cil.c .17 27 1.1  2 870    800 4400   0 4.3 310 37 2 3.7 280 36 2 4.3 270 38 2 260    130 3100   0 900    7500 12000   0 900     7400 10000    0 6.6 340 56 2 900    3600 8700   0 7.7 370 68 2 8.0 350 60 2 7.5 380 63 2 18 290 140 2
minepump_spec1_product26_true-unreach-call_false-termination.cil.c .14 27 1.2  2 870    950 4200   0 4.4 310 36 2 3.8 280 39 2 4.7 270 35 2 410    160 5200   0 900    7400 12000   0 900     7400 11000    0 6.1 340 53 2 900    3300 9500   0 8.3 450 65 2 8.2 370 68 2 7.8 440 65 2 18 290 130 2
minepump_spec1_product27_true-unreach-call_false-termination.cil.c .14 27 1.2  2 870    940 4800   0 4.5 300 41 2 3.9 280 34 2 5.1 280 38 2 460    190 6600   0 900    5800 10000   0 900     5800 9400    0 6.6 350 53 2 900    2800 8700   0 8.1 430 60 2 12   530 90 2 8.1 440 62 2 18 280 150 2
minepump_spec1_product28_true-unreach-call_false-termination.cil.c .14 27 1.1  2 870    880 4900   0 4.4 310 34 2 4.3 280 35 2 4.6 280 38 2 470    200 5700   0 900    5500 10000   0 900     5500 11000    0 6.5 350 60 2 900    2900 9500   0 8.0 440 60 2 13   590 110 2 8.1 440 75 2 18 280 130 2
minepump_spec1_product29_true-unreach-call_false-termination.cil.c .18 27 1.3  2 870    780 4500   0 4.5 300 38 2 4.0 280 38 2 4.2 270 34 2 5.4  280 51   2 900    6200 10000   0 .17  28 2.2  2 6.9 330 64 2 900    2800 8000   0 7.9 400 68 2 8.9 420 83 2 7.6 390 67 2 18 290 140 2
minepump_spec1_product30_true-unreach-call_false-termination.cil.c .15 30 1.3  2 870    960 5900   0 4.5 310 41 2 4.1 280 35 2 4.6 270 39 2 460    210 5700   0 900    5400 11000   0 900     5400 11000    0 6.5 350 55 2 900    2900 10000   0 8.4 470 60 2 8.8 500 77 2 8.0 460 64 2 18 290 160 2
minepump_spec1_product31_true-unreach-call_false-termination.cil.c .18 28 1.3  2 870    930 5000   0 4.8 290 42 2 4.6 290 41 2 5.0 280 38 2 620    240 8500   0 900    6900 13000   0 900     7000 11000    0 6.4 340 54 2 900    2500 10000   0 7.9 440 64 2 14   580 110 2 8.2 450 70 2 18 290 140 2
minepump_spec1_product32_true-unreach-call_false-termination.cil.c .16 28 1.3  2 870    900 5000   0 4.2 310 38 2 5.5 300 46 2 4.9 280 38 2 560    250 7600   0 900    5200 12000   0 900     5200 12000    0 6.4 350 51 2 900    2500 11000   0 8.3 460 70 2 14   640 130 2 8.4 460 62 2 19 290 140 2
minepump_spec1_product45_true-unreach-call_false-termination.cil.c .16 28 2.1  2 870    1800 6300   0 6.0 310 56 2 5.5 300 47 2 6.1 310 47 2 7.8  330 72   2 900    3300 9700   0 .13  28 1.5  2 21   920 200 2 900    4000 6500   0 17   730 150 2 14   580 110 2 96   2500 1000 2 26 500 190 2
minepump_spec1_product46_true-unreach-call_false-termination.cil.c .18 28 1.5  2 870    1800 6700   0 6.2 320 51 2 6.9 360 56 2 6.2 310 44 2 900    220 11000   0 900    3600 9400   0 900     3500 11000    0 23   970 180 2 900    3700 11000   0 27   890 250 2 900   4500 11000 0 150   3800 1500 2 30 470 260 2
minepump_spec1_product47_true-unreach-call_false-termination.cil.c 900    3100 11000    0 870    2000 6900   0 6.3 330 52 2 5.5 300 51 2 5.9 320 48 2 900    220 11000   0 900    3200 9300   0 900     3100 10000    0 26   1600 200 2 900    2900 8600   0 20   770 140 2 18   700 160 2 130   2400 1300 2 900 810 8900 0
minepump_spec1_product48_true-unreach-call_false-termination.cil.c 900    2500 9000    0 870    2000 6400   0 6.9 370 53 2 6.1 330 56 2 6.4 330 51 2 900    230 11000   0 900    3000 10000   0 900     3000 10000    0 31   1700 280 2 900    3200 8300   0 29   850 230 2 20   700 160 2 200   2900 2200 2 900 820 7600 0
minepump_spec1_product57_true-unreach-call_false-termination.cil.c 900    2600 9200    0 870    1900 6900   0 6.4 330 50 2 6.3 360 51 2 4.7 280 34 2 900    170 12000   0 900    3000 11000   0 900     3000 10000    0 25   1300 210 2 900    3800 9000   0 22   760 200 2 900   1500 11000 0 96   2100 1100 2 900 770 8500 0
minepump_spec1_product58_true-unreach-call_false-termination.cil.c 900    2700 12000    0 870    1900 7500   0 6.7 350 59 2 5.9 340 47 2 4.9 280 41 2 900    190 10000   0 900    3300 10000   0 900     3300 10000    0 27   1300 220 2 900    3600 9200   0 25   880 190 2 900   1600 10000 0 190   2500 1800 2 900 790 8300 0
minepump_spec1_product59_true-unreach-call_false-termination.cil.c 900    3100 11000    0 870    1900 6300   0 7.4 370 61 2 5.8 330 50 2 5.1 280 38 2 900    210 11000   0 900    3100 9600   0 900     3000 9700    0 28   1300 240 2 900    2900 9000   0 31   880 240 2 900   1500 11000 0 290   4000 3400 2 900 850 8900 0
minepump_spec1_product60_true-unreach-call_false-termination.cil.c 900    2400 10000    0 870    1900 7500   0 6.8 390 52 2 6.5 370 52 2 5.2 280 38 2 900    200 12000   0 900    2900 9700   0 900     2900 10000    0 34   1800 280 2 900    3100 10000   0 27   900 210 2 21   760 200 2 900   2000 9900 0 900 850 6600 0
minepump_spec1_product61_true-unreach-call_false-termination.cil.c .19 31 2.1  2 870    3600 5700   0 6.3 330 46 2 5.8 340 47 2 4.8 280 43 2 6.8  290 71   2 900    3600 11000   0 .19  29 2.2  2 26   1100 200 2 900    3900 5900   0 21   740 180 2 14   610 130 2 190   3300 2000 2 29 500 280 2
minepump_spec1_product62_true-unreach-call_false-termination.cil.c .25 30 1.9  2 870    3700 5300   0 6.7 330 57 2 6.8 400 55 2 4.8 290 45 2 900    290 13000   0 900    3400 7600   0 900     3400 11000    0 26   1200 210 2 900    3500 8900   0 26   860 240 2 900   1500 11000 0 250   2600 2900 2 33 500 300 2
minepump_spec1_product63_true-unreach-call_false-termination.cil.c 900    3300 9900    0 870    3300 8100   0 6.6 340 53 2 6.4 340 53 2 5.5 280 40 2 900    290 11000   0 900    3100 9200   0 900     3100 9900    0 31   1400 240 2 900    3000 11000   0 20   770 170 2 25   840 230 2 210   3300 2200 2 900 800 7800 0
minepump_spec1_product64_true-unreach-call_false-termination.cil.c 900    2500 9500    0 870    3300 5800   0 7.8 400 63 2 6.6 390 50 2 5.1 280 40 2 900    290 13000   0 900    3000 11000   0 900     3000 11000    0 35   2000 310 2 900    3300 9200   0 19   760 170 2 26   840 230 2 900   5300 9700 0 900 810 7800 0
minepump_spec2_product01_true-unreach-call_false-termination.cil.c .16 27 .96 2 870    930 4800   0 5.7 310 43 2 3.4 280 29 2 4.0 260 35 2 5.1  270 53   2 900    6900 10000   0 .093 28 1.2  2 8.4 450 71 2 900    3400 9800   0 10   530 83 2 8.0 440 71 2 28   1000 260 2 18 290 140 2
minepump_spec2_product02_true-unreach-call_false-termination.cil.c .12 29 1.3  2 870    980 5200   0 5.8 310 56 2 3.5 280 32 2 4.1 260 37 2 5.4  280 54   2 900    7100 9800   0 .091 28 1.2  2 8.0 440 64 2 900    3500 8100   0 10   530 91 2 8.3 370 73 2 42   1400 440 2 17 290 120 2
minepump_spec2_product03_true-unreach-call_false-termination.cil.c .14 27 .98 2 870    970 6900   0 6.2 330 52 2 3.8 280 33 2 4.7 280 39 2 430    180 4800   0 900    7600 11000   0 900     7600 12000    0 8.6 440 73 2 900    2400 11000   0 8.2 400 70 2 8.0 360 74 2 8.2 410 69 2 17 290 130 2
minepump_spec2_product04_true-unreach-call_false-termination.cil.c .15 27 .96 2 870    1000 6100   0 6.1 310 55 2 3.7 280 35 2 4.6 270 38 2 430    180 5200   0 900    5900 10000   0 900     5900 10000    0 9.1 460 69 2 900    2400 8100   0 7.2 350 62 2 8.0 350 62 2 7.0 340 58 2 18 300 140 2
minepump_spec2_product05_true-unreach-call_false-termination.cil.c .16 27 1.3  2 870    940 4800   0 6.0 320 53 2 3.9 270 37 2 3.9 260 33 2 5.5  280 46   2 900    7400 12000   0 .12  28 .95 2 8.1 430 68 2 900    3900 8000   0 7.4 380 55 2 7.6 430 65 2 7.6 390 59 2 18 290 130 2
minepump_spec2_product06_true-unreach-call_false-termination.cil.c .15 27 1.2  2 870    960 5100   0 6.9 340 58 2 4.0 280 38 2 4.4 270 32 2 420    160 5000   0 900    7800 9300   0 900     7900 10000    0 8.4 440 67 2 900    3500 7600   0 7.8 410 61 2 8.9 430 73 2 8.0 410 65 2 17 290 130 2
minepump_spec2_product07_true-unreach-call_false-termination.cil.c .16 27 1.2  2 870    930 5600   0 6.3 340 52 2 4.3 280 41 2 4.9 280 45 2 530    190 6900   0 900    7600 11000   0 900     7600 11000    0 8.2 450 67 2 900    2600 9200   0 8.6 440 73 2 900   1400 12000 0 8.2 430 66 2 19 290 140 2
minepump_spec2_product08_true-unreach-call_false-termination.cil.c .16 28 1.0  2 870    1100 6400   0 6.8 360 54 2 4.4 280 41 2 4.5 270 41 2 480    190 5500   0 900    5700 11000   0 900     5700 13000    0 8.5 450 63 2 900    3100 8900   0 8.3 450 69 2 17   620 130 2 8.5 440 61 2 18 300 140 2
minepump_spec2_product09_true-unreach-call_false-termination.cil.c .13 29 1.1  2 870    940 4900   0 5.5 310 50 2 3.4 280 34 2 4.2 260 30 2 5.7  280 52   2 900    6100 11000   0 .12  28 1.2  2 9.1 450 79 2 900    3500 9700   0 10   530 90 2 6.9 340 52 2 32   1200 320 2 17 290 140 2
minepump_spec2_product10_true-unreach-call_false-termination.cil.c .16 27 1.1  2 870    950 5200   0 5.8 310 51 2 3.4 280 29 2 4.3 270 38 2 5.4  270 52   2 900    6900 11000   0 .13  28 .99 2 8.4 440 60 2 900    3400 7700   0 13   500 85 2 8.5 390 63 2 44   1600 410 2 18 290 130 2
minepump_spec2_product11_true-unreach-call_false-termination.cil.c .14 27 1.1  2 870    950 5000   0 6.2 330 53 2 3.6 280 34 2 4.7 280 37 2 430    170 4700   0 900    6100 10000   0 900     6100 12000    0 8.6 450 65 2 900    2400 13000   0 7.3 350 60 2 8.5 400 69 2 7.4 350 60 2 18 290 140 2
minepump_spec2_product12_true-unreach-call_false-termination.cil.c .15 27 1.2  2 870    960 6100   0 6.0 310 48 2 3.7 280 31 2 4.9 280 43 2 420    170 5500   0 900    7700 9800   0 900     7700 13000    0 8.3 440 65 2 900    2400 9700   0 7.5 340 64 2 8.7 480 67 2 7.7 350 62 2 18 290 140 2
minepump_spec2_product13_true-unreach-call_false-termination.cil.c .14 27 1.4  2 870    980 6400   0 5.8 320 55 2 4.1 300 36 2 4.5 270 40 2 5.4  280 51   2 900    6600 9500   0 .10  28 1.0  2 9.3 440 65 2 900    4300 9300   0 7.8 390 70 2 10   520 79 2 7.5 370 55 2 17 290 150 2
minepump_spec2_product14_true-unreach-call_false-termination.cil.c .17 29 1.1  2 870    1000 7400   0 5.9 320 48 2 3.9 280 33 2 4.3 270 36 2 420    170 6000   0 900    6600 10000   0 900     6600 12000    0 9.5 450 71 2 900    3400 9000   0 8.0 400 69 2 9.8 510 84 2 7.7 410 60 2 17 290 130 2
minepump_spec2_product15_true-unreach-call_false-termination.cil.c .17 27 1.2  2 870    930 4400   0 6.6 350 52 2 4.5 280 37 2 5.1 280 45 2 530    190 7200   0 900    7600 12000   0 900     7500 13000    0 8.5 450 66 2 900    3000 10000   0 7.6 370 65 2 21   760 180 2 7.8 370 57 2 18 290 140 2
minepump_spec2_product16_true-unreach-call_false-termination.cil.c .14 27 1.1  2 870    1000 6900   0 7.2 370 60 2 4.5 290 43 2 4.9 280 36 2 490    190 7100   0 900    6000 11000   0 900     6000 10000    0 8.7 440 71 2 900    3100 9600   0 8.4 440 72 2 900   1600 14000 0 8.3 450 69 2 19 290 130 2
minepump_spec2_product17_true-unreach-call_false-termination.cil.c .14 27 1.5  2 870    940 4900   0 5.9 330 56 2 4.4 280 43 2 4.1 270 37 2 270    150 3600   0 900    7500 9400   0 900     7400 12000    0 8.4 440 70 2 900    3800 11000   0 8.1 390 62 2 9.0 480 72 2 7.6 400 57 2 18 290 130 2
minepump_spec2_product18_true-unreach-call_false-termination.cil.c .15 27 1.3  2 870    970 6100   0 6.9 350 49 2 4.7 280 48 2 4.3 270 43 2 420    170 5200   0 900    7600 11000   0 900     7700 13000    0 8.3 440 67 2 900    3600 9900   0 7.7 400 67 2 900   1300 12000 0 7.6 400 60 2 18 290 130 2
minepump_spec2_product19_true-unreach-call_false-termination.cil.c .17 27 1.4  2 870    940 4300   0 6.6 330 56 2 4.8 280 44 2 4.9 280 42 2 480    200 6000   0 900    5800 9200   0 900     5900 10000    0 8.1 450 63 2 900    3100 10000   0 7.9 360 67 2 15   650 130 2 7.4 360 63 2 17 290 130 2
minepump_spec2_product20_true-unreach-call_false-termination.cil.c .15 27 1.3  2 870    990 5500   0 7.1 380 58 2 5.1 290 45 2 4.6 270 39 2 460    200 6100   0 900    6300 12000   0 900     6200 10000    0 9.3 450 68 2 900    3100 8300   0 8.2 450 65 2 19   660 180 2 8.2 450 73 2 18 290 150 2
minepump_spec2_product21_true-unreach-call_false-termination.cil.c .16 28 1.2  2 870    950 5300   0 6.2 310 52 2 4.3 290 41 2 4.4 270 36 2 5.6  280 53   2 900    5600 11000   0 .21  29 1.9  2 8.2 440 68 2 900    3400 8300   0 7.9 400 59 2 14   590 130 2 7.9 410 64 2 18 290 130 2
minepump_spec2_product22_true-unreach-call_false-termination.cil.c .16 28 1.5  2 870    950 4100   0 6.4 350 48 2 4.7 290 39 2 4.4 270 39 2 490    220 6300   0 900    5800 12000   0 900     5700 11000    0 8.5 450 66 2 900    3300 11000   0 8.5 470 71 2 9.1 420 74 2 8.3 480 67 2 18 290 140 2
minepump_spec2_product23_true-unreach-call_false-termination.cil.c .19 28 1.3  2 870    910 5100   0 6.4 340 62 2 5.6 300 51 2 4.8 280 38 2 640    250 7800   0 900    6200 9800   0 900     6200 9800    0 8.5 430 69 2 900    2800 9800   0 7.5 380 59 2 17   650 160 2 7.5 380 67 2 19 290 140 2
minepump_spec2_product24_true-unreach-call_false-termination.cil.c .19 28 1.5  2 870    1000 6200   0 7.2 430 60 2 6.6 370 64 2 4.6 270 37 2 560    260 7000   0 900    6700 13000   0 900     6700 13000    0 8.2 450 65 2 900    2900 9900   0 8.5 470 70 2 900   1400 11000 0 7.9 460 66 2 19 290 150 2
minepump_spec2_product25_true-unreach-call_false-termination.cil.c .15 27 1.0  2 870    940 4400   0 6.2 320 48 2 4.4 280 41 2 4.2 270 38 2 260    150 3200   0 900    7400 11000   0 900     7400 11000    0 8.5 450 66 2 900    3500 7100   0 8.4 410 68 2 900   1600 9200 0 7.8 390 62 2 18 300 140 2
minepump_spec2_product26_true-unreach-call_false-termination.cil.c .17 27 1.1  2 870    980 5500   0 6.5 350 54 2 4.7 290 41 2 4.4 270 39 2 440    180 6700   0 900    6600 9900   0 900     6600 10000    0 8.4 440 65 2 900    3600 8500   0 8.4 450 62 2 8.1 360 63 2 8.7 460 70 2 18 290 130 2
minepump_spec2_product27_true-unreach-call_false-termination.cil.c .15 29 1.6  2 870    940 6300   0 6.6 340 53 2 4.7 280 43 2 5.1 280 41 2 460    200 5600   0 900    5700 11000   0 900     5700 12000    0 8.4 450 68 2 900    3000 8800   0 8.0 380 66 2 20   670 170 2 7.8 370 62 2 18 290 150 2
minepump_spec2_product28_true-unreach-call_false-termination.cil.c .17 28 1.2  2 870    970 5200   0 6.9 380 64 2 4.9 290 48 2 4.6 280 43 2 470    210 5900   0 900    8000 12000   0 900     7900 11000    0 8.2 440 68 2 900    3100 9900   0 7.8 380 59 2 14   580 110 2 7.6 370 59 2 18 290 150 2
minepump_spec2_product29_true-unreach-call_false-termination.cil.c .16 28 1.3  2 870    940 5100   0 6.2 320 53 2 4.3 280 39 2 4.5 270 36 2 5.5  290 50   2 900    7600 12000   0 .19  29 2.3  2 8.2 450 67 2 900    3300 9300   0 7.8 400 64 2 11   500 94 2 7.8 410 58 2 18 280 130 2
minepump_spec2_product30_true-unreach-call_false-termination.cil.c .16 28 1.3  2 870    980 5800   0 7.1 350 61 2 4.5 290 38 2 4.5 270 34 2 480    220 5700   0 900    5700 12000   0 900     5700 13000    0 8.2 450 67 2 900    3300 9400   0 7.7 420 61 2 8.9 500 76 2 8.0 420 62 2 18 310 140 2
minepump_spec2_product31_true-unreach-call_false-termination.cil.c .19 28 1.3  2 870    930 4800   0 6.5 360 56 2 5.6 310 46 2 4.8 270 42 2 640    260 9800   0 900    6400 10000   0 900     6400 10000    0 8.5 430 63 2 900    2800 9900   0 8.1 460 65 2 15   630 120 2 8.6 450 68 2 19 290 140 2
minepump_spec2_product32_true-unreach-call_false-termination.cil.c .14 28 1.8  2 870    1000 5400   0 7.5 300 63 2 6.5 370 55 2 4.9 270 36 2 560    260 7000   0 900    7400 12000   0 900     7500 12000    0 9.5 450 74 2 900    2900 9900   0 7.7 380 66 2 16   670 140 2 7.7 390 58 2 18 290 150 2
minepump_spec2_product37_true-unreach-call_false-termination.cil.c .76 45 7.9  2 870    1300 11000   0 8.0 460 67 2 6.1 350 48 2 6.1 310 51 2 810    200 9500   0 900    3700 11000   0 900     3700 10000    0 62   2900 630 -16 900    3900 11000   0 18   740 150 2 34   990 370 2 880   5400 10000 2 37 490 320 2
minepump_spec2_product38_true-unreach-call_false-termination.cil.c .78 43 9.5  2 870    1400 8800   0 9.5 470 74 2 6.3 370 61 2 6.7 330 52 2 900    230 9000   0 900    3700 9400   0 900     3700 9400    0 67   3100 680 -16 900    3400 9300   0 19   730 150 2 900   1300 14000 0 900   5400 12000 0 37 490 320 2
minepump_spec2_product39_true-unreach-call_false-termination.cil.c 900    3300 9400    0 870    1400 6300   0 9.4 460 72 2 6.3 380 55 2 6.7 320 46 2 900    220 13000   0 900    3300 10000   0 900     3200 10000    0 120   3500 1500 -16 900    3100 12000   0 22   820 190 2 900   1300 13000 0 900   5300 11000 0 900 980 8100 0
minepump_spec2_product40_true-unreach-call_false-termination.cil.c 900    2700 9400    0 870    1600 6900   0 9.1 460 73 2 6.5 400 60 2 6.2 330 52 2 900    230 14000   0 900    3300 9900   0 900     3300 9800    0 320   4700 3800 -16 900    3300 11000   0 34   1000 310 2 900   1400 9900 0 900   3000 8800 0 900 990 9700 0
minepump_spec2_product45_true-unreach-call_false-termination.cil.c .20 29 1.5  2 870    1900 7300   0 7.9 450 67 2 7.7 430 66 2 5.4 290 39 2 7.9  330 70   2 900    3400 8600   0 .16  29 1.3  2 25   1200 220 2 900    4100 10000   0 17   740 140 2 15   680 120 2 130   3500 1600 2 27 490 230 2
minepump_spec2_product46_true-unreach-call_false-termination.cil.c .16 29 1.4  2 870    1900 6700   0 8.6 470 67 2 6.9 440 58 2 6.3 310 53 2 900    240 11000   0 900    3400 9600   0 900     3400 10000    0 26   1400 210 2 900    3600 8800   0 19   760 160 2 900   1900 11000 0 180   3600 2000 2 30 490 260 2
minepump_spec2_product47_true-unreach-call_false-termination.cil.c 900    3200 9500    0 870    1800 6700   0 8.3 460 66 2 6.9 440 55 2 6.2 320 48 2 900    240 11000   0 900    3000 11000   0 900     3000 10000    0 31   1400 240 2 900    3000 8200   0 17   690 140 2 900   1600 13000 0 130   3400 1600 2 900 900 7200 0
minepump_spec2_product48_true-unreach-call_false-termination.cil.c 900    2600 9600    0 870    2000 7100   0 8.8 460 67 2 7.6 440 63 2 6.0 310 48 2 900    250 11000   0 900    3300 11000   0 900     3300 9100    0 40   2600 340 2 900    3300 8100   0 29   1100 250 2 27   820 240 2 340   4500 3700 2 900 910 11000 0
minepump_spec2_product49_true-unreach-call_false-termination.cil.c 900    3300 10000    0 870    2500 6900   0 8.9 480 74 2 5.9 370 46 2 4.5 280 40 2 900    160 12000   0 900    3700 10000   0 900     3700 9600    0 100   4000 1100 -16 900    3900 7900   0 27   860 210 2 29   840 300 2 900   5300 12000 0 900 1000 7200 0
minepump_spec2_product50_true-unreach-call_false-termination.cil.c 900    3400 13000    0 870    2600 6400   0 9.8 460 76 2 6.4 410 50 2 4.9 280 41 2 900    190 10000   0 900    3600 11000   0 900     3600 11000    0 100   4000 1100 -16 900    3900 8200   0 26   690 230 2 900   1800 15000 0 900   5400 10000 0 900 1000 7900 0
minepump_spec2_product51_true-unreach-call_false-termination.cil.c 900    3200 9400    0 870    1400 6700   0 8.8 460 68 2 6.6 420 52 2 5.3 280 46 2 900    200 12000   0 900    3200 9100   0 900     3100 11000    0 140   4000 1700 -16 900    2900 9800   0 24   750 170 2 70   1400 800 2 730   5200 8800 2 900 870 7500 0
minepump_spec2_product52_true-unreach-call_false-termination.cil.c 900    2700 9000    0 870    1600 8300   0 10   470 78 2 6.8 450 57 2 5.3 280 45 2 900    200 11000   0 900    3300 11000   0 900     3300 11000    0 180   4000 2500 -16 900    3200 8400   0 34   930 250 2 900   1400 10000 0 900   2300 11000 0 900 870 9100 0
minepump_spec2_product53_true-unreach-call_false-termination.cil.c .86 54 9.5  2 870    2800 5900   0 8.7 470 71 2 6.4 390 48 2 4.7 280 40 2 900    270 14000   0 900    3300 9900   0 900     3400 11000    0 97   4000 1100 -16 900    3800 6300   0 19   710 140 2 23   740 210 2 900   4000 9400 0 45 490 500 2
minepump_spec2_product54_true-unreach-call_false-termination.cil.c .97 58 11    2 870    2800 6500   0 8.8 460 74 2 7.4 420 59 2 5.0 280 40 2 900    290 11000   0 900    3300 9700   0 900     3300 9700    0 100   4000 1100 -16 900    3900 8300   0 33   990 300 2 82   1600 960 2 900   1900 9800 0 45 500 410 2
minepump_spec2_product55_true-unreach-call_false-termination.cil.c 900    3400 9400    0 870    2500 5600   0 9.1 460 64 2 6.8 400 67 2 5.4 290 42 2 900    290 12000   0 900    3200 9800   0 900     3200 10000    0 210   3900 2500 -16 900    3000 10000   0 17   750 150 2 54   1300 540 2 900   2900 12000 0 900 890 9500 0
minepump_spec2_product56_true-unreach-call_false-termination.cil.c 900    2700 10000    0 870    2600 7300   0 9.7 460 81 2 7.3 440 57 2 5.1 280 43 2 900    290 13000   0 900    3100 7800   0 900     3100 10000    0 370   5500 4500 -16 900    3300 9500   0 27   870 210 2 900   1500 11000 0 900   2100 11000 0 900 900 8500 0
minepump_spec2_product57_true-unreach-call_false-termination.cil.c 900    2900 8900    0 870    1900 7100   0 8.3 450 63 2 7.5 440 64 2 4.8 270 39 2 900    180 12000   0 900    3400 9600   0 900     3400 12000    0 60   3500 570 2 900    4100 8200   0 34   920 270 2 900   1800 13000 0 350   2400 3600 2 900 960 7800 0
minepump_spec2_product58_true-unreach-call_false-termination.cil.c 900    2900 9100    0 870    1900 7500   0 9.3 480 87 2 7.5 440 57 2 4.8 280 44 2 900    200 9100   0 900    3200 10000   0 900     3100 11000    0 75   3800 820 2 900    3700 8100   0 34   1000 310 2 900   2100 12000 0 900   5200 12000 0 900 970 9100 0
minepump_spec2_product59_true-unreach-call_false-termination.cil.c 900    3300 10000    0 870    1900 6300   0 8.8 450 80 2 8.4 450 63 2 5.0 290 44 2 900    220 11000   0 900    3100 10000   0 900     3100 10000    0 62   3600 630 2 900    3000 12000   0 32   930 240 2 76   1600 980 2 600   3700 8100 2 900 620 8500 0
minepump_spec2_product60_true-unreach-call_false-termination.cil.c 900    2800 7400    0 870    1900 6700   0 10   460 81 2 8.0 440 65 2 5.3 280 44 2 900    210 13000   0 900    3000 11000   0 900     3000 13000    0 110   3800 1500 2 900    3300 9500   0 36   1100 330 2 900   1900 10000 0 900   1900 8700 0 900 630 10000 0
minepump_spec2_product61_true-unreach-call_false-termination.cil.c .23 30 2.3  2 870    3700 6500   0 7.7 460 63 2 7.1 440 67 2 4.9 280 40 2 6.8  290 68   2 900    3300 10000   0 .23  29 2.8  2 37   2100 330 2 900    4000 8000   0 29   880 230 2 14   630 140 2 290   2800 3700 2 30 510 260 2
minepump_spec2_product62_true-unreach-call_false-termination.cil.c .24 30 2.0  2 870    3700 8900   0 11   460 75 2 7.4 440 61 2 5.0 280 47 2 900    310 12000   0 900    3200 10000   0 900     3300 9500    0 41   2100 340 2 900    3700 8700   0 21   730 180 2 900   1700 12000 0 410   3300 5600 2 35 510 330 2
minepump_spec2_product63_true-unreach-call_false-termination.cil.c 900    3400 11000    0 870    3300 5600   0 8.4 450 70 2 7.8 440 67 2 5.0 280 44 2 900    300 8900   0 900    3200 9900   0 900     3200 9400    0 41   2500 390 2 900    3100 9500   0 18   750 140 2 900   1500 13000 0 250   2700 2800 2 900 880 7500 0
minepump_spec2_product64_true-unreach-call_false-termination.cil.c 900    2700 9500    0 870    3400 7600   0 11   510 92 2 8.5 440 62 2 5.1 280 42 2 900    320 11000   0 900    3300 9300   0 900     3300 12000    0 63   3800 700 2 900    3300 8900   0 19   770 140 2 21   730 200 2 900   5100 10000 0 900 890 7600 0
minepump_spec3_product33_true-unreach-call_false-termination.cil.c .15 28 1.1  2 870    2100 7100   0 6.6 330 57 2 4.9 290 46 2 5.3 280 43 2 7.8  330 65   2 900    3400 10000   0 .17  28 2.2  2 27   920 180 2 900    3800 7100   0 11   540 100 2 8.8 430 68 2 11   540 93 2 26 480 210 2
minepump_spec3_product34_true-unreach-call_false-termination.cil.c .16 30 1.1  2 870    2100 6900   0 7.0 330 52 2 5.4 300 46 2 5.6 310 48 2 680    180 8000   0 900    3400 11000   0 900     3300 12000    0 21   930 170 2 900    3500 9000   0 12   580 99 2 9.6 520 88 2 12   580 91 2 26 480 220 2
minepump_spec3_product37_true-unreach-call_false-termination.cil.c .15 28 1.7  2 870    1600 5900   0 6.7 350 54 2 5.0 290 47 2 6.2 320 49 2 8.0  340 73   2 900    3100 11000   0 .18  29 2.0  2 20   1000 150 2 900    4000 9900   0 20   740 160 2 900   2700 11000 0 470   4700 5500 2 32 480 310 2
minepump_spec3_product38_true-unreach-call_false-termination.cil.c .17 28 1.8  2 870    1600 7200   0 6.8 350 56 2 5.1 290 47 2 6.3 320 52 2 900    220 11000   0 900    3200 10000   0 900     3200 11000    0 21   900 160 2 900    3700 7400   0 18   710 140 2 900   1500 14000 0 20   560 150 2 33 510 300 2
minepump_spec3_product41_true-unreach-call_false-termination.cil.c .16 28 1.5  2 870    2500 4900   0 7.0 360 62 2 5.5 290 45 2 5.5 280 47 2 7.2  320 61   2 900    3500 10000   0 .18  29 2.4  2 32   1400 260 2 900    3600 7100   0 13   640 110 2 9.9 510 90 2 13   660 100 2 27 490 230 2
minepump_spec3_product42_true-unreach-call_false-termination.cil.c .16 28 1.4  2 870    2500 8800   0 7.1 400 61 2 5.1 290 48 2 6.2 280 45 2 830    190 9800   0 900    3400 12000   0 900     3400 12000    0 33   1300 280 2 900    3500 11000   0 14   600 110 2 900   1900 10000 0 15   670 110 2 28 450 230 2
minepump_spec3_product45_true-unreach-call_false-termination.cil.c .16 30 1.8  2 870    2000 8500   0 7.0 380 55 2 5.9 310 45 2 5.9 290 46 2 8.4  330 79   2 900    3400 9200   0 .18  28 2.1  2 33   1600 290 2 900    4100 7200   0 20   730 170 2 900   1900 14000 0 380   2500 4200 2 34 490 360 2
minepump_spec3_product46_true-unreach-call_false-termination.cil.c .19 28 1.5  2 870    2000 6000   0 7.5 410 64 2 7.1 370 69 2 6.6 310 54 2 900    230 13000   0 900    3100 9700   0 900     3100 11000    0 36   1700 300 2 900    3700 8300   0 22   770 180 2 900   2800 10000 0 22   790 180 2 34 500 330 2
minepump_spec3_product49_true-unreach-call_false-termination.cil.c .67 42 7.3  2 870    1700 7400   0 6.3 350 51 2 4.9 290 43 2 4.6 270 37 2 900    120 13000   0 900    3500 9800   0 900     3600 13000    0 19   940 170 2 900    4000 8300   0 21   750 150 2 900   2100 12000 0 300   4600 4000 2 900 660 8000 0
minepump_spec3_product50_true-unreach-call_false-termination.cil.c .72 39 8.5  2 870    1700 8000   0 6.6 340 56 2 5.4 300 46 2 5.0 290 38 2 900    130 12000   0 900    3200 10000   0 900     3200 11000    0 20   1000 150 2 900    3600 9800   0 22   870 180 2 900   4100 10000 0 23   850 190 2 900 680 8800 0
minepump_spec3_product53_true-unreach-call_false-termination.cil.c .87 48 11    2 870    2500 5600   0 6.6 360 55 2 5.1 290 39 2 4.9 280 41 2 900    150 12000   0 900    3500 9900   0 900     3600 9100    0 32   1200 260 2 900    3800 7300   0 20   750 160 2 900   2500 11000 0 900   5400 10000 0 900 870 8200 0
minepump_spec3_product54_true-unreach-call_false-termination.cil.c 1.0  50 14    2 870    2500 6600   0 6.8 360 63 2 5.6 290 51 2 5.1 280 46 2 900    180 11000   0 900    3300 9800   0 900     3300 9500    0 35   1400 280 2 900    3900 9600   0 24   790 190 2 900   1600 12000 0 900   3200 12000 0 900 880 7700 0
minepump_spec3_product57_true-unreach-call_false-termination.cil.c 900    2700 9800    0 870    2000 7200   0 7.6 400 56 2 5.9 320 50 2 4.9 280 37 2 890    110 14000   0 900    3000 12000   0 900     3000 10000    0 19   910 150 2 900    3800 7100   0 23   790 190 2 900   1300 11000 0 900   5100 11000 0 900 810 8600 0
minepump_spec3_product58_true-unreach-call_false-termination.cil.c 900    2800 13000    0 870    2000 6100   0 7.5 450 66 2 6.9 380 65 2 5.2 280 40 2 900    120 11000   0 900    3000 13000   0 900     2900 13000    0 23   960 170 2 900    3800 11000   0 24   870 210 2 900   1200 12000 0 25   850 220 2 900 650 7300 0
minepump_spec3_product61_true-unreach-call_false-termination.cil.c 900    2800 8900    0 870    3300 5500   0 7.4 390 60 2 5.8 320 46 2 5.0 290 44 2 900    150 11000   0 900    3400 13000   0 900     3400 9500    0 42   1700 300 2 900    3900 8000   0 26   840 190 2 41   1300 480 2 900   2400 13000 0 900 780 8300 0
minepump_spec3_product62_true-unreach-call_false-termination.cil.c 900    2800 10000    0 870    3300 7400   0 7.7 450 64 2 6.9 400 57 2 5.2 280 47 2 900    170 13000   0 900    3100 10000   0 900     3100 10000    0 36   1800 330 2 900    3800 7000   0 28   880 230 2 900   1700 13000 0 900   2100 12000 0 900 790 7600 0
minepump_spec4_product01_true-unreach-call_false-termination.cil.c .16 26 .94 2 870    880 4200   0 3.8 310 33 2 3.4 270 26 2 3.8 260 36 2 5.3  280 45   2 900    7000 9400   0 .12  28 1.0  2 8.2 440 72 2 900    2500 7700   0 7.4 380 64 2 7.9 470 68 2 7.6 400 55 2 17 290 130 2
minepump_spec4_product02_true-unreach-call_false-termination.cil.c .12 27 1.3  2 870    950 4800   0 4.1 290 33 2 3.3 270 27 2 4.0 260 34 2 5.3  270 47   2 900    7600 11000   0 .11  28 1.1  2 8.6 440 70 2 900    3000 9300   0 8.0 440 58 2 7.8 460 62 2 8.1 430 72 2 17 290 120 2
minepump_spec4_product03_true-unreach-call_false-termination.cil.c .15 27 1.1  2 870    930 4100   0 4.5 290 41 2 3.4 270 32 2 4.7 280 42 2 430    160 4800   0 900    5400 8400   0 900     5500 11000    0 9.1 460 71 2 900    2200 9500   0 9.6 540 81 2 8.2 390 61 2 9.5 530 72 2 17 290 130 2
minepump_spec4_product04_true-unreach-call_false-termination.cil.c .14 27 1.0  2 870    890 3800   0 4.3 310 41 2 3.3 270 29 2 4.5 270 34 2 440    160 5700   0 900    7100 11000   0 900     7100 10000    0 7.9 440 64 2 900    2300 11000   0 9.4 530 74 2 8.4 450 78 2 9.3 520 72 2 17 280 140 2
minepump_spec4_product05_true-unreach-call_false-termination.cil.c .14 29 1.3  2 870    810 4200   0 4.3 310 36 2 3.8 300 35 2 4.2 260 36 2 370    130 5600   0 900    5700 11000   0 900     5700 10000    0 8.4 440 65 2 900    3500 8900   0 9.9 520 78 2 8.3 360 66 2 8.6 500 65 2 17 290 130 2
minepump_spec4_product06_true-unreach-call_false-termination.cil.c .17 27 1.1  2 870    990 6800   0 4.5 310 41 2 3.8 280 35 2 4.2 270 36 2 420    150 4900   0 900    7400 10000   0 900     7400 9900    0 9.2 450 73 2 900    3400 9200   0 10   530 85 2 13   580 110 2 11   540 95 2 17 300 140 2
minepump_spec4_product07_true-unreach-call_false-termination.cil.c .17 27 1.0  2 870    960 4300   0 4.6 310 35 2 4.0 270 33 2 4.8 270 41 2 540    180 5900   0 900    5600 11000   0 900     5600 11000    0 9.0 450 61 2 900    2800 8800   0 11   550 82 2 38   1000 390 2 10   550 90 2 17 290 130 2
minepump_spec4_product08_true-unreach-call_false-termination.cil.c .16 27 1.0  2 870    890 4600   0 4.3 290 39 2 3.9 280 39 2 4.8 280 39 2 540    180 8000   0 900    5700 9400   0 900     5800 13000    0 8.4 440 67 2 900    3000 11000   0 12   540 96 2 20   790 220 2 11   530 97 2 18 290 150 2
minepump_spec4_product09_true-unreach-call_false-termination.cil.c .13 27 .99 2 870    890 4500   0 4.1 290 37 2 3.3 270 29 2 3.8 260 34 2 5.2  270 43   2 900    5300 10000   0 .12  28 .96 2 8.0 430 58 2 900    2800 9500   0 11   490 95 2 8.3 470 64 2 8.6 480 77 2 17 280 130 2
minepump_spec4_product10_true-unreach-call_false-termination.cil.c .16 27 1.0  2 870    950 4800   0 4.0 310 33 2 3.2 270 32 2 4.1 270 36 2 5.2  270 46   2 900    5700 11000   0 .096 28 1.2  2 8.8 450 70 2 900    3000 8200   0 8.1 430 61 2 7.7 460 64 2 8.4 440 62 2 17 290 130 2
minepump_spec4_product11_true-unreach-call_false-termination.cil.c .15 27 1.1  2 870    930 4700   0 4.2 290 34 2 3.3 270 30 2 4.6 270 33 2 430    150 6100   0 900    7300 11000   0 900     7300 12000    0 8.2 430 70 2 900    2300 10000   0 9.3 520 78 2 8.0 440 69 2 9.2 530 74 2 17 290 120 2
minepump_spec4_product12_true-unreach-call_false-termination.cil.c .14 27 1.0  2 870    880 4800   0 4.0 300 31 2 3.4 280 26 2 4.5 270 35 2 420    160 6200   0 900    7500 11000   0 900     7500 11000    0 8.3 430 60 2 900    2300 10000   0 9.5 530 83 2 8.5 480 72 2 9.8 520 82 2 18 280 140 2
minepump_spec4_product13_true-unreach-call_false-termination.cil.c .17 27 1.0  2 870    800 3200   0 4.4 290 41 2 3.9 280 31 2 4.0 260 34 2 370    130 5600   0 900    5700 10000   0 900     5800 11000    0 8.5 460 70 2 900    3600 8300   0 8.6 510 74 2 7.7 410 65 2 11   540 80 2 17 280 120 2
minepump_spec4_product14_true-unreach-call_false-termination.cil.c .14 29 1.4  2 870    930 5100   0 4.3 290 36 2 3.7 280 36 2 4.3 270 40 2 420    150 6300   0 900    5900 11000   0 900     6000 13000    0 8.7 440 76 2 900    3300 10000   0 10   540 80 2 12   580 110 2 10   510 76 2 18 290 130 2
minepump_spec4_product15_true-unreach-call_false-termination.cil.c .14 27 1.1  2 870    950 5000   0 4.6 310 38 2 4.1 280 38 2 4.8 280 39 2 540    180 7700   0 900    6000 12000   0 900     6100 11000    0 9.0 450 70 2 900    2800 11000   0 11   520 90 2 11   560 85 2 11   540 96 2 17 290 120 2
minepump_spec4_product16_true-unreach-call_false-termination.cil.c .16 29 1.1  2 870    910 5600   0 4.3 310 34 2 4.0 280 37 2 4.6 280 37 2 540    190 6200   0 900    5400 10000   0 900     5400 11000    0 8.7 430 65 2 900    2900 9100   0 11   530 92 2 10   530 88 2 11   540 87 2 17 290 140 2
minepump_spec4_product17_true-unreach-call_false-termination.cil.c .15 27 1.3  2 870    810 4800   0 4.4 290 38 2 3.6 270 32 2 3.9 260 30 2 270    130 3200   0 900    6700 9700   0 900     6700 11000    0 8.7 440 69 2 900    2900 9300   0 8.8 500 71 2 8.3 360 64 2 9.8 520 83 2 18 290 130 2
minepump_spec4_product18_true-unreach-call_false-termination.cil.c .13 27 1.6  2 870    940 5100   0 4.5 290 37 2 3.9 280 37 2 4.4 270 37 2 450    170 5500   0 900    7100 11000   0 900     7200 11000    0 8.9 440 73 2 900    2800 9900   0 11   520 97 2 9.6 480 75 2 12   520 98 2 17 290 130 2
minepump_spec4_product19_true-unreach-call_false-termination.cil.c .16 27 1.2  2 870    950 4300   0 4.5 290 39 2 4.0 280 34 2 4.9 280 37 2 460    190 5700   0 900    5500 12000   0 900     5400 11000    0 8.5 440 69 2 900    2500 10000   0 11   560 100 2 17   650 140 2 11   530 87 2 18 290 140 2
minepump_spec4_product20_true-unreach-call_false-termination.cil.c .15 27 1.1  2 870    920 5200   0 4.1 290 36 2 3.9 280 38 2 4.6 280 36 2 450    250 6600   0 900    5700 13000   0 900     5700 11000    0 8.3 440 69 2 900    2600 11000   0 11   530 88 2 30   910 290 2 11   530 90 2 17 280 140 2
minepump_spec4_product21_true-unreach-call_false-termination.cil.c .16 28 1.1  2 870    790 5100   0 4.7 290 42 2 4.0 280 36 2 4.1 270 39 2 270    170 3600   0 900    5900 12000   0 900     5800 11000    0 8.7 460 70 2 900    3000 9700   0 9.3 530 79 2 17   670 140 2 9.4 520 78 2 18 290 140 2
minepump_spec4_product22_true-unreach-call_false-termination.cil.c .18 28 1.3  2 870    990 6800   0 4.4 310 36 2 4.0 280 35 2 4.3 270 37 2 470    210 5900   0 900    7500 13000   0 900     7500 12000    0 8.3 430 65 2 900    2900 8900   0 11   570 93 2 16   700 150 2 11   540 91 2 18 290 160 2
minepump_spec4_product23_true-unreach-call_false-termination.cil.c .18 28 1.2  2 870    960 5200   0 4.7 290 39 2 4.6 280 42 2 4.8 270 39 2 520    240 6400   0 900    5100 13000   0 900     5100 9300    0 8.2 430 62 2 900    2500 9800   0 11   590 100 2 900   1400 13000 0 12   560 97 2 18 290 140 2
minepump_spec4_product24_true-unreach-call_false-termination.cil.c .17 28 1.3  2 870    940 7700   0 4.5 290 38 2 5.7 310 47 2 4.5 280 37 2 550    240 8000   0 900    5000 12000   0 900     5000 10000    0 8.4 430 63 2 900    2600 11000   0 11   540 99 2 25   810 260 2 11   560 110 2 18 290 140 2
minepump_spec4_product25_true-unreach-call_false-termination.cil.c .14 27 1.1  2 870    780 5400   0 4.4 290 34 2 3.7 270 34 2 4.0 260 34 2 240    140 3400   0 900    6800 11000   0 900     6800 10000    0 8.4 450 64 2 900    2900 11000   0 9.0 520 73 2 13   630 120 2 9.3 510 74 2 17 290 130 2
minepump_spec4_product26_true-unreach-call_false-termination.cil.c .17 27 1.1  2 870    960 4900   0 4.4 290 43 2 3.8 280 31 2 4.5 270 33 2 460    170 7100   0 900    7200 10000   0 900     7200 13000    0 8.2 460 67 2 900    2800 11000   0 11   560 91 2 8.4 370 71 2 11   550 82 2 17 290 130 2
minepump_spec4_product27_true-unreach-call_false-termination.cil.c .15 28 1.2  2 870    980 7800   0 4.5 290 37 2 3.8 280 32 2 4.6 270 40 2 460    190 5500   0 900    6800 12000   0 900     6800 13000    0 8.9 450 77 2 900    2500 9900   0 11   560 89 2 29   930 290 2 11   540 90 2 18 290 150 2
minepump_spec4_product28_true-unreach-call_false-termination.cil.c .16 27 1.0  2 870    890 5700   0 4.3 290 36 2 3.8 280 31 2 4.5 270 40 2 450    190 5400   0 900    5300 10000   0 900     5300 10000    0 9.2 460 68 2 900    2600 11000   0 12   540 91 2 11   550 92 2 11   530 90 2 18 290 140 2
minepump_spec4_product29_true-unreach-call_false-termination.cil.c .18 28 1.3  2 870    790 5200   0 4.6 290 39 2 4.0 280 37 2 4.0 260 31 2 270    170 3700   0 900    5600 10000   0 900     5600 11000    0 9.2 450 73 2 900    3000 12000   0 9.4 520 68 2 16   670 120 2 8.8 520 69 2 18 290 140 2
minepump_spec4_product30_true-unreach-call_false-termination.cil.c .16 30 1.3  2 870    970 6500   0 4.4 290 34 2 3.9 280 35 2 4.4 280 40 2 450    210 5500   0 900    7300 10000   0 900     7400 10000    0 8.4 430 65 2 900    2900 10000   0 12   560 87 2 13   640 110 2 12   560 91 2 18 300 140 2
minepump_spec4_product31_true-unreach-call_false-termination.cil.c .16 28 1.3  2 870    960 6000   0 4.7 310 42 2 4.6 290 43 2 4.6 270 41 2 530    240 6500   0 900    5000 10000   0 900     5000 12000    0 8.6 450 74 2 900    2500 9200   0 11   550 89 2 20   680 180 2 11   550 98 2 18 290 150 2
minepump_spec4_product32_true-unreach-call_false-termination.cil.c .17 30 1.2  2 870    870 4300   0 4.4 290 37 2 5.8 310 53 2 4.6 280 36 2 560    240 6200   0 900    5600 9900   0 900     5600 9500    0 8.4 430 68 2 900    2600 11000   0 12   550 100 2 11   520 92 2 11   540 86 2 18 290 130 2
minepump_spec4_product49_true-unreach-call_false-termination.cil.c .63 41 7.4  2 870    1500 10000   0 7.5 460 63 2 5.2 300 48 2 4.8 270 39 2 900    170 11000   0 900    3500 11000   0 900     3600 11000    0 17   690 130 2 900    4100 7200   0 18   740 150 2 900   1200 12000 0 42   1300 440 2 53 490 550 2
minepump_spec4_product50_true-unreach-call_false-termination.cil.c .67 42 7.7  2 870    1500 6800   0 7.9 450 60 2 5.4 310 43 2 5.2 280 43 2 900    190 12000   0 900    3200 11000   0 900     3200 10000    0 17   810 130 2 900    3700 11000   0 24   860 190 2 23   850 240 2 120   2800 1300 2 53 470 550 2
minepump_spec4_product51_true-unreach-call_false-termination.cil.c 900    3000 10000    0 870    1400 7100   0 8.1 410 58 2 5.8 330 57 2 4.9 280 41 2 900    200 10000   0 900    2900 10000   0 900     2900 10000    0 22   940 180 2 900    3000 9000   0 22   790 180 2 57   1300 620 2 69   1500 580 2 900 690 7700 0
minepump_spec4_product52_true-unreach-call_false-termination.cil.c 900    2400 12000    0 870    1600 7800   0 8.4 450 67 2 5.6 330 53 2 5.1 280 42 2 900    190 13000   0 900    3100 9900   0 900     3100 11000    0 29   1100 220 2 900    3200 10000   0 21   760 190 2 39   1000 370 2 130   3300 1600 2 900 700 7500 0
minepump_spec4_product53_true-unreach-call_false-termination.cil.c .73 52 7.6  2 870    2400 6100   0 8.1 470 72 2 5.8 350 46 2 4.7 280 37 2 900    230 12000   0 900    3300 12000   0 900     3200 9800    0 21   940 180 2 900    3800 9200   0 24   860 200 2 20   740 170 2 250   2000 2900 2 62 500 620 2
minepump_spec4_product54_true-unreach-call_false-termination.cil.c .65 52 7.0  2 870    2400 6700   0 8.8 450 70 2 5.7 350 52 2 4.8 280 43 2 900    250 13000   0 900    3500 10000   0 900     3400 9000    0 21   910 170 2 900    3800 8400   0 27   810 220 2 20   770 200 2 460   4800 5100 2 62 500 650 2
minepump_spec4_product55_true-unreach-call_false-termination.cil.c 900    3200 11000    0 870    2500 6100   0 7.8 450 62 2 6.3 400 57 2 5.3 280 46 2 900    270 12000   0 900    3100 11000   0 900     3000 10000    0 26   1300 210 2 900    2900 10000   0 26   860 250 2 65   1300 770 2 180   3300 2000 2 900 870 8500 0
minepump_spec4_product56_true-unreach-call_false-termination.cil.c 900    2500 11000    0 870    2500 5900   0 9.1 330 85 2 5.9 360 52 2 5.0 290 40 2 900    250 12000   0 900    3200 12000   0 900     3200 11000    0 33   1300 250 2 900    3200 7800   0 32   1000 270 2 140   2500 1700 2 900   2000 9500 0 900 880 7300 0
minepump_spec4_product57_true-unreach-call_false-termination.cil.c .54 43 5.9  2 870    1900 6600   0 8.2 450 64 2 6.3 360 57 2 4.6 270 42 2 900    180 14000   0 900    3100 8600   0 900     3100 11000    0 32   1400 250 2 900    3600 7300   0 20   770 150 2 26   870 270 2 79   1600 860 2 61 510 580 2
minepump_spec4_product58_true-unreach-call_false-termination.cil.c .65 45 7.3  2 870    1900 6300   0 8.3 450 60 2 6.4 380 52 2 4.8 280 36 2 900    190 11000   0 900    2900 9300   0 900     2900 13000    0 33   1400 240 2 900    3500 7800   0 29   860 230 2 900   2000 12000 0 250   3600 2500 2 61 500 600 2
minepump_spec4_product59_true-unreach-call_false-termination.cil.c 900    3100 10000    0 870    1900 5600   0 8.2 450 76 2 6.9 450 59 2 4.9 280 45 2 900    210 12000   0 900    2900 9400   0 900     2900 11000    0 32   1600 240 2 900    3000 12000   0 25   850 220 2 65   1200 760 2 79   1600 750 2 900 840 9100 0
minepump_spec4_product60_true-unreach-call_false-termination.cil.c 900    2400 9600    0 870    1900 8800   0 9.7 450 72 2 6.7 410 54 2 5.2 280 42 2 900    200 13000   0 900    2700 10000   0 900     2700 11000    0 34   2200 300 2 900    3200 8800   0 26   880 190 2 64   1300 740 2 800   5400 9100 2 900 600 7300 0
minepump_spec4_product61_true-unreach-call_false-termination.cil.c .71 57 9.7  2 870    3200 5300   0 8.1 440 69 2 6.8 440 64 2 4.7 270 41 2 900    250 11000   0 900    3300 9700   0 900     3300 10000    0 32   1200 230 2 900    4000 8700   0 18   750 150 2 900   2400 11000 0 160   3000 1800 2 66 510 720 2
minepump_spec4_product62_true-unreach-call_false-termination.cil.c .81 61 9.9  2 870    3200 6100   0 8.5 450 69 2 7.3 430 55 2 4.9 280 37 2 900    260 12000   0 900    3200 9700   0 900     3200 11000    0 31   1400 200 2 900    3700 8600   0 27   900 210 2 900   1600 10000 0 270   3500 3800 2 66 500 660 2
minepump_spec4_product63_true-unreach-call_false-termination.cil.c 900    3300 11000    0 870    3300 6000   0 8.3 450 65 2 7.0 430 56 2 5.0 280 45 2 900    280 12000   0 900    2800 11000   0 900     2900 9600    0 31   1600 240 2 900    3000 11000   0 29   860 230 2 900   2500 12000 0 400   3900 5300 2 900 800 7500 0
minepump_spec4_product64_true-unreach-call_false-termination.cil.c 900    2700 10000    0 870    3300 8600   0 9.6 450 70 2 6.9 420 56 2 5.0 280 39 2 900    260 12000   0 900    3100 11000   0 900     3100 9900    0 36   2100 290 2 900    3200 11000   0 35   870 250 2 45   1100 460 2 900   5400 11000 0 900 800 7800 0
minepump_spec5_product01_true-unreach-call_false-termination.cil.c .15 27 1.0  2 870    910 5400   0 4.0 300 37 2 3.4 280 35 2 4.3 270 37 2 5.5  280 54   2 900    5100 11000   0 .14  28 .79 2 9.7 450 84 2 .18 11 2.1 2 6.6 310 54 2 900   1300 12000 0 7.0 320 53 2 18 290 150 2
minepump_spec5_product02_true-unreach-call_false-termination.cil.c .16 27 1.1  2 870    970 6700   0 4.0 300 38 2 3.4 270 28 2 4.5 270 37 2 5.3  280 51   2 900    5400 13000   0 .11  28 1.0  2 12   470 97 2 900    3300 6900   0 7.6 360 63 2 900   1200 14000 0 7.3 360 64 2 17 290 150 2
minepump_spec5_product03_true-unreach-call_false-termination.cil.c .16 27 1.0  2 870    970 6600   0 4.3 290 42 2 3.3 270 31 2 4.8 280 41 2 6.0  290 55   2 900    5100 11000   0 .11  28 1.2  2 10   460 87 2 900    2400 9800   0 7.4 350 57 2 6.3 330 52 2 7.6 360 63 2 17 290 120 2
minepump_spec5_product04_true-unreach-call_false-termination.cil.c .13 29 1.4  2 870    830 5300   0 4.4 290 37 2 3.4 290 36 2 4.9 280 41 2 5.7  280 57   2 900    6300 12000   0 .11  28 1.0  2 10   450 82 2 .17 11 1.7 2 8.1 430 60 2 6.4 340 51 2 8.1 420 68 2 17 290 150 2
minepump_spec5_product05_true-unreach-call_false-termination.cil.c .15 27 1.1  2 870    790 5100   0 4.4 310 35 2 4.0 280 33 2 4.2 270 34 2 5.4  280 49   2 900    5900 9800   0 .11  28 1.1  2 10   450 79 2 900    3600 10000   0 8.0 400 65 2 900   1400 11000 0 8.0 400 61 2 18 290 140 2
minepump_spec5_product06_true-unreach-call_false-termination.cil.c .14 27 1.3  2 870    940 4800   0 4.3 310 44 2 4.0 280 40 2 4.3 270 37 2 5.7  290 55   2 900    7100 11000   0 .18  28 1.6  2 12   480 90 2 900    3500 8400   0 7.8 410 65 2 7.7 420 63 2 7.9 420 64 2 18 290 140 2
minepump_spec5_product07_true-unreach-call_false-termination.cil.c .17 27 1.1  2 870    930 5100   0 4.8 290 39 2 4.3 280 33 2 5.0 280 44 2 6.1  300 59   2 900    6600 11000   0 .20  28 1.9  2 11   470 82 2 900    2900 9800   0 8.3 460 73 2 8.7 510 71 2 8.3 460 61 2 18 300 130 2
minepump_spec5_product08_true-unreach-call_false-termination.cil.c .15 27 1.4  2 870    840 4500   0 4.4 310 34 2 4.0 270 34 2 4.6 280 40 2 5.7  280 52   2 900    6400 12000   0 .17  28 2.0  2 12   470 91 2 900    3100 10000   0 7.5 370 62 2 8.9 480 79 2 7.5 380 63 2 18 290 140 2
minepump_spec5_product09_true-unreach-call_false-termination.cil.c .16 27 1.1  2 870    910 4400   0 4.1 290 33 2 3.4 280 30 2 4.0 260 37 2 5.5  280 46   2 900    6500 11000   0 .091 28 1.1  2 9.7 460 81 2 900    3500 9200   0 7.2 330 58 2 900   1400 11000 0 7.1 330 54 2 17 290 120 2
minepump_spec5_product10_true-unreach-call_false-termination.cil.c .14 27 1.2  2 870    930 4500   0 4.1 310 34 2 3.2 270 27 2 4.4 270 39 2 5.4  280 49   2 900    5900 13000   0 .092 28 1.0  2 11   460 90 2 .20 11 2.0 2 7.6 370 61 2 900   1300 12000 0 7.4 370 60 2 18 290 120 2
minepump_spec5_product11_true-unreach-call_false-termination.cil.c .14 27 1.0  2 870    920 4600   0 4.4 290 39 2 3.5 270 28 2 5.0 280 43 2 5.9  300 49   2 900    6400 9100   0 .10  28 1.2  2 11   470 85 2 900    2400 9400   0 11   490 70 2 6.1 330 52 2 7.8 420 57 2 18 300 130 2
minepump_spec5_product12_true-unreach-call_false-termination.cil.c .14 27 1.1  2 870    820 4400   0 4.3 290 33 2 3.3 280 30 2 4.7 280 37 2 5.9  290 63   2 900    7400 10000   0 .098 28 .92 2 12   480 87 2 .19 11 2.2 2 8.1 430 60 2 900   1500 12000 0 7.9 430 68 2 18 290 150 2
minepump_spec5_product13_true-unreach-call_false-termination.cil.c .16 27 1.2  2 870    790 4200   0 4.3 300 36 2 3.9 280 35 2 4.2 270 39 2 5.5  280 48   2 900    4700 12000   0 .11  28 1.2  2 11   470 86 2 900    3500 7400   0 7.8 410 64 2 900   1600 12000 0 7.9 400 64 2 18 300 140 2
minepump_spec5_product14_true-unreach-call_false-termination.cil.c .17 27 1.1  2 870    940 5100   0 4.4 290 38 2 3.9 280 36 2 4.5 270 41 2 5.6  290 53   2 900    5300 10000   0 .18  28 1.7  2 10   470 88 2 900    3400 10000   0 8.3 460 64 2 8.0 470 62 2 7.9 470 71 2 18 280 130 2
minepump_spec5_product15_true-unreach-call_false-termination.cil.c .16 27 1.1  2 870    920 4900   0 4.8 310 39 2 4.2 280 33 2 4.7 280 45 2 6.3  300 52   2 900    5000 13000   0 .18  29 2.0  2 11   460 79 2 900    2900 11000   0 8.5 480 63 2 9.2 550 75 2 8.3 460 66 2 18 290 150 2
minepump_spec5_product16_true-unreach-call_false-termination.cil.c .15 27 1.2  2 870    840 4700   0 4.3 290 38 2 3.9 280 36 2 5.0 280 40 2 6.2  300 61   2 900    4800 10000   0 .19  28 2.2  2 10   460 82 2 900    3000 12000   0 8.7 460 65 2 8.9 480 75 2 8.9 460 64 2 18 290 150 2
minepump_spec5_product17_true-unreach-call_false-termination.cil.c .15 27 1.1  2 870    800 5100   0 4.6 300 37 2 3.9 280 33 2 4.2 270 33 2 5.4  280 48   2 900    4600 12000   0 .11  28 1.1  2 10   470 90 2 900    3500 11000   0 9.7 430 75 2 900   1500 12000 0 7.9 400 73 2 18 290 140 2
minepump_spec5_product18_true-unreach-call_false-termination.cil.c .16 28 1.2  2 870    960 5800   0 4.5 310 43 2 3.8 280 39 2 4.7 270 33 2 5.5  290 49   2 900    6200 9400   0 .17  29 2.0  2 10   460 94 2 900    3600 8500   0 8.8 480 65 2 7.9 420 68 2 8.5 470 76 2 18 290 140 2
minepump_spec5_product19_true-unreach-call_false-termination.cil.c .17 28 .95 2 870    950 5900   0 4.8 300 45 2 4.3 290 42 2 4.9 280 40 2 6.2  290 57   2 900    5700 10000   0 .19  29 1.7  2 9.9 470 85 2 900    3000 10000   0 7.8 440 75 2 8.7 450 70 2 8.6 450 65 2 19 300 150 2
minepump_spec5_product20_true-unreach-call_false-termination.cil.c .15 27 .97 2 870    910 7500   0 4.6 310 36 2 4.0 280 32 2 4.9 280 40 2 5.9  280 59   2 900    4700 13000   0 .18  29 2.0  2 11   460 76 2 900    2800 8600   0 8.5 460 66 2 11   500 78 2 8.5 460 69 2 19 310 150 2
minepump_spec5_product21_true-unreach-call_false-termination.cil.c .16 30 1.6  2 870    830 4400   0 4.5 290 44 2 3.9 280 38 2 4.3 270 38 2 5.6  280 50   2 900    5100 12000   0 .18  28 1.9  2 11   470 89 2 900    3200 8700   0 7.9 410 64 2 900   1600 12000 0 8.0 420 75 2 18 290 130 2
minepump_spec5_product22_true-unreach-call_false-termination.cil.c .16 28 1.3  2 870    940 5200   0 4.5 290 39 2 3.9 280 39 2 4.6 270 38 2 5.6  280 54   2 900    6300 11000   0 .22  29 2.3  2 12   470 92 2 900    3300 8800   0 9.5 530 78 2 8.8 470 72 2 9.7 530 77 2 19 290 150 2
minepump_spec5_product23_true-unreach-call_false-termination.cil.c .17 29 1.4  2 870    940 5700   0 4.8 300 42 2 4.2 280 42 2 5.1 270 43 2 6.1  300 53   2 900    4900 10000   0 .20  29 2.3  2 10   470 81 2 900    2800 9700   0 8.5 470 67 2 10   530 98 2 8.5 470 67 2 19 300 150 2
minepump_spec5_product24_true-unreach-call_false-termination.cil.c .17 28 1.5  2 870    850 5600   0 4.3 290 36 2 4.4 280 39 2 4.7 280 38 2 6.1  280 49   2 900    6400 11000   0 .23  29 2.2  2 11   480 94 2 900    2900 9800   0 8.5 480 66 2 9.7 520 83 2 8.7 480 63 2 20 320 150 2
minepump_spec5_product25_true-unreach-call_false-termination.cil.c .16 29 1.2  2 870    840 5800   0 4.4 290 38 2 3.9 280 35 2 4.5 280 39 2 5.5  280 47   2 900    6100 12000   0 .13  29 1.2  2 11   470 85 2 900    4200 7700   0 7.6 400 67 2 900   1500 12000 0 8.3 410 70 2 17 290 130 2
minepump_spec5_product26_true-unreach-call_false-termination.cil.c .15 27 1.3  2 870    990 6200   0 4.5 290 40 2 3.8 280 33 2 4.3 270 37 2 5.7  280 46   2 900    5700 11000   0 .20  29 1.9  2 10   460 98 2 900    3700 8100   0 8.0 460 67 2 7.3 470 62 2 8.5 460 68 2 19 290 150 2
minepump_spec5_product27_true-unreach-call_false-termination.cil.c .17 27 1.3  2 870    930 5400   0 4.7 310 43 2 4.2 280 36 2 5.2 280 34 2 5.9  290 51   2 900    5000 11000   0 .16  28 1.9  2 10   460 78 2 900    2700 9700   0 8.1 450 64 2 9.8 510 86 2 8.1 450 67 2 18 300 130 2
minepump_spec5_product28_true-unreach-call_false-termination.cil.c .17 28 1.2  2 870    860 6100   0 4.4 310 40 2 4.0 280 37 2 5.0 280 42 2 5.7  290 52   2 900    5600 10000   0 .19  28 2.1  2 10   440 78 2 900    2800 7500   0 8.5 460 73 2 8.9 540 82 2 8.3 460 66 2 18 300 130 2
minepump_spec5_product29_true-unreach-call_false-termination.cil.c .15 30 1.6  2 870    870 6700   0 4.5 310 40 2 4.2 280 36 2 4.5 270 37 2 5.8  290 56   2 900    6100 12000   0 .21  29 2.2  2 10   450 85 2 900    3300 8900   0 7.9 420 65 2 900   1500 11000 0 7.7 430 56 2 18 290 130 2
minepump_spec5_product30_true-unreach-call_false-termination.cil.c .18 28 1.3  2 870    940 4500   0 4.7 290 35 2 4.2 280 37 2 4.6 270 39 2 5.6  280 58   2 900    6300 10000   0 .22  29 2.1  2 11   460 81 2 900    3200 7500   0 9.8 520 83 2 9.2 460 76 2 9.7 530 88 2 18 290 140 2
minepump_spec5_product31_true-unreach-call_false-termination.cil.c .18 30 1.3  2 870    930 5300   0 4.8 290 39 2 4.4 280 37 2 4.9 280 37 2 6.7  300 65   2 900    6100 10000   0 .23  29 2.4  2 11   650 88 2 900    2800 9600   0 8.5 470 77 2 10   640 85 2 8.6 470 64 2 19 300 130 2
minepump_spec5_product32_true-unreach-call_false-termination.cil.c .16 28 1.6  2 870    850 4900   0 4.4 300 40 2 4.5 280 40 2 4.7 280 40 2 5.8  290 58   2 900    6100 10000   0 .23  29 2.2  2 11   470 96 2 900    2800 9800   0 7.8 390 63 2 11   630 94 2 7.8 380 59 2 19 310 130 2
minepump_spec5_product33_true-unreach-call_false-termination.cil.c .50 35 5.4  2 870    1600 7700   0 6.2 320 52 2 4.5 280 43 2 6.4 320 55 2 890    150 9800   0 900    3100 11000   0 900     3100 9800    0 18   640 140 -16 900    4600 5800   0 19   740 170 2 40   1100 450 2 82   2000 900 2 43 490 380 2
minepump_spec5_product34_true-unreach-call_false-termination.cil.c .52 35 4.5  2 870    1700 6900   0 6.5 350 58 2 5.0 290 38 2 6.6 320 54 2 770    180 11000   0 900    3200 10000   0 900     3200 10000    0 16   640 120 -16 900    4100 8600   0 18   740 150 2 900   2100 11000 0 92   2200 1000 2 43 470 410 2
minepump_spec5_product35_true-unreach-call_false-termination.cil.c .84 42 9.3  2 870    1800 8400   0 7.0 380 58 2 5.5 290 47 2 6.1 310 59 2 900    180 11000   0 900    2700 12000   0 900     2700 9700    0 17   640 140 -16 900    3100 12000   0 18   730 140 2 900   2300 13000 0 83   2000 820 2 42 430 490 2
minepump_spec5_product36_true-unreach-call_false-termination.cil.c 900    2900 10000    0 870    910 9300   0 7.8 450 70 2 5.3 300 45 2 7.1 320 56 2 900    120 13000   0 900    2700 11000   0 900     2700 11000    0 17   640 140 -16 900    3200 8800   0 28   840 240 2 900   4200 14000 0 900   4500 13000 0 900 1500 11000 0
minepump_spec5_product37_true-unreach-call_false-termination.cil.c .32 33 3.7  2 870    1500 6800   0 7.7 470 71 2 5.4 290 49 2 7.1 330 55 2 900    120 11000   0 900    3200 10000   0 900     3200 12000    0 16   660 130 -16 900    3900 9000   0 43   1300 400 2 900   1400 9300 0 900   2600 11000 0 900 900 7600 0
minepump_spec5_product38_true-unreach-call_false-termination.cil.c .45 34 4.5  2 870    2500 7700   0 7.8 450 69 2 6.0 310 51 2 7.4 340 54 2 900    130 11000   0 900    2900 9700   0 900     2900 10000    0 17   660 140 -16 900    3600 8200   0 49   1300 450 2 900   2300 14000 0 900   2700 11000 0 900 920 8700 0
minepump_spec5_product39_true-unreach-call_false-termination.cil.c 900    3300 10000    0 870    1400 7000   0 8.6 340 66 2 6.2 330 51 2 7.3 330 57 2 900    150 11000   0 900    2900 9300   0 900     2900 9400    0 15   660 130 -16 900    3000 9800   0 45   1300 400 2 900   2300 12000 0 900   4100 12000 0 900 830 7400 0
minepump_spec5_product40_true-unreach-call_false-termination.cil.c 900    3000 9300    0 870    1600 7500   0 9.0 460 72 2 5.6 320 51 2 7.4 330 53 2 900    140 11000   0 900    3000 12000   0 900     3000 11000    0 17   650 130 -16 900    3300 7900   0 60   1700 610 2 900   3500 11000 0 900   3000 10000 0 900 800 10000 0
minepump_spec5_product41_true-unreach-call_false-termination.cil.c 900    3100 12000    0 870    1900 6800   0 6.6 350 52 2 5.3 310 45 2 6.0 310 54 2 900    150 10000   0 900    3300 12000   0 900     3200 10000    0 34   1700 260 2 900    3300 8100   0 17   720 140 2 900   4500 11000 0 130   2700 1500 2 900 710 9700 0
minepump_spec5_product42_true-unreach-call_false-termination.cil.c 900    3200 10000    0 870    1900 7600   0 6.6 360 57 2 5.5 310 50 2 6.8 330 55 2 900    170 11000   0 900    2900 9500   0 900     2900 10000    0 38   1600 320 2 900    3400 9200   0 19   740 170 2 900   1600 12000 0 170   2900 1600 2 900 730 8200 0
minepump_spec5_product43_true-unreach-call_false-termination.cil.c 900    3300 13000    0 870    2100 7000   0 7.5 380 60 2 6.2 360 47 2 6.4 310 56 2 900    170 11000   0 900    2600 10000   0 900     2600 9000    0 30   1800 260 2 900    3000 11000   0 18   760 180 2 900   2800 11000 0 130   2700 1400 2 900 750 9400 0
minepump_spec5_product44_true-unreach-call_false-termination.cil.c 900    2900 9000    0 870    2100 7400   0 7.7 450 62 2 6.3 360 53 2 7.2 330 61 2 900    120 11000   0 900    2600 11000   0 900     2600 11000    0 31   950 250 -16 900    3200 12000   0 31   900 280 2 900   2000 14000 0 900   4600 10000 0 900 770 8100 0
minepump_spec5_product45_true-unreach-call_false-termination.cil.c 900    2900 9500    0 870    1800 4900   0 7.1 450 64 2 6.2 400 57 2 7.2 320 52 2 900    130 12000   0 900    3000 10000   0 900     2900 12000    0 33   1400 260 2 900    3900 7800   0 48   1400 500 2 900   1400 12000 0 380   4700 4500 2 900 900 8800 0
minepump_spec5_product46_true-unreach-call_false-termination.cil.c 900    3000 9200    0 870    1800 7700   0 7.6 440 62 2 6.5 430 55 2 7.5 330 61 2 900    140 12000   0 900    2900 11000   0 900     2900 10000    0 34   1600 260 2 900    3900 7400   0 49   1600 440 2 900   1700 11000 0 900   2900 11000 0 900 910 9700 0
minepump_spec5_product47_true-unreach-call_false-termination.cil.c 900    3100 9700    0 870    1800 5700   0 8.6 460 72 2 6.9 440 54 2 6.8 330 53 2 900    150 13000   0 900    2900 9400   0 900     2900 7800    0 32   1600 310 2 900    3000 12000   0 46   1400 390 2 900   1900 11000 0 330   4500 3600 2 900 980 6700 0
minepump_spec5_product48_true-unreach-call_false-termination.cil.c 900    2900 8600    0 870    2000 6700   0 7.6 450 62 2 7.6 430 67 2 7.5 340 56 2 900    150 12000   0 900    2800 9700   0 900     2800 9500    0 34   1700 310 2 900    3000 12000   0 61   2100 590 2 900   3100 13000 0 900   3400 9500 0 900 980 8300 0
minepump_spec5_product49_true-unreach-call_false-termination.cil.c .45 34 6.4  2 870    1500 6700   0 7.2 450 61 2 5.2 310 49 2 5.7 290 46 2 900    140 11000   0 900    3500 10000   0 900     3500 11000    0 28   1300 210 2 900    4500 7600   0 30   1000 260 2 900   1500 12000 0 120   2700 1300 2 720 820 5600 2
minepump_spec5_product50_true-unreach-call_false-termination.cil.c .52 36 5.7  2 870    1500 7200   0 7.3 450 67 2 5.3 300 42 2 5.9 310 49 2 900    150 12000   0 900    3500 9900   0 900     3500 9200    0 28   1300 240 2 900    3900 7900   0 30   900 250 2 900   2000 12000 0 160   2800 1700 2 720 810 6600 2
minepump_spec5_product51_true-unreach-call_false-termination.cil.c .82 51 10    2 870    1600 7400   0 8.1 470 64 2 6.1 330 56 2 6.0 290 49 2 900    170 12000   0 900    2800 10000   0 900     2800 9400    0 30   1300 250 2 900    3000 8500   0 38   1100 270 2 900   1500 14000 0 120   2500 1100 2 740 870 6100 2
minepump_spec5_product52_true-unreach-call_false-termination.cil.c 900    2900 11000    0 870    1600 6700   0 9.5 450 76 2 6.1 320 53 2 6.0 310 44 2 900    140 11000   0 900    2700 11000   0 900     2700 11000    0 38   1600 330 2 900    3200 8300   0 41   1100 350 2 900   2300 11000 0 430   3300 5700 2 900 870 8300 0
minepump_spec5_product53_true-unreach-call_false-termination.cil.c .44 34 4.8  2 870    2400 5900   0 7.6 460 59 2 5.8 340 49 2 6.6 310 47 2 900    180 11000   0 900    3200 9600   0 900     3200 9200    0 33   1500 270 2 900    4200 6900   0 40   1100 300 2 900   1400 9600 0 410   3300 5600 2 840 840 8000 2
minepump_spec5_product54_true-unreach-call_false-termination.cil.c .49 36 4.4  2 870    2400 4400   0 8.0 450 64 2 6.4 320 50 2 6.6 320 52 2 900    200 13000   0 900    3400 9500   0 900     3500 12000    0 37   1800 290 2 900    3800 10000   0 37   1100 330 2 900   2400 10000 0 900   5700 10000 0 850 840 6900 2
minepump_spec5_product55_true-unreach-call_false-termination.cil.c .99 66 11    2 870    2600 5900   0 8.9 470 68 2 6.5 360 51 2 5.8 280 49 2 900    220 11000   0 900    2800 11000   0 900     2800 11000    0 35   1800 270 2 900    3100 12000   0 28   890 260 2 900   2500 13000 0 580   4700 7200 2 870 880 7000 2
minepump_spec5_product56_true-unreach-call_false-termination.cil.c 900    3200 9700    0 870    2600 8100   0 9.5 450 79 2 6.3 360 53 2 6.1 310 47 2 900    190 12000   0 900    3200 13000   0 900     3200 9700    0 46   2000 400 2 900    3300 9900   0 33   1100 290 2 900   2300 13000 0 900   2600 9500 0 900 890 7300 0
minepump_spec5_product57_true-unreach-call_false-termination.cil.c 900    3100 11000    0 870    1900 7400   0 7.6 460 61 2 7.1 430 54 2 5.8 290 45 2 900    130 11000   0 900    2900 11000   0 900     2900 10000    0 41   2700 390 2 900    4000 7800   0 34   1000 300 2 900   1400 12000 0 200   2000 2100 2 900 960 10000 0
minepump_spec5_product58_true-unreach-call_false-termination.cil.c 900    3200 9100    0 870    1900 6200   0 7.7 440 59 2 6.9 440 57 2 5.8 310 49 2 900    140 11000   0 900    2900 8900   0 900     2900 9600    0 44   3000 360 2 900    3700 8200   0 30   1000 240 2 900   2900 11000 0 420   4800 5400 2 900 630 8100 0
minepump_spec5_product59_true-unreach-call_false-termination.cil.c 900    3300 11000    0 870    1900 6700   0 8.1 450 67 2 7.4 430 58 2 5.8 310 46 2 900    170 10000   0 900    2800 9700   0 900     2800 11000    0 49   3500 450 2 900    3000 9300   0 33   1100 290 2 900   2600 12000 0 210   3000 2100 2 900 850 8500 0
minepump_spec5_product60_true-unreach-call_false-termination.cil.c 900    3100 10000    0 870    1900 7000   0 9.9 440 84 2 7.1 440 66 2 5.8 310 46 2 900    140 11000   0 900    2800 9900   0 900     2800 12000    0 55   3300 460 2 900    3300 11000   0 38   1200 320 2 900   2600 14000 0 900   4500 9800 0 900 1000 7700 0
minepump_spec5_product61_true-unreach-call_false-termination.cil.c 900    3300 10000    0 870    3200 6200   0 8.0 450 57 2 7.4 440 54 2 5.6 290 52 2 900    180 11000   0 900    3200 12000   0 900     3200 10000    0 32   1500 250 2 900    4100 7500   0 46   1200 370 2 900   1400 10000 0 580   4100 7600 2 900 760 9500 0
minepump_spec5_product62_true-unreach-call_false-termination.cil.c 900    3300 11000    0 870    3200 5600   0 8.7 450 61 2 7.1 430 67 2 6.1 310 45 2 900    200 11000   0 900    3200 11000   0 900     3200 10000    0 37   1700 270 2 900    3600 8300   0 51   1300 450 2 900   1900 14000 0 900   5400 12000 0 900 760 7100 0
minepump_spec5_product63_true-unreach-call_false-termination.cil.c 900    3500 9200    0 870    3300 6000   0 8.1 470 63 2 7.2 430 56 2 6.3 310 52 2 900    220 12000   0 900    3000 11000   0 900     3000 7700    0 35   1600 310 2 900    3000 13000   0 49   1300 430 2 900   2200 15000 0 420   3000 4300 2 900 880 6900 0
minepump_spec5_product64_true-unreach-call_false-termination.cil.c 900    3200 9100    0 870    3400 7700   0 8.7 440 71 2 7.6 440 63 2 5.9 310 45 2 890    190 11000   0 900    3100 9500   0 900     3100 9900    0 32   1600 270 2 900    3300 8300   0 46   1300 410 2 900   2800 14000 0 900   2700 9300 0 900 890 7000 0
minepump_spec5_productSimulator_true-unreach-call_false-termination.cil.c 900    3300 9200    0 870    3100 5800   0 11   490 83 2 12   470 88 2 34   2400 300 2 900    250 10000   0 900    2700 10000   0 900     2700 9600    0 59   3800 600 2 900    3700 7700   0 56   1800 460 2 900   5500 13000 0 900   5100 10000 0 900 940 7600 0
../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
total 597 60000 450000 650000 795 597 210000 480000 1500000 301 597 170000 2300000 1200000 711 597 170000 2000000 1400000 663 597 7000 310000 66000 919 597 260000 250000 3200000 443 597 220000 1200000 2600000 453 597 160000 820000 1900000 573 597 250000 2000000 2900000 203 597 210000 870000 2200000 461 597 220000 3200000 1700000 626 597 300000 1400000 4000000 440 597 280000 2200000 3200000 529 597 270000 1000000 2600000 513
    correct results 530 7800 260000 68000 795 207 660 13000 7200 243 433 20000 600000 150000 711 389 4100 170000 36000 663 587 7000 310000 65000 909 289 69000 160000 810000 443 359 710 16000 7400 453 419 1100 21000 12000 573 317 9900 360000 93000 539 363 200 6800 2400 461 361 7700 240000 75000 626 265 4300 150000 42000 440 312 19000 330000 210000 529 254 31000 270000 300000 508
        correct true 265 1200 64000 12000 530 36 140 1600 1600 72 278 3500 160000 27000 556 274 1700 100000 15000 548 322 3300 180000 32000 644 154 49000 140000 590000 308 94 86 3500 1100 188 154 120 6100 1400 308 222 6700 260000 61000 444 98 88 2100 1100 196 265 6600 200000 67000 530 175 2800 110000 27000 350 217 17000 260000 200000 434 254 31000 270000 300000 508
        correct false 265 6600 200000 56000 265 171 520 11000 5600 171 155 17000 450000 120000 155 115 2400 70000 22000 115 265 3600 130000 34000 265 135 20000 24000 220000 135 265 620 13000 6400 265 265 1000 15000 11000 265 95 3200 100000 32000 95 265 110 4700 1300 265 96 1100 49000 8500 96 90 1400 47000 15000 90 95 1700 63000 15000 95 0
    correct-unconfimed results 0 150 1600 14000 16000 58 0 23 3000 70000 28000 0 10 56 2800 460 10 128 64000 42000 720000 0 0 0 1 36 1500 300 0 0 0 0 0 5 1900 18000 21000 5
        correct-unconfirmed true 0 58 170 2700 1900 58 0 0 10 56 2800 460 10 0 0 0 0 0 0 0 0 5 1900 18000 21000 5
        correct-unconfirmed false 0 92 1400 11000 14000 0 0 23 3000 70000 28000 0 0 128 64000 42000 720000 0 0 0 1 36 1500 300 0 0 0 0 0 0
    incorrect results 0 0 0 0 0 0 0 0 21 2000 54000 24000 -336 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 21 2000 54000 24000 -336 0 0 0 0 0
score (597 tasks, max score: 929) 795 301 711 663 919 443 453 573 203 461 626 440 529 513
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