Tool CBMC 5.8 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 11:20:26 CET 2017-12-01 07:26:01 CET 2017-12-01 07:56:00 CET 2017-12-01 08:08:00 CET 2017-12-01 08:15:34 CET 2017-12-01 04:22:29 CET 2017-12-01 07:31:28 CET
Run set cbmc.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cbmc.2017-11-30_1120.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 .45 42 4.5 true -32 wit inspect 8.7  410 true -32 wit inspect 10     450   unknown 0 wit inspect 25    1600 false(unreach-call) 1 wit inspect 1.3    20    - wit inspect - wit inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 42 4.9 true -32 wit inspect 9.2  410 true -32 wit inspect 10     450   unknown 0 wit inspect 26    1500 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .47 42 4.3 true -32 wit inspect 9.5  430 true -32 wit inspect 10     450   unknown 0 wit inspect 27    1600 false(unreach-call) 1 wit inspect 1.0    20    - wit inspect - wit inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .47 42 4.6 true -32 wit inspect 9.0  410 true -32 wit inspect 10     460   unknown 0 wit inspect 26    1500 false(unreach-call) 1 wit inspect 1.4    20    - wit inspect - wit inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11    450 110   true -32 wit inspect 5.6  280 true -32 wit inspect 9.1   420   unknown 0 wit inspect 29    2000 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 13   true -32 wit inspect 6.5  280 true -32 wit inspect 8.2   370   unknown 0 wit inspect 18    1300 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 13   true -32 wit inspect 7.1  300 true -32 wit inspect 9.7   410   unknown 0 wit inspect 35    1700 false(unreach-call) 1 wit inspect 1.5    20    - wit inspect - wit inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 12   true -32 wit inspect 6.2  280 true -32 wit inspect 8.6   410   unknown 0 wit inspect 25    1700 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  43 16   true -32 wit inspect 7.2  280 true -32 wit inspect 9.6   400   unknown 0 wit inspect 31    2000 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 14   true -32 wit inspect 6.4  290 true -32 wit inspect 8.8   380   unknown 0 wit inspect 28    1600 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 13   true -32 wit inspect 6.3  280 true -32 wit inspect 10     390   unknown 0 wit inspect 29    2000 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 12   true -32 wit inspect 6.6  300 true -32 wit inspect 9.5   380   unknown 0 wit inspect 26    1700 false(unreach-call) 1 wit inspect 1.4    20    - wit inspect - wit inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  43 16   true -32 wit inspect 7.4  300 true -32 wit inspect 9.0   420   unknown 0 wit inspect 30    2100 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 85    1200 760   true -32 wit inspect 6.3  280 true -32 wit inspect 10     430   unknown 0 wit inspect 34    1900 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 1.2  42 12   true -32 wit inspect 8.4  340 true -32 wit inspect 9.0   390   unknown 0 wit inspect 24    1200 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 12   true -32 wit inspect 9.7  430 true -32 wit inspect 11     410   unknown 0 wit inspect 28    1800 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 12   true -32 wit inspect 9.8  320 true -32 wit inspect 10     380   unknown 0 wit inspect 29    1600 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  43 13   true -32 wit inspect 12    430 true -32 wit inspect 8.7   410   unknown 0 wit inspect 39    1900 false(unreach-call) 1 wit inspect 1.4    20    - wit inspect - wit inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 11   true -32 wit inspect 7.9  320 true -32 wit inspect 8.9   380   unknown 0 wit inspect 23    1600 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 13   true -32 wit inspect 10    410 true -32 wit inspect 9.5   410   unknown 0 wit inspect 31    1900 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 14   true -32 wit inspect 7.7  300 true -32 wit inspect 9.1   390   unknown 0 wit inspect 27    1800 false(unreach-call) 1 wit inspect 1.3    20    - wit inspect - wit inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  43 14   true -32 wit inspect 9.4  430 true -32 wit inspect 9.2   410   unknown 0 wit inspect 33    2200 false(unreach-call) 1 wit inspect 1.1    21    - wit inspect - wit inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 48    930 380   true -32 wit inspect 5.4  280 true -32 wit inspect 8.3   430   unknown 0 wit inspect 32    2100 false(unreach-call) 1 wit inspect 1.5    21    - wit inspect - wit inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 43 6.4 true -32 wit inspect 8.1  280 true -32 wit inspect 9.3   460   unknown 0 wit inspect 39    2000 false(unreach-call) 1 wit inspect 1.1    21    - wit inspect - wit inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .61 43 5.7 true -32 wit inspect 6.9  280 true -32 wit inspect 12     450   unknown 0 wit inspect 32    2200 false(unreach-call) 1 wit inspect 1.1    21    - wit inspect - wit inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .66 43 7.3 true -32 wit inspect 6.6  280 true -32 wit inspect 8.8   460   unknown 0 wit inspect 32    2000 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 .67 43 7.1 true -32 wit inspect 6.6  280 true -32 wit inspect 12     460   unknown 0 wit inspect 43    2300 false(unreach-call) 1 wit inspect 1.1    22    - wit inspect - wit inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .68 44 6.4 true -32 wit inspect 7.5  280 true -32 wit inspect 9.0   460   unknown 0 wit inspect 48    2200 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .69 44 8.0 true -32 wit inspect 7.2  310 true -32 wit inspect 9.9   460   unknown 0 wit inspect 39    2100 false(unreach-call) 1 wit inspect 1.3    22    - wit inspect - wit inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .64 43 6.4 true -32 wit inspect 6.8  280 true -32 wit inspect 9.2   460   unknown 0 wit inspect 41    2200 false(unreach-call) 1 wit inspect 1.4    21    - wit inspect - wit inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .64 43 7.5 true -32 wit inspect 7.4  280 true -32 wit inspect 9.2   450   unknown 0 wit inspect 31    2300 false(unreach-call) 1 wit inspect 1.2    22    - wit inspect - wit inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .68 44 7.2 true -32 wit inspect 7.3  280 true -32 wit inspect 12     460   unknown 0 wit inspect 36    2300 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 44 8.1 true -32 wit inspect 6.9  290 true -32 wit inspect 9.9   460   unknown 0 wit inspect 48    2500 false(unreach-call) 1 wit inspect 1.2    22    - wit inspect - wit inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 43    950 410   true -32 wit inspect 6.4  280 true -32 wit inspect 9.1   470   unknown 0 wit inspect 51    2500 false(unreach-call) 1 wit inspect 1.2    22    - wit inspect - wit inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  44 13   true -32 wit inspect 9.9  350 true -32 wit inspect 11     400   unknown 0 wit inspect 27    1800 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  42 14   true -32 wit inspect 10    430 true -32 wit inspect 9.1   390   unknown 0 wit inspect 31    1800 false(unreach-call) 1 wit inspect 1.1    21    - wit inspect - wit inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 13   true -32 wit inspect 8.6  310 true -32 wit inspect 8.6   380   unknown 0 wit inspect 29    1800 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  42 13   true -32 wit inspect 9.8  410 true -32 wit inspect 9.0   390   unknown 0 wit inspect 31    2200 false(unreach-call) 1 wit inspect 1.6    21    - wit inspect - wit inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 47    930 450   true -32 wit inspect 7.1  270 true -32 wit inspect 12     450   unknown 0 wit inspect 51    2400 true -32 wit inspect 1.3    21    - wit inspect - wit inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    12000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.8
elevator_spec13_product22_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    12000 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.8
elevator_spec13_product23_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 750    15000 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .023 4.9
elevator_spec13_product24_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 760    15000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .024 4.8
elevator_spec13_product29_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 880    12000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.8
elevator_spec13_product30_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 880    12000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .042 4.8
elevator_spec13_product31_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 750    15000 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .020 4.9
elevator_spec13_product32_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 750    15000 9800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 4.9
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    460 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .048 4.8
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.3  47 37   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 300     7000  
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.3  47 42   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 280     7000  
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.4  47 37   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 280     7000  
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  47 44   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 220     7000  
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  47 40   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 290     7000  
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.4  47 44   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 200     7000  
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect 2.8  45 27   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 270     7000  
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.0  45 34   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 250     7000  
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect 2.8  45 36   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 340     7000  
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.1  45 33   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 260     7000  
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect 2.9  45 30   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 270     7000  
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.1  46 45   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 230     7000  
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.0  45 39   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 240     7000  
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.2  47 39   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 240     7000  
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.0  45 33   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 out of memory 0 wit inspect 200     7000  
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.1  46 37   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 270     7000  
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.1  46 39   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 190     7000  
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.3  47 41   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 270     7000  
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  42 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 150     7000  
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  42 22   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960    5500 out of memory 0 wit inspect 160     7000  
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.5  42 16   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 140     7000  
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 170     7000  
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  42 16   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 940    5500 out of memory 0 wit inspect 130     7000  
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  43 20   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 200     7000  
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  43 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 140     7000  
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 16   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 230     7000  
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  42 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 940    5500 out of memory 0 wit inspect 140     7000  
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 17   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 150     7000  
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 17   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 130     7000  
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.8  43 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 150     7000  
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  47 40   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 150     7000  
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  47 40   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 160     7000  
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  47 37   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 190     7000  
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.6  47 41   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5400 out of memory 0 wit inspect 160     7000  
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.9  50 42   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 140     7000  
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 1 wit inspect 4.0  49 46   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 240     7000  
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.6  47 44   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 170     7000  
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.6  48 50   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5400 out of memory 0 wit inspect 200     7000  
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.9  50 47   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 110     7000  
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 1 wit inspect 4.0  50 52   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 210     7000  
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.5  42 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    5500 out of memory 0 wit inspect 190     7000  
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  44 17   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 140     7000  
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  42 19   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    5500 out of memory 0 wit inspect 180     7000  
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 130     7000  
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 16   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 180     7000  
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.8  43 17   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 140     7000  
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.1  55 25   true -32 wit inspect 13    410 true -32 wit inspect 8.9   400   unknown 0 wit inspect 9.3  310 true -32 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.5  64 70   true -32 wit inspect 5.9  280 true -32 wit inspect 9.2   430   unknown 0 wit inspect 9.6  400 true -32 wit inspect 1.3    21    - wit inspect - wit inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1  56 32   true -32 wit inspect 12    410 true -32 wit inspect 9.8   410   unknown 0 wit inspect 10    420 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.0  65 57   true -32 wit inspect 6.7  270 true -32 wit inspect 9.8   440   unknown 0 wit inspect 9.5  430 true -32 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.4  57 37   true -32 wit inspect 13    440 true -32 wit inspect 10     420   unknown 0 wit inspect 8.3  420 true -32 wit inspect 1.3    20    - wit inspect - wit inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.6  60 41   true -32 wit inspect 5.8  280 true -32 wit inspect 8.9   440   unknown 0 wit inspect 7.4  430 true -32 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.0  76 64   true -32 wit inspect 6.5  280 true -32 wit inspect 11     470   unknown 0 wit inspect 12    470 true -32 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.4  77 73   true -32 wit inspect 17    590 true -32 wit inspect 7.7   470   unknown 0 wit inspect 9.2  430 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c error (42) 0 wit inspect 870    1800 5200   error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0019 .29 - wit inspect - wit inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.0  56 34   true -32 wit inspect 6.4  260 true -32 wit inspect 8.5   370   unknown 0 wit inspect 7.2  290 true -32 wit inspect 1.3    20    - wit inspect - wit inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.1  63 42   true -32 wit inspect 5.6  260 true -32 wit inspect 9.3   410   unknown 0 wit inspect 9.2  430 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.1  56 31   true -32 wit inspect 7.5  290 true -32 wit inspect 10     420   unknown 0 wit inspect 8.8  310 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.9  65 54   true -32 wit inspect 6.9  270 true -32 wit inspect 9.0   410   unknown 0 wit inspect 11    410 false(unreach-call) 1 wit inspect 1.4    20    - wit inspect - wit inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.2  57 41   true -32 wit inspect 6.7  290 true -32 wit inspect 8.1   410   unknown 0 wit inspect 8.4  420 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.3  70 62   true -32 wit inspect 6.0  280 true -32 wit inspect 11     450   unknown 0 wit inspect 11    420 false(unreach-call) 1 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.5  58 38   true -32 wit inspect 5.9  270 true -32 wit inspect 11     420   unknown 0 wit inspect 7.7  360 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.5  77 77   true -32 wit inspect 7.0  270 true -32 wit inspect 9.4   470   unknown 0 wit inspect 11    480 true -32 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c error (42) 0 wit inspect 870    2200 5000   error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.8  55 37   true -32 wit inspect 6.3  270 true -32 wit inspect 8.8   400   unknown 0 wit inspect 8.7  420 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.8  54 29   true -32 wit inspect 5.8  270 true -32 wit inspect 8.7   400   unknown 0 wit inspect 10    450 true -32 wit inspect 1.5    20    - wit inspect - wit inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.0  54 35   true -32 wit inspect 9.2  280 true -32 wit inspect 8.7   410   unknown 0 wit inspect 12    470 true -32 wit inspect 1.3    21    - wit inspect - wit inspect
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.1  61 46   true -32 wit inspect 15    490 true -32 wit inspect 8.5   420   unknown 0 wit inspect 12    410 true -32 wit inspect 1.1    21    - wit inspect - wit inspect
email_spec1_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.6  63 50   true -32 wit inspect 20    580 true -32 wit inspect 9.5   430   unknown 0 wit inspect 11    470 false(unreach-call) 1 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1  56 32   true -32 wit inspect 6.8  270 true -32 wit inspect 11     400   unknown 0 wit inspect 8.9  420 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.9  64 62   true -32 wit inspect 6.2  290 true -32 wit inspect 11     420   unknown 0 wit inspect 11    370 false(unreach-call) 1 wit inspect 1.5    20    - wit inspect - wit inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.3  56 42   true -32 wit inspect 7.5  280 true -32 wit inspect 9.3   440   unknown 0 wit inspect 11    380 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.2  54 33   true -32 wit inspect 5.8  270 true -32 wit inspect 9.8   390   unknown 0 wit inspect 9.5  420 false(unreach-call) 1 wit inspect 1.3    20    - wit inspect - wit inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.4  56 41   true -32 wit inspect 15    390 true -32 wit inspect 8.5   430   unknown 0 wit inspect 11    470 error (2) 0 wit inspect 1.4    21    - wit inspect - wit inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.2  67 60   true -32 wit inspect 6.1  280 true -32 wit inspect 9.6   430   unknown 0 wit inspect 15    470 true -32 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.6  56 41   true -32 wit inspect 6.0  270 true -32 wit inspect 11     440   unknown 0 wit inspect 12    460 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.0  72 66   true -32 wit inspect 5.9  280 true -32 wit inspect 9.9   460   unknown 0 wit inspect 11    470 true -32 wit inspect 1.5    20    - wit inspect - wit inspect
email_spec1_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.4  74 94   true -32 wit inspect 7.4  280 true -32 wit inspect 8.8   450   unknown 0 wit inspect 19    880 true -32 wit inspect 1.5    22    - wit inspect - wit inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130    640 1700   true -32 wit inspect 5.9  280 true -32 wit inspect 11     460   unknown 0 wit inspect 15    610 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1  57 34   true -32 wit inspect 6.1  270 unknown 0 wit inspect 50     640   unknown 0 wit inspect 9.4  430 false(unreach-call) 1 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0  55 34   true -32 wit inspect 6.0  270 true -32 wit inspect 8.1   380   unknown 0 wit inspect 9.5  370 false(unreach-call) 1 wit inspect 1.4    20    - wit inspect - wit inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1  57 34   true -32 wit inspect 6.4  270 true -32 wit inspect 10     420   unknown 0 wit inspect 12    420 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.4  63 46   true -32 wit inspect 20    400 unknown 0 wit inspect 42     790   unknown 0 wit inspect 12    370 true -32 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.2  57 35   true -32 wit inspect 13    420 true -32 wit inspect 10     400   unknown 0 wit inspect 11    380 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec27_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.9  66 59   true -32 wit inspect 18    500 true -32 wit inspect 8.6   430   unknown 0 wit inspect 13    400 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec27_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.3  68 57   true -32 wit inspect 15    470 true -32 wit inspect 11     470   unknown 0 wit inspect 19    680 error (2) 0 wit inspect 1.6    22    - wit inspect - wit inspect
email_spec27_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.4  59 42   true -32 wit inspect 13    450 true -32 wit inspect 11     430   unknown 0 wit inspect 6.6  470 true -32 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec27_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.4  58 36   true -32 wit inspect 6.0  280 true -32 wit inspect 9.1   410   unknown 0 wit inspect 15    470 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec27_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.5  58 44   true -32 wit inspect 12    420 true -32 wit inspect 10     440   unknown 0 wit inspect 12    470 true -32 wit inspect 1.4    21    - wit inspect - wit inspect
email_spec27_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.6  72 62   true -32 wit inspect 6.3  290 true -32 wit inspect 13     490   unknown 0 wit inspect 16    740 error (2) 0 wit inspect 1.2    22    - wit inspect - wit inspect
email_spec27_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.7  59 43   true -32 wit inspect 17    470 true -32 wit inspect 9.9   430   unknown 0 wit inspect 15    590 error (2) 0 wit inspect 1.3    21    - wit inspect - wit inspect
email_spec27_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.4  76 71   true -32 wit inspect 25    640 true -32 wit inspect 8.9   480   unknown 0 wit inspect 13    410 false(unreach-call) 1 wit inspect 1.4    21    - wit inspect - wit inspect
email_spec27_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.9  79 80   true -32 wit inspect 7.6  280 true -32 wit inspect 9.6   460   unknown 0 wit inspect 13    550 true -32 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 340    920 2600   true -32 wit inspect 7.4  280 true -32 wit inspect 12     460   unknown 0 wit inspect 14    600 error (2) 0 wit inspect 1.6    22    - wit inspect - wit inspect
email_spec3_product13_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .84 45 8.4 true -32 wit inspect 6.5  260 unknown 0 wit inspect 32     510   unknown 0 wit inspect 8.1  320 false(unreach-call) 1 wit inspect 1.0    20    - wit inspect - wit inspect
email_spec3_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.0  50 12   true -32 wit inspect 6.4  270 unknown 0 wit inspect 28     570   unknown 0 wit inspect 8.6  290 false(unreach-call) 1 wit inspect 1.1    19    - wit inspect - wit inspect
email_spec3_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .98 48 10   true -32 wit inspect 5.7  270 unknown 0 wit inspect 27     540   unknown 0 wit inspect 7.5  310 false(unreach-call) 1 wit inspect 1.0    20    - wit inspect - wit inspect
email_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .99 49 10   true -32 wit inspect 5.4  270 unknown 0 wit inspect 29     520   unknown 0 wit inspect 6.5  290 false(unreach-call) 1 wit inspect 1.0    20    - wit inspect - wit inspect
email_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.5  60 18   true -32 wit inspect 6.8  270 unknown 0 wit inspect 30     570   unknown 0 wit inspect 7.5  280 false(unreach-call) 1 wit inspect 1.3    19    - wit inspect - wit inspect
email_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.1  49 11   true -32 wit inspect 6.2  270 unknown 0 wit inspect 29     530   unknown 0 wit inspect 6.8  310 false(unreach-call) 1 wit inspect 1.1    19    - wit inspect - wit inspect
email_spec3_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.6  60 22   true -32 wit inspect 6.0  260 unknown 0 wit inspect 30     580   unknown 0 wit inspect 7.6  280 false(unreach-call) 1 wit inspect 1.0    19    - wit inspect - wit inspect
email_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.7  60 19   true -32 wit inspect 5.5  270 unknown 0 wit inspect 31     550   unknown 0 wit inspect 7.6  280 false(unreach-call) 1 wit inspect 1.3    19    - wit inspect - wit inspect
email_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .90 47 8.3 true -32 wit inspect 5.6  270 unknown 0 wit inspect 32     530   unknown 0 wit inspect 6.5  280 false(unreach-call) 1 wit inspect 1.3    20    - wit inspect - wit inspect
email_spec3_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.1  54 13   true -32 wit inspect 5.8  270 unknown 0 wit inspect 37     570   unknown 0 wit inspect 7.6  330 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec3_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.1  51 13   true -32 wit inspect 5.4  270 unknown 0 wit inspect 29     580   unknown 0 wit inspect 6.6  280 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.1  50 13   true -32 wit inspect 6.2  260 unknown 0 wit inspect 30     570   unknown 0 wit inspect 6.8  280 false(unreach-call) 1 wit inspect 1.5    20    - wit inspect - wit inspect
email_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.8  63 21   true -32 wit inspect 5.6  270 unknown 0 wit inspect 30     580   unknown 0 wit inspect 7.1  280 false(unreach-call) 1 wit inspect 1.3    20    - wit inspect - wit inspect
email_spec3_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  52 13   true -32 wit inspect 14    450 unknown 0 wit inspect 27     570   unknown 0 wit inspect 7.2  360 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec3_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.1  68 26   true -32 wit inspect 26    610 unknown 0 wit inspect 33     590   unknown 0 wit inspect 7.9  390 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec3_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.2  69 30   true -32 wit inspect 13    620 unknown 0 wit inspect 39     800   unknown 0 wit inspect 8.8  350 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 47    670 390   true -32 wit inspect 6.3  270 unknown 0 wit inspect 37     850   unknown 0 wit inspect 7.2  280 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec4_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.0  54 30   true -32 wit inspect 6.1  290 true -32 wit inspect 8.2   400   unknown 0 wit inspect 8.9  430 true -32 wit inspect 1.4    20    - wit inspect - wit inspect
email_spec4_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0  55 33   true -32 wit inspect 12    300 true -32 wit inspect 11     410   unknown 0 wit inspect 9.9  430 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec4_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.2  61 51   true -32 wit inspect 6.3  270 true -32 wit inspect 11     430   unknown 0 wit inspect 14    470 true -32 wit inspect 1.4    21    - wit inspect - wit inspect
email_spec4_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.1  54 32   true -32 wit inspect 6.0  270 true -32 wit inspect 8.8   420   unknown 0 wit inspect 13    400 true -32 wit inspect 1.5    20    - wit inspect - wit inspect
email_spec4_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.5  63 65   true -32 wit inspect 18    580 true -32 wit inspect 10     460   unknown 0 wit inspect 15    470 true -32 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec4_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.9  64 51   true -32 wit inspect 7.5  280 true -32 wit inspect 10     470   unknown 0 wit inspect 17    600 true -32 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec4_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.2  55 33   true -32 wit inspect 6.2  280 true -32 wit inspect 8.4   410   unknown 0 wit inspect 12    430 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec4_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.4  56 41   true -32 wit inspect 13    470 true -32 wit inspect 9.2   420   unknown 0 wit inspect 11    370 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec4_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.2  67 59   true -32 wit inspect 6.1  290 true -32 wit inspect 11     420   unknown 0 wit inspect 14    530 true -32 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec4_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.5  57 36   true -32 wit inspect 6.1  290 true -32 wit inspect 10     440   unknown 0 wit inspect 11    390 true -32 wit inspect 1.5    20    - wit inspect - wit inspect
email_spec4_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.0  71 90   true -32 wit inspect 6.0  290 true -32 wit inspect 9.5   470   unknown 0 wit inspect 17    910 false(unreach-call) 1 wit inspect 1.4    22    - wit inspect - wit inspect
email_spec4_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.4  76 81   true -32 wit inspect 6.2  280 true -32 wit inspect 11     460   unknown 0 wit inspect 18    950 true -32 wit inspect 1.5    22    - wit inspect - wit inspect
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 130    640 1300   true -32 wit inspect 6.1  300 true -32 wit inspect 10     460   unknown 0 wit inspect 16    610 true -32 wit inspect 1.3    21    - wit inspect - wit inspect
email_spec6_product12_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.6  53 27   true -32 wit inspect 9.1  280 true -32 wit inspect 9.2   370   unknown 0 wit inspect 9.8  320 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec6_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0  56 39   true -32 wit inspect 6.6  270 true -32 wit inspect 9.8   400   unknown 0 wit inspect 8.2  310 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec6_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.9  56 31   true -32 wit inspect 5.7  270 true -32 wit inspect 7.9   390   unknown 0 wit inspect 8.6  420 error (2) 0 wit inspect 1.3    20    - wit inspect - wit inspect
email_spec6_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.1  54 36   true -32 wit inspect 5.3  260 true -32 wit inspect 8.5   410   unknown 0 wit inspect 7.7  340 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec6_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.5  64 51   true -32 wit inspect 17    520 true -32 wit inspect 11     420   unknown 0 wit inspect 14    410 error (2) 0 wit inspect 1.4    21    - wit inspect - wit inspect
email_spec6_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.8  66 54   true -32 wit inspect 5.6  270 true -32 wit inspect 9.0   420   unknown 0 wit inspect 9.1  420 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec6_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.2  56 35   true -32 wit inspect 6.2  260 true -32 wit inspect 9.5   400   unknown 0 wit inspect 9.2  360 false(unreach-call) 1 wit inspect 1.1    19    - wit inspect - wit inspect
email_spec6_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.3  68 65   true -32 wit inspect 7.7  270 true -32 wit inspect 11     460   unknown 0 wit inspect 11    470 error (2) 0 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec6_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.6  53 27   true -32 wit inspect 6.6  270 true -32 wit inspect 8.1   410   unknown 0 wit inspect 7.7  390 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec6_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.5  59 41   true -32 wit inspect 6.0  280 true -32 wit inspect 9.4   460   unknown 0 wit inspect 11    420 error (2) 0 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec6_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.2  58 30   true -32 wit inspect 5.9  270 true -32 wit inspect 14     390   unknown 0 wit inspect 7.2  280 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec6_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.5  59 32   true -32 wit inspect 14    450 true -32 wit inspect 11     430   unknown 0 wit inspect 11    430 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec6_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.4  69 71   true -32 wit inspect 18    590 true -32 wit inspect 11     460   unknown 0 wit inspect 11    470 error (2) 0 wit inspect 1.1    21    - wit inspect - wit inspect
email_spec6_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.5  58 39   true -32 wit inspect 7.3  270 true -32 wit inspect 12     430   unknown 0 wit inspect 9.4  420 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec6_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.3  75 73   true -32 wit inspect 6.3  280 true -32 wit inspect 12     470   unknown 0 wit inspect 14    380 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 6.7  77 73   true -32 wit inspect 17    570 true -32 wit inspect 11     480   unknown 0 wit inspect 11    320 true -32 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 120    650 1500   true -32 wit inspect 6.2  300 true -32 wit inspect 11     480   unknown 0 wit inspect 14    470 error (2) 0 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec7_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.6  54 37   true -32 wit inspect 6.1  260 true -32 wit inspect 8.1   400   unknown 0 wit inspect 8.6  390 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec7_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.3  57 36   true -32 wit inspect 6.1  300 true -32 wit inspect 8.7   440   unknown 0 wit inspect 9.8  320 true -32 wit inspect 1.4    20    - wit inspect - wit inspect
email_spec7_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.2  56 35   true -32 wit inspect 13    440 true -32 wit inspect 9.9   410   unknown 0 wit inspect 9.3  420 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec7_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.4  57 37   true -32 wit inspect 13    450 true -32 wit inspect 11     430   unknown 0 wit inspect 8.0  420 true -32 wit inspect 1.4    20    - wit inspect - wit inspect
email_spec7_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.1  67 76   true -32 wit inspect 6.3  280 true -32 wit inspect 12     460   unknown 0 wit inspect 12    470 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec7_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.5  57 41   true -32 wit inspect 5.8  280 true -32 wit inspect 9.5   450   unknown 0 wit inspect 14    540 error (2) 0 wit inspect 1.1    21    - wit inspect - wit inspect
email_spec7_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.0  72 78   true -32 wit inspect 19    630 true -32 wit inspect 8.6   460   unknown 0 wit inspect 9.9  460 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec7_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.3  75 92   true -32 wit inspect 24    630 true -32 wit inspect 12     460   unknown 0 wit inspect 13    610 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 150    740 1200   true -32 wit inspect 6.6  290 true -32 wit inspect 11     470   unknown 0 wit inspect 26    1300 error (2) 0 wit inspect 1.8    22    - wit inspect - wit inspect
email_spec8_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.9  53 32   true -32 wit inspect 5.7  270 true -32 wit inspect 8.2   390   unknown 0 wit inspect 8.7  310 error (2) 0 wit inspect 1.4    20    - wit inspect - wit inspect
email_spec8_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.0  55 34   true -32 wit inspect 12    410 true -32 wit inspect 9.4   400   unknown 0 wit inspect 12    470 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec8_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.2  61 49   true -32 wit inspect 16    480 true -32 wit inspect 9.3   440   unknown 0 wit inspect 13    470 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 4.7  64 52   true -32 wit inspect 6.1  270 true -32 wit inspect 9.0   450   unknown 0 wit inspect 11    410 error (2) 0 wit inspect 1.3    21    - wit inspect - wit inspect
email_spec8_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.1  55 36   true -32 wit inspect 12    420 true -32 wit inspect 8.6   420   unknown 0 wit inspect 12    460 error (2) 0 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec8_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.0  65 54   true -32 wit inspect 7.6  280 true -32 wit inspect 8.8   450   unknown 0 wit inspect 16    610 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec8_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.2  56 34   true -32 wit inspect 6.0  280 true -32 wit inspect 8.8   410   unknown 0 wit inspect 9.7  430 error (2) 0 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec8_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.4  58 41   true -32 wit inspect 14    450 true -32 wit inspect 9.5   440   unknown 0 wit inspect 15    510 error (2) 0 wit inspect 1.3    21    - wit inspect - wit inspect
email_spec8_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.3  68 51   true -32 wit inspect 6.3  280 true -32 wit inspect 9.7   460   unknown 0 wit inspect 11    460 error (2) 0 wit inspect 1.3    20    - wit inspect - wit inspect
email_spec8_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.5  55 38   true -32 wit inspect 15    460 true -32 wit inspect 9.5   460   unknown 0 wit inspect 14    610 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec8_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.1  72 68   true -32 wit inspect 6.9  290 true -32 wit inspect 12     480   unknown 0 wit inspect 17    670 error (2) 0 wit inspect 1.3    22    - wit inspect - wit inspect
email_spec8_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.4  75 90   true -32 wit inspect 6.2  280 true -32 wit inspect 11     470   unknown 0 wit inspect 17    600 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 130    640 1200   true -32 wit inspect 6.3  280 true -32 wit inspect 12     460   unknown 0 wit inspect 18    490 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 2.8  53 36   true -32 wit inspect 4.0  270 true -32 wit inspect 11     390   unknown 0 wit inspect 12    420 error (2) 0 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec9_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.0  54 31   true -32 wit inspect 9.9  350 true -32 wit inspect 8.8   410   unknown 0 wit inspect 10    430 error (2) 0 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec9_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.2  62 44   true -32 wit inspect 17    500 true -32 wit inspect 8.4   410   unknown 0 wit inspect 10    460 error (2) 0 wit inspect 1.4    21    - wit inspect - wit inspect
email_spec9_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.6  63 63   true -32 wit inspect 11    610 true -32 wit inspect 9.1   440   unknown 0 wit inspect 14    610 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec9_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.0  55 43   true -32 wit inspect 6.7  300 true -32 wit inspect 9.7   410   unknown 0 wit inspect 12    470 error (2) 0 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.0  64 56   true -32 wit inspect 5.8  280 true -32 wit inspect 8.7   440   unknown 0 wit inspect 16    600 error (2) 0 wit inspect 1.1    21    - wit inspect - wit inspect
email_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.2  55 35   true -32 wit inspect 13    300 true -32 wit inspect 8.8   420   unknown 0 wit inspect 11    470 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec9_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.5  55 43   true -32 wit inspect 14    360 true -32 wit inspect 12     460   unknown 0 wit inspect 12    410 error (2) 0 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.2  67 65   true -32 wit inspect 6.1  310 true -32 wit inspect 14     460   unknown 0 wit inspect 14    560 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec9_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.5  57 42   true -32 wit inspect 12    300 true -32 wit inspect 9.2   430   unknown 0 wit inspect 16    450 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 6.1  72 78   true -32 wit inspect 9.0  310 true -32 wit inspect 10     470   unknown 0 wit inspect 16    910 error (2) 0 wit inspect 1.4    22    - wit inspect - wit inspect
email_spec9_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.5  75 78   true -32 wit inspect 24    540 true -32 wit inspect 11     460   unknown 0 wit inspect 13    610 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 130    640 1100   true -32 wit inspect 5.8  280 true -32 wit inspect 12     460   unknown 0 wit inspect 14    600 error (2) 0 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec0_product05_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.7  42 28   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 14    470 true 2 wit inspect 11     370  
email_spec0_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.5  42 39   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 33    1500 true 2 wit inspect 12     400  
email_spec0_product10_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.8  42 30   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 26    990 true 2 wit inspect 11     390  
email_spec0_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.3  44 34   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 32    1900 true 2 wit inspect 16     510  
email_spec0_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.8  45 38   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 66    2900 true 2 wit inspect 22     520  
email_spec0_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.8  46 43   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 54    3100 true 2 wit inspect 31     740  
email_spec0_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.6  45 59   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 130    4600 true 2 wit inspect 27     630  
email_spec0_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.0  47 63   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 98    3900 true 2 wit inspect 42     950  
email_spec0_product36_true-unreach-call_true-termination.cil.c true 2 wit inspect 4.0  44 46   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 27    1400 true 2 wit inspect 15     460  
email_spec0_product37_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.4  44 34   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 59    2700 true 2 wit inspect 26     740  
email_spec0_product38_true-unreach-call_true-termination.cil.c true 2 wit inspect 4.3  47 45   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 68    3200 true 2 wit inspect 18     520  
email_spec0_product40_true-unreach-call_true-termination.cil.c true 2 wit inspect 4.6  45 62   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 67    2900 true 2 wit inspect 34     740  
email_spec11_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.5  42 24   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 21    750 true 2 wit inspect 14     460  
email_spec11_product07_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.4  42 40   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 23    1200 true 2 wit inspect 12     390  
email_spec11_product08_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.3  46 35   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 51    2600 true 2 wit inspect 18     520  
email_spec11_product10_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.7  43 34   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 17    600 true 2 wit inspect 11     370  
email_spec11_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.6  46 42   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 51    2700 true 2 wit inspect 29     610  
email_spec11_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.0  45 57   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 71    3200 true 2 wit inspect 31     700  
email_spec11_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.9  45 38   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 47    2500 true 2 wit inspect 24     600  
email_spec11_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.0  45 68   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 120    3800 true 2 wit inspect 37     610  
email_spec11_product36_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.9  42 53   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 32    1800 true 2 wit inspect 15     430  
email_spec11_product37_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.5  45 42   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 31    2000 true 2 wit inspect 25     560  
email_spec11_product39_true-unreach-call_true-termination.cil.c true 2 wit inspect 4.1  45 43   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 69    3200 true 2 wit inspect 19     510  
email_spec11_product40_true-unreach-call_true-termination.cil.c true 2 wit inspect 4.7  45 52   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 68    3100 true 2 wit inspect 20     520  
email_spec1_product12_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.2  46 34   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 47    2500 out of memory 0 wit inspect 240     7000  
email_spec1_product28_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.4  45 31   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 62    3000 out of memory 0 wit inspect 170     7000  
email_spec27_product13_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.4  52 30   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 130    4400 out of memory 0 wit inspect 230     7000  
email_spec27_product28_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  53 34   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 42    2400 out of memory 0 wit inspect 240     7000  
email_spec4_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.3  50 38   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 37    2100 true 2 wit inspect 200     5600  
email_spec4_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.8  53 43   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 77    3000 out of memory 0 wit inspect 160     7000  
email_spec4_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.4  50 45   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 80    3500 true 2 wit inspect 81     2100  
email_spec4_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 4.4  55 48   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 100    3700 out of memory 0 wit inspect 150     7000  
email_spec7_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.1  44 40   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 31    2200 true 2 wit inspect 15     500  
email_spec7_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.6  45 41   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 61    2900 true 2 wit inspect 16     510  
email_spec7_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.6  47 34   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 99    3400 true 2 wit inspect 15     520  
email_spec7_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.7  45 40   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 43    2500 true 2 wit inspect 15     480  
email_spec7_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.0  45 54   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 69    3000 true 2 wit inspect 23     530  
email_spec7_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 4.0  45 42   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 72    3600 true 2 wit inspect 19     510  
email_spec7_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.4  47 75   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 140    4800 true 2 wit inspect 19     510  
email_spec7_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.0  50 70   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 100    3700 true 2 wit inspect 24     690  
email_spec8_product12_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.1  45 31   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 140    4200 true 2 wit inspect 84     4500  
email_spec8_product14_true-unreach-call_true-termination.cil.c true 1 wit inspect 4.0  55 42   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 77    3500 out of memory 0 wit inspect 190     7000  
email_spec8_product28_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.4  45 27   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 95    3500 out of memory 0 wit inspect 150     7000  
email_spec8_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 4.4  57 44   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 130    4700 out of memory 0 wit inspect 220     7000  
email_spec9_product12_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.1  45 35   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 61    2800 true 2 wit inspect 78     4400  
email_spec9_product14_true-unreach-call_true-termination.cil.c true 1 wit inspect 4.0  55 42   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 120    4200 out of memory 0 wit inspect 140     7000  
email_spec9_product28_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.4  45 36   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 100    3300 out of memory 0 wit inspect 200     7000  
email_spec9_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 4.5  57 56   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 110    3600 out of memory 0 wit inspect 180     7000  
minepump_spec1_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 35 2.4 true -32 wit inspect 3.9  260 true -32 wit inspect 5.9   250   unknown 0 wit inspect 3.9  230 false(unreach-call) 1 wit inspect .74   19    - wit inspect - wit inspect
minepump_spec1_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 35 2.7 false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 5.3   240   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .96   19    - wit inspect - wit inspect
minepump_spec1_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 36 3.0 false(unreach-call) 1 wit inspect 3.9  270 true -32 wit inspect 6.6   240   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .83   19    - wit inspect - wit inspect
minepump_spec1_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 35 2.8 false(unreach-call) 1 wit inspect 3.9  260 true -32 wit inspect 6.3   240   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .73   19    - wit inspect - wit inspect
minepump_spec1_product37_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .34 36 3.1 false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 5.4   250   unknown 0 wit inspect 4.8  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec1_product38_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .34 36 3.7 true -32 wit inspect 5.2  260 true -32 wit inspect 6.4   250   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .99   19    - wit inspect - wit inspect
minepump_spec1_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 36 3.5 false(unreach-call) 1 wit inspect 4.0  270 true -32 wit inspect 5.3   250   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .78   18    - wit inspect - wit inspect
minepump_spec1_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .34 38 3.1 true -32 wit inspect 3.7  260 true -32 wit inspect 5.1   250   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .90   19    - wit inspect - wit inspect
minepump_spec1_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 35 2.8 true -32 wit inspect 4.4  260 true -32 wit inspect 6.1   230   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .73   19    - wit inspect - wit inspect
minepump_spec1_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .33 35 2.4 true -32 wit inspect 4.1  270 true -32 wit inspect 6.3   240   unknown 0 wit inspect 5.0  220 false(unreach-call) 1 wit inspect .73   19    - wit inspect - wit inspect
minepump_spec1_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 36 2.9 true -32 wit inspect 4.2  260 true -32 wit inspect 5.6   250   unknown 0 wit inspect 4.5  220 false(unreach-call) 1 wit inspect .92   19    - wit inspect - wit inspect
minepump_spec1_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 36 3.6 true -32 wit inspect 7.8  330 true -32 wit inspect 5.3   260   unknown 0 wit inspect 4.9  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec1_product49_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 36 3.1 false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 7.1   240   unknown 0 wit inspect 4.2  210 false(unreach-call) 1 wit inspect .87   19    - wit inspect - wit inspect
minepump_spec1_product50_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 36 3.4 true -32 wit inspect 4.0  260 true -32 wit inspect 8.2   310   unknown 0 wit inspect 5.1  220 false(unreach-call) 1 wit inspect .82   19    - wit inspect - wit inspect
minepump_spec1_product51_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .34 36 2.9 true -32 wit inspect 4.4  270 true -32 wit inspect 6.2   260   unknown 0 wit inspect 4.6  230 false(unreach-call) 1 wit inspect .91   19    - wit inspect - wit inspect
minepump_spec1_product52_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .34 36 3.0 false(unreach-call) 1 wit inspect 4.5  270 true -32 wit inspect 5.9   250   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .76   19    - wit inspect - wit inspect
minepump_spec1_product53_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .37 39 3.6 false(unreach-call) 1 wit inspect 3.8  270 true -32 wit inspect 5.6   240   unknown 0 wit inspect 3.8  220 false(unreach-call) 1 wit inspect .76   19    - wit inspect - wit inspect
minepump_spec1_product54_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .40 37 3.7 true -32 wit inspect 4.0  260 true -32 wit inspect 5.5   240   unknown 0 wit inspect 3.8  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec1_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .40 37 4.2 false(unreach-call) 1 wit inspect 4.0  270 true -32 wit inspect 5.5   250   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
minepump_spec1_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .37 39 3.6 false(unreach-call) 1 wit inspect 5.7  280 true -32 wit inspect 6.1   260   unknown 0 wit inspect 4.9  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect .67 51 8.2 true -32 wit inspect 3.9  260 true -32 wit inspect 6.8   250   unknown 0 wit inspect 5.2  240 error (2) 0 wit inspect 1.0    19    - wit inspect - wit inspect
minepump_spec2_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 36 3.3 true -32 wit inspect 3.9  260 true -32 wit inspect 6.4   240   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .87   19    - wit inspect - wit inspect
minepump_spec2_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 36 2.9 true -32 wit inspect 3.8  260 true -32 wit inspect 5.4   240   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .79   19    - wit inspect - wit inspect
minepump_spec2_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect .30 36 2.9 true -32 wit inspect 3.7  260 true -32 wit inspect 5.8   240   unknown 0 wit inspect 3.6  220 error (2) 0 wit inspect .78   19    - wit inspect - wit inspect
minepump_spec2_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 36 2.7 true -32 wit inspect 3.8  260 true -32 wit inspect 5.2   250   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
minepump_spec2_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .87 38 8.0 true -32 wit inspect 5.5  270 true -32 wit inspect 6.5   240   unknown 0 wit inspect 5.2  220 false(unreach-call) 1 wit inspect .95   19    - wit inspect - wit inspect
minepump_spec2_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .88 37 8.3 true -32 wit inspect 5.8  290 true -32 wit inspect 6.0   250   unknown 0 wit inspect 4.3  220 false(unreach-call) 1 wit inspect .90   19    - wit inspect - wit inspect
minepump_spec2_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect .85 37 9.5 true -32 wit inspect 6.0  280 true -32 wit inspect 5.8   240   unknown 0 wit inspect 4.1  220 error (2) 0 wit inspect .72   19    - wit inspect - wit inspect
minepump_spec2_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .90 37 8.4 true -32 wit inspect 4.0  260 true -32 wit inspect 7.0   240   unknown 0 wit inspect 4.9  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect .69 51 8.6 true -32 wit inspect 3.8  260 true -32 wit inspect 6.4   260   unknown 0 wit inspect 4.2  220 error (2) 0 wit inspect .78   19    - wit inspect - wit inspect
minepump_spec3_product01_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .28 35 2.4 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 7.2   270   unknown 0 wit inspect 3.6  220 false(unreach-call) 1 wit inspect .91   19    - wit inspect - wit inspect
minepump_spec3_product02_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .28 35 2.8 false(unreach-call) 1 wit inspect 2.7  270 true -32 wit inspect 8.0   270   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .87   19    - wit inspect - wit inspect
minepump_spec3_product03_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 35 2.5 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 6.3   270   unknown 0 wit inspect 4.7  210 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 .27 35 2.7 true -32 wit inspect 4.0  270 true -32 wit inspect 6.6   280   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .89   19    - wit inspect - wit inspect
minepump_spec3_product05_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 35 2.5 true -32 wit inspect 3.7  260 true -32 wit inspect 6.5   270   unknown 0 wit inspect 3.6  220 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
minepump_spec3_product06_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 35 2.5 false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 9.4   320   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
minepump_spec3_product07_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .28 35 2.5 true -32 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 6.2   270   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
minepump_spec3_product08_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 35 2.4 true -32 wit inspect 4.8  260 true -32 wit inspect 10     330   unknown 0 wit inspect 4.8  210 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec3_product09_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 35 2.7 false(unreach-call) 1 wit inspect 4.1  270 false(unreach-call) 1 wit inspect 7.0   280   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
minepump_spec3_product10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .26 35 3.5 false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 8.4   280   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
minepump_spec3_product11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 35 2.4 false(unreach-call) 1 wit inspect 4.1  270 false(unreach-call) 1 wit inspect 7.1   280   unknown 0 wit inspect 4.6  210 false(unreach-call) 1 wit inspect .77   19    - wit inspect - wit inspect
minepump_spec3_product12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 35 2.4 true -32 wit inspect 4.9  260 true -32 wit inspect 7.4   290   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec3_product13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 35 2.4 false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 5.9   270   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
minepump_spec3_product14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 35 2.6 true -32 wit inspect 4.0  260 true -32 wit inspect 8.3   290   unknown 0 wit inspect 4.7  220 false(unreach-call) 1 wit inspect .86   19    - wit inspect - wit inspect
minepump_spec3_product15_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 35 2.5 false(unreach-call) 1 wit inspect 4.2  270 false(unreach-call) 1 wit inspect 7.2   270   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
minepump_spec3_product16_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .27 37 2.7 true -32 wit inspect 4.1  260 true -32 wit inspect 7.2   280   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
minepump_spec3_product17_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 36 2.5 false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 7.5   280   unknown 0 wit inspect 3.8  220 false(unreach-call) 1 wit inspect .82   19    - wit inspect - wit inspect
minepump_spec3_product18_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .28 36 3.1 false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 7.9   290   unknown 0 wit inspect 4.7  220 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
minepump_spec3_product19_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 37 2.4 false(unreach-call) 1 wit inspect 4.1  270 false(unreach-call) 1 wit inspect 6.1   280   unknown 0 wit inspect 3.9  210 false(unreach-call) 1 wit inspect .74   19    - wit inspect - wit inspect
minepump_spec3_product20_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .28 36 2.5 true -32 wit inspect 4.6  260 true -32 wit inspect 8.2   290   unknown 0 wit inspect 2.5  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec3_product21_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 35 2.7 false(unreach-call) 1 wit inspect 4.0  280 true -32 wit inspect 8.5   280   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .73   19    - wit inspect - wit inspect
minepump_spec3_product22_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 35 2.5 false(unreach-call) 1 wit inspect 3.9  270 true -32 wit inspect 6.1   270   unknown 0 wit inspect 4.4  220 false(unreach-call) 1 wit inspect .89   19    - wit inspect - wit inspect
minepump_spec3_product23_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 35 2.4 false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 6.7   270   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
minepump_spec3_product24_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 36 2.5 false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 7.4   290   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec3_product25_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 35 2.7 false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 6.0   280   unknown 0 wit inspect 3.9  210 false(unreach-call) 1 wit inspect .76   19    - wit inspect - wit inspect
minepump_spec3_product26_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 35 2.5 true -32 wit inspect 4.0  260 true -32 wit inspect 6.9   290   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .83   19    - wit inspect - wit inspect
minepump_spec3_product27_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 35 2.5 false(unreach-call) 1 wit inspect 4.7  270 false(unreach-call) 1 wit inspect 5.9   270   unknown 0 wit inspect 3.4  220 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
minepump_spec3_product28_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .27 36 3.6 true -32 wit inspect 3.8  260 true -32 wit inspect 8.0   280   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .92   19    - wit inspect - wit inspect
minepump_spec3_product29_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .28 36 2.6 false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 5.8   270   unknown 0 wit inspect 4.8  210 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
minepump_spec3_product30_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 35 2.4 false(unreach-call) 1 wit inspect 3.8  260 true -32 wit inspect 7.5   270   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .82   19    - wit inspect - wit inspect
minepump_spec3_product31_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 36 2.4 false(unreach-call) 1 wit inspect 4.9  270 false(unreach-call) 1 wit inspect 7.7   280   unknown 0 wit inspect 4.0  210 false(unreach-call) 1 wit inspect .70   19    - wit inspect - wit inspect
minepump_spec3_product32_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 36 2.6 false(unreach-call) 1 wit inspect 3.7  270 true -32 wit inspect 7.7   280   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .74   19    - wit inspect - wit inspect
minepump_spec3_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .33 35 2.7 true -32 wit inspect 3.7  260 true -32 wit inspect 6.4   240   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .73   19    - wit inspect - wit inspect
minepump_spec3_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 38 2.8 false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 6.4   250   unknown 0 wit inspect 3.6  220 false(unreach-call) 1 wit inspect .73   19    - wit inspect - wit inspect
minepump_spec3_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 38 3.1 true -32 wit inspect 3.8  270 true -32 wit inspect 5.8   240   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .81   19    - wit inspect - wit inspect
minepump_spec3_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 38 3.9 false(unreach-call) 1 wit inspect 3.9  260 true -32 wit inspect 5.4   240   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .74   19    - wit inspect - wit inspect
minepump_spec3_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 36 3.2 false(unreach-call) 1 wit inspect 5.1  270 true -32 wit inspect 6.9   260   unknown 0 wit inspect 4.4  210 false(unreach-call) 1 wit inspect .94   19    - wit inspect - wit inspect
minepump_spec3_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 36 3.5 false(unreach-call) 1 wit inspect 4.5  270 true -32 wit inspect 6.5   250   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .74   19    - wit inspect - wit inspect
minepump_spec3_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .35 37 3.5 true -32 wit inspect 3.9  260 true -32 wit inspect 6.0   260   unknown 0 wit inspect 3.8  220 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
minepump_spec3_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .35 37 4.2 false(unreach-call) 1 wit inspect 5.3  270 true -32 wit inspect 5.9   250   unknown 0 wit inspect 5.6  220 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
minepump_spec3_product51_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .35 38 2.9 false(unreach-call) 1 wit inspect 4.4  270 true -32 wit inspect 6.1   250   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
minepump_spec3_product52_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .36 36 2.9 false(unreach-call) 1 wit inspect 4.1  260 true -32 wit inspect 6.2   250   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
minepump_spec3_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .37 38 4.0 false(unreach-call) 1 wit inspect 3.6  260 true -32 wit inspect 6.7   260   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .72   18    - wit inspect - wit inspect
minepump_spec3_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .40 38 3.7 false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 5.9   250   unknown 0 wit inspect 4.8  220 false(unreach-call) 1 wit inspect .87   19    - wit inspect - wit inspect
minepump_spec3_product59_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .33 36 3.3 true -32 wit inspect 3.9  260 true -32 wit inspect 5.3   250   unknown 0 wit inspect 3.2  220 false(unreach-call) 1 wit inspect .85   19    - wit inspect - wit inspect
minepump_spec3_product60_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .35 37 3.7 false(unreach-call) 1 wit inspect 2.8  270 true -32 wit inspect 6.5   250   unknown 0 wit inspect 4.1  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec3_product63_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .39 39 4.0 false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 5.8   250   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .80   18    - wit inspect - wit inspect
minepump_spec3_product64_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .41 39 5.0 false(unreach-call) 1 wit inspect 5.0  270 true -32 wit inspect 6.2   240   unknown 0 wit inspect 4.7  260 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec3_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .69 52 7.7 true -32 wit inspect 4.2  260 true -32 wit inspect 6.0   270   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .74   19    - wit inspect - wit inspect
minepump_spec4_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .81 38 9.1 true -32 wit inspect 4.2  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 4.2  220 false(unreach-call) 1 wit inspect .79   19    - wit inspect - wit inspect
minepump_spec4_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .78 36 8.1 true -32 wit inspect 4.5  270 true -32 wit inspect 7.4   250   unknown 0 wit inspect 4.2  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec4_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .81 38 11   true -32 wit inspect 3.8  260 true -32 wit inspect 7.0   240   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .70   19    - wit inspect - wit inspect
minepump_spec4_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .85 38 7.8 true -32 wit inspect 4.9  270 true -32 wit inspect 5.4   240   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .79   18    - wit inspect - wit inspect
minepump_spec4_product37_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .90 39 9.2 true -32 wit inspect 4.0  260 true -32 wit inspect 6.7   240   unknown 0 wit inspect 4.7  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
minepump_spec4_product38_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .91 37 9.4 true -32 wit inspect 6.9  290 true -32 wit inspect 5.1   250   unknown 0 wit inspect 4.8  270 false(unreach-call) 1 wit inspect .78   19    - wit inspect - wit inspect
minepump_spec4_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect .91 38 10   true -32 wit inspect 8.0  280 true -32 wit inspect 5.2   240   unknown 0 wit inspect 5.6  270 error (2) 0 wit inspect .79   19    - wit inspect - wit inspect
minepump_spec4_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .91 40 9.8 true -32 wit inspect 4.1  270 true -32 wit inspect 5.8   270   unknown 0 wit inspect 5.3  270 false(unreach-call) 1 wit inspect .77   19    - wit inspect - wit inspect
minepump_spec4_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .84 36 8.2 true -32 wit inspect 4.0  260 true -32 wit inspect 6.9   250   unknown 0 wit inspect 4.5  220 false(unreach-call) 1 wit inspect .83   19    - wit inspect - wit inspect
minepump_spec4_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .83 38 11   true -32 wit inspect 4.2  260 true -32 wit inspect 5.8   260   unknown 0 wit inspect 4.5  220 false(unreach-call) 1 wit inspect .93   19    - wit inspect - wit inspect
minepump_spec4_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .84 38 7.7 true -32 wit inspect 4.3  260 true -32 wit inspect 5.4   240   unknown 0 wit inspect 4.0  260 false(unreach-call) 1 wit inspect .91   18    - wit inspect - wit inspect
minepump_spec4_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .88 38 7.7 true -32 wit inspect 4.9  270 true -32 wit inspect 7.0   250   unknown 0 wit inspect 4.4  220 false(unreach-call) 1 wit inspect .79   19    - wit inspect - wit inspect
minepump_spec4_product45_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .93 39 10   true -32 wit inspect 4.1  270 true -32 wit inspect 6.4   250   unknown 0 wit inspect 4.2  220 false(unreach-call) 1 wit inspect .76   19    - wit inspect - wit inspect
minepump_spec4_product46_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .94 40 10   false(unreach-call) 1 wit inspect 3.0  270 true -32 wit inspect 8.4   300   unknown 0 wit inspect 4.5  220 false(unreach-call) 1 wit inspect .97   19    - wit inspect - wit inspect
minepump_spec4_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect .94 42 9.9 true -32 wit inspect 4.5  270 true -32 wit inspect 7.4   310   unknown 0 wit inspect 4.3  220 error (2) 0 wit inspect .94   19    - wit inspect - wit inspect
minepump_spec4_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .97 40 12   false(unreach-call) 1 wit inspect 4.6  280 true -32 wit inspect 7.6   260   unknown 0 wit inspect 4.8  220 false(unreach-call) 1 wit inspect .96   19    - wit inspect - wit inspect
minepump_spec4_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 2.2  83 25   true -32 wit inspect 4.0  270 true -32 wit inspect 7.4   280   unknown 0 wit inspect 4.8  220 error (2) 0 wit inspect .77   19    - wit inspect - wit inspect
minepump_spec1_product01_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    890 4700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.8
minepump_spec1_product02_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 4700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8
minepump_spec1_product03_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    990 6500   - 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_spec1_product04_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 6500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8
minepump_spec1_product05_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    790 4100   - 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_product06_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9
minepump_spec1_product07_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    980 6200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .042 4.8
minepump_spec1_product08_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    890 5300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 5.0
minepump_spec1_product09_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    890 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 5.0
minepump_spec1_product10_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1000 7300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 4.9
minepump_spec1_product11_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 4700   - 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_spec1_product12_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 5800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9
minepump_spec1_product13_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    800 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.8
minepump_spec1_product14_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 5400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 46 error (2) 0 wit inspect .021 4.9
minepump_spec1_product15_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .022 4.9
minepump_spec1_product16_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    890 5300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 45 error (2) 0 wit inspect .020 4.8
minepump_spec1_product17_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    820 5500   - 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_product18_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .022 4.8
minepump_spec1_product19_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.9
minepump_spec1_product20_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    900 5400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .051 4.9
minepump_spec1_product21_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    800 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .048 5.0
minepump_spec1_product22_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    960 4400   - 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_spec1_product23_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1000 6800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .048 4.8
minepump_spec1_product24_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    900 5700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .020 4.9
minepump_spec1_product25_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    800 4400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.8
minepump_spec1_product26_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 4200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .023 5.0
minepump_spec1_product27_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .035 4.8
minepump_spec1_product28_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    880 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.9
minepump_spec1_product29_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    780 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 45 error (2) 0 wit inspect .018 4.9
minepump_spec1_product30_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    960 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .021 5.0
minepump_spec1_product31_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 5000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .044 4.9
minepump_spec1_product32_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    900 5000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .022 4.9
minepump_spec1_product45_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1800 6300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .019 4.9
minepump_spec1_product46_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1800 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9
minepump_spec1_product47_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2000 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .024 4.8
minepump_spec1_product48_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2000 6400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .019 4.8
minepump_spec1_product57_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 6900   - 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_spec1_product58_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 7500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .019 4.8
minepump_spec1_product59_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 6300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.8
minepump_spec1_product60_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 7500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 45 error (2) 0 wit inspect .038 4.8
minepump_spec1_product61_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3600 5700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .019 5.0
minepump_spec1_product62_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3700 5300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 5.0
minepump_spec1_product63_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3300 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .048 4.8
minepump_spec1_product64_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3300 5800   - 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_spec2_product01_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 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_spec2_product02_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    980 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .018 4.9
minepump_spec2_product03_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    970 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .032 4.9
minepump_spec2_product04_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1000 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .023 5.0
minepump_spec2_product05_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .048 4.9
minepump_spec2_product06_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    960 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 46 error (2) 0 wit inspect .018 4.9
minepump_spec2_product07_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .017 4.8
minepump_spec2_product08_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1100 6400   - 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_spec2_product09_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 5.0
minepump_spec2_product10_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
minepump_spec2_product11_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 5000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .043 4.8
minepump_spec2_product12_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    960 6100   - 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_product13_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    980 6400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .026 4.8
minepump_spec2_product14_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1000 7400   - 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_spec2_product15_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 4400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
minepump_spec2_product16_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1000 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .036 4.9
minepump_spec2_product17_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .019 4.8
minepump_spec2_product18_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    970 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8
minepump_spec2_product19_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 4300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 5.0
minepump_spec2_product20_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    990 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .021 4.8
minepump_spec2_product21_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 5300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .018 4.9
minepump_spec2_product22_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 4100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .047 4.9
minepump_spec2_product23_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    910 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .023 4.8
minepump_spec2_product24_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1000 6200   - 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_spec2_product25_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 4400   - 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_spec2_product26_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    980 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .051 4.8
minepump_spec2_product27_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 6300   - 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_spec2_product28_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    970 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .023 4.8
minepump_spec2_product29_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .018 5.0
minepump_spec2_product30_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    980 5800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .047 5.0
minepump_spec2_product31_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .018 4.9
minepump_spec2_product32_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1000 5400   - 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_product37_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1300 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .027 4.9
minepump_spec2_product38_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1400 8800   - 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_product39_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1400 6300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .020 5.0
minepump_spec2_product40_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1600 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .019 5.0
minepump_spec2_product45_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 7300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.9
minepump_spec2_product46_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 4.8
minepump_spec2_product47_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1800 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .018 4.8
minepump_spec2_product48_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2000 7100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.8
minepump_spec2_product49_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2500 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9
minepump_spec2_product50_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2600 6400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.8
minepump_spec2_product51_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1400 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9
minepump_spec2_product52_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1600 8300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .020 4.9
minepump_spec2_product53_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2800 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 5.0
minepump_spec2_product54_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2800 6500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .019 5.0
minepump_spec2_product55_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2500 5600   - 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
minepump_spec2_product56_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2600 7300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.9
minepump_spec2_product57_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 7100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9
minepump_spec2_product58_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 7500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.8
minepump_spec2_product59_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 6300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .020 4.9
minepump_spec2_product60_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 5.0
minepump_spec2_product61_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3700 6500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .020 4.9
minepump_spec2_product62_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3700 8900   - 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_product63_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3300 5600   - 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_spec2_product64_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3400 7600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 46 error (2) 0 wit inspect .040 4.9
minepump_spec3_product33_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2100 7100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 5.0
minepump_spec3_product34_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2100 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .019 4.9
minepump_spec3_product37_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1600 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .021 4.8
minepump_spec3_product38_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1600 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .018 4.9
minepump_spec3_product41_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2500 4900   - 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_spec3_product42_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2500 8800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 44 error (2) 0 wit inspect .018 4.9
minepump_spec3_product45_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2000 8500   - 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_spec3_product46_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2000 6000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 4.8
minepump_spec3_product49_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1700 7400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.9
minepump_spec3_product50_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1700 8000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .020 5.0
minepump_spec3_product53_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2500 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 5.0
minepump_spec3_product54_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2500 6600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.9
minepump_spec3_product57_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2000 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .019 4.8
minepump_spec3_product58_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2000 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9
minepump_spec3_product61_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3300 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .048 5.0
minepump_spec3_product62_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3300 7400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .020 4.8
minepump_spec4_product01_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    880 4200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .020 4.9
minepump_spec4_product02_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.9
minepump_spec4_product03_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 4100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .020 5.0
minepump_spec4_product04_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    890 3800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 4.8
minepump_spec4_product05_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    810 4200   - 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_spec4_product06_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    990 6800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 5.0
minepump_spec4_product07_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    960 4300   - 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_product08_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    890 4600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .050 4.8
minepump_spec4_product09_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    890 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.8
minepump_spec4_product10_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 4800   - 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
minepump_spec4_product11_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 4700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .021 4.9
minepump_spec4_product12_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    880 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .024 4.8
minepump_spec4_product13_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    800 3200   - 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_product14_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.9
minepump_spec4_product15_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 5000   - 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_spec4_product16_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    910 5600   - 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_spec4_product17_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    810 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .022 4.8
minepump_spec4_product18_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9
minepump_spec4_product19_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 4300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.9
minepump_spec4_product20_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    920 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.9
minepump_spec4_product21_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    790 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 45 error (2) 0 wit inspect .021 4.9
minepump_spec4_product22_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    990 6800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 46 error (2) 0 wit inspect .019 4.9
minepump_spec4_product23_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    960 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 44 error (2) 0 wit inspect .019 4.8
minepump_spec4_product24_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8
minepump_spec4_product25_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    780 5400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .019 4.9
minepump_spec4_product26_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    960 4900   - 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_spec4_product27_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    980 7800   - 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_product28_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    890 5700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .018 4.9
minepump_spec4_product29_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    790 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.9
minepump_spec4_product30_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    970 6500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .023 5.0
minepump_spec4_product31_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    960 6000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .048 4.9
minepump_spec4_product32_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    870 4300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .021 4.8
minepump_spec4_product49_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1500 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 5.0
minepump_spec4_product50_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1500 6800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .018 5.0
minepump_spec4_product51_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1400 7100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .021 4.8
minepump_spec4_product52_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1600 7800   - 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_product53_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2400 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .023 5.0
minepump_spec4_product54_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2400 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
minepump_spec4_product55_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2500 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .020 4.9
minepump_spec4_product56_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2500 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 4.9
minepump_spec4_product57_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 6600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .021 4.8
minepump_spec4_product58_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 6300   - 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_spec4_product59_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 45 error (2) 0 wit inspect .019 5.0
minepump_spec4_product60_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 8800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .018 4.9
minepump_spec4_product61_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3200 5300   - 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_spec4_product62_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3200 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .045 4.8
minepump_spec4_product63_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3300 6000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .021 5.0
minepump_spec4_product64_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3300 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .023 4.8
minepump_spec5_product01_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    910 5400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .020 4.8
minepump_spec5_product02_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    970 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .018 5.0
minepump_spec5_product03_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    970 6600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.9
minepump_spec5_product04_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    830 5300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .027 5.0
minepump_spec5_product05_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    790 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .020 4.8
minepump_spec5_product06_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
minepump_spec5_product07_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .021 4.9
minepump_spec5_product08_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    840 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8
minepump_spec5_product09_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    910 4400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .049 4.8
minepump_spec5_product10_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .018 5.0
minepump_spec5_product11_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    920 4600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.8
minepump_spec5_product12_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    820 4400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 46 error (2) 0 wit inspect .050 4.8
minepump_spec5_product13_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    790 4200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 45 error (2) 0 wit inspect .023 4.8
minepump_spec5_product14_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.8
minepump_spec5_product15_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    920 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.9
minepump_spec5_product16_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    840 4700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .044 5.0
minepump_spec5_product17_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    800 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .020 4.8
minepump_spec5_product18_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    960 5800   - 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_spec5_product19_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    950 5900   - 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_spec5_product20_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    910 7500   - 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_spec5_product21_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    830 4400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .021 4.8
minepump_spec5_product22_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .018 4.8
minepump_spec5_product23_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 5700   - 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_spec5_product24_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    850 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9
minepump_spec5_product25_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    840 5800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8
minepump_spec5_product26_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    990 6200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .023 5.0
minepump_spec5_product27_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 5400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .021 4.9
minepump_spec5_product28_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    860 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .018 4.9
minepump_spec5_product29_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    870 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .046 4.9
minepump_spec5_product30_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    940 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .018 4.8
minepump_spec5_product31_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    930 5300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .019 5.0
minepump_spec5_product32_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    850 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .018 4.8
minepump_spec5_product33_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1600 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .021 4.9
minepump_spec5_product34_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1700 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .021 5.0
minepump_spec5_product35_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1800 8400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .019 4.9
minepump_spec5_product36_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    910 9300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .025 4.8
minepump_spec5_product37_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1500 6800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9
minepump_spec5_product38_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2500 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .020 4.9
minepump_spec5_product39_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1400 7000   - 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_product40_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1600 7500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.9
minepump_spec5_product41_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 6800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 42 error (2) 0 wit inspect .019 5.0
minepump_spec5_product42_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 7600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.8
minepump_spec5_product43_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2100 7000   - 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_spec5_product44_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2100 7400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .051 4.9
minepump_spec5_product45_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1800 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .049 4.9
minepump_spec5_product46_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1800 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .023 4.8
minepump_spec5_product47_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1800 5700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 5.0
minepump_spec5_product48_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2000 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .018 5.0
minepump_spec5_product49_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1500 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .018 5.0
minepump_spec5_product50_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1500 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9
minepump_spec5_product51_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1600 7400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .031 4.9
minepump_spec5_product52_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1600 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.8
minepump_spec5_product53_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2400 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 45 error (2) 0 wit inspect .021 4.9
minepump_spec5_product54_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2400 4400   - 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_spec5_product55_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2600 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 5.0
minepump_spec5_product56_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2600 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .020 4.9
minepump_spec5_product57_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 7400   - 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_spec5_product58_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 6200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .024 4.9
minepump_spec5_product59_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 5.0
minepump_spec5_product60_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1900 7000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 4.8
minepump_spec5_product61_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3200 6200   - 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_spec5_product62_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3200 5600   - 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_spec5_product63_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3300 6000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .018 4.8
minepump_spec5_product64_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3400 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 45 error (2) 0 wit inspect .019 4.8
minepump_spec5_productSimulator_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    3100 5800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 5.0
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 301 210000 480000 1500000 265 -6964 1900 82000 265 -7478 2700 100000 265 0 3100 150000 265 -1173 280 5200 332 0 45000 400000 332 72 13000 440000
    correct results 207 243 660 13000 7200 44 44 180 12000 10 10 67 2700 0 171 171 170 3300 0 36 72 1100 34000
        correct true 36 72 140 1600 1600 0 0 0 0 0 36 72 1100 34000
        correct false 171 171 520 11000 5600 44 44 180 12000 10 10 67 2700 0 171 171 170 3300 0 0
    correct-unconfimed results 150 58 1600 14000 16000 0 0 0 0 0 0
        correct-unconfirmed true 58 58 170 2700 1900 0 0 0 0 0 0
        correct-unconfirmed false 92 0 1400 11000 14000 0 0 0 0 0 0
    incorrect results 0 219 -7008 1700 70000 234 -7488 2000 86000 0 42 -1344 53 860 0 0
        incorrect true 0 219 -7008 1700 70000 234 -7488 2000 86000 0 42 -1344 53 860 0 0
        incorrect false 0 0 0 0 0 0 0
score (597 tasks, max score: 929) 301 -6964 -7478 0 -1173 0 72
Run set cbmc.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-ProductLines