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