Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
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 CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 16:01:31 CET 2017-12-01 08:31:47 CET 2017-12-01 08:56:50 CET 2017-12-01 08:59:39 CET 2017-12-01 09:01:39 CET 2017-12-01 08:10:33 CET 2017-12-01 08:38:18 CET
Run set depthk.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/product-lines/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
elevator_spec14_product20_false-unreach-call_true-termination.cil.c 1 480    380 4200   -32 5.9  280 -32 8.5   360   0 6.0  270 1 .94   20    - -
elevator_spec14_product24_false-unreach-call_true-termination.cil.c 1 480    520 4200   -32 6.0  270 -32 5.6   370   0 5.8  280 1 1.0    20    - -
elevator_spec14_product28_false-unreach-call_true-termination.cil.c 1 480    420 5600   -32 5.9  270 -32 5.7   380   0 5.5  270 1 .96   20    - -
elevator_spec14_product32_false-unreach-call_true-termination.cil.c 1 6.3  540 64   -32 6.2  270 -32 8.5   380   0 5.7  270 1 1.0    20    - -
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c 1 530    1400 5600   -32 31    1200 -32 9.0   410   0 5.8  280 1 1.0    20    - -
elevator_spec1_product18_false-unreach-call_true-termination.cil.c 1 490    180 6300   -32 6.4  270 -32 8.5   390   0 5.5  280 1 .99   20    - -
elevator_spec1_product20_false-unreach-call_true-termination.cil.c 1 490    200 6900   -32 6.5  290 -32 8.8   390   0 5.9  280 1 1.0    20    - -
elevator_spec1_product22_false-unreach-call_true-termination.cil.c 1 500    240 6800   -32 6.1  260 -32 8.1   390   0 5.7  280 1 1.0    20    - -
elevator_spec1_product24_false-unreach-call_true-termination.cil.c 1 500    330 5800   -32 4.2  270 -32 5.7   410   0 5.9  290 1 1.1    20    - -
elevator_spec1_product26_false-unreach-call_true-termination.cil.c 1 490    210 6000   -32 6.0  270 -32 8.6   380   0 5.5  270 1 1.0    20    - -
elevator_spec1_product28_false-unreach-call_true-termination.cil.c 1 490    210 7200   -32 6.4  270 -32 8.5   380   0 5.9  290 1 1.0    20    - -
elevator_spec1_product30_false-unreach-call_true-termination.cil.c 1 500    320 6000   -32 6.4  270 -32 9.2   390   0 5.7  270 1 1.1    20    - -
elevator_spec1_product32_false-unreach-call_true-termination.cil.c 1 500    340 5500   -32 6.4  280 -32 8.6   390   0 5.9  280 1 1.1    20    - -
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c 1 700    790 9100   -32 36    1600 -32 8.8   430   0 6.1  290 1 1.1    20    - -
elevator_spec2_product18_false-unreach-call_true-termination.cil.c 1 490    190 5100   -32 5.9  270 -32 8.3   380   0 5.8  270 1 1.0    20    - -
elevator_spec2_product20_false-unreach-call_true-termination.cil.c 1 490    200 5800   -32 6.0  270 -32 8.4   370   0 5.6  280 1 1.0    19    - -
elevator_spec2_product22_false-unreach-call_true-termination.cil.c 1 500    240 5700   -32 6.4  290 -32 9.8   420   0 5.6  270 1 1.0    20    - -
elevator_spec2_product24_false-unreach-call_true-termination.cil.c 1 500    330 5800   -32 6.6  300 -32 8.6   390   0 5.6  280 1 1.0    20    - -
elevator_spec2_product26_false-unreach-call_true-termination.cil.c 1 490    200 5800   -32 6.1  270 -32 8.9   370   0 5.5  270 1 1.0    20    - -
elevator_spec2_product28_false-unreach-call_true-termination.cil.c 1 490    220 6100   -32 6.2  270 -32 6.0   400   0 5.4  270 1 1.0    19    - -
elevator_spec2_product30_false-unreach-call_true-termination.cil.c 1 500    320 6000   -32 4.1  270 -32 8.6   380   0 5.5  280 1 1.0    20    - -
elevator_spec2_product32_false-unreach-call_true-termination.cil.c 1 500    340 5900   -32 6.9  280 -32 8.8   390   0 5.7  270 1 1.0    20    - -
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c 1 700    730 8800   -32 32    1100 -32 9.7   420   0 6.1  280 1 1.1    20    - -
elevator_spec3_product03_false-unreach-call_true-termination.cil.c 1 480    250 5100   -32 7.8  290 -32 8.8   420   0 6.4  290 1 1.0    20    - -
elevator_spec3_product11_false-unreach-call_true-termination.cil.c 1 480    270 5500   -32 6.8  280 -32 8.5   400   0 6.5  290 1 1.0    20    - -
elevator_spec3_product19_false-unreach-call_true-termination.cil.c 1 480    420 5500   -32 7.1  310 -32 9.4   420   0 6.5  290 1 1.1    21    - -
elevator_spec3_product20_false-unreach-call_true-termination.cil.c 1 480    390 6100   -32 7.0  280 -32 9.6   420   0 6.1  290 1 1.0    21    - -
elevator_spec3_product23_false-unreach-call_true-termination.cil.c 1 480    320 5900   -32 6.8  290 -32 9.2   420   0 6.1  290 1 1.1    20    - -
elevator_spec3_product24_false-unreach-call_true-termination.cil.c 1 480    540 3800   -32 6.9  290 -32 9.0   430   0 6.6  290 1 1.1    21    - -
elevator_spec3_product27_false-unreach-call_true-termination.cil.c 1 480    430 5200   -32 7.3  290 -32 9.5   420   0 6.2  290 1 1.1    21    - -
elevator_spec3_product28_false-unreach-call_true-termination.cil.c 1 480    420 5600   -32 6.8  290 -32 9.2   420   0 6.3  290 1 1.0    21    - -
elevator_spec3_product31_false-unreach-call_true-termination.cil.c 1 480    330 5100   -32 6.9  290 -32 8.2   430   0 6.1  290 1 1.1    20    - -
elevator_spec3_product32_false-unreach-call_true-termination.cil.c 1 480    560 4400   -32 7.0  290 -32 8.7   440   0 6.4  300 1 1.1    20    - -
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c 1 610    1400 4500   -32 44    1800 -32 9.7   450   0 6.6  320 1 1.2    21    - -
elevator_spec9_product26_false-unreach-call_true-termination.cil.c 1 490    200 5100   -32 5.8  270 -32 8.7   370   0 3.7  270 1 1.0    20    - -
elevator_spec9_product28_false-unreach-call_true-termination.cil.c 1 490    220 6000   -32 6.6  270 -32 8.3   370   0 6.0  280 1 1.0    20    - -
elevator_spec9_product30_false-unreach-call_true-termination.cil.c 1 500    320 6800   -32 6.2  270 -32 8.7   380   0 5.6  280 1 1.0    20    - -
elevator_spec9_product32_false-unreach-call_true-termination.cil.c 1 500    340 6300   -32 4.2  270 -32 8.6   380   0 6.0  280 1 1.1    20    - -
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c 1 690    730 7500   -32 35    1300 -32 9.3   420   0 6.8  290 1 1.1    20    - -
elevator_spec13_product21_true-unreach-call_false-termination.cil.c 0 890    1500 12000   - - - - 0 .58 43 0 .019 4.9
elevator_spec13_product22_true-unreach-call_false-termination.cil.c 0 900    2100 10000   - - - - 0 .52 44 0 .018 4.9
elevator_spec13_product23_true-unreach-call_false-termination.cil.c 0 890    660 10000   - - - - 0 .53 41 0 .018 4.8
elevator_spec13_product24_true-unreach-call_false-termination.cil.c 0 890    2400 11000   - - - - 0 .53 43 0 .019 4.9
elevator_spec13_product29_true-unreach-call_false-termination.cil.c 0 890    1700 10000   - - - - 0 .54 44 0 .019 4.9
elevator_spec13_product30_true-unreach-call_false-termination.cil.c 0 890    740 11000   - - - - 0 .57 43 0 .019 4.8
elevator_spec13_product31_true-unreach-call_false-termination.cil.c 0 900    660 11000   - - - - 0 .59 41 0 .019 4.9
elevator_spec13_product32_true-unreach-call_false-termination.cil.c 0 900    750 12000   - - - - 0 .55 43 0 .020 4.9
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c 0 900    1400 8500   - - - - 0 .54 43 0 .035 4.8
elevator_spec14_product03_true-unreach-call_true-termination.cil.c 2 540    300 6500   - - - - 2 18    660 0 260     7000  
elevator_spec14_product11_true-unreach-call_true-termination.cil.c 2 550    290 7300   - - - - 2 17    680 0 240     7000  
elevator_spec14_product19_true-unreach-call_true-termination.cil.c 2 550    290 7000   - - - - 2 20    710 0 290     7000  
elevator_spec14_product23_true-unreach-call_true-termination.cil.c 2 660    310 7700   - - - - 2 23    990 0 230     7000  
elevator_spec14_product27_true-unreach-call_true-termination.cil.c 2 550    290 6500   - - - - 2 18    740 0 260     7000  
elevator_spec14_product31_true-unreach-call_true-termination.cil.c 2 660    330 7700   - - - - 2 24    1100 0 180     7000  
elevator_spec1_product01_true-unreach-call_true-termination.cil.c 2 520    290 6900   - - - - 2 64    1400 0 230     7000  
elevator_spec1_product03_true-unreach-call_true-termination.cil.c 2 540    290 6500   - - - - 2 67    1500 0 200     7000  
elevator_spec1_product09_true-unreach-call_true-termination.cil.c 2 540    290 6300   - - - - 2 80    1400 0 300     7000  
elevator_spec1_product11_true-unreach-call_true-termination.cil.c 2 550    290 7300   - - - - 2 81    1600 0 240     7000  
elevator_spec1_product17_true-unreach-call_true-termination.cil.c 2 530    290 6300   - - - - 2 69    1600 0 300     7000  
elevator_spec1_product19_true-unreach-call_true-termination.cil.c 2 550    300 7300   - - - - 2 90    1700 0 280     7000  
elevator_spec1_product21_true-unreach-call_true-termination.cil.c 2 570    290 6800   - - - - 2 130    1900 0 280     7000  
elevator_spec1_product23_true-unreach-call_true-termination.cil.c 2 580    300 7300   - - - - 2 120    2100 0 170     7000  
elevator_spec1_product25_true-unreach-call_true-termination.cil.c 2 550    290 8100   - - - - 2 75    1600 0 160     7000  
elevator_spec1_product27_true-unreach-call_true-termination.cil.c 2 550    300 7600   - - - - 2 94    1800 0 220     7000  
elevator_spec1_product29_true-unreach-call_true-termination.cil.c 2 580    290 7200   - - - - 2 190    1900 0 160     7000  
elevator_spec1_product31_true-unreach-call_true-termination.cil.c 2 590    300 7800   - - - - 2 130    2100 0 200     7000  
elevator_spec2_product01_true-unreach-call_true-termination.cil.c 2 440    280 5700   - - - - 2 25    890 0 130     7000  
elevator_spec2_product03_true-unreach-call_true-termination.cil.c 2 500    280 6200   - - - - 2 35    880 0 150     7000  
elevator_spec2_product09_true-unreach-call_true-termination.cil.c 2 500    280 6700   - - - - 2 32    900 0 140     7000  
elevator_spec2_product11_true-unreach-call_true-termination.cil.c 2 500    280 5900   - - - - 2 33    970 0 150     7000  
elevator_spec2_product17_true-unreach-call_true-termination.cil.c 2 480    270 6400   - - - - 2 32    920 0 140     7000  
elevator_spec2_product19_true-unreach-call_true-termination.cil.c 2 500    290 7000   - - - - 2 34    970 0 150     7000  
elevator_spec2_product21_true-unreach-call_true-termination.cil.c 2 510    280 6800   - - - - 2 45    1100 0 130     7000  
elevator_spec2_product23_true-unreach-call_true-termination.cil.c 2 510    280 6300   - - - - 2 35    1300 0 190     7000  
elevator_spec2_product25_true-unreach-call_true-termination.cil.c 2 500    280 5200   - - - - 2 29    930 0 130     7000  
elevator_spec2_product27_true-unreach-call_true-termination.cil.c 2 510    290 6600   - - - - 2 42    1000 0 160     7000  
elevator_spec2_product29_true-unreach-call_true-termination.cil.c 2 510    280 6300   - - - - 2 40    1200 0 130     7000  
elevator_spec2_product31_true-unreach-call_true-termination.cil.c 2 510    290 5400   - - - - 2 41    1300 0 150     7000  
elevator_spec3_product01_true-unreach-call_true-termination.cil.c 2 490    300 5900   - - - - 2 17    670 0 190     7000  
elevator_spec3_product09_true-unreach-call_true-termination.cil.c 2 490    330 6000   - - - - 2 17    680 0 140     7000  
elevator_spec3_product17_true-unreach-call_true-termination.cil.c 2 490    300 6300   - - - - 2 14    710 0 200     7000  
elevator_spec3_product18_true-unreach-call_true-termination.cil.c 2 490    360 5000   - - - - 2 27    890 0 150     7000  
elevator_spec3_product21_true-unreach-call_true-termination.cil.c 2 490    610 6300   - - - - 2 19    880 0 120     7000  
elevator_spec3_product22_true-unreach-call_true-termination.cil.c 2 500    460 4300   - - - - 2 26    1500 0 200     7000  
elevator_spec3_product25_true-unreach-call_true-termination.cil.c 2 490    330 5900   - - - - 2 18    700 0 150     7000  
elevator_spec3_product26_true-unreach-call_true-termination.cil.c 2 490    400 5700   - - - - 2 24    930 0 190     7000  
elevator_spec3_product29_true-unreach-call_true-termination.cil.c 2 490    320 6300   - - - - 2 26    960 0 150     7000  
elevator_spec3_product30_true-unreach-call_true-termination.cil.c 2 500    520 5400   - - - - 2 34    1600 0 170     7000  
elevator_spec9_product09_true-unreach-call_true-termination.cil.c 2 500    280 7400   - - - - 2 31    900 0 190     7000  
elevator_spec9_product11_true-unreach-call_true-termination.cil.c 2 500    280 7300   - - - - 2 28    970 0 130     7000  
elevator_spec9_product25_true-unreach-call_true-termination.cil.c 2 500    280 6200   - - - - 2 30    950 0 140     7000  
elevator_spec9_product27_true-unreach-call_true-termination.cil.c 2 510    290 6100   - - - - 2 34    1100 0 160     7000  
elevator_spec9_product29_true-unreach-call_true-termination.cil.c 2 510    280 6800   - - - - 2 36    1200 0 150     7000  
elevator_spec9_product31_true-unreach-call_true-termination.cil.c 2 510    280 6800   - - - - 2 42    1300 0 140     7000  
email_spec0_product16_false-unreach-call_true-termination.cil.c 0 490    170 6100   -32 9.8  280 -32 8.7   390   0 6.2  290 0 1.0    20    - -
email_spec0_product21_false-unreach-call_true-termination.cil.c 0 500    300 6300   -32 14    350 -32 5.9   430   0 6.4  290 0 .84   20    - -
email_spec0_product22_false-unreach-call_true-termination.cil.c 0 490    190 4700   -32 10    300 -32 8.4   390   0 3.9  280 0 .86   20    - -
email_spec0_product26_false-unreach-call_true-termination.cil.c 0 500    490 5600   -32 14    450 -32 8.9   420   0 6.1  290 0 .85   20    - -
email_spec0_product31_false-unreach-call_true-termination.cil.c 0 490    180 5300   -32 7.5  420 -32 9.3   410   0 6.2  290 0 1.1    20    - -
email_spec0_product33_false-unreach-call_true-termination.cil.c 0 490    160 4900   -32 11    410 -32 8.9   410   0 5.9  280 0 1.0    20    - -
email_spec0_product34_false-unreach-call_true-termination.cil.c 0 500    230 6400   -32 15    470 -32 9.7   440   0 6.0  290 0 1.0    20    - -
email_spec0_product35_false-unreach-call_true-termination.cil.c 0 500    220 4800   -32 16    460 -32 10     450   0 6.2  290 0 1.1    20    - -
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c 0 890    1600 12000   0 .51 41 0 .019 4.9 0 .82 47 0 .0012 .31 - -
email_spec11_product15_false-unreach-call_true-termination.cil.c 0 490    140 5700   -32 10    390 -32 8.1   360   0 6.9  300 0 1.1    20    - -
email_spec11_product20_false-unreach-call_true-termination.cil.c 0 490    320 5700   -32 12    340 -32 8.5   400   0 4.1  290 0 .84   20    - -
email_spec11_product22_false-unreach-call_true-termination.cil.c 0 490    270 6300   -32 11    420 -32 8.2   400   0 6.1  290 0 1.0    20    - -
email_spec11_product26_false-unreach-call_true-termination.cil.c 0 500    190 5900   -32 13    460 -32 8.9   410   0 6.2  300 0 .85   20    - -
email_spec11_product30_false-unreach-call_true-termination.cil.c 0 490    200 6200   -32 11    420 -32 8.7   410   0 6.1  290 0 1.1    20    - -
email_spec11_product32_false-unreach-call_true-termination.cil.c 0 500    210 5400   -32 14    440 -32 9.2   410   0 5.7  280 0 1.0    20    - -
email_spec11_product33_false-unreach-call_true-termination.cil.c 0 490    180 5600   -32 11    420 -32 8.8   420   0 6.1  290 0 1.1    20    - -
email_spec11_product35_false-unreach-call_true-termination.cil.c 0 500    310 5100   -32 15    470 -32 6.6   470   0 6.5  290 0 .86   20    - -
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c 0 890    1600 8700   0 .50 41 0 .020 5.0 0 .91 49 0 .0012 .34 - -
email_spec1_product14_false-unreach-call_true-termination.cil.c 0 490    200 5400   -32 9.2  370 -32 9.1   400   0 6.2  290 0 1.0    21    - -
email_spec1_product15_false-unreach-call_true-termination.cil.c 0 490    210 5800   -32 8.7  360 -32 9.4   360   0 5.8  290 0 1.0    20    - -
email_spec1_product16_false-unreach-call_true-termination.cil.c 0 490    160 5400   -32 9.9  390 -32 5.6   400   0 5.9  280 0 1.1    20    - -
email_spec1_product20_false-unreach-call_true-termination.cil.c 0 490    180 6300   -32 12    320 -32 9.1   400   0 6.3  290 0 .87   21    - -
email_spec1_product21_false-unreach-call_true-termination.cil.c 0 490    170 5400   -32 13    470 -32 8.6   410   0 6.0  290 0 1.1    21    - -
email_spec1_product22_false-unreach-call_true-termination.cil.c 0 490    300 5400   -32 6.5  420 -32 8.7   390   0 5.8  280 0 1.0    20    - -
email_spec1_product26_false-unreach-call_true-termination.cil.c 0 490    320 5000   -32 14    460 -32 9.0   430   0 6.3  290 0 1.1    20    - -
email_spec1_product29_false-unreach-call_true-termination.cil.c 0 490    200 5500   -32 11    430 -32 9.1   430   0 6.4  300 0 .83   21    - -
email_spec1_product30_false-unreach-call_true-termination.cil.c 0 490    210 5600   -32 12    420 -32 8.5   380   0 5.9  290 0 1.0    21    - -
email_spec1_product31_false-unreach-call_true-termination.cil.c 0 490    140 5800   -32 11    430 -32 8.7   410   0 6.0  290 0 1.1    21    - -
email_spec1_product32_false-unreach-call_true-termination.cil.c 0 490    320 5500   -32 14    460 -32 8.5   420   0 6.5  300 0 1.1    20    - -
email_spec1_product33_false-unreach-call_true-termination.cil.c 0 490    360 6700   -32 7.4  420 -32 9.2   410   0 6.2  290 0 1.1    20    - -
email_spec1_product34_false-unreach-call_true-termination.cil.c 0 490    220 5600   -32 16    480 -32 9.0   460   0 6.8  290 0 1.2    21    - -
email_spec1_product35_false-unreach-call_true-termination.cil.c 0 490    240 6100   -32 15    470 -32 6.2   450   0 6.4  290 0 1.1    20    - -
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c 0 620    1600 6400   -32 33    1400 -32 10     460   0 6.6  320 0 1.2    21    - -
email_spec27_product17_false-unreach-call_true-termination.cil.c 0 490    350 5700   -32 9.9  390 -32 9.0   420   0 6.2  290 0 .87   20    - -
email_spec27_product18_false-unreach-call_true-termination.cil.c 0 490    170 5000   -32 9.2  380 -32 8.5   390   0 6.1  290 0 .86   20    - -
email_spec27_product19_false-unreach-call_true-termination.cil.c 0 490    170 5500   -32 10    310 -32 8.7   400   0 6.4  300 0 1.1    20    - -
email_spec27_product23_false-unreach-call_true-termination.cil.c 0 490    300 6200   -32 12    350 -32 8.8   410   0 6.1  300 0 1.1    20    - -
email_spec27_product24_false-unreach-call_true-termination.cil.c 0 490    230 4700   -32