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