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     - ---