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