Tool DIVINE CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 11:06:04 CET 2018-12-08 03:24:14 CET 2018-12-08 05:17:35 CET 2018-12-08 06:43:53 CET 2018-12-12 20:24:22 CET 2018-12-08 01:45:35 CET 2018-12-08 04:38:54 CET
Run set divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/product-lines/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
elevator_spec14_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.9 8.9 440 100 0      0     false(unreach-call) 1 wit inspect 9.0  4.8  280 0   0     true -32 --- inspect 18     9.9   460   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  280 0   0      false(unreach-call) 1 --- inspect .88   .88   20    .34 0     - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 440 110 0      0     false(unreach-call) 1 wit inspect 9.2  4.9  290 0   0     true -32 --- inspect 17     9.8   500   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  270 0   0      false(unreach-call) 1 --- inspect .91   .94   20    .34 0     - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 440 85 0      0     false(unreach-call) 1 wit inspect 8.6  4.6  280 0   0     true -32 --- inspect 18     10     500   .62 0     false(unreach-call) 1 --- inspect 6.4  3.5  270 0   .086  false(unreach-call) 1 --- inspect .84   .84   20    .34 0     - --- inspect - --- inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 440 120 0      0     false(unreach-call) 1 wit inspect 8.0  4.3  290 0   0     true -32 --- inspect 15     8.8   510   .66 0     false(unreach-call) 1 --- inspect 7.7  4.2  270 0   .17   false(unreach-call) 1 --- inspect .86   .88   21    .25 0     - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 42   22   440 470 0      0     false(unreach-call) 1 wit inspect 11    6.1  440 0   0     true -32 --- inspect 21     12     470   .66 0     unknown 0 --- inspect 7.4  4.1  270 0   0      true -32 --- inspect .90   .90   20    .38 0     - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 140 0      .049 false(unreach-call) 1 wit inspect 7.5  4.0  280 0   0     true -32 --- inspect 16     9.2   510   .62 0     false(unreach-call) 1 --- inspect 6.8  3.8  270 0   0      false(unreach-call) 1 --- inspect .86   .86   20    .34 .074 - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 120 0      0     false(unreach-call) 1 wit inspect 9.1  4.9  300 0   0     true -32 --- inspect 18     10     510   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  270 0   0      false(unreach-call) 1 --- inspect .88   .88   21    .36 .074 - --- inspect - --- inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.9 9.0 430 120 0      0     false(unreach-call) 1 wit inspect 8.2  4.4  310 0   0     true -32 --- inspect 16     9.1   530   .66 0     false(unreach-call) 1 --- inspect 7.2  4.0  270 0   5.8    false(unreach-call) 1 --- inspect .90   .90   20    .35 0     - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.9 8.9 430 100 0      0     false(unreach-call) 1 wit inspect 9.5  5.1  290 0   0     true -32 --- inspect 16     9.4   530   .66 0     false(unreach-call) 1 --- inspect 7.0  3.8  270 0   0      false(unreach-call) 1 --- inspect .86   .86   20    .36 0     - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 100 0      0     false(unreach-call) 1 wit inspect 8.4  4.5  290 0   0     true -32 --- inspect 19     11     470   .66 0     false(unreach-call) 1 --- inspect 6.6  3.7  260 0   0      false(unreach-call) 1 --- inspect .89   .90   20    .35 0     - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 130 0      0     false(unreach-call) 1 wit inspect 9.0  4.9  280 0   0     true -32 --- inspect 20     11     500   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  260 0   0      false(unreach-call) 1 --- inspect .89   .90   20    .35 0     - --- inspect - --- inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.8 430 110 0      0     false(unreach-call) 1 wit inspect 8.6  4.6  290 0   0     true -32 --- inspect 17     9.4   530   .66 0     false(unreach-call) 1 --- inspect 6.8  3.8  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .36 .074 - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.8 430 110 0      0     false(unreach-call) 1 wit inspect 9.2  4.9  290 0   0     true -32 --- inspect 21     12     460   .62 0     false(unreach-call) 1 --- inspect 5.4  3.0  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .36 0     - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 73   35   440 850 0      0     false(unreach-call) 1 wit inspect 40    25    1200 0   0     true -32 --- inspect 20     11     530   .66 0     unknown 0 --- inspect 7.3  4.1  270 0   0      true -32 --- inspect .88   .88   20    .39 0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 110 0      0     false(unreach-call) 1 wit inspect 8.8  4.7  280 0   0     true -32 --- inspect 16     9.2   470   .66 0     false(unreach-call) 1 --- inspect 6.1  3.4  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .34 0     - --- inspect - --- inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.9 430 110 0      0     false(unreach-call) 1 wit inspect 8.4  4.5  290 0   0     true -32 --- inspect 18     10     520   .66 0     false(unreach-call) 1 --- inspect 7.1  3.9  270 0   0      false(unreach-call) 1 --- inspect .88   .87   20    .36 0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 430 100 0      0     false(unreach-call) 1 wit inspect 8.3  4.5  290 0   0     true -32 --- inspect 17     9.6   510   .66 0     false(unreach-call) 1 --- inspect 5.6  3.2  270 0   0      false(unreach-call) 1 --- inspect .84   .84   20    .35 0     - --- inspect - --- inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 100 0      0     false(unreach-call) 1 wit inspect 9.9  5.3  290 0   0     true -32 --- inspect 18     10     510   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  270 0   0      false(unreach-call) 1 --- inspect .88   .88   20    .36 0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 100 0      0     false(unreach-call) 1 wit inspect 9.2  4.9  280 0   0     true -32 --- inspect 18     10     470   .66 0     false(unreach-call) 1 --- inspect 5.6  3.1  270 0   0      false(unreach-call) 1 --- inspect .87   .88   21    .35 0     - --- inspect - --- inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 110 0      0     false(unreach-call) 1 wit inspect 7.0  3.7  280 0   0     true -32 --- inspect 21     11     460   .66 0     false(unreach-call) 1 --- inspect 6.4  3.6  270 0   0      false(unreach-call) 1 --- inspect .89   .90   20    .36 0     - --- inspect - --- inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 430 110 0      0     false(unreach-call) 1 wit inspect 8.1  4.4  290 0   0     true -32 --- inspect 18     10     460   .66 0     false(unreach-call) 1 --- inspect 5.5  3.1  270 0   0      false(unreach-call) 1 --- inspect .87   .89   20    .36 0     - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 110 0      0     false(unreach-call) 1 wit inspect 9.9  5.3  290 0   0     true -32 --- inspect 19     11     520   .66 .078 false(unreach-call) 1 --- inspect 5.8  3.2  270 0   0      false(unreach-call) 1 --- inspect .88   .88   20    .36 0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 72   35   450 740 0      0     false(unreach-call) 1 wit inspect 42    25    1200 0   0     true -32 --- inspect 20     11     550   .66 0     unknown 0 --- inspect 7.0  3.9  270 0   0      true -32 --- inspect .88   .88   20    .39 .082 - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 440 100 0      0     false(unreach-call) 1 wit inspect 9.8  5.2  290 0   0     true -32 --- inspect 16     9.3   500   .66 0     false(unreach-call) 1 --- inspect 7.3  4.0  270 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .34 0     - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 440 100 0      0     false(unreach-call) 1 wit inspect 9.1  4.9  290 0   0     true -32 --- inspect 15     8.7   510   .66 0     false(unreach-call) 1 --- inspect 7.6  4.2  260 0   0      false(unreach-call) 1 --- inspect .88   .88   21    .34 0     - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 440 110 0      0     false(unreach-call) 1 wit inspect 11    5.6  310 0   0     true -32 --- inspect 19     11     470   .66 0     false(unreach-call) 1 --- inspect 7.1  3.9  260 0   0      false(unreach-call) 1 --- inspect .86   .86   21    .35 .074 - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.9 8.9 440 100 0      0     false(unreach-call) 1 wit inspect 8.3  4.4  310 0   0     true -32 --- inspect 18     10     510   .66 0     false(unreach-call) 1 --- inspect 5.9  3.3  270 0   .070  false(unreach-call) 1 --- inspect .85   .87   21    .26 0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.0 9.0 440 120 0      0     false(unreach-call) 1 wit inspect 9.0  4.9  310 0   0     true -32 --- inspect 17     9.7   520   .66 0     false(unreach-call) 1 --- inspect 7.4  4.1  270 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .36 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.9 440 110 0      0     false(unreach-call) 1 wit inspect 8.3  4.5  320 0   0     true -32 --- inspect 17     9.7   520   .66 0     false(unreach-call) 1 --- inspect 5.7  3.1  270 0   0      false(unreach-call) 1 --- inspect .88   .88   21    .36 .078 - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.8 440 120 0      0     false(unreach-call) 1 wit inspect 8.8  4.7  290 0   0     true -32 --- inspect 19     10     470   .66 0     false(unreach-call) 1 --- inspect 5.9  3.3  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .35 0     - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 440 120 0      0     false(unreach-call) 1 wit inspect 11    5.6  310 0   0     true -32 --- inspect 15     8.9   510   .66 0     false(unreach-call) 1 --- inspect 6.2  3.4  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .36 0     - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 440 110 0      0     false(unreach-call) 1 wit inspect 8.8  4.8  310 0   0     true -32 --- inspect 21     11     460   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  270 0   0      false(unreach-call) 1 --- inspect .88   .89   20    .36 0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 440 110 0      0     false(unreach-call) 1 wit inspect 8.7  4.7  320 0   0     true -32 --- inspect 18     10     470   .66 0     false(unreach-call) 1 --- inspect 7.2  4.0  270 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .36 0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 200   85   460 2200 0      0     false(unreach-call) 1 wit inspect 20    11    610 0   0     true -32 --- inspect 21     12     530   .66 0     unknown 0 --- inspect 6.1  3.4  270 0   0      true -32 --- inspect .90   .90   20    .39 0     - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 430 100 0      0     false(unreach-call) 1 wit inspect 9.7  5.2  280 0   0     true -32 --- inspect 15     8.7   510   .66 0     false(unreach-call) 1 --- inspect 6.5  3.6  270 0   0      false(unreach-call) 1 --- inspect .87   .89   20    .34 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 120 0      0     false(unreach-call) 1 wit inspect 8.0  4.3  290 0   0     true -32 --- inspect 15     8.5   520   .66 0     false(unreach-call) 1 --- inspect 5.6  3.1  270 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .36 0     - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.9 8.9 430 110 0      0     false(unreach-call) 1 wit inspect 9.0  4.8  300 0   0     true -32 --- inspect 18     10     510   .66 0     false(unreach-call) 1 --- inspect 6.0  3.4  260 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .36 0     - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.0 9.0 430 110 0      0     false(unreach-call) 1 wit inspect 9.9  5.3  290 0   0     true -32 --- inspect 16     9.3   530   .66 0     false(unreach-call) 1 --- inspect 7.6  4.2  290 0   0      false(unreach-call) 1 --- inspect .86   .86   20    .36 0     - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 84   39   450 940 0      0     false(unreach-call) 1 wit inspect 43    25    1300 0   0     true -32 --- inspect 22     12     560   .66 0     unknown 0 --- inspect 7.1  3.9  270 0   0      true -32 --- inspect .94   .93   20    .39 0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.9 8.9 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2700 0   0      out of memory 0 --- inspect 220     150     7000   .65 0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.5 8.5 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3300 0   0      out of memory 0 --- inspect 200     130     7000   .66 0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.7 8.7 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3700 0   0      out of memory 0 --- inspect 260     180     7000   .65 0    
elevator_spec13_product24_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.6 8.6 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4300 0   0      out of memory 0 --- inspect 260     170     7000   1.7  0    
elevator_spec13_product29_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.5 8.5 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    2400 0   0      out of memory 0 --- inspect 230     150     7000   .68 0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.7 8.7 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3400 0   0      out of memory 0 --- inspect 210     140     7000   .65 0    
elevator_spec13_product31_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.7 8.8 370 96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3700 0   0      out of memory 0 --- inspect 200     130     7000   .65 0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.6 8.6 370 98 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4400 0   .0041 out of memory 0 --- inspect 240     170     7000   .65 0    
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c true 1 wit inspect 44   17   380 400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3400 0   0      out of memory 0 --- inspect 230     150     7000   .72 0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    660 0   0      out of memory 0 --- inspect 270     190     7000   .72 0    
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    680 0   0      out of memory 0 --- inspect 280     200     7000   .65 0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    700 0   0      out of memory 0 --- inspect 310     220     7000   1.6  .033
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.9 8.9 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    18    1100 0   0      out of memory 0 --- inspect 240     160     7000   .66 0    
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    710 0   0      out of memory 0 --- inspect 330     240     7000   .79 0    
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    17    1100 0   0      out of memory 0 --- inspect 250     170     7000   .71 .041
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 81    66    1600 0   0      out of memory 0 --- inspect 260     190     7000   .64 0    
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.7 370 98 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 82    68    1700 0   0      out of memory 0 --- inspect 260     180     7000   .65 0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 91    75    1700 0   0      out of memory 0 --- inspect 260     180     7000   .64 0    
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.4 370 130 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 100    89    1700 0   0      out of memory 0 --- inspect 280     190     7000   1.6  0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 80    69    1800 0   0      out of memory 0 --- inspect 250     180     7000   .64 0    
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 97    85    1800 0   0      out of memory 0 --- inspect 330     230     7000   .66 0    
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 170    160    2200 0   0      out of memory 0 --- inspect 260     190     7000   .72 0    
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 90 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 160    150    2300 0   0      out of memory 0 --- inspect 340     240     7000   .64 0    
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 94    79    1800 0   0      out of memory 0 --- inspect 260     180     7000   .65 0    
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 97 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    98    2000 0   0      out of memory 0 --- inspect 250     180     7000   .66 0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 340    320    2300 0   0      out of memory 0 --- inspect 290     200     7000   .68 0    
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 99 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 200    180    2500 0   0      out of memory 0 --- inspect 290     200     7000   .64 0    
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.7 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    25    1000 0   0      out of memory 0 --- inspect 180     120     7000   1.5  0    
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    26    1100 0   0      out of memory 0 --- inspect 220     150     7000   .69 0    
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    23    1100 0   0      out of memory 0 --- inspect 160     100     7000   .66 0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    25    1100 0   0      out of memory 0 --- inspect 180     120     7000   1.3  0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    27    1100 0   0      out of memory 0 --- inspect 160     100     7000   .65 0    
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 46    32    1200 0   0      out of memory 0 --- inspect 200     140     7000   .66 0    
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 56    42    1300 0   0      out of memory 0 --- inspect 200     130     7000   .64 0    
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 59    45    1400 0   0      out of memory 0 --- inspect 300     210     7000   .64 0    
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    26    1200 0   0      out of memory 0 --- inspect 170     110     7000   .64 0    
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 50    36    1200 0   0      out of memory 0 --- inspect 220     140     7000   .65 0    
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 60    48    1500 0   0      out of memory 0 --- inspect 210     140     7000   .75 0    
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 56    42    1500 0   0      out of memory 0 --- inspect 230     160     7000   .70 0    
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.9 8.9 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.4  670 0   0      out of memory 0 --- inspect 180     110     7000   .64 0    
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.8  650 0   0      out of memory 0 --- inspect 150     95     7000   .66 0    
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.6  670 0   0      out of memory 0 --- inspect 200     120     7000   .65 .36 
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.4 370 130 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 29    16    840 0   0      out of memory 0 --- inspect 200     130     7000   .91 0    
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    13    930 0   0      out of memory 0 --- inspect 240     160     7000   .64 0    
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.7 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 34    19    1300 0   0      out of memory 0 --- inspect 230     160     7000   .64 0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 99 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    10    700 0   0      out of memory 0 --- inspect 190     120     7000   1.5  0    
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25    14    930 0   0      out of memory 0 --- inspect 270     180     7000   .64 0    
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23    13    910 0   0      out of memory 0 --- inspect 260     180     7000   .66 0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    21    1500 0   0      out of memory 0 --- inspect 190     130     7000   .71 0    
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    27    1100 0   0      out of memory 0 --- inspect 210     140     7000   .71 0    
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.7 370 96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    28    1100 0   0      out of memory 0 --- inspect 180     120     7000   .65 0    
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    27    1200 0   0      out of memory 0 --- inspect 210     140     7000   .70 0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    28    1200 0   0      out of memory 0 --- inspect 200     130     7000   .65 0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.9 8.9 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 85    70    1500 0   0      out of memory 0 --- inspect 220     150     7000   .82 0    
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.9 8.9 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 61    49    1600 0   0      out of memory 0 --- inspect 250     170     7000   .71 0    
email_spec0_product16_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .59 .37 42 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect 1.2  .75 47 0   0      error (invalid witness file) 0 --- inspect .0048 .0060 .54 0    0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 710 0      0     error (invalid witness file) 0 --- inspect .75 .45 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0      error (invalid witness file) 0 --- inspect .0053 .0064 .54 0    0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 820 0      0     error (invalid witness file) 0 --- inspect .73 .44 41 0   0     error (2) 0 --- inspect .031 .032 5.6 0    0     error (invalid witness file) 0 --- inspect 1.4  .89 47 0   0      error (invalid witness file) 0 --- inspect .0046 .0074 .54 0    0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 710 0      0     error (invalid witness file) 0 --- inspect .78 .47 42 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .67 49 0   0      error (invalid witness file) 0 --- inspect .0023 .0029 .54 0    0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 710 0      0     error (invalid witness file) 0 --- inspect .74 .44 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .97 .64 47 0   0      error (invalid witness file) 0 --- inspect .0055 .0068 .53 0    0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 740 0      0     error (invalid witness file) 0 --- inspect .65 .40 41 0   0     error (2) 0 --- inspect .029 .030 5.5 0    0     error (invalid witness file) 0 --- inspect 1.1  .69 47 0   0      error (invalid witness file) 0 --- inspect .0055 .0072 .54 0    0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   34   440 780 0      0     error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .020 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .99 .64 46 0   0      error (invalid witness file) 0 --- inspect .0055 .0065 .54 0    0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 730 0      0     error (invalid witness file) 0 --- inspect .75 .45 40 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0      error (invalid witness file) 0 --- inspect .0016 .0021 .54 0    0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 21   14   440 230 0      0     error (invalid witness file) 0 --- inspect .64 .40 40 0   0     error (2) 0 --- inspect .024 .026 5.6 0    0     error (invalid witness file) 0 --- inspect .90 .59 47 0   0      error (invalid witness file) 0 --- inspect .0023 .0029 .53 0    0     - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 760 0      0     error (invalid witness file) 0 --- inspect .74 .47 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .67 48 0   0      error (invalid witness file) 0 --- inspect .0021 .0027 .41 0    0     - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .77 .48 41 0   0     error (2) 0 --- inspect .036 .038 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0      error (invalid witness file) 0 --- inspect .0058 .0070 .52 0    0     - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 730 0      0     error (invalid witness file) 0 --- inspect .61 .38 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .59 48 0   0      error (invalid witness file) 0 --- inspect .0021 .0042 .61 0    0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .99 .64 48 0   0      error (invalid witness file) 0 --- inspect .0055 .0082 .53 0    0     - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 720 0      0     error (invalid witness file) 0 --- inspect .78 .47 41 0   0     error (2) 0 --- inspect .025 .025 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .71 49 0   0      error (invalid witness file) 0 --- inspect .0058 .018  .52 0    0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .76 .46 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .61 46 0   0      error (invalid witness file) 0 --- inspect .0020 .0025 .53 0    0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 740 0      0     error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .028 .028 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .79 47 0   0      error (invalid witness file) 0 --- inspect .0016 .0020 .52 0    0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 750 0      0     error (invalid witness file) 0 --- inspect .59 .36 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 46 0   0      error (invalid witness file) 0 --- inspect .0064 .011  .48 0    0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 21   14   440 260 0      0     error (invalid witness file) 0 --- inspect .78 .47 42 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .78 48 0   0      error (invalid witness file) 0 --- inspect .0059 .0075 .52 0    0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 730 0      0     error (invalid witness file) 0 --- inspect .76 .45 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 46 0   0      error (invalid witness file) 0 --- inspect .0047 .0058 .54 0    0     - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 670 0      0     error (invalid witness file) 0 --- inspect .71 .43 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.4  .88 47 0   0      error (invalid witness file) 0 --- inspect .0045 .0055 .54 0    0     - --- inspect - --- inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 720 0      0     error (invalid witness file) 0 --- inspect .56 .35 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .67 48 0   0      error (invalid witness file) 0 --- inspect .0051 .0065 .41 0    0     - --- inspect - --- inspect
email_spec1_product20_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 780 0      0     error (invalid witness file) 0 --- inspect .72 .44 40 0   0     error (2) 0 --- inspect .026 .028 5.8 0    0     error (invalid witness file) 0 --- inspect .96 .62 48 0   0      error (invalid witness file) 0 --- inspect .0061 .0078 .52 0    0     - --- inspect - --- inspect
email_spec1_product21_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   450 780 0      0     error (invalid witness file) 0 --- inspect .61 .39 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .98 .64 47 0   0      error (invalid witness file) 0 --- inspect .0051 .0064 .40 0    0     - --- inspect - --- inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .60 .38 40 0   0     error (2) 0 --- inspect .019 .020 5.7 0    0     error (invalid witness file) 0 --- inspect 1.2  .75 47 0   0      error (invalid witness file) 0 --- inspect .0050 .0060 .39 0    0     - --- inspect - --- inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 810 0      0     error (invalid witness file) 0 --- inspect .62 .38 42 0   0     error (2) 0 --- inspect .027 .028 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0044 .0059 .54 0    0     - --- inspect - --- inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect 1.2  .75 46 0   0      error (invalid witness file) 0 --- inspect .0022 .0027 .54 0    0     - --- inspect - --- inspect
email_spec1_product30_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 770 0      0     error (invalid witness file) 0 --- inspect .71 .44 40 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .73 47 0   0      error (invalid witness file) 0 --- inspect .0046 .0056 .54 0    0     - --- inspect - --- inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 730 0      0     error (invalid witness file) 0 --- inspect .63 .39 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .74 47 0   0      error (invalid witness file) 0 --- inspect .0022 .0027 .54 0    0     - --- inspect - --- inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 780 0      0     error (invalid witness file) 0 --- inspect .61 .37 42 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0      error (invalid witness file) 0 --- inspect .0023 .0030 .54 0    0     - --- inspect - --- inspect
email_spec1_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 760 0      0     error (invalid witness file) 0 --- inspect .64 .40 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .98 .66 47 0   0      error (invalid witness file) 0 --- inspect .0044 .0056 .39 0    0     - --- inspect - --- inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 640 0      0     error (invalid witness file) 0 --- inspect .66 .39 42 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .79 47 0   0      error (invalid witness file) 0 --- inspect .0060 .0074 .54 0    0     - --- inspect - --- inspect
email_spec1_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   34   450 710 0      0     error (invalid witness file) 0 --- inspect .80 .48 41 0   0     error (2) 0 --- inspect .026 .028 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0039 .0051 .54 0    0     - --- inspect - --- inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 14   11   430 150 0      0     error (invalid witness file) 0 --- inspect .61 .37 41 0   0     error (2) 0 --- inspect .023 .024 5.7 0    0     error (invalid witness file) 0 --- inspect 1.1  .68 47 0   0      error (invalid witness file) 0 --- inspect .0059 .0081 .53 0    0     - --- inspect - --- inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 880 0      0     error (invalid witness file) 0 --- inspect .77 .46 42 0   0     error (2) 0 --- inspect .028 .028 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0      error (invalid witness file) 0 --- inspect .0050 .0066 .54 0    0     - --- inspect - --- inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 720 0      0     error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .037 .038 5.5 0    0     error (invalid witness file) 0 --- inspect 1.2  .78 47 0   0      error (invalid witness file) 0 --- inspect .0021 .0029 .53 0    0     - --- inspect - --- inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 680 0      0     error (invalid witness file) 0 --- inspect .82 .51 40 0   0     error (2) 0 --- inspect .026 .026 5.6 0    0     error (invalid witness file) 0 --- inspect .98 .63 47 0   0      error (invalid witness file) 0 --- inspect .0024 .0037 .53 0    0     - --- inspect - --- inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 810 0      0     error (invalid witness file) 0 --- inspect .75 .46 40 0   0     error (2) 0 --- inspect .027 .029 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .74 47 0   0      error (invalid witness file) 0 --- inspect .0049 .0059 .40 0    0     - --- inspect - --- inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 710 0      0     error (invalid witness file) 0 --- inspect .58 .37 41 0   0     error (2) 0 --- inspect .024 .025 5.7 0    0     error (invalid witness file) 0 --- inspect 1.0  .67 46 0   0      error (invalid witness file) 0 --- inspect .0060 .0077 .53 0    0     - --- inspect - --- inspect
email_spec27_product25_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 740 0      0     error (invalid witness file) 0 --- inspect .73 .46 43 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.4  .87 47 0   0      error (invalid witness file) 0 --- inspect .0057 .0074 .54 0    0     - --- inspect - --- inspect
email_spec27_product27_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   450 700 0      0     error (invalid witness file) 0 --- inspect .65 .39 42 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .68 46 0   0      error (invalid witness file) 0 --- inspect .0017 .0021 .53 0    0     - --- inspect - --- inspect
email_spec27_product29_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   450 680 0      0     error (invalid witness file) 0 --- inspect .81 .49 41 0   0     error (2) 0 --- inspect .026 .028 5.8 0    0     error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0060 .0088 .52 0    0     - --- inspect - --- inspect
email_spec27_product30_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 680 0      0     error (invalid witness file) 0 --- inspect .71 .44 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .99 .65 46 0   0      error (invalid witness file) 0 --- inspect .0013 .0014 .40 0    0     - --- inspect - --- inspect
email_spec27_product31_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 710 0      0     error (invalid witness file) 0 --- inspect .62 .39 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.3  .84 48 0   0      error (invalid witness file) 0 --- inspect .0021 .0029 .53 0    0     - --- inspect - --- inspect
email_spec27_product32_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 780 0      0     error (invalid witness file) 0 --- inspect .88 .53 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .69 48 0   0      error (invalid witness file) 0 --- inspect .0060 .011  .62 0    0     - --- inspect - --- inspect
email_spec27_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 790 0      0     error (invalid witness file) 0 --- inspect .62 .39 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .78 47 0   0      error (invalid witness file) 0 --- inspect .0065 .0088 .53 0    0     - --- inspect - --- inspect
email_spec27_product34_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 760 0      0     error (invalid witness file) 0 --- inspect .74 .44 42 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .73 47 0   0      error (invalid witness file) 0 --- inspect .0025 .0037 .53 0    0     - --- inspect - --- inspect
email_spec27_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 760 0      0     error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .022 .024 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0      error (invalid witness file) 0 --- inspect .0050 .0066 .52 0    0     - --- inspect - --- inspect
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 16   12   440 180 0      0     error (invalid witness file) 0 --- inspect .68 .41 40 0   0     error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0      error (invalid witness file) 0 --- inspect .0060 .0077 .52 0    0     - --- inspect - --- inspect
email_spec3_product13_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140   62   510 1500 0      0     false(unreach-call) 1 wit inspect 8.6  4.7  330 0   0     true -32 --- inspect 19     10     490   .66 0     unknown 0 --- inspect 7.2  4.0  260 0   0      true -32 --- inspect .84   .84   20    .37 0     - --- inspect - --- inspect
email_spec3_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140   63   510 1500 0      0     false(unreach-call) 1 wit inspect 11    5.9  350 0   0     true -32 --- inspect 15     8.3   480   .66 0     unknown 0 --- inspect 7.0  3.9  270 0   0      true -32 --- inspect .84   .84   20    .38 0     - --- inspect - --- inspect
email_spec3_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 180   67   510 1700 0      0     false(unreach-call) 1 wit inspect 9.9  5.4  330 0   0     true -32 --- inspect 14     8.2   470   .62 0     unknown 0 --- inspect 6.8  3.8  260 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .38 0     - --- inspect - --- inspect
email_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140   62   500 1600 0      0     false(unreach-call) 1 wit inspect 11    6.0  340 0   0     true -32 --- inspect 14     8.5   470   .62 0     unknown 0 --- inspect 5.4  3.1  260 0   0      true -32 --- inspect .85   .85   21    .38 0     - --- inspect - --- inspect
email_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 120   51   490 1300 0      0     false(unreach-call) 1 wit inspect 9.9  5.3  370 0   0     true -32 --- inspect 16     9.2   510   .66 0     unknown 0 --- inspect 5.6  3.1  260 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .39 0     - --- inspect - --- inspect
email_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140   61   510 1500 0      0     false(unreach-call) 1 wit inspect 11    5.9  330 0   0     true -32 --- inspect 17     9.9   490   .66 0     unknown 0 --- inspect 5.7  3.2  270 0   0      false(unreach-call) 1 --- inspect .86   .86   20    .39 0     - --- inspect - --- inspect
email_spec3_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140   62   500 1400 0      0     false(unreach-call) 1 wit inspect 9.3  5.1  370 0   0     true -32 --- inspect 15     8.9   470   .62 0     unknown 0 --- inspect 6.6  3.7  270 0   0      true -32 --- inspect .89   .89   20    .39 0     - --- inspect - --- inspect
email_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 120   58   480 1400 0      0     false(unreach-call) 1 wit inspect 9.3  5.0  380 0   0     true -32 --- inspect 16     9.1   500   .66 0     unknown 0 --- inspect 6.9  3.9  260 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .39 0     - --- inspect - --- inspect
email_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130   55   510 1400 0      0     false(unreach-call) 1 wit inspect 8.0  4.4  330 0   0     true -32 --- inspect 20     11     500   .66 0     unknown 0 --- inspect 5.9  3.3  260 0   0      true -32 --- inspect .85   .85   20    .39 0     - --- inspect - --- inspect
email_spec3_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140   62   640 1400 0      130     false(unreach-call) 1 wit inspect 9.9  5.4  370 0   0     true -32 --- inspect 16     8.9   470   .62 0     unknown 0 --- inspect 6.4  3.6  270 0   0      true -32 --- inspect .85   .85   20    .39 0     - --- inspect - --- inspect
email_spec3_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130   55   490 1300 0      0     false(unreach-call) 1 wit inspect 11    6.0  350 0   0     true -32 --- inspect 16     9.3   460   .66 0     unknown 0 --- inspect 6.9  3.9  260 0   0      false(unreach-call) 1 --- inspect .85   .85   21    .39 0     - --- inspect - --- inspect
email_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140   62   510 1500 0      0     false(unreach-call) 1 wit inspect 11    5.8  340 0   0     true -32 --- inspect 15     8.8   500   .66 0     unknown 0 --- inspect 7.0  3.9  260 0   0      true -32 --- inspect .84   .84   21    .39 .066 - --- inspect - --- inspect
email_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130   55   500 1200 0      0     false(unreach-call) 1 wit inspect 12    6.6  380 0   0     true -32 --- inspect 19     11     470   .66 0     unknown 0 --- inspect 5.8  3.3  260 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .40 0     - --- inspect - --- inspect
email_spec3_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 120   58   490 1200 0      0     false(unreach-call) 1 wit inspect 11    6.1  340 0   0     true -32 --- inspect 20     11     460   .66 0     unknown 0 --- inspect 6.9  3.9  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .40 0     - --- inspect - --- inspect
email_spec3_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140   62   500 1200 0      0     false(unreach-call) 1 wit inspect 10    5.4  390 0   0     true -32 --- inspect 17     9.9   520   .66 0     unknown 0 --- inspect 6.7  3.7  280 0   0      true -32 --- inspect .88   .88   21    .40 0     - --- inspect - --- inspect
email_spec3_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140   62   520 1600 0      0     false(unreach-call) 1 wit inspect 14    7.3  400 0   0     true -32 --- inspect 19     11     460   .66 0     unknown 0 --- inspect 7.7  4.3  260 0   0      false(unreach-call) 1 --- inspect .89   .88   20    .40 0     - --- inspect - --- inspect
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 14   11   440 180 0      0     error (invalid witness file) 0 --- inspect .75 .47 41 0   0     error (2) 0 --- inspect .026 .028 5.7 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0      error (invalid witness file) 0 --- inspect .0058 .0096 .52 0    0     - --- inspect - --- inspect
email_spec4_product18_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 850 0      0     error (invalid witness file) 0 --- inspect .69 .41 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0      error (invalid witness file) 0 --- inspect .0061 .0077 .54 0    0     - --- inspect - --- inspect
email_spec4_product19_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 750 0      0     error (invalid witness file) 0 --- inspect .72 .45 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.4  .90 47 0   0      error (invalid witness file) 0 --- inspect .0019 .0024 .54 0    0     - --- inspect - --- inspect
email_spec4_product23_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   450 740 0      0     error (invalid witness file) 0 --- inspect .79 .49 40 0   0     error (2) 0 --- inspect .031 .032 5.6 0    0     error (invalid witness file) 0 --- inspect 1.3  .80 47 0   0      error (invalid witness file) 0 --- inspect .0049 .0059 .54 0    0     - --- inspect - --- inspect
email_spec4_product24_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 810 0      0     error (invalid witness file) 0 --- inspect .80 .49 42 0   0     error (2) 0 --- inspect .025 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .64 47 0   0      error (invalid witness file) 0 --- inspect .0018 .0022 .41 0    0     - --- inspect - --- inspect
email_spec4_product25_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 680 0      0     error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .026 .027 5.8 0    0     error (invalid witness file) 0 --- inspect .97 .64 47 0   0      error (invalid witness file) 0 --- inspect .0057 .0072 .54 0    0     - --- inspect - --- inspect
email_spec4_product27_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 660 0      0     error (invalid witness file) 0 --- inspect .58 .37 40 0   0     error (2) 0 --- inspect .024 .026 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .78 47 0   0      error (invalid witness file) 0 --- inspect .0022 .0036 .54 0    0     - --- inspect - --- inspect
email_spec4_product30_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 700 0      0     error (invalid witness file) 0 --- inspect .74 .46 40 0   0     error (2) 0 --- inspect .030 .030 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .74 47 0   0      error (invalid witness file) 0 --- inspect .0016 .0024 .54 0    0     - --- inspect - --- inspect
email_spec4_product31_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 720 0      0     error (invalid witness file) 0 --- inspect .70 .43 40 0   0     error (2) 0 --- inspect .032 .034 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .63 46 0   0      error (invalid witness file) 0 --- inspect .0054 .0063 .54 0    0     - --- inspect - --- inspect
email_spec4_product32_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 770 0      0     error (invalid witness file) 0 --- inspect .67 .41 42 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .81 47 0   0      error (invalid witness file) 0 --- inspect .0018 .0024 .54 0    0     - --- inspect - --- inspect
email_spec4_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 760 0      0     error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .91 .60 47 0   0      error (invalid witness file) 0 --- inspect .0022 .0039 .41 0    0     - --- inspect - --- inspect
email_spec4_product34_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 760 0      0     error (invalid witness file) 0 --- inspect .69 .42 42 0   0     error (2) 0 --- inspect .028 .028 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .74 47 0   0      error (invalid witness file) 0 --- inspect .0050 .0061 .54 0    0     - --- inspect - --- inspect
email_spec4_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 680 0      0     error (invalid witness file) 0 --- inspect .73 .44 41 0   0     error (2) 0 --- inspect .035 .036 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .71 47 0   0      error (invalid witness file) 0 --- inspect .0050 .0061 .53 0    0     - --- inspect - --- inspect
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 14   11   440 170 0      0     error (invalid witness file) 0 --- inspect .65 .39 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .64 48 0   0      error (invalid witness file) 0 --- inspect .0055 .0074 .53 0    0     - --- inspect - --- inspect
email_spec6_product12_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 170   75   480 1800 0      0     error (invalid witness file) 0 --- inspect .79 .48 42 0   0     error (2) 0 --- inspect .027 .028 5.6 0    0     error (invalid witness file) 0 --- inspect .97 .63 49 0   0      error (invalid witness file) 0 --- inspect .0038 .0043 .40 0    0     - --- inspect - --- inspect
email_spec6_product14_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   55   480 1400 0      0     error (invalid witness file) 0 --- inspect .59 .35 40 0   0     error (2) 0 --- inspect .025 .026 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .73 48 0   0      error (invalid witness file) 0 --- inspect .0055 .0070 .52 0    0     - --- inspect - --- inspect
email_spec6_product15_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   470 1300 0      0     error (invalid witness file) 0 --- inspect .78 .49 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .99 .64 49 0   0      error (invalid witness file) 0 --- inspect .0017 .0023 .52 0    0     - --- inspect - --- inspect
email_spec6_product16_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   490 1400 0      0     error (invalid witness file) 0 --- inspect .66 .40 40 0   0     error (2) 0 --- inspect .028 .030 5.7 0    0     error (invalid witness file) 0 --- inspect .92 .61 47 0   0      error (invalid witness file) 0 --- inspect .0066 .0084 .54 0    0     - --- inspect - --- inspect
email_spec6_product20_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   480 1400 0      0     error (invalid witness file) 0 --- inspect .66 .41 42 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .83 48 0   0      error (invalid witness file) 0 --- inspect .0022 .0030 .41 0    0     - --- inspect - --- inspect
email_spec6_product21_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   490 1200 0      0     error (invalid witness file) 0 --- inspect .70 .43 42 0   0     error (2) 0 --- inspect .030 .030 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .59 46 0   0      error (invalid witness file) 0 --- inspect .0015 .0021 .53 0    0     - --- inspect - --- inspect
email_spec6_product22_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   490 1300 0      0     error (invalid witness file) 0 --- inspect .77 .47 40 0   0     error (2) 0 --- inspect .025 .026 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .73 47 0   0      error (invalid witness file) 0 --- inspect .0056 .0071 .54 0    0     - --- inspect - --- inspect
email_spec6_product26_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 190   67   510 1800 0      0     error (invalid witness file) 0 --- inspect .66 .40 40 0   0     error (2) 0 --- inspect .027 .028 5.7 0    0     error (invalid witness file) 0 --- inspect 1.4  .90 47 0   0      error (invalid witness file) 0 --- inspect .0055 .0072 .52 0    0     - --- inspect - --- inspect
email_spec6_product28_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 140   61   490 1400 0      0     error (invalid witness file) 0 --- inspect .62 .43 42 0   0     error (2) 0 --- inspect .027 .028 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0      error (invalid witness file) 0 --- inspect .0047 .0064 .54 0    0     - --- inspect - --- inspect
email_spec6_product29_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 180   67   490 1800 0      0     error (invalid witness file) 0 --- inspect .65 .40 43 0   0     error (2) 0 --- inspect .025 .026 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .81 47 0   0      error (invalid witness file) 0 --- inspect .0019 .0024 .54 0    0     - --- inspect - --- inspect
email_spec6_product30_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   55   470 1500 0      0     error (invalid witness file) 0 --- inspect .69 .43 40 0   0     error (2) 0 --- inspect .024 .026 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .80 46 0   0      error (invalid witness file) 0 --- inspect .0054 .0070 .53 0    0     - --- inspect - --- inspect
email_spec6_product31_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   500 1500 0      0     error (invalid witness file) 0 --- inspect .80 .49 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .74 48 0   0      error (invalid witness file) 0 --- inspect .0058 .0080 .53 0    0     - --- inspect - --- inspect
email_spec6_product32_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 140   62   490 1400 0      0     error (invalid witness file) 0 --- inspect .67 .42 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .80 48 0   0      error (invalid witness file) 0 --- inspect .0046 .0059 .54 0    0     - --- inspect - --- inspect
email_spec6_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 190   74   490 1800 0      0     error (invalid witness file) 0 --- inspect .76 .46 41 0   0     error (2) 0 --- inspect .029 .029 5.6 0    0     error (invalid witness file) 0 --- inspect .91 .59 47 0   0      error (invalid witness file) 0 --- inspect .0051 .0067 .41 0    0     - --- inspect - --- inspect
email_spec6_product34_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   500 1300 0      0     error (invalid witness file) 0 --- inspect .70 .43 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .79 48 0   0      error (invalid witness file) 0 --- inspect .0048 .0058 .53 0    0     - --- inspect - --- inspect
email_spec6_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   490 1300 0      0     error (invalid witness file) 0 --- inspect .76 .46 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .74 49 0   0      error (invalid witness file) 0 --- inspect .0054 .0073 .53 0    0     - --- inspect - --- inspect
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 14   11   430 140 0      0     error (invalid witness file) 0 --- inspect .76 .46 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .76 48 0   0      error (invalid witness file) 0 --- inspect .0016 .0022 .41 0    0     - --- inspect - --- inspect
email_spec7_product28_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 690 0      0     error (invalid witness file) 0 --- inspect .74 .44 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.3  .82 48 0   0      error (invalid witness file) 0 --- inspect .0018 .0031 .54 0    0     - --- inspect - --- inspect
email_spec7_product29_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .61 47 0   0      error (invalid witness file) 0 --- inspect .0037 .0048 .54 0    0     - --- inspect - --- inspect
email_spec7_product30_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 750 0      0     error (invalid witness file) 0 --- inspect .77 .47 40 0   0     error (2) 0 --- inspect .026 .027 5.5 0    0     error (invalid witness file) 0 --- inspect 1.1  .69 47 0   0      error (invalid witness file) 0 --- inspect .0015 .0019 .39 0    0     - --- inspect - --- inspect
email_spec7_product31_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 810 0      0     error (invalid witness file) 0 --- inspect .75 .45 42 0   0     error (2) 0 --- inspect .028 .028 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .62 47 0   0      error (invalid witness file) 0 --- inspect .0051 .0070 .54 0    0     - --- inspect - --- inspect
email_spec7_product32_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 680 0      0     error (invalid witness file) 0 --- inspect .66 .42 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.3  .83 47 0   0      error (invalid witness file) 0 --- inspect .0024 .0031 .41 0    0     - --- inspect - --- inspect
email_spec7_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 680 0      0     error (invalid witness file) 0 --- inspect .78 .49 40 0   0     error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0      error (invalid witness file) 0 --- inspect .0050 .0062 .54 0    0     - --- inspect - --- inspect
email_spec7_product34_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 700 0      0     error (invalid witness file) 0 --- inspect .70 .42 40 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect 1.3  .83 47 0   0      error (invalid witness file) 0 --- inspect .0043 .0055 .54 0    0     - --- inspect - --- inspect
email_spec7_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 680 0      0     error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .021 .023 5.7 0    0     error (invalid witness file) 0 --- inspect .98 .64 49 0   0      error (invalid witness file) 0 --- inspect .0019 .0025 .54 0    0     - --- inspect - --- inspect
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 16   12   440 210 0      0     error (invalid witness file) 0 --- inspect .79 .49 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .79 48 0   0      error (invalid witness file) 0 --- inspect .0056 .0071 .53 0    0     - --- inspect - --- inspect
email_spec8_product15_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 140   62   490 1600 0      0     error (invalid witness file) 0 --- inspect .78 .49 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .98 .63 47 0   0      error (invalid witness file) 0 --- inspect .0051 .0065 .41 0    0     - --- inspect - --- inspect
email_spec8_product16_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   490 1300 0      0     error (invalid witness file) 0 --- inspect .60 .38 41 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .68 48 0   0      error (invalid witness file) 0 --- inspect .0054 .0064 .54 0    0     - --- inspect - --- inspect
email_spec8_product20_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 140   62   490 1500 0      0     error (invalid witness file) 0 --- inspect .75 .45 42 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect .96 .62 47 0   0      error (invalid witness file) 0 --- inspect .0021 .0027 .54 0    0     - --- inspect - --- inspect
email_spec8_product21_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   490 1300 0      0     error (invalid witness file) 0 --- inspect .78 .48 42 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .63 48 0   0      error (invalid witness file) 0 --- inspect .0070 .010  .54 0    0     - --- inspect - --- inspect
email_spec8_product22_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   500 1500 0      0     error (invalid witness file) 0 --- inspect .62 .38 40 0   0     error (2) 0 --- inspect .022 .022 5.5 0    0     error (invalid witness file) 0 --- inspect 1.1  .77 47 0   0      error (invalid witness file) 0 --- inspect .0045 .0057 .54 0    0     - --- inspect - --- inspect
email_spec8_product26_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 120   51   470 1200 0      0     error (invalid witness file) 0 --- inspect .78 .47 43 0   0     error (2) 0 --- inspect .028 .028 5.5 0    0     error (invalid witness file) 0 --- inspect 1.2  .78 47 0   0      error (invalid witness file) 0 --- inspect .0017 .0022 .54 0    0     - --- inspect - --- inspect
email_spec8_product30_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 140   62   490 1400 0      0     error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .026 .026 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .70 46 0   0      error (invalid witness file) 0 --- inspect .0049 .0052 .41 0    0     - --- inspect - --- inspect
email_spec8_product31_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   55   510 1300 0      0     error (invalid witness file) 0 --- inspect .75 .48 41 0   0     error (2) 0 --- inspect .027 .028 5.7 0    0     error (invalid witness file) 0 --- inspect .98 .63 46 0   0      error (invalid witness file) 0 --- inspect .0050 .0069 .54 0    0     - --- inspect - --- inspect
email_spec8_product32_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 120   51   470 1300 0      0     error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .023 .025 5.6 0    0     error (invalid witness file) 0 --- inspect 1.3  .81 49 0   0      error (invalid witness file) 0 --- inspect .0064 .0081 .53 0    0     - --- inspect - --- inspect
email_spec8_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   490 1400 0      0     error (invalid witness file) 0 --- inspect .84 .52 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.3  .81 48 0   0      error (invalid witness file) 0 --- inspect .0058 .0075 .53 0    0     - --- inspect - --- inspect
email_spec8_product34_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   55   490 1300 0      0     error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .78 47 0   0      error (invalid witness file) 0 --- inspect .0053 .0067 .54 0    0     - --- inspect - --- inspect
email_spec8_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 140   62   500 1300 0      0     error (invalid witness file) 0 --- inspect .75 .47 43 0   0     error (2) 0 --- inspect .023 .025 5.7 0    0     error (invalid witness file) 0 --- inspect 1.2  .86 48 0   0      error (invalid witness file) 0 --- inspect .0047 .0058 .54 0    0     - --- inspect - --- inspect
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 14   11   440 160 0      0     error (invalid witness file) 0 --- inspect .75 .45 42 0   0     error (2) 0 --- inspect .021 .023 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .68 46 0   0      error (invalid witness file) 0 --- inspect .0050 .0069 .52 0    0     - --- inspect - --- inspect
email_spec9_product15_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 140   62   480 1400 0      0     error (invalid witness file) 0 --- inspect .67 .42 40 0   0     error (2) 0 --- inspect .025 .026 5.7 0    0     error (invalid witness file) 0 --- inspect 1.2  .74 47 0   0      error (invalid witness file) 0 --- inspect .0020 .0026 .53 0    0     - --- inspect - --- inspect
email_spec9_product16_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   55   490 1300 0      0     error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .025 .025 5.5 0    0     error (invalid witness file) 0 --- inspect 1.2  .75 47 0   0      error (invalid witness file) 0 --- inspect .0020 .0026 .41 0    0     - --- inspect - --- inspect
email_spec9_product20_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 140   62   490 1300 0      0     error (invalid witness file) 0 --- inspect .75 .47 40 0   0     error (2) 0 --- inspect .024 .025 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0054 .0072 .54 0    0     - --- inspect - --- inspect
email_spec9_product21_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   55   490 1300 0      0     error (invalid witness file) 0 --- inspect .64 .41 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0    0     error (invalid witness file) 0 --- inspect 1.3  .81 46 0   0      error (invalid witness file) 0 --- inspect .0021 .0023 .41 0    0     - --- inspect - --- inspect
email_spec9_product22_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   480 1200 0      0     error (invalid witness file) 0 --- inspect .70 .43 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.4  .88 47 0   0      error (invalid witness file) 0 --- inspect .0039 .0051 .54 0    0     - --- inspect - --- inspect
email_spec9_product26_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   470 1300 0      0     error (invalid witness file) 0 --- inspect .73 .46 43 0   0     error (2) 0 --- inspect .024 .026 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .80 47 0   0      error (invalid witness file) 0 --- inspect .0020 .0026 .54 0    0     - --- inspect - --- inspect
email_spec9_product30_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 120   58   470 1500 0      0     error (invalid witness file) 0 --- inspect .60 .36 40 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .75 47 0   0      error (invalid witness file) 0 --- inspect .0062 .0080 .54 0    0     - --- inspect - --- inspect
email_spec9_product31_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   54   490 1200 0      0     error (invalid witness file) 0 --- inspect .67 .40 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0      error (invalid witness file) 0 --- inspect .0013 .0015 .41 0    0     - --- inspect - --- inspect
email_spec9_product32_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 120   58   470 1400 0      0     error (invalid witness file) 0 --- inspect .77 .48 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .62 47 0   0      error (invalid witness file) 0 --- inspect .0021 .0028 .54 0    0     - --- inspect - --- inspect
email_spec9_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   55   510 1400 0      0     error (invalid witness file) 0 --- inspect .73 .44 40 0   0     error (2) 0 --- inspect .025 .026 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .61 47 0   0      error (invalid witness file) 0 --- inspect .0014 .0016 .40 0    0     - --- inspect - --- inspect
email_spec9_product34_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 140   62   500 1500 0      0     error (invalid witness file) 0 --- inspect .71 .43 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0      error (invalid witness file) 0 --- inspect .0062 .0079 .52 0    0     - --- inspect - --- inspect
email_spec9_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   55   490 1300 0      0     error (invalid witness file) 0 --- inspect .77 .46 40 0   0     error (2) 0 --- inspect .026 .028 5.7 0    0     error (invalid witness file) 0 --- inspect 1.2  .74 46 0   0      error (invalid witness file) 0 --- inspect .0047 .0058 .53 0    0     - --- inspect - --- inspect
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 14   11   430 170 0      0     error (invalid witness file) 0 --- inspect .61 .37 42 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 48 0   0      error (invalid witness file) 0 --- inspect .0059 .010  .53 0    0     - --- inspect - --- inspect
email_spec0_product05_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 23 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0    
email_spec0_product09_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 27 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 41 0   0      error (2) 0 --- inspect .027 .028 5.5 0    0    
email_spec0_product10_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0    
email_spec0_product11_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 18 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0    
email_spec0_product19_true-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 750 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .40 41 0   0      error (2) 0 --- inspect .020 .022 5.6 0    0    
email_spec0_product24_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 23 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
email_spec0_product25_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0      error (2) 0 --- inspect .025 .027 5.7 0    0    
email_spec0_product27_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0    
email_spec0_product36_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 24 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
email_spec0_product37_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 22 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
email_spec0_product38_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
email_spec0_product40_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 41 0   0      error (2) 0 --- inspect .023 .025 5.6 0    0    
email_spec11_product03_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 25 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
email_spec11_product07_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 19 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
email_spec11_product08_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 19 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
email_spec11_product10_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 19 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
email_spec11_product18_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 21 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0    
email_spec11_product23_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 21 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .026 .028 5.8 0    0    
email_spec11_product24_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 19 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .50 42 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
email_spec11_product27_true-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 730 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .40 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
email_spec11_product36_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
email_spec11_product37_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
email_spec11_product39_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 19 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
email_spec11_product40_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 21 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .37 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
email_spec1_product12_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 25 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .47 41 0   0      error (2) 0 --- inspect .027 .028 5.8 0    0    
email_spec1_product28_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 21 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
email_spec27_product13_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 24 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0    
email_spec27_product28_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 24 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 40 0   0      error (2) 0 --- inspect .032 .033 5.7 0    0    
email_spec4_product13_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .42 41 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0    
email_spec4_product17_true-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
email_spec4_product28_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 19 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0    
email_spec4_product29_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 23 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
email_spec7_product13_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
email_spec7_product17_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.7 1.7 200 24 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .47 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
email_spec7_product18_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 22 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
email_spec7_product19_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 19 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0      error (2) 0 --- inspect .024 .026 5.6 0    0    
email_spec7_product23_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 23 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
email_spec7_product24_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 24 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
email_spec7_product25_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 23 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0    
email_spec7_product27_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0    
email_spec8_product12_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 23 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 42 0   0      error (2) 0 --- inspect .027 .028 5.5 0    0    
email_spec8_product14_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 21 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
email_spec8_product28_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 18 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .40 40 0   0      error (2) 0 --- inspect .029 .030 5.7 0    0    
email_spec8_product29_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 25 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .024 .025 5.8 0    0    
email_spec9_product12_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0    
email_spec9_product14_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.7 1.7 200 23 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .49 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
email_spec9_product28_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 22 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .020 .022 5.6 0    0    
email_spec9_product29_true-unreach-call_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0    
minepump_spec1_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 640 0      0     false(unreach-call) 1 wit inspect 6.0  3.3  260 0   0     true -32 --- inspect 12     6.5   320   .66 0     unknown 0 --- inspect 4.3  2.5  250 0   0      false(unreach-call) 1 --- inspect .68   .68   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   450 660 0      0     false(unreach-call) 1 wit inspect 4.9  2.7  260 0   0     true -32 --- inspect 9.8   5.4   320   .66 0     unknown 0 --- inspect 4.3  2.5  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 .020 - --- inspect - --- inspect
minepump_spec1_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 66   43   440 770 0      0     false(unreach-call) 1 wit inspect 6.1  3.3  260 0   0     true -32 --- inspect 9.2   5.5   330   .66 0     unknown 0 --- inspect 5.3  3.1  250 0   0      false(unreach-call) 1 --- inspect .67   .67   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 66   43   450 840 0      0     false(unreach-call) 1 wit inspect 6.2  3.3  260 0   0     true -32 --- inspect 9.6   5.3   320   .66 0     unknown 0 --- inspect 4.2  2.4  250 0   0      false(unreach-call) 1 --- inspect .69   .69   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product37_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   40   440 740 0      0     false(unreach-call) 1 wit inspect 5.4  3.0  250 0   0     true -32 --- inspect 11     6.1   320   .66 0     unknown 0 --- inspect 4.6  2.7  250 0   0      false(unreach-call) 1 --- inspect .69   .68   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product38_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 830 0      0     false(unreach-call) 1 wit inspect 6.0  3.3  250 0   0     true -32 --- inspect 12     6.9   320   .66 0     unknown 0 --- inspect 5.7  3.2  250 0   0      false(unreach-call) 1 --- inspect .67   .68   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 66   43   440 830 0      0     false(unreach-call) 1 wit inspect 6.0  3.2  260 0   0     true -32 --- inspect 9.8   5.7   320   .66 0     unknown 0 --- inspect 4.3  2.4  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 66   43   440 900 0      0     false(unreach-call) 1 wit inspect 5.6  3.0  260 0   0     true -32 --- inspect 12     6.7   320   .66 0     unknown 0 --- inspect 4.4  2.5  250 0   .16   false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 120   62   450 1200 0      0     false(unreach-call) 1 wit inspect 6.7  3.7  260 0   0     true -32 --- inspect 11     6.2   320   .66 0     unknown 0 --- inspect 4.2  2.4  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 120   62   450 1500 0      0     false(unreach-call) 1 wit inspect 5.3  2.9  270 0   0     true -32 --- inspect 12     6.9   320   .66 0     unknown 0 --- inspect 4.8  2.8  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 130   65   450 1300 0      0     false(unreach-call) 1 wit inspect 5.6  3.1  260 0   0     true -32 --- inspect 11     6.4   320   .66 0     unknown 0 --- inspect 5.4  3.1  250 0   0      false(unreach-call) 1 --- inspect .69   .68   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 130   65   460 1300 0      0     false(unreach-call) 1 wit inspect 5.9  3.2  260 0   0     true -32 --- inspect 11     6.6   320   .62 0     unknown 0 --- inspect 5.7  3.2  250 0   0      false(unreach-call) 1 --- inspect .68   .69   20    .14 0     - --- inspect - --- inspect
minepump_spec1_product49_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   24   440 460 0      0     false(unreach-call) 1 wit inspect 5.3  3.0  260 0   0     true -32 --- inspect 9.3   5.5   320   .66 0     unknown 0 --- inspect 5.4  3.1  250 0   0      false(unreach-call) 1 --- inspect .67   .66   20    .14 .020 - --- inspect - --- inspect
minepump_spec1_product50_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 61   40   440 780 0      0     false(unreach-call) 1 wit inspect 5.1  2.8  260 0   0     true -32 --- inspect 9.2   5.2   330   .66 0     unknown 0 --- inspect 5.4  3.1  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .15 0     - --- inspect - --- inspect
minepump_spec1_product51_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 66   43   440 800 0      0     false(unreach-call) 1 wit inspect 5.6  3.1  260 0   0     true -32 --- inspect 12     6.8   330   .66 0     unknown 0 --- inspect 5.1  2.9  250 0   0      false(unreach-call) 1 --- inspect .70   .71   20    .15 0     - --- inspect - --- inspect
minepump_spec1_product52_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 48   25   440 520 0      0     false(unreach-call) 1 wit inspect 5.4  3.0  260 0   0     true -32 --- inspect 10     5.8   330   .66 0     unknown 0 --- inspect 5.0  2.8  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .15 0     - --- inspect - --- inspect
minepump_spec1_product53_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 62   40   440 670 0      0     false(unreach-call) 1 wit inspect 5.8  3.2  250 0   0     true -32 --- inspect 11     6.2   320   .66 0     unknown 0 --- inspect 4.5  2.6  250 0   0      false(unreach-call) 1 --- inspect .69   .70   20    .15 0     - --- inspect - --- inspect
minepump_spec1_product54_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 61   40   440 650 0      0     false(unreach-call) 1 wit inspect 5.8  3.1  260 0   0     true -32 --- inspect 12     6.6   330   .66 0     unknown 0 --- inspect 4.3  2.5  250 0   0      false(unreach-call) 1 --- inspect .67   .67   20    .15 .020 - --- inspect - --- inspect
minepump_spec1_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 48   25   440 510 0      0     false(unreach-call) 1 wit inspect 5.9  3.2  260 0   0     true -32 --- inspect 10     5.5   320   .66 0     unknown 0 --- inspect 4.4  2.5  250 0   0      false(unreach-call) 1 --- inspect .67   .67   20    .15 .020 - --- inspect - --- inspect
minepump_spec1_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 66   43   440 810 0      0     false(unreach-call) 1 wit inspect 6.1  3.4  260 0   0     true -32 --- inspect 12     6.6   310   .66 0     unknown 0 --- inspect 4.3  2.5  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .15 0     - --- inspect - --- inspect
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 9500 .0041 0     error (invalid witness file) 0 --- inspect .73 .45 42 0   0     error (2) 0 --- inspect .029 .030 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 46 0   0      error (invalid witness file) 0 --- inspect .0026 .0033 .53 0    0     - --- inspect - --- inspect
minepump_spec2_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 140   66   450 1400 0      0     false(unreach-call) 1 wit inspect 4.8  2.6  260 0   0     true -32 --- inspect 11     6.0   320   .66 0     unknown 0 --- inspect 4.2  2.5  250 0   0      false(unreach-call) 1 --- inspect .67   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec2_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 150   69   450 1500 0      0     false(unreach-call) 1 wit inspect 6.5  3.5  260 0   0     true -32 --- inspect 10     6.1   320   .66 0     unknown 0 --- inspect 4.3  2.5  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec2_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 150   69   450 1500 0      0     false(unreach-call) 1 wit inspect 5.7  3.1  260 0   0     true -32 --- inspect 11     6.4   330   .66 0     unknown 0 --- inspect 4.5  2.6  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 .020 - --- inspect - --- inspect
minepump_spec2_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 160   74   450 1400 0      0     false(unreach-call) 1 wit inspect 4.9  2.7  260 0   0     true -32 --- inspect 11     5.9   320   .66 0     unknown 0 --- inspect 5.1  2.9  250 0   0      false(unreach-call) 1 --- inspect .67   .69   20    .14 0     - --- inspect - --- inspect
minepump_spec2_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 250   98   470 2300 0      0     false(unreach-call) 1 wit inspect 7.1  3.9  270 0   0     true -32 --- inspect 12     6.6   320   .66 0     unknown 0 --- inspect 5.0  2.9  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec2_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 250   96   470 2200 0      0     false(unreach-call) 1 wit inspect 6.9  3.8  270 0   0     true -32 --- inspect 9.2   5.5   320   .66 0     unknown 0 --- inspect 4.4  2.6  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec2_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 230   83   460 2300 0      0     false(unreach-call) 1 wit inspect 6.1  3.4  270 0   0     true -32 --- inspect 11     6.4   320   .66 0     unknown 0 --- inspect 4.7  2.7  250 0   0      false(unreach-call) 1 --- inspect .68   .68   20    .14 0     - --- inspect - --- inspect
minepump_spec2_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 230   83   460 2000 0      0     false(unreach-call) 1 wit inspect 7.2  3.9  270 0   0     true -32 --- inspect 10     5.8   320   .66 0     unknown 0 --- inspect 5.4  3.1  250 0   0      false(unreach-call) 1 --- inspect .69   .68   20    .15 0     - --- inspect - --- inspect
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 8500 .0041 0     error (invalid witness file) 0 --- inspect .61 .38 42 0   0     error (2) 0 --- inspect .032 .033 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .64 47 0   0      error (invalid witness file) 0 --- inspect .0023 .0029 .52 0    0     - --- inspect - --- inspect
minepump_spec3_product01_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 510 0      0     false(unreach-call) 1 wit inspect 5.5  3.0  260 0   0     true -32 --- inspect 10     5.7   320   .66 0     unknown 0 --- inspect 4.3  2.5  260 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product02_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   24   440 520 0      0     false(unreach-call) 1 wit inspect 5.1  2.8  260 0   0     true -32 --- inspect 9.8   5.4   320   .66 0     unknown 0 --- inspect 5.3  3.0  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 .020 - --- inspect - --- inspect
minepump_spec3_product03_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 480 0      0     false(unreach-call) 1 wit inspect 5.8  3.1  260 0   0     true -32 --- inspect 11     6.1   320   .66 0     unknown 0 --- inspect 4.5  2.6  250 0   0      false(unreach-call) 1 --- inspect .67   .66   20    .14 .020 - --- inspect - --- inspect
minepump_spec3_product04_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 460 0      0     false(unreach-call) 1 wit inspect 4.9  2.7  260 0   0     true -32 --- inspect 11     6.3   330   .66 0     unknown 0 --- inspect 4.5  2.6  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product05_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 45   24   440 510 0      0     false(unreach-call) 1 wit inspect 5.1  2.8  260 0   0     true -32 --- inspect 11     6.5   330   .66 0     unknown 0 --- inspect 4.2  2.5  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product06_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 490 0      0     false(unreach-call) 1 wit inspect 5.6  3.0  260 0   0     true -32 --- inspect 11     6.3   320   .66 0     unknown 0 --- inspect 4.6  2.6  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product07_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 460 0      0     false(unreach-call) 1 wit inspect 5.9  3.2  250 0   0     true -32 --- inspect 9.7   5.7   320   .66 0     unknown 0 --- inspect 5.6  3.2  250 0   0      false(unreach-call) 1 --- inspect .67   .70   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product08_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 520 0      0     false(unreach-call) 1 wit inspect 6.0  3.3  260 0   0     true -32 --- inspect 9.3   5.6   330   .62 0     unknown 0 --- inspect 5.2  3.0  250 0   0      false(unreach-call) 1 --- inspect .65   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product09_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 700 0      0     false(unreach-call) 1 wit inspect 5.3  2.9  260 0   0     true -32 --- inspect 10     6.0   320   .66 0     unknown 0 --- inspect 5.3  3.0  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 740 0      0     false(unreach-call) 1 wit inspect 4.8  2.6  260 0   0     true -32 --- inspect 9.1   5.4   320   .66 0     unknown 0 --- inspect 4.2  2.4  250 0   0      false(unreach-call) 1 --- inspect .65   .64   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 730 0      0     false(unreach-call) 1 wit inspect 4.6  2.6  260 0   0     true -32 --- inspect 12     6.6   320   .66 0     unknown 0 --- inspect 4.1  2.4  250 0   0      false(unreach-call) 1 --- inspect .70   .73   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 670 0      0     false(unreach-call) 1 wit inspect 4.8  2.6  260 0   0     true -32 --- inspect 11     6.2   320   .66 0     unknown 0 --- inspect 4.2  2.4  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   24   440 480 0      0     false(unreach-call) 1 wit inspect 5.9  3.2  260 0   0     true -32 --- inspect 9.5   5.6   320   .66 0     unknown 0 --- inspect 5.2  3.0  250 0   0      false(unreach-call) 1 --- inspect .68   .68   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 540 0      0     false(unreach-call) 1 wit inspect 4.7  2.6  260 0   0     true -32 --- inspect 11     6.6   320   .66 0     unknown 0 --- inspect 4.3  2.5  250 0   0      false(unreach-call) 1 --- inspect .67   .67   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product15_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 770 0      0     false(unreach-call) 1 wit inspect 4.9  2.7  250 0   0     true -32 --- inspect 12     6.7   310   .66 0     unknown 0 --- inspect 5.4  3.1  250 0   0      false(unreach-call) 1 --- inspect .71   .71   20    .14 .020 - --- inspect - --- inspect
minepump_spec3_product16_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 690 0      0     false(unreach-call) 1 wit inspect 5.7  3.1  260 0   0     true -32 --- inspect 10     5.6   330   .66 0     unknown 0 --- inspect 5.2  3.0  250 0   0      false(unreach-call) 1 --- inspect .69   .69   20    .14 .020 - --- inspect - --- inspect
minepump_spec3_product17_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 480 0      0     false(unreach-call) 1 wit inspect 5.0  2.7  250 0   0     true -32 --- inspect 11     6.3   320   .66 0     unknown 0 --- inspect 4.3  2.5  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product18_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 660 0      0     false(unreach-call) 1 wit inspect 5.1  2.7  250 0   0     true -32 --- inspect 11     6.2   320   .66 0     unknown 0 --- inspect 5.3  3.1  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product19_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 460 0      0     false(unreach-call) 1 wit inspect 6.0  3.3  260 0   0     true -32 --- inspect 10     5.5   320   .66 0     unknown 0 --- inspect 4.8  2.8  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product20_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 720 0      0     false(unreach-call) 1 wit inspect 6.3  3.4  260 0   0     true -32 --- inspect 11     5.9   320   .66 0     unknown 0 --- inspect 5.1  2.9  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product21_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   24   440 510 0      0     false(unreach-call) 1 wit inspect 4.7  2.6  260 0   0     true -32 --- inspect 11     6.0   320   .66 0     unknown 0 --- inspect 5.2  3.0  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product22_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 470 0      0     false(unreach-call) 1 wit inspect 5.6  3.1  260 0   0     true -32 --- inspect 9.4   5.2   330   .66 0     unknown 0 --- inspect 4.2  2.4  250 0   0      false(unreach-call) 1 --- inspect .67   .68   20    .14 .020 - --- inspect - --- inspect
minepump_spec3_product23_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 780 0      0     false(unreach-call) 1 wit inspect 5.0  2.7  260 0   0     true -32 --- inspect 9.8   5.7   320   .66 0     unknown 0 --- inspect 4.9  2.8  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product24_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   450 700 0      0     false(unreach-call) 1 wit inspect 5.0  2.7  260 0   0     true -32 --- inspect 12     6.7   320   .66 0     unknown 0 --- inspect 4.6  2.6  250 0   0      false(unreach-call) 1 --- inspect .71   .71   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product25_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 640 0      0     false(unreach-call) 1 wit inspect 5.2  2.8  260 0   0     true -32 --- inspect 11     6.5   320   .66 0     unknown 0 --- inspect 4.3  2.5  260 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product26_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 61   40   440 660 0      0     false(unreach-call) 1 wit inspect 5.8  3.2  250 0   0     true -32 --- inspect 9.6   5.3   320   .66 0     unknown 0 --- inspect 4.4  2.5  250 0   0      false(unreach-call) 1 --- inspect .68   .68   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product27_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 440 0      0     false(unreach-call) 1 wit inspect 4.7  2.6  250 0   0     true -32 --- inspect 9.6   5.7   330   .66 0     unknown 0 --- inspect 5.4  3.1  250 0   0      false(unreach-call) 1 --- inspect .67   .67   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product28_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 630 0      0     false(unreach-call) 1 wit inspect 5.7  3.2  250 0   0     true -32 --- inspect 12     6.6   330   .66 0     unknown 0 --- inspect 4.2  2.4  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product29_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 780 0      0     false(unreach-call) 1 wit inspect 5.9  3.2  260 0   0     true -32 --- inspect 10     6.0   320   .66 0     unknown 0 --- inspect 4.9  2.8  250 0   0      false(unreach-call) 1 --- inspect .66   .68   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product30_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 690 0      0     false(unreach-call) 1 wit inspect 5.4  2.9  250 0   0     true -32 --- inspect 12     7.0   320   .66 0     unknown 0 --- inspect 4.3  2.5  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 .020 - --- inspect - --- inspect
minepump_spec3_product31_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 60   39   440 730 0      0     false(unreach-call) 1 wit inspect 6.3  3.4  260 0   0     true -32 --- inspect 9.3   5.2   330   .66 0     unknown 0 --- inspect 5.4  3.1  250 0   0      false(unreach-call) 1 --- inspect .69   .69   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product32_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 44   23   440 450 0      0     false(unreach-call) 1 wit inspect 5.7  3.1  250 0   0     true -32 --- inspect 11     6.4   320   .66 0     unknown 0 --- inspect 5.9  3.3  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 51   26   440 520 0      0     false(unreach-call) 1 wit inspect 6.1  3.3  250 0   0     true -32 --- inspect 11     6.5   320   .66 0     unknown 0 --- inspect 4.6  2.6  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 70   45   450 780 0      0     false(unreach-call) 1 wit inspect 5.9  3.2  260 0   0     true -32 --- inspect 9.3   5.6   320   .66 0     unknown 0 --- inspect 5.4  3.1  250 0   .73   error (2) 0 --- inspect .66   .66   20    .14 .020 - --- inspect - --- inspect
minepump_spec3_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 70   45   450 920 0      0     false(unreach-call) 1 wit inspect 4.6  2.5  260 0   0     true -32 --- inspect 13     7.3   320   .66 0     unknown 0 --- inspect 4.9  2.8  250 0   0      false(unreach-call) 1 --- inspect .66   .66   21    .14 0     - --- inspect - --- inspect
minepump_spec3_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 51   26   440 580 0      0     false(unreach-call) 1 wit inspect 5.7  3.1  260 0   0     true -32 --- inspect 11     6.7   330   .66 0     unknown 0 --- inspect 5.8  3.3  250 0   0      false(unreach-call) 1 --- inspect .67   .67   20    .14 .020 - --- inspect - --- inspect
minepump_spec3_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 70   45   440 890 0      0     false(unreach-call) 1 wit inspect 4.9  2.7  260 0   0     true -32 --- inspect 9.9   5.5   320   .66 0     unknown 0 --- inspect 4.4  2.5  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 70   46   450 820 0      0     false(unreach-call) 1 wit inspect 5.8  3.2  250 0   0     true -32 --- inspect 10     5.8   320   .66 0     unknown 0 --- inspect 5.8  3.3  250 0   0      error (2) 0 --- inspect .66   .67   20    .14 0     - --- inspect - --- inspect
minepump_spec3_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 51   26   440 510 0      0     false(unreach-call) 1 wit inspect 4.7  2.6  260 0   0     true -32 --- inspect 12     6.7   330   .62 0     unknown 0 --- inspect 5.0  2.8  250 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .15 0     - --- inspect - --- inspect
minepump_spec3_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 51   27   440 610 0      0     false(unreach-call) 1 wit inspect 6.1  3.3  280 0   0     true -32 --- inspect 10     6.0   320   .66 0     unknown 0 --- inspect 5.1  2.9  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .15 0     - --- inspect - --- inspect
minepump_spec3_product51_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 51   27   440 620 0      0     false(unreach-call) 1 wit inspect 6.1  3.3  260 0   0     true -32 --- inspect 12     6.9   330   .66 0     unknown 0 --- inspect 5.5  3.2  250 0   0      false(unreach-call) 1 --- inspect .67   .67   20    .15 0     - --- inspect - --- inspect
minepump_spec3_product52_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 71   46   440 950 0      0     false(unreach-call) 1 wit inspect 5.8  3.2  260 0   0     true -32 --- inspect 9.7   5.8   320   .66 0     unknown 0 --- inspect 5.6  3.2  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .15 0     - --- inspect - --- inspect
minepump_spec3_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 71   46   450 850 0      0     false(unreach-call) 1 wit inspect 5.3  2.9  250 0   0     true -32 --- inspect 12     7.1   330   .66 0     unknown 0 --- inspect 5.0  2.8  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .15 .020 - --- inspect - --- inspect
minepump_spec3_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 51   27   440 630 0      0     false(unreach-call) 1 wit inspect 6.6  3.6  280 0   0     true -32 --- inspect 12     6.3   330   .66 0     unknown 0 --- inspect 5.5  3.1  250 0   0      false(unreach-call) 1 --- inspect .70   .70   20    .15 .020 - --- inspect - --- inspect
minepump_spec3_product59_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 51   26   440 600 0      0     false(unreach-call) 1 wit inspect 6.1  3.3  280 0   0     true -32 --- inspect 11     5.8   330   .66 0     unknown 0 --- inspect 4.2  2.4  250 0   1.2    false(unreach-call) 1 --- inspect .66   .66   20    .15 .020 - --- inspect - --- inspect
minepump_spec3_product60_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 52   27   440 550 0      0     false(unreach-call) 1 wit inspect 4.8  2.6  260 0   0     true -32 --- inspect 12     7.0   320   .62 0     unknown 0 --- inspect 5.0  2.9  250 0   0      false(unreach-call) 1 --- inspect .69   .69   20    .15 .020 - --- inspect - --- inspect
minepump_spec3_product63_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 71   46   450 850 0      0     false(unreach-call) 1 wit inspect 5.2  2.9  260 0   0     true -32 --- inspect 9.8   5.4   320   .66 0     unknown 0 --- inspect 5.3  3.1  250 0   0      false(unreach-call) 1 --- inspect .69   .69   20    .15 0     - --- inspect - --- inspect
minepump_spec3_product64_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 51   27   440 580 0      0     false(unreach-call) 1 wit inspect 4.6  2.6  260 0   0     true -32 --- inspect 9.4   5.4   320   .66 0     unknown 0 --- inspect 4.9  2.8  250 0   0      false(unreach-call) 1 --- inspect .67   .67   20    .15 0     - --- inspect - --- inspect
minepump_spec3_productSimulator_false-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 8400 .0041 0     error (invalid witness file) 0 --- inspect .69 .43 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 48 0   0      error (invalid witness file) 0 --- inspect .0048 .0055 .39 0    0     - --- inspect - --- inspect
minepump_spec4_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 580   180   470 4700 0      0     false(unreach-call) 1 wit inspect 5.7  3.1  270 0   0     true -32 --- inspect 9.1   5.1   330   .66 0     unknown 0 --- inspect 4.9  2.8  250 0   .0041 false(unreach-call) 1 --- inspect .69   .69   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 220   83   460 2100 0      0     false(unreach-call) 1 wit inspect 6.1  3.3  270 0   0     true -32 --- inspect 10     6.1   310   .62 0     unknown 0 --- inspect 4.8  2.8  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 .020 - --- inspect - --- inspect
minepump_spec4_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 640   200   470 5100 0      0     false(unreach-call) 1 wit inspect 7.3  3.9  270 0   0     true -32 --- inspect 12     7.0   320   .66 0     unknown 0 --- inspect 5.2  3.0  250 0   0      false(unreach-call) 1 --- inspect .68   .68   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 650   200   470 5300 0      0     false(unreach-call) 1 wit inspect 7.3  4.0  270 0   0     true -32 --- inspect 12     6.3   320   .66 0     unknown 0 --- inspect 4.6  2.7  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product37_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 650   200   470 5300 0      0     false(unreach-call) 1 wit inspect 7.1  3.8  270 0   0     true -32 --- inspect 9.0   5.3   320   .66 0     unknown 0 --- inspect 4.8  2.7  250 0   0      error (2) 0 --- inspect .66   .68   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product38_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 240   89   460 2100 0      0     false(unreach-call) 1 wit inspect 7.7  4.2  270 0   0     true -32 --- inspect 11     6.5   320   .66 0     unknown 0 --- inspect 5.3  3.1  250 0   0      error (2) 0 --- inspect .66   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 270   100   460 2500 0      0     false(unreach-call) 1 wit inspect 7.0  3.9  270 0   0     true -32 --- inspect 11     6.8   320   .66 0     unknown 0 --- inspect 5.4  3.1  260 0   0      error (2) 0 --- inspect .65   .65   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 480   150   460 3600 0      0     false(unreach-call) 1 wit inspect 6.1  3.4  270 0   0     true -32 --- inspect 12     6.9   320   .66 0     unknown 0 --- inspect 5.6  3.2  250 0   0      error (2) 0 --- inspect .66   .66   20    .14 .020 - --- inspect - --- inspect
minepump_spec4_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 600   190   480 4600 0      0     false(unreach-call) 1 wit inspect 6.6  3.6  270 0   0     true -32 --- inspect 10     6.1   310   .66 0     unknown 0 --- inspect 5.1  3.0  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 220   83   460 1900 0      0     false(unreach-call) 1 wit inspect 6.4  3.6  270 0   0     true -32 --- inspect 11     6.5   330   .66 0     unknown 0 --- inspect 4.4  2.6  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 230   86   450 2000 0      0     false(unreach-call) 1 wit inspect 5.9  3.3  270 0   0     true -32 --- inspect 10     5.6   320   .62 0     unknown 0 --- inspect 5.5  3.1  250 0   0      false(unreach-call) 1 --- inspect .70   .70   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 650   210   480 5500 0      0     false(unreach-call) 1 wit inspect 8.0  4.4  270 0   0     true -32 --- inspect 10     5.6   320   .66 0     unknown 0 --- inspect 4.4  2.5  250 0   0      false(unreach-call) 1 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product45_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 670   210   480 5800 0      0     false(unreach-call) 1 wit inspect 6.7  3.7  270 0   .020 true -32 --- inspect 9.4   5.6   330   .62 0     unknown 0 --- inspect 5.9  3.3  250 0   0      error (2) 0 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product46_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 270   100   460 2400 0      0     false(unreach-call) 1 wit inspect 7.8  4.2  290 0   0     true -32 --- inspect 10     5.7   320   .66 0     unknown 0 --- inspect 4.6  2.6  250 0   0      error (2) 0 --- inspect .65   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 660   210   480 5300 0      0     false(unreach-call) 1 wit inspect 6.9  3.8  270 0   0     true -32 --- inspect 9.6   5.3   320   .66 0     unknown 0 --- inspect 5.6  3.2  250 0   0      error (2) 0 --- inspect .66   .66   20    .14 0     - --- inspect - --- inspect
minepump_spec4_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 270   100   460 2700 0      0     false(unreach-call) 1 wit inspect 7.2  4.0  270 0   0     true -32 --- inspect 9.9   5.6   320   .66 0     unknown 0 --- inspect 5.1  2.9  250 0   0      error (2) 0 --- inspect .67   .67   20    .14 0     - --- inspect - --- inspect
minepump_spec4_productSimulator_false-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 10000 .0041 0     error (invalid witness file) 0 --- inspect .65 .39 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .78 47 0   0      error (invalid witness file) 0 --- inspect .0017 .0019 .40 0    0     - --- inspect - --- inspect
minepump_spec1_product01_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0    
minepump_spec1_product02_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
minepump_spec1_product03_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 41 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0    
minepump_spec1_product04_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec1_product05_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec1_product06_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
minepump_spec1_product07_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec1_product08_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec1_product09_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
minepump_spec1_product10_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
minepump_spec1_product11_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec1_product12_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec1_product13_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec1_product14_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7200 .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 42 0   0      error (2) 0 --- inspect .027 .029 5.6 0    0    
minepump_spec1_product15_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .46 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec1_product16_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0    
minepump_spec1_product17_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec1_product18_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 40 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0    
minepump_spec1_product19_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec1_product20_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec1_product21_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 41 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0    
minepump_spec1_product22_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 42 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
minepump_spec1_product23_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec1_product24_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec1_product25_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 41 0   0      error (2) 0 --- inspect .027 .028 5.5 0    0    
minepump_spec1_product26_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .95 .57 42 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
minepump_spec1_product27_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec1_product28_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 41 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0    
minepump_spec1_product29_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec1_product30_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec1_product31_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .46 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec1_product32_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0    
minepump_spec1_product45_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec1_product46_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec1_product47_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .37 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0    
minepump_spec1_product48_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec1_product57_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0      error (2) 0 --- inspect .023 .025 5.6 0    0    
minepump_spec1_product58_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 40 0   0      error (2) 0 --- inspect .023 .025 5.6 0    0    
minepump_spec1_product59_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 41 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0    
minepump_spec1_product60_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0    
minepump_spec1_product61_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 42 0   0      error (2) 0 --- inspect .027 .029 5.6 0    0    
minepump_spec1_product62_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec1_product63_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0    
minepump_spec1_product64_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0      error (2) 0 --- inspect .028 .030 5.7 0    0    
minepump_spec2_product01_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 40 0   0      error (2) 0 --- inspect .029 .030 5.7 0    0    
minepump_spec2_product02_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec2_product03_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .025 .026 5.5 0    0    
minepump_spec2_product04_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0    
minepump_spec2_product05_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec2_product06_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0    
minepump_spec2_product07_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 42 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec2_product08_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 40 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0    
minepump_spec2_product09_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec2_product10_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0    
minepump_spec2_product11_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 40 0   0      error (2) 0 --- inspect .023 .024 5.8 0    0    
minepump_spec2_product12_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .43 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec2_product13_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec2_product14_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0    
minepump_spec2_product15_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
minepump_spec2_product16_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .022 .024 5.7 0    0    
minepump_spec2_product17_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7300 .0041 .13  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
minepump_spec2_product18_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec2_product19_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0    
minepump_spec2_product20_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec2_product21_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .027 .027 5.5 0    0    
minepump_spec2_product22_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 5900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .40 40 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0    
minepump_spec2_product23_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 41 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0    
minepump_spec2_product24_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7800 .0041 .15  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec2_product25_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0    
minepump_spec2_product26_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.5 0    0    
minepump_spec2_product27_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec2_product28_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec2_product29_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec2_product30_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0      error (2) 0 --- inspect .022 .022 5.5 0    0    
minepump_spec2_product31_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0      error (2) 0 --- inspect .025 .028 5.8 0    0    
minepump_spec2_product32_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0    
minepump_spec2_product37_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec2_product38_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0      error (2) 0 --- inspect .022 .025 5.6 0    0    
minepump_spec2_product39_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec2_product40_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0    
minepump_spec2_product45_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec2_product46_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec2_product47_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec2_product48_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0    
minepump_spec2_product49_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec2_product50_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0    
minepump_spec2_product51_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .47 40 0   0      error (2) 0 --- inspect .020 .021 5.7 0    0    
minepump_spec2_product52_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0    
minepump_spec2_product53_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec2_product54_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec2_product55_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 42 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
minepump_spec2_product56_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec2_product57_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .023 .024 5.5 0    0    
minepump_spec2_product58_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec2_product59_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0    
minepump_spec2_product60_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 7700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
minepump_spec2_product61_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0    
minepump_spec2_product62_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0      error (2) 0 --- inspect .030 .031 5.6 0    0    
minepump_spec2_product63_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec2_product64_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec3_product33_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec3_product34_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 40 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0    
minepump_spec3_product37_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0      error (2) 0 --- inspect .024 .026 5.7 0    0    
minepump_spec3_product38_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec3_product41_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 40 0   0      error (2) 0 --- inspect .021 .021 5.7 0    0    
minepump_spec3_product42_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec3_product45_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 42 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec3_product46_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 6300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
minepump_spec3_product49_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .40 40 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0    
minepump_spec3_product50_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec3_product53_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0    
minepump_spec3_product54_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec3_product57_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .021 .023 5.7 0    0    
minepump_spec3_product58_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0    
minepump_spec3_product61_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec3_product62_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec4_product01_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   400 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 41 0   0      error (2) 0 --- inspect .023 .024 5.7 0    0    
minepump_spec4_product02_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   400 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
minepump_spec4_product03_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 8000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0    
minepump_spec4_product04_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
minepump_spec4_product05_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   400 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 41 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0    
minepump_spec4_product06_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0    
minepump_spec4_product07_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec4_product08_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec4_product09_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   400 7600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
minepump_spec4_product10_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0      error (2) 0 --- inspect .023 .025 5.6 0    0    
minepump_spec4_product11_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec4_product12_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0    
minepump_spec4_product13_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   400 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
minepump_spec4_product14_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   400 7700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .50 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
minepump_spec4_product15_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
minepump_spec4_product16_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 41 0   0      error (2) 0 --- inspect .027 .029 5.6 0    0    
minepump_spec4_product17_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   400 6700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 43 0   0      error (2) 0 --- inspect .025 .027 5.6 0    0    
minepump_spec4_product18_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec4_product19_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0      error (2) 0 --- inspect .027 .028 5.5 0    0    
minepump_spec4_product20_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0    
minepump_spec4_product21_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   400 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec4_product22_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec4_product23_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0      error (2) 0 --- inspect .031 .032 5.6 0    0    
minepump_spec4_product24_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec4_product25_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   400 7600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec4_product26_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
minepump_spec4_product27_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
minepump_spec4_product28_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec4_product29_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   400 7500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
minepump_spec4_product30_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 8100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
minepump_spec4_product31_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec4_product32_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 42 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0    
minepump_spec4_product49_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7100 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec4_product50_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0      error (2) 0 --- inspect .022 .023 5.8 0    0    
minepump_spec4_product51_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 40 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0    
minepump_spec4_product52_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0    
minepump_spec4_product53_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 40 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0    
minepump_spec4_product54_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .48 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec4_product55_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0    
minepump_spec4_product56_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec4_product57_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7200 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec4_product58_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
minepump_spec4_product59_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0    
minepump_spec4_product60_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .47 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
minepump_spec4_product61_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .40 40 0   0      error (2) 0 --- inspect .023 .024 5.7 0    0    
minepump_spec4_product62_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec4_product63_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .43 40 0   0      error (2) 0 --- inspect .025 .026 5.7 0    0    
minepump_spec4_product64_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 40 0   0      error (2) 0 --- inspect .021 .024 5.6 0    0    
minepump_spec5_product01_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .029 .030 5.6 0    0    
minepump_spec5_product02_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
minepump_spec5_product03_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec5_product04_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec5_product05_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0      error (2) 0 --- inspect .023 .025 5.6 0    0    
minepump_spec5_product06_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .019 .020 5.6 0    0    
minepump_spec5_product07_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec5_product08_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0      error (2) 0 --- inspect .020 .022 5.6 0    0    
minepump_spec5_product09_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0      error (2) 0 --- inspect .027 .029 5.6 0    0    
minepump_spec5_product10_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0    
minepump_spec5_product11_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0      error (2) 0 --- inspect .025 .027 5.6 0    0    
minepump_spec5_product12_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0    
minepump_spec5_product13_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0    
minepump_spec5_product14_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec5_product15_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec5_product16_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0    
minepump_spec5_product17_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 5800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec5_product18_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 41 0   0      error (2) 0 --- inspect .023 .024 5.7 0    0    
minepump_spec5_product19_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0    
minepump_spec5_product20_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0    
minepump_spec5_product21_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 40 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0    
minepump_spec5_product22_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec5_product23_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec5_product24_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 40 0   0      error (2) 0 --- inspect .024 .024 5.5 0    0    
minepump_spec5_product25_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec5_product26_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0    
minepump_spec5_product27_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
minepump_spec5_product28_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec5_product29_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .021 .023 5.7 0    0    
minepump_spec5_product30_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   410 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
minepump_spec5_product31_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0    
minepump_spec5_product32_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0    
minepump_spec5_product33_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec5_product34_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0    
minepump_spec5_product35_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
minepump_spec5_product36_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec5_product37_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec5_product38_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .027 .028 5.8 0    0    
minepump_spec5_product39_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .42 41 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0    
minepump_spec5_product40_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0    
minepump_spec5_product41_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec5_product42_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 43 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    
minepump_spec5_product43_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec5_product44_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0      error (2) 0 --- inspect .025 .027 5.6 0    0    
minepump_spec5_product45_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .026 .027 5.5 0    0    
minepump_spec5_product46_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .49 41 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0    
minepump_spec5_product47_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 41 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0    
minepump_spec5_product48_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0    
minepump_spec5_product49_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0    
minepump_spec5_product50_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    
minepump_spec5_product51_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0      error (2) 0 --- inspect .029 .029 5.6 0    0    
minepump_spec5_product52_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0    
minepump_spec5_product53_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0    
minepump_spec5_product54_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   420 7100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0    
minepump_spec5_product55_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec5_product56_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7700 .0041 .020 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0    
minepump_spec5_product57_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .50 40 0   0      error (2) 0 --- inspect .023 .025 5.7 0    0    
minepump_spec5_product58_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
minepump_spec5_product59_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 8000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0      error (2) 0 --- inspect .025 .026 5.8 0    0    
minepump_spec5_product60_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 7400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0    
minepump_spec5_product61_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0      error (2) 0 --- inspect .021 .021 5.7 0    0    
minepump_spec5_product62_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   440 6600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    
minepump_spec5_product63_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .43 40 0   0      error (2) 0 --- inspect .025 .026 5.7 0    0    
minepump_spec5_product64_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 6600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0    
minepump_spec5_productSimulator_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   230   430 8800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0    
sv-benchmarks/c/product-lines/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 597 248 240000 66000 250000 1900000 .99 130   265 147 1200 690 49000 0   .020 265 -4704 2000 1100 58000 96 .078 265 34 940 550 43000 0   8.2 265 -292 110 110 3100 33   .91 332 92 11000 10000 100000 0   .0041 332 0 13000 8800 390000 42 .43
    correct results 193 239 16000 7300 84000 160000 0    130   147 147 1200 640 44000 0   .020 0 34 34 220 120 9100 0   6.1 124 124 91 91 2500 27   .72 46 92 2800 2300 60000 0   0      0
        correct true 46 92 400 400 17000 5000 0    0   0 0 0 0 46 92 2800 2300 60000 0   0      0
        correct false 147 147 16000 6900 66000 150000 0    130   147 147 1200 640 44000 0   .020 0 34 34 220 120 9100 0   6.1 124 124 91 91 2500 27   .72 0 0
    correct-unconfimed results 9 9 110 87 3400 1200 0    0   0 0 0 0 0 0
        correct-unconfirmed true 9 9 110 87 3400 1200 0    0   0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 0 147 -4704 2000 1100 57000 96 .078 0 13 -416 11 11 270 5.0 .15 0 0
        incorrect true 0 0 147 -4704 2000 1100 57000 96 .078 0 13 -416 11 11 270 5.0 .15 0 0
        incorrect false 0 0 0 0 0 0 0
score (597 tasks, max score: 929) 248 147 -4704 34 -292 92 0
Run set divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines