Tool 2LS 0.6.0 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 11:20:26 CET 2017-12-01 07:32:03 CET 2017-12-01 08:01:50 CET 2017-12-01 08:11:41 CET 2017-12-01 08:15:34 CET 2017-12-01 04:23:32 CET 2017-12-01 07:36:49 CET
Run set 2ls.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/2ls.2017-11-30_1120.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 6.0  1200 56    -32 11   330 -32 9.5 460 0 19   1300 1 1.2  20 - -
elevator_spec14_product24_false-unreach-call_true-termination.cil.c 1 9.9  2000 81    -32 12   440 -32 10   450 0 33   1700 1 1.2  20 - -
elevator_spec14_product28_false-unreach-call_true-termination.cil.c 1 6.2  1300 60    -32 10   430 -32 8.8 450 0 24   1400 1 1.2  20 - -
elevator_spec14_product32_false-unreach-call_true-termination.cil.c 1 11    2100 100    -32 8.9 410 -32 11   460 0 26   1700 1 1.2  20 - -
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c 1 36    7000 320    -32 13   360 -32 9.5 420 0 37   2100 1 1.5  21 - -
elevator_spec1_product18_false-unreach-call_true-termination.cil.c 1 41    850 490    -32 8.5 350 -32 8.9 370 0 16   600 1 1.1  21 - -
elevator_spec1_product20_false-unreach-call_true-termination.cil.c 1 43    900 360    -32 9.8 410 -32 9.9 390 0 15   990 1 1.1  21 - -
elevator_spec1_product22_false-unreach-call_true-termination.cil.c 1 43    1200 450    -32 8.9 400 -32 8.4 400 0 18   830 1 1.3  21 - -
elevator_spec1_product24_false-unreach-call_true-termination.cil.c 1 49    1300 380    -32 7.5 280 -32 8.3 400 0 19   1100 1 1.2  21 - -
elevator_spec1_product26_false-unreach-call_true-termination.cil.c 1 43    890 370    -32 8.5 280 -32 8.7 380 0 14   610 1 1.1  20 - -
elevator_spec1_product28_false-unreach-call_true-termination.cil.c 1 45    950 560    -32 10   410 -32 10   390 0 16   960 1 1.2  21 - -
elevator_spec1_product30_false-unreach-call_true-termination.cil.c 1 53    1200 420    -32 6.8 280 -32 8.8 390 0 14   820 1 1.2  20 - -
elevator_spec1_product32_false-unreach-call_true-termination.cil.c 1 62    1300 440    -32 10   430 -32 11   390 0 22   1100 1 1.1  21 - -
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c 1 140    3700 1100    -32 9.8 430 -32 10   440 0 17   1100 1 1.2  21 - -
elevator_spec2_product18_false-unreach-call_true-termination.cil.c 1 36    870 380    -32 8.2 280 -32 11   390 0 15   480 1 1.0  20 - -
elevator_spec2_product20_false-unreach-call_true-termination.cil.c 1 37    930 330    -32 9.6 300 -32 8.5 370 0 15   820 1 1.4  21 - -
elevator_spec2_product22_false-unreach-call_true-termination.cil.c 1 46    1200 540    -32 8.9 360 -32 8.6 400 0 12   720 1 1.2  21 - -
elevator_spec2_product24_false-unreach-call_true-termination.cil.c 1 44    1300 340    -32 6.6 420 -32 11   410 0 19   1000 1 1.2  21 - -
elevator_spec2_product26_false-unreach-call_true-termination.cil.c 1 32    900 310    -32 8.7 330 -32 8.8 380 0 14   610 1 1.4  20 - -
elevator_spec2_product28_false-unreach-call_true-termination.cil.c 1 36    970 290    -32 11   430 -32 8.6 410 0 15   700 1 1.3  21 - -
elevator_spec2_product30_false-unreach-call_true-termination.cil.c 1 40    1200 380    -32 8.3 360 -32 8.6 400 0 13   680 1 1.2  22 - -
elevator_spec2_product32_false-unreach-call_true-termination.cil.c 1 46    1300 430    -32 9.7 410 -32 8.4 410 0 17   1000 1 1.2  21 - -
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c 1 130    3800 1200    -32 5.9 290 -32 9.0 430 0 6.0 280 1 1.4  21 - -
elevator_spec3_product03_false-unreach-call_true-termination.cil.c 1 2.9  580 31    -32 7.5 280 -32 9.0 450 0 8.2 390 1 1.1  22 - -
elevator_spec3_product11_false-unreach-call_true-termination.cil.c 1 3.1  620 29    -32 7.8 280 -32 9.4 460 0 11   400 1 1.1  22 - -
elevator_spec3_product19_false-unreach-call_true-termination.cil.c 1 3.2  660 32    -32 8.4 280 -32 12   460 0 9.0 290 1 1.2  22 - -
elevator_spec3_product20_false-unreach-call_true-termination.cil.c 1 6.1  1200 61    -32 8.3 280 -32 10   460 0 9.3 280 1 1.1  21 - -
elevator_spec3_product23_false-unreach-call_true-termination.cil.c 1 5.4  1000 53    -32 7.7 280 -32 9.6 460 0 6.6 420 1 1.2  22 - -
elevator_spec3_product24_false-unreach-call_true-termination.cil.c 1 11    2000 99    -32 8.4 290 -32 12   460 0 8.8 420 1 1.2  22 - -
elevator_spec3_product27_false-unreach-call_true-termination.cil.c 1 3.6  700 34    -32 7.5 280 -32 9.6 450 0 9.9 420 1 1.3  22 - -
elevator_spec3_product28_false-unreach-call_true-termination.cil.c 1 6.6  1300 63    -32 8.2 310 -32 10   460 0 8.7 430 1 1.2  21 - -
elevator_spec3_product31_false-unreach-call_true-termination.cil.c 1 5.5  1100 64    -32 5.3 280 -32 12   460 0 9.0 420 1 1.3  22 - -
elevator_spec3_product32_false-unreach-call_true-termination.cil.c 1 11    2100 120    -32 8.9 310 -32 10   460 0 8.5 420 1 1.5  22 - -
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c 1 38    7000 400    -32 8.0 290 1 54   2500 0 9.4 310 1 1.3  22 - -
elevator_spec9_product26_false-unreach-call_true-termination.cil.c 1 39    900 390    -32 8.2 300 -32 11   390 0 13   610 1 1.3  20 - -
elevator_spec9_product28_false-unreach-call_true-termination.cil.c 1 39    950 400    -32 9.1 420 -32 8.7 380 0 19   890 1 1.4  21 - -
elevator_spec9_product30_false-unreach-call_true-termination.cil.c 1 46    1300 360    -32 9.2 390 -32 11   410 0 15   690 1 1.2  21 - -
elevator_spec9_product32_false-unreach-call_true-termination.cil.c 1 47    1300 340    -32 11   430 -32 11   410 0 24   1100 1 1.3  21 - -
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c 1 93    3700 870    -32 5.8 300 -32 9.0 420 0 6.1 280 1 1.2  21 - -
elevator_spec13_product21_true-unreach-call_false-termination.cil.c 0 5.4  1000 48    - - - - 0 .64 42 0 .019 4.9
elevator_spec13_product22_true-unreach-call_false-termination.cil.c 0 11    1900 100    - - - - 0 .53 41 0 .019 5.0
elevator_spec13_product23_true-unreach-call_false-termination.cil.c 0 5.9  1100 50    - - - - 0 .56 43 0 .018 5.0
elevator_spec13_product24_true-unreach-call_false-termination.cil.c 0 11    2100 98    - - - - 0 .56 41 0 .018 4.8
elevator_spec13_product29_true-unreach-call_false-termination.cil.c 0 5.6  1100 44    - - - - 0 .57 43 0 .018 5.0
elevator_spec13_product30_true-unreach-call_false-termination.cil.c 0 11    2000 91    - - - - 0 .59 42 0 .048 4.8
elevator_spec13_product31_true-unreach-call_false-termination.cil.c 0 5.8  1200 60    - - - - 0 .57 43 0 .024 5.0
elevator_spec13_product32_true-unreach-call_false-termination.cil.c 0 11    2200 140    - - - - 0 .65 41 0 .023 4.8
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c 0 47    7300 380    - - - - 0 .54 45 0 .050 4.9
elevator_spec14_product03_true-unreach-call_true-termination.cil.c 2 20    860 210    - - - - 2 22    900 0 330     7000  
elevator_spec14_product11_true-unreach-call_true-termination.cil.c 2 20    910 180    - - - - 2 31    980 0 310     7000  
elevator_spec14_product19_true-unreach-call_true-termination.cil.c 2 24    1000 240    - - - - 2 24    1400 0 230     7000  
elevator_spec14_product23_true-unreach-call_true-termination.cil.c 2 10    1300 100    - - - - 2 35    1600 0 260     7000  
elevator_spec14_product27_true-unreach-call_true-termination.cil.c 2 24    1100 220    - - - - 2 23    1400 0 280     7000  
elevator_spec14_product31_true-unreach-call_true-termination.cil.c 2 11    1400 110    - - - - 2 32    1600 0 210     7000  
elevator_spec1_product01_true-unreach-call_true-termination.cil.c 2 28    1000 240    - - - - 2 80    1800 0 290     7000  
elevator_spec1_product03_true-unreach-call_true-termination.cil.c 2 30    1100 300    - - - - 2 78    1900 0 270     7000  
elevator_spec1_product09_true-unreach-call_true-termination.cil.c 2 29    1000 270    - - - - 2 100    1900 0 270     7000  
elevator_spec1_product11_true-unreach-call_true-termination.cil.c 2 31    1100 300    - - - - 2 86    2100 0 290     7000  
elevator_spec1_product17_true-unreach-call_true-termination.cil.c 2 33    1100 300    - - - - 2 78    1900 0 280     7000  
elevator_spec1_product19_true-unreach-call_true-termination.cil.c 2 31    1100 280    - - - - 2 100    2100 0 230     7000  
elevator_spec1_product21_true-unreach-call_true-termination.cil.c 2 39    1500 350    - - - - 2 170    2600 0 290     7000  
elevator_spec1_product23_true-unreach-call_true-termination.cil.c 2 39    1600 420    - - - - 2 140    2700 0 220     7000  
elevator_spec1_product25_true-unreach-call_true-termination.cil.c 2 29    1100 330    - - - - 2 72    2000 0 230     7000  
elevator_spec1_product27_true-unreach-call_true-termination.cil.c 2 34    1200 320    - - - - 2 88    2200 0 310     7000  
elevator_spec1_product29_true-unreach-call_true-termination.cil.c 2 37    1600 350    - - - - 2 190    2700 0 200     7000  
elevator_spec1_product31_true-unreach-call_true-termination.cil.c 2 37    1600 420    - - - - 2 150    2800 0 240     7000  
elevator_spec2_product01_true-unreach-call_true-termination.cil.c 2 21    710 180    - - - - 2 31    1100 0 140     7000  
elevator_spec2_product03_true-unreach-call_true-termination.cil.c 2 21    750 220    - - - - 2 37    1200 0 150     7000  
elevator_spec2_product09_true-unreach-call_true-termination.cil.c 2 22    750 200    - - - - 2 31    1200 0 170     7000  
elevator_spec2_product11_true-unreach-call_true-termination.cil.c 2 22    790 240    - - - - 2 38    1300 0 150     7000  
elevator_spec2_product17_true-unreach-call_true-termination.cil.c 2 23    780 260    - - - - 2 35    1300 0 130     7000  
elevator_spec2_product19_true-unreach-call_true-termination.cil.c 2 26    830 250    - - - - 2 34    1400 0 110     7000  
elevator_spec2_product21_true-unreach-call_true-termination.cil.c 2 24    1100 280    - - - - 2 52    1500 0 140     7000  
elevator_spec2_product23_true-unreach-call_true-termination.cil.c 2 29    1100 240    - - - - 2 44    1600 0 230     7000  
elevator_spec2_product25_true-unreach-call_true-termination.cil.c 2 25    810 220    - - - - 2 36    1300 0 130     7000  
elevator_spec2_product27_true-unreach-call_true-termination.cil.c 2 27    860 230    - - - - 2 56    1700 0 190     7000  
elevator_spec2_product29_true-unreach-call_true-termination.cil.c 2 28    1100 220    - - - - 2 61    1600 0 130     7000  
elevator_spec2_product31_true-unreach-call_true-termination.cil.c 2 30    1200 260    - - - - 2 56    1800 0 190     7000  
elevator_spec3_product01_true-unreach-call_true-termination.cil.c 2 3.1  630 31    - - - - 2 23    920 0 220     7000  
elevator_spec3_product09_true-unreach-call_true-termination.cil.c 2 3.3  680 31    - - - - 2 26    890 0 160     7000  
elevator_spec3_product17_true-unreach-call_true-termination.cil.c 2 3.4  730 34    - - - - 2 29    920 0 150     7000  
elevator_spec3_product18_true-unreach-call_true-termination.cil.c 2 6.4  1400 61    - - - - 2 30    1600 0 190     7000  
elevator_spec3_product21_true-unreach-call_true-termination.cil.c 2 5.5  1200 50    - - - - 2 29    1400 0 130     7000  
elevator_spec3_product22_true-unreach-call_true-termination.cil.c 2 11    2300 120    - - - - 2 40    1600 0 190     7000  
elevator_spec3_product25_true-unreach-call_true-termination.cil.c 2 3.6  770 34    - - - - 2 28    980 0 130     7000  
elevator_spec3_product26_true-unreach-call_true-termination.cil.c 2 6.8  1500 63    - - - - 2 32    1600 0 220     7000  
elevator_spec3_product29_true-unreach-call_true-termination.cil.c 2 5.7  1200 57    - - - - 2 28    1400 0 120     7000  
elevator_spec3_product30_true-unreach-call_true-termination.cil.c 2 12    2400 120    - - - - 2 42    1700 0 230     7000  
elevator_spec9_product09_true-unreach-call_true-termination.cil.c 2 22    750 220    - - - - 2 33    1300 0 180     7000  
elevator_spec9_product11_true-unreach-call_true-termination.cil.c 2 22    780 190    - - - - 2 40    1300 0 130     7000  
elevator_spec9_product25_true-unreach-call_true-termination.cil.c 2 22    810 320    - - - - 2 32    1200 0 140     7000  
elevator_spec9_product27_true-unreach-call_true-termination.cil.c 2 24    860 210    - - - - 2 38    1700 0 120     7000  
elevator_spec9_product29_true-unreach-call_true-termination.cil.c 2 28    1100 280    - - - - 2 48    1600 0 230     7000  
elevator_spec9_product31_true-unreach-call_true-termination.cil.c 2 33    1200 320    - - - - 2 53    1800 0 180     7000  
email_spec0_product16_false-unreach-call_true-termination.cil.c 1 21    290 190    -32 9.1 390 0 29   580 0 7.2 290 1 1.1  20 - -
email_spec0_product21_false-unreach-call_true-termination.cil.c 1 37    500 300    -32 18   530 0 33   570 0 9.2 420 1 1.1  20 - -
email_spec0_product22_false-unreach-call_true-termination.cil.c 1 26    310 190    -32 9.2 410 0 34   600 0 7.5 350 1 1.1  20 - -
email_spec0_product26_false-unreach-call_true-termination.cil.c 1 42    540 550    -32 18   630 0 55   640 0 12   420 1 1.3  20 - -
email_spec0_product31_false-unreach-call_true-termination.cil.c 1 20    320 210    -32 10   410 0 40   610 0 9.0 370 1 1.2  20 - -
email_spec0_product33_false-unreach-call_true-termination.cil.c 1 25    350 210    -32 9.6 410 0 32   580 0 9.2 280 1 1.1  20 - -
email_spec0_product34_false-unreach-call_true-termination.cil.c 1 37    590 430    -32 15   460 0 45   680 0 8.2 420 1 1.1  20 - -
email_spec0_product35_false-unreach-call_true-termination.cil.c 1 48    670 450    -32 5.7 270 0 50   880 0 10   450 1 1.5  20 - -
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c 1 200    8000 1300    -32 7.2 300 -32 11   440 0 11   460 1 1.2  21 - -
email_spec11_product15_false-unreach-call_true-termination.cil.c 1 19    270 240    -32 11   410 0 41   590 0 8.7 420 1 1.2  20 - -
email_spec11_product20_false-unreach-call_true-termination.cil.c 1 41    460 400    -32 11   400 0 39   620 0 8.9 360 1 1.1  19 - -
email_spec11_product22_false-unreach-call_true-termination.cil.c 1 21    310 210    -32 12   440 0 29   570 0 8.3 420 1 1.0  20 - -
email_spec11_product26_false-unreach-call_true-termination.cil.c 1 43    540 370    -32 18   630 0 41   560 0 9.0 410 1 1.1  20 - -
email_spec11_product30_false-unreach-call_true-termination.cil.c 1 23    300 190    -32 9.3 410 0 37   640 0 8.9 280 1 1.1  20 - -
email_spec11_product32_false-unreach-call_true-termination.cil.c 1 39    520 370    -32 13   460 0 47   720 0 7.9 380 1 1.2  20 - -
email_spec11_product33_false-unreach-call_true-termination.cil.c 1 22    350 210    -32 14   400 0 39   670 0 11   420 1 1.1  20 - -
email_spec11_product35_false-unreach-call_true-termination.cil.c 1 46    640 420    -32 15   460 0 40   780 0 8.2 410 1 1.1  20 - -
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c 1 280    8500 1400    -32 15   490 -32 10   460 0 12   470 1 1.2  20 - -
email_spec1_product14_false-unreach-call_true-termination.cil.c 1 31    390 290    -32 9.1 340 -32 8.8 380 0 7.5 330 1 1.1  20 - -
email_spec1_product15_false-unreach-call_true-termination.cil.c 1 23    250 180    -32 8.8 370 -32 9.9 380 0 6.7 300 1 1.4  20 - -
email_spec1_product16_false-unreach-call_true-termination.cil.c 1 23    270 180    -32 9.2 370 -32 9.9 390 0 7.4 330 1 1.3  20 - -
email_spec1_product20_false-unreach-call_true-termination.cil.c 1 41    440 320    -32 12   410 -32 8.4 400 0 11   280 1 1.4  20 - -
email_spec1_product21_false-unreach-call_true-termination.cil.c 1 42    480 350    -32 18   580 -32 8.9 410 0 8.9 410 1 1.2  21 - -
email_spec1_product22_false-unreach-call_true-termination.cil.c 1 25    290 210    -32 10   430 -32 8.3 400 0 7.3 340 1 1.1  20 - -
email_spec1_product26_false-unreach-call_true-termination.cil.c 1 44    520 400    -32 13   470 -32 10   430 0 8.1 280 1 1.1  20 - -
email_spec1_product29_false-unreach-call_true-termination.cil.c 1 33    460 280    -32 13   460 -32 10   440 0 9.0 410 1 1.2  20 - -
email_spec1_product30_false-unreach-call_true-termination.cil.c 1 21    300 240    -32 6.0 270 -32 8.8 400 0 10   300 1 1.2  20 - -
email_spec1_product31_false-unreach-call_true-termination.cil.c 1 22    310 260    -32 11   410 -32 9.9 400 0 7.9 370 1 1.2  21 - -
email_spec1_product32_false-unreach-call_true-termination.cil.c 1 39    500 330    -32 13   460 -32 9.2 430 0 8.4 410 1 1.2  20 - -
email_spec1_product33_false-unreach-call_true-termination.cil.c 1 25    340 270    -32 11   410 -32 11   430 0 9.3 280 1 1.2  21 - -
email_spec1_product34_false-unreach-call_true-termination.cil.c 1 40    570 340    -32 16   460 -32 9.9 460 0 10   420 1 1.2  21 - -
email_spec1_product35_false-unreach-call_true-termination.cil.c 1 45    620 360    -32 16   460 -32 9.5 450 0 9.2 410 1 1.5  20 - -
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c 1 140    7600 1100    -32 14   470 -32 9.6 460 0 10   460 1 1.2  21 - -
email_spec27_product17_false-unreach-call_true-termination.cil.c 1 32    400 280    -32 9.3 370 0 34   610 0 7.7 280 1 1.3  20 - -
email_spec27_product18_false-unreach-call_true-termination.cil.c 1 23    260 180    -32 8.8 380 -32 8.5 390 0 8.1 310 1 1.4  21 - -
email_spec27_product19_false-unreach-call_true-termination.cil.c 1 19    280 190    -32 9.3 410 -32 10   400 0 8.3 340 1 1.2  21 - -
email_spec27_product23_false-unreach-call_true-termination.cil.c 1 44    450 370    -32 13   440 0 45   700 0 8.1 280 1 1.3  21 - -
email_spec27_product24_false-unreach-call_true-termination.cil.c 1 23    300 200    -32 6.8 440 -32 10   400 0 9.5 280 1 1.3  21 - -
email_spec27_product25_false-unreach-call_true-termination.cil.c 1 33    480 330    -32 14   440 0 39