Tool ULTIMATE Automizer 0.1.23-3204b741 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-02 01:06:24 CET 2017-12-03 03:07:09 CET 2017-12-03 03:49:57 CET 2017-12-03 03:57:59 CET 2017-12-03 04:29:07 CET 2017-12-02 23:12:02 CET 2017-12-03 03:11:19 CET
Run set uautomizer.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.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/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.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/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/uautomizer.2017-12-02_0106.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   13000 8000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 7300 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 6100 error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   12000 7800 error (invalid witness file) 0 wit inspect .70 46 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 .0016 .26 - wit inspect - wit inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6500 error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 8800 error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .30 - wit inspect - wit inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 6900 error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .046 5.0 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7400 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.2  52 error (invalid witness file) 0 wit inspect .0020 .29 - wit inspect - wit inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 6600 error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0012 .35 - wit inspect - wit inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6000 error (invalid witness file) 0 wit inspect .73 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .76 50 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 7000 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .87 48 error (invalid witness file) 0 wit inspect .0017 .30 - wit inspect - wit inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7200 error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .98 49 error (invalid witness file) 0 wit inspect .0011 .36 - wit inspect - wit inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6500 error (invalid witness file) 0 wit inspect .72 47 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 7000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5900 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 5200 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .89 47 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 6200 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7800 error (invalid witness file) 0 wit inspect .55 43 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 .0017 .30 - wit inspect - wit inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 5200 error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .049 4.8 error (invalid witness file) 0 wit inspect .77 49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7700 error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .73 50 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   14000 6600 error (invalid witness file) 0 wit inspect .70 46 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0020 .30 - wit inspect - wit inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7100 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5200 error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0019 .30 - wit inspect - wit inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 6300 error (invalid witness file) 0 wit inspect .54 46 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.1  48 error (invalid witness file) 0 wit inspect .0018 .30 - wit inspect - wit inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 5900 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0021 .29 - wit inspect - wit inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6500 error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .90 47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 6400 error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6900 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 6100 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect 1.3  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 5700 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .045 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 5600 error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 5600 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .97 49 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 7200 error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .91 48 error (invalid witness file) 0 wit inspect .0014 .32 - wit inspect - wit inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6600 error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 4900 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5000 error (invalid witness file) 0 wit inspect .61 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 .0017 .30 - wit inspect - wit inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0019 .29 - wit inspect - wit inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5600 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5200 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .89 50 error (invalid witness file) 0 wit inspect .0017 .30 - wit inspect - wit inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   14000 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .023 4.9
elevator_spec13_product22_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   14000 5700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 5.0
elevator_spec13_product23_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   14000 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .020 4.9
elevator_spec13_product24_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   14000 6300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .024 4.8
elevator_spec13_product29_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   13000 5800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.9
elevator_spec13_product30_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   14000 5700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
elevator_spec13_product31_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   13000 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .023 4.8
elevator_spec13_product32_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   14000 6100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .022 4.9
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   11000 7800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .034 5.0
elevator_spec14_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7300 - 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_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.8
elevator_spec14_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .022 4.8
elevator_spec14_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 8000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .017 4.8
elevator_spec14_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.8
elevator_spec14_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 46 error (2) 0 wit inspect .019 5.0
elevator_spec1_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 8300 - 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
elevator_spec1_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.9
elevator_spec1_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   12000 7800 - 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_spec1_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .019 4.9
elevator_spec1_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   11000 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .019 4.9
elevator_spec1_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 8000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9
elevator_spec1_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 46 error (2) 0 wit inspect .020 4.9
elevator_spec1_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.8
elevator_spec1_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .021 4.9
elevator_spec1_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   12000 7800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .021 4.8
elevator_spec1_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .018 4.9
elevator_spec1_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 6900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .019 4.9
elevator_spec2_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 5100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .021 5.0
elevator_spec2_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 5900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8
elevator_spec2_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 4700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .024 4.9
elevator_spec2_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.9
elevator_spec2_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 5200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9
elevator_spec2_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   12000 6300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.8
elevator_spec2_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .021 4.9
elevator_spec2_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .020 4.9
elevator_spec2_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.9
elevator_spec2_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .019 4.8
elevator_spec2_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 5100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .025 4.8
elevator_spec2_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.9
elevator_spec3_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 4.9
elevator_spec3_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 4800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .023 5.0
elevator_spec3_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.8
elevator_spec3_product18_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 5900 - 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_spec3_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 4800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .020 4.8
elevator_spec3_product22_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 4.8
elevator_spec3_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .018 4.8
elevator_spec3_product26_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.8
elevator_spec3_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .022 5.0
elevator_spec3_product30_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .051 4.8
elevator_spec9_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 5400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .020 4.9
elevator_spec9_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.8
elevator_spec9_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .021 5.0
elevator_spec9_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .019 4.9
elevator_spec9_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 6500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .026 4.8
elevator_spec9_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 4.9
email_spec0_product16_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   10000 7300 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 6900 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  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 6100 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7300 error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 6800 error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect - wit inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 6500 error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 6700 error (invalid witness file) 0 wit inspect .67 45 error (2) 0 wit inspect .029 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7300 error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 5000 error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 7300 error (invalid witness file) 0 wit inspect .77 44 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .97 49 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 6800 error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 7400 error (invalid witness file) 0 wit inspect .71 46 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .93 47 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 8200 error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 8100 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0018 .27 - wit inspect - wit inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   14000 6500 error (invalid witness file) 0 wit inspect .44 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .96 47 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect - wit inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 6200 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 7100 error (invalid witness file) 0 wit inspect .46 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .91 50 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 6800 error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0017 .32 - wit inspect - wit inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 5600 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .020 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_product15_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   12000 8000 error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 9400 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .70 49 error (invalid witness file) 0 wit inspect .0019 .29 - wit inspect - wit inspect
email_spec1_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 7400 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
email_spec1_product21_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 7800 error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .82 50 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 8400 error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0021 .28 - wit inspect - wit inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 7300 error (invalid witness file) 0 wit inspect .76 44 error (2) 0 wit inspect .045 4.8 error (invalid witness file) 0 wit inspect .99 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 7000 error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .92 47 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
email_spec1_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 7800 error (invalid witness file) 0 wit inspect .53 41 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 .0017 .26 - wit inspect - wit inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 6900 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .94 47 error (invalid witness file) 0 wit inspect .0019 .29 - wit inspect - wit inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   11000 7400 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
email_spec1_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 5700 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect - wit inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 7800 error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
email_spec1_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   14000 5800 error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.2  49 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6100 error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0018 .30 - wit inspect - wit inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 5700 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .82 50 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   13000 8800 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 8300 error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .97 47 error (invalid witness file) 0 wit inspect .0013 .35 - wit inspect - wit inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 8500 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 8100 error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
email_spec27_product25_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 4900 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0016 .34 - wit inspect - wit inspect
email_spec27_product27_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   13000 6000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .97 48 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
email_spec27_product29_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   12000 8200 error (invalid witness file) 0 wit inspect .65 46 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .97 47 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
email_spec27_product30_false-unreach-call_true-termination.cil.c timeout 0 wit