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