Tool ULTIMATE Kojak 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] 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 02:33:02 CET 2017-12-03 03:22:18 CET 2017-12-03 03:55:21 CET 2017-12-03 04:22:06 CET 2017-12-03 04:36:43 CET 2017-12-03 00:36:56 CET 2017-12-03 03:32:10 CET
Run set ukojak.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/ukojak.2017-12-02_0233.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   3300 11000 0 .55 41 0 .019 4.9 0 1.0  49 0 .0012 .32 - -
elevator_spec14_product24_false-unreach-call_true-termination.cil.c 0 900   2800 11000 0 .41 44 0 .020 4.9 0 .88 49 0 .0020 .35 - -
elevator_spec14_product28_false-unreach-call_true-termination.cil.c 0 900   2800 15000 0 .56 44 0 .020 4.9 0 .84 50 0 .0013 .26 - -
elevator_spec14_product32_false-unreach-call_true-termination.cil.c 0 900   2800 12000 0 .54 41 0 .026 4.8 0 1.0  49 0 .0012 .36 - -
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c 0 900   2500 15000 0 .53 43 0 .024 4.8 0 1.1  47 0 .0013 .26 - -
elevator_spec1_product18_false-unreach-call_true-termination.cil.c 0 900   3300 13000 0 .56 44 0 .026 4.8 0 1.2  51 0 .0012 .26 - -
elevator_spec1_product20_false-unreach-call_true-termination.cil.c 0 900   3200 13000 0 .69 41 0 .022 5.0 0 .80 49 0 .0016 .29 - -
elevator_spec1_product22_false-unreach-call_true-termination.cil.c 0 900   3100 12000 0 .54 45 0 .025 4.8 0 1.1  49 0 .0015 .26 - -
elevator_spec1_product24_false-unreach-call_true-termination.cil.c 0 900   3100 11000 0 .65 42 0 .024 5.0 0 1.0  50 0 .0020 .26 - -
elevator_spec1_product26_false-unreach-call_true-termination.cil.c 0 900   2900 14000 0 .55 43 0 .036 4.9 0 1.0  49 0 .0020 .29 - -
elevator_spec1_product28_false-unreach-call_true-termination.cil.c 0 900   4600 11000 0 .70 42 0 .018 4.8 0 .90 49 0 .0015 .34 - -
elevator_spec1_product30_false-unreach-call_true-termination.cil.c 0 900   3700 14000 0 .52 42 0 .035 4.9 0 .95 47 0 .0016 .27 - -
elevator_spec1_product32_false-unreach-call_true-termination.cil.c 0 900   3100 12000 0 .63 41 0 .021 4.9 0 1.1  48 0 .0014 .27 - -
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c 0 900   4300 13000 0 .52 41 0 .021 4.9 0 .97 49 0 .0015 .32 - -
elevator_spec2_product18_false-unreach-call_true-termination.cil.c 0 900   5400 12000 0 .58 42 0 .021 4.9 0 1.0  47 0 .0013 .27 - -
elevator_spec2_product20_false-unreach-call_true-termination.cil.c 0 900   5700 12000 0 .55 43 0 .018 4.9 0 1.1  50 0 .0018 .29 - -
elevator_spec2_product22_false-unreach-call_true-termination.cil.c 0 900   3400 15000 0 .53 43 0 .019 4.8 0 1.0  49 0 .0015 .32 - -
elevator_spec2_product24_false-unreach-call_true-termination.cil.c 0 900   3700 13000 0 .52 41 0 .018 4.8 0 1.0  49 0 .0022 .26 - -
elevator_spec2_product26_false-unreach-call_true-termination.cil.c 0 900   4700 14000 0 .51 44 0 .018 4.8 0 .81 47 0 .0017 .29 - -
elevator_spec2_product28_false-unreach-call_true-termination.cil.c 0 900   4400 13000 0 .53 42 0 .018 4.9 0 1.2  51 0 .0018 .29 - -
elevator_spec2_product30_false-unreach-call_true-termination.cil.c 0 900   4800 12000 0 .50 41 0 .023 4.8 0 .87 49 0 .0015 .29 - -
elevator_spec2_product32_false-unreach-call_true-termination.cil.c 0 900   3700 15000 0 .57 43 0 .027 4.8 0 1.1  49 0 .0017 .29 - -
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c 0 900   1500 16000 0 .58 43 0 .018 4.8 0 .88 48 0 .0014 .27 - -
elevator_spec3_product03_false-unreach-call_true-termination.cil.c 0 900   1600 10000 0 .52 41 0 .023 5.0 0 .83 48 0 .0017 .26 - -
elevator_spec3_product11_false-unreach-call_true-termination.cil.c 0 900   2900 11000 0 .54 43 0 .019 4.9 0 1.1  47 0 .0016 .34 - -
elevator_spec3_product19_false-unreach-call_true-termination.cil.c 0 900   2900 14000 0 .67 44 0 .024 4.9 0 1.1  49 0 .0015 .27 - -
elevator_spec3_product20_false-unreach-call_true-termination.cil.c 0 900   5400 12000 0 .51 41 0 .018 4.8 0 .94 47 0 .0016 .29 - -
elevator_spec3_product23_false-unreach-call_true-termination.cil.c 0 900   2500 12000 0 .52 43 0 .024 4.8 0 1.1  50 0 .0017 .29 - -
elevator_spec3_product24_false-unreach-call_true-termination.cil.c 0 900   5400 13000 0 .57 42 0 .024 5.0 0 1.1  49 0 .0015 .26 - -
elevator_spec3_product27_false-unreach-call_true-termination.cil.c 0 900   2900 11000 0 .53 43 0 .020 4.8 0 .82 48 0 .0020 .29 - -
elevator_spec3_product28_false-unreach-call_true-termination.cil.c 0 900   5400 14000 0 .55 44 0 .021 5.0 0 .99 49 0 .0015 .34 - -
elevator_spec3_product31_false-unreach-call_true-termination.cil.c 0 900   2500 12000 0 .39 40 0 .020 5.0 0 1.1  50 0 .0014 .34 - -
elevator_spec3_product32_false-unreach-call_true-termination.cil.c 0 900   5400 14000 0 .54 41 0 .022 5.0 0 1.1  48 0 .0016 .26 - -
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c 0 900   3100 12000 0 .59 43 0 .018 4.8 0 .88 49 0 .0040 .26 - -
elevator_spec9_product26_false-unreach-call_true-termination.cil.c 0 900   4500 15000 0 .54 41 0 .019 5.0 0 .82 50 0 .0016 .26 - -
elevator_spec9_product28_false-unreach-call_true-termination.cil.c 0 900   5200 11000 0 .51 43 0 .022 4.8 0 1.0  48 0 .0014 .29 - -
elevator_spec9_product30_false-unreach-call_true-termination.cil.c 0 900   4900 13000 0 .54 41 0 .023 4.9 0 .90 47 0 .0018 .29 - -
elevator_spec9_product32_false-unreach-call_true-termination.cil.c 0 900   2600 12000 0 .55 43 0 .019 4.8 0 .97 49 0 .0016 .26 - -
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c 0 900   1500 13000 0 .53 43 0 .038 4.9 0 1.1  49 0 .0015 .30 - -
elevator_spec13_product21_true-unreach-call_false-termination.cil.c 0 900   2600 15000 - - - - 0 .52 41 0 .020 4.9
elevator_spec13_product22_true-unreach-call_false-termination.cil.c 0 900   2000 14000 - - - - 0 .66 43 0 .019 4.9
elevator_spec13_product23_true-unreach-call_false-termination.cil.c 0 900   2500 11000 - - - - 0 .59 43 0 .022 4.8
elevator_spec13_product24_true-unreach-call_false-termination.cil.c 0 900   2300 11000 - - - - 0 .55 43 0 .020 5.0
elevator_spec13_product29_true-unreach-call_false-termination.cil.c 0 900   2500 11000 - - - - 0 .53 44 0 .020 4.8
elevator_spec13_product30_true-unreach-call_false-termination.cil.c 0 900   2200 11000 - - - - 0 .62 44 0 .019 4.9
elevator_spec13_product31_true-unreach-call_false-termination.cil.c 0 900   2500 13000 - - - - 0 .64 41 0 .020 4.9
elevator_spec13_product32_true-unreach-call_false-termination.cil.c 0 900   2300 9900 - - - - 0 .65 41 0 .022 4.8
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c 0 900   2400 11000 - - - - 0 .55 45 0 .020 4.9
elevator_spec14_product03_true-unreach-call_true-termination.cil.c 0 900   3100 12000 - - - - 0 .57 43 0 .021 4.8
elevator_spec14_product11_true-unreach-call_true-termination.cil.c 0 900   1500 14000 - - - - 0 .68 42 0 .020 4.9
elevator_spec14_product19_true-unreach-call_true-termination.cil.c 0 900   2400 13000 - - - - 0 .63 41 0 .018 5.0
elevator_spec14_product23_true-unreach-call_true-termination.cil.c 0 900   2600 12000 - - - - 0 .62 44 0 .018 4.8
elevator_spec14_product27_true-unreach-call_true-termination.cil.c 0 900   1800 12000 - - - - 0 .58 43 0 .019 4.8
elevator_spec14_product31_true-unreach-call_true-termination.cil.c 0 900   2600 11000 - - - - 0 .55 41 0 .018 4.9
elevator_spec1_product01_true-unreach-call_true-termination.cil.c 0 900   3200 12000 - - - - 0 .50 42 0 .018 4.9
elevator_spec1_product03_true-unreach-call_true-termination.cil.c 0 900   2500 14000 - - - - 0 .70 43 0 .017 4.8
elevator_spec1_product09_true-unreach-call_true-termination.cil.c 0 900   2500 13000 - - - - 0 .55 43 0 .022 4.8
elevator_spec1_product11_true-unreach-call_true-termination.cil.c 0 900   2900 10000 - - - - 0 .53 41 0 .019 4.8
elevator_spec1_product17_true-unreach-call_true-termination.cil.c 0 900   2100 12000 - - - - 0 .69 41 0 .020 4.8
elevator_spec1_product19_true-unreach-call_true-termination.cil.c 0 900   2900 11000 - - - - 0 .52 43 0 .018 5.0
elevator_spec1_product21_true-unreach-call_true-termination.cil.c 0 900   2200 14000 - - - - 0 .57 41 0 .019 4.8
elevator_spec1_product23_true-unreach-call_true-termination.cil.c 0 900   2700 14000 - - - - 0 .55 43 0 .018 4.8
elevator_spec1_product25_true-unreach-call_true-termination.cil.c 0 900   3600 13000 - - - - 0 .60 44 0 .017 5.0
elevator_spec1_product27_true-unreach-call_true-termination.cil.c 0 900   3300 11000 - - - - 0 .64 43 0 .019 4.9
elevator_spec1_product29_true-unreach-call_true-termination.cil.c 0 900   3000 13000 - - - - 0 .69 46 0 .018 4.8
elevator_spec1_product31_true-unreach-call_true-termination.cil.c 0 900   2700 12000 - - - - 0 .62 42 0 .020 4.9
elevator_spec2_product01_true-unreach-call_true-termination.cil.c 0 900   2900 12000 - - - - 0 .61 43 0 .018 4.8
elevator_spec2_product03_true-unreach-call_true-termination.cil.c 0 900   4500 13000 - - - - 0 .67 43 0 .020 5.0
elevator_spec2_product09_true-unreach-call_true-termination.cil.c 0 900   3400 9600 - - - - 0 .54 43 0 .019 4.8
elevator_spec2_product11_true-unreach-call_true-termination.cil.c 0 900   3700 12000 - - - - 0 .64 43 0 .020 4.9
elevator_spec2_product17_true-unreach-call_true-termination.cil.c 0 900   3200 11000 - - - - 0 .68 46 0 .019 5.0
elevator_spec2_product19_true-unreach-call_true-termination.cil.c 0 900   5300 11000 - - - - 0 .56 43 0 .018 4.8
elevator_spec2_product21_true-unreach-call_true-termination.cil.c 0 900   3400 11000 - - - - 0 .55 43 0 .020 4.8
elevator_spec2_product23_true-unreach-call_true-termination.cil.c 0 900   2400 11000 - - - - 0 .66 41 0 .020 4.9
elevator_spec2_product25_true-unreach-call_true-termination.cil.c 0 900   3700 13000 - - - - 0 .54 43 0 .020 4.8
elevator_spec2_product27_true-unreach-call_true-termination.cil.c 0 900   3100 14000 - - - - 0 .70 43 0 .021 4.8
elevator_spec2_product29_true-unreach-call_true-termination.cil.c 0 900   3000 14000 - - - - 0 .58 43 0 .018 4.9
elevator_spec2_product31_true-unreach-call_true-termination.cil.c 0 900   5300 13000 - - - - 0 .70 44 0 .018 4.8
elevator_spec3_product01_true-unreach-call_true-termination.cil.c 0 900   2700 10000 - - - - 0 .58 43 0 .020 5.0
elevator_spec3_product09_true-unreach-call_true-termination.cil.c 0 900   2800 12000 - - - - 0 .61 41 0 .020 4.8
elevator_spec3_product17_true-unreach-call_true-termination.cil.c 0 900   1900 10000 - - - - 0 .66 43 0 .020 5.0
elevator_spec3_product18_true-unreach-call_true-termination.cil.c 0 900   5300 13000 - - - - 0 .59 42 0 .019 4.8
elevator_spec3_product21_true-unreach-call_true-termination.cil.c 0 900   2600 12000 - - - - 0 .40 45 0 .018 4.9
elevator_spec3_product22_true-unreach-call_true-termination.cil.c 0 900   2300 13000 - - - - 0 .54 44 0 .019 4.8
elevator_spec3_product25_true-unreach-call_true-termination.cil.c 0 900   3300 12000 - - - - 0 .62 42 0 .017 4.8
elevator_spec3_product26_true-unreach-call_true-termination.cil.c 0 900   5200 14000 - - - - 0 .64 43 0 .019 5.0
elevator_spec3_product29_true-unreach-call_true-termination.cil.c 0 900   3600 13000 - - - - 0 .59 43 0 .019 5.0
elevator_spec3_product30_true-unreach-call_true-termination.cil.c 0 900   5300 11000 - - - - 0 .53 43 0 .019 4.8
elevator_spec9_product09_true-unreach-call_true-termination.cil.c 0 900   3500 13000 - - - - 0 .59 44 0 .020 4.9
elevator_spec9_product11_true-unreach-call_true-termination.cil.c 0 900   2800 11000 - - - - 0 .56 44 0 .017 4.9
elevator_spec9_product25_true-unreach-call_true-termination.cil.c 0 900   2900 12000 - - - - 0 .59 43 0 .020 4.8
elevator_spec9_product27_true-unreach-call_true-termination.cil.c 0 900   3200 14000 - - - - 0 .60 41 0 .018 4.8
elevator_spec9_product29_true-unreach-call_true-termination.cil.c 0 900   3700 11000 - - - - 0 .55 43 0 .020 4.9
elevator_spec9_product31_true-unreach-call_true-termination.cil.c 0 900   2300 14000 - - - - 0 .66 41 0 .017 4.9
email_spec0_product16_false-unreach-call_true-termination.cil.c 0 900   4400 12000 0 .68 41 0 .025 5.0 0 1.0  48 0 .0041 .34 - -
email_spec0_product21_false-unreach-call_true-termination.cil.c 0 900   4200 13000 0 .64 42 0 .022 4.8 0 1.1  50 0 .0017 .29 - -
email_spec0_product22_false-unreach-call_true-termination.cil.c 0 900   6200 11000 0 .65 42 0 .022 4.8 0 1.1  49 0 .0013 .26 - -
email_spec0_product26_false-unreach-call_true-termination.cil.c 0 900   5400 13000 0 .53 44 0 .019 4.8 0 1.0  49 0 .0014 .34 - -
email_spec0_product31_false-unreach-call_true-termination.cil.c 0 900   4100 12000 0 .52 41 0 .020 4.9 0 1.1  47 0 .0017 .26 - -
email_spec0_product33_false-unreach-call_true-termination.cil.c 0 900   5500 12000 0 .55 41 0 .018 5.0 0 .69 49 0 .0015 .28 - -
email_spec0_product34_false-unreach-call_true-termination.cil.c 0 900   4500 12000 0 .51 41 0 .023 4.9 0 .99 49 0 .0017 .26 - -
email_spec0_product35_false-unreach-call_true-termination.cil.c 0 900   5000 11000 0 .76 41 0 .018 4.9 0 1.1  50 0 .0021 .28 - -
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c 0 910   6500 13000 0 .55 43 0 .018 4.9 0 1.0  49 0 .0016 .28 - -
email_spec11_product15_false-unreach-call_true-termination.cil.c 0 900   6200 12000 0 .53 41 0 .019 4.9 0 1.1  49 0 .0019 .26 - -
email_spec11_product20_false-unreach-call_true-termination.cil.c 0 900   4500 14000 0 .55 43 0 .019 4.8 0 .80 47 0 .0016 .29 - -
email_spec11_product22_false-unreach-call_true-termination.cil.c 0 900   3500 13000 0 .57 43 0 .021 4.9 0 1.1  50 0 .0022 .28 - -
email_spec11_product26_false-unreach-call_true-termination.cil.c 0 900   3400 14000 0 .55 42 0 .020 5.0 0 .97 50 0 .0014 .29 - -
email_spec11_product30_false-unreach-call_true-termination.cil.c 0 900   6300 12000 0 .54 43 0 .047 4.8 0 1.1  47 0 .0014 .28 - -
email_spec11_product32_false-unreach-call_true-termination.cil.c 0 900   4500 11000 0 .63 44 0 .019 4.8 0 1.0  49 0 .0016 .26 - -
email_spec11_product33_false-unreach-call_true-termination.cil.c 0 900   4400 13000 0 .65 44 0 .024 4.9 0 1.0  49 0 .0016 .34 - -
email_spec11_product35_false-unreach-call_true-termination.cil.c 0 900   6000 14000 0 .55 43 0 .020 4.9 0 .87 50 0 .0017 .28 - -
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c 0 900   6600 11000 0 .53 41 0 .036 4.8 0 .96 49 0 .0021 .30 - -
email_spec1_product14_false-unreach-call_true-termination.cil.c 0 900   6200 12000 0 .55 43 0 .021 4.8 0 .94 50 0 .0014 .30 - -
email_spec1_product15_false-unreach-call_true-termination.cil.c 0 900   7000 12000 0 .54 43 0 .049 5.0 0 .70 49 0 .0018 .29 - -
email_spec1_product16_false-unreach-call_true-termination.cil.c 0 900   6600 11000 0 .53 41 0 .027 4.8 0 1.0  50 0 .0016 .26 - -
email_spec1_product20_false-unreach-call_true-termination.cil.c 0 900   6100 13000 0 .52 43 0 .049 4.8 0 1.1  49 0 .0015 .29 - -
email_spec1_product21_false-unreach-call_true-termination.cil.c 0 900   6400 13000 0 .55 43 0 .024 4.9 0 1.1  48 0 .0019 .28 - -
email_spec1_product22_false-unreach-call_true-termination.cil.c 0 900   6800 10000 0 .54 43 0 .024 4.8 0 .81 49 0 .0017 .32 - -
email_spec1_product26_false-unreach-call_true-termination.cil.c 0 900   6200 13000 0 .54 43 0 .019 4.9 0 1.1  50 0 .0012 .35 - -
email_spec1_product29_false-unreach-call_true-termination.cil.c 0 900   6300 12000 0 .59 45 0 .019 4.8 0 1.1  49 0 .0016 .30 - -
email_spec1_product30_false-unreach-call_true-termination.cil.c 0 900   6400 12000 0 .55 43 0 .019 4.8 0 1.1  50 0 .0016 .26 - -
email_spec1_product31_false-unreach-call_true-termination.cil.c 0 900   6200 15000 0 .56 45 0 .019 4.8 0 .82 49 0 .0017 .28 - -
email_spec1_product32_false-unreach-call_true-termination.cil.c 0 900   6100 13000 0 .52 41 0 .022 4.8 0 .82 47 0 .0017 .26 - -
email_spec1_product33_false-unreach-call_true-termination.cil.c 0 900   6600 12000 0 .54 44 0 .018 4.9 0 .99 49 0 .0016 .29 - -
email_spec1_product34_false-unreach-call_true-termination.cil.c 0 900   6100 13000 0 .51 41 0 .020 4.9 0 1.1  50 0 .0019 .29 - -
email_spec1_product35_false-unreach-call_true-termination.cil.c 0 900   6100 14000 0 .59 43 0 .023 4.8 0 .83 50 0 .0017 .28 - -
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c 0 900   6300 11000 0 .52 43 0 .018 4.8 0 .94 48 0 .0019 .35 - -
email_spec27_product17_false-unreach-call_true-termination.cil.c 0 900   3500 13000 0 .57 41 0 .019 5.0 0 1.1  47 0 .0017 .28 - -
email_spec27_product18_false-unreach-call_true-termination.cil.c 0 900   5500 12000 0 .57 44 0 .020 4.9 0 .98 47 0 .0015 .28 - -
email_spec27_product19_false-unreach-call_true-termination.cil.c 0 900   3500 13000 0 .55 44 0 .024 5.0 0 .83 49 0 .0015 .29 - -
email_spec27_product23_false-unreach-call_true-termination.cil.c 0 900   2700 12000 0 .54 42 0 .025 4.8 0 .82 47 0 .0012 .30 - -
email_spec27_product24_false-unreach-call_true-termination.cil.c 0 900   4700 12000 0 .50 41 0 .019 4.8 0 .95 50 0 .0014 .34 - -
email_spec27_product25_false-unreach-call_true-termination.cil.c 0 900   4800 12000 0 .55 43 0 .020 5.0 0 .83 47 0 .0013 .26 - -
email_spec27_product27_false-unreach-call_true-termination.cil.c 0 900   3200 14000 0 .63 46 0 .023 5.0 0 1.1  47 0 .0016 .26 - -
email_spec27_product29_false-unreach-call_true-termination.cil.c 0 900   3500 14000 0 .60 41 0 .023 5.0 0 .98 47 0 .0015 .29 - -
email_spec27_product30_false-unreach-call_true-termination.cil.c 0 900   6200 13000 0 .60 44 0 .024 4.8 0 .83 49 0 .0021 .28 - -
email_spec27_product31_false-unreach-call_true-termination.cil.c 0 900   6100 13000 0 .57 43 0 .019 5.0 0 .88 49 0 .0014 .29 - -
email_spec27_product32_false-unreach-call_true-termination.cil.c 0 900   5600 14000 0 .53 44 0 .021 4.8 0 .95 49 0 .0016 .28 - -
email_spec27_product33_false-unreach-call_true-termination.cil.c 0 900   5500 13000 0 .55 43 0 .019 4.9 0 1.1  47 0 .0015 .28 - -
email_spec27_product34_false-unreach-call_true-termination.cil.c 0 900   4900 14000 0 .42 41 0 .024 4.8 0 1.1  48 0 .0017 .25 - -
email_spec27_product35_false-unreach-call_true-termination.cil.c 0 900   4500 12000 0 .40 43 0 .023 4.9 0 .98 47 0 .0013 .31 - -
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c 0 900   6300 11000 0 .52 43 0 .021 5.0 0 1.2  49 0 .0017 .29 - -
email_spec3_product13_false-unreach-call_true-termination.cil.c 0 75   1200 870 0 .72 46 0 .027 4.9 0 1.2  47 0 .0015 .26 - -
email_spec3_product17_false-unreach-call_true-termination.cil.c 0 84   1200 830 0 .61 43 0 .025 4.9 0 1.1  47 0 .0016 .26 - -
email_spec3_product18_false-unreach-call_true-termination.cil.c 0 82   1200 790 0 .54 43 0 .018 4.8 0 1.2  49 0 .0019 .26 - -
email_spec3_product19_false-unreach-call_true-termination.cil.c 0 85   1200 850 0 .57 43 0 .018 4.9 0 .85 50 0 .0014 .26 - -
email_spec3_product23_false-unreach-call_true-termination.cil.c 0 79   1100 810 0 .54 44 0 .021 5.0 0 .89 49 0 .0014 .26 - -
email_spec3_product24_false-unreach-call_true-termination.cil.c 0 85   1200 900 0 .62 41 0 .018 5.0 0 .88 49 0 .0014 .26 - -
email_spec3_product25_false-unreach-call_true-termination.cil.c 0 87   1200 980 0 .51 43 0 .024 4.8 0 .96 48 0 .0015 .28 - -
email_spec3_product27_false-unreach-call_true-termination.cil.c 0 85   1100 930 0 .42 44 0 .025 4.9 0 1.1  47 0 .0015 .35 - -
email_spec3_product28_false-unreach-call_true-termination.cil.c 0 900   4700 12000 0 .53 43 0 .046 4.8 0 1.1  47 0 .0011 .31 - -
email_spec3_product29_false-unreach-call_true-termination.cil.c 0 900   4500 12000 0 .54 41 0 .025 4.9 0 1.1  49 0 .0017 .27 - -
email_spec3_product30_false-unreach-call_true-termination.cil.c 0 900   4500 11000 0 .58 44 0 .021 4.9 0 .69 49 0 .0015 .34 - -
email_spec3_product31_false-unreach-call_true-termination.cil.c 0 900   4000 14000 0 .53 43 0 .024 4.8 0 1.1  49 0 .0020 .26 - -
email_spec3_product32_false-unreach-call_true-termination.cil.c 0 900   4600 13000 0 .51 41 0 .025 4.8 0 1.2  49 0 .0016 .32 - -
email_spec3_product33_false-unreach-call_true-termination.cil.c 0 900   4400 13000 0 .55 44 0 .019 4.8 0 1.1  49 0 .0021 .28 - -
email_spec3_product34_false-unreach-call_true-termination.cil.c 0 900   4900 14000 0 .40 44 0 .020 4.8 0 .90 49 0 .0013 .27 - -
email_spec3_product35_false-unreach-call_true-termination.cil.c 0 900   4300 12000 0 .54 41 0 .019 4.8 0 1.1  47 0 .0012 .28 - -
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c 0 900   5000 12000 0 .51 43 0 .045 4.9 0 .96 49 0 .0015 .32 - -
email_spec4_product18_false-unreach-call_true-termination.cil.c 0 900   3700 12000 0 .41 43 0 .021 4.9 0 .69 49 0 .0019 .28 - -
email_spec4_product19_false-unreach-call_true-termination.cil.c 0 900   4400 13000 0 .52 43 0 .018 4.9 0 1.2  52 0 .0019 .28 - -
email_spec4_product23_false-unreach-call_true-termination.cil.c 0 900   6100 12000 0 .54 44 0 .019 5.0 0 .95 49 0 .0015 .26 - -
email_spec4_product24_false-unreach-call_true-termination.cil.c 0 900   3800 13000 0 .53 44 0 .018 4.8 0 .78 47 0 .0014 .26 - -
email_spec4_product25_false-unreach-call_true-termination.cil.c 0 900   5000 12000 0 .53 41 0 .025 4.8 0 1.1  49 0 .0018 .29 - -
email_spec4_product27_false-unreach-call_true-termination.cil.c 0 900   3200 11000 0 .58 41 0 .018 5.0 0 1.1  49 0 .0037 .34 - -
email_spec4_product30_false-unreach-call_true-termination.cil.c 0 900   6400 11000 0 .55 44 0 .021 4.9 0 1.2  52 0 .0017 .28 - -
email_spec4_product31_false-unreach-call_true-termination.cil.c 0 900   6400 11000 0 .53 41 0 .020 4.9 0 .82 47 0 .0017 .31 - -
email_spec4_product32_false-unreach-call_true-termination.cil.c 0 900   3500 12000 0 .54 44 0 .018 4.8 0 .92 47 0 .0016 .34 - -
email_spec4_product33_false-unreach-call_true-termination.cil.c 0 900   4900 11000 0 .59 41 0 .037 4.9 0 .90 48 0 .0014 .32 - -
email_spec4_product34_false-unreach-call_true-termination.cil.c 0 900   6400 12000 0 .52 41 0 .020 4.8 0 1.1  49 0 .0027 .34 - -
email_spec4_product35_false-unreach-call_true-termination.cil.c 0 900   4000 11000 0 .55 41 0 .025 4.8 0 .94 49 0 .0015 .32 - -
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c 0 900   4500 12000 0 .55 41 0 .026 4.8 0 1.1  47 0 .0017 .26 - -
email_spec6_product12_false-unreach-call_true-termination.cil.c 0 900   6500 12000 0 .52 41 0 .023 4.8 0 1.1  49 0 .0014 .32 - -
email_spec6_product14_false-unreach-call_true-termination.cil.c 0 900   6200 12000 0 .52 43 0 .023 4.8 0 1.0  50 0 .0016 .26 - -
email_spec6_product15_false-unreach-call_true-termination.cil.c 0 900   4100 12000 0 .52 43 0 .020 4.9 0 1.1  51 0 .0016 .26 - -
email_spec6_product16_false-unreach-call_true-termination.cil.c 0 900   6500 13000 0 .58 41 0 .024 4.9 0 1.1  47 0 .0014 .29 - -
email_spec6_product20_false-unreach-call_true-termination.cil.c 0 900   6200 14000 0 .55 42 0 .026 4.9 0 .79 47 0 .0013 .28 - -
email_spec6_product21_false-unreach-call_true-termination.cil.c 0 900   6200 15000 0 .52 41 0 .018 4.8 0 .88 47 0 .0014 .35 - -
email_spec6_product22_false-unreach-call_true-termination.cil.c 0 910   6500 13000 0 .57 43 0 .023 4.8 0 1.0  47 0 .0015 .31 - -
email_spec6_product26_false-unreach-call_true-termination.cil.c 0 900   6000 12000 0 .53 43 0 .018 5.0 0 .93 51 0 .0037 .33 - -
email_spec6_product28_false-unreach-call_true-termination.cil.c 0 900   6400 10000 0 .56 43 0 .022 5.0 0 1.2  47 0 .0017 .27 - -
email_spec6_product29_false-unreach-call_true-termination.cil.c 0 900   6000 14000 0 .61 44 0 .019 4.8 0 .98 47 0 .0017 .28 - -
email_spec6_product30_false-unreach-call_true-termination.cil.c 0 900   6300 12000 0 .53 43 0 .019 4.9 0 1.1  50 0 .0019 .27 - -
email_spec6_product31_false-unreach-call_true-termination.cil.c 0 900   6600 12000 0 .55 41 0 .025 5.0 0 .78 47 0 .0017 .26 - -
email_spec6_product32_false-unreach-call_true-termination.cil.c 0 900   5900 11000 0 .60 43 0 .018 4.9 0 1.1  49 0 .0012 .27 - -
email_spec6_product33_false-unreach-call_true-termination.cil.c 0 900   6300 13000 0 .54 42 0 .020 4.9 0 1.1  51 0 .0015 .28 - -
email_spec6_product34_false-unreach-call_true-termination.cil.c 0 900   5900 15000 0 .59 45 0 .025 4.8 0 1.1  49 0 .0017 .28 - -
email_spec6_product35_false-unreach-call_true-termination.cil.c 0 900   6100 12000 0 .55 41 0 .025 4.9 0 1.1  47 0 .0017 .26 - -
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c 0 900   6300 13000 0 .56 43 0 .023 4.8 0 .89 49 0 .0012 .29 - -
email_spec7_product28_false-unreach-call_true-termination.cil.c 0 900   4800 12000 0 .56 41 0 .023 4.9 0 1.0  49 0 .0014 .29 - -
email_spec7_product29_false-unreach-call_true-termination.cil.c 0 900   4300 14000 0 .54 43 0 .019 4.8 0 .98 50 0 .0020 .28 - -
email_spec7_product30_false-unreach-call_true-termination.cil.c 0 900   4900 14000 0 .58 43 0 .019 5.0 0 .92 50 0 .0015 .26 - -
email_spec7_product31_false-unreach-call_true-termination.cil.c 0 900   6200 15000 0 .57 44 0 .024 4.9 0 .95 47 0 .0016 .29 - -
email_spec7_product32_false-unreach-call_true-termination.cil.c 0 900   5000 12000 0 .56 43 0 .023 4.9 0 1.1  49 0 .0013 .27 - -
email_spec7_product33_false-unreach-call_true-termination.cil.c 0 900   4800 11000 0 .55 43 0 .021 4.9 0 1.1  51 0 .0016 .32 - -
email_spec7_product34_false-unreach-call_true-termination.cil.c 0 900   6200 12000 0 .55 43 0 .020 4.8 0 1.1  47 0 .0016 .30 - -
email_spec7_product35_false-unreach-call_true-termination.cil.c 0 900   6200 12000 0 .53 44 0 .025 4.8 0 .66 49 0 .0013 .30 - -
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c 0 900   6200 10000 0 .53 42 0 .019 4.8 0 .86 49 0 .0018 .26 - -
email_spec8_product15_false-unreach-call_true-termination.cil.c 0 900   6900 11000 0 .53 41 0 .027 4.8 0 1.0  50 0 .0018 .26 - -
email_spec8_product16_false-unreach-call_true-termination.cil.c 0 900   6500 11000 0 .58 43 0 .020 4.9 0 1.0  50 0 .0018 .26 - -
email_spec8_product20_false-unreach-call_true-termination.cil.c 0 900   6500 14000 0 .53 42 0 .019 4.8 0 1.1  49 0 .0016 .27 - -
email_spec8_product21_false-unreach-call_true-termination.cil.c 0 900   6400 12000 0 .38 43 0 .023 4.9 0 .86 49 0 .0017 .27 - -
email_spec8_product22_false-unreach-call_true-termination.cil.c 0 900   6900 11000 0 .51 41 0 .022 4.8 0 1.1  49 0 .0017 .28 - -
email_spec8_product26_false-unreach-call_true-termination.cil.c 0 900   6500 14000 0 .54 41 0 .020 5.0 0 .84 47 0 .0012 .34 - -
email_spec8_product30_false-unreach-call_true-termination.cil.c 0 900   6600 11000 0 .66 41 0 .019 5.0 0 .91 49 0 .0016 .26 - -
email_spec8_product31_false-unreach-call_true-termination.cil.c 0 900   6900 14000 0 .55 42 0 .020 4.8 0 1.1  47 0 .0012 .34 - -
email_spec8_product32_false-unreach-call_true-termination.cil.c 0 900   6600 10000 0 .60 45 0 .020 4.9 0 1.1  47 0 .0016 .29 - -
email_spec8_product33_false-unreach-call_true-termination.cil.c 0 900   6600 11000 0 .53 41 0 .024 4.8 0 1.1  47 0 .0014 .26 - -
email_spec8_product34_false-unreach-call_true-termination.cil.c 0 900   6700 11000 0 .53 41 0 .018 4.8 0 1.1  50 0 .0015 .26 - -
email_spec8_product35_false-unreach-call_true-termination.cil.c 0 900   6000 11000 0 .57 44 0 .023 4.8 0 1.1  47 0 .0018 .28 - -
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c 0 900   6200 12000 0 .54 43 0 .019 4.8 0 1.3  47 0 .0014 .28 - -
email_spec9_product15_false-unreach-call_true-termination.cil.c 0 900   6400 12000 0 .39 43 0 .019 4.8 0 1.1  48 0 .0018 .29 - -
email_spec9_product16_false-unreach-call_true-termination.cil.c 0 900   6700 13000 0 .51 43 0 .046 5.0 0 .86 48 0 .0037 .34 - -
email_spec9_product20_false-unreach-call_true-termination.cil.c 0 900   6400 12000 0 .51 41 0 .018 4.8 0 1.1  48 0 .0015 .28 - -
email_spec9_product21_false-unreach-call_true-termination.cil.c 0 900   6400 13000 0 .70 44 0 .018 5.0 0 .90 50 0 .0017 .28 - -
email_spec9_product22_false-unreach-call_true-termination.cil.c 0 900   6400 12000 0 .53 43 0 .036 4.8 0 1.1  49 0 .0016 .28 - -
email_spec9_product26_false-unreach-call_true-termination.cil.c 0 900   6800 11000 0 .51 42 0 .025 5.0 0 1.1  50 0 .0017 .28 - -
email_spec9_product30_false-unreach-call_true-termination.cil.c 0 900   6600 12000 0 .53 43 0 .019 4.9 0 1.1  49 0 .0015 .28 - -
email_spec9_product31_false-unreach-call_true-termination.cil.c 0 900   6800 11000 0 .55 43 0 .018 5.0 0 1.1  47 0 .0017 .29 - -
email_spec9_product32_false-unreach-call_true-termination.cil.c 0 900   6200 13000 0 .55 43 0 .019 5.0 0 1.1  49 0 .0017 .27 - -
email_spec9_product33_false-unreach-call_true-termination.cil.c 0 900   6900 11000 0 .53 41 0 .025 4.8 0 1.1  49 0 .0014 .33 - -
email_spec9_product34_false-unreach-call_true-termination.cil.c 0 900   6800 10000 0 .39 43 0 .023 4.8 0 .90 50 0 .0015 .34 - -
email_spec9_product35_false-unreach-call_true-termination.cil.c 0 900   6900 13000 0 .62 43 0 .025 4.8 0 1.0  49 0 .0020 .26 - -
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c 0 900   6100 12000 0 .53 41 0 .023 4.8 0 .94 49 0 .0016 .29 - -
email_spec0_product05_true-unreach-call_true-termination.cil.c 2 8.9 420 71 - - - - 2 9.9  300 2 8.8   360  
email_spec0_product09_true-unreach-call_true-termination.cil.c 2 10   510 74 - - - - 2 14    330 2 9.4   400  
email_spec0_product10_true-unreach-call_true-termination.cil.c 2 9.2 440 80 - - - - 2 11    420 2 8.7   380  
email_spec0_product11_true-unreach-call_true-termination.cil.c 2 11   500 88 - - - - 2 11    460 2 12     510  
email_spec0_product19_true-unreach-call_true-termination.cil.c 2 13   520 88 - - - - 2 13    450 2 18     590  
email_spec0_product24_true-unreach-call_true-termination.cil.c 2 13   510 90 - - - - 2 17    380 2 28     720  
email_spec0_product25_true-unreach-call_true-termination.cil.c 2 14   520 110 - - - - 2 16    490 2 18     620  
email_spec0_product27_true-unreach-call_true-termination.cil.c 2 13   510 99 - - - - 2 19    550 2 36     760  
email_spec0_product36_true-unreach-call_true-termination.cil.c 2 10   510 78 - - - - 2 12    440 2 10     440  
email_spec0_product37_true-unreach-call_true-termination.cil.c 2 11   520 79 - - - - 2 11    460 2 20     630  
email_spec0_product38_true-unreach-call_true-termination.cil.c 2 13   530 100 - - - - 2 17    380 2 12     510  
email_spec0_product40_true-unreach-call_true-termination.cil.c 2 12   530 92 - - - - 2 14    470 2 22     710  
email_spec11_product03_true-unreach-call_true-termination.cil.c 2 8.0 400 56 - - - - 2 8.9  370 2 11     470  
email_spec11_product07_true-unreach-call_true-termination.cil.c 2 9.8 520 79 - - - - 2 11    430 2 9.2   390  
email_spec11_product08_true-unreach-call_true-termination.cil.c 2 11   500 94 - - - - 2 13    340 2 12     520  
email_spec11_product10_true-unreach-call_true-termination.cil.c 2 9.0 430 64 - - - - 2 12    300 2 9.4   380  
email_spec11_product18_true-unreach-call_true-termination.cil.c 2 12   520 97 - - - - 2 16    370 2 21     590  
email_spec11_product23_true-unreach-call_true-termination.cil.c 2 13   520 94 - - - - 2 15    480 2 22     600  
email_spec11_product24_true-unreach-call_true-termination.cil.c 2 13   510 100 - - - - 2 13    460 2 20     580  
email_spec11_product27_true-unreach-call_true-termination.cil.c 2 14   550 99 - - - - 2 20    470 2 21     640  
email_spec11_product36_true-unreach-call_true-termination.cil.c 2 10   510 84 - - - - 2 13    360 2 9.9   420  
email_spec11_product37_true-unreach-call_true-termination.cil.c 2 11   510 86 - - - - 2 14    340 2 21     520  
email_spec11_product39_true-unreach-call_true-termination.cil.c 2 11   510 88 - - - - 2 15    380 2 14     510  
email_spec11_product40_true-unreach-call_true-termination.cil.c 2 12   510 99 - - - - 2 17    470 2 14     520  
email_spec1_product12_true-unreach-call_true-termination.cil.c 0 900   6600 11000 - - - - 0 .54 44 0 .018 4.9
email_spec1_product28_true-unreach-call_true-termination.cil.c 0 900   6900 13000 - - - - 0 .61 45 0 .018 5.0
email_spec27_product13_true-unreach-call_true-termination.cil.c 0 900   3600 13000 - - - - 0 .42 43 0 .020 4.9
email_spec27_product28_true-unreach-call_true-termination.cil.c 0 900   4100 13000 - - - - 0 .53 44 0 .021 4.9
email_spec4_product13_true-unreach-call_true-termination.cil.c 0 900   6600 12000 - - - - 0 .57 41 0 .018 4.8
email_spec4_product17_true-unreach-call_true-termination.cil.c 0 900   3600 12000 - - - - 0 .65 44 0 .025 4.9
email_spec4_product28_true-unreach-call_true-termination.cil.c 0 900   4500 11000 - - - - 0 .54 42 0 .019 5.0
email_spec4_product29_true-unreach-call_true-termination.cil.c 0 900   4800 13000 - - - - 0 .54 43 0 .019 4.8
email_spec7_product13_true-unreach-call_true-termination.cil.c 2 11   520 100 - - - - 2 14    340 2 13     470  
email_spec7_product17_true-unreach-call_true-termination.cil.c 2 13   530 99 - - - - 2 14    390 2 14     520  
email_spec7_product18_true-unreach-call_true-termination.cil.c 2 11   510 99 - - - - 2 15    450 2 13     520  
email_spec7_product19_true-unreach-call_true-termination.cil.c 2 11   520 82 - - - - 2 15    360 2 14     470  
email_spec7_product23_true-unreach-call_true-termination.cil.c 2 12   530 100 - - - - 2 15    470 2 14     530  
email_spec7_product24_true-unreach-call_true-termination.cil.c 2 12   520 100 - - - - 2 14    480 2 13     530  
email_spec7_product25_true-unreach-call_true-termination.cil.c 2 12   520 100 - - - - 2 15    380 2 13     510  
email_spec7_product27_true-unreach-call_true-termination.cil.c 2 13   520 99 - - - - 2 20    470 2 14     530  
email_spec8_product12_true-unreach-call_true-termination.cil.c 0 900   6600 11000 - - - - 0 .65 44 0 .020 4.8
email_spec8_product14_true-unreach-call_true-termination.cil.c 0 900   6100 14000 - - - - 0 .58 44 0 .020 5.0
email_spec8_product28_true-unreach-call_true-termination.cil.c 0 900   6700 12000 - - - - 0 .55 44 0 .018 4.8
email_spec8_product29_true-unreach-call_true-termination.cil.c 0 900   6700 10000 - - - - 0 .67 43 0 .018 4.8
email_spec9_product12_true-unreach-call_true-termination.cil.c 0 900   7000 11000 - - - - 0 .68 42 0 .020 4.8
email_spec9_product14_true-unreach-call_true-termination.cil.c 0 900   6900 11000 - - - - 0 .66 43 0 .019 4.8
email_spec9_product28_true-unreach-call_true-termination.cil.c 0 900   6600 13000 - - - - 0 .63 43 0 .018 4.8
email_spec9_product29_true-unreach-call_true-termination.cil.c 0 900   6500 11000 - - - - 0 .60 43 0 .024 4.9
minepump_spec1_product33_false-unreach-call_false-termination.cil.c 1 6.2 310 49 -32 2.8  260 1 7.0   290   0 4.8  220 1 .75   19    - -
minepump_spec1_product34_false-unreach-call_false-termination.cil.c 1 6.5 320 52 -32 4.2  260 1 4.3   280   0 4.3  210 1 .88   19    - -
minepump_spec1_product35_false-unreach-call_false-termination.cil.c 1 7.2 340 51 -32 3.9  260 1 4.7   290   0 4.3  210 1 .83   19    - -
minepump_spec1_product36_false-unreach-call_false-termination.cil.c 1 6.8 370 56 -32 4.0  260 1 8.4   280   0 4.0  220 1 .89   19    - -
minepump_spec1_product37_false-unreach-call_false-termination.cil.c 1 7.1 340 58 -32 4.4  260 1 9.8   290   0 4.4  210 1 .87   19    - -
minepump_spec1_product38_false-unreach-call_false-termination.cil.c 1 7.3 350 50 -32 2.7  260 1 8.6   290   0 4.5  210 1 .71   19    - -
minepump_spec1_product39_false-unreach-call_false-termination.cil.c 1 7.5 410 53 -32 4.1  260 1 4.4   290   0 4.9  230 0 .68   19    - -
minepump_spec1_product40_false-unreach-call_false-termination.cil.c 1 7.5 380 62 -32 4.5  260 1 8.3   290   0 4.8  210 1 .90   19    - -
minepump_spec1_product41_false-unreach-call_false-termination.cil.c 1 11   530 79 -32 4.0  260 1 7.5   300   0 5.0  220 1 .90   19    - -
minepump_spec1_product42_false-unreach-call_false-termination.cil.c 1 13   580 110 -32 5.0  260 1 13     420   0 4.8  220 1 .91   19    - -
minepump_spec1_product43_false-unreach-call_false-termination.cil.c 1 14   660 120 -32 4.2  270 1 6.4   300   0 3.5  220 1 .81   19    - -
minepump_spec1_product44_false-unreach-call_false-termination.cil.c 0 900   1700 11000 0 .54 44 0 .019 5.0 0 1.0  47 0 .0016 .28 - -
minepump_spec1_product49_false-unreach-call_false-termination.cil.c 1 6.9 350 53 -32 4.8  260 1 8.4   290   0 4.1  210 1 .91   19    - -
minepump_spec1_product50_false-unreach-call_false-termination.cil.c 1 9.1 370 60 -32 4.2  260 1 6.2   280   0 3.5  210 1 .88   19    - -
minepump_spec1_product51_false-unreach-call_false-termination.cil.c 1 7.7 370 65 -32 4.2  260 1 6.3   290   0 4.7  220 0 .69   19    - -
minepump_spec1_product52_false-unreach-call_false-termination.cil.c 1 7.9 390 66 -32 4.3  260 1 6.5   290   0 4.3  210 1 .68   19    - -
minepump_spec1_product53_false-unreach-call_false-termination.cil.c 1 7.8 350 57 -32 4.0  260 1 6.9   300   0 4.6  220 1 .87   19    - -
minepump_spec1_product54_false-unreach-call_false-termination.cil.c 1 9.3 370 61 -32 4.3  260 1 8.2   290   0 4.2  220 1 .89   19    - -
minepump_spec1_product55_false-unreach-call_false-termination.cil.c 1 7.9 400 61 -32 4.1  260 1 6.5   290   0 4.5  210 0 .94   19    - -
minepump_spec1_product56_false-unreach-call_false-termination.cil.c 1 8.4 390 73 -32 4.3  260 1 8.5   290   0 4.5  210 1 .85   19    - -
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c 0 900   1600 12000 0 .67 41 0 .019 4.8 0 1.1  49 0 .0016 .29 - -
minepump_spec2_product33_false-unreach-call_false-termination.cil.c 1 12   540 100 -32 5.3  270 1 15     470   0 4.5  210 1 .70   20    - -
minepump_spec2_product34_false-unreach-call_false-termination.cil.c 1 13   620 110 -32 4.2  270 1 12     450   0 4.7  220 1 .89   20    - -
minepump_spec2_product35_false-unreach-call_false-termination.cil.c 1 13   560 100 -32 4.2  260 1 10     440   0 4.7  220 1 .81   19    - -
minepump_spec2_product36_false-unreach-call_false-termination.cil.c 1 13   610 110 -32 4.1  260 1 13     450   0 3.9  210 1 .89   19    - -
minepump_spec2_product41_false-unreach-call_false-termination.cil.c 1 11   540 100 -32 4.3  260 1 18     520   0 4.6  220 1 .90   20    - -
minepump_spec2_product42_false-unreach-call_false-termination.cil.c 0 900   1400 11000 0 .52 42 0 .022 4.9 0 .88 47 0 .0015 .26 - -
minepump_spec2_product43_false-unreach-call_false-termination.cil.c 1 34   910 350 -32 4.2  270 1 7.8   530   0 4.4  220 1 .83   20    - -
minepump_spec2_product44_false-unreach-call_false-termination.cil.c 1 23   800 210 -32 4.2  260 1 8.1   300   0 3.7  240 1 .93   20    - -
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c 1 140   2500 1600 -32 7.3  370 1 12     510   0 5.8  220 0 .92   20    - -
minepump_spec3_product01_false-unreach-call_false-termination.cil.c 1 6.1 310 48 -32 4.6  260 1 7.6   330   0 4.5  220 1 .87   19    - -
minepump_spec3_product02_false-unreach-call_false-termination.cil.c 1 6.3 300 46 -32 3.6  260 1 6.2   280   0 4.7  220 1 .88   19    - -
minepump_spec3_product03_false-unreach-call_false-termination.cil.c 1 5.9 310 45 -32 3.5  260 1 6.3   280   0 3.7  210 1 .88   19    - -
minepump_spec3_product04_false-unreach-call_false-termination.cil.c 1 6.0 310 47 -32 2.5  260 1 6.3   280   0 3.6  210 1 .76   19    - -
minepump_spec3_product05_false-unreach-call_false-termination.cil.c 1 6.0 330 51 -32 4.4  260 1 6.8   280   0 3.4  210 1 .90   19    - -
minepump_spec3_product06_false-unreach-call_false-termination.cil.c 1 6.3 330 49 -32 4.1  260 1 5.9   290   0 4.0  210 1 .79   19    - -
minepump_spec3_product07_false-unreach-call_false-termination.cil.c 1 6.6 320 57 -32 3.8  260 1 6.4   280   0 3.5  210 1 .79   19    - -
minepump_spec3_product08_false-unreach-call_false-termination.cil.c 1 6.7 320 54 -32 2.6  260 1 6.6   290   0 4.6  230 1 .96   19    - -
minepump_spec3_product09_false-unreach-call_false-termination.cil.c 1 6.0 310 48 -32 3.8  260 1 6.0   280   0 3.3  210 1 .86   19    - -
minepump_spec3_product10_false-unreach-call_false-termination.cil.c 1 6.3 310 52 -32 3.8  260 1 6.7   280   0 4.1  210 1 .67   19    - -
minepump_spec3_product11_false-unreach-call_false-termination.cil.c 1 6.0 310 44 -32 4.7  260 1 7.5   280   0 4.5  220 1 .86   19    - -
minepump_spec3_product12_false-unreach-call_false-termination.cil.c 1 6.0 310 48 -32 4.4  270 1 7.7   270   0 3.8  220 1 .78   19    - -
minepump_spec3_product13_false-unreach-call_false-termination.cil.c 1 6.1 320 46 -32 4.2  260 1 6.8   280   0 3.7  220 1 .88   19    - -
minepump_spec3_product14_false-unreach-call_false-termination.cil.c 1 6.8 330 54 -32 3.9  260 1 6.2   280   0 4.5  240 1 .66   19    - -
minepump_spec3_product15_false-unreach-call_false-termination.cil.c 1 6.5 330 48 -32 3.8  260 1 5.8   280   0 3.4  210 1 .69   19    - -
minepump_spec3_product16_false-unreach-call_false-termination.cil.c 1 6.4 320 48 -32 4.0  260 1 6.3   280   0 4.5  210 1 .79   19    - -
minepump_spec3_product17_false-unreach-call_false-termination.cil.c 1 7.6 390 68 -32 4.5  260 1 7.1   280   0 3.4  210 1 .74   19    - -
minepump_spec3_product18_false-unreach-call_false-termination.cil.c 1 7.9 420 58 -32 3.8  260 1 6.8   280   0 4.5  210 1 .67   19    - -
minepump_spec3_product19_false-unreach-call_false-termination.cil.c 1 6.5 330 51 -32 3.9  260 1 6.2   280   0 3.8  220 1 .90   19    - -
minepump_spec3_product20_false-unreach-call_false-termination.cil.c 1 6.7 350 53 -32 3.7  260 1 6.7   280   0 4.7  210 1 .83   19    - -
minepump_spec3_product21_false-unreach-call_false-termination.cil.c 1 6.7 340 53 -32 4.9  260 1 8.6   280   0 4.5  210 1 .81   19    - -
minepump_spec3_product22_false-unreach-call_false-termination.cil.c 1 6.6 330 54 -32 3.9  260 1 6.0   290   0 3.7  220 1 .90   19    - -
minepump_spec3_product23_false-unreach-call_false-termination.cil.c 1 6.6 320 51 -32 4.0  260 1 7.7   280   0 4.6  210 1 .75   19    - -
minepump_spec3_product24_false-unreach-call_false-termination.cil.c 1 6.5 330 59 -32 3.9  260 1 6.5   280   0 3.7  230 1 .69   19    - -
minepump_spec3_product25_false-unreach-call_false-termination.cil.c 1 7.6 420 62 -32 3.9  260 1 6.4   290   0 4.3  210 1 .72   19    - -
minepump_spec3_product26_false-unreach-call_false-termination.cil.c 1 7.4 420 60 -32 3.9  260 1 6.5   280   0 4.4  210 1 .88   19    - -
minepump_spec3_product27_false-unreach-call_false-termination.cil.c 1 6.2 330 56 -32 3.8  260 1 6.0   280   0 4.6  220 1 .74   19    - -
minepump_spec3_product28_false-unreach-call_false-termination.cil.c 1 6.8 350 53 -32 4.1  260 1 6.1   280   0 4.7  210 1 .90   19    - -
minepump_spec3_product29_false-unreach-call_false-termination.cil.c 1 6.4 330 52 -32 4.0  260 1 9.0   290   0 3.6  210 1 .81   19    - -
minepump_spec3_product30_false-unreach-call_false-termination.cil.c 1 6.4 340 54 -32 3.9  260 1 5.8   270   0 4.5  230 1 .91   19    - -
minepump_spec3_product31_false-unreach-call_false-termination.cil.c 1 6.7 330 53 -32 3.9  260 1 6.5   280   0 3.6  210 1 .73   19    - -
minepump_spec3_product32_false-unreach-call_false-termination.cil.c 1 6.7 330 57 -32 4.0  260 1 7.7   290   0 3.8  220 1 .70   19    - -
minepump_spec3_product35_false-unreach-call_false-termination.cil.c 1 5.9 310 56 -32 5.1  260 1 8.1   280   0 3.4  210 1 .90   19    - -
minepump_spec3_product36_false-unreach-call_false-termination.cil.c 1 6.2 320 46 -32 4.1  260 1 8.1   280   0 4.1  220 1 .73   19    - -
minepump_spec3_product39_false-unreach-call_false-termination.cil.c 1 6.9 330 60 -32 4.4  260 1 6.6   290   0 4.8  220 1 .82   19    - -
minepump_spec3_product40_false-unreach-call_false-termination.cil.c 1 6.7 330 57 -32 4.0  260 1 6.5   290   0 4.2  210 1 .81   19    - -
minepump_spec3_product43_false-unreach-call_false-termination.cil.c 1 6.8 340 61 -32 4.0  260 1 8.0   280   0 4.4  210 1 .90   19    - -
minepump_spec3_product44_false-unreach-call_false-termination.cil.c 1 6.1 320 47 -32 4.7  260 1 8.4   280   0 3.4  210 1 .87   19    - -
minepump_spec3_product47_false-unreach-call_false-termination.cil.c 1 6.7 320 60 -32 4.5  260 1 8.8   290   0 4.6  240 1 .79   19    - -
minepump_spec3_product48_false-unreach-call_false-termination.cil.c 1 7.0 350 57 -32 5.1  260 1 7.4   290   0 3.7  210 1 .71   19    - -
minepump_spec3_product51_false-unreach-call_false-termination.cil.c 1 6.7 320 54 -32 4.2  260 1 5.9   290   0 4.9  230 1 .75   19    - -
minepump_spec3_product52_false-unreach-call_false-termination.cil.c 1 6.7 340 54 -32 4.2  260 1 4.9   290   0 4.4  210 1 .78   19    - -
minepump_spec3_product55_false-unreach-call_false-termination.cil.c 1 6.9 330 54 -32 4.0  260 1 6.8   290   0 3.7  210 1 .78   19    - -
minepump_spec3_product56_false-unreach-call_false-termination.cil.c 1 7.1 340 57 -32 3.9  260 1 10     340   0 4.6  210 1 .78   19    - -
minepump_spec3_product59_false-unreach-call_false-termination.cil.c 1 8.0 440 70 -32 4.1  260 1 6.2   290   0 4.4  210 1 .89   19    - -
minepump_spec3_product60_false-unreach-call_false-termination.cil.c 1 6.6 340 55 -32 4.2  260 1 6.4   290   0 4.4  210 1 .72   19    - -
minepump_spec3_product63_false-unreach-call_false-termination.cil.c 1 6.8 340 53 -32 4.1  260 1 8.1   300   0 4.5  210 1 .79   19    - -
minepump_spec3_product64_false-unreach-call_false-termination.cil.c 1 7.2 360 64 -32 4.2  260 1 8.2   290   0 3.5  210 1 .82   19    - -
minepump_spec3_productSimulator_false-unreach-call_false-termination.cil.c 1 7.8 350 59 -32 6.9  360 1 5.2   310   0 5.5  220 1 .74   19    - -
minepump_spec4_product33_false-unreach-call_false-termination.cil.c 1 15   720 130 -32 5.1  260 1 5.3   310   0 4.6  210 1 .90   19    - -
minepump_spec4_product34_false-unreach-call_false-termination.cil.c 1 23   850 240 -32 5.2  260 1 7.6   310   0 3.6  210 1 .92   19    - -
minepump_spec4_product35_false-unreach-call_false-termination.cil.c 1 31   1000 320 -32 4.1  270 1 11     350   0 3.7  210 1 .91   19    - -
minepump_spec4_product36_false-unreach-call_false-termination.cil.c 1 26   880 240 -32 4.5  260 1 13     490   0 3.7  220 1 .86   20    - -
minepump_spec4_product37_false-unreach-call_false-termination.cil.c 1 22   860 220 -32 4.1  270 1 12     510   0 5.1  210 0 .80   20    - -
minepump_spec4_product38_false-unreach-call_false-termination.cil.c 1 24   820 270 -32 4.2  260 1 6.2   300   0 4.8  220 0 .85   20    - -
minepump_spec4_product39_false-unreach-call_false-termination.cil.c 1 51   1200 620 -32 4.3  260 1 11     400   0 3.9  220 0 .85   19    - -
minepump_spec4_product40_false-unreach-call_false-termination.cil.c 0 900   1900 11000 0 .51 42 0 .023 4.8 0 1.2  47 0 .0015 .34 - -
minepump_spec4_product41_false-unreach-call_false-termination.cil.c 1 19   750 180 -32 4.2  260 1 7.6   290   0 4.4  220 1 .80   19    - -
minepump_spec4_product42_false-unreach-call_false-termination.cil.c 1 14   620 120 -32 4.3  260 1 12     510   0 4.7  210 1 .87   20    - -
minepump_spec4_product43_false-unreach-call_false-termination.cil.c 1 48   1200 590 -32 4.1  260 1 9.4   360   0 3.7  220 1 .73   19    - -
minepump_spec4_product44_false-unreach-call_false-termination.cil.c 1 24   850 250 -32 4.2  260 1 10     350   0 3.6  220 1 .68   20    - -
minepump_spec4_product45_false-unreach-call_false-termination.cil.c 0 900   1700 11000 0 .54 43 0 .024 4.8 0 1.1  49 0 .0016 .28 - -
minepump_spec4_product46_false-unreach-call_false-termination.cil.c 1 32   890 390 -32 4.3  260 1 11     510   0 4.3  220 0 .68   19    - -
minepump_spec4_product47_false-unreach-call_false-termination.cil.c 0 900   1600 11000 0 .54 41 0 .026 4.8 0 1.1  49 0 .0017 .26 - -
minepump_spec4_product48_false-unreach-call_false-termination.cil.c 1 35   950 350 -32 4.2  260 1 17     530   0 3.8  220 0 .91   19    - -
minepump_spec4_productSimulator_false-unreach-call_false-termination.cil.c 1 320   4700 4800 -32 6.8  360 1 11     500   0 4.8  220 0 .74   20    - -
minepump_spec1_product01_true-unreach-call_false-termination.cil.c 2 6.8 340 54 - - - - 0 910    6200 2 8.0   290  
minepump_spec1_product02_true-unreach-call_false-termination.cil.c 2 6.5 340 50 - - - - 0 910    6600 2 9.8   380  
minepump_spec1_product03_true-unreach-call_false-termination.cil.c 2 7.0 350 53 - - - - 0 590    7000 2 8.8   310  
minepump_spec1_product04_true-unreach-call_false-termination.cil.c 2 6.5 350 50 - - - - 0 680    7000 2 8.9   300  
minepump_spec1_product05_true-unreach-call_false-termination.cil.c 2 10   540 89 - - - - 0 790    7000 2 9.0   300  
minepump_spec1_product06_true-unreach-call_false-termination.cil.c 2 8.2 450 69 - - - - 0 900    6200 2 9.3   300  
minepump_spec1_product07_true-unreach-call_false-termination.cil.c 2 12   530 100 - - - - 0 520    7000 2 8.0   290  
minepump_spec1_product08_true-unreach-call_false-termination.cil.c 0 900   1400 10000 - - - - 0 .55 43 0 .019 4.8
minepump_spec1_product09_true-unreach-call_false-termination.cil.c 2 6.4 340 47 - - - - 0 910    6100 2 9.5   360  
minepump_spec1_product10_true-unreach-call_false-termination.cil.c 2 6.3 340 52 - - - - 0 830    7000 2 9.9   390  
minepump_spec1_product11_true-unreach-call_false-termination.cil.c 2 6.5 350 50 - - - - 0 550    7000 2 9.1   310  
minepump_spec1_product12_true-unreach-call_false-termination.cil.c 2 6.9 350 54 - - - - 0 710    7000 2 8.5   310  
minepump_spec1_product13_true-unreach-call_false-termination.cil.c 2 11   460 94 - - - - 0 740    7000 2 7.5   300  
minepump_spec1_product14_true-unreach-call_false-termination.cil.c 2 11   570 95 - - - - 0 910    6300 2 9.6   360  
minepump_spec1_product15_true-unreach-call_false-termination.cil.c 2 13   580 120 - - - - 0 540    7000 2 9.1   310  
minepump_spec1_product16_true-unreach-call_false-termination.cil.c 2 11   510 110 - - - - 0 590    7000 2 7.9   280  
minepump_spec1_product17_true-unreach-call_false-termination.cil.c 0 900   1700 12000 - - - - 0 .70 43 0 .019 4.9
minepump_spec1_product18_true-unreach-call_false-termination.cil.c 2 7.7 370 59 - - - - 0 730    7000 2 8.3   300  
minepump_spec1_product19_true-unreach-call_false-termination.cil.c 2 9.3 490 84 - - - - 0 460    7000 2 9.3   330  
minepump_spec1_product20_true-unreach-call_false-termination.cil.c 2 12   540 110 - - - - 0 640    7000 2 7.6   290  
minepump_spec1_product21_true-unreach-call_false-termination.cil.c 2 8.7 410 81 - - - - 0 740    7000 2 8.5   300  
minepump_spec1_product22_true-unreach-call_false-termination.cil.c 2 12   520 77 - - - - 0 630    7000 2 8.7   310  
minepump_spec1_product23_true-unreach-call_false-termination.cil.c 2 12   520 99 - - - - 0 490    7000 2 11     360  
minepump_spec1_product24_true-unreach-call_false-termination.cil.c 2 19   670 160 - - - - 0 550    7000 2 9.1   350  
minepump_spec1_product25_true-unreach-call_false-termination.cil.c 2 8.0 350 60 - - - - 0 820    7000 2 8.3   290  
minepump_spec1_product26_true-unreach-call_false-termination.cil.c 2 8.2 370 68 - - - - 0 720    7000 2 8.3   300  
minepump_spec1_product27_true-unreach-call_false-termination.cil.c 2 12   530 90 - - - - 0 470    7000 2 8.6   300  
minepump_spec1_product28_true-unreach-call_false-termination.cil.c 2 13   590 110 - - - - 0 730    7000 2 10     320  
minepump_spec1_product29_true-unreach-call_false-termination.cil.c 2 8.9 420 83 - - - - 0 810    7000 2 8.9   290  
minepump_spec1_product30_true-unreach-call_false-termination.cil.c 2 8.8 500 77 - - - - 0 610    7000 2 9.0   300  
minepump_spec1_product31_true-unreach-call_false-termination.cil.c 2 14   580 110 - - - - 0 490    7000 2 9.8   340  
minepump_spec1_product32_true-unreach-call_false-termination.cil.c 2 14   640 130 - - - - 0 530    7000 2 8.8   310  
minepump_spec1_product45_true-unreach-call_false-termination.cil.c 2 14   580 110 - - - - 0 480    7000 2 19     570  
minepump_spec1_product46_true-unreach-call_false-termination.cil.c 0 900   4500 11000 - - - - 0 .53 41 0 .020 4.9
minepump_spec1_product47_true-unreach-call_false-termination.cil.c 2 18   700 160 - - - - 0 540    7000 2 20     570  
minepump_spec1_product48_true-unreach-call_false-termination.cil.c 2 20   700 160 - - - - 0 590    7000 2 27     630  
minepump_spec1_product57_true-unreach-call_false-termination.cil.c 0 900   1500 11000 - - - - 0 .56 43 0 .019 4.8
minepump_spec1_product58_true-unreach-call_false-termination.cil.c 0 900   1600 10000 - - - - 0 .67 41 0 .019 4.8
minepump_spec1_product59_true-unreach-call_false-termination.cil.c 0 900   1500 11000 - - - - 0 .69 43 0 .019 4.9
minepump_spec1_product60_true-unreach-call_false-termination.cil.c 2 21   760 200 - - - - 0 910    6700 2 29     680  
minepump_spec1_product61_true-unreach-call_false-termination.cil.c 2 14   610 130 - - - - 0 550    7000 2 18     580  
minepump_spec1_product62_true-unreach-call_false-termination.cil.c 0 900   1500 11000 - - - - 0 .55 42 0 .024 5.0
minepump_spec1_product63_true-unreach-call_false-termination.cil.c 2 25   840 230 - - - - 0 590    7000 2 23     620  
minepump_spec1_product64_true-unreach-call_false-termination.cil.c 2 26   840 230 - - - - 0 510    7000 2 21     500  
minepump_spec2_product01_true-unreach-call_false-termination.cil.c 2 8.0 440 71 - - - - 0 900    6100 2 7.6   280  
minepump_spec2_product02_true-unreach-call_false-termination.cil.c 2 8.3 370 73 - - - - 0 900    5600 2 14     510  
minepump_spec2_product03_true-unreach-call_false-termination.cil.c 2 8.0 360 74 - - - - 0 530    7000 2 6.7   330  
minepump_spec2_product04_true-unreach-call_false-termination.cil.c 2 8.0 350 62 - - - - 0 590    7000 2 7.7   280  
minepump_spec2_product05_true-unreach-call_false-termination.cil.c 2 7.6 430 65 - - - - 0 740    7000 2 8.2   290  
minepump_spec2_product06_true-unreach-call_false-termination.cil.c 2 8.9 430 73 - - - - 0 800    7000 2 9.7   310  
minepump_spec2_product07_true-unreach-call_false-termination.cil.c 0 900   1400 12000 - - - - 0 .53 42 0 .018 4.8
minepump_spec2_product08_true-unreach-call_false-termination.cil.c 2 17   620 130 - - - - 0 530    7000 2 8.1   300  
minepump_spec2_product09_true-unreach-call_false-termination.cil.c 2 6.9 340 52 - - - - 0 900    6000 2 14     510  
minepump_spec2_product10_true-unreach-call_false-termination.cil.c 2 8.5 390 63 - - - - 0 900    5800 2 10     410  
minepump_spec2_product11_true-unreach-call_false-termination.cil.c 2 8.5 400 69 - - - - 0 540    7000 2 12     500  
minepump_spec2_product12_true-unreach-call_false-termination.cil.c 2 8.7 480 67 - - - - 0 620    7000 2 7.6   290  
minepump_spec2_product13_true-unreach-call_false-termination.cil.c 2 10   520 79 - - - - 0 640    7000 2 9.0   310  
minepump_spec2_product14_true-unreach-call_false-termination.cil.c 2 9.8 510 84 - - - - 0 890    7000 2 8.6   300  
minepump_spec2_product15_true-unreach-call_false-termination.cil.c 2 21   760 180 - - - - 0 420    7000 2 8.2   310  
minepump_spec2_product16_true-unreach-call_false-termination.cil.c 0 900   1600 14000 - - - - 0 .66 41 0 .021 4.8
minepump_spec2_product17_true-unreach-call_false-termination.cil.c 2 9.0 480 72 - - - - 0 910    6200 2 8.0   300  
minepump_spec2_product18_true-unreach-call_false-termination.cil.c 0 900   1300 12000 - - - - 0 .59 43 0 .018 4.8
minepump_spec2_product19_true-unreach-call_false-termination.cil.c 2 15   650 130 - - - - 0 670    7000 2 8.2   300  
minepump_spec2_product20_true-unreach-call_false-termination.cil.c 2 19   660 180 - - - - 0 910    6300 2 8.5   310  
minepump_spec2_product21_true-unreach-call_false-termination.cil.c 2 14   590 130 - - - - 0 570    7000 2 9.8   330  
minepump_spec2_product22_true-unreach-call_false-termination.cil.c 2 9.1 420 74 - - - - 0 640    7000 2 9.0   330  
minepump_spec2_product23_true-unreach-call_false-termination.cil.c 2 17   650 160 - - - - 0 470    7000 2 11     330  
minepump_spec2_product24_true-unreach-call_false-termination.cil.c 0 900   1400 11000 - - - - 0 .69 41 0 .019 4.9
minepump_spec2_product25_true-unreach-call_false-termination.cil.c 0 900   1600 9200 - - - - 0 .69 43 0 .018 4.8
minepump_spec2_product26_true-unreach-call_false-termination.cil.c 2 8.1 360 63 - - - - 0 850    7000 2 8.0   310  
minepump_spec2_product27_true-unreach-call_false-termination.cil.c 2 20   670 170 - - - - 0 680    7000 2 8.5   320  
minepump_spec2_product28_true-unreach-call_false-termination.cil.c 2 14   580 110 - - - - 0 880    7000 2 8.7   290  
minepump_spec2_product29_true-unreach-call_false-termination.cil.c 2 11   500 94 - - - - 0 640    7000 2 8.8   310  
minepump_spec2_product30_true-unreach-call_false-termination.cil.c 2 8.9 500 76 - - - - 0 620    7000 2 9.2   310  
minepump_spec2_product31_true-unreach-call_false-termination.cil.c 2 15   630 120 - - - - 0 500    7000 2 8.9   300  
minepump_spec2_product32_true-unreach-call_false-termination.cil.c 2 16   670 140 - - - - 0 570    7000 2 10     310  
minepump_spec2_product37_true-unreach-call_false-termination.cil.c 2 34   990 370 - - - - 0 590    7000 2 17     570  
minepump_spec2_product38_true-unreach-call_false-termination.cil.c 0 900   1300 14000 - - - - 0 .69 43 0 .018 4.9
minepump_spec2_product39_true-unreach-call_false-termination.cil.c 0 900   1300 13000 - - - - 0 .58 43 0 .018 4.9
minepump_spec2_product40_true-unreach-call_false-termination.cil.c 0 900   1400 9900 - - - - 0 .66 44 0 .019 4.9
minepump_spec2_product45_true-unreach-call_false-termination.cil.c 2 15   680 120 - - - - 0 430    7000 2 28     680  
minepump_spec2_product46_true-unreach-call_false-termination.cil.c 0 900   1900 11000 - - - - 0 .55 43 0 .019 4.8
minepump_spec2_product47_true-unreach-call_false-termination.cil.c 0 900   1600 13000 - - - - 0 .52 42 0 .018 4.8
minepump_spec2_product48_true-unreach-call_false-termination.cil.c 2 27   820 240 - - - - 0 650    7000 2 33     700  
minepump_spec2_product49_true-unreach-call_false-termination.cil.c 2 29   840 300 - - - - 0 910    6700 2 30     660  
minepump_spec2_product50_true-unreach-call_false-termination.cil.c 0 900   1800 15000 - - - - 0 .55 43 0 .018 4.9
minepump_spec2_product51_true-unreach-call_false-termination.cil.c 2 70   1400 800 - - - - 0 910    7000 2 29     640  
minepump_spec2_product52_true-unreach-call_false-termination.cil.c 0 900   1400 10000 - - - - 0 .61 41 0 .019 4.8
minepump_spec2_product53_true-unreach-call_false-termination.cil.c 2 23   740 210 - - - - 0 500    7000 2 20     620  
minepump_spec2_product54_true-unreach-call_false-termination.cil.c 2 82   1600 960 - - - - 0 470    7000 2 30     690  
minepump_spec2_product55_true-unreach-call_false-termination.cil.c 2 54   1300 540 - - - - 0 600    7000 2 16     570  
minepump_spec2_product56_true-unreach-call_false-termination.cil.c 0 900   1500 11000 - - - - 0 .66 44 0 .020 4.9
minepump_spec2_product57_true-unreach-call_false-termination.cil.c 0 900   1800 13000 - - - - 0 .52 43 0 .019 5.0
minepump_spec2_product58_true-unreach-call_false-termination.cil.c 0 900   2100 12000 - - - - 0 .58 42 0 .018 4.9
minepump_spec2_product59_true-unreach-call_false-termination.cil.c 2 76   1600 980 - - - - 0 900    7000 2 31     700  
minepump_spec2_product60_true-unreach-call_false-termination.cil.c 0 900   1900 10000 - - - - 0 .66 41 0 .019 4.9
minepump_spec2_product61_true-unreach-call_false-termination.cil.c 2 14   630 140 - - - - 0 390    7000 2 41     610  
minepump_spec2_product62_true-unreach-call_false-termination.cil.c 0 900   1700 12000 - - - - 0 .59 41 0 .019 5.0
minepump_spec2_product63_true-unreach-call_false-termination.cil.c 0 900   1500 13000 - - - - 0 .61 44 0 .019 4.9
minepump_spec2_product64_true-unreach-call_false-termination.cil.c 2 21   730 200 - - - - 0 560    7000 2 18     560  
minepump_spec3_product33_true-unreach-call_false-termination.cil.c 2 8.8 430 68 - - - - 0 910    4800 2 11     490  
minepump_spec3_product34_true-unreach-call_false-termination.cil.c 2 9.6 520 88 - - - - 0 910    6700 2 11     520  
minepump_spec3_product37_true-unreach-call_false-termination.cil.c 0 900   2700 11000 - - - - 0 .40 43 0 .019 4.9
minepump_spec3_product38_true-unreach-call_false-termination.cil.c 0 900   1500 14000 - - - - 0 .51 41 0 .023 4.8
minepump_spec3_product41_true-unreach-call_false-termination.cil.c 2 9.9 510 90 - - - - 0 640    7000 2 12     510  
minepump_spec3_product42_true-unreach-call_false-termination.cil.c 0 900   1900 10000 - - - - 0 .68 41 0 .019 5.0
minepump_spec3_product45_true-unreach-call_false-termination.cil.c 0 900   1900 14000 - - - - 0 .53 43 0 .019 4.9
minepump_spec3_product46_true-unreach-call_false-termination.cil.c 0 900   2800 10000 - - - - 0 .71 44 0 .019 4.9
minepump_spec3_product49_true-unreach-call_false-termination.cil.c 0 900   2100 12000 - - - - 0 .54 44 0 .019 4.9
minepump_spec3_product50_true-unreach-call_false-termination.cil.c 0 900   4100 10000 - - - - 0 .66 43 0 .019 4.9
minepump_spec3_product53_true-unreach-call_false-termination.cil.c 0 900   2500 11000 - - - - 0 .61 42 0 .018 5.0
minepump_spec3_product54_true-unreach-call_false-termination.cil.c 0 900   1600 12000 - - - - 0 .56 41 0 .020 4.9
minepump_spec3_product57_true-unreach-call_false-termination.cil.c 0 900   1300 11000 - - - - 0 .68 41 0 .020 4.8
minepump_spec3_product58_true-unreach-call_false-termination.cil.c 0 900   1200 12000 - - - - 0 .68 43 0 .018 4.8
minepump_spec3_product61_true-unreach-call_false-termination.cil.c 2 41   1300 480 - - - - 0 900    6900 2 31     690  
minepump_spec3_product62_true-unreach-call_false-termination.cil.c 0 900   1700 13000 - - - - 0 .73 41 0 .022 4.9
minepump_spec4_product01_true-unreach-call_false-termination.cil.c 2 7.9 470 68 - - - - 0 900    6600 2 7.9   310  
minepump_spec4_product02_true-unreach-call_false-termination.cil.c 2 7.8 460 62 - - - - 0 900    5300 2 9.3   340  
minepump_spec4_product03_true-unreach-call_false-termination.cil.c 2 8.2 390 61 - - - - 0 900    5800 2 12     460  
minepump_spec4_product04_true-unreach-call_false-termination.cil.c 2 8.4 450 78 - - - - 0 910    5800 2 9.9   420  
minepump_spec4_product05_true-unreach-call_false-termination.cil.c 2 8.3 360 66 - - - - 0 820    7000 2 11     440  
minepump_spec4_product06_true-unreach-call_false-termination.cil.c 2 13   580 110 - - - - 0 910    6500 2 11     450  
minepump_spec4_product07_true-unreach-call_false-termination.cil.c 2 38   1000 390 - - - - 0 670    7000 2 11     500  
minepump_spec4_product08_true-unreach-call_false-termination.cil.c 2 20   790 220 - - - - 0 730    7000 2 8.9   500  
minepump_spec4_product09_true-unreach-call_false-termination.cil.c 2 8.3 470 64 - - - - 0 910    6100 2 9.6   350  
minepump_spec4_product10_true-unreach-call_false-termination.cil.c 2 7.7 460 64 - - - - 0 900    4700 2 9.0   330  
minepump_spec4_product11_true-unreach-call_false-termination.cil.c 2 8.0 440 69 - - - - 0 910    5800 2 10     410  
minepump_spec4_product12_true-unreach-call_false-termination.cil.c 2 8.5 480 72 - - - - 0 910    5800 2 10     470  
minepump_spec4_product13_true-unreach-call_false-termination.cil.c 2 7.7 410 65 - - - - 0 760    7000 2 10     440  
minepump_spec4_product14_true-unreach-call_false-termination.cil.c 2 12   580 110 - - - - 0 850    7000 2 9.8   390  
minepump_spec4_product15_true-unreach-call_false-termination.cil.c 2 11   560 85 - - - - 0 640    7000 2 12     490  
minepump_spec4_product16_true-unreach-call_false-termination.cil.c 2 10   530 88 - - - - 0 670    7000 2 11     490  
minepump_spec4_product17_true-unreach-call_false-termination.cil.c 2 8.3 360 64 - - - - 0 910    6500 2 10     380  
minepump_spec4_product18_true-unreach-call_false-termination.cil.c 2 9.6 480 75 - - - - 0 840    7000 2 11     480  
minepump_spec4_product19_true-unreach-call_false-termination.cil.c 2 17   650 140 - - - - 0 700    7000 2 12     510  
minepump_spec4_product20_true-unreach-call_false-termination.cil.c 2 30   910 290 - - - - 0 770    7000 2 12     500  
minepump_spec4_product21_true-unreach-call_false-termination.cil.c 2 17   670 140 - - - - 0 910    6300 2 11     470  
minepump_spec4_product22_true-unreach-call_false-termination.cil.c 2 16   700 150 - - - - 0 670    7000 2 11     410  
minepump_spec4_product23_true-unreach-call_false-termination.cil.c 0 900   1400 13000 - - - - 0 .54 43 0 .019 4.9
minepump_spec4_product24_true-unreach-call_false-termination.cil.c 2 25   810 260 - - - - 0 570    7000 2 11     510  
minepump_spec4_product25_true-unreach-call_false-termination.cil.c 2 13   630 120 - - - - 0 900    5800 2 6.9   380  
minepump_spec4_product26_true-unreach-call_false-termination.cil.c 2 8.4 370 71 - - - - 0 850    7000 2 10     420  
minepump_spec4_product27_true-unreach-call_false-termination.cil.c 2 29   930 290 - - - - 0 790    7000 2 12     500  
minepump_spec4_product28_true-unreach-call_false-termination.cil.c 2 11   550 92 - - - - 0 700    7000 2 13     470  
minepump_spec4_product29_true-unreach-call_false-termination.cil.c 2 16   670 120 - - - - 0 910    6600 2 12     460  
minepump_spec4_product30_true-unreach-call_false-termination.cil.c 2 13   640 110 - - - - 0 740    7000 2 9.8   400  
minepump_spec4_product31_true-unreach-call_false-termination.cil.c 2 20   680 180 - - - - 0 630    7000 2 11     500  
minepump_spec4_product32_true-unreach-call_false-termination.cil.c 2 11   520 92 - - - - 0 620    7000 2 13     510  
minepump_spec4_product49_true-unreach-call_false-termination.cil.c 0 900   1200 12000 - - - - 0 .56 43 0 .019 4.9
minepump_spec4_product50_true-unreach-call_false-termination.cil.c 2 23   850 240 - - - - 0 810    7000 2 28     630  
minepump_spec4_product51_true-unreach-call_false-termination.cil.c 2 57   1300 620 - - - - 0 670    7000 2 20     640  
minepump_spec4_product52_true-unreach-call_false-termination.cil.c 2 39   1000 370 - - - - 0 820    7000 2 24     630  
minepump_spec4_product53_true-unreach-call_false-termination.cil.c 2 20   740 170 - - - - 0 500    7000 2 29     680  
minepump_spec4_product54_true-unreach-call_false-termination.cil.c 2 20   770 200 - - - - 0 560    7000 2 31     550  
minepump_spec4_product55_true-unreach-call_false-termination.cil.c 2 65   1300 770 - - - - 0 710    7000 2 27     640  
minepump_spec4_product56_true-unreach-call_false-termination.cil.c 2 140   2500 1700 - - - - 0 670    7000 2 34     690  
minepump_spec4_product57_true-unreach-call_false-termination.cil.c 2 26   870 270 - - - - 0 640    7000 2 22     620  
minepump_spec4_product58_true-unreach-call_false-termination.cil.c 0 900   2000 12000 - - - - 0 .59 43 0 .018 4.8
minepump_spec4_product59_true-unreach-call_false-termination.cil.c 2 65   1200 760 - - - - 0 640    7000 2 34     680  
minepump_spec4_product60_true-unreach-call_false-termination.cil.c 2 64   1300 740 - - - - 0 740    7000 2 33     670  
minepump_spec4_product61_true-unreach-call_false-termination.cil.c 0 900   2400 11000 - - - - 0 .68 42 0 .019 4.8
minepump_spec4_product62_true-unreach-call_false-termination.cil.c 0 900   1600 10000 - - - - 0 .65 41 0 .019 4.8
minepump_spec4_product63_true-unreach-call_false-termination.cil.c 0 900   2500 12000 - - - - 0 .61 43 0 .019 4.9
minepump_spec4_product64_true-unreach-call_false-termination.cil.c 2 45   1100 460 - - - - 0 530    7000 2 35     710  
minepump_spec5_product01_true-unreach-call_false-termination.cil.c 0 900   1300 12000 - - - - 0 .56 43 0 .023 4.8
minepump_spec5_product02_true-unreach-call_false-termination.cil.c 0 900   1200 14000 - - - - 0 .55 41 0 .019 4.9
minepump_spec5_product03_true-unreach-call_false-termination.cil.c 2 6.3 330 52 - - - - 2 7.3  290 2 8.1   290  
minepump_spec5_product04_true-unreach-call_false-termination.cil.c 2 6.4 340 51 - - - - 2 6.6  290 2 8.6   320  
minepump_spec5_product05_true-unreach-call_false-termination.cil.c 0 900   1400 11000 - - - - 0 .67 44 0 .020 5.0
minepump_spec5_product06_true-unreach-call_false-termination.cil.c 2 7.7 420 63 - - - - 2 7.4  320 2 8.5   330  
minepump_spec5_product07_true-unreach-call_false-termination.cil.c 2 8.7 510 71 - - - - 2 9.5  340 2 9.9   360  
minepump_spec5_product08_true-unreach-call_false-termination.cil.c 2 8.9 480 79 - - - - 2 8.1  300 2 8.2   310  
minepump_spec5_product09_true-unreach-call_false-termination.cil.c 0 900   1400 11000 - - - - 0 .73 41 0 .019 4.9
minepump_spec5_product10_true-unreach-call_false-termination.cil.c 0 900   1300 12000 - - - - 0 .73 44 0 .020 4.9
minepump_spec5_product11_true-unreach-call_false-termination.cil.c 2 6.1 330 52 - - - - 2 8.0  300 2 7.9   310  
minepump_spec5_product12_true-unreach-call_false-termination.cil.c 0 900   1500 12000 - - - - 0 .54 46 0 .018 4.8
minepump_spec5_product13_true-unreach-call_false-termination.cil.c 0 900   1600 12000 - - - - 0 .69 41 0 .018 5.0
minepump_spec5_product14_true-unreach-call_false-termination.cil.c 2 8.0 470 62 - - - - 2 9.3  330 2 8.8   310  
minepump_spec5_product15_true-unreach-call_false-termination.cil.c 2 9.2 550 75 - - - - 2 9.1  300 2 7.8   300  
minepump_spec5_product16_true-unreach-call_false-termination.cil.c 2 8.9 480 75 - - - - 2 8.4  300 2 9.0   310  
minepump_spec5_product17_true-unreach-call_false-termination.cil.c 0 900   1500 12000 - - - - 0 .70 43 0 .019 4.9
minepump_spec5_product18_true-unreach-call_false-termination.cil.c 2 7.9 420 68 - - - - 2 8.7  300 2 10     340  
minepump_spec5_product19_true-unreach-call_false-termination.cil.c 2 8.7 450 70 - - - - 2 7.2  330 2 8.5   300  
minepump_spec5_product20_true-unreach-call_false-termination.cil.c 2 11   500 78 - - - - 2 8.5  300 2 9.4   360  
minepump_spec5_product21_true-unreach-call_false-termination.cil.c 0 900   1600 12000 - - - - 0 .64 43 0 .018 5.0
minepump_spec5_product22_true-unreach-call_false-termination.cil.c 2 8.8 470 72 - - - - 2 8.6  370 2 9.5   380  
minepump_spec5_product23_true-unreach-call_false-termination.cil.c 2 10   530 98 - - - - 2 9.7  380 2 8.3   300  
minepump_spec5_product24_true-unreach-call_false-termination.cil.c 2 9.7 520 83 - - - - 2 7.5  380 2 8.3   340  
minepump_spec5_product25_true-unreach-call_false-termination.cil.c 0 900   1500 12000 - - - - 0 .62 43 0 .024 4.8
minepump_spec5_product26_true-unreach-call_false-termination.cil.c 2 7.3 470 62 - - - - 2 9.5  300 2 6.1   370  
minepump_spec5_product27_true-unreach-call_false-termination.cil.c 2 9.8 510 86 - - - - 2 9.5  300 2 10     350  
minepump_spec5_product28_true-unreach-call_false-termination.cil.c 2 8.9 540 82 - - - - 2 6.9  330 2 8.3   310  
minepump_spec5_product29_true-unreach-call_false-termination.cil.c 0 900   1500 11000 - - - - 0 .54 43 0 .019 4.8
minepump_spec5_product30_true-unreach-call_false-termination.cil.c 2 9.2 460 76 - - - - 2 8.8  320 2 11     460  
minepump_spec5_product31_true-unreach-call_false-termination.cil.c 2 10   640 85 - - - - 2 10    390 2 7.8   290  
minepump_spec5_product32_true-unreach-call_false-termination.cil.c 2 11   630 94 - - - - 2 8.9  390 2 8.0   300  
minepump_spec5_product33_true-unreach-call_false-termination.cil.c 2 40   1100 450 - - - - 2 8.6  300 2 16     550  
minepump_spec5_product34_true-unreach-call_false-termination.cil.c 0 900   2100 11000 - - - - 0 .63 42 0 .019 4.9
minepump_spec5_product35_true-unreach-call_false-termination.cil.c 0 900   2300 13000 - - - - 0 .41 43 0 .019 4.9
minepump_spec5_product36_true-unreach-call_false-termination.cil.c 0 900   4200 14000 - - - - 0 .61 44 0 .018 4.8
minepump_spec5_product37_true-unreach-call_false-termination.cil.c 0 900   1400 9300 - - - - 0 .63 43 0 .019 5.0
minepump_spec5_product38_true-unreach-call_false-termination.cil.c 0 900   2300 14000 - - - - 0 .53 43 0 .019 4.8
minepump_spec5_product39_true-unreach-call_false-termination.cil.c 0 900   2300 12000 - - - - 0 .69 41 0 .019 4.9
minepump_spec5_product40_true-unreach-call_false-termination.cil.c 0 900   3500 11000 - - - - 0 .73 42 0 .018 4.8
minepump_spec5_product41_true-unreach-call_false-termination.cil.c 0 900   4500 11000 - - - - 0 .57 43 0 .018 5.0
minepump_spec5_product42_true-unreach-call_false-termination.cil.c 0 900   1600 12000 - - - - 0 .72 44 0 .018 4.9
minepump_spec5_product43_true-unreach-call_false-termination.cil.c 0 900   2800 11000 - - - - 0 .65 42 0 .019 4.8
minepump_spec5_product44_true-unreach-call_false-termination.cil.c 0 900   2000 14000 - - - - 0 .64 41 0 .019 4.9
minepump_spec5_product45_true-unreach-call_false-termination.cil.c 0 900   1400 12000 - - - - 0 .54 42 0 .019 4.8
minepump_spec5_product46_true-unreach-call_false-termination.cil.c 0 900   1700 11000 - - - - 0 .60 41 0 .020 4.9
minepump_spec5_product47_true-unreach-call_false-termination.cil.c 0 900   1900 11000 - - - - 0 .73 43 0 .018 4.8
minepump_spec5_product48_true-unreach-call_false-termination.cil.c 0 900   3100 13000 - - - - 0 .50 41 0 .019 4.9
minepump_spec5_product49_true-unreach-call_false-termination.cil.c 0 900   1500 12000 - - - - 0 .74 43 0 .020 4.8
minepump_spec5_product50_true-unreach-call_false-termination.cil.c 0 900   2000 12000 - - - - 0 .69 43 0 .019 4.9
minepump_spec5_product51_true-unreach-call_false-termination.cil.c 0 900   1500 14000 - - - - 0 .52 43 0 .017 4.9
minepump_spec5_product52_true-unreach-call_false-termination.cil.c 0 900   2300 11000 - - - - 0 .66 43 0 .017 4.8
minepump_spec5_product53_true-unreach-call_false-termination.cil.c 0 900   1400 9600 - - - - 0 .58 42 0 .018 4.9
minepump_spec5_product54_true-unreach-call_false-termination.cil.c 0 900   2400 10000 - - - - 0 .54 42 0 .018 4.8
minepump_spec5_product55_true-unreach-call_false-termination.cil.c 0 900   2500 13000 - - - - 0 .57 43 0 .019 4.9
minepump_spec5_product56_true-unreach-call_false-termination.cil.c 0 900   2300 13000 - - - - 0 .52 44 0 .019 4.9
minepump_spec5_product57_true-unreach-call_false-termination.cil.c 0 900   1400 12000 - - - - 0 .72 41 0 .018 4.9
minepump_spec5_product58_true-unreach-call_false-termination.cil.c 0 900   2900 11000 - - - - 0 .67 42 0 .019 5.0
minepump_spec5_product59_true-unreach-call_false-termination.cil.c 0 900   2600 12000 - - - - 0 .70 45 0 .017 4.9
minepump_spec5_product60_true-unreach-call_false-termination.cil.c 0 900   2600 14000 - - - - 0 .69 43 0 .019 4.9
minepump_spec5_product61_true-unreach-call_false-termination.cil.c 0 900   1400 10000 - - - - 0 .63 43 0 .019 4.8
minepump_spec5_product62_true-unreach-call_false-termination.cil.c 0 900   1900 14000 - - - - 0 .66 44 0 .018 4.9
minepump_spec5_product63_true-unreach-call_false-termination.cil.c 0 900   2200 15000 - - - - 0 .56 43 0 .020 5.0
minepump_spec5_product64_true-unreach-call_false-termination.cil.c 0 900   2800 14000 - - - - 0 .64 43 0 .020 4.9
minepump_spec5_productSimulator_true-unreach-call_false-termination.cil.c 0 900   5500 13000 - - - - 0 .57 44 0 .022 5.0
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
total 597 440 300000 1400000 4000000 265 -2880 480 31000 265 90 720 30000 265 0 560 28000 265 80 74 1800 332 108 87000 850000 332 350 2400 78000
    correct results 265 440 4300 150000 42000 0 90 90 720 29000 0 80 80 65 1500 54 108 640 20000 175 350 2400 77000
        correct true 175 350 2800 110000 27000 0 0 0 0 54 108 640 20000 175 350 2400 77000
        correct false 90 90 1400 47000 15000 0 90 90 720 29000 0 80 80 65 1500 0 0
    incorrect results 0 90 -2880 380 24000 0 0 0 0 0
        incorrect true 0 90 -2880 380 24000 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (597 tasks, max score: 929) 440 -2880 90 0 80 108 350
Run set ukojak.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-ProductLines