Tool BLAST 2.7.1 CPAchecker 1.1.10-svcomp13 ESBMC 1.20 LLBMC SV-COMP-13 Predator UFO 2012-10-22
Limits timelimit: 900 s, memlimit: 15360 MB
System CPU: Intel(R) Core(TM) i7-2600K CPU @ 3.40GHz with 4 cores, frequency: 3401 MHz; RAM: 16343684 kB
Date of run 2012-11-25 00:16 2012-11-14 06:53 2012-11-14 08:27 2012-11-17 03:16 2012-12-04 06:32 2012-12-03 03:44 2012-12-14 13:52
Options -alias bdd
-enable-recursion
-noprofile
-cref
-sv-comp
-lattice
-include-lattice symb
-sv-comp13--explitp-pred
-heap 12000m
-disable-java-assertions
-sv-comp13--combinations
-heap 12000m
-disable-java-assertions
-t label
-m32
--cex=${logfile_path_abs}/${test_name}.${sourcefile_name}.cex
../sv-benchmarks-trunk/product-lines/ status time status time status time status time status time status time status time
elevator_spec14_product20_unsafe.cil.c unsafe 370    exception 880    unsafe 2.7  unsafe 0.83 unsafe 1.00 unsafe 0.36 unsafe 1.3 
elevator_spec14_product24_unsafe.cil.c error 1.4  timeout 900    unsafe 2.8  unsafe 0.89 unsafe 1.2  unsafe 1.8  unsafe 1.8 
elevator_spec14_product28_unsafe.cil.c unsafe 400    timeout 900    unsafe 2.7  unsafe 0.82 unsafe 0.85 unsafe 0.34 unsafe 1.4 
elevator_spec14_product32_unsafe.cil.c error 1.5  timeout 900    unsafe 2.7  unsafe 0.81 unsafe 1.1  unsafe 1.8  unsafe 1.9 
elevator_spec14_productSimulator_unsafe.cil.c error 110    timeout 900    timeout 910    safe 780    unsafe 13    unsafe 2.1  unsafe 13   
elevator_spec1_product18_unsafe.cil.c timeout 910    timeout 900    unsafe 2.7  unsafe 0.82 unsafe 2.0  unsafe 0.35 unsafe 5.1 
elevator_spec1_product20_unsafe.cil.c timeout 910    timeout 900    unsafe 2.9  unsafe 0.83 unsafe 2.1  unsafe 0.34 unsafe 7.2 
elevator_spec1_product22_unsafe.cil.c error 2.8  timeout 900    unsafe 2.9  unsafe 0.84 unsafe 2.8  unsafe 1.5  unsafe 9.9 
elevator_spec1_product24_unsafe.cil.c error 2.7  timeout 900    unsafe 2.9  unsafe 0.82 unsafe 3.0  unsafe 1.5  unsafe 9.9 
elevator_spec1_product26_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 0.80 unsafe 2.2  unsafe 0.34 unsafe 7.4 
elevator_spec1_product28_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 0.95 unsafe 2.4  unsafe 0.35 unsafe 5.6 
elevator_spec1_product30_unsafe.cil.c error 3.3  timeout 900    unsafe 2.8  unsafe 0.77 unsafe 3.0  unsafe 1.5  unsafe 9.9 
elevator_spec1_product32_unsafe.cil.c error 3.1  timeout 900    unsafe 2.9  unsafe 0.83 unsafe 3.5  unsafe 1.4  unsafe 9.9 
elevator_spec1_productSimulator_unsafe.cil.c timeout 910    timeout 900    timeout 900    timeout 900    unsafe 22    unsafe 4.8  unsafe 38   
elevator_spec2_product18_unsafe.cil.c timeout 910    timeout 900    unsafe 2.7  unsafe 0.83 unsafe 2.0  unsafe 0.33 unsafe 4.5 
elevator_spec2_product20_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 0.84 unsafe 2.1  unsafe 0.33 unsafe 4.4 
elevator_spec2_product22_unsafe.cil.c error 2.7  timeout 900    unsafe 2.8  unsafe 0.80 unsafe 3.0  unsafe 0.88 unsafe 6.3 
elevator_spec2_product24_unsafe.cil.c error 2.7  timeout 900    unsafe 2.9  unsafe 0.85 unsafe 3.4  unsafe 0.90 unsafe 6.4 
elevator_spec2_product26_unsafe.cil.c timeout 910    timeout 900    unsafe 2.7  unsafe 0.84 unsafe 2.2  unsafe 0.33 unsafe 4.5 
elevator_spec2_product28_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 0.83 unsafe 2.4  unsafe 0.34 unsafe 4.8 
elevator_spec2_product30_unsafe.cil.c error 3.1  timeout 900    unsafe 2.8  unsafe 0.86 unsafe 3.4  unsafe 0.89 unsafe 6.4 
elevator_spec2_product32_unsafe.cil.c error 3.0  timeout 900    unsafe 2.9  unsafe 0.79 unsafe 3.4  unsafe 0.91 unsafe 6.5 
elevator_spec2_productSimulator_unsafe.cil.c timeout 910    timeout 900    timeout 900    timeout 900    unsafe 22    unsafe 1.8  unsafe 20   
elevator_spec3_product03_unsafe.cil.c unsafe 0.54 timeout 900    unsafe 3.1  unsafe 0.88 unsafe 0.37 unsafe 0.32 unsafe 0.80
elevator_spec3_product11_unsafe.cil.c unsafe 0.54 timeout 900    unsafe 2.9  unsafe 0.87 unsafe 0.39 unsafe 0.32 unsafe 0.79
elevator_spec3_product19_unsafe.cil.c unsafe 0.56 timeout 900    unsafe 3.0  unsafe 0.84 unsafe 0.38 unsafe 0.32 unsafe 0.80
elevator_spec3_product20_unsafe.cil.c unsafe 0.59 timeout 900    unsafe 3.0  unsafe 0.87 unsafe 0.72 unsafe 0.35 unsafe 1.3 
elevator_spec3_product23_unsafe.cil.c error 1.2  timeout 900    unsafe 3.1  unsafe 0.96 unsafe 0.54 unsafe 1.4  unsafe 1.1 
elevator_spec3_product24_unsafe.cil.c error 1.2  timeout 900    unsafe 3.1  unsafe 0.94 unsafe 1.0  unsafe 1.6  unsafe 1.8 
elevator_spec3_product27_unsafe.cil.c unsafe 0.57 timeout 900    unsafe 3.1  unsafe 0.88 unsafe 0.43 unsafe 0.33 unsafe 0.82
elevator_spec3_product28_unsafe.cil.c unsafe 0.59 timeout 900    unsafe 3.0  unsafe 0.85 unsafe 0.76 unsafe 0.37 unsafe 1.4 
elevator_spec3_product31_unsafe.cil.c error 1.2  timeout 900    unsafe 3.2  unsafe 0.91 unsafe 0.57 unsafe 1.4  unsafe 1.1 
elevator_spec3_product32_unsafe.cil.c error 1.2  timeout 900    unsafe 3.2  unsafe 0.85 unsafe 1.1  unsafe 1.7  unsafe 1.9 
elevator_spec3_productSimulator_unsafe.cil.c error 370    timeout 900    timeout 910    timeout 900    unsafe 17    unsafe 2.6  unsafe 14   
elevator_spec9_product26_unsafe.cil.c timeout 910    timeout 900    unsafe 2.7  unsafe 0.79 unsafe 2.1  unsafe 0.36 unsafe 4.7 
elevator_spec9_product28_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 0.83 unsafe 2.5  unsafe 0.35 unsafe 4.7 
elevator_spec9_product30_unsafe.cil.c error 55    timeout 900    unsafe 2.8  unsafe 0.80 unsafe 3.0  unsafe 0.90 unsafe 5.7 
elevator_spec9_product32_unsafe.cil.c error 78    timeout 900    unsafe 2.9  unsafe 0.84 unsafe 3.7  unsafe 0.92 unsafe 6.5 
elevator_spec9_productSimulator_unsafe.cil.c timeout 910    timeout 900    timeout 900    timeout 900    unsafe 22    unsafe 1.8  unsafe 15   
elevator_spec13_product21_safe.cil.c error 1.7  timeout 900    safe 2.3  safe 0.86 safe 68    safe 88    safe 80   
elevator_spec13_product22_safe.cil.c error 1.7  timeout 900    safe 2.2  safe 0.87 safe 87    safe 110    safe 140   
elevator_spec13_product23_safe.cil.c error 1.7  timeout 900    safe 2.3  safe 0.84 safe 71    safe 19    safe 46   
elevator_spec13_product24_safe.cil.c error 1.7  timeout 900    safe 2.3  safe 0.87 safe 90    safe 21    safe 130   
elevator_spec13_product29_safe.cil.c error 1.9  timeout 900    safe 2.2  safe 0.92 safe 70    safe 88    safe 92   
elevator_spec13_product30_safe.cil.c error 2.0  timeout 900    safe 2.2  safe 0.86 safe 97    safe 120    safe 71   
elevator_spec13_product31_safe.cil.c error 1.9  timeout 900    safe 2.3  safe 0.83 safe 65    safe 20    safe 84   
elevator_spec13_product32_safe.cil.c error 2.0  timeout 900    safe 2.3  safe 0.95 safe 94    safe 21    safe 140   
elevator_spec13_productSimulator_safe.cil.c error 2.5  timeout 900    safe 4.1  timeout 900    timeout 910    timeout 900    safe 660   
elevator_spec14_product03_safe.cil.c timeout 910    timeout 900    safe 2.4  safe 0.82 safe 11    safe 0.41 safe 10   
elevator_spec14_product11_safe.cil.c timeout 910    timeout 900    safe 2.5  safe 0.83 safe 11    safe 0.41 safe 20   
elevator_spec14_product19_safe.cil.c timeout 910    timeout 900    safe 2.5  safe 0.87 safe 11    safe 0.40 safe 12   
elevator_spec14_product23_safe.cil.c error 1.4  timeout 900    safe 2.7  safe 0.82 safe 22    safe 4.0  safe 7.1 
elevator_spec14_product27_safe.cil.c timeout 910    timeout 900    safe 2.5  safe 0.92 safe 12    safe 0.41 safe 22   
elevator_spec14_product31_safe.cil.c error 1.4  timeout 900    safe 2.6  safe 0.93 safe 24    safe 4.2  safe 7.1 
elevator_spec1_product01_safe.cil.c timeout 910    timeout 900    safe 2.4  safe 0.76 safe 6.9  safe 0.37 safe 71   
elevator_spec1_product03_safe.cil.c timeout 910    timeout 900    safe 2.6  safe 0.80 safe 6.8  safe 0.40 safe 43   
elevator_spec1_product09_safe.cil.c timeout 910    timeout 900    safe 2.4  safe 0.85 safe 7.1  safe 0.38 safe 65   
elevator_spec1_product11_safe.cil.c timeout 910    timeout 900    safe 2.4  safe 0.86 safe 7.9  safe 0.40 safe 75   
elevator_spec1_product17_safe.cil.c timeout 910    timeout 900    safe 2.4  safe 0.81 safe 7.3  safe 0.39 safe 49   
elevator_spec1_product19_safe.cil.c timeout 910    timeout 900    safe 2.4  safe 0.83 safe 8.1  safe 0.40 safe 48   
elevator_spec1_product21_safe.cil.c error 3.8  timeout 900    safe 2.4  safe 0.84 safe 11    unsafe 5.9  safe 200   
elevator_spec1_product23_safe.cil.c error 23    timeout 900    safe 2.5  safe 0.81 safe 11    unsafe 5.2  safe 190   
elevator_spec1_product25_safe.cil.c timeout 910    timeout 900    safe 2.4  safe 0.80 safe 7.6  safe 0.39 safe 64   
elevator_spec1_product27_safe.cil.c timeout 910    timeout 900    safe 2.5  safe 0.80 safe 8.3  safe 0.41 safe 63   
elevator_spec1_product29_safe.cil.c error 3.8  timeout 900    safe 2.5  safe 0.89 safe 12    unsafe 6.2  safe 170   
elevator_spec1_product31_safe.cil.c error 24    timeout 900    safe 2.6  safe 0.87 safe 12    unsafe 5.1  safe 230   
elevator_spec2_product01_safe.cil.c timeout 910    timeout 900    safe 2.2  safe 0.81 safe 2.4  safe 0.32 safe 6.1 
elevator_spec2_product03_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.80 safe 2.8  safe 0.33 safe 14   
elevator_spec2_product09_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.81 safe 3.0  safe 0.34 safe 9.9 
elevator_spec2_product11_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.87 safe 2.8  safe 0.34 safe 11   
elevator_spec2_product17_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.82 safe 3.0  safe 0.33 safe 13   
elevator_spec2_product19_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.84 safe 3.1  safe 0.35 safe 8.2 
elevator_spec2_product21_safe.cil.c error 3.7  timeout 900    safe 2.3  safe 0.79 safe 3.9  unsafe 1.3  safe 7.6 
elevator_spec2_product23_safe.cil.c error 32    timeout 900    safe 2.3  safe 0.81 safe 4.5  unsafe 1.3  safe 11   
elevator_spec2_product25_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.80 safe 3.2  safe 0.33 safe 15   
elevator_spec2_product27_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.79 safe 3.0  safe 0.33 safe 10   
elevator_spec2_product29_safe.cil.c error 3.8  timeout 900    safe 2.3  safe 0.82 safe 4.7  unsafe 1.3  safe 13   
elevator_spec2_product31_safe.cil.c error 33    timeout 900    safe 2.3  safe 0.84 safe 5.0  unsafe 1.3  safe 12   
elevator_spec3_product01_safe.cil.c timeout 910    timeout 900    safe 2.6  safe 0.80 safe 13    safe 0.42 safe 1.6 
elevator_spec3_product09_safe.cil.c timeout 910    timeout 900    safe 2.6  safe 0.81 safe 14    safe 0.44 safe 1.3 
elevator_spec3_product17_safe.cil.c timeout 910    timeout 900    safe 2.7  safe 0.84 safe 14    safe 0.43 safe 1.2 
elevator_spec3_product18_safe.cil.c timeout 910    timeout 900    safe 2.6  safe 0.81 safe 28    safe 0.50 safe 2.1 
elevator_spec3_product21_safe.cil.c error 2.9  timeout 900    safe 2.6  safe 0.88 safe 21    safe 4.3  safe 1.7 
elevator_spec3_product22_safe.cil.c error 3.0  timeout 900    safe 2.6  safe 0.85 safe 42    safe 5.5  safe 3.0 
elevator_spec3_product25_safe.cil.c timeout 910    timeout 900    safe 2.7  safe 0.88 safe 15    safe 0.43 safe 1.4 
elevator_spec3_product26_safe.cil.c timeout 910    timeout 900    safe 2.6  safe 0.86 safe 30    safe 0.49 safe 2.4 
elevator_spec3_product29_safe.cil.c error 2.9  timeout 900    safe 2.7  safe 0.88 safe 22    safe 4.8  safe 1.9 
elevator_spec3_product30_safe.cil.c error 3.0  timeout 900    safe 2.7  safe 0.90 safe 44    safe 5.3  safe 3.2 
elevator_spec9_product09_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.79 safe 3.1  safe 0.32 safe 12   
elevator_spec9_product11_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.79 safe 2.9  safe 0.34 safe 14   
elevator_spec9_product25_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.76 safe 2.9  safe 0.34 safe 8.5 
elevator_spec9_product27_safe.cil.c timeout 910    timeout 900    safe 2.3  safe 0.79 safe 3.1  safe 0.34 safe 19   
elevator_spec9_product29_safe.cil.c error 16    timeout 900    safe 2.3  safe 0.80 safe 4.4  unsafe 1.4  safe 7.9 
elevator_spec9_product31_safe.cil.c error 28    timeout 900    safe 2.3  safe 0.84 safe 5.0  unsafe 1.3  safe 7.7 
email_spec0_product16_unsafe.cil.c unsafe 320    unsafe 270    unsafe 2.9  unsafe 1.0  unsafe 1.4  unsafe 1.3  unsafe 1.6 
email_spec0_product21_unsafe.cil.c timeout 910    timeout 900    unsafe 2.9  unsafe 2.0  unsafe 4.3  unsafe 1.5  unsafe 6.3 
email_spec0_product22_unsafe.cil.c timeout 910    timeout 900    unsafe 3.0  unsafe 1.2  unsafe 1.6  unsafe 2.8  unsafe 2.3 
email_spec0_product26_unsafe.cil.c timeout 910    timeout 900    unsafe 2.9  unsafe 2.0  unsafe 4.2  unsafe 3.5  unsafe 7.9 
email_spec0_product31_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 1.3  unsafe 2.0  unsafe 2.0  unsafe 2.0 
email_spec0_product33_unsafe.cil.c timeout 910    timeout 900    unsafe 3.0  unsafe 1.3  unsafe 2.3  unsafe 5.8  unsafe 2.5 
email_spec0_product34_unsafe.cil.c timeout 910    timeout 900    unsafe 2.9  unsafe 2.4  unsafe 5.3  unsafe 2.3  unsafe 8.6 
email_spec0_product35_unsafe.cil.c timeout 910    timeout 900    unsafe 3.0  unsafe 2.4  unsafe 5.3  unsafe 6.8  unsafe 9.9 
email_spec0_productSimulator_unsafe.cil.c timeout 910    timeout 900    segmentation fault 180    unsafe 130    unsafe 450    unsafe 62    unsafe 130   
email_spec11_product15_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 1.2  unsafe 1.6  unsafe 2.1  unsafe 1.6 
email_spec11_product20_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 1.6  unsafe 4.0  unsafe 2.6  unsafe 5.0 
email_spec11_product22_unsafe.cil.c timeout 910    timeout 900    unsafe 2.7  unsafe 1.2  unsafe 1.6  unsafe 3.4  unsafe 2.5 
email_spec11_product26_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 1.9  unsafe 4.2  unsafe 4.3  unsafe 7.0 
email_spec11_product30_unsafe.cil.c timeout 910    timeout 900    unsafe 2.9  unsafe 1.2  unsafe 1.9  unsafe 4.1  unsafe 1.4 
email_spec11_product32_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 2.0  unsafe 5.4  unsafe 4.8  unsafe 6.6 
email_spec11_product33_unsafe.cil.c timeout 910    timeout 900    unsafe 2.9  unsafe 1.3  unsafe 2.2  unsafe 7.1  unsafe 3.8 
email_spec11_product35_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 2.5  unsafe 6.4  unsafe 8.5  unsafe 9.7 
email_spec11_productSimulator_unsafe.cil.c timeout 910    timeout 900    segmentation fault 120    unsafe 180    unsafe 810    unsafe 110    unsafe 200   
email_spec1_product14_unsafe.cil.c timeout 910    unsafe 450    unsafe 3.0  unsafe 1.3  unsafe 1.8  unsafe 8.0  unsafe 1.8 
email_spec1_product15_unsafe.cil.c timeout 910    timeout 900    unsafe 4.2  unsafe 1.1  unsafe 1.0  unsafe 0.47 unsafe 2.0 
email_spec1_product16_unsafe.cil.c timeout 910    timeout 900    unsafe 3.4  unsafe 1.1  unsafe 1.0  unsafe 1.5  unsafe 2.3 
email_spec1_product20_unsafe.cil.c timeout 910    timeout 900    unsafe 3.1  unsafe 1.6  unsafe 2.0  unsafe 0.50 unsafe 4.6 
email_spec1_product21_unsafe.cil.c timeout 910    timeout 900    unsafe 3.1  unsafe 1.7  unsafe 2.0  unsafe 1.7  unsafe 7.2 
email_spec1_product22_unsafe.cil.c timeout 910    timeout 900    unsafe 3.6  unsafe 1.1  unsafe 1.00 unsafe 0.58 unsafe 3.4 
email_spec1_product26_unsafe.cil.c timeout 910    timeout 900    unsafe 3.2  unsafe 1.8  unsafe 2.2  unsafe 0.69 unsafe 8.4 
email_spec1_product29_unsafe.cil.c timeout 910    timeout 900    unsafe 3.0  unsafe 1.2  unsafe 1.9  unsafe 13    unsafe 2.4 
email_spec1_product30_unsafe.cil.c timeout 910    timeout 900    unsafe 4.4  unsafe 1.1  unsafe 1.1  unsafe 0.66 unsafe 2.4 
email_spec1_product31_unsafe.cil.c timeout 910    timeout 900    unsafe 3.6  unsafe 1.2  unsafe 1.1  unsafe 2.4  unsafe 2.1 
email_spec1_product32_unsafe.cil.c timeout 910    timeout 900    unsafe 3.3  unsafe 2.0  unsafe 2.7  unsafe 0.74 unsafe 8.6 
email_spec1_product33_unsafe.cil.c timeout 910    timeout 900    unsafe 4.1  unsafe 1.3  unsafe 1.2  unsafe 0.96 unsafe 3.8 
email_spec1_product34_unsafe.cil.c timeout 910    timeout 900    unsafe 3.2  unsafe 2.2  unsafe 2.9  unsafe 2.7  unsafe 9.4 
email_spec1_product35_unsafe.cil.c timeout 910    timeout 900    unsafe 3.4  unsafe 2.4  unsafe 2.8  unsafe 1.1  unsafe 11   
email_spec1_productSimulator_unsafe.cil.c timeout 910    timeout 900    segmentation fault 280    unsafe 40    unsafe 52    unsafe 16    unsafe 60   
email_spec27_product17_unsafe.cil.c unsafe 51    timeout 900    unsafe 4.6  unsafe 1.2  unsafe 1.7  unsafe 3.3  unsafe 2.8 
email_spec27_product18_unsafe.cil.c unsafe 6.2  unsafe 340    unsafe 11    unsafe 1.1  unsafe 1.1  unsafe 0.58 unsafe 2.0 
email_spec27_product19_unsafe.cil.c unsafe 51    timeout 900    unsafe 3.5  unsafe 1.1  unsafe 1.1  unsafe 6.0  unsafe 2.6 
email_spec27_product23_unsafe.cil.c unsafe 6.7  timeout 900    unsafe 5.7  unsafe 1.8  unsafe 2.6  unsafe 0.63 unsafe 7.5 
email_spec27_product24_unsafe.cil.c unsafe 6.2  timeout 900    unsafe 3.9  unsafe 1.2  unsafe 1.3  unsafe 0.78 unsafe 2.7 
email_spec27_product25_unsafe.cil.c unsafe 54    timeout 900    unsafe 3.7  unsafe 1.9  unsafe 2.6  unsafe 5.8  unsafe 8.1 
email_spec27_product27_unsafe.cil.c unsafe 6.9  timeout 900    unsafe 4.0  unsafe 2.0  unsafe 2.7  unsafe 0.87 unsafe 9.4 
email_spec27_product29_unsafe.cil.c unsafe 110    timeout 900    unsafe 5.2  unsafe 1.3  unsafe 2.6  unsafe 4.1  unsafe 2.9 
email_spec27_product30_unsafe.cil.c unsafe 330    unsafe 400    unsafe 12    unsafe 1.2  unsafe 1.5  unsafe 0.70 unsafe 2.6 
email_spec27_product31_unsafe.cil.c unsafe 490    timeout 900    unsafe 3.8  unsafe 1.3  unsafe 1.5  unsafe 8.3  unsafe 2.9 
email_spec27_product32_unsafe.cil.c unsafe 340    timeout 900    unsafe 6.2  unsafe 2.3  unsafe 3.5  unsafe 0.78 unsafe 12   
email_spec27_product33_unsafe.cil.c unsafe 220    timeout 900    unsafe 4.2  unsafe 1.5  unsafe 1.5  unsafe 1.0  unsafe 5.2 
email_spec27_product34_unsafe.cil.c unsafe 530    timeout 900    unsafe 3.9  unsafe 2.6  unsafe 3.6  unsafe 7.6  unsafe 9.9 
email_spec27_product35_unsafe.cil.c unsafe 230    timeout 900    unsafe 4.2  unsafe 2.7  unsafe 3.7  unsafe 1.2  unsafe 17   
email_spec27_productSimulator_unsafe.cil.c unsafe 44    timeout 900    unknown 260    unsafe 190    timeout 910    unsafe 16    unsafe 180   
email_spec3_product13_unsafe.cil.c unsafe 62    unsafe 20    unsafe 2.8  unsafe 0.95 unsafe 0.09 unsafe 0.11 unsafe 1.1 
email_spec3_product17_unsafe.cil.c unsafe 66    unsafe 210    unsafe 2.9  unsafe 1.1  unsafe 0.12 unsafe 0.13 unsafe 1.4 
email_spec3_product18_unsafe.cil.c unsafe 4.4  unsafe 20    unsafe 3.0  unsafe 1.2  unsafe 0.11 unsafe 0.11 unsafe 0.89
email_spec3_product19_unsafe.cil.c unsafe 62    unsafe 21    unsafe 2.8  unsafe 1.2  unsafe 0.10 unsafe 0.12 unsafe 1.0 
email_spec3_product23_unsafe.cil.c unsafe 4.8  unsafe 230    unsafe 3.1  unsafe 1.9  unsafe 0.11 unsafe 0.13 unsafe 2.2 
email_spec3_product24_unsafe.cil.c unsafe 4.4  unsafe 21    unsafe 3.1  unsafe 1.2  unsafe 0.10 unsafe 0.12 unsafe 1.4 
email_spec3_product25_unsafe.cil.c unsafe 66    unsafe 230    unsafe 2.8  unsafe 1.9  unsafe 0.17 unsafe 0.12 unsafe 2.6 
email_spec3_product27_unsafe.cil.c unsafe 4.9  unsafe 220    unsafe 3.1  unsafe 2.1  unsafe 0.13 unsafe 0.13 unsafe 2.8 
email_spec3_product28_unsafe.cil.c unsafe 100    unsafe 130    unsafe 2.9  unsafe 0.96 unsafe 0.10 unsafe 0.13 unsafe 1.2 
email_spec3_product29_unsafe.cil.c unsafe 110    timeout 900    unsafe 2.9  unsafe 1.3  unsafe 0.20 unsafe 0.14 unsafe 1.7 
email_spec3_product30_unsafe.cil.c unsafe 5.2  unsafe 330    unsafe 3.1  unsafe 1.2  unsafe 0.10 unsafe 0.12 unsafe 1.3 
email_spec3_product31_unsafe.cil.c unsafe 110    unsafe 130    unsafe 2.9  unsafe 1.3  unsafe 0.12 unsafe 0.12 unsafe 1.3 
email_spec3_product32_unsafe.cil.c unsafe 5.6  timeout 900    unsafe 3.4  unsafe 2.4  unsafe 0.19 unsafe 0.13 unsafe 3.5 
email_spec3_product33_unsafe.cil.c unsafe 5.2  unsafe 320    unsafe 3.2  unsafe 1.4  unsafe 0.11 unsafe 0.13 unsafe 1.8 
email_spec3_product34_unsafe.cil.c unsafe 120    timeout 900    unsafe 2.9  unsafe 2.6  unsafe 0.22 unsafe 0.14 unsafe 3.9 
email_spec3_product35_unsafe.cil.c unsafe 5.7  timeout 900    unsafe 3.3  unsafe 2.8  unsafe 0.20 unsafe 0.14 unsafe 3.9 
email_spec3_productSimulator_unsafe.cil.c unsafe 17    timeout 900    unsafe 16    unsafe 46    unsafe 6.7  unsafe 0.15 unsafe 23   
email_spec4_product18_unsafe.cil.c timeout 910    timeout 900    unsafe 3.0  unsafe 1.1  unsafe 0.95 unsafe 0.59 unsafe 2.0 
email_spec4_product19_unsafe.cil.c timeout 910    timeout 900    unsafe 2.9  unsafe 1.1  unsafe 0.85 unsafe 0.39 unsafe 2.1 
email_spec4_product23_unsafe.cil.c timeout 910    timeout 900    unsafe 2.9  unsafe 1.6  unsafe 2.3  unsafe 0.66 unsafe 3.6 
email_spec4_product24_unsafe.cil.c timeout 910    timeout 900    unsafe 2.9  unsafe 1.1  unsafe 1.1  unsafe 0.49 unsafe 3.1 
email_spec4_product25_unsafe.cil.c timeout 910    timeout 900    unsafe 3.1  unsafe 1.7  unsafe 1.8  unsafe 0.43 unsafe 5.8 
email_spec4_product27_unsafe.cil.c timeout 910    timeout 900    unsafe 3.0  unsafe 1.8  unsafe 2.7  unsafe 0.55 unsafe 6.3 
email_spec4_product30_unsafe.cil.c timeout 910    timeout 900    unsafe 3.0  unsafe 1.2  unsafe 1.2  unsafe 0.72 unsafe 2.1 
email_spec4_product31_unsafe.cil.c timeout 910    timeout 900    unsafe 3.2  unsafe 1.4  unsafe 1.3  unsafe 0.46 unsafe 2.4 
email_spec4_product32_unsafe.cil.c timeout 910    timeout 900    unsafe 3.1  unsafe 2.1  unsafe 3.3  unsafe 0.79 unsafe 8.3 
email_spec4_product33_unsafe.cil.c timeout 910    timeout 900    unsafe 3.0  unsafe 1.5  unsafe 1.2  unsafe 0.59 unsafe 3.9 
email_spec4_product34_unsafe.cil.c timeout 910    timeout 900    unsafe 3.4  unsafe 2.5  unsafe 3.3  unsafe 0.52 unsafe 9.1 
email_spec4_product35_unsafe.cil.c timeout 910    timeout 900    unsafe 3.0  unsafe 2.4  unsafe 3.8  unsafe 0.64 unsafe 8.2 
email_spec4_productSimulator_unsafe.cil.c timeout 910    timeout 900    segmentation fault 280    unsafe 39    unsafe 62    unsafe 9.6  unsafe 69   
email_spec6_product12_unsafe.cil.c timeout 910    unsafe 110    unsafe 2.8  unsafe 0.96 unsafe 0.75 unsafe 1.1  unsafe 1.9 
email_spec6_product14_unsafe.cil.c timeout 910    unsafe 170    unsafe 2.8  unsafe 1.1  unsafe 1.5  unsafe 1.2  unsafe 2.1 
email_spec6_product15_unsafe.cil.c timeout 910    unsafe 110    unsafe 2.8  unsafe 1.1  unsafe 0.92 unsafe 1.9  unsafe 1.6 
email_spec6_product16_unsafe.cil.c timeout 910    timeout 900    unsafe 2.7  unsafe 1.1  unsafe 0.93 unsafe 1.4  unsafe 1.9 
email_spec6_product20_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 2.2  unsafe 2.2  unsafe 2.3  unsafe 5.0 
email_spec6_product21_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 1.8  unsafe 1.9  unsafe 1.5  unsafe 6.0 
email_spec6_product22_unsafe.cil.c timeout 910    unsafe 150    unsafe 2.7  unsafe 1.2  unsafe 1.00 unsafe 3.0  unsafe 3.2 
email_spec6_product26_unsafe.cil.c unsafe 550    timeout 900    unsafe 2.7  unsafe 2.0  unsafe 2.3  unsafe 3.8  unsafe 7.9 
email_spec6_product28_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 0.95 unsafe 0.83 unsafe 1.4  unsafe 1.9 
email_spec6_product29_unsafe.cil.c timeout 910    timeout 900    unsafe 2.7  unsafe 1.2  unsafe 1.8  unsafe 1.6  unsafe 3.1 
email_spec6_product30_unsafe.cil.c unsafe 480    timeout 900    unsafe 2.8  unsafe 1.2  unsafe 1.2  unsafe 3.4  unsafe 2.0 
email_spec6_product31_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 1.3  unsafe 1.0  unsafe 2.1  unsafe 2.3 
email_spec6_product32_unsafe.cil.c unsafe 520    timeout 900    unsafe 2.8  unsafe 2.2  unsafe 2.9  unsafe 4.0  unsafe 6.4 
email_spec6_product33_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 1.3  unsafe 1.2  unsafe 6.0  unsafe 3.6 
email_spec6_product34_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 2.4  unsafe 2.3  unsafe 2.3  unsafe 5.6 
email_spec6_product35_unsafe.cil.c unsafe 570    timeout 900    unsafe 2.8  unsafe 2.5  unsafe 2.5  unsafe 7.1  unsafe 8.5 
email_spec6_productSimulator_unsafe.cil.c timeout 910    timeout 900    unknown 280    unsafe 42    unsafe 50    unsafe 2.3  unsafe 41   
email_spec7_product28_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 0.95 unsafe 0.80 unsafe 1.3  unsafe 2.0 
email_spec7_product29_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 1.2  unsafe 1.7  unsafe 1.5  unsafe 2.4 
email_spec7_product30_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 1.2  unsafe 1.0  unsafe 3.4  unsafe 1.7 
email_spec7_product31_unsafe.cil.c timeout 910    unsafe 490    unsafe 2.8  unsafe 1.2  unsafe 0.97 unsafe 2.1  unsafe 1.8 
email_spec7_product32_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 2.0  unsafe 2.2  unsafe 3.9  unsafe 7.5 
email_spec7_product33_unsafe.cil.c timeout 910    timeout 900    unsafe 2.9  unsafe 1.2  unsafe 1.0  unsafe 5.9  unsafe 2.9 
email_spec7_product34_unsafe.cil.c timeout 910    timeout 900    unsafe 2.7  unsafe 2.2  unsafe 2.2  unsafe 2.3  unsafe 8.3 
email_spec7_product35_unsafe.cil.c timeout 910    timeout 900    unsafe 2.8  unsafe 2.3  unsafe 2.6  unsafe 6.9  unsafe 9.6 
email_spec7_productSimulator_unsafe.cil.c timeout 910    timeout 900    segmentation fault 160    unsafe 50    unsafe 100    unsafe 2.2  unsafe 74   
email_spec8_product15_unsafe.cil.c timeout 910    timeout 900    unsafe 4.1  unsafe 1.2  unsafe 1.1  unsafe 2.1  unsafe 2.0 
email_spec8_product16_unsafe.cil.c timeout 910    timeout 900    unsafe 3.3  unsafe 1.1  unsafe 1.1  unsafe 1.5  unsafe 2.2 
email_spec8_product20_unsafe.cil.c timeout 910    timeout 900    unsafe 4.4  unsafe 1.7  unsafe 2.6  unsafe 2.5  unsafe 4.6 
email_spec8_product21_unsafe.cil.c timeout 910    timeout 900    unsafe 3.6  unsafe 1.7  unsafe 2.1  unsafe 1.7  unsafe 7.6 
email_spec8_product22_unsafe.cil.c timeout 910    timeout 900    unsafe 3.7  unsafe 1.2  unsafe 1.1  unsafe 3.3  unsafe 2.9 
email_spec8_product26_unsafe.cil.c timeout 910    timeout 900    unsafe 4.0  unsafe 1.9  unsafe 2.3  unsafe 4.2  unsafe 9.1 
email_spec8_product30_unsafe.cil.c timeout 910    timeout 900    unsafe 4.5  unsafe 1.2  unsafe 1.1  unsafe 3.8  unsafe 1.7 
email_spec8_product31_unsafe.cil.c timeout 910    timeout 900    unsafe 3.8  unsafe 1.2  unsafe 1.3  unsafe 2.4  unsafe 2.1 
email_spec8_product32_unsafe.cil.c timeout 910    timeout 900    unsafe 4.7  unsafe 2.4  unsafe 3.4  unsafe 4.4  unsafe 8.0 
email_spec8_product33_unsafe.cil.c timeout 910    timeout 900    unsafe 4.1  unsafe 1.3  unsafe 1.3  unsafe 6.7  unsafe 3.4 
email_spec8_product34_unsafe.cil.c timeout 910    timeout 900    unsafe 3.8  unsafe 2.3  unsafe 3.5  unsafe 2.7  unsafe 9.5 
email_spec8_product35_unsafe.cil.c timeout 910    timeout 900    unsafe 4.2  unsafe 2.4  unsafe 3.2  unsafe 8.0  unsafe 8.7 
email_spec8_productSimulator_unsafe.cil.c timeout 910    timeout 900    unknown 420    unsafe 41    unsafe 57    unsafe 16    unsafe 62   
email_spec9_product15_unsafe.cil.c timeout 910    timeout 900    unsafe 4.2  unsafe 1.1  unsafe 1.1  unsafe 2.0  unsafe 2.0 
email_spec9_product16_unsafe.cil.c timeout 910    timeout 900    unsafe 3.5  unsafe 1.1  unsafe 0.95 unsafe 1.5  unsafe 2.2 
email_spec9_product20_unsafe.cil.c timeout 910    timeout 900    unsafe 4.5  unsafe 2.0  unsafe 2.5  unsafe 2.5  unsafe 6.2 
email_spec9_product21_unsafe.cil.c timeout 910    timeout 900    unsafe 3.5  unsafe 1.7  unsafe 2.5  unsafe 1.8  unsafe 7.3 
email_spec9_product22_unsafe.cil.c timeout 910    timeout 900    unsafe 3.8  unsafe 1.1  unsafe 1.2  unsafe 3.3  unsafe 3.0 
email_spec9_product26_unsafe.cil.c timeout 910    timeout 900    unsafe 4.0  unsafe 1.9  unsafe 2.3  unsafe 4.2  unsafe 8.8 
email_spec9_product30_unsafe.cil.c timeout 910    timeout 900    unsafe 4.7  unsafe 1.2  unsafe 1.1  unsafe 3.8  unsafe 2.2 
email_spec9_product31_unsafe.cil.c timeout 910    timeout 900    unsafe 3.8  unsafe 1.2  unsafe 1.3  unsafe 2.4  unsafe 2.6 
email_spec9_product32_unsafe.cil.c timeout 910    timeout 900    unsafe 4.8  unsafe 2.2  unsafe 3.0  unsafe 4.4  unsafe 8.0 
email_spec9_product33_unsafe.cil.c timeout 910    timeout 900    unsafe 4.2  unsafe 1.6  unsafe 1.2  unsafe 6.7  unsafe 3.9 
email_spec9_product34_unsafe.cil.c timeout 910    timeout 900    unsafe 4.0  unsafe 2.3  unsafe 3.0  unsafe 2.7  unsafe 9.6 
email_spec9_product35_unsafe.cil.c timeout 910    timeout 900    unsafe 4.3  unsafe 2.4  unsafe 3.6  unsafe 8.0  unsafe 8.2 
email_spec9_productSimulator_unsafe.cil.c timeout 910    timeout 900    segmentation fault 390    unsafe 41    unsafe 52    unsafe 16    unsafe 80   
email_spec0_product05_safe.cil.c safe 0.47 safe 3.3  safe 13    safe 0.73 safe 0.33 safe 5.8  safe 0.47
email_spec0_product09_safe.cil.c safe 0.80 safe 3.9  safe 18    safe 0.83 safe 0.47 safe 8.3  safe 0.47
email_spec0_product10_safe.cil.c safe 0.63 safe 3.2  safe 18    safe 0.75 safe 0.37 safe 5.9  safe 0.47
email_spec0_product11_safe.cil.c safe 0.89 safe 3.9  safe 25    safe 0.81 safe 0.59 safe 30    safe 0.47
email_spec0_product19_safe.cil.c safe 1.2  safe 4.0  safe 42    safe 0.88 safe 0.65 safe 120    safe 0.50
email_spec0_product24_safe.cil.c safe 1.4  safe 4.0  safe 48    safe 0.90 safe 0.66 safe 220    safe 0.54
email_spec0_product25_safe.cil.c safe 2.2  safe 5.1  safe 50    safe 1.2  safe 0.97 safe 430    safe 0.54
email_spec0_product27_safe.cil.c safe 2.7  safe 4.9  safe 69    safe 1.2  safe 0.95 safe 700    safe 0.55
email_spec0_product36_safe.cil.c safe 1.1  safe 3.8  safe 22    safe 0.98 safe 0.53 safe 12    safe 0.50
email_spec0_product37_safe.cil.c safe 1.3  safe 4.2  safe 35    safe 0.85 safe 0.62 safe 51    safe 0.50
email_spec0_product38_safe.cil.c safe 1.3  safe 4.5  safe 34    safe 0.92 safe 0.77 safe 87    safe 0.49
email_spec0_product40_safe.cil.c safe 2.0  safe 4.7  safe 43    safe 0.96 safe 0.81 safe 160    safe 0.51
email_spec11_product03_safe.cil.c safe 0.44 safe 3.1  safe 13    safe 0.70 safe 0.32 safe 6.1  safe 0.49
email_spec11_product07_safe.cil.c safe 0.70 safe 3.4  safe 17    safe 0.86 safe 0.46 safe 12    safe 0.49
email_spec11_product08_safe.cil.c safe 1.00 safe 3.7  safe 23    safe 0.79 safe 0.59 safe 25    safe 0.46
email_spec11_product10_safe.cil.c safe 0.57 safe 3.4  safe 18    safe 0.74 safe 0.34 safe 6.5  safe 0.49
email_spec11_product18_safe.cil.c safe 1.2  safe 4.4  safe 41    safe 0.89 safe 0.65 safe 58    safe 0.48
email_spec11_product23_safe.cil.c safe 2.0  safe 4.8  safe 48    safe 1.1  safe 0.91 safe 280    safe 0.50
email_spec11_product24_safe.cil.c safe 1.4  safe 4.5  safe 62    safe 0.89 safe 0.69 safe 220    safe 0.48
email_spec11_product27_safe.cil.c safe 2.8  safe 5.4  safe 79    safe 1.2  safe 1.1  safe 700    safe 0.55
email_spec11_product36_safe.cil.c safe 1.00 safe 3.7  safe 24    safe 0.92 safe 0.52 safe 9.0  safe 0.50
email_spec11_product37_safe.cil.c safe 1.2  safe 4.0  safe 32    safe 0.88 safe 0.61 safe 50    safe 0.49
email_spec11_product39_safe.cil.c safe 1.5  safe 4.4  safe 35    safe 0.90 safe 0.78 safe 66    safe 0.51
email_spec11_product40_safe.cil.c safe 2.0  safe 4.3  safe 40    safe 1.0  safe 0.82 safe 160    safe 0.51
email_spec1_product12_safe.cil.c safe 0.87 timeout 900    safe 31    safe 0.82 safe 1.5  safe 21    safe 0.44
email_spec1_product28_safe.cil.c safe 1.1  timeout 900    safe 35    safe 0.85 safe 1.8  safe 25    safe 0.50
email_spec27_product13_safe.cil.c unsafe 48    safe 180    safe 34    safe 0.88 safe 1.6  safe 24    safe 0.81
email_spec27_product28_safe.cil.c unsafe 97    timeout 900    safe 42    safe 0.92 safe 1.9  safe 26    safe 0.89
email_spec4_product13_safe.cil.c safe 17    safe 38    safe 35    safe 0.86 safe 1.4  safe 24    safe 0.48
email_spec4_product17_safe.cil.c safe 86    safe 43    safe 41    safe 0.94 safe 5.0  safe 100    safe 0.52
email_spec4_product28_safe.cil.c safe 110    timeout 900    safe 44    safe 0.91 safe 1.8  safe 24    safe 0.49
email_spec4_product29_safe.cil.c safe 540    safe 100    safe 55    safe 1.0  safe 5.5  safe 140    safe 0.50
email_spec7_product13_safe.cil.c safe 0.88 safe 3.7  safe 34    safe 0.86 safe 0.60 safe 24    safe 0.52
email_spec7_product17_safe.cil.c safe 1.1  safe 4.3  safe 43    safe 0.97 safe 0.85 safe 97    safe 0.51
email_spec7_product18_safe.cil.c safe 1.2  safe 3.8  safe 36    safe 0.87 safe 0.65 safe 59    safe 0.51
email_spec7_product19_safe.cil.c safe 1.2  safe 3.9  safe 47    safe 0.97 safe 0.63 safe 120    safe 0.50
email_spec7_product23_safe.cil.c safe 2.0  safe 4.4  safe 49    safe 1.1  safe 0.89 safe 280    safe 0.52
email_spec7_product24_safe.cil.c safe 1.4  safe 4.0  safe 61    safe 0.92 safe 0.69 safe 220    safe 0.49
email_spec7_product25_safe.cil.c safe 2.2  safe 4.9  safe 55    safe 1.1  safe 0.96 safe 430    safe 0.55
email_spec7_product27_safe.cil.c safe 2.7  safe 5.1  safe 83    safe 1.1  safe 0.99 safe 700    safe 0.54
email_spec8_product12_safe.cil.c safe 0.90 safe 18    safe 31    safe 0.81 safe 1.4  safe 21    safe 0.50
email_spec8_product14_safe.cil.c timeout 910    timeout 900    safe 35    safe 1.00 safe 4.7  safe 70    safe 4.6 
email_spec8_product28_safe.cil.c safe 1.1  safe 740    safe 40    safe 0.84 safe 1.6  safe 24    safe 0.49
email_spec8_product29_safe.cil.c timeout 910    timeout 900    safe 84    safe 1.1  safe 5.4  safe 140    safe 3.0 
email_spec9_product12_safe.cil.c safe 0.91 safe 18    safe 32    safe 0.87 safe 1.4  safe 22    safe 0.51
email_spec9_product14_safe.cil.c timeout 910    timeout 900    safe 41    safe 0.99 safe 4.6  safe 70    safe 4.4 
email_spec9_product28_safe.cil.c safe 1.1  safe 750    safe 40    safe 0.86 safe 1.8  safe 24    safe 0.52
email_spec9_product29_safe.cil.c timeout 910    timeout 900    safe 77    safe 1.2  safe 5.5  safe 140    safe 3.1 
minepump_spec1_product33_unsafe.cil.c unsafe 0.70 unsafe 2.5  unsafe 1.5  unsafe 0.42 unsafe 0.07 unsafe 0.07 unsafe 0.60
minepump_spec1_product34_unsafe.cil.c unsafe 0.72 unsafe 2.4  unsafe 1.7  unsafe 0.44 unsafe 0.06 unsafe 0.08 unsafe 0.62
minepump_spec1_product35_unsafe.cil.c unsafe 0.82 unsafe 2.8  unsafe 1.6  unsafe 0.43 unsafe 0.07 unsafe 0.07 unsafe 0.68
minepump_spec1_product36_unsafe.cil.c unsafe 0.84 unsafe 2.7  unsafe 1.6  unsafe 0.44 unsafe 0.07 unsafe 0.08 unsafe 0.67
minepump_spec1_product37_unsafe.cil.c unsafe 0.71 unsafe 2.4  unsafe 1.6  unsafe 0.44 unsafe 0.06 unsafe 0.08 unsafe 0.63
minepump_spec1_product38_unsafe.cil.c unsafe 0.73 unsafe 2.4  unsafe 1.6  unsafe 0.45 unsafe 0.06 unsafe 0.08 unsafe 0.65
minepump_spec1_product39_unsafe.cil.c unsafe 0.84 unsafe 2.8  unsafe 1.6  unsafe 0.48 unsafe 0.06 unsafe 0.07 unsafe 0.69
minepump_spec1_product40_unsafe.cil.c unsafe 0.86 unsafe 2.4  unsafe 1.6  unsafe 0.44 unsafe 0.08 unsafe 0.08 unsafe 0.69
minepump_spec1_product41_unsafe.cil.c unsafe 7.3  unsafe 3.6  unsafe 1.7  unsafe 0.42 unsafe 0.09 unsafe 0.08 unsafe 0.74
minepump_spec1_product42_unsafe.cil.c unsafe 7.4  unsafe 3.2  unsafe 1.7  unsafe 0.42 unsafe 0.09 unsafe 0.09 unsafe 0.73
minepump_spec1_product43_unsafe.cil.c unsafe 16    unsafe 3.8  unsafe 1.7  unsafe 0.42 unsafe 0.10 unsafe 0.08 unsafe 0.80
minepump_spec1_product44_unsafe.cil.c unsafe 17    unsafe 3.4  unsafe 1.7  unsafe 0.42 unsafe 0.10 unsafe 0.10 unsafe 0.87
minepump_spec1_product49_unsafe.cil.c unsafe 0.70 unsafe 2.5  unsafe 1.6  unsafe 0.50 unsafe 0.06 unsafe 0.07 unsafe 0.64
minepump_spec1_product50_unsafe.cil.c unsafe 0.72 unsafe 2.5  unsafe 1.6  unsafe 0.49 unsafe 0.07 unsafe 0.07 unsafe 0.60
minepump_spec1_product51_unsafe.cil.c unsafe 0.84 unsafe 2.6  unsafe 1.6  unsafe 0.50 unsafe 0.06 unsafe 0.07 unsafe 0.67
minepump_spec1_product52_unsafe.cil.c unsafe 0.86 unsafe 2.5  unsafe 1.6  unsafe 0.51 unsafe 0.07 unsafe 0.07 unsafe 0.74
minepump_spec1_product53_unsafe.cil.c unsafe 0.71 unsafe 2.4  unsafe 1.6  unsafe 0.60 unsafe 0.07 unsafe 0.07 unsafe 0.71
minepump_spec1_product54_unsafe.cil.c unsafe 0.73 unsafe 2.6  unsafe 1.6  unsafe 0.62 unsafe 0.06 unsafe 0.08 unsafe 0.66
minepump_spec1_product55_unsafe.cil.c unsafe 0.85 unsafe 2.9  unsafe 1.6  unsafe 0.60 unsafe 0.08 unsafe 0.08 unsafe 0.77
minepump_spec1_product56_unsafe.cil.c unsafe 0.87 unsafe 2.5  unsafe 1.6  unsafe 0.60 unsafe 0.07 unsafe 0.09 unsafe 0.76
minepump_spec1_productSimulator_unsafe.cil.c unsafe 1.5  unsafe 5.2  unsafe 3.0  unsafe 1.2  unsafe 0.13 unsafe 37    unsafe 1.0 
minepump_spec2_product33_unsafe.cil.c unsafe 6.2  unsafe 3.7  unsafe 1.8  unsafe 0.44 unsafe 0.10 unsafe 0.06 unsafe 0.73
minepump_spec2_product34_unsafe.cil.c unsafe 6.3  unsafe 3.7  unsafe 2.0  unsafe 0.46 unsafe 0.10 unsafe 0.09 unsafe 0.76
minepump_spec2_product35_unsafe.cil.c unsafe 17    unsafe 3.9  unsafe 2.0  unsafe 0.43 unsafe 0.11 unsafe 0.09 unsafe 0.87
minepump_spec2_product36_unsafe.cil.c unsafe 17    unsafe 3.7  unsafe 2.0  unsafe 0.44 unsafe 0.11 unsafe 0.09 unsafe 0.84
minepump_spec2_product41_unsafe.cil.c unsafe 19    unsafe 5.4  unsafe 1.9  unsafe 0.46 unsafe 0.15 unsafe 0.09 unsafe 0.91
minepump_spec2_product42_unsafe.cil.c unsafe 20    unsafe 4.7  unsafe 2.1  unsafe 0.43 unsafe 0.15 unsafe 0.08 unsafe 0.96
minepump_spec2_product43_unsafe.cil.c unsafe 58    unsafe 4.1  unsafe 2.2  unsafe 0.45 unsafe 0.16 unsafe 0.09 unsafe 1.1 
minepump_spec2_product44_unsafe.cil.c unsafe 51    unsafe 4.4  unsafe 2.3  unsafe 0.45 unsafe 0.16 unsafe 0.12 unsafe 1.3 
minepump_spec2_productSimulator_unsafe.cil.c unsafe 450    unsafe 7.2  unsafe 4.0  unsafe 0.95 unsafe 0.25 unsafe 62    unsafe 1.3 
minepump_spec3_product01_unsafe.cil.c unsafe 0.10 unsafe 2.2  unsafe 1.5  unsafe 0.39 unsafe 0.05 unsafe 0.07 unsafe 0.54
minepump_spec3_product02_unsafe.cil.c unsafe 0.11 unsafe 2.1  unsafe 1.6  unsafe 0.41 unsafe 0.05 unsafe 0.06 unsafe 0.55
minepump_spec3_product03_unsafe.cil.c unsafe 0.11 unsafe 2.1  unsafe 1.7  unsafe 0.39 unsafe 0.06 unsafe 0.07 unsafe 0.57
minepump_spec3_product04_unsafe.cil.c unsafe 0.96 unsafe 2.1  unsafe 1.6  unsafe 0.41 unsafe 0.06 unsafe 0.06 unsafe 0.56
minepump_spec3_product05_unsafe.cil.c unsafe 0.11 unsafe 2.5  unsafe 1.6  unsafe 0.38 unsafe 0.06 unsafe 0.07 unsafe 0.55
minepump_spec3_product06_unsafe.cil.c unsafe 0.12 unsafe 2.5  unsafe 1.6  unsafe 0.37 unsafe 0.06 unsafe 0.06 unsafe 0.55
minepump_spec3_product07_unsafe.cil.c unsafe 0.95 unsafe 2.2  unsafe 1.6  unsafe 0.41 unsafe 0.06 unsafe 0.07 unsafe 0.56
minepump_spec3_product08_unsafe.cil.c unsafe 0.96 unsafe 2.3  unsafe 1.6  unsafe 0.38 unsafe 0.06 unsafe 0.06 unsafe 0.55
minepump_spec3_product09_unsafe.cil.c unsafe 0.11 unsafe 2.2  unsafe 1.5  unsafe 0.39 unsafe 0.05 unsafe 0.06 unsafe 0.54
minepump_spec3_product10_unsafe.cil.c unsafe 0.11 unsafe 2.1  unsafe 1.5  unsafe 0.38 unsafe 0.06 unsafe 0.06 unsafe 0.56
minepump_spec3_product11_unsafe.cil.c unsafe 0.11 unsafe 2.1  unsafe 1.6  unsafe 0.40 unsafe 0.06 unsafe 0.07 unsafe 0.56
minepump_spec3_product12_unsafe.cil.c unsafe 0.96 unsafe 2.2  unsafe 1.6  unsafe 0.40 unsafe 0.05 unsafe 0.06 unsafe 0.58
minepump_spec3_product13_unsafe.cil.c unsafe 0.11 unsafe 2.1  unsafe 1.6  unsafe 0.40 unsafe 0.06 unsafe 0.06 unsafe 0.55
minepump_spec3_product14_unsafe.cil.c unsafe 0.12 unsafe 2.5  unsafe 1.6  unsafe 0.37 unsafe 0.06 unsafe 0.07 unsafe 0.56
minepump_spec3_product15_unsafe.cil.c unsafe 0.95 unsafe 2.2  unsafe 1.6  unsafe 0.40 unsafe 0.06 unsafe 0.08 unsafe 0.57
minepump_spec3_product16_unsafe.cil.c unsafe 0.95 unsafe 2.5  unsafe 1.6  unsafe 0.38 unsafe 0.06 unsafe 0.08 unsafe 0.53
minepump_spec3_product17_unsafe.cil.c unsafe 0.11 unsafe 2.3  unsafe 1.6  unsafe 0.40 unsafe 0.06 unsafe 0.08 unsafe 0.55
minepump_spec3_product18_unsafe.cil.c unsafe 0.11 unsafe 2.3  unsafe 1.6  unsafe 0.52 unsafe 0.06 unsafe 0.07 unsafe 0.56
minepump_spec3_product19_unsafe.cil.c unsafe 0.96 unsafe 2.3  unsafe 1.6  unsafe 0.47 unsafe 0.07 unsafe 0.09 unsafe 0.56
minepump_spec3_product20_unsafe.cil.c unsafe 0.95 unsafe 2.7  unsafe 1.6  unsafe 0.41 unsafe 0.06 unsafe 0.07 unsafe 0.56
minepump_spec3_product21_unsafe.cil.c unsafe 0.11 unsafe 3.0  unsafe 1.6  unsafe 0.42 unsafe 0.05 unsafe 0.07 unsafe 0.56
minepump_spec3_product22_unsafe.cil.c unsafe 0.11 unsafe 2.5  unsafe 1.6  unsafe 0.45 unsafe 0.06 unsafe 0.07 unsafe 0.56
minepump_spec3_product23_unsafe.cil.c unsafe 0.95 unsafe 2.2  unsafe 1.6  unsafe 0.41 unsafe 0.07 unsafe 0.07 unsafe 0.58
minepump_spec3_product24_unsafe.cil.c unsafe 0.96 unsafe 3.3  unsafe 1.6  unsafe 0.39 unsafe 0.06 unsafe 0.06 unsafe 0.55
minepump_spec3_product25_unsafe.cil.c unsafe 0.11 unsafe 2.3  unsafe 1.6  unsafe 0.40 unsafe 0.06 unsafe 0.07 unsafe 0.56
minepump_spec3_product26_unsafe.cil.c unsafe 0.12 unsafe 2.3  unsafe 1.6  unsafe 0.42 unsafe 0.06 unsafe 0.06 unsafe 0.54
minepump_spec3_product27_unsafe.cil.c unsafe 0.95 unsafe 2.4  unsafe 1.6  unsafe 0.42 unsafe 0.06 unsafe 0.08 unsafe 0.58
minepump_spec3_product28_unsafe.cil.c unsafe 0.95 unsafe 2.7  unsafe 1.6  unsafe 0.41 unsafe 0.06 unsafe 0.08 unsafe 0.53
minepump_spec3_product29_unsafe.cil.c unsafe 0.11 unsafe 2.4  unsafe 1.6  unsafe 0.40 unsafe 0.06 unsafe 0.08 unsafe 0.58
minepump_spec3_product30_unsafe.cil.c unsafe 0.12 unsafe 2.5  unsafe 1.6  unsafe 0.40 unsafe 0.07 unsafe 0.06 unsafe 0.56
minepump_spec3_product31_unsafe.cil.c unsafe 0.96 unsafe 2.2  unsafe 1.6  unsafe 0.39 unsafe 0.06 unsafe 0.07 unsafe 0.61
minepump_spec3_product32_unsafe.cil.c unsafe 0.96 unsafe 3.2  unsafe 1.6  unsafe 0.40 unsafe 0.06 unsafe 0.07 unsafe 0.55
minepump_spec3_product35_unsafe.cil.c unsafe 1.1  unsafe 2.3  unsafe 1.9  unsafe 0.45 unsafe 0.06 unsafe 0.08 unsafe 0.70
minepump_spec3_product36_unsafe.cil.c unsafe 1.1  unsafe 3.3  unsafe 2.0  unsafe 0.48 unsafe 0.06 unsafe 0.07 unsafe 0.71
minepump_spec3_product39_unsafe.cil.c unsafe 1.1  unsafe 2.3  unsafe 1.8  unsafe 0.46 unsafe 0.08 unsafe 0.09 unsafe 0.67
minepump_spec3_product40_unsafe.cil.c unsafe 1.1  unsafe 3.6  unsafe 1.7  unsafe 0.47 unsafe 0.08 unsafe 0.07 unsafe 0.76
minepump_spec3_product43_unsafe.cil.c unsafe 1.1  unsafe 2.4  unsafe 2.0  unsafe 0.41 unsafe 0.07 unsafe 0.07 unsafe 0.66
minepump_spec3_product44_unsafe.cil.c unsafe 1.1  unsafe 3.8  unsafe 2.0  unsafe 0.44 unsafe 0.06 unsafe 0.08 unsafe 0.70
minepump_spec3_product47_unsafe.cil.c unsafe 1.1  unsafe 2.3  unsafe 1.8  unsafe 0.45 unsafe 0.07 unsafe 0.08 unsafe 0.74
minepump_spec3_product48_unsafe.cil.c unsafe 1.1  unsafe 4.1  unsafe 1.8  unsafe 0.46 unsafe 0.07 unsafe 0.08 unsafe 0.72
minepump_spec3_product51_unsafe.cil.c unsafe 1.1  unsafe 2.4  unsafe 1.6  unsafe 0.50 unsafe 0.07 unsafe 0.07 unsafe 0.71
minepump_spec3_product52_unsafe.cil.c unsafe 1.1  unsafe 3.9  unsafe 1.6  unsafe 0.48 unsafe 0.07 unsafe 0.07 unsafe 0.68
minepump_spec3_product55_unsafe.cil.c unsafe 1.1  unsafe 2.2  unsafe 1.6  unsafe 0.62 unsafe 0.08 unsafe 0.08 unsafe 0.70
minepump_spec3_product56_unsafe.cil.c unsafe 1.1  unsafe 4.2  unsafe 1.7  unsafe 0.59 unsafe 0.08 unsafe 0.08 unsafe 0.74
minepump_spec3_product59_unsafe.cil.c unsafe 1.1  unsafe 2.4  unsafe 1.8  unsafe 0.52 unsafe 0.08 unsafe 0.08 unsafe 0.72
minepump_spec3_product60_unsafe.cil.c unsafe 1.1  unsafe 4.4  unsafe 1.8  unsafe 0.49 unsafe 0.07 unsafe 0.08 unsafe 0.75
minepump_spec3_product63_unsafe.cil.c unsafe 1.1  unsafe 2.3  unsafe 1.8  unsafe 0.59 unsafe 0.08 unsafe 0.08 unsafe 0.83
minepump_spec3_product64_unsafe.cil.c unsafe 1.1  unsafe 4.9  unsafe 1.9  unsafe 0.62 unsafe 0.07 unsafe 0.07 unsafe 0.77
minepump_spec3_productSimulator_unsafe.cil.c unsafe 1.6  unsafe 6.3  unsafe 2.8  unsafe 0.94 unsafe 0.13 unsafe 0.93 unsafe 0.94
minepump_spec4_product33_unsafe.cil.c unsafe 21    unsafe 2.6  unsafe 1.7  unsafe 0.39 unsafe 0.14 unsafe 0.07 unsafe 0.79
minepump_spec4_product34_unsafe.cil.c unsafe 18    unsafe 3.2  unsafe 1.7  unsafe 0.39 unsafe 0.15 unsafe 0.06 unsafe 0.80
minepump_spec4_product35_unsafe.cil.c unsafe 35    unsafe 3.3  unsafe 1.7  unsafe 0.41 unsafe 0.16 unsafe 0.09 unsafe 0.96
minepump_spec4_product36_unsafe.cil.c unsafe 28    unsafe 3.2  unsafe 1.7  unsafe 0.42 unsafe 0.16 unsafe 0.12 unsafe 1.1 
minepump_spec4_product37_unsafe.cil.c unsafe 37    unsafe 4.0  unsafe 1.9  unsafe 0.46 unsafe 0.17 unsafe 0.07 unsafe 0.98
minepump_spec4_product38_unsafe.cil.c unsafe 37    unsafe 3.7  unsafe 1.9  unsafe 0.43 unsafe 0.16 unsafe 0.06 unsafe 0.88
minepump_spec4_product39_unsafe.cil.c unsafe 75    unsafe 3.9  unsafe 2.1  unsafe 0.47 unsafe 0.17 unsafe 0.08 unsafe 1.3 
minepump_spec4_product40_unsafe.cil.c unsafe 31    unsafe 4.1  unsafe 2.1  unsafe 0.49 unsafe 0.18 unsafe 0.08 unsafe 1.2 
minepump_spec4_product41_unsafe.cil.c unsafe 25    unsafe 3.2  unsafe 1.8  unsafe 0.43 unsafe 0.16 unsafe 0.07 unsafe 0.87
minepump_spec4_product42_unsafe.cil.c unsafe 30    unsafe 3.3  unsafe 1.8  unsafe 0.41 unsafe 0.15 unsafe 0.07 unsafe 0.88
minepump_spec4_product43_unsafe.cil.c unsafe 89    unsafe 3.6  unsafe 1.8  unsafe 0.42 unsafe 0.17 unsafe 0.08 unsafe 1.1 
minepump_spec4_product44_unsafe.cil.c unsafe 110    unsafe 3.2  unsafe 1.8  unsafe 0.44 unsafe 0.16 unsafe 0.09 unsafe 1.1 
minepump_spec4_product45_unsafe.cil.c unsafe 45    unsafe 4.1  unsafe 2.0  unsafe 0.45 unsafe 0.17 unsafe 0.07 unsafe 0.89
minepump_spec4_product46_unsafe.cil.c unsafe 52    unsafe 3.8  unsafe 2.0  unsafe 0.47 unsafe 0.18 unsafe 0.07 unsafe 0.89
minepump_spec4_product47_unsafe.cil.c unsafe 44    unsafe 4.1  unsafe 2.2  unsafe 0.47 unsafe 0.19 unsafe 0.10 unsafe 1.3 
minepump_spec4_product48_unsafe.cil.c unsafe 170    unsafe 3.9  unsafe 2.1  unsafe 0.50 unsafe 0.18 unsafe 0.09 unsafe 1.2 
minepump_spec4_productSimulator_unsafe.cil.c timeout 910    unsafe 9.7  unsafe 4.8  unsafe 0.92 unsafe 0.45 unsafe 2.7  unsafe 2.4 
minepump_spec1_product01_safe.cil.c safe 0.08 safe 1.9  safe 1.3  safe 0.40 safe 0.74 safe 0.19 safe 0.42
minepump_spec1_product02_safe.cil.c safe 0.09 safe 1.9  safe 1.3  safe 0.38 safe 0.77 safe 0.20 safe 0.41
minepump_spec1_product03_safe.cil.c safe 0.10 safe 1.9  safe 1.4  safe 0.35 safe 0.85 safe 0.21 safe 0.42
minepump_spec1_product04_safe.cil.c safe 0.10 safe 1.9  safe 1.4  safe 0.36 safe 0.83 safe 0.20 safe 0.40
minepump_spec1_product05_safe.cil.c safe 0.09 safe 1.7  safe 1.3  safe 0.36 safe 0.89 safe 0.20 safe 0.41
minepump_spec1_product06_safe.cil.c safe 0.10 safe 1.6  safe 1.4  safe 0.35 safe 0.87 safe 0.20 safe 0.42
minepump_spec1_product07_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.38 safe 1.1  safe 0.21 safe 0.42
minepump_spec1_product08_safe.cil.c safe 0.09 safe 1.7  safe 1.5  safe 0.38 safe 1.1  safe 0.20 safe 0.41
minepump_spec1_product09_safe.cil.c safe 0.09 safe 1.9  safe 1.3  safe 0.38 safe 0.67 safe 0.19 safe 0.41
minepump_spec1_product10_safe.cil.c safe 0.09 safe 1.9  safe 1.3  safe 0.35 safe 0.76 safe 0.20 safe 0.41
minepump_spec1_product11_safe.cil.c safe 0.10 safe 1.9  safe 1.5  safe 0.38 safe 0.84 safe 0.20 safe 0.41
minepump_spec1_product12_safe.cil.c safe 0.10 safe 2.0  safe 1.5  safe 0.39 safe 0.86 safe 0.20 safe 0.41
minepump_spec1_product13_safe.cil.c safe 0.09 safe 1.7  safe 1.3  safe 0.37 safe 0.83 safe 0.21 safe 0.41
minepump_spec1_product14_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.40 safe 0.90 safe 0.20 safe 0.42
minepump_spec1_product15_safe.cil.c safe 0.09 safe 1.7  safe 1.5  safe 0.36 safe 1.1  safe 0.20 safe 0.42
minepump_spec1_product16_safe.cil.c safe 0.09 safe 1.7  safe 1.5  safe 0.40 safe 1.1  safe 0.21 safe 0.40
minepump_spec1_product17_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.38 safe 0.83 safe 0.20 safe 0.40
minepump_spec1_product18_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.38 safe 0.91 safe 0.21 safe 0.39
minepump_spec1_product19_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.40 safe 1.1  safe 0.20 safe 0.42
minepump_spec1_product20_safe.cil.c safe 0.09 safe 1.7  safe 1.5  safe 0.39 safe 1.1  safe 0.20 safe 0.41
minepump_spec1_product21_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.36 safe 1.0  safe 0.20 safe 0.42
minepump_spec1_product22_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.36 safe 1.1  safe 0.20 safe 0.44
minepump_spec1_product23_safe.cil.c safe 0.10 safe 1.8  safe 1.5  safe 0.38 safe 1.2  safe 0.20 safe 0.41
minepump_spec1_product24_safe.cil.c safe 0.10 safe 1.8  safe 1.5  safe 0.38 safe 1.3  safe 0.20 safe 0.40
minepump_spec1_product25_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.37 safe 0.92 safe 0.20 safe 0.38
minepump_spec1_product26_safe.cil.c safe 0.09 safe 1.9  safe 1.4  safe 0.38 safe 0.97 safe 0.20 safe 0.44
minepump_spec1_product27_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.39 safe 1.1  safe 0.20 safe 0.42
minepump_spec1_product28_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.38 safe 1.1  safe 0.20 safe 0.41
minepump_spec1_product29_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.39 safe 1.1  safe 0.21 safe 0.42
minepump_spec1_product30_safe.cil.c safe 0.09 safe 1.8  safe 1.4  safe 0.37 safe 1.1  safe 0.20 safe 0.41
minepump_spec1_product31_safe.cil.c safe 0.10 safe 1.8  safe 1.5  safe 0.45 safe 1.3  safe 0.20 safe 0.40
minepump_spec1_product32_safe.cil.c safe 0.10 safe 1.8  safe 1.5  safe 0.70 safe 1.3  safe 0.21 safe 0.42
minepump_spec1_product45_safe.cil.c safe 1.7  safe 3.5  safe 1.6  safe 0.44 safe 1.4  safe 0.22 safe 0.61
minepump_spec1_product46_safe.cil.c safe 1.7  safe 3.4  safe 1.7  safe 0.43 safe 1.5  safe 0.21 safe 0.67
minepump_spec1_product47_safe.cil.c safe 51    safe 3.4  safe 1.8  safe 0.45 safe 2.1  safe 0.23 safe 1.5 
minepump_spec1_product48_safe.cil.c safe 56    safe 3.7  safe 1.8  safe 0.42 safe 2.1  safe 0.24 safe 1.3 
minepump_spec1_product57_safe.cil.c safe 7.7  safe 3.8  safe 1.5  safe 0.51 safe 1.8  safe 0.22 safe 1.1 
minepump_spec1_product58_safe.cil.c safe 7.8  safe 4.1  safe 1.5  safe 0.47 safe 1.9  safe 0.22 safe 1.1 
minepump_spec1_product59_safe.cil.c safe 51    safe 4.1  safe 1.6  safe 0.48 safe 2.3  safe 0.22 safe 1.8 
minepump_spec1_product60_safe.cil.c safe 88    safe 4.3  safe 1.5  safe 0.48 safe 2.3  safe 0.22 safe 1.8 
minepump_spec1_product61_safe.cil.c safe 1.8  safe 3.8  safe 1.5  safe 0.51 safe 2.1  safe 0.21 safe 0.68
minepump_spec1_product62_safe.cil.c safe 1.8  safe 3.5  safe 1.5  safe 0.49 safe 2.1  safe 0.22 safe 0.61
minepump_spec1_product63_safe.cil.c safe 39    safe 3.8  safe 1.6  safe 0.51 safe 2.8  safe 0.22 safe 1.5 
minepump_spec1_product64_safe.cil.c safe 63    safe 3.7  safe 1.6  safe 0.52 safe 2.8  safe 0.23 safe 1.5 
minepump_spec2_product01_safe.cil.c safe 0.08 safe 2.2  safe 1.3  safe 0.38 safe 0.79 safe 0.20 safe 0.40
minepump_spec2_product02_safe.cil.c safe 0.09 safe 2.3  safe 1.4  safe 0.37 safe 0.87 safe 0.21 safe 0.40
minepump_spec2_product03_safe.cil.c safe 0.09 safe 1.9  safe 1.5  safe 0.37 safe 0.95 safe 0.22 safe 0.42
minepump_spec2_product04_safe.cil.c safe 0.10 safe 2.4  safe 1.5  safe 0.37 safe 0.92 safe 0.22 safe 0.36
minepump_spec2_product05_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.37 safe 0.99 safe 0.20 safe 0.42
minepump_spec2_product06_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.37 safe 1.0  safe 0.20 safe 0.42
minepump_spec2_product07_safe.cil.c safe 0.09 safe 1.7  safe 1.5  safe 0.39 safe 1.2  safe 0.20 safe 0.40
minepump_spec2_product08_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.38 safe 1.2  safe 0.22 safe 0.41
minepump_spec2_product09_safe.cil.c safe 0.09 safe 2.2  safe 1.3  safe 0.38 safe 0.77 safe 0.21 safe 0.41
minepump_spec2_product10_safe.cil.c safe 0.09 safe 2.4  safe 1.4  safe 0.36 safe 0.88 safe 0.20 safe 0.41
minepump_spec2_product11_safe.cil.c safe 0.09 safe 2.0  safe 1.4  safe 0.37 safe 0.89 safe 0.20 safe 0.42
minepump_spec2_product12_safe.cil.c safe 0.10 safe 2.4  safe 1.4  safe 0.37 safe 0.99 safe 0.20 safe 0.39
minepump_spec2_product13_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.35 safe 0.95 safe 0.20 safe 0.41
minepump_spec2_product14_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.37 safe 1.0  safe 0.20 safe 0.40
minepump_spec2_product15_safe.cil.c safe 0.10 safe 1.7  safe 1.6  safe 0.40 safe 1.2  safe 0.21 safe 0.42
minepump_spec2_product16_safe.cil.c safe 0.09 safe 1.8  safe 1.4  safe 0.39 safe 1.2  safe 0.21 safe 0.40
minepump_spec2_product17_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.38 safe 1.0  safe 0.21 safe 0.42
minepump_spec2_product18_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.39 safe 1.1  safe 0.20 safe 0.39
minepump_spec2_product19_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.36 safe 1.2  safe 0.21 safe 0.42
minepump_spec2_product20_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.37 safe 1.2  safe 0.22 safe 0.40
minepump_spec2_product21_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.41 safe 1.1  safe 0.20 safe 0.40
minepump_spec2_product22_safe.cil.c safe 0.10 safe 1.8  safe 1.4  safe 0.38 safe 1.2  safe 0.21 safe 0.40
minepump_spec2_product23_safe.cil.c safe 0.10 safe 1.8  safe 1.5  safe 0.37 safe 1.4  safe 0.21 safe 0.40
minepump_spec2_product24_safe.cil.c safe 0.10 safe 1.9  safe 1.5  safe 0.40 safe 1.4  safe 0.21 safe 0.45
minepump_spec2_product25_safe.cil.c safe 0.10 safe 1.9  safe 1.4  safe 0.36 safe 1.0  safe 0.20 safe 0.41
minepump_spec2_product26_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.38 safe 1.1  safe 0.22 safe 0.39
minepump_spec2_product27_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.37 safe 1.2  safe 0.22 safe 0.41
minepump_spec2_product28_safe.cil.c safe 0.09 safe 1.7  safe 1.5  safe 0.42 safe 1.3  safe 0.21 safe 0.39
minepump_spec2_product29_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.39 safe 1.2  safe 0.21 safe 0.42
minepump_spec2_product30_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.39 safe 1.2  safe 0.20 safe 0.40
minepump_spec2_product31_safe.cil.c safe 0.11 safe 1.8  safe 1.6  safe 0.40 safe 1.4  safe 0.21 safe 0.42
minepump_spec2_product32_safe.cil.c safe 0.09 safe 1.8  safe 1.5  safe 0.37 safe 1.5  safe 0.21 safe 0.34
minepump_spec2_product37_safe.cil.c safe 22    safe 4.0  safe 1.6  safe 0.43 safe 1.5  safe 0.23 safe 1.1 
minepump_spec2_product38_safe.cil.c safe 24    safe 3.9  safe 1.7  safe 0.42 safe 1.5  safe 0.23 safe 1.2 
minepump_spec2_product39_safe.cil.c safe 95    safe 3.5  safe 1.9  safe 0.42 safe 2.1  safe 0.25 safe 1.8 
minepump_spec2_product40_safe.cil.c safe 120    safe 3.6  safe 1.8  safe 0.43 safe 2.2  safe 0.24 safe 1.8 
minepump_spec2_product45_safe.cil.c safe 4.6  safe 4.2  safe 1.6  safe 0.42 safe 1.5  safe 0.21 safe 1.3 
minepump_spec2_product46_safe.cil.c safe 4.7  safe 3.6  safe 1.6  safe 0.44 safe 1.5  safe 0.22 safe 0.55
minepump_spec2_product47_safe.cil.c safe 75    safe 3.4  safe 1.8  safe 0.45 safe 2.1  safe 0.23 safe 2.2 
minepump_spec2_product48_safe.cil.c safe 90    safe 3.6  safe 1.8  safe 0.44 safe 2.2  safe 0.24 safe 2.2 
minepump_spec2_product49_safe.cil.c safe 60    safe 4.1  safe 1.5  safe 0.46 safe 1.8  safe 0.22 safe 2.3 
minepump_spec2_product50_safe.cil.c safe 65    safe 4.1  safe 1.5  safe 0.47 safe 1.8  safe 0.21 safe 2.2 
minepump_spec2_product51_safe.cil.c safe 89    safe 4.2  safe 1.6  safe 0.47 safe 2.2  safe 0.23 safe 2.9 
minepump_spec2_product52_safe.cil.c safe 180    safe 4.4  safe 1.7  safe 0.48 safe 2.2  safe 0.23 safe 2.3 
minepump_spec2_product53_safe.cil.c safe 56    safe 3.9  safe 1.6  safe 0.49 safe 1.9  safe 0.21 safe 1.1 
minepump_spec2_product54_safe.cil.c safe 59    safe 3.9  safe 1.5  safe 0.47 safe 1.9  safe 0.21 safe 1.2 
minepump_spec2_product55_safe.cil.c safe 110    safe 3.8  safe 1.6  safe 0.47 safe 2.7  safe 0.23 safe 2.5 
minepump_spec2_product56_safe.cil.c safe 120    safe 3.9  safe 1.7  safe 0.49 safe 2.6  safe 0.23 safe 2.5 
minepump_spec2_product57_safe.cil.c safe 38    safe 4.5  safe 1.5  safe 0.47 safe 2.0  safe 0.22 safe 1.9 
minepump_spec2_product58_safe.cil.c safe 58    safe 4.5  safe 1.5  safe 0.47 safe 2.0  safe 0.23 safe 2.0 
minepump_spec2_product59_safe.cil.c safe 49    safe 4.9  safe 1.6  safe 0.45 safe 2.2  safe 0.23 safe 2.4 
minepump_spec2_product60_safe.cil.c safe 130    safe 4.8  safe 1.6  safe 0.46 safe 2.3  safe 0.23 safe 2.3 
minepump_spec2_product61_safe.cil.c safe 4.7  safe 4.0  safe 1.5  safe 0.49 safe 2.1  safe 0.21 safe 0.72
minepump_spec2_product62_safe.cil.c safe 4.8  safe 3.6  safe 1.5  safe 0.50 safe 2.2  safe 0.22 safe 0.69
minepump_spec2_product63_safe.cil.c safe 49    safe 3.7  safe 1.7  safe 0.50 safe 2.9  safe 0.23 safe 2.4 
minepump_spec2_product64_safe.cil.c safe 94    safe 3.9  safe 1.6  safe 0.50 safe 3.0  safe 0.22 safe 2.3 
minepump_spec3_product33_safe.cil.c safe 6.0  safe 3.5  safe 1.6  safe 0.40 safe 1.4  safe 0.21 safe 0.65
minepump_spec3_product34_safe.cil.c safe 6.1  safe 3.6  safe 1.6  safe 0.39 safe 1.4  safe 0.22 safe 0.68
minepump_spec3_product37_safe.cil.c safe 68    safe 3.9  safe 1.6  safe 0.42 safe 1.6  safe 0.23 safe 0.68
minepump_spec3_product38_safe.cil.c safe 68    safe 3.9  safe 1.7  safe 0.40 safe 1.7  safe 0.21 safe 0.68
minepump_spec3_product41_safe.cil.c safe 36    safe 3.6  safe 1.5  safe 0.40 safe 1.5  safe 0.21 safe 0.60
minepump_spec3_product42_safe.cil.c safe 30    safe 3.9  safe 1.5  safe 0.42 safe 1.5  safe 0.22 safe 0.63
minepump_spec3_product45_safe.cil.c safe 120    safe 3.8  safe 1.6  safe 0.43 safe 1.8  safe 0.21 safe 0.68
minepump_spec3_product46_safe.cil.c safe 71    safe 4.2  safe 1.6  safe 0.44 safe 1.8  safe 0.22 safe 0.69
minepump_spec3_product49_safe.cil.c safe 56    safe 4.4  safe 1.5  safe 0.48 safe 1.8  safe 0.21 safe 2.2 
minepump_spec3_product50_safe.cil.c safe 56    safe 3.7  safe 1.5  safe 0.46 safe 1.8  safe 0.22 safe 1.7 
minepump_spec3_product53_safe.cil.c error 64    safe 4.4  safe 1.5  safe 0.53 safe 2.3  safe 0.21 safe 2.0 
minepump_spec3_product54_safe.cil.c safe 320    safe 4.5  safe 1.6  safe 0.76 safe 2.3  safe 0.21 safe 1.5 
minepump_spec3_product57_safe.cil.c error 34    safe 4.0  safe 1.5  safe 0.58 safe 2.0  safe 0.21 safe 2.1 
minepump_spec3_product58_safe.cil.c error 36    safe 4.1  safe 1.5  safe 0.59 safe 2.0  safe 0.21 safe 1.9 
minepump_spec3_product61_safe.cil.c safe 190    safe 4.8  safe 1.5  safe 0.59 safe 2.7  safe 0.21 safe 2.7 
minepump_spec3_product62_safe.cil.c error 34    safe 4.7  safe 1.5  safe 0.60 safe 2.6  safe 0.21 safe 1.9 
minepump_spec4_product01_safe.cil.c safe 0.09 safe 2.0  safe 1.3  safe 0.35 safe 0.75 safe 0.20 safe 0.40
minepump_spec4_product02_safe.cil.c safe 0.09 safe 2.0  safe 1.3  safe 0.39 safe 0.79 safe 0.20 safe 0.40
minepump_spec4_product03_safe.cil.c safe 0.09 safe 1.9  safe 1.4  safe 0.36 safe 0.80 safe 0.21 safe 0.42
minepump_spec4_product04_safe.cil.c safe 0.10 safe 1.8  safe 1.4  safe 0.39 safe 0.90 safe 0.20 safe 0.42
minepump_spec4_product05_safe.cil.c safe 0.09 safe 1.6  safe 1.4  safe 0.36 safe 0.89 safe 0.20 safe 0.42
minepump_spec4_product06_safe.cil.c safe 0.10 safe 1.6  safe 1.4  safe 0.39 safe 0.96 safe 0.20 safe 0.41
minepump_spec4_product07_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.34 safe 1.1  safe 0.20 safe 0.40
minepump_spec4_product08_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.39 safe 1.1  safe 0.21 safe 0.42
minepump_spec4_product09_safe.cil.c safe 0.09 safe 1.7  safe 1.3  safe 0.37 safe 0.70 safe 0.19 safe 0.40
minepump_spec4_product10_safe.cil.c safe 0.09 safe 2.1  safe 1.3  safe 0.37 safe 0.72 safe 0.20 safe 0.40
minepump_spec4_product11_safe.cil.c safe 0.10 safe 1.9  safe 1.4  safe 0.37 safe 0.85 safe 0.20 safe 0.41
minepump_spec4_product12_safe.cil.c safe 0.10 safe 1.8  safe 1.4  safe 0.33 safe 0.90 safe 0.20 safe 0.40
minepump_spec4_product13_safe.cil.c safe 0.09 safe 1.6  safe 1.3  safe 0.36 safe 0.90 safe 0.20 safe 0.41
minepump_spec4_product14_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.38 safe 0.96 safe 0.20 safe 0.42
minepump_spec4_product15_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.38 safe 1.1  safe 0.21 safe 0.41
minepump_spec4_product16_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.39 safe 1.1  safe 0.20 safe 0.44
minepump_spec4_product17_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.38 safe 0.93 safe 0.20 safe 0.40
minepump_spec4_product18_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.36 safe 0.99 safe 0.20 safe 0.41
minepump_spec4_product19_safe.cil.c safe 0.09 safe 1.7  safe 1.5  safe 0.40 safe 1.0  safe 0.21 safe 0.42
minepump_spec4_product20_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.36 safe 1.1  safe 0.20 safe 0.41
minepump_spec4_product21_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.37 safe 1.1  safe 0.20 safe 0.41
minepump_spec4_product22_safe.cil.c safe 0.09 safe 1.8  safe 1.4  safe 0.39 safe 1.2  safe 0.20 safe 0.44
minepump_spec4_product23_safe.cil.c safe 0.10 safe 1.8  safe 1.5  safe 0.35 safe 1.2  safe 0.21 safe 0.41
minepump_spec4_product24_safe.cil.c safe 0.09 safe 1.8  safe 1.5  safe 0.38 safe 1.3  safe 0.21 safe 0.42
minepump_spec4_product25_safe.cil.c safe 0.09 safe 1.7  safe 1.3  safe 0.38 safe 0.93 safe 0.20 safe 0.42
minepump_spec4_product26_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.38 safe 0.98 safe 0.20 safe 0.41
minepump_spec4_product27_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.37 safe 1.1  safe 0.21 safe 0.41
minepump_spec4_product28_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.39 safe 1.1  safe 0.21 safe 0.41
minepump_spec4_product29_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.37 safe 1.1  safe 0.20 safe 0.42
minepump_spec4_product30_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.36 safe 1.2  safe 0.20 safe 0.40
minepump_spec4_product31_safe.cil.c safe 0.10 safe 1.8  safe 1.5  safe 0.38 safe 1.2  safe 0.19 safe 0.42
minepump_spec4_product32_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.39 safe 1.3  safe 0.21 safe 0.40
minepump_spec4_product49_safe.cil.c safe 35    safe 3.8  safe 1.5  safe 0.47 safe 1.7  safe 0.21 safe 1.1 
minepump_spec4_product50_safe.cil.c safe 27    safe 3.8  safe 1.6  safe 0.44 safe 1.7  safe 0.21 safe 1.00
minepump_spec4_product51_safe.cil.c safe 21    safe 3.9  safe 1.6  safe 0.45 safe 2.0  safe 0.21 safe 1.4 
minepump_spec4_product52_safe.cil.c safe 25    safe 4.0  safe 1.5  safe 0.46 safe 2.1  safe 0.22 safe 1.5 
minepump_spec4_product53_safe.cil.c safe 130    safe 4.2  safe 1.5  safe 0.49 safe 2.2  safe 0.21 safe 1.1 
minepump_spec4_product54_safe.cil.c safe 47    safe 4.3  safe 1.5  safe 0.49 safe 2.2  safe 0.21 safe 1.2 
minepump_spec4_product55_safe.cil.c safe 19    safe 4.6  safe 1.6  safe 0.49 safe 2.5  safe 0.22 safe 1.9 
minepump_spec4_product56_safe.cil.c safe 25    safe 4.6  safe 1.5  safe 0.52 safe 2.6  safe 0.22 safe 1.7 
minepump_spec4_product57_safe.cil.c safe 59    safe 4.1  safe 1.4  safe 0.45 safe 1.9  safe 0.21 safe 1.0 
minepump_spec4_product58_safe.cil.c safe 31    safe 3.8  safe 1.5  safe 0.47 safe 1.9  safe 0.20 safe 1.0 
minepump_spec4_product59_safe.cil.c safe 37    safe 3.9  safe 1.5  safe 0.47 safe 2.2  safe 0.21 safe 1.7 
minepump_spec4_product60_safe.cil.c safe 57    safe 4.1  safe 1.6  safe 0.47 safe 2.1  safe 0.22 safe 2.0 
minepump_spec4_product61_safe.cil.c safe 64    safe 4.5  safe 1.4  safe 0.53 safe 2.5  safe 0.21 safe 1.1 
minepump_spec4_product62_safe.cil.c safe 71    safe 4.4  safe 1.5  safe 0.53 safe 2.5  safe 0.21 safe 1.1 
minepump_spec4_product63_safe.cil.c safe 38    safe 4.8  safe 1.5  safe 0.54 safe 2.7  safe 0.21 safe 1.8 
minepump_spec4_product64_safe.cil.c safe 180    safe 5.1  safe 1.6  safe 0.55 safe 2.8  safe 0.22 safe 1.5 
minepump_spec5_product01_safe.cil.c safe 0.08 safe 1.8  safe 1.3  safe 0.35 safe 0.80 safe 0.20 safe 0.41
minepump_spec5_product02_safe.cil.c safe 0.10 safe 1.8  safe 1.4  safe 0.39 safe 0.81 safe 0.20 safe 0.42
minepump_spec5_product03_safe.cil.c safe 0.09 safe 2.0  safe 1.5  safe 0.37 safe 0.85 safe 0.21 safe 0.41
minepump_spec5_product04_safe.cil.c safe 0.10 safe 2.1  safe 1.5  safe 0.36 safe 0.90 safe 0.22 safe 0.42
minepump_spec5_product05_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.37 safe 0.92 safe 0.20 safe 0.42
minepump_spec5_product06_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.38 safe 1.0  safe 0.20 safe 0.41
minepump_spec5_product07_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.37 safe 1.2  safe 0.20 safe 0.42
minepump_spec5_product08_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.37 safe 1.1  safe 0.22 safe 0.40
minepump_spec5_product09_safe.cil.c safe 0.09 safe 1.9  safe 1.4  safe 0.38 safe 0.82 safe 0.20 safe 0.36
minepump_spec5_product10_safe.cil.c safe 0.09 safe 1.8  safe 1.4  safe 0.36 safe 0.85 safe 0.20 safe 0.41
minepump_spec5_product11_safe.cil.c safe 0.10 safe 2.0  safe 1.5  safe 0.37 safe 0.93 safe 0.21 safe 0.39
minepump_spec5_product12_safe.cil.c safe 0.09 safe 2.1  safe 1.5  safe 0.40 safe 0.95 safe 0.22 safe 0.41
minepump_spec5_product13_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.37 safe 0.90 safe 0.20 safe 0.42
minepump_spec5_product14_safe.cil.c safe 0.10 safe 1.8  safe 1.4  safe 0.37 safe 0.93 safe 0.20 safe 0.42
minepump_spec5_product15_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.37 safe 1.1  safe 0.22 safe 0.41
minepump_spec5_product16_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.38 safe 1.1  safe 0.22 safe 0.41
minepump_spec5_product17_safe.cil.c safe 0.10 safe 1.7  safe 1.4  safe 0.37 safe 0.93 safe 0.20 safe 0.40
minepump_spec5_product18_safe.cil.c safe 0.10 safe 1.8  safe 1.4  safe 0.39 safe 0.98 safe 0.20 safe 0.42
minepump_spec5_product19_safe.cil.c safe 0.10 safe 1.9  safe 1.5  safe 0.38 safe 1.2  safe 0.22 safe 0.43
minepump_spec5_product20_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.39 safe 1.1  safe 0.22 safe 0.40
minepump_spec5_product21_safe.cil.c safe 0.10 safe 1.8  safe 1.4  safe 0.38 safe 1.2  safe 0.20 safe 0.42
minepump_spec5_product22_safe.cil.c safe 0.10 safe 1.8  safe 1.4  safe 0.38 safe 1.2  safe 0.20 safe 0.41
minepump_spec5_product23_safe.cil.c safe 0.10 safe 1.8  safe 1.6  safe 0.37 safe 1.3  safe 0.21 safe 0.40
minepump_spec5_product24_safe.cil.c safe 0.10 safe 1.8  safe 1.5  safe 0.38 safe 1.4  safe 0.22 safe 0.42
minepump_spec5_product25_safe.cil.c safe 0.09 safe 1.7  safe 1.4  safe 0.38 safe 0.99 safe 0.20 safe 0.42
minepump_spec5_product26_safe.cil.c safe 0.10 safe 1.8  safe 1.4  safe 0.38 safe 1.0  safe 0.20 safe 0.40
minepump_spec5_product27_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.38 safe 1.1  safe 0.21 safe 0.42
minepump_spec5_product28_safe.cil.c safe 0.10 safe 1.7  safe 1.5  safe 0.37 safe 1.2  safe 0.21 safe 0.45
minepump_spec5_product29_safe.cil.c safe 0.10 safe 1.8  safe 1.4  safe 0.38 safe 1.2  safe 0.20 safe 0.46
minepump_spec5_product30_safe.cil.c safe 0.09 safe 1.8  safe 1.4  safe 0.39 safe 1.2  safe 0.20 safe 0.41
minepump_spec5_product31_safe.cil.c safe 0.10 safe 1.8  safe 1.5  safe 0.37 safe 1.4  safe 0.21 safe 0.45
minepump_spec5_product32_safe.cil.c safe 0.09 safe 1.8  safe 1.5  safe 0.42 safe 1.4  safe 0.22 safe 0.42
minepump_spec5_product33_safe.cil.c safe 53    safe 4.1  safe 1.7  safe 0.91 safe 1.4  safe 0.23 safe 1.0 
minepump_spec5_product34_safe.cil.c safe 26    safe 3.9  safe 1.6  safe 0.42 safe 1.5  safe 0.23 safe 0.98
minepump_spec5_product35_safe.cil.c safe 81    safe 4.1  safe 1.8  safe 0.41 safe 1.7  safe 0.25 safe 1.3 
minepump_spec5_product36_safe.cil.c error 120    safe 4.2  safe 1.8  safe 0.41 safe 1.8  safe 0.27 safe 1.8 
minepump_spec5_product37_safe.cil.c safe 150    safe 4.4  safe 1.8  safe 0.42 safe 1.8  safe 0.23 safe 3.3 
minepump_spec5_product38_safe.cil.c safe 200    safe 4.4  safe 1.8  safe 0.45 safe 1.8  safe 0.24 safe 2.6 
minepump_spec5_product39_safe.cil.c safe 96    safe 4.5  safe 2.0  safe 0.42 safe 2.1  safe 0.26 safe 6.4 
minepump_spec5_product40_safe.cil.c error 170    safe 4.3  safe 1.9  safe 0.42 safe 2.2  safe 0.27 safe 2.0 
minepump_spec5_product41_safe.cil.c safe 110    safe 3.6  safe 1.6  safe 0.41 safe 1.7  safe 0.22 safe 0.70
minepump_spec5_product42_safe.cil.c safe 51    safe 4.2  safe 1.7  safe 0.41 safe 1.6  safe 0.22 safe 1.2 
minepump_spec5_product43_safe.cil.c safe 260    safe 4.4  safe 1.8  safe 0.42 safe 1.8  safe 0.24 safe 1.4 
minepump_spec5_product44_safe.cil.c error 320    safe 4.0  safe 1.8  safe 0.44 safe 1.9  safe 0.25 safe 1.9 
minepump_spec5_product45_safe.cil.c safe 290    safe 4.2  safe 1.8  safe 0.42 safe 2.0  safe 0.23 safe 1.3 
minepump_spec5_product46_safe.cil.c safe 230    safe 4.6  safe 1.8  safe 0.45 safe 2.0  safe 0.24 safe 1.4 
minepump_spec5_product47_safe.cil.c safe 360    safe 4.9  safe 2.0  safe 0.46 safe 2.2  safe 0.26 safe 1.7 
minepump_spec5_product48_safe.cil.c error 400    safe 4.6  safe 1.9  safe 0.45 safe 2.2  safe 0.27 safe 1.4 
minepump_spec5_product49_safe.cil.c safe 16    safe 4.3  safe 1.5  safe 0.48 safe 1.8  safe 0.22 safe 2.1 
minepump_spec5_product50_safe.cil.c safe 24    safe 4.1  safe 1.6  safe 0.47 safe 1.8  safe 0.23 safe 2.1 
minepump_spec5_product51_safe.cil.c safe 98    safe 4.5  safe 1.7  safe 0.47 safe 2.1  safe 0.24 safe 2.6 
minepump_spec5_product52_safe.cil.c safe 130    safe 4.3  safe 1.6  safe 0.47 safe 2.1  safe 0.24 safe 2.8 
minepump_spec5_product53_safe.cil.c safe 34    safe 4.4  safe 1.6  safe 0.51 safe 2.3  safe 0.22 safe 2.0 
minepump_spec5_product54_safe.cil.c safe 76    safe 4.3  safe 1.6  safe 0.54 safe 2.4  safe 0.22 safe 2.1 
minepump_spec5_product55_safe.cil.c safe 190    safe 4.4  safe 1.7  safe 0.55 safe 2.6  safe 0.23 safe 4.0 
minepump_spec5_product56_safe.cil.c safe 440    safe 4.4  safe 1.6  safe 0.58 safe 2.8  safe 0.24 safe 2.0 
minepump_spec5_product57_safe.cil.c safe 18    safe 4.2  safe 1.6  safe 0.49 safe 2.0  safe 0.22 safe 1.3 
minepump_spec5_product58_safe.cil.c safe 18    safe 4.2  safe 1.6  safe 0.47 safe 2.0  safe 0.22 safe 1.4 
minepump_spec5_product59_safe.cil.c safe 290    safe 4.7  safe 1.7  safe 0.52 safe 2.3  safe 0.23 safe 2.1 
minepump_spec5_product60_safe.cil.c error 380    safe 4.5  safe 1.7  safe 0.53 safe 2.3  safe 0.24 safe 1.5 
minepump_spec5_product61_safe.cil.c safe 19    safe 4.8  safe 1.5  safe 0.54 safe 2.6  safe 0.22 safe 1.4 
minepump_spec5_product62_safe.cil.c safe 19    safe 5.0  safe 1.6  safe 0.58 safe 2.6  safe 0.22 safe 1.5 
minepump_spec5_product63_safe.cil.c safe 460    safe 5.3  safe 1.7  safe 0.60 safe 3.0  safe 0.23 safe 1.7 
minepump_spec5_product64_safe.cil.c error 740    safe 5.4  safe 1.7  safe 0.61 safe 3.0  safe 0.24 safe 2.0 
minepump_spec5_productSimulator_safe.cil.c timeout 910    safe 7.3  safe 2.4  safe 0.79 safe 7.1  timeout 900    safe 3.6 
total files 597 150000 597 200000 597 10000 597 6500 597 5400 597 9300 597 5000
correct results 400 16000 386 7300 583 3100 591 1200 595 3600 585 7500 597 5000
false negatives 0 0 0 0 0 0 1 780 0 0 0 0 0 0
false positives 2 150 0 0 0 0 0 0 0 0 10 30 0 0
false properties 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (597 files, max score: 929) 652 655 915 914 926 865 929