Tool 2LS 0.6.0 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:32:03 CET 2017-12-01 08:01:50 CET 2017-12-01 08:11:41 CET 2017-12-01 08:15:34 CET 2017-12-01 04:23:32 CET 2017-12-01 07:36:49 CET
Run set 2ls.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/product-lines/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
elevator_spec14_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.0  1200 56    true -32 wit inspect 11   330 true -32 wit inspect 9.5 460 unknown 0 wit inspect 19   1300 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.9  2000 81    true -32 wit inspect 12   440 true -32 wit inspect 10   450 unknown 0 wit inspect 33   1700 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.2  1300 60    true -32 wit inspect 10   430 true -32 wit inspect 8.8 450 unknown 0 wit inspect 24   1400 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11    2100 100    true -32 wit inspect 8.9 410 true -32 wit inspect 11   460 unknown 0 wit inspect 26   1700 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 36    7000 320    true -32 wit inspect 13   360 true -32 wit inspect 9.5 420 unknown 0 wit inspect 37   2100 false(unreach-call) 1 wit inspect 1.5  21 - wit inspect - wit inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 41    850 490    true -32 wit inspect 8.5 350 true -32 wit inspect 8.9 370 unknown 0 wit inspect 16   600 false(unreach-call) 1 wit inspect 1.1  21 - wit inspect - wit inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 43    900 360    true -32 wit inspect 9.8 410 true -32 wit inspect 9.9 390 unknown 0 wit inspect 15   990 false(unreach-call) 1 wit inspect 1.1  21 - wit inspect - wit inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 43    1200 450    true -32 wit inspect 8.9 400 true -32 wit inspect 8.4 400 unknown 0 wit inspect 18   830 false(unreach-call) 1 wit inspect 1.3  21 - wit inspect - wit inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 49    1300 380    true -32 wit inspect 7.5 280 true -32 wit inspect 8.3 400 unknown 0 wit inspect 19   1100 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 43    890 370    true -32 wit inspect 8.5 280 true -32 wit inspect 8.7 380 unknown 0 wit inspect 14   610 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 45    950 560    true -32 wit inspect 10   410 true -32 wit inspect 10   390 unknown 0 wit inspect 16   960 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 53    1200 420    true -32 wit inspect 6.8 280 true -32 wit inspect 8.8 390 unknown 0 wit inspect 14   820 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 62    1300 440    true -32 wit inspect 10   430 true -32 wit inspect 11   390 unknown 0 wit inspect 22   1100 false(unreach-call) 1 wit inspect 1.1  21 - wit inspect - wit inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140    3700 1100    true -32 wit inspect 9.8 430 true -32 wit inspect 10   440 unknown 0 wit inspect 17   1100 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 36    870 380    true -32 wit inspect 8.2 280 true -32 wit inspect 11   390 unknown 0 wit inspect 15   480 false(unreach-call) 1 wit inspect 1.0  20 - wit inspect - wit inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 37    930 330    true -32 wit inspect 9.6 300 true -32 wit inspect 8.5 370 unknown 0 wit inspect 15   820 false(unreach-call) 1 wit inspect 1.4  21 - wit inspect - wit inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 46    1200 540    true -32 wit inspect 8.9 360 true -32 wit inspect 8.6 400 unknown 0 wit inspect 12   720 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 44    1300 340    true -32 wit inspect 6.6 420 true -32 wit inspect 11   410 unknown 0 wit inspect 19   1000 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 32    900 310    true -32 wit inspect 8.7 330 true -32 wit inspect 8.8 380 unknown 0 wit inspect 14   610 false(unreach-call) 1 wit inspect 1.4  20 - wit inspect - wit inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 36    970 290    true -32 wit inspect 11   430 true -32 wit inspect 8.6 410 unknown 0 wit inspect 15   700 false(unreach-call) 1 wit inspect 1.3  21 - wit inspect - wit inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 40    1200 380    true -32 wit inspect 8.3 360 true -32 wit inspect 8.6 400 unknown 0 wit inspect 13   680 false(unreach-call) 1 wit inspect 1.2  22 - wit inspect - wit inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 46    1300 430    true -32 wit inspect 9.7 410 true -32 wit inspect 8.4 410 unknown 0 wit inspect 17   1000 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130    3800 1200    true -32 wit inspect 5.9 290 true -32 wit inspect 9.0 430 unknown 0 wit inspect 6.0 280 false(unreach-call) 1 wit inspect 1.4  21 - wit inspect - wit inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.9  580 31    true -32 wit inspect 7.5 280 true -32 wit inspect 9.0 450 unknown 0 wit inspect 8.2 390 false(unreach-call) 1 wit inspect 1.1  22 - wit inspect - wit inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1  620 29    true -32 wit inspect 7.8 280 true -32 wit inspect 9.4 460 unknown 0 wit inspect 11   400 false(unreach-call) 1 wit inspect 1.1  22 - wit inspect - wit inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.2  660 32    true -32 wit inspect 8.4 280 true -32 wit inspect 12   460 unknown 0 wit inspect 9.0 290 false(unreach-call) 1 wit inspect 1.2  22 - wit inspect - wit inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.1  1200 61    true -32 wit inspect 8.3 280 true -32 wit inspect 10   460 unknown 0 wit inspect 9.3 280 false(unreach-call) 1 wit inspect 1.1  21 - wit inspect - wit inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.4  1000 53    true -32 wit inspect 7.7 280 true -32 wit inspect 9.6 460 unknown 0 wit inspect 6.6 420 false(unreach-call) 1 wit inspect 1.2  22 - wit inspect - wit inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11    2000 99    true -32 wit inspect 8.4 290 true -32 wit inspect 12   460 unknown 0 wit inspect 8.8 420 false(unreach-call) 1 wit inspect 1.2  22 - wit inspect - wit inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.6  700 34    true -32 wit inspect 7.5 280 true -32 wit inspect 9.6 450 unknown 0 wit inspect 9.9 420 false(unreach-call) 1 wit inspect 1.3  22 - wit inspect - wit inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.6  1300 63    true -32 wit inspect 8.2 310 true -32 wit inspect 10   460 unknown 0 wit inspect 8.7 430 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.5  1100 64    true -32 wit inspect 5.3 280 true -32 wit inspect 12   460 unknown 0 wit inspect 9.0 420 false(unreach-call) 1 wit inspect 1.3  22 - wit inspect - wit inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11    2100 120    true -32 wit inspect 8.9 310 true -32 wit inspect 10   460 unknown 0 wit inspect 8.5 420 false(unreach-call) 1 wit inspect 1.5  22 - wit inspect - wit inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 38    7000 400    true -32 wit inspect 8.0 290 false(unreach-call) 1 wit inspect 54   2500 unknown 0 wit inspect 9.4 310 false(unreach-call) 1 wit inspect 1.3  22 - wit inspect - wit inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 39    900 390    true -32 wit inspect 8.2 300 true -32 wit inspect 11   390 unknown 0 wit inspect 13   610 false(unreach-call) 1 wit inspect 1.3  20 - wit inspect - wit inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 39    950 400    true -32 wit inspect 9.1 420 true -32 wit inspect 8.7 380 unknown 0 wit inspect 19   890 false(unreach-call) 1 wit inspect 1.4  21 - wit inspect - wit inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 46    1300 360    true -32 wit inspect 9.2 390 true -32 wit inspect 11   410 unknown 0 wit inspect 15   690 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 47    1300 340    true -32 wit inspect 11   430 true -32 wit inspect 11   410 unknown 0 wit inspect 24   1100 false(unreach-call) 1 wit inspect 1.3  21 - wit inspect - wit inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 93    3700 870    true -32 wit inspect 5.8 300 true -32 wit inspect 9.0 420 unknown 0 wit inspect 6.1 280 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c error (5) 0 wit inspect 5.4  1000 48    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 4.9
elevator_spec13_product22_true-unreach-call_false-termination.cil.c error (5) 0 wit inspect 11    1900 100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 5.0
elevator_spec13_product23_true-unreach-call_false-termination.cil.c error (5) 0 wit inspect 5.9  1100 50    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0
elevator_spec13_product24_true-unreach-call_false-termination.cil.c error (5) 0 wit inspect 11    2100 98    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8
elevator_spec13_product29_true-unreach-call_false-termination.cil.c error (5) 0 wit inspect 5.6  1100 44    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0
elevator_spec13_product30_true-unreach-call_false-termination.cil.c error (5) 0 wit inspect 11    2000 91    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .048 4.8
elevator_spec13_product31_true-unreach-call_false-termination.cil.c error (5) 0 wit inspect 5.8  1200 60    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .024 5.0
elevator_spec13_product32_true-unreach-call_false-termination.cil.c error (5) 0 wit inspect 11    2200 140    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .023 4.8
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c error (5) 0 wit inspect 47    7300 380    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .050 4.9
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 20    860 210    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 22    900 out of memory 0 wit inspect 330     7000  
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 20    910 180    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    980 out of memory 0 wit inspect 310     7000  
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 24    1000 240    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24    1400 out of memory 0 wit inspect 230     7000  
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 10    1300 100    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 35    1600 out of memory 0 wit inspect 260     7000  
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 24    1100 220    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    1400 out of memory 0 wit inspect 280     7000  
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 11    1400 110    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 32    1600 out of memory 0 wit inspect 210     7000  
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 28    1000 240    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 80    1800 out of memory 0 wit inspect 290     7000  
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 30    1100 300    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 78    1900 out of memory 0 wit inspect 270     7000  
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 29    1000 270    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 100    1900 out of memory 0 wit inspect 270     7000  
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 31    1100 300    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 86    2100 out of memory 0 wit inspect 290     7000  
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 33    1100 300    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 78    1900 out of memory 0 wit inspect 280     7000  
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 31    1100 280    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 100    2100 out of memory 0 wit inspect 230     7000  
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 39    1500 350    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 170    2600 out of memory 0 wit inspect 290     7000  
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 39    1600 420    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140    2700 out of memory 0 wit inspect 220     7000  
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 29    1100 330    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 72    2000 out of memory 0 wit inspect 230     7000  
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 34    1200 320    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 88    2200 out of memory 0 wit inspect 310     7000  
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 37    1600 350    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 190    2700 out of memory 0 wit inspect 200     7000  
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 37    1600 420    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 150    2800 out of memory 0 wit inspect 240     7000  
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 21    710 180    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    1100 out of memory 0 wit inspect 140     7000  
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 21    750 220    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 37    1200 out of memory 0 wit inspect 150     7000  
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    750 200    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    1200 out of memory 0 wit inspect 170     7000  
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    790 240    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 38    1300 out of memory 0 wit inspect 150     7000  
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 23    780 260    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 35    1300 out of memory 0 wit inspect 130     7000  
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 26    830 250    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 34    1400 out of memory 0 wit inspect 110     7000  
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 24    1100 280    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 52    1500 out of memory 0 wit inspect 140     7000  
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 29    1100 240    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 44    1600 out of memory 0 wit inspect 230     7000  
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 25    810 220    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 36    1300 out of memory 0 wit inspect 130     7000  
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 27    860 230    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 56    1700 out of memory 0 wit inspect 190     7000  
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 28    1100 220    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 61    1600 out of memory 0 wit inspect 130     7000  
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 30    1200 260    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 56    1800 out of memory 0 wit inspect 190     7000  
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.1  630 31    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    920 out of memory 0 wit inspect 220     7000  
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.3  680 31    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    890 out of memory 0 wit inspect 160     7000  
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.4  730 34    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 29    920 out of memory 0 wit inspect 150     7000  
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.4  1400 61    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    1600 out of memory 0 wit inspect 190     7000  
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.5  1200 50    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 29    1400 out of memory 0 wit inspect 130     7000  
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 11    2300 120    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 40    1600 out of memory 0 wit inspect 190     7000  
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.6  770 34    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28    980 out of memory 0 wit inspect 130     7000  
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.8  1500 63    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 32    1600 out of memory 0 wit inspect 220     7000  
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.7  1200 57    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28    1400 out of memory 0 wit inspect 120     7000  
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 12    2400 120    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 42    1700 out of memory 0 wit inspect 230     7000  
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    750 220    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 33    1300 out of memory 0 wit inspect 180     7000  
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    780 190    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 40    1300 out of memory 0 wit inspect 130     7000  
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    810 320    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 32    1200 out of memory 0 wit inspect 140     7000  
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 24    860 210    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 38    1700 out of memory 0 wit inspect 120     7000  
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 28    1100 280    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 48    1600 out of memory 0 wit inspect 230     7000  
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 33    1200 320    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 53    1800 out of memory 0 wit inspect 180     7000  
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 21    290 190    true -32 wit inspect 9.1 390 unknown 0 wit inspect 29   580 unknown 0 wit inspect 7.2 290 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 37    500 300    true -32 wit inspect 18   530 unknown 0 wit inspect 33   570 unknown 0 wit inspect 9.2 420 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 26    310 190    true -32 wit inspect 9.2 410 unknown 0 wit inspect 34   600 unknown 0 wit inspect 7.5 350 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 42    540 550    true -32 wit inspect 18   630 unknown 0 wit inspect 55   640 unknown 0 wit inspect 12   420 false(unreach-call) 1 wit inspect 1.3  20 - wit inspect - wit inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 20    320 210    true -32 wit inspect 10   410 unknown 0 wit inspect 40   610 unknown 0 wit inspect 9.0 370 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 25    350 210    true -32 wit inspect 9.6 410 unknown 0 wit inspect 32   580 unknown 0 wit inspect 9.2 280 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 37    590 430    true -32 wit inspect 15   460 unknown 0 wit inspect 45   680 unknown 0 wit inspect 8.2 420 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 48    670 450    true -32 wit inspect 5.7 270 unknown 0 wit inspect 50   880 unknown 0 wit inspect 10   450 false(unreach-call) 1 wit inspect 1.5  20 - wit inspect - wit inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 200    8000 1300    true -32 wit inspect 7.2 300 true -32 wit inspect 11   440 unknown 0 wit inspect 11   460 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 19    270 240    true -32 wit inspect 11   410 unknown 0 wit inspect 41   590 unknown 0 wit inspect 8.7 420 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 41    460 400    true -32 wit inspect 11   400 unknown 0 wit inspect 39   620 unknown 0 wit inspect 8.9 360 false(unreach-call) 1 wit inspect 1.1  19 - wit inspect - wit inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 21    310 210    true -32 wit inspect 12   440 unknown 0 wit inspect 29   570 unknown 0 wit inspect 8.3 420 false(unreach-call) 1 wit inspect 1.0  20 - wit inspect - wit inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 43    540 370    true -32 wit inspect 18   630 unknown 0 wit inspect 41   560 unknown 0 wit inspect 9.0 410 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 23    300 190    true -32 wit inspect 9.3 410 unknown 0 wit inspect 37   640 unknown 0 wit inspect 8.9 280 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 39    520 370    true -32 wit inspect 13   460 unknown 0 wit inspect 47   720 unknown 0 wit inspect 7.9 380 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 22    350 210    true -32 wit inspect 14   400 unknown 0 wit inspect 39   670 unknown 0 wit inspect 11   420 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 46    640 420    true -32 wit inspect 15   460 unknown 0 wit inspect 40   780 unknown 0 wit inspect 8.2 410 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 280    8500 1400    true -32 wit inspect 15   490 true -32 wit inspect 10   460 unknown 0 wit inspect 12   470 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 31    390 290    true -32 wit inspect 9.1 340 true -32 wit inspect 8.8 380 unknown 0 wit inspect 7.5 330 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 23    250 180    true -32 wit inspect 8.8 370 true -32 wit inspect 9.9 380 unknown 0 wit inspect 6.7 300 false(unreach-call) 1 wit inspect 1.4  20 - wit inspect - wit inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 23    270 180    true -32 wit inspect 9.2 370 true -32 wit inspect 9.9 390 unknown 0 wit inspect 7.4 330 false(unreach-call) 1 wit inspect 1.3  20 - wit inspect - wit inspect
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 41    440 320    true -32 wit inspect 12   410 true -32 wit inspect 8.4 400 unknown 0 wit inspect 11   280 false(unreach-call) 1 wit inspect 1.4  20 - wit inspect - wit inspect
email_spec1_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 42    480 350    true -32 wit inspect 18   580 true -32 wit inspect 8.9 410 unknown 0 wit inspect 8.9 410 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 25    290 210    true -32 wit inspect 10   430 true -32 wit inspect 8.3 400 unknown 0 wit inspect 7.3 340 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 44    520 400    true -32 wit inspect 13   470 true -32 wit inspect 10   430 unknown 0 wit inspect 8.1 280 false(unreach-call) 1 wit inspect 1.1  20 - wit inspect - wit inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 33    460 280    true -32 wit inspect 13   460 true -32 wit inspect 10   440 unknown 0 wit inspect 9.0 410 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 21    300 240    true -32 wit inspect 6.0 270 true -32 wit inspect 8.8 400 unknown 0 wit inspect 10   300 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 22    310 260    true -32 wit inspect 11   410 true -32 wit inspect 9.9 400 unknown 0 wit inspect 7.9 370 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 39    500 330    true -32 wit inspect 13   460 true -32 wit inspect 9.2 430 unknown 0 wit inspect 8.4 410 false(unreach-call) 1 wit inspect 1.2  20 - wit inspect - wit inspect
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 25    340 270    true -32 wit inspect 11   410 true -32 wit inspect 11   430 unknown 0 wit inspect 9.3 280 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 40    570 340    true -32 wit inspect 16   460 true -32 wit inspect 9.9 460 unknown 0 wit inspect 10   420 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
email_spec1_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 45    620 360    true -32 wit inspect 16   460 true -32 wit inspect 9.5 450 unknown 0 wit inspect 9.2 410 false(unreach-call) 1 wit inspect 1.5  20 - wit inspect - wit inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 140    7600 1100    true -32 wit inspect 14   470 true -32 wit inspect 9.6 460 unknown 0 wit inspect 10   460 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 32    400 280    true -32 wit inspect 9.3 370 unknown 0 wit inspect 34   610 unknown 0 wit inspect 7.7 280 false(unreach-call) 1 wit inspect 1.3  20 - wit inspect - wit inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 23    260 180    true -32 wit inspect 8.8 380 true -32 wit inspect 8.5 390 unknown 0 wit inspect 8.1 310 false(unreach-call) 1 wit inspect 1.4  21 - wit inspect - wit inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 19    280 190    true -32 wit inspect 9.3 410 true -32 wit inspect 10   400 unknown 0 wit inspect 8.3 340 false(unreach-call) 1 wit inspect 1.2  21 - wit inspect - wit inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 44    450 370    true -32 wit inspect 13   440 unknown 0 wit inspect 45   700 unknown 0 wit inspect 8.1 280 false(unreach-call) 1 wit inspect 1.3  21 - wit inspect - wit inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 23    300 200    true -32 wit inspect 6.8 440 true -32 wit inspect 10   400 unknown 0 wit inspect 9.5 280 false(unreach-call) 1 wit inspect 1.3  21 - wit inspect - wit inspect
email_spec27_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 33    480 330    true -32 wit inspect 14   440 unknown 0 wit inspect 39