Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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* [apollon005; apollon043; apollon077; apollon078; apollon087; apollon118] [apollon061; apollon077; apollon078; apollon086; apollon134] [apollon038; apollon077; apollon078; apollon083] [apollon077; apollon078; apollon161] 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 22:41:19 CET 2017-12-02 21:10:50 CET 2017-12-02 22:39:24 CET 2017-12-02 22:51:52 CET 2017-12-02 23:01:21 CET 2017-12-02 19:44:15 CET 2017-12-02 21:36:25 CET
Run set symbiotic.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.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 .38 18 4.6 false(unreach-call) 1 wit inspect 6.5 290 true -32 wit inspect 8.7 370 unknown 0 wit inspect 3.4 220 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 19 3.8 false(unreach-call) 1 wit inspect 7.3 300 true -32 wit inspect 5.5 370 unknown 0 wit inspect 5.2 230 false(unreach-call) 1 wit inspect .89 18 - wit inspect - wit inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 19 4.6 false(unreach-call) 1 wit inspect 4.4 290 true -32 wit inspect 8.0 370 unknown 0 wit inspect 5.0 230 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 19 4.9 false(unreach-call) 1 wit inspect 6.4 300 true -32 wit inspect 9.0 390 unknown 0 wit inspect 5.2 250 false(unreach-call) 1 wit inspect .85 18 - wit inspect - wit inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 23 6.1 false(unreach-call) 1 wit inspect 14   500 true -32 wit inspect 8.7 410 unknown 0 wit inspect 5.4 240 true -32 wit inspect .87 18 - wit inspect - wit inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 18 4.8 false(unreach-call) 1 wit inspect 4.2 290 true -32 wit inspect 5.5 370 unknown 0 wit inspect 3.5 230 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 19 4.6 false(unreach-call) 1 wit inspect 4.3 290 true -32 wit inspect 8.4 380 unknown 0 wit inspect 5.2 240 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 .37 19 4.4 false(unreach-call) 1 wit inspect 4.2 300 true -32 wit inspect 6.0 370 unknown 0 wit inspect 3.5 250 false(unreach-call) 1 wit inspect .85 18 - wit inspect - wit inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 19 5.1 false(unreach-call) 1 wit inspect 6.6 310 true -32 wit inspect 8.6 380 unknown 0 wit inspect 3.4 240 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 19 3.8 false(unreach-call) 1 wit inspect 7.0 290 true -32 wit inspect 8.1 360 unknown 0 wit inspect 5.3 250 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 19 4.9 false(unreach-call) 1 wit inspect 6.9 300 true -32 wit inspect 8.3 370 unknown 0 wit inspect 5.3 240 false(unreach-call) 1 wit inspect .90 19 - wit inspect - wit inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 20 4.6 false(unreach-call) 1 wit inspect 4.4 300 true -32 wit inspect 5.6 370 unknown 0 wit inspect 3.5 240 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 20 4.5 false(unreach-call) 1 wit inspect 7.7 300 true -32 wit inspect 5.6 380 unknown 0 wit inspect 5.3 250 false(unreach-call) 1 wit inspect .90 19 - wit inspect - wit inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 24 6.5 false(unreach-call) 1 wit inspect 45   2100 true -32 wit inspect 9.3 410 unknown 0 wit inspect 3.7 250 true -32 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 18 4.3 false(unreach-call) 1 wit inspect 8.2 290 true -32 wit inspect 7.6 360 unknown 0 wit inspect 5.1 240 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36 19 4.9 false(unreach-call) 1 wit inspect 6.6 290 true -32 wit inspect 6.0 370 unknown 0 wit inspect 5.2 240 false(unreach-call) 1 wit inspect .87 18 - wit inspect - wit inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 19 4.7 false(unreach-call) 1 wit inspect 6.5 300 true -32 wit inspect 5.5 370 unknown 0 wit inspect 5.3 240 false(unreach-call) 1 wit inspect .89 19 - wit inspect - wit inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 20 5.1 false(unreach-call) 1 wit inspect 4.5 310 true -32 wit inspect 6.1 390 unknown 0 wit inspect 3.5 240 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36 19 4.4 false(unreach-call) 1 wit inspect 6.6 290 true -32 wit inspect 8.4 370 unknown 0 wit inspect 5.3 240 false(unreach-call) 1 wit inspect .84 18 - wit inspect - wit inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 19 4.9 false(unreach-call) 1 wit inspect 6.3 290 true -32 wit inspect 6.0 380 unknown 0 wit inspect 3.5 250 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 20 5.3 false(unreach-call) 1 wit inspect 7.5 300 true -32 wit inspect 8.4 370 unknown 0 wit inspect 3.5 250 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 20 4.8 false(unreach-call) 1 wit inspect 7.2 300 true -32 wit inspect 5.6 380 unknown 0 wit inspect 3.5 250 false(unreach-call) 1 wit inspect .87 18 - wit inspect - wit inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .45 24 6.1 false(unreach-call) 1 wit inspect 35   2000 true -32 wit inspect 8.5 410 unknown 0 wit inspect 5.6 240 true -32 wit inspect .90 19 - wit inspect - wit inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 19 4.3 false(unreach-call) 1 wit inspect 8.7 310 true -32 wit inspect 7.7 360 unknown 0 wit inspect 3.4 220 false(unreach-call) 1 wit inspect .88 19 - wit inspect - wit inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 20 4.5 false(unreach-call) 1 wit inspect 7.5 310 true -32 wit inspect 5.5 370 unknown 0 wit inspect 3.4 230 false(unreach-call) 1 wit inspect .85 19 - wit inspect - wit inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 20 4.9 false(unreach-call) 1 wit inspect 7.4 320 true -32 wit inspect 8.4 360 unknown 0 wit inspect 4.9 220 false(unreach-call) 1 wit inspect .84 18 - wit inspect - wit inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 21 4.1 false(unreach-call) 1 wit inspect 7.1 330 true -32 wit inspect 8.2 370 unknown 0 wit inspect 3.6 270 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 21 4.9 false(unreach-call) 1 wit inspect 5.7 350 true -32 wit inspect 8.3 380 unknown 0 wit inspect 3.3 220 false(unreach-call) 1 wit inspect .88 19 - wit inspect - wit inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 22 5.5 false(unreach-call) 1 wit inspect 5.2 360 true -32 wit inspect 5.9 390 unknown 0 wit inspect 3.4 240 false(unreach-call) 1 wit inspect .89 18 - wit inspect - wit inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 21 4.6 false(unreach-call) 1 wit inspect 4.9 320 true -32 wit inspect 8.4 380 unknown 0 wit inspect 4.9 230 false(unreach-call) 1 wit inspect .86 19 - wit inspect - wit inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 22 4.5 false(unreach-call) 1 wit inspect 8.7 340 true -32 wit inspect 8.3 370 unknown 0 wit inspect 3.5 240 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 .39 22 5.6 false(unreach-call) 1 wit inspect 7.5 350 true -32 wit inspect 6.3 390 unknown 0 wit inspect 3.4 220 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 .41 22 4.7 false(unreach-call) 1 wit inspect 8.7 360 true -32 wit inspect 5.8 390 unknown 0 wit inspect 5.2 240 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 .44 26 6.2 false(unreach-call) 1 wit inspect 22   910 true -32 wit inspect 8.8 420 unknown 0 wit inspect 3.8 250 true -32 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36 19 4.6 false(unreach-call) 1 wit inspect 5.9 290 true -32 wit inspect 5.6 360 unknown 0 wit inspect 5.1 240 false(unreach-call) 1 wit inspect .85 18 - wit inspect - wit inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 20 4.7 false(unreach-call) 1 wit inspect 6.4 290 true -32 wit inspect 8.2 370 unknown 0 wit inspect 5.4 250 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 .37 20 4.6 false(unreach-call) 1 wit inspect 4.3 300 true -32 wit inspect 8.3 370 unknown 0 wit inspect 3.5 240 false(unreach-call) 1 wit inspect .88 18 - wit inspect - wit inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 20 4.8 false(unreach-call) 1 wit inspect 7.1 310 true -32 wit inspect 8.6 380 unknown 0 wit inspect 3.6 240 false(unreach-call) 1 wit inspect .87 19 - wit inspect - wit inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .45 24 5.8 false(unreach-call) 1 wit inspect 39   2000 true -32 wit inspect 8.7 400 unknown 0 wit inspect 3.7 240 true -32 wit inspect .88 19 - wit inspect - wit inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    15000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 44 error (2) 0 wit inspect .021 4.8
elevator_spec13_product22_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    15000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9
elevator_spec13_product23_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    15000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.9
elevator_spec13_product24_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    15000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
elevator_spec13_product29_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    15000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .021 4.8
elevator_spec13_product30_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    15000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 46 error (2) 0 wit inspect .018 5.0
elevator_spec13_product31_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    15000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .018 4.8
elevator_spec13_product32_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    15000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .019 4.9
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    15000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.9
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 17 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    670 out of memory 0 wit inspect 210     7000  
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 18 4.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    690 out of memory 0 wit inspect 300     7000  
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 17 4.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    720 out of memory 0 wit inspect 260     7000  
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 22 5.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    1000 out of memory 0 wit inspect 240     7000  
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 18 4.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    660 out of memory 0 wit inspect 260     7000  
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 19 4.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 32    1100 out of memory 0 wit inspect 140     7000  
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 17 5.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 68    1400 out of memory 0 wit inspect 280     7000  
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 18 4.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 70    1500 out of memory 0 wit inspect 300     7000  
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 18 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 77    1500 out of memory 0 wit inspect 200     7000  
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 18 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 88    1600 out of memory 0 wit inspect 250     7000  
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .34 18 5.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 77    1500 out of memory 0 wit inspect 280     7000  
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 18 4.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 80    1700 out of memory 0 wit inspect 270     7000  
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 18 5.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 160    1900 out of memory 0 wit inspect 290     7000  
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 19 4.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 110    2100 out of memory 0 wit inspect 170     7000  
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 19 4.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 65    1700 out of memory 0 wit inspect 190     7000  
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 19 5.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 94    1700 out of memory 0 wit inspect 240     7000  
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 19 5.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 150    2000 out of memory 0 wit inspect 180     7000  
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .40 20 4.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140    2100 out of memory 0 wit inspect 210     7000  
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 17 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    890 out of memory 0 wit inspect 150     7000  
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 17 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 32    880 out of memory 0 wit inspect 110     7000  
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 18 4.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 34    910 out of memory 0 wit inspect 160     7000  
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 18 4.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 35    970 out of memory 0 wit inspect 160     7000  
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 18 4.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 33    940 out of memory 0 wit inspect 120     7000  
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 18 4.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    960 out of memory 0 wit inspect 160     7000  
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 18 4.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 48    1100 out of memory 0 wit inspect 130     7000  
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 19 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 35    1200 out of memory 0 wit inspect 280     7000  
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 18 4.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 32    920 out of memory 0 wit inspect 130     7000  
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 19 4.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 43    1000 out of memory 0 wit inspect 180     7000  
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 19 5.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 48    1200 out of memory 0 wit inspect 180     7000  
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .40 19 4.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 54    1300 out of memory 0 wit inspect 160     7000  
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 19 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    680 out of memory 0 wit inspect 210     7000  
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 20 4.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    670 out of memory 0 wit inspect 170     7000  
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 20 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    700 out of memory 0 wit inspect 260     7000  
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 20 4.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    850 out of memory 0 wit inspect 150     7000  
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 20 4.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24    880 out of memory 0 wit inspect 130     7000  
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 21 4.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    1500 out of memory 0 wit inspect 230     7000  
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 20 4.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    690 out of memory 0 wit inspect 140     7000  
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 21 4.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28    1100 out of memory 0 wit inspect 190     7000  
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 21 5.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24    910 out of memory 0 wit inspect 130     7000  
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 22 4.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28    1600 out of memory 0 wit inspect 180     7000  
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 18 4.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 34    920 out of memory 0 wit inspect 210     7000  
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 19 4.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    970 out of memory 0 wit inspect 160     7000  
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 18 4.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 35    940 out of memory 0 wit inspect 150     7000  
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 19 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 36    1000 out of memory 0 wit inspect 140     7000  
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 19 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 46    1200 out of memory 0 wit inspect 180     7000  
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 20 4.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 36    1200 out of memory 0 wit inspect 140     7000  
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 15 4.5 false(unreach-call) 1 wit inspect 11   460 true -32 wit inspect 7.9 330 unknown 0 wit inspect 4.6 220 true -32 wit inspect .84 19 - wit inspect - wit inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 17 4.6 false(unreach-call) 1 wit inspect 8.7 510 true -32 wit inspect 5.7 360 unknown 0 wit inspect 3.3 230 true -32 wit inspect .85 18 - wit inspect - wit inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 16 4.7 false(unreach-call) 1 wit inspect 6.0 470 true -32 wit inspect 5.7 350 unknown 0 wit inspect 4.7 220 true -32 wit inspect .85 19 - wit inspect - wit inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 18 4.8 false(unreach-call) 1 wit inspect 17   510 true -32 wit inspect 8.1 370 unknown 0 wit inspect 5.0 220 true -32 wit inspect .88 19 - wit inspect - wit inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 17 4.6 false(unreach-call) 1 wit inspect 11   470 true -32 wit inspect 5.6 350 unknown 0 wit inspect 4.9 220 true -32 wit inspect .85 18 - wit inspect - wit inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 18 5.3 false(unreach-call) 1 wit inspect 8.2 460 true -32 wit inspect 5.3 360 unknown 0 wit inspect 3.3 220 true -32 wit inspect .84 18 - wit inspect - wit inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 19 4.8 false(unreach-call) 1 wit inspect 16   530 true -32 wit inspect 8.1 370 unknown 0 wit inspect 3.5 220 true -32 wit inspect .87 19 - wit inspect - wit inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .45 20 5.0 false(unreach-call) 1 wit inspect 8.8 510 true -32 wit inspect 8.3 390 unknown 0 wit inspect 5.4 270 true -32 wit inspect .85 18 - wit inspect - wit inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  38 15   false(unreach-call) 1 wit inspect 19   630 true -32 wit inspect 6.0 430 unknown 0 wit inspect 3.5 240 true -32 wit inspect .90 19 - wit inspect - wit inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 15 3.9 false(unreach-call) 1 wit inspect 8.5 450 true -32 wit inspect 7.8 330 unknown 0 wit inspect 4.6 230 false(unreach-call) 1 wit inspect .83 18 - wit inspect - wit inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 17 5.2 false(unreach-call) 1 wit inspect 17   490 true -32 wit inspect 7.7 350 unknown 0 wit inspect 4.9 220 false(unreach-call) 1 wit inspect .88 18 - wit inspect - wit inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 16 4.5 false(unreach-call) 1 wit inspect 8.4 460 true -32 wit inspect 5.3 340 unknown 0 wit inspect 3.2 220 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 .38 18 4.4 false(unreach-call) 1 wit inspect 12   510 true -32 wit inspect 5.5 370 unknown 0 wit inspect 3.4 260 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 16 4.7 false(unreach-call) 1 wit inspect 9.1 470 true -32 wit inspect 5.5 340 unknown 0 wit inspect 3.3 230 false(unreach-call) 1 wit inspect .85 18 - wit inspect - wit inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 18 5.4 false(unreach-call) 1 wit inspect 14   510 true -32 wit inspect 5.7 370 unknown 0 wit inspect 3.6 240 false(unreach-call) 1 wit inspect .88 18 - wit inspect - wit inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 18 5.2 false(unreach-call) 1 wit inspect 6.0 470 true -32 wit inspect 5.6 360 unknown 0 wit inspect 5.1 270 false(unreach-call) 1 wit inspect .85 18 - wit inspect - wit inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 20 5.3 false(unreach-call) 1 wit inspect 16   420 true -32 wit inspect 5.8 380 unknown 0 wit inspect 5.0 230 false(unreach-call) 1 wit inspect .86 18 - wit inspect - wit inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .72 25 9.0 false(unreach-call) 1 wit inspect 19   620 true -32 wit inspect 9.4 430 unknown 0 wit inspect 3.5 240 true -32 wit inspect .89 18 - wit inspect - wit inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 16 5.4 false(unreach-call) 1 wit inspect 9.5 460 true -32 wit inspect 8.0 340 unknown 0 wit inspect 3.2 220 true -32 wit inspect .83 18 - wit inspect - wit inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 17 5.4 false(unreach-call) 1 wit inspect 8.7 470 true -32 wit inspect 7.8 330 unknown 0 wit inspect 3.3 270 true -32 wit inspect .84 18 - wit inspect - wit inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 15 5.0 false(unreach-call) 1 wit inspect 11   460 true -32 wit inspect 5.4 340 unknown 0 wit inspect 4.8 220 true -32 wit inspect .84 18 - wit inspect - wit inspect
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 17 4.8 false(unreach-call) 1 wit inspect 6.1 470 true -32 wit inspect 5.2 360 unknown 0 wit inspect 4.9 270 true -32 wit inspect .84 18 - wit inspect - wit inspect
email_spec1_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 17 4.7 false(unreach-call) 1 wit inspect 6.7 480 true -32 wit inspect 5.7 360 unknown 0 wit inspect 4.8 220 true -32 wit inspect .85 18 - wit inspect - wit inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .45 16 4.9 false(unreach-call) 1 wit inspect 10   480 true -32 wit inspect 5.3 340 unknown 0 wit inspect 4.4 220 true -32 wit inspect .86 19 - wit inspect - wit inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43 18 5.3 false(unreach-call) 1 wit inspect 11   480 true -32 wit inspect 5.9 360 unknown 0 wit inspect 3.2 230 true -32 wit inspect .85 19 - wit inspect - wit inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43 17 5.2 false(unreach-call) 1 wit inspect 12   480 true -32 wit inspect 7.6 360 unknown 0 wit inspect 4.8 230 true -32 wit inspect .89 18 - wit inspect - wit inspect
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 17 6.4 false(unreach-call) 1 wit inspect 12   480 true -32 wit inspect 8.5 350 unknown 0 wit inspect 3.4 270 true -32 wit inspect .85 18 - wit inspect - wit inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 17 4.5 false(unreach-call) 1 wit inspect 11   370 true -32 wit inspect 5.7 350 unknown 0 wit inspect 4.8 270 true -32 wit inspect .88 19 - wit inspect - wit inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 18 5.5 false(unreach-call) 1 wit inspect 12   480 true -32 wit inspect 5.5 360 unknown 0 wit inspect 3.3 220 true -32 wit inspect .85 19 - wit inspect - wit inspect
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 18 5.0 false(unreach-call) 1 wit inspect 11   480 true -32 wit inspect 8.2 360 unknown 0 wit inspect 3.3 270 true -32 wit inspect .87 18 - wit inspect - wit inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43 19 4.9 false(unreach-call) 1 wit inspect 7.1 490 true -32 wit inspect 5.8 380 unknown 0 wit inspect 4.9 220 true -32 wit inspect .85 19 - wit inspect - wit inspect
email_spec1_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .47 20 7.1 false(unreach-call) 1 wit inspect 10   490 true -32 wit inspect 8.4 390 unknown 0 wit inspect 3.3 230 true -32 wit inspect .86 18 - wit inspect - wit inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  41 15   false(unreach-call) 1 wit inspect 14   520 true -32 wit inspect 8.9 420 unknown 0 wit inspect 3.5 230 true -32 wit inspect .90 19 - wit inspect - wit inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .55 19 6.3 false(unreach-call) 1 wit inspect 14   490 true -32 wit inspect 5.3 350 unknown 0 wit inspect 3.2 230 true -32 wit inspect .84 18 - wit inspect - wit inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .57 20 6.8 false(unreach-call) 1 wit inspect 16   500 true -32 wit inspect 7.6 340 unknown 0 wit inspect 4.6 220 true -32 wit inspect .84 18 - wit inspect - wit inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43 16 5.2 false(unreach-call) 1 wit inspect 13   510 true -32 wit inspect 5.5 350 unknown 0 wit inspect 4.8 220 true -32 wit inspect .84 18 - wit inspect - wit inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .58 20 8.1 false(unreach-call) 1 wit inspect 15   500 true -32 wit inspect 8.6 360 unknown 0 wit inspect 5.0 270 true -32 wit inspect .85 18 - wit inspect - wit inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 17 5.8 false(unreach-call) 1 wit inspect 15   500 true -32 wit inspect 5.0 350 unknown 0 wit inspect 4.8 220 true -32 wit inspect .88 18 - wit inspect - wit inspect
email_spec27_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43 18 5.1 false(unreach-call) 1 wit inspect 17   510