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* [apollon010; apollon035; apollon045; apollon077; apollon078; apollon138] [apollon007; apollon077; apollon078; apollon143] 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-01 08:49:27 CET 2017-12-01 22:53:44 CET 2017-12-01 23:38:04 CET 2017-12-01 23:47:42 CET 2017-12-01 23:55:24 CET 2017-12-01 22:20:30 CET 2017-12-01 23:01:53 CET
Run set esbmc-incr.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-incr.2017-12-01_0849.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 .20 38 1.9 false(unreach-call) 1 wit inspect 6.2 290 true -32 wit inspect 8.5 370 unknown 0 wit inspect 3.0 220 false(unreach-call) 1 wit inspect .84 18 - wit inspect - wit inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .17 39 1.6 false(unreach-call) 1 wit inspect 5.5 300 true -32 wit inspect 8.9 380 unknown 0 wit inspect 3.2 270 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .19 39 1.7 false(unreach-call) 1 wit inspect 5.7 280 true -32 wit inspect 8.2 370 unknown 0 wit inspect 4.2 220 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .16 39 1.9 false(unreach-call) 1 wit inspect 6.4 300 true -32 wit inspect 8.6 370 unknown 0 wit inspect 4.6 270 false(unreach-call) 1 wit inspect .87 18 - wit inspect - wit inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.7  160 49   true -32 wit inspect 5.6 270 true -32 wit inspect 8.5 400 unknown 0 wit inspect 7.4 330 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .23 39 2.4 false(unreach-call) 1 wit inspect 5.8 280 true -32 wit inspect 7.7 360 unknown 0 wit inspect 4.6 270 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .22 39 2.4 false(unreach-call) 1 wit inspect 5.8 290 true -32 wit inspect 8.4 380 unknown 0 wit inspect 4.7 270 false(unreach-call) 1 wit inspect .88 19 - wit inspect - wit inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .22 39 2.1 false(unreach-call) 1 wit inspect 6.0 300 true -32 wit inspect 8.2 370 unknown 0 wit inspect 3.2 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 .23 39 2.2 false(unreach-call) 1 wit inspect 6.1 300 true -32 wit inspect 8.2 370 unknown 0 wit inspect 4.7 270 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .20 39 2.2 false(unreach-call) 1 wit inspect 6.1 290 true -32 wit inspect 6.1 370 unknown 0 wit inspect 4.5 260 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .23 39 2.2 false(unreach-call) 1 wit inspect 6.0 290 true -32 wit inspect 8.4 370 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24 40 2.3 false(unreach-call) 1 wit inspect 6.1 300 true -32 wit inspect 8.7 380 unknown 0 wit inspect 4.8 270 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .22 40 3.2 false(unreach-call) 1 wit inspect 6.1 300 true -32 wit inspect 9.2 380 unknown 0 wit inspect 4.8 270 false(unreach-call) 1 wit inspect .87 18 - wit inspect - wit inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.3  190 110   true -32 wit inspect 5.9 270 true -32 wit inspect 8.6 420 unknown 0 wit inspect 6.0 470 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .23 39 2.1 false(unreach-call) 1 wit inspect 5.8 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 .20 39 2.4 false(unreach-call) 1 wit inspect 6.4 290 true -32 wit inspect 8.1 370 unknown 0 wit inspect 4.8 270 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .23 39 2.2 false(unreach-call) 1 wit inspect 6.5 300 true -32 wit inspect 8.2 380 unknown 0 wit inspect 4.6 240 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .21 40 2.2 false(unreach-call) 1 wit inspect 5.8 300 true -32 wit inspect 8.1 380 unknown 0 wit inspect 4.7 270 false(unreach-call) 1 wit inspect .85 18 - wit inspect - wit inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .19 39 2.5 false(unreach-call) 1 wit inspect 6.2 290 true -32 wit inspect 8.4 370 unknown 0 wit inspect 3.2 270 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .23 39 2.2 false(unreach-call) 1 wit inspect 6.2 290 true -32 wit inspect 9.5 380 unknown 0 wit inspect 3.0 220 false(unreach-call) 1 wit inspect .84 18 - wit inspect - wit inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .21 40 2.3 false(unreach-call) 1 wit inspect 5.8 300 true -32 wit inspect 8.5 370 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24 40 2.3 false(unreach-call) 1 wit inspect 6.0 300 true -32 wit inspect 6.0 380 unknown 0 wit inspect 4.8 270 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.4  190 84   true -32 wit inspect 5.7 260 true -32 wit inspect 6.4 440 unknown 0 wit inspect 8.8 440 false(unreach-call) 1 wit inspect .90 19 - wit inspect - wit inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .20 39 1.9 false(unreach-call) 1 wit inspect 5.8 290 true -32 wit inspect 8.3 370 unknown 0 wit inspect 4.6 270 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .17 39 2.0 false(unreach-call) 1 wit inspect 6.5 300 true -32 wit inspect 5.8 380 unknown 0 wit inspect 4.5 270 false(unreach-call) 1 wit inspect .88 19 - wit inspect - wit inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .21 39 2.0 false(unreach-call) 1 wit inspect 6.6 300 true -32 wit inspect 9.9 380 unknown 0 wit inspect 4.5 270 false(unreach-call) 1 wit inspect .88 19 - wit inspect - wit inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .18 39 2.2 false(unreach-call) 1 wit inspect 6.3 300 true -32 wit inspect 9.2 380 unknown 0 wit inspect 4.7 270 false(unreach-call) 1 wit inspect .85 18 - wit inspect - wit inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .19 40 2.0 false(unreach-call) 1 wit inspect 6.1 310 true -32 wit inspect 8.2 380 unknown 0 wit inspect 3.2 260 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .18 40 2.0 false(unreach-call) 1 wit inspect 6.5 320 true -32 wit inspect 8.6 390 unknown 0 wit inspect 3.2 270 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .21 39 2.0 false(unreach-call) 1 wit inspect 7.2 300 true -32 wit inspect 8.4 390 unknown 0 wit inspect 4.5 270 false(unreach-call) 1 wit inspect .89 18 - wit inspect - wit inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .20 39 1.8 false(unreach-call) 1 wit inspect 6.1 300 true -32 wit inspect 5.6 380 unknown 0 wit inspect 4.6 270 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .18 40 2.1 false(unreach-call) 1 wit inspect 6.8 320 true -32 wit inspect 5.9 390 unknown 0 wit inspect 4.7 270 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .19 40 2.1 false(unreach-call) 1 wit inspect 7.6 320 true -32 wit inspect 6.0 400 unknown 0 wit inspect 4.4 260 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11    260 100   true -32 wit inspect 5.1 270 true -32 wit inspect 9.1 420 unknown 0 wit inspect 6.2 430 false(unreach-call) 1 wit inspect .91 19 - wit inspect - wit inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .23 39 2.2 false(unreach-call) 1 wit inspect 6.1 290 true -32 wit inspect 8.6 380 unknown 0 wit inspect 3.0 220 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .22 39 2.3 false(unreach-call) 1 wit inspect 5.9 290 true -32 wit inspect 8.1 370 unknown 0 wit inspect 3.1 270 false(unreach-call) 1 wit inspect .84 18 - wit inspect - wit inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .22 39 2.6 false(unreach-call) 1 wit inspect 6.5 300 true -32 wit inspect 8.2 370 unknown 0 wit inspect 4.7 270 false(unreach-call) 1 wit inspect .88 19 - wit inspect - wit inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .20 40 3.1 false(unreach-call) 1 wit inspect 7.5 300 true -32 wit inspect 8.1 380 unknown 0 wit inspect 4.8 270 false(unreach-call) 1 wit inspect .90 19 - wit inspect - wit inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.8  190 80   true -32 wit inspect 5.0 270 true -32 wit inspect 6.1 400 unknown 0 wit inspect 11   470 false(unreach-call) 1 wit inspect .91 19 - wit inspect - wit inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    1500 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 5.0
elevator_spec13_product22_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    1400 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .021 4.8
elevator_spec13_product23_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 .65 43 error (2) 0 wit inspect .018 4.9
elevator_spec13_product24_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    1900 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 44 error (2) 0 wit inspect .018 4.9
elevator_spec13_product29_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 44 error (2) 0 wit inspect .018 4.8
elevator_spec13_product30_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    1400 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 5.0
elevator_spec13_product31_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 .65 43 error (2) 0 wit inspect .024 4.8
elevator_spec13_product32_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    2000 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 42 error (2) 0 wit inspect .019 4.9
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    3300 9400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .018 4.9
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .64 36 8.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    660 out of memory 0 wit inspect 340     7000  
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .67 37 8.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    690 out of memory 0 wit inspect 290     7000  
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .75 37 8.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    730 out of memory 0 wit inspect 270     7000  
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.1  37 15   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    1000 out of memory 0 wit inspect 320     7000  
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .76 37 9.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 18    710 out of memory 0 wit inspect 270     7000  
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.1  37 12   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 29    1000 out of memory 0 wit inspect 230     7000  
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .54 37 6.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 68    1400 out of memory 0 wit inspect 230     7000  
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .62 37 8.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 78    1500 out of memory 0 wit inspect 220     7000  
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .54 37 6.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 77    1500 out of memory 0 wit inspect 290     7000  
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .60 37 6.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 87    1600 out of memory 0 wit inspect 280     7000  
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .51 37 6.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 83    1500 out of memory 0 wit inspect 240     7000  
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .54 37 6.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 99    1700 out of memory 0 wit inspect 290     7000  
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .61 37 7.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 150    1900 out of memory 0 wit inspect 230     7000  
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .70 38 9.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 110    2100 out of memory 0 wit inspect 250     7000  
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .54 37 6.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 71    1700 out of memory 0 wit inspect 250     7000  
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .60 38 7.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 94    1800 out of memory 0 wit inspect 200     7000  
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .54 38 5.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 190    2000 out of memory 0 wit inspect 170     7000  
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .74 38 11   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140    2100 out of memory 0 wit inspect 240     7000  
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .29 37 3.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    860 out of memory 0 wit inspect 190     7000  
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .30 37 3.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 35    910 out of memory 0 wit inspect 170     7000  
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 37 3.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 34    900 out of memory 0 wit inspect 140     7000  
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 37 3.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 38    990 out of memory 0 wit inspect 160     7000  
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .30 37 3.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 32    930 out of memory 0 wit inspect 130     7000  
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .32 37 3.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 38    1000 out of memory 0 wit inspect 160     7000  
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 37 3.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 57    1100 out of memory 0 wit inspect 130     7000  
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .32 38 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 42    1200 out of memory 0 wit inspect 210     7000  
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .29 37 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 40    960 out of memory 0 wit inspect 150     7000  
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .34 37 3.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 29    1100 out of memory 0 wit inspect 190     7000  
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 38 3.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 47    1200 out of memory 0 wit inspect 140     7000  
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 38 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 56    1300 out of memory 0 wit inspect 110     7000  
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .97 37 11   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    670 out of memory 0 wit inspect 230     7000  
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .89 37 12   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 22    690 out of memory 0 wit inspect 150     7000  
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .97 37 11   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 22    690 out of memory 0 wit inspect 220     7000  
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.1  37 13   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24    830 out of memory 0 wit inspect 180     7000  
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.1  38 15   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    890 out of memory 0 wit inspect 150     7000  
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.3  38 14   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 34    1600 out of memory 0 wit inspect 190     7000  
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.0  37 13   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    700 out of memory 0 wit inspect 170     7000  
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.1  38 13   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    930 out of memory 0 wit inspect 190     7000  
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.1  38 14   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24    930 out of memory 0 wit inspect 110     7000  
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.2  38 19   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    1700 out of memory 0 wit inspect 230     7000  
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .29 37 2.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 32    900 out of memory 0 wit inspect 150     7000  
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 37 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 36    910 out of memory 0 wit inspect 100     7000  
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 37 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 33    920 out of memory 0 wit inspect 110     7000  
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 37 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 39    1000 out of memory 0 wit inspect 130     7000  
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .29 38 3.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 43    1200 out of memory 0 wit inspect 150     7000  
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 38 3.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 42    1300 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.7  41 24   false(unreach-call) 1 wit inspect 6.3 280 true -32 wit inspect 5.2 340 unknown 0 wit inspect 5.3 270 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.8  50 44   false(unreach-call) 1 wit inspect 6.9 300 true -32 wit inspect 5.7 360 unknown 0 wit inspect 5.9 280 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.6  43 28   false(unreach-call) 1 wit inspect 6.2 290 true -32 wit inspect 7.7 340 unknown 0 wit inspect 5.1 270 false(unreach-call) 1 wit inspect .84 18 - wit inspect - wit inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.0  54 46   false(unreach-call) 1 wit inspect 7.0 300 true -32 wit inspect 8.8 370 unknown 0 wit inspect 6.1 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.7  43 29   false(unreach-call) 1 wit inspect 7.9 300 true -32 wit inspect 8.1 360 unknown 0 wit inspect 3.8 280 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.8  45 29   false(unreach-call) 1 wit inspect 6.2 290 true -32 wit inspect 5.9 350 unknown 0 wit inspect 5.3 280 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.1  56 45   timeout 0 wit inspect 92   1700 true -32 wit inspect 6.0 380 unknown 0 wit inspect 5.7 280 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.8  58 49   timeout 0 wit inspect 92   1700 true -32 wit inspect 8.5 400 unknown 0 wit inspect 5.9 280 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 48    440 560   true -32 wit inspect 4.9 270 true -32 wit inspect 9.5 450 unknown 0 wit inspect 4.5 320 false(unreach-call) 1 wit inspect .91 19 - wit inspect - wit inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.4  41 23   false(unreach-call) 1 wit inspect 5.8 280 true -32 wit inspect 7.6 330 unknown 0 wit inspect 3.7 270 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.0  49 45   false(unreach-call) 1 wit inspect 6.8 290 true -32 wit inspect 5.3 360 unknown 0 wit inspect 5.9 280 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.6  43 28   false(unreach-call) 1 wit inspect 6.3 290 true -32 wit inspect 8.3 340 unknown 0 wit inspect 5.5 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.9  53 40   false(unreach-call) 1 wit inspect 7.1 280 true -32 wit inspect 6.5 370 unknown 0 wit inspect 5.6 280 false(unreach-call) 1 wit inspect .88 19 - wit inspect - wit inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.6  43 24   false(unreach-call) 1 wit inspect 4.5 300 true -32 wit inspect 5.4 340 unknown 0 wit inspect 3.7 280 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.6  54 46   false(unreach-call) 1 wit inspect 6.9 310 true -32 wit inspect 5.6 370 unknown 0 wit inspect 4.2 290 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.8  45 28   false(unreach-call) 1 wit inspect 8.2 300 true -32 wit inspect 7.9 360 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 4.3  58 48   timeout 0 wit inspect 92   1400 true -32 wit inspect 8.3 380 unknown 0 wit inspect 5.6 280 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 56    490 630   true -32 wit inspect 5.1 260 true -32 wit inspect 9.9 470 unknown 0 wit inspect 6.3 280 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 2.9  39 26   true -32 wit inspect 16   450 true -32 wit inspect 8.0 340 unknown 0 wit inspect 5.9 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 2.6  37 29   true -32 wit inspect 7.6 290 true -32 wit inspect 7.5 330 unknown 0 wit inspect 3.9 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.9  37 27   true -32 wit inspect 8.3 310 true -32 wit inspect 5.5 340 unknown 0 wit inspect 6.2 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 2.9  45 25   true -32 wit inspect 14   410 true -32 wit inspect 8.2 350 unknown 0 wit inspect 4.3 310 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec1_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1  46 32   true -32 wit inspect 14   460 true -32 wit inspect 8.4 360 unknown 0 wit inspect 4.5 320 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0  39 25   true -32 wit inspect 8.0 320 true -32 wit inspect 6.4 340 unknown 0 wit inspect 6.3 310 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.4  48 31   true -32 wit inspect 15   460 true -32 wit inspect 8.5 370 unknown 0 wit inspect 4.5 290 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.8  41 24   true -32 wit inspect 22   610 true -32 wit inspect 9.8 350 unknown 0 wit inspect 6.2 290 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 2.6  39 21   true -32 wit inspect 9.3 410 true -32 wit inspect 5.5 340 unknown 0 wit inspect 6.4 300 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.9  39 25   true -32 wit inspect 23   610 true -32 wit inspect 8.8 380 unknown 0 wit inspect 4.3 280 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.9  48 31   true -32 wit inspect 18   550 true -32 wit inspect 8.4 370 unknown 0 wit inspect 4.4 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 2.9  41 29   true -32 wit inspect 22   620 true -32 wit inspect 8.0 370 unknown 0 wit inspect 6.8 280 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.3  49 33   true -32 wit inspect 57   1900 true -32 wit inspect 9.0 380 unknown 0 wit inspect 4.8 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 3.3  52 39   true -32 wit inspect 55   2100 true -32 wit inspect 11   380 unknown 0 wit inspect 4.9 290 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.8  170 120   true -32 wit inspect 5.7 270 true -32 wit inspect 7.1 450 unknown 0 wit inspect 8.0 330 false(unreach-call) 1 wit inspect .92 19 - wit inspect - wit inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.6  40 31   false(unreach-call) 1 wit inspect 9.1 300 true -32 wit inspect 7.5 350 unknown 0 wit inspect 4.6 320 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0  38 37   false(unreach-call) 1 wit inspect 8.6 290 true -32 wit inspect 7.6 330 unknown 0 wit inspect 4.1 280 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.9  38 32   true -32 wit inspect 26   610 true -32 wit inspect 8.1 340 unknown 0 wit inspect 5.7 420 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.8  46 39   false(unreach-call) 1 wit inspect 8.6 310 true -32 wit inspect 8.2 350 unknown 0 wit inspect 4.5 280 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.7  40 38   true -32 wit inspect 21   630 true -32 wit inspect 9.5 350 unknown 0 wit inspect 5.8 470 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
email_spec27_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit