Tool CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:36:53 CET 2017-12-01 08:24:12 CET 2017-12-01 08:27:09 CET 2017-12-01 08:31:26 CET 2017-12-01 04:24:37 CET 2017-12-01 07:42:15 CET
Run set cpa-bam-bnb.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/product-lines/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
elevator_spec14_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 92   4600 710 false(unreach-call) 1 wit inspect 6.6  300 false(unreach-call) 1 wit inspect 19     820   unknown 0 wit inspect 5.8  270 false(unreach-call) 1 wit inspect .89   22    - wit inspect - wit inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130   5700 910 false(unreach-call) 1 wit inspect 6.7  300 false(unreach-call) 1 wit inspect 38     1400   unknown 0 wit inspect 6.6  270 false(unreach-call) 1 wit inspect .90   22    - wit inspect - wit inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 93   4800 670 false(unreach-call) 1 wit inspect 6.2  290 false(unreach-call) 1 wit inspect 26     980   unknown 0 wit inspect 5.7  270 false(unreach-call) 1 wit inspect .87   22    - wit inspect - wit inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140   6000 980 false(unreach-call) 1 wit inspect 6.5  300 false(unreach-call) 1 wit inspect 62     1500   unknown 0 wit inspect 5.8  270 false(unreach-call) 1 wit inspect .90   22    - wit inspect - wit inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .93 52 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5600 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0015 .32 - wit inspect - wit inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5200 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5200 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .93 48 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5700 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect 1.1  48 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5600 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 6100 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5100 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .93 50 error (invalid witness file) 0 wit inspect .0032 .34 - wit inspect - wit inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 6100 error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5700 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5800 error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect - wit inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5600 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5700 error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5500 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect - wit inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5300 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .98 51 error (invalid witness file) 0 wit inspect .0020 .26 - wit inspect - wit inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5400 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5600 error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .84 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5900 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5500 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8300 9100 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .92 50 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8800 8400 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8600 6900 error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .92 50 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8700 8600 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .97 50 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   9000 7800 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8600 9100 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .91 52 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8700 7800 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.1  52 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8600 7800 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8500 7600 error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8700 9400 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .025 5.0 error (invalid witness file) 0 wit inspect 1.1  48 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8500 8900 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .94 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5800 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 6200 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5900 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5300 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .69 50 error (invalid witness file) 0 wit inspect .0010 .31 - wit inspect - wit inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5800 error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   8300 7100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.8
elevator_spec13_product22_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   11000 7200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.9
elevator_spec13_product23_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   8100 7400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8
elevator_spec13_product24_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   8200 7400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .017 4.8
elevator_spec13_product29_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   8600 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .024 5.0
elevator_spec13_product30_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   11000 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8
elevator_spec13_product31_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   8600 8000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .022 4.9
elevator_spec13_product32_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   8000 7600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .021 4.8
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   8100 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.9
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 120   5500 870 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    580 out of memory 0 wit inspect 360     7000  
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 120   5300 830 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    660 out of memory 0 wit inspect 210     7000  
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 120   5500 960 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24    680 out of memory 0 wit inspect 330     7000  
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 190   6500 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    980 out of memory 0 wit inspect 230     7000  
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 140   5500 890 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24    720 out of memory 0 wit inspect 220     7000  
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 180   6500 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    1100 out of memory 0 wit inspect 240     7000  
elevator_spec1_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .024 4.8
elevator_spec1_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 4700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9
elevator_spec1_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.9
elevator_spec1_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
elevator_spec1_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .022 5.0
elevator_spec1_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 4500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8
elevator_spec1_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 4700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .021 4.8
elevator_spec1_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .020 5.0
elevator_spec1_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .021 4.9
elevator_spec1_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .023 4.8
elevator_spec1_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 5.0
elevator_spec1_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .026 4.8
elevator_spec2_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .024 4.8
elevator_spec2_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .017 4.9
elevator_spec2_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .017 5.0
elevator_spec2_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .025 5.0
elevator_spec2_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .024 4.9
elevator_spec2_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .019 5.0
elevator_spec2_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .020 4.9
elevator_spec2_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8
elevator_spec2_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .38 43 error (2) 0 wit inspect .021 5.0
elevator_spec2_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .018 4.9
elevator_spec2_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8
elevator_spec2_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8
elevator_spec3_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   9800 7600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 5.0
elevator_spec3_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   9400 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .023 4.8
elevator_spec3_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   9400 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.8
elevator_spec3_product18_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   9200 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .020 4.9
elevator_spec3_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8300 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .018 4.9
elevator_spec3_product22_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   9300 7600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .019 4.8
elevator_spec3_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   9400 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.9
elevator_spec3_product26_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   9200 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.9
elevator_spec3_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8300 7900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.8
elevator_spec3_product30_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   9300 8200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .022 4.9
elevator_spec9_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .020 5.0
elevator_spec9_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .021 4.8
elevator_spec9_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .83 44 error (2) 0 wit inspect .020 4.8
elevator_spec9_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9
elevator_spec9_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .020 4.9
elevator_spec9_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .022 5.0
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130   5500 1100 false(unreach-call) 1 wit inspect 6.6  290 unknown 0 wit inspect 49     770   unknown 0 wit inspect 5.8  270 true -32 wit inspect .89   20    - wit inspect - wit inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5200 error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .94 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 210   6600 1500 false(unreach-call) 1 wit inspect 6.2  290 unknown 0 wit inspect 35     640   unknown 0 wit inspect 5.1  270 true -32 wit inspect .90   20    - wit inspect - wit inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 6300 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0013 .32 - wit inspect - wit inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5200 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5900 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .99 47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 6100 error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 6000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .99 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 8200 error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5600 error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .89 48 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 6200 error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.0  51 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 580   9900 4200 false(unreach-call) 1 wit inspect 6.7  290 unknown 0 wit inspect 42     770   unknown 0 wit inspect 4.8  270 false(unreach-call) 1 wit inspect .88   20    - wit inspect - wit inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5400 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0037 .29 - wit inspect - wit inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 240   6900 1700 false(unreach-call) 1 wit inspect 6.4  290 unknown 0 wit inspect 58     730   unknown 0 wit inspect 6.4  280 false(unreach-call) 1 wit inspect .90   20    - wit inspect - wit inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5300 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0011 .27 - wit inspect - wit inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5200 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5300 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .89 50 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   8600 10000 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .89 51 error (invalid witness file) 0 wit inspect .0021 .33 - wit inspect - wit inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8000 9100 error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 83   4200 640 false(unreach-call) 1 wit inspect 7.7  290 true -32 wit inspect 8.3   400   unknown 0 wit inspect 6.3  270 true -32 wit inspect .91   21    - wit inspect - wit inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5900 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 430   9500 3300 false(unreach-call) 1 wit inspect 8.7  300 true -32 wit inspect 10     430   unknown 0 wit inspect 5.3  270 true -32 wit inspect .91   21    - wit inspect - wit inspect
email_spec1_product21_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5600 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8200 9200 error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 4700 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.0  52 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8200 9500 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0011 .31 - wit inspect - wit inspect
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 160   5700 1300 false(unreach-call) 1 wit inspect 8.3  300 true -32 wit inspect 10     420   unknown 0 wit inspect 6.4  270 true -32 wit inspect .88   22    - wit inspect - wit inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 240   6800 1700 false(unreach-call) 1 wit inspect 7.8  300 true -32 wit inspect 12     430   unknown 0 wit inspect 6.5  270 true -32 wit inspect .92   22    - wit inspect - wit inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   8300 9400 error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 320   8000 2400 false(unreach-call) 1 wit inspect 7.7  300 true -32 wit inspect 9.9   440   unknown 0 wit inspect 6.2  270 true -32 wit inspect .89   22    - wit inspect - wit inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 6500 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .98 49 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
email_spec1_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5600 error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0028 .28 - wit inspect - wit inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   8900 8300 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .88 47 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 350   8300 2500 false(unreach-call) 1 wit inspect 7.3  300 true -32 wit inspect 9.5   430   unknown 0 wit inspect 6.0  270 true -32 wit inspect .88   22    - wit inspect - wit inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 350   7800 2400 false(unreach-call) 1 wit inspect 7.0  300 true -32 wit inspect 11     410   unknown 0 wit inspect 5.4  270 true -32 wit inspect .94   22    - wit inspect - wit inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 320   8200 2500 false(unreach-call) 1 wit inspect 7.8  300 true -32 wit inspect 9.5   400   unknown 0 wit inspect 5.5  270 true -32 wit inspect .87   22    - wit inspect - wit inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5500 error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 5100 error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .82 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
email_spec27_product25_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 4800 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.1  51 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
email_spec27_product27_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 5400 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.0  51 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
email_spec27_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 160   5600 1300 false(unreach-call)