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