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