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