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