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