Tool CPAchecker 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-05 07:52:24 CET 2017-12-05 13:10:09 CET 2017-12-05 13:34:02 CET 2017-12-05 13:37:41 CET 2017-12-05 13:41:35 CET 2017-12-05 12:37:13 CET 2017-12-05 13:13:01 CET
Run set interpchecker.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.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   3900 13000 0 .41 43 0 .024 4.9 0 .82 47 0 .0035 .29 - -
elevator_spec14_product24_false-unreach-call_true-termination.cil.c 0 900   4200 13000 0 .53 44 0 .048 4.9 0 .83 49 0 .0012 .30 - -
elevator_spec14_product28_false-unreach-call_true-termination.cil.c 0 910   4300 11000 0 .52 41 0 .040 4.9 0 .85 50 0 .0035 .34 - -
elevator_spec14_product32_false-unreach-call_true-termination.cil.c 0 900   4000 11000 0 .49 41 0 .023 4.9 0 .87 49 0 .0031 .34 - -
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c 0 900   4200 12000 0 .56 44 0 .022 5.0 0 .84 49 0 .0013 .30 - -
elevator_spec1_product18_false-unreach-call_true-termination.cil.c 0 960   8100 9500 0 .55 43 0 .025 4.9 0 .84 49 0 .0042 .26 - -
elevator_spec1_product20_false-unreach-call_true-termination.cil.c 0 970   9200 9400 0 .58 41 0 .024 4.9 0 .84 47 0 .0040 .26 - -
elevator_spec1_product22_false-unreach-call_true-termination.cil.c 0 970   8900 10000 0 .55 43 0 .018 5.0 0 .82 49 0 .0012 .32 - -
elevator_spec1_product24_false-unreach-call_true-termination.cil.c 0 960   10000 9500 0 .51 41 0 .032 4.8 0 .86 49 0 .0029 .32 - -
elevator_spec1_product26_false-unreach-call_true-termination.cil.c 0 970   8100 8600 0 .53 41 0 .018 4.8 0 .95 50 0 .0047 .26 - -
elevator_spec1_product28_false-unreach-call_true-termination.cil.c 0 970   9600 8900 0 .51 43 0 .047 4.9 0 .86 49 0 .0036 .34 - -
elevator_spec1_product30_false-unreach-call_true-termination.cil.c 0 960   8200 9600 0 .54 44 0 .048 4.9 0 .85 49 0 .0044 .26 - -
elevator_spec1_product32_false-unreach-call_true-termination.cil.c 0 920   8800 9400 0 .53 43 0 .047 5.0 0 .90 49 0 .0037 .31 - -
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c 0 970   7400 10000 0 .50 41 0 .019 4.9 0 .86 47 0 .0041 .35 - -
elevator_spec2_product18_false-unreach-call_true-termination.cil.c 0 900   3500 13000 0 .53 41 0 .040 4.9 0 .81 47 0 .0040 .30 - -
elevator_spec2_product20_false-unreach-call_true-termination.cil.c 0 900   3600 12000 0 .52 41 0 .044 4.9 0 .84 49 0 .0041 .34 - -
elevator_spec2_product22_false-unreach-call_true-termination.cil.c 0 900   3600 11000 0 .56 41 0 .052 4.8 0 .84 49 0 .0037 .35 - -
elevator_spec2_product24_false-unreach-call_true-termination.cil.c 0 900   3800 14000 0 .53 41 0 .047 4.9 0 .89 48 0 .0040 .26 - -
elevator_spec2_product26_false-unreach-call_true-termination.cil.c 0 900   3100 11000 0 .52 43 0 .024 4.9 0 .79 53 0 .0037 .33 - -
elevator_spec2_product28_false-unreach-call_true-termination.cil.c 0 900   3900 12000 0 .52 44 0 .018 4.9 0 .84 49 0 .0019 .26 - -
elevator_spec2_product30_false-unreach-call_true-termination.cil.c 0 900   3800 13000 0 .54 43 0 .047 4.8 0 .82 47 0 .0036 .32 - -
elevator_spec2_product32_false-unreach-call_true-termination.cil.c 0 900   3700 11000 0 .50 42 0 .045 4.9 0 .85 49 0 .0041 .34 - -
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c 0 950   8000 8900 0 .55 42 0 .018 4.9 0 .85 50 0 .0049 .28 - -
elevator_spec3_product03_false-unreach-call_true-termination.cil.c 0 940   6500 11000 0 .53 41 0 .018 4.9 0 .83 47 0 .0017 .34 - -
elevator_spec3_product11_false-unreach-call_true-termination.cil.c 0 940   6700 11000 0 .52 42 0 .047 4.9 0 .86 51 0 .0039 .33 - -
elevator_spec3_product19_false-unreach-call_true-termination.cil.c 0 940   7300 11000 0 .53 43 0 .025 4.8 0 .81 49 0 .0035 .31 - -
elevator_spec3_product20_false-unreach-call_true-termination.cil.c 0 940   6400 12000 0 .54 41 0 .037 4.9 0 .84 49 0 .0047 .26 - -
elevator_spec3_product23_false-unreach-call_true-termination.cil.c 0 940   6900 10000 0 .51 44 0 .024 4.8 0 .85 51 0 .0015 .31 - -
elevator_spec3_product24_false-unreach-call_true-termination.cil.c 0 930   6300 10000 0 .56 42 0 .047 5.0 0 .84 48 0 .0034 .32 - -
elevator_spec3_product27_false-unreach-call_true-termination.cil.c 0 940   7100 11000 0 .55 41 0 .023 4.8 0 .85 49 0 .0053 .26 - -
elevator_spec3_product28_false-unreach-call_true-termination.cil.c 0 930   6500 9800 0 .55 41 0 .019 4.8 0 .80 49 0 .0036 .31 - -
elevator_spec3_product31_false-unreach-call_true-termination.cil.c 0 940   6700 11000 0 .55 43 0 .018 5.0 0 .83 49 0 .0040 .31 - -
elevator_spec3_product32_false-unreach-call_true-termination.cil.c 0 940   7300 9600 0 .55 41 0 .049 4.8 0 .84 49 0 .0041 .35 - -
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c 0 910   6500 10000 0 .55 45 0 .018 4.9 0 .84 47 0 .0036 .34 - -
elevator_spec9_product26_false-unreach-call_true-termination.cil.c 0 900   4200 12000 0 .52 43 0 .019 4.9 0 .84 49 0 .0020 .31 - -
elevator_spec9_product28_false-unreach-call_true-termination.cil.c 0 920   5000 14000 0 .53 41 0 .048 4.9 0 .86 48 0 .0033 .30 - -
elevator_spec9_product30_false-unreach-call_true-termination.cil.c 0 910   4600 13000 0 .56 42 0 .019 4.8 0 .84 50 0 .0041 .30 - -
elevator_spec9_product32_false-unreach-call_true-termination.cil.c 0 970   6100 11000 0 .52 41 0 .036 4.9 0 .83 49 0 .0041 .34 - -
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c 0 970   9000 11000 0 .55 45 0 .044 5.0 0 .79 49 0 .0041 .34 - -
elevator_spec13_product21_true-unreach-call_false-termination.cil.c 0 900   4000 11000 - - - - 0 .69 41 0 .049 5.0
elevator_spec13_product22_true-unreach-call_false-termination.cil.c 0 900   4000 11000 - - - - 0 .54 42 0 .018 4.9
elevator_spec13_product23_true-unreach-call_false-termination.cil.c 0 900   4000 12000 - - - - 0 .63 43 0 .026 4.9
elevator_spec13_product24_true-unreach-call_false-termination.cil.c 0 900   4100 13000 - - - - 0 .54 42 0 .019 4.9
elevator_spec13_product29_true-unreach-call_false-termination.cil.c 0 900   3900 11000 - - - - 0 .64 41 0 .021 4.9
elevator_spec13_product30_true-unreach-call_false-termination.cil.c 0 900   4000 12000 - - - - 0 .68 43 0 .018 4.8
elevator_spec13_product31_true-unreach-call_false-termination.cil.c 0 900   4000 11000 - - - - 0 .52 43 0 .046 4.9
elevator_spec13_product32_true-unreach-call_false-termination.cil.c 0 900   4000 14000 - - - - 0 .58 41 0 .017 4.8
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c 0 900   4400 13000 - - - - 0 .59 43 0 .044 4.9
elevator_spec14_product03_true-unreach-call_true-termination.cil.c 0 900   4000 13000 - - - - 0 .58 43 0 .018 4.9
elevator_spec14_product11_true-unreach-call_true-termination.cil.c 0 900   3700 11000 - - - - 0 .53 43 0 .018 4.9
elevator_spec14_product19_true-unreach-call_true-termination.cil.c 0 900   4000 13000 - - - - 0 .54 43 0 .021 4.9
elevator_spec14_product23_true-unreach-call_true-termination.cil.c 0 900   4000 11000 - - - - 0 .52 42 0 .046 4.9
elevator_spec14_product27_true-unreach-call_true-termination.cil.c 0 900   3400 12000 - - - - 0 .67 41 0 .018 4.9
elevator_spec14_product31_true-unreach-call_true-termination.cil.c 0 900   4000 11000 - - - - 0 .53 44 0 .019 4.9
elevator_spec1_product01_true-unreach-call_true-termination.cil.c 0 960   8600 9600 - - - - 0 .65 44 0 .019 4.9
elevator_spec1_product03_true-unreach-call_true-termination.cil.c 0 970   8100 9400 - - - - 0 .71 41 0 .024 4.8
elevator_spec1_product09_true-unreach-call_true-termination.cil.c 0 960   8400 8800 - - - - 0 .56 41 0 .018 4.9
elevator_spec1_product11_true-unreach-call_true-termination.cil.c 0 970   8200 9800 - - - - 0 .62 42 0 .024 4.8
elevator_spec1_product17_true-unreach-call_true-termination.cil.c 0 960   10000 9000 - - - - 0 .58 41 0 .049 4.8
elevator_spec1_product19_true-unreach-call_true-termination.cil.c 0 970   8300 8700 - - - - 0 .55 43 0 .019 4.9
elevator_spec1_product21_true-unreach-call_true-termination.cil.c 0 920   8900 10000 - - - - 0 .62 41 0 .018 4.8
elevator_spec1_product23_true-unreach-call_true-termination.cil.c 0 970   8400 9500 - - - - 0 .56 44 0 .026 4.8
elevator_spec1_product25_true-unreach-call_true-termination.cil.c 0 960   9400 10000 - - - - 0 .54 41 0 .050 4.8
elevator_spec1_product27_true-unreach-call_true-termination.cil.c 0 970   8300 9100 - - - - 0 .64 41 0 .050 4.8
elevator_spec1_product29_true-unreach-call_true-termination.cil.c 0 960   8700 8100 - - - - 0 .55 41 0 .018 4.9
elevator_spec1_product31_true-unreach-call_true-termination.cil.c 0 970   8600 9100 - - - - 0 .59 43 0 .017 5.0
elevator_spec2_product01_true-unreach-call_true-termination.cil.c 0 910   3800 12000 - - - - 0 .50 41 0 .018 4.8
elevator_spec2_product03_true-unreach-call_true-termination.cil.c 0 920   5000 14000 - - - - 0 .51 43 0 .023 4.9
elevator_spec2_product09_true-unreach-call_true-termination.cil.c 0 910   3800 13000 - - - - 0 .61 41 0 .024 4.8
elevator_spec2_product11_true-unreach-call_true-termination.cil.c 0 920   5000 14000 - - - - 0 .64 42 0 .018 4.9
elevator_spec2_product17_true-unreach-call_true-termination.cil.c 0 900   3800 13000 - - - - 0 .72 42 0 .018 4.8
elevator_spec2_product19_true-unreach-call_true-termination.cil.c 0 900   3600 11000 - - - - 0 .67 42 0 .018 5.0
elevator_spec2_product21_true-unreach-call_true-termination.cil.c 0 900   3400 11000 - - - - 0 .68 41 0 .028 4.8
elevator_spec2_product23_true-unreach-call_true-termination.cil.c 0 900   3700 13000 - - - - 0 .60 43 0 .017 4.9
elevator_spec2_product25_true-unreach-call_true-termination.cil.c 0 900   3700 11000 - - - - 0 .71 44 0 .024 4.8
elevator_spec2_product27_true-unreach-call_true-termination.cil.c 0 900   3100 14000 - - - - 0 .54 41 0 .018 5.0
elevator_spec2_product29_true-unreach-call_true-termination.cil.c 0 900   3700 14000 - - - - 0 .53 44 0 .024 4.8
elevator_spec2_product31_true-unreach-call_true-termination.cil.c 0 900   3700 11000 - - - - 0 .71 41 0 .018 4.8
elevator_spec3_product01_true-unreach-call_true-termination.cil.c 0 940   7000 11000 - - - - 0 .63 43 0 .017 4.8
elevator_spec3_product09_true-unreach-call_true-termination.cil.c 0 940   6900 10000 - - - - 0 .72 44 0 .021 5.0
elevator_spec3_product17_true-unreach-call_true-termination.cil.c 0 970   7200 9800 - - - - 0 .58 43 0 .025 4.9
elevator_spec3_product18_true-unreach-call_true-termination.cil.c 0 930   7600 10000 - - - - 0 .62 43 0 .025 4.9
elevator_spec3_product21_true-unreach-call_true-termination.cil.c 0 940   6800 9800 - - - - 0 .70 41 0 .030 4.8
elevator_spec3_product22_true-unreach-call_true-termination.cil.c 0 940   6900 9500 - - - - 0 .53 43 0 .019 4.9
elevator_spec3_product25_true-unreach-call_true-termination.cil.c 0 940   7900 11000 - - - - 0 .58 44 0 .045 4.8
elevator_spec3_product26_true-unreach-call_true-termination.cil.c 0 940   7000 10000 - - - - 0 .52 42 0 .047 4.9
elevator_spec3_product29_true-unreach-call_true-termination.cil.c 0 960   7300 12000 - - - - 0 .53 43 0 .022 4.9
elevator_spec3_product30_true-unreach-call_true-termination.cil.c 0 940   6900 11000 - - - - 0 .54 44 0 .032 4.8
elevator_spec9_product09_true-unreach-call_true-termination.cil.c 0 900   4000 11000 - - - - 0 .61 43 0 .017 5.0
elevator_spec9_product11_true-unreach-call_true-termination.cil.c 0 910   4600 10000 - - - - 0 .67 43 0 .022 4.8
elevator_spec9_product25_true-unreach-call_true-termination.cil.c 0 910   4100 12000 - - - - 0 .65 43 0 .025 4.9
elevator_spec9_product27_true-unreach-call_true-termination.cil.c 0 930   4900 13000 - - - - 0 .69 44 0 .018 4.8
elevator_spec9_product29_true-unreach-call_true-termination.cil.c 0 910   4500 10000 - - - - 0 .64 41 0 .026 4.9
elevator_spec9_product31_true-unreach-call_true-termination.cil.c 0 960   7000 11000 - - - - 0 .60 41 0 .022 4.9
email_spec0_product16_false-unreach-call_true-termination.cil.c 0 900   4800 9600 0 .54 42 0 .047 4.8 0 .82 49 0 .0043 .36 - -
email_spec0_product21_false-unreach-call_true-termination.cil.c 0 900   4800 12000 0 .50 41 0 .019 4.8 0 .84 49 0 .0039 .29 - -
email_spec0_product22_false-unreach-call_true-termination.cil.c 0 900   4600 12000 0 .55 42 0 .049 4.8 0 .85 48 0 .0044 .26 - -
email_spec0_product26_false-unreach-call_true-termination.cil.c 0 900   4700 11000 0 .52 43 0 .018 4.9 0 .85 49 0 .0041 .32 - -
email_spec0_product31_false-unreach-call_true-termination.cil.c 0 900   5600 11000 0 .50 41 0 .023 4.8 0 .83 49 0 .0035 .32 - -
email_spec0_product33_false-unreach-call_true-termination.cil.c 0 900   5500 9200 0 .55 43 0 .019 4.8 0 .84 49 0 .0043 .26 - -
email_spec0_product34_false-unreach-call_true-termination.cil.c 0 900   5400 12000 0 .54 43 0 .018 4.9 0 .84 50 0 .0034 .31 - -
email_spec0_product35_false-unreach-call_true-termination.cil.c 0 900   5600 11000 0 .51 41 0 .035 4.9 0 .85 49 0 .0020 .26 - -
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c 0 910   5900 11000 0 .55 42 0 .047 4.9 0 .88 49 0 .0036 .31 - -
email_spec11_product15_false-unreach-call_true-termination.cil.c 0 900   4300 13000 0 .53 41 0 .047 4.8 0 .90 49 0 .0038 .32 - -
email_spec11_product20_false-unreach-call_true-termination.cil.c 0 900   4500 10000 0 .57 43 0 .017 4.9 0 .84 51 0 .0038 .35 - -
email_spec11_product22_false-unreach-call_true-termination.cil.c 0 900   4500 12000 0 .53 41 0 .018 4.9 0 .84 49 0 .0040 .31 - -
email_spec11_product26_false-unreach-call_true-termination.cil.c 0 900   4500 11000 0 .57 43 0 .021 4.8 0 .81 50 0 .0043 .31 - -
email_spec11_product30_false-unreach-call_true-termination.cil.c 0 900   4400 12000 0 .54 44 0 .025 4.9 0 .84 50 0 .0041 .34 - -
email_spec11_product32_false-unreach-call_true-termination.cil.c 0 900   4700 9900 0 .54 44 0 .021 4.9 0 .86 49 0 .0041 .35 - -
email_spec11_product33_false-unreach-call_true-termination.cil.c 0 900   4800 11000 0 .53 43 0 .050 4.8 0 .87 49 0 .0042 .26 - -
email_spec11_product35_false-unreach-call_true-termination.cil.c 0 900   4900 10000 0 .53 44 0 .022 4.9 0 .87 49 0 .0040 .34 - -
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c 0 910   5900 11000 0 .55 46 0 .019 4.8 0 .85 49 0 .0037 .31 - -
email_spec1_product14_false-unreach-call_true-termination.cil.c 0 900   5000 11000 0 .51 44 0 .025 4.8 0 .88 49 0 .0017 .29 - -
email_spec1_product15_false-unreach-call_true-termination.cil.c 0 900   4900 12000 0 .55 43 0 .022 4.8 0 .83 50 0 .0037 .34 - -
email_spec1_product16_false-unreach-call_true-termination.cil.c 0 900   5600 10000 0 .51 43 0 .046 4.8 0 .82 49 0 .0041 .29 - -
email_spec1_product20_false-unreach-call_true-termination.cil.c 0 900   4900 11000 0 .51 43 0 .023 4.8 0 .81 47 0 .0036 .32 - -
email_spec1_product21_false-unreach-call_true-termination.cil.c 0 910   5700 11000 0 .54 44 0 .048 4.8 0 .84 47 0 .0029 .29 - -
email_spec1_product22_false-unreach-call_true-termination.cil.c 0 900   4900 11000 0 .55 43 0 .022 4.9 0 .84 48 0 .0041 .33 - -
email_spec1_product26_false-unreach-call_true-termination.cil.c 0 900   4800 12000 0 .55 43 0 .031 4.9 0 .89 49 0 .0046 .29 - -
email_spec1_product29_false-unreach-call_true-termination.cil.c 0 900   5500 11000 0 .52 41 0 .046 5.0 0 .83 47 0 .0041 .32 - -
email_spec1_product30_false-unreach-call_true-termination.cil.c 0 930   5700 12000 0 .55 43 0 .018 5.0 0 .88 50 0 .0037 .31 - -
email_spec1_product31_false-unreach-call_true-termination.cil.c 0 910   5900 11000 0 .54 41 0 .048 4.8 0 .85 51 0 .0037 .34 - -
email_spec1_product32_false-unreach-call_true-termination.cil.c 0 900   5500 11000 0 .52 44 0 .047 4.9 0 .84 47 0 .0040 .26 - -
email_spec1_product33_false-unreach-call_true-termination.cil.c 0 900   5600 13000 0 .51 42 0 .021 4.9 0 .85 49 0 .0036 .34 - -
email_spec1_product34_false-unreach-call_true-termination.cil.c 0 910   5900 10000 0 .55 45 0 .022 4.9 0 .86 49 0 .0040 .31 - -
email_spec1_product35_false-unreach-call_true-termination.cil.c 0 930   5900 10000 0 .55 41 0 .025 4.8 0 .85 49 0 .0039 .33 - -
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c 0 910   6400 10000 0 .54 43 0 .023 4.9 0 .85 47 0 .0016 .26 - -
email_spec27_product17_false-unreach-call_true-termination.cil.c 0 900   4500 14000 0 .51 41 0 .018 4.9 0 .84 49 0 .0037 .34 - -
email_spec27_product18_false-unreach-call_true-termination.cil.c 0 900   4300 13000 0 .54 43 0 .038 4.8 0 .82 47 0 .0042 .31 - -
email_spec27_product19_false-unreach-call_true-termination.cil.c 0 900   4700 13000 0 .54 43 0 .019 4.8 0 .82 49 0 .0035 .32 - -
email_spec27_product23_false-unreach-call_true-termination.cil.c 0 900   4400 12000 0 .53 43 0 .023 4.9 0 .88 49 0 .0037 .31 - -
email_spec27_product24_false-unreach-call_true-termination.cil.c 0 900   4400 12000 0 .53 41 0 .034 4.9 0 .82 49 0 .0046 .30 - -
email_spec27_product25_false-unreach-call_true-termination.cil.c 0 900   4500 11000 0 .53 43 0 .049 4.9 0 .84 49 0 .0011 .34 - -
email_spec27_product27_false-unreach-call_true-termination.cil.c 0 900   4400 11000 0 .53 43 0 .018 5.0 0 .87 47 0 .0045 .26 - -
email_spec27_product29_false-unreach-call_true-termination.cil.c 0 900   4500 11000 0 .53 43 0 .019 4.8 0 .78 47 0