Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon073; apollon077; apollon078; apollon119; apollon130] apollon* [apollon077; apollon078; apollon091; apollon114] 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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-01 12:59:33 CET 2017-12-02 09:20:19 CET 2017-12-02 10:53:45 CET 2017-12-02 11:06:16 CET 2017-12-02 11:21:21 CET 2017-12-02 06:57:43 CET 2017-12-02 09:56:59 CET
Run set esbmc-kind.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.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 .17  39 2.0  false(unreach-call) 1 wit inspect 4.0 290 true -32 wit inspect 11   370 unknown 0 wit inspect 4.4 270 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .20  39 2.2  false(unreach-call) 1 wit inspect 5.5 300 true -32 wit inspect 9.4 380 unknown 0 wit inspect 3.1 220 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .19  39 1.9  false(unreach-call) 1 wit inspect 5.6 280 true -32 wit inspect 8.2 370 unknown 0 wit inspect 4.5 270 false(unreach-call) 1 wit inspect .85 18 - wit inspect - wit inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .18  39 1.9  false(unreach-call) 1 wit inspect 5.6 300 true -32 wit inspect 8.2 380 unknown 0 wit inspect 3.2 270 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.1   200 63    true -32 wit inspect 5.9 270 true -32 wit inspect 6.2 420 unknown 0 wit inspect 7.6 330 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.4   61 16    false(unreach-call) 1 wit inspect 5.7 280 true -32 wit inspect 5.8 370 unknown 0 wit inspect 3.2 270 false(unreach-call) 1 wit inspect .87 18 - wit inspect - wit inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.5   63 18    false(unreach-call) 1 wit inspect 5.7 290 true -32 wit inspect 8.9 380 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .89 18 - wit inspect - wit inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.9   76 21    false(unreach-call) 1 wit inspect 3.9 300 true -32 wit inspect 8.5 380 unknown 0 wit inspect 4.7 270 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.0   79 27    false(unreach-call) 1 wit inspect 4.0 300 true -32 wit inspect 8.1 390 unknown 0 wit inspect 4.7 270 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.6   65 18    false(unreach-call) 1 wit inspect 3.8 280 true -32 wit inspect 9.1 370 unknown 0 wit inspect 4.6 270 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.6   68 21    false(unreach-call) 1 wit inspect 3.9 290 true -32 wit inspect 8.8 380 unknown 0 wit inspect 4.4 220 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.0   80 24    false(unreach-call) 1 wit inspect 3.9 300 true -32 wit inspect 8.5 380 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .88 18 - wit inspect - wit inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.3   84 28    false(unreach-call) 1 wit inspect 7.4 300 true -32 wit inspect 5.9 390 unknown 0 wit inspect 3.3 270 false(unreach-call) 1 wit inspect .90 18 - wit inspect - wit inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 20     300 220    true -32 wit inspect 5.8 270 true -32 wit inspect 11   420 unknown 0 wit inspect 9.0 470 false(unreach-call) 1 wit inspect .92 19 - wit inspect - wit inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.7   68 24    false(unreach-call) 1 wit inspect 7.5 280 true -32 wit inspect 8.4 370 unknown 0 wit inspect 3.2 270 false(unreach-call) 1 wit inspect .87 18 - wit inspect - wit inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.8   70 21    false(unreach-call) 1 wit inspect 3.8 280 true -32 wit inspect 8.2 370 unknown 0 wit inspect 4.6 270 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.2   83 28    false(unreach-call) 1 wit inspect 4.7 290 true -32 wit inspect 8.3 370 unknown 0 wit inspect 4.8 270 false(unreach-call) 1 wit inspect .88 18 - wit inspect - wit inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.4   85 28    false(unreach-call) 1 wit inspect 3.9 300 true -32 wit inspect 9.0 380 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .90 19 - wit inspect - wit inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.8   71 22    false(unreach-call) 1 wit inspect 5.9 290 true -32 wit inspect 5.6 370 unknown 0 wit inspect 4.5 270 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.9   74 22    false(unreach-call) 1 wit inspect 4.3 290 true -32 wit inspect 5.5 380 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.2   86 35    false(unreach-call) 1 wit inspect 5.8 300 true -32 wit inspect 8.1 370 unknown 0 wit inspect 3.2 270 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.5   91 28    false(unreach-call) 1 wit inspect 4.0 300 true -32 wit inspect 5.6 380 unknown 0 wit inspect 3.3 270 false(unreach-call) 1 wit inspect .88 19 - wit inspect - wit inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 20     300 210    true -32 wit inspect 6.1 270 true -32 wit inspect 7.2 420 unknown 0 wit inspect 8.8 450 false(unreach-call) 1 wit inspect .91 19 - wit inspect - wit inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .17  39 1.9  false(unreach-call) 1 wit inspect 7.9 290 true -32 wit inspect 8.6 380 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .20  39 2.1  false(unreach-call) 1 wit inspect 7.5 300 true -32 wit inspect 9.3 380 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .17  39 1.9  false(unreach-call) 1 wit inspect 4.2 300 true -32 wit inspect 9.0 370 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .20  39 1.9  false(unreach-call) 1 wit inspect 4.1 300 true -32 wit inspect 8.7 370 unknown 0 wit inspect 4.5 270 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .23  39 2.1  false(unreach-call) 1 wit inspect 7.5 310 true -32 wit inspect 8.1 380 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .19  40 2.7  false(unreach-call) 1 wit inspect 6.5 320 true -32 wit inspect 8.4 380 unknown 0 wit inspect 4.9 290 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .21  39 1.8  false(unreach-call) 1 wit inspect 6.6 290 true -32 wit inspect 8.4 380 unknown 0 wit inspect 3.2 270 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .23  40 1.6  false(unreach-call) 1 wit inspect 4.1 290 true -32 wit inspect 8.6 380 unknown 0 wit inspect 4.7 270 false(unreach-call) 1 wit inspect .85 18 - wit inspect - wit inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .18  40 2.0  false(unreach-call) 1 wit inspect 6.6 310 true -32 wit inspect 6.0 390 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .22  40 2.1  false(unreach-call) 1 wit inspect 4.2 320 true -32 wit inspect 5.7 390 unknown 0 wit inspect 3.2 270 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12     330 160    true -32 wit inspect 3.3 270 true -32 wit inspect 9.6 430 unknown 0 wit inspect 6.2 430 false(unreach-call) 1 wit inspect .90 19 - wit inspect - wit inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.8   71 22    false(unreach-call) 1 wit inspect 3.8 280 true -32 wit inspect 8.3 360 unknown 0 wit inspect 3.2 270 false(unreach-call) 1 wit inspect .84 18 - wit inspect - wit inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.8   77 26    false(unreach-call) 1 wit inspect 7.0 290 true -32 wit inspect 8.1 370 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .88 18 - wit inspect - wit inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.3   88 27    false(unreach-call) 1 wit inspect 6.0 300 true -32 wit inspect 8.4 370 unknown 0 wit inspect 4.6 270 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.3   91 26    false(unreach-call) 1 wit inspect 8.0 300 true -32 wit inspect 6.8 390 unknown 0 wit inspect 4.6 270 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 20     290 250    true -32 wit inspect 3.2 270 true -32 wit inspect 10   420 unknown 0 wit inspect 6.1 470 false(unreach-call) 1 wit inspect .88 19 - wit inspect - wit inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     1500 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .028 4.8
elevator_spec13_product22_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     1400 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .018 4.9
elevator_spec13_product23_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     1900 11000    - 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_spec13_product24_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     1900 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .024 4.8
elevator_spec13_product29_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     1500 14000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .023 4.9
elevator_spec13_product30_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     1500 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .019 4.9
elevator_spec13_product31_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     2000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .019 4.9
elevator_spec13_product32_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     1900 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .020 4.9
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     3700 7000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 5.0
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.6   51 21    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    650 out of memory 0 wit inspect 290     7000  
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.7   54 23    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    680 out of memory 0 wit inspect 220     7000  
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.8   52 23    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    710 out of memory 0 wit inspect 280     7000  
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.3   61 34    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    990 out of memory 0 wit inspect 220     7000  
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.9   54 23    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    720 out of memory 0 wit inspect 260     7000  
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.4   64 35    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    1100 out of memory 0 wit inspect 190     7000  
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.2   46 14    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 74    1400 out of memory 0 wit inspect 310     7000  
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.4   48 19    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 76    1500 out of memory 0 wit inspect 280     7000  
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.3   50 16    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 80    1500 out of memory 0 wit inspect 320     7000  
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.5   51 20    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 81    1700 out of memory 0 wit inspect 190     7000  
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.2   46 13    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 75    1500 out of memory 0 wit inspect 310     7000  
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.3   49 15    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 82    1600 out of memory 0 wit inspect 220     7000  
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.7   56 21    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 150    1800 out of memory 0 wit inspect 220     7000  
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.9   58 27    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 120    2100 out of memory 0 wit inspect 210     7000  
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.4   50 18    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 82    1600 out of memory 0 wit inspect 190     7000  
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.5   52 16    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 100    1800 out of memory 0 wit inspect 290     7000  
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.7   60 21    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 170    1900 out of memory 0 wit inspect 170     7000  
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.0   61 26    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140    2000 out of memory 0 wit inspect 230     7000  
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.2   52 13    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 29    750 out of memory 0 wit inspect 130     7000  
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.3   54 14    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    880 out of memory 0 wit inspect 170     7000  
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.3   56 16    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    900 out of memory 0 wit inspect 130     7000  
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.4   56 15    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 38    950 out of memory 0 wit inspect 150     7000  
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.2   53 15    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 29    900 out of memory 0 wit inspect 150     7000  
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.3   55 17    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 36    970 out of memory 0 wit inspect 110     7000  
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.6   59 18    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 45    1100 out of memory 0 wit inspect 100     7000  
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.7   61 19    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 44    1200 out of memory 0 wit inspect 220     7000  
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.4   56 15    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 32    940 out of memory 0 wit inspect 150     7000  
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.5   58 18    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 37    1100 out of memory 0 wit inspect 160     7000  
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.7   62 20    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 44    1200 out of memory 0 wit inspect 160     7000  
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.8   64 21    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 49    1300 out of memory 0 wit inspect 120     7000  
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .81  45 10    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    670 out of memory 0 wit inspect 200     7000  
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .90  49 9.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    700 out of memory 0 wit inspect 120     7000  
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .87  47 11    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    720 out of memory 0 wit inspect 220     7000  
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.4   60 17    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    880 out of memory 0 wit inspect 150     7000  
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.2   55 13    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    870 out of memory 0 wit inspect 130     7000  
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.0   75 24    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    1600 out of memory 0 wit inspect 240     7000  
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .93  50 9.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    700 out of memory 0 wit inspect 150     7000  
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.6   65 20    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    890 out of memory 0 wit inspect 270     7000  
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.4   58 16    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    960 out of memory 0 wit inspect 160     7000  
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.2   79 29    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28    1600 out of memory 0 wit inspect 200     7000  
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.3   55 16    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 40    910 out of memory 0 wit inspect 180     7000  
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.5   56 17    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 33    960 out of memory 0 wit inspect 180     7000  
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.3   55 16    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    940 out of memory 0 wit inspect 170     7000  
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.5   57 19    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 34    1100 out of memory 0 wit inspect 130     7000  
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.7   64 19    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 42    1200 out of memory 0 wit inspect 150     7000  
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.8   65 22    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 36    1200 out of memory 0 wit inspect 150     7000  
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.8   41 27    false(unreach-call) 1 wit inspect 6.9 290 true -32 wit inspect 7.9 340 unknown 0 wit inspect 4.1 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.3   52 43    false(unreach-call) 1 wit inspect 6.2 290 true -32 wit inspect 8.3 360 unknown 0 wit inspect 4.2 290 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.2   43 34    false(unreach-call) 1 wit inspect 6.3 290 true -32 wit inspect 8.2 340 unknown 0 wit inspect 4.1 290 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.6   54 46    false(unreach-call) 1 wit inspect 4.2 290 true -32 wit inspect 8.4 390 unknown 0 wit inspect 6.2 310 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0   43 30    false(unreach-call) 1 wit inspect 8.2 300 true -32 wit inspect 7.7 360 unknown 0 wit inspect 4.0 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.5   45 37    false(unreach-call) 1 wit inspect 8.0 310 true -32 wit inspect 8.0 360 unknown 0 wit inspect 4.1 280 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.3   57 59    timeout 0 wit inspect 92   1500 true -32 wit inspect 5.7 380 unknown 0 wit inspect 6.0 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.2   59 54    timeout 0 wit inspect 92   1900 true -32 wit inspect 5.7 410 unknown 0 wit inspect 4.4 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 65     470 730    true -32 wit inspect 4.8 270 true -32 wit inspect 9.6 440 unknown 0 wit inspect 4.7 330 false(unreach-call) 1 wit inspect .93 18 - wit inspect - wit inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.5   40 31    false(unreach-call) 1 wit inspect 5.1 290 true -32 wit inspect 8.0 330 unknown 0 wit inspect 5.6 280 false(unreach-call) 1 wit inspect .83 19 - wit inspect - wit inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.4   51 35    false(unreach-call) 1 wit inspect 3.8 280 true -32 wit inspect 5.7 350 unknown 0 wit inspect 5.4 280 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0   43 30    false(unreach-call) 1 wit inspect 5.8 280 true -32 wit inspect 8.3 340 unknown 0 wit inspect 4.0 290 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.3   54 62    false(unreach-call) 1 wit inspect 7.4 290 true -32 wit inspect 8.2 380 unknown 0 wit inspect 3.8 290 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.8   43 24    false(unreach-call) 1 wit inspect 4.6 300 true -32 wit inspect 5.3 340 unknown 0 wit inspect 5.9 280 false(unreach-call) 1 wit inspect .88 19 - wit inspect - wit inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.7   55 42    false(unreach-call) 1 wit inspect 8.1 290 true -32 wit inspect 8.4 400 unknown 0 wit inspect 5.6 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0   45 33    false(unreach-call) 1 wit inspect 8.7 300 true -32 wit inspect 5.5 370 unknown 0 wit inspect 5.6 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.0   59 67    timeout 0 wit inspect 91   1400 true -32 wit inspect 8.3 390 unknown 0 wit inspect 4.1 290 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 75     520 830    true -32 wit inspect 4.5 260 true -32 wit inspect 9.1 450 unknown 0 wit inspect 5.9 290 false(unreach-call) 1 wit inspect .90 19 - wit inspect - wit inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.6   42 35    true -32 wit inspect 6.1 400 true -32 wit inspect 7.8 340 unknown 0 wit inspect 4.1 290 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.5   40 29    true -32 wit inspect 6.1 380 true -32 wit inspect 7.8 330 unknown 0 wit inspect 4.1 310 false(unreach-call) 1 wit inspect .83 19 - wit inspect - wit inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.6   41 34    true -32 wit inspect 4.6 270 true -32 wit inspect 8.3 340 unknown 0 wit inspect 6.1 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.6   49 42    true -32 wit inspect 6.9 410 true -32 wit inspect 5.9 380 unknown 0 wit inspect 4.8 320 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec1_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.6   52 44    true -32 wit inspect 11   400 true -32 wit inspect 6.0 380 unknown 0 wit inspect 4.4 320 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.9   43 36    true -32 wit inspect 4.6 280 true -32 wit inspect 5.3 350 unknown 0 wit inspect 6.1 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.4   54 55    true -32 wit inspect 12   410 true -32 wit inspect 5.8 390 unknown 0 wit inspect 6.9 290 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1   45 44    true -32 wit inspect 15   440 true -32 wit inspect 5.6 370 unknown 0 wit inspect 4.3 310 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.5   43 33    true -32 wit inspect 13   410 true -32 wit inspect 7.9 340 unknown 0 wit inspect 6.6 280 false(unreach-call) 1 wit inspect .91 19 - wit inspect - wit inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.6   43 36    true -32 wit inspect 15   440 true -32 wit inspect 8.4 360 unknown 0 wit inspect 4.4 320 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.0   55 51    true -32 wit inspect 15   460 true -32 wit inspect 8.2 360 unknown 0 wit inspect 7.1 310 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.0   45 37    true -32 wit inspect 16   440 true -32 wit inspect 8.5 370 unknown 0 wit inspect 6.6 310 false(unreach-call) 1 wit inspect .90 19 - wit inspect - wit inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.9   55 48    true -32 wit inspect 17   590 true -32 wit inspect 8.8 370 unknown 0 wit inspect 4.5 320 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec1_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.0   59 57    true -32 wit inspect 11   510 true -32 wit inspect 6.5 410 unknown 0 wit inspect 4.9 320 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 28     210 300    true -32 wit inspect 4.9 260 true -32 wit inspect 10   470 unknown 0 wit inspect 6.8 280 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.2   43 45    false(unreach-call) 1 wit inspect 8.9 300 true -32 wit inspect 7.9 350 unknown 0 wit inspect 6.6 290 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.0   41 45    false(unreach-call) 1 wit inspect 7.2 300 true -32 wit inspect 7.6 330 unknown 0 wit inspect 6.3 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.3   41 38    true -32 wit inspect 12   440 true -32 wit inspect 5.3 340 unknown 0 wit inspect 5.4 380 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.3   51 49    false(unreach-call) 1 wit inspect 8.5 300 true -32 wit inspect 7.9 360 unknown 0 wit inspect 4.5 290 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.6   44 42    true -32 wit inspect 14   460 true -32 wit inspect 7.9 340 unknown 0 wit inspect 5.4 420 false(unreach-call) 1