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