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