Tool ULTIMATE Taipan 0.1.23-3204b741 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-12-02 17:23:13 CET 2017-12-03 07:22:17 CET 2017-12-03 07:45:29 CET 2017-12-03 07:47:53 CET 2017-12-03 07:50:34 CET 2017-12-03 06:47:45 CET 2017-12-03 07:25:40 CET
Run set utaipan.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/utaipan.2017-12-02_1723.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 0 900   4700 12000 0 .53 43 0 .026 4.8 0 .81 49 0 .0035 .30 - -
elevator_spec14_product24_false-unreach-call_true-termination.cil.c 0 900   4600 9600 0 .55 43 0 .032 4.8 0 .86 49 0 .0024 .32 - -
elevator_spec14_product28_false-unreach-call_true-termination.cil.c 0 900   4600 12000 0 .57 43 0 .051 4.8 0 .83 49 0 .0042 .31 - -
elevator_spec14_product32_false-unreach-call_true-termination.cil.c 0 900   4700 11000 0 .55 41 0 .046 4.9 0 .84 47 0 .0045 .30 - -
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c 0 900   4700 11000 0 .57 43 0 .018 4.8 0 .85 47 0 .0041 .26 - -
elevator_spec1_product18_false-unreach-call_true-termination.cil.c 0 900   5400 11000 0 .51 43 0 .035 4.8 0 .83 49 0 .0032 .29 - -
elevator_spec1_product20_false-unreach-call_true-termination.cil.c 0 900   4600 10000 0 .53 45 0 .025 4.8 0 .88 49 0 .0032 .31 - -
elevator_spec1_product22_false-unreach-call_true-termination.cil.c 0 900   4700 11000 0 .54 45 0 .052 5.0 0 .82 47 0 .0042 .34 - -
elevator_spec1_product24_false-unreach-call_true-termination.cil.c 0 900   4600 10000 0 .51 43 0 .045 4.8 0 .86 49 0 .0036 .31 - -
elevator_spec1_product26_false-unreach-call_true-termination.cil.c 0 900   8200 10000 0 .54 41 0 .019 5.0 0 .85 47 0 .0018 .31 - -
elevator_spec1_product28_false-unreach-call_true-termination.cil.c 0 900   4600 10000 0 .51 43 0 .018 4.9 0 .79 47 0 .0012 .26 - -
elevator_spec1_product30_false-unreach-call_true-termination.cil.c 0 900   4600 11000 0 .53 41 0 .018 4.8 0 .83 49 0 .0011 .32 - -
elevator_spec1_product32_false-unreach-call_true-termination.cil.c 0 900   4600 10000 0 .55 43 0 .048 4.9 0 .85 49 0 .0047 .29 - -
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c 0 900   4400 11000 0 .52 41 0 .024 4.8 0 .85 47 0 .0036 .32 - -
elevator_spec2_product18_false-unreach-call_true-termination.cil.c 0 900   6100 11000 0 .53 44 0 .023 5.0 0 .79 47 0 .0041 .26 - -
elevator_spec2_product20_false-unreach-call_true-termination.cil.c 0 900   13000 7600 0 .54 46 0 .021 5.0 0 .83 47 0 .0042 .30 - -
elevator_spec2_product22_false-unreach-call_true-termination.cil.c 0 900   6500 10000 0 .54 44 0 .018 4.8 0 .78 49 0 .0035 .34 - -
elevator_spec2_product24_false-unreach-call_true-termination.cil.c 0 900   4600 11000 0 .56 43 0 .051 4.9 0 .85 49 0 .0041 .35 - -
elevator_spec2_product26_false-unreach-call_true-termination.cil.c 0 900   6200 10000 0 .53 43 0 .025 4.8 0 .83 48 0 .0040 .34 - -
elevator_spec2_product28_false-unreach-call_true-termination.cil.c 0 900   4700 11000 0 .51 43 0 .046 4.8 0 .86 49 0 .0035 .30 - -
elevator_spec2_product30_false-unreach-call_true-termination.cil.c 0 900   5600 11000 0 .52 41 0 .018 4.9 0 .88 49 0 .0043 .29 - -
elevator_spec2_product32_false-unreach-call_true-termination.cil.c 0 900   4600 11000 0 .56 43 0 .050 4.9 0 .84 49 0 .0041 .29 - -
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c 0 900   6500 10000 0 .53 43 0 .045 4.8 0 .89 50 0 .0036 .31 - -
elevator_spec3_product03_false-unreach-call_true-termination.cil.c 0 900   5400 10000 0 .58 47 0 .042 4.9 0 .84 49 0 .0044 .29 - -
elevator_spec3_product11_false-unreach-call_true-termination.cil.c 0 900   5500 11000 0 .55 41 0 .025 4.8 0 .86 49 0 .0045 .26 - -
elevator_spec3_product19_false-unreach-call_true-termination.cil.c 0 900   4600 11000 0 .53 43 0 .025 4.9 0 .83 49 0 .0042 .31 - -
elevator_spec3_product20_false-unreach-call_true-termination.cil.c 0 900   5400 11000 0 .55 44 0 .039 4.9 0 .87 49 0 .0041 .26 - -
elevator_spec3_product23_false-unreach-call_true-termination.cil.c 0 900   4600 13000 0 .52 42 0 .018 4.9 0 .87 49 0 .0042 .29 - -
elevator_spec3_product24_false-unreach-call_true-termination.cil.c 0 900   4600 11000 0 .55 45 0 .023 4.9 0 .85 49 0 .0048 .26 - -
elevator_spec3_product27_false-unreach-call_true-termination.cil.c 0 900   5400 11000 0 .51 43 0 .018 4.9 0 .84 47 0 .0048 .29 - -
elevator_spec3_product28_false-unreach-call_true-termination.cil.c 0 900   4600 12000 0 .56 42 0 .018 5.0 0 .85 49 0 .0037 .30 - -
elevator_spec3_product31_false-unreach-call_true-termination.cil.c 0 900   4600 10000 0 .50 43 0 .023 4.8 0 .85 49 0 .0035 .34 - -
elevator_spec3_product32_false-unreach-call_true-termination.cil.c 0 900   4600 11000 0 .54 42 0 .023 4.9 0 .85 47 0 .0041 .34 - -
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c 0 900   4700 12000 0 .52 41 0 .018 4.9 0 .83 47 0 .0041 .30 - -
elevator_spec9_product26_false-unreach-call_true-termination.cil.c 0 910   14000 5000 0 .52 43 0 .047 4.9 0 .79 47 0 .0041 .30 - -
elevator_spec9_product28_false-unreach-call_true-termination.cil.c 0 910   14000 5400 0 .55 44 0 .046 5.0 0 .87 49 0 .0043 .26 - -
elevator_spec9_product30_false-unreach-call_true-termination.cil.c 0 910   14000 5200 0 .55 44 0 .051 4.8 0 .84 49 0 .0047 .26 - -
elevator_spec9_product32_false-unreach-call_true-termination.cil.c 0 910   14000 5000 0 .54 41 0 .027 4.8 0 .86 48 0 .0043 .26 - -
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c 0 910   14000 4900 0 .54 44 0 .025 4.8 0 .85 52 0 .0041 .30 - -
elevator_spec13_product21_true-unreach-call_false-termination.cil.c 0 900   5400 10000 - - - - 0 .69 41 0 .020 4.9
elevator_spec13_product22_true-unreach-call_false-termination.cil.c 0 900   4700 12000 - - - - 0 .50 44 0 .048 4.8
elevator_spec13_product23_true-unreach-call_false-termination.cil.c 0 900   4600 11000 - - - - 0 .50 42 0 .017 5.0
elevator_spec13_product24_true-unreach-call_false-termination.cil.c 0 900   4900 11000 - - - - 0 .64 46 0 .021 4.9
elevator_spec13_product29_true-unreach-call_false-termination.cil.c 0 900   5400 11000 - - - - 0 .52 43 0 .023 4.9
elevator_spec13_product30_true-unreach-call_false-termination.cil.c 0 900   5300 12000 - - - - 0 .72 42 0 .019 4.9
elevator_spec13_product31_true-unreach-call_false-termination.cil.c 0 900   4700 11000 - - - - 0 .52 42 0 .018 4.8
elevator_spec13_product32_true-unreach-call_false-termination.cil.c 0 900   5400 13000 - - - - 0 .57 43 0 .018 4.8
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c 0 900   5000 10000 - - - - 0 .53 43 0 .018 5.0
elevator_spec14_product03_true-unreach-call_true-termination.cil.c 0 900   4600 10000 - - - - 0 .53 42 0 .019 4.9
elevator_spec14_product11_true-unreach-call_true-termination.cil.c 0 900   4600 11000 - - - - 0 .59 43 0 .018 4.9
elevator_spec14_product19_true-unreach-call_true-termination.cil.c 0 900   4600 12000 - - - - 0 .51 43 0 .018 5.0
elevator_spec14_product23_true-unreach-call_true-termination.cil.c 0 900   4600 11000 - - - - 0 .60 44 0 .018 4.9
elevator_spec14_product27_true-unreach-call_true-termination.cil.c 0 900   4700 12000 - - - - 0 .54 41 0 .048 4.9
elevator_spec14_product31_true-unreach-call_true-termination.cil.c 0 900   4600 10000 - - - - 0 .55 43 0 .019 4.8
elevator_spec1_product01_true-unreach-call_true-termination.cil.c 0 900   4600 10000 - - - - 0 .57 42 0 .023 4.9
elevator_spec1_product03_true-unreach-call_true-termination.cil.c 0 900   4700 11000 - - - - 0 .61 41 0 .018 4.8
elevator_spec1_product09_true-unreach-call_true-termination.cil.c 0 900   4600 11000 - - - - 0 .56 44 0 .049 4.9
elevator_spec1_product11_true-unreach-call_true-termination.cil.c 0 900   4200 9500 - - - - 0 .52 42 0 .041 4.9
elevator_spec1_product17_true-unreach-call_true-termination.cil.c 0 900   5400 10000 - - - - 0 .55 41 0 .017 5.0
elevator_spec1_product19_true-unreach-call_true-termination.cil.c 0 900   4500 10000 - - - - 0 .60 42 0 .017 4.8
elevator_spec1_product21_true-unreach-call_true-termination.cil.c 0 900   4600 9900 - - - - 0 .67 41 0 .042 4.9
elevator_spec1_product23_true-unreach-call_true-termination.cil.c 0 900   4600 11000 - - - - 0 .52 41 0 .037 4.8
elevator_spec1_product25_true-unreach-call_true-termination.cil.c 0 900   6200 12000 - - - - 0 .70 44 0 .018 4.9
elevator_spec1_product27_true-unreach-call_true-termination.cil.c 0 900   4700 11000 - - - - 0 .67 43 0 .018 5.0
elevator_spec1_product29_true-unreach-call_true-termination.cil.c 0 900   4600 10000 - - - - 0 .60 44 0 .042 4.8
elevator_spec1_product31_true-unreach-call_true-termination.cil.c 0 900   4600 12000 - - - - 0 .55 41 0 .018 4.9
elevator_spec2_product01_true-unreach-call_true-termination.cil.c 0 910   13000 6000 - - - - 0 .51 43 0 .018 5.0
elevator_spec2_product03_true-unreach-call_true-termination.cil.c 0 900   6700 13000 - - - - 0 .56 45 0 .019 4.8
elevator_spec2_product09_true-unreach-call_true-termination.cil.c 0 910   13000 5500 - - - - 0 .54 41 0 .018 4.8
elevator_spec2_product11_true-unreach-call_true-termination.cil.c 0 900   6300 12000 - - - - 0 .55 43 0 .048 4.9
elevator_spec2_product17_true-unreach-call_true-termination.cil.c 0 910   14000 6000 - - - - 0 .58 43 0 .023 4.9
elevator_spec2_product19_true-unreach-call_true-termination.cil.c 0 900   5900 11000 - - - - 0 .55 43 0 .018 4.9
elevator_spec2_product21_true-unreach-call_true-termination.cil.c 0 900   8600 8500 - - - - 0 .66 41 0 .045 4.8
elevator_spec2_product23_true-unreach-call_true-termination.cil.c 0 900   4700 11000 - - - - 0 .52 41 0 .017 4.8
elevator_spec2_product25_true-unreach-call_true-termination.cil.c 0 900   13000 5500 - - - - 0 .55 43 0 .025 4.9
elevator_spec2_product27_true-unreach-call_true-termination.cil.c 0 900   6200 11000 - - - - 0 .52 43 0 .023 4.8
elevator_spec2_product29_true-unreach-call_true-termination.cil.c 0 900   12000 7500 - - - - 0 .53 43 0 .018 4.8
elevator_spec2_product31_true-unreach-call_true-termination.cil.c 0 900   6000 12000 - - - - 0 .59 42 0 .038 4.9
elevator_spec3_product01_true-unreach-call_true-termination.cil.c 0 900   6500 11000 - - - - 0 .62 44 0 .047 4.9
elevator_spec3_product09_true-unreach-call_true-termination.cil.c 0 900   13000 5600 - - - - 0 .54 41 0 .019 4.9
elevator_spec3_product17_true-unreach-call_true-termination.cil.c 0 900   6600 11000 - - - - 0 .60 43 0 .018 4.9
elevator_spec3_product18_true-unreach-call_true-termination.cil.c 0 910   13000 6600 - - - - 0 .57 43 0 .019 4.9
elevator_spec3_product21_true-unreach-call_true-termination.cil.c 0 900   8400 11000 - - - - 0 .71 41 0 .019 5.0
elevator_spec3_product22_true-unreach-call_true-termination.cil.c 0 900   9600 8900 - - - - 0 .52 43 0 .018 4.8
elevator_spec3_product25_true-unreach-call_true-termination.cil.c 0 900   7000 11000 - - - - 0 .54 41 0 .017 5.0
elevator_spec3_product26_true-unreach-call_true-termination.cil.c 0 900   6400 10000 - - - - 0 .55 41 0 .018 4.8
elevator_spec3_product29_true-unreach-call_true-termination.cil.c 0 900   8400 9800 - - - - 0 .71 43 0 .018 4.9
elevator_spec3_product30_true-unreach-call_true-termination.cil.c 0 900   4600 11000 - - - - 0 .68 44 0 .048 4.8
elevator_spec9_product09_true-unreach-call_true-termination.cil.c 0 910   13000 5800 - - - - 0 .53 43 0 .018 4.8
elevator_spec9_product11_true-unreach-call_true-termination.cil.c 0 910   14000 5200 - - - - 0 .69 43 0 .024 4.9
elevator_spec9_product25_true-unreach-call_true-termination.cil.c 0 910   13000 6900 - - - - 0 .54 45 0 .018 5.0
elevator_spec9_product27_true-unreach-call_true-termination.cil.c 0 910   14000 5300 - - - - 0 .56 41 0 .018 5.0
elevator_spec9_product29_true-unreach-call_true-termination.cil.c 0 910   13000 6000 - - - - 0 .52 44 0 .049 5.0
elevator_spec9_product31_true-unreach-call_true-termination.cil.c 0 910   14000 5300 - - - - 0 .55 43 0 .018 5.0
email_spec0_product16_false-unreach-call_true-termination.cil.c 0 900   6000 11000 0 .53 44 0 .018 4.9 0 .86 50 0 .0041 .35 - -
email_spec0_product21_false-unreach-call_true-termination.cil.c 0 900   5400 12000 0 .53 45 0 .047 4.9 0 .84 47 0 .0041 .34 - -
email_spec0_product22_false-unreach-call_true-termination.cil.c 0 910   13000 5700 0 .55 43 0 .048 4.9 0 .86 49 0 .0041 .28 - -
email_spec0_product26_false-unreach-call_true-termination.cil.c 0 910   12000 7500 0 .49 43 0 .047 4.8 0 .84 49 0 .0041 .30 - -
email_spec0_product31_false-unreach-call_true-termination.cil.c 0 900   6200 12000 0 .54 41 0 .046 4.9 0 .87 49 0 .0044 .29 - -
email_spec0_product33_false-unreach-call_true-termination.cil.c 0 900   5400 12000 0 .51 42 0 .027 5.0 0 .87 49 0 .0042 .31 - -
email_spec0_product34_false-unreach-call_true-termination.cil.c 0 900   5800 12000 0 .50 41 0 .048 4.8 0 .80 49 0 .0039 .30 - -
email_spec0_product35_false-unreach-call_true-termination.cil.c 0 900   4800 13000 0 .55 43 0 .050 5.0 0 .86 49 0 .0045 .26 - -
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c 0 900   4600 11000 0 .53 44 0 .024 4.9 0 .81 49 0 .0046 .29 - -
email_spec11_product15_false-unreach-call_true-termination.cil.c 0 900   6600 9600 0 .54 42 0 .020 4.8 0 .84 48 0 .0027 .29 - -
email_spec11_product20_false-unreach-call_true-termination.cil.c 0 900   5400 12000 0 .55 44 0 .017 5.0 0 .84 47 0 .0011 .34 - -
email_spec11_product22_false-unreach-call_true-termination.cil.c 0 900   6000 11000 0 .52 41 0 .047 4.8 0 .83 49 0 .0042 .26 - -
email_spec11_product26_false-unreach-call_true-termination.cil.c 0 900   5300 13000 0 .56 42 0 .018 4.8 0 .78 49 0 .0045 .34 - -
email_spec11_product30_false-unreach-call_true-termination.cil.c 0 900   7600 11000 0 .55 44 0 .027 5.0 0 .84 49 0 .0012 .26 - -
email_spec11_product32_false-unreach-call_true-termination.cil.c 0 900   6700 9900 0 .49 42 0 .048 4.9 0 .85 49 0 .0022 .31 - -
email_spec11_product33_false-unreach-call_true-termination.cil.c 0 900   6800 12000 0 .55 43 0 .051 4.9 0 .86 50 0 .0038 .26 - -
email_spec11_product35_false-unreach-call_true-termination.cil.c 0 900   6000 9700 0 .55 41 0 .018 4.9 0 .82 47 0 .0012 .29 - -
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c 0 900   13000 6200 0 .50 41 0 .042 4.8 0 .90 50 0 .0038 .34 - -
email_spec1_product14_false-unreach-call_true-termination.cil.c 0 900   9900 8600 0 .54 41 0 .022 5.0 0 .86 50 0 .0013 .28 - -
email_spec1_product15_false-unreach-call_true-termination.cil.c 0 900   5700 12000 0 .58 43 0 .018 5.0 0 .81 47 0 .0037 .35 - -
email_spec1_product16_false-unreach-call_true-termination.cil.c 0 900   5700 12000 0 .55 43 0 .049 4.8 0 .88 51 0 .0037 .29 - -
email_spec1_product20_false-unreach-call_true-termination.cil.c 0 900   8400 10000 0 .53 44 0 .031 4.8 0 .84 48 0 .0042 .26 - -
email_spec1_product21_false-unreach-call_true-termination.cil.c 0 900   9200 11000 0 .51 41 0 .033 4.9 0 .81 49 0 .0014 .34 - -
email_spec1_product22_false-unreach-call_true-termination.cil.c 0 900   5500 11000 0 .54 43 0 .038 4.8 0 .82 47 0 .0012 .26 - -
email_spec1_product26_false-unreach-call_true-termination.cil.c 0 900   9700 8000 0 .55 45 0 .050 4.9 0 .86 49 0 .0014 .26 - -
email_spec1_product29_false-unreach-call_true-termination.cil.c 0 900   9300 9600 0 .58 44 0 .020 5.0 0 .80 48 0 .0041 .33 - -
email_spec1_product30_false-unreach-call_true-termination.cil.c 0 900   7400 11000 0 .51 43 0 .018 4.9 0 .85 51 0 .0047 .26 - -
email_spec1_product31_false-unreach-call_true-termination.cil.c 0 910   10000 9700 0 .56 43 0 .018 4.9 0 .88 52 0 .0042 .26 - -
email_spec1_product32_false-unreach-call_true-termination.cil.c 0 900   10000 10000 0 .55 43 0 .046 4.8 0 .88 49 0 .0037 .30 - -
email_spec1_product33_false-unreach-call_true-termination.cil.c 0 900   12000 9000 0 .55 45 0 .021 5.0 0 .89 49 0 .0037 .32 - -
email_spec1_product34_false-unreach-call_true-termination.cil.c 0 900   9800 9100 0 .53 42 0 .025 4.9 0 .83 49 0 .0038 .29 - -
email_spec1_product35_false-unreach-call_true-termination.cil.c 0 900   11000 9000 0 .57 41 0 .046 4.8 0 .90 49 0 .0047 .26 - -
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c 0 900   5100 13000 0 .56 43 0 .024 4.9 0 .83 51 0 .0040 .33 - -
email_spec27_product17_false-unreach-call_true-termination.cil.c 0 900   5200 11000 0 .55 44 0 .024 4.8 0 .83 49 0 .0047 .26 - -
email_spec27_product18_false-unreach-call_true-termination.cil.c 0 900   6200 11000 0 .52 41 0 .026 4.9 0 .87 50 0 .0042 .26 - -
email_spec27_product19_false-unreach-call_true-termination.cil.c 0 900   5400 11000 0 .53 43 0 .020 4.9 0 .85 50 0 .0037 .34 - -
email_spec27_product23_false-unreach-call_true-termination.cil.c 0 900   5400 12000 0 .55 43 0 .018 4.9 0 .80 48 0 .0017 .35 - -
email_spec27_product24_false-unreach-call_true-termination.cil.c 0 900   5900 12000 0 .53 43 0 .050 4.9 0 .82 47 0 .0032 .26 - -
email_spec27_product25_false-unreach-call_true-termination.cil.c 0 900   6200 10000 0 .56 41 0 .047 4.8 0 .85 47 0 .0045 .29 - -
email_spec27_product27_false-unreach-call_true-termination.cil.c 0 900   4600 10000 0 .53 41 0 .031 4.8 0 .87 49 0 .0032 .26 - -
email_spec27_product29_false-unreach-call_true-termination.cil.c 0 900   4700 11000 0 .57 44 0 .049 4.9 0 .82 49 0 .0035 .30 - -
email_spec27_product30_false-unreach-call_true-termination.cil.c 0 900   6000 11000 0 .56 44 0 .023 4.8 0