Tool DepthK 3.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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* [apollon001; apollon005; apollon039; apollon053; apollon087; apollon091] [apollon007; apollon009; apollon073; apollon078] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-05 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-06 11:42:46 CET 2018-12-12 19:35:41 CET 2018-12-06 09:26:28 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/product-lines/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
elevator_spec14_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .25 .25 45 2.4 1.0  0      false(unreach-call) 1 wit inspect 7.0 3.7 280 0   0   true -32 --- inspect 16   9.1 510 .62 0   false(unreach-call) 1 --- inspect 5.5 3.1 270 0     0   false(unreach-call) 1 --- inspect .84 .84 20 .34 0     - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24 .23 45 2.7 1.0  0      false(unreach-call) 1 wit inspect 9.5 5.1 300 0   0   true -32 --- inspect 15   9.1 520 .62 0   false(unreach-call) 1 --- inspect 5.3 3.0 260 0     0   false(unreach-call) 1 --- inspect .85 .85 20 .35 0     - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24 .23 45 2.9 1.0  0      false(unreach-call) 1 wit inspect 6.9 3.7 280 0   0   true -32 --- inspect 16   9.3 470 .62 0   false(unreach-call) 1 --- inspect 5.3 3.0 260 0     0   false(unreach-call) 1 --- inspect .88 .88 21 .34 0     - --- inspect - --- inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 45 2.9 .85 0      false(unreach-call) 1 wit inspect 7.3 3.9 290 0   0   true -32 --- inspect 16   9.0 510 .66 0   false(unreach-call) 1 --- inspect 5.6 3.1 270 0     0   false(unreach-call) 1 --- inspect .84 .84 20 .35 0     - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.9  2.9  160 35   1.0  0      true -32 wit inspect 7.1 3.8 280 0   0   true -32 --- inspect 17   9.8 540 .62 0   false(unreach-call) 1 --- inspect 7.6 4.1 370 0     0   false(unreach-call) 1 --- inspect .86 .86 21 .38 0     - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.9  3.9  86 47   62    0      false(unreach-call) 1 wit inspect 7.4 4.0 280 0   0   true -32 --- inspect 15   8.8 510 .62 0   false(unreach-call) 1 --- inspect 5.4 3.0 270 0     0   false(unreach-call) 1 --- inspect .84 .84 20 .34 0     - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.2  4.2  90 48   52    0      false(unreach-call) 1 wit inspect 7.2 3.8 280 0   0   true -32 --- inspect 16   9.4 530 .62 0   false(unreach-call) 1 --- inspect 5.6 3.1 260 0     0   false(unreach-call) 1 --- inspect .85 .85 21 .36 .074 - --- inspect - --- inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.1  5.1  110 66   60    0      false(unreach-call) 1 wit inspect 7.5 4.0 290 0   0   true -32 --- inspect 16   9.5 460 .62 0   false(unreach-call) 1 --- inspect 5.4 3.0 260 0     0   false(unreach-call) 1 --- inspect .84 .84 20 .35 .074 - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.6  5.6  110 69   62    0      false(unreach-call) 1 wit inspect 7.8 4.2 290 0   0   true -32 --- inspect 15   9.0 510 .62 0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0     0   false(unreach-call) 1 --- inspect .85 .86 20 .36 0     - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.2  4.2  95 53   62    0      false(unreach-call) 1 wit inspect 8.9 4.8 280 0   0   true -32 --- inspect 15   9.0 510 .62 0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0     0   false(unreach-call) 1 --- inspect .86 .87 20 .35 .074 - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.3  4.3  99 53   52    0      false(unreach-call) 1 wit inspect 7.4 4.0 290 0   0   true -32 --- inspect 17   9.8 470 .62 0   false(unreach-call) 1 --- inspect 5.4 3.1 270 0     0   false(unreach-call) 1 --- inspect .87 .87 20 .36 0     - --- inspect - --- inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.3  5.3  110 77   62    0      false(unreach-call) 1 wit inspect 7.8 4.2 290 0   0   true -32 --- inspect 17   10   520 .62 0   false(unreach-call) 1 --- inspect 5.4 3.0 270 0     0   false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.8  5.8  120 81   62    0      false(unreach-call) 1 wit inspect 7.7 4.1 290 0   0   true -32 --- inspect 17   9.9 530 .62 0   false(unreach-call) 1 --- inspect 5.4 3.1 270 0     0   false(unreach-call) 1 --- inspect .86 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 27    27    260 330   62    0      true -32 wit inspect 6.4 3.4 280 0   0   true -32 --- inspect 16   9.6 530 .62 0   false(unreach-call) 1 --- inspect 9.4 5.0 430 0     0   false(unreach-call) 1 --- inspect .91 .95 21 .33 0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.9  3.9  86 50   62    0      false(unreach-call) 1 wit inspect 7.2 3.9 280 0   0   true -32 --- inspect 16   9.3 460 .62 0   false(unreach-call) 1 --- inspect 5.4 3.0 260 0     0   false(unreach-call) 1 --- inspect .84 .84 20 .34 0     - --- inspect - --- inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.3  4.2  89 50   62    0      false(unreach-call) 1 wit inspect 7.7 4.1 290 0   0   true -32 --- inspect 15   8.8 520 .66 0   false(unreach-call) 1 --- inspect 5.5 3.0 270 0     0   false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.1  5.1  110 61   62    0      false(unreach-call) 1 wit inspect 7.2 3.9 290 0   0   true -32 --- inspect 15   9.0 510 .62 0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0     0   false(unreach-call) 1 --- inspect .88 .90 21 .35 0     - --- inspect - --- inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.4  5.4  110 76   52    0      false(unreach-call) 1 wit inspect 7.6 4.1 290 0   0   true -32 --- inspect 15   8.3 510 .62 0   false(unreach-call) 1 --- inspect 5.6 3.1 270 0     0   false(unreach-call) 1 --- inspect .87 .87 20 .36 0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.1  4.1  94 63   62    0      false(unreach-call) 1 wit inspect 7.2 3.8 280 0   0   true -32 --- inspect 15   8.5 470 .62 0   false(unreach-call) 1 --- inspect 5.1 2.9 270 0     0   false(unreach-call) 1 --- inspect .85 .85 20 .35 0     - --- inspect - --- inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.5  4.5  97 57   52    0      false(unreach-call) 1 wit inspect 7.6 4.1 280 0   0   true -32 --- inspect 15   8.2 510 .62 0   false(unreach-call) 1 --- inspect 5.5 3.1 260 0     0   false(unreach-call) 1 --- inspect .86 .86 20 .36 0     - --- inspect - --- inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.3  5.3  110 69   54    0      false(unreach-call) 1 wit inspect 8.3 4.5 290 0   0   true -32 --- inspect 16   9.3 470 .62 0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0     0   false(unreach-call) 1 --- inspect .84 .84 20 .36 0     - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.7  5.7  120 71   52    0      false(unreach-call) 1 wit inspect 8.7 4.7 290 0   0   true -32 --- inspect 17   9.9 520 .62 0   false(unreach-call) 1 --- inspect 5.8 3.2 290 0     0   false(unreach-call) 1 --- inspect .87 .90 21 .24 0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 26    26    260 360   62    0      true -32 wit inspect 7.0 3.7 280 0   0   true -32 --- inspect 19   11   520 .62 0   false(unreach-call) 1 --- inspect 9.0 4.8 430 0     0   false(unreach-call) 1 --- inspect .91 .91 21 .39 0     - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 45 3.0 .85 0      false(unreach-call) 1 wit inspect 7.9 4.2 290 0   0   true -32 --- inspect 15   8.8 520 .62 0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0     0   false(unreach-call) 1 --- inspect .84 .84 20 .34 0     - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 45 2.9 1.0  0      false(unreach-call) 1 wit inspect 8.9 4.8 290 0   0   true -32 --- inspect 15   8.9 470 .62 0   false(unreach-call) 1 --- inspect 5.2 3.0 270 0     0   false(unreach-call) 1 --- inspect .85 .85 20 .34 0     - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 45 2.8 1.0  0      false(unreach-call) 1 wit inspect 8.8 4.7 290 0   0   true -32 --- inspect 14   8.2 520 .62 0   false(unreach-call) 1 --- inspect 5.4 3.0 270 0     0   false(unreach-call) 1 --- inspect .85 .85 21 .35 .074 - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 45 3.5 1.0  0      false(unreach-call) 1 wit inspect 8.2 4.4 290 0   0   true -32 --- inspect 16   9.1 510 .62 0   false(unreach-call) 1 --- inspect 5.1 2.9 260 0     0   false(unreach-call) 1 --- inspect .84 .84 20 .35 0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 45 2.9 1.0  0      false(unreach-call) 1 wit inspect 8.2 4.4 310 0   0   true -32 --- inspect 17   9.5 520 .62 0   false(unreach-call) 1 --- inspect 5.4 3.1 260 0     0   false(unreach-call) 1 --- inspect .87 .87 20 .36 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .25 .25 46 2.8 .85 0      false(unreach-call) 1 wit inspect 7.9 4.3 320 0   0   true -32 --- inspect 18   10   480 .62 0   false(unreach-call) 1 --- inspect 5.2 2.9 270 0     0   false(unreach-call) 1 --- inspect .86 .86 20 .36 .078 - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 46 2.6 1.0  0      false(unreach-call) 1 wit inspect 8.4 4.5 290 0   0   true -32 --- inspect 15   8.7 510 .62 0   false(unreach-call) 1 --- inspect 5.4 3.1 270 0     0   false(unreach-call) 1 --- inspect .84 .86 20 .35 0     - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .25 .25 46 2.7 1.0  0      false(unreach-call) 1 wit inspect 8.6 4.6 290 0   0   true -32 --- inspect 17   9.6 470 .62 0   false(unreach-call) 1 --- inspect 5.5 3.1 270 0     0   false(unreach-call) 1 --- inspect .88 .90 20 .36 0     - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 46 3.0 .85 0      false(unreach-call) 1 wit inspect 8.6 4.7 310 0   0   true -32 --- inspect 15   8.6 520 .62 0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0     0   false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .25 .25 46 2.7 1.0  0      false(unreach-call) 1 wit inspect 8.2 4.4 320 0   0   true -32 --- inspect 15   9.0 520 .62 0   false(unreach-call) 1 --- inspect 5.5 3.1 260 0     0   false(unreach-call) 1 --- inspect .86 .86 20 .36 0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.2  5.2  260 65   .85 0      true -32 wit inspect 7.2 3.8 280 0   0   true -32 --- inspect 16   9.7 470 .62 0   false(unreach-call) 1 --- inspect 10   5.4 440 0     0   false(unreach-call) 1 --- inspect .88 .88 21 .39 0     - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.3  4.2  96 51   52    0      false(unreach-call) 1 wit inspect 7.0 3.8 280 0   0   true -32 --- inspect 17   9.5 470 .62 0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0     0   false(unreach-call) 1 --- inspect .84 .84 20 .34 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.5  4.5  98 57   62    0      false(unreach-call) 1 wit inspect 7.4 4.0 290 0   0   true -32 --- inspect 15   9.1 510 .62 0   false(unreach-call) 1 --- inspect 5.2 2.9 270 0     0   false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.6  5.5  110 62   61    0      false(unreach-call) 1 wit inspect 8.8 4.7 290 0   0   true -32 --- inspect 16   9.1 470 .62 0   false(unreach-call) 1 --- inspect 5.8 3.2 280 0     0   false(unreach-call) 1 --- inspect .86 .86 20 .36 0     - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.8  5.8  120 85   62    0      false(unreach-call) 1 wit inspect 8.6 4.6 300 0   0   true -32 --- inspect 18   11   470 .62 0   false(unreach-call) 1 --- inspect 5.4 3.1 270 0     0   false(unreach-call) 1 --- inspect .90 .90 20 .36 .078 - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 26    26    260 320   52    0      true -32 wit inspect 6.7 3.6 280 0   0   true -32 --- inspect 18   10   520 .62 0   false(unreach-call) 1 --- inspect 9.0 4.9 430 0     0   false(unreach-call) 1 --- inspect .87 .87 21 .39 0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 2.0  1.7  66 25   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2800 0   0   out of memory 0 --- inspect 240     150     7000   .67 0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 2.6  2.4  81 30   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3300 0   0   out of memory 0 --- inspect 200     130     7000   .64 0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 2.1  1.8  66 28   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4000 0   0   out of memory 0 --- inspect 240     160     7000   .84 0    
elevator_spec13_product24_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 2.8  2.6  85 37   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4300 0   0   out of memory 0 --- inspect 220     160     7000   .72 0    
elevator_spec13_product29_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 2.0  1.7  67 26   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2900 0   0   out of memory 0 --- inspect 240     160     7000   .66 0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 3.3  3.0  100 37   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3500 0   0   out of memory 0 --- inspect 210     150     7000   .65 0    
elevator_spec13_product31_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 2.1  1.8  67 23   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3700 0   0   out of memory 0 --- inspect 230     150     7000   .72 0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 2.8  2.6  88 36   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4500 0   0   out of memory 0 --- inspect 220     150     7000   .64 0    
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    4100 12000   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3400 0   0   out of memory 0 --- inspect 230     160     7000   .63 0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 2.0  1.7  67 25   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    680 0   0   out of memory 0 --- inspect 250     180     7000   .63 0    
elevator_spec14_product11_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 2.1  1.9  67 27   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    10    680 0   0   out of memory 0 --- inspect 270     190     7000   .65 0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 2.1  1.8  65 23   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23    13    710 0   0   out of memory 0 --- inspect 260     190     7000   .64 0    
elevator_spec14_product23_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 4.8  4.5  83 60   62    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25    15    1100 0   0   out of memory 0 --- inspect 290     190     7000   .64 0    
elevator_spec14_product27_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 2.2  1.9  67 26   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    730 0   0   out of memory 0 --- inspect 290     220     7000   .64 0    
elevator_spec14_product31_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 5.0  4.8  85 56   62    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    16    1100 0   0   out of memory 0 --- inspect 220     150     7000   .66 0    
elevator_spec1_product01_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 20    20    130 250   240    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 74    61    1600 0   0   out of memory 0 --- inspect 250     170     7000   .64 0    
elevator_spec1_product03_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 22    21    140 230   240    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 87    74    1700 0   0   out of memory 0 --- inspect 260     180     7000   .63 0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 22    22    150 270   240    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 79    65    1700 0   0   out of memory 0 --- inspect 240     170     7000   .63 0    
elevator_spec1_product11_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 23    23    160 350   240    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 94    80    1800 0   0   out of memory 0 --- inspect 250     170     7000   .65 0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 21    20    140 280   240    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 84    72    1800 0   0   out of memory 0 --- inspect 240     170     7000   .65 0    
elevator_spec1_product19_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 22    21    140 250   210    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 98    86    1800 0   0   out of memory 0 --- inspect 260     190     7000   .64 0    
elevator_spec1_product21_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 28    27    170 340   240    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 160    140    2300 0   0   out of memory 0 --- inspect 250     170     7000   .64 0    
elevator_spec1_product23_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 29    29    180 390   230    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 160    150    2300 0   0   out of memory 0 --- inspect 300     220     7000   .65 0    
elevator_spec1_product25_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 22    22    150 270   240    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 85    72    1900 0   0   out of memory 0 --- inspect 250     180     7000   1.3  0    
elevator_spec1_product27_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 24    23    160 340   240    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    100    2000 0   0   out of memory 0 --- inspect 300     210     7000   .67 0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 29    28    190 330   240    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 270    250    2300 0   0   out of memory 0 --- inspect 240     160     7000   .64 0    
elevator_spec1_product31_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 31    31    190 440   240    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 180    170    2400 0   0   out of memory 0 --- inspect 330     230     7000   .63 0    
elevator_spec2_product01_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 7.6  7.3  89 82   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    21    1000 0   0   out of memory 0 --- inspect 160     100     7000   1.7  0    
elevator_spec2_product03_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 7.9  7.6  91 110   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    26    1100 0   0   out of memory 0 --- inspect 230     150     7000   1.2  0    
elevator_spec2_product09_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 8.3  8.0  98 110   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    21    1100 0   0   out of memory 0 --- inspect 180     120     7000   .79 0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 8.8  8.5  100 100   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    25    1100 0   0   out of memory 0 --- inspect 200     140     7000   .65 0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 7.6  7.4  90 110   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    25    1200 0   0   out of memory 0 --- inspect 170     110     7000   .67 0    
elevator_spec2_product19_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 8.2  7.9  92 110   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 42    30    1200 0   0   out of memory 0 --- inspect 200     130     7000   .66 0    
elevator_spec2_product21_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 10    9.7  110 120   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 50    38    1300 0   0   out of memory 0 --- inspect 190     130     7000   .65 0    
elevator_spec2_product23_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 11    10    110 120   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 55    42    1500 0   0   out of memory 0 --- inspect 270     190     7000   .65 0    
elevator_spec2_product25_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 8.5  8.3  99 110   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    26    1200 0   0   out of memory 0 --- inspect 160     110     7000   .68 0    
elevator_spec2_product27_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 9.1  8.8  100 110   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 42    31    1200 0   0   out of memory 0 --- inspect 180     120     7000   .71 0    
elevator_spec2_product29_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 11    10    120 130   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 58    46    1500 0   0   out of memory 0 --- inspect 180     120     7000   .71 0    
elevator_spec2_product31_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 11    11    120 130   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 50    39    1600 0   0   out of memory 0 --- inspect 270     180     7000   .63 0    
elevator_spec3_product01_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 1.8  1.5  67 22   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.2  650 0   0   out of memory 0 --- inspect 150     97     7000   .65 0    
elevator_spec3_product09_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 1.9  1.6  66 25   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.7  660 0   0   out of memory 0 --- inspect 150     97     7000   .81 0    
elevator_spec3_product17_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 1.8  1.6  67 21   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.8  660 0   0   out of memory 0 --- inspect 180     120     7000   .71 0    
elevator_spec3_product18_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 2.5  2.2  67 31   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23    13    850 0   0   out of memory 0 --- inspect 170     110     7000   .65 0    
elevator_spec3_product21_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 2.2  1.9  67 26   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23    12    890 0   0   out of memory 0 --- inspect 220     150     7000   1.5  0    
elevator_spec3_product22_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 3.0  2.7  81 34   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 29    17    1400 0   0   out of memory 0 --- inspect 200     140     7000   1.6  0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 1.9  1.7  67 22   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    10    710 0   0   out of memory 0 --- inspect 150     97     7000   .66 0    
elevator_spec3_product26_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 2.6  2.3  71 31   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 26    14    940 0   0   out of memory 0 --- inspect 180     120     7000   .65 0    
elevator_spec3_product29_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 2.3  2.0  67 26   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    880 0   0   out of memory 0 --- inspect 240     160     7000   .71 0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 3.1  2.8  86 38   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    17    1600 0   0   out of memory 0 --- inspect 230     160     7000   .72 .033
elevator_spec9_product09_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 8.2  7.9  98 87   100    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    24    1100 0   0   out of memory 0 --- inspect 170     120     7000   1.5  0    
elevator_spec9_product11_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 8.8  8.5  100 97   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    29    1100 0   0   out of memory 0 --- inspect 220     140     7000   .71 0    
elevator_spec9_product25_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 8.4  8.1  99 130   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    23    1200 0   0   out of memory 0 --- inspect 210     140     7000   .70 0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 9.1  8.8  100 110   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 42    30    1200 0   0   out of memory 0 --- inspect 220     150     7000   .71 0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 11    10    120 120   120    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 69    58    1400 0   0   out of memory 0 --- inspect 190     130     7000   .66 0    
elevator_spec9_product31_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 11    11    120 120   100    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 62    48    1600 0   0   out of memory 0 --- inspect 270     180     7000   .64 0    
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.2  4.1  49 55   92    0      false(unreach-call) 1 wit inspect 7.1 3.8 290 0   0   true -32 --- inspect 15   8.6 460 .62 0   false(unreach-call) 1 --- inspect 6.7 3.7 270 0     0   false(unreach-call) 1 --- inspect .83 .83 21 .37 0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.8  6.8  61 85   78    0      false(unreach-call) 1 wit inspect 7.1 3.8 290 0   0   true -32 --- inspect 16   9.2 460 .62 0   false(unreach-call) 1 --- inspect 6.9 3.7 290 0     0   false(unreach-call) 1 --- inspect .84 .84 21 .38 0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.7  4.6  51 67   91    0      false(unreach-call) 1 wit inspect 7.4 3.9 290 0   0   true -32 --- inspect 15   8.7 500 .62 0   false(unreach-call) 1 --- inspect 6.6 3.6 280 0     0   false(unreach-call) 1 --- inspect .84 .84 21 .38 .066 - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.6  7.6  66 110   92    0      false(unreach-call) 1 wit inspect 9.7 5.1 300 0   0   true -32 --- inspect 15   8.2 510 .62 0   false(unreach-call) 1 --- inspect 7.0 3.8 290 0     0   false(unreach-call) 1 --- inspect .86 .86 21 .39 0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.5  4.5  51 62   77    0      false(unreach-call) 1 wit inspect 8.8 4.7 300 0   0   true -32 --- inspect 17   9.6 510 .62 0   false(unreach-call) 1 --- inspect 6.7 3.7 280 0     0   false(unreach-call) 1 --- inspect .83 .83 21 .39 0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.9  4.9  54 69   79    0      false(unreach-call) 1 wit inspect 7.6 4.0 300 0   0   true -32 --- inspect 15   8.5 470 .62 0   false(unreach-call) 1 --- inspect 6.5 3.6 280 0     0   false(unreach-call) 1 --- inspect .85 .85 21 .39 0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.8  7.8  65 93   78    0      false(unreach-call) 1 wit inspect 7.5 4.0 300 0   0   true -32 --- inspect 16   9.3 500 .62 0   false(unreach-call) 1 --- inspect 7.1 3.9 290 0     0   false(unreach-call) 1 --- inspect .85 .85 21 .39 0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8  8.8  70 120   92    0      false(unreach-call) 1 wit inspect 9.5 5.1 300 0   0   true -32 --- inspect 16   9.3 470 .62 0   false(unreach-call) 1 --- inspect 7.4 4.1 280 0     0   false(unreach-call) 1 --- inspect .89 .89 21 .40 0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 120    120    380 1600   88    0      true -32 wit inspect 6.5 3.5 280 0   0   true -32 --- inspect 17   9.7 510 .62 0   false(unreach-call) 1 --- inspect 7.3 4.0 290 0     0   false(unreach-call) 1 --- inspect .89 .89 21 .43 0     - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.9  3.8  47 50   92    0      false(unreach-call) 1 wit inspect 8.3 4.4 300 0   0   true -32 --- inspect 16   9.2 470 .62 0   false(unreach-call) 1 --- inspect 6.4 3.6 280 0     0   false(unreach-call) 1 --- inspect .84 .84 21 .37 0     - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.5  6.5  60 92   90    0      false(unreach-call) 1 wit inspect 8.5 4.5 290 0   0   true -32 --- inspect 16   9.2 460 .62 0   false(unreach-call) 1 --- inspect 6.4 3.5 270 0     0   false(unreach-call) 1 --- inspect .83 .83 21 .38 .066 - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.5  4.5  52 55   92    0      false(unreach-call) 1 wit inspect 8.2 4.4 290 0   0   true -32 --- inspect 14   8.1 480 .62 0   false(unreach-call) 1 --- inspect 6.4 3.6 270 0     0   false(unreach-call) 1 --- inspect .83 .83 20 .37 0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.3  8.3  67 110   92    0      false(unreach-call) 1 wit inspect 7.3 3.9 290 0   0   true -32 --- inspect 15   8.4 470 .66 0   false(unreach-call) 1 --- inspect 6.1 3.3 280 0     0   false(unreach-call) 1 --- inspect .84 .85 20 .39 0     - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.2  4.2  49 48   78    0      false(unreach-call) 1 wit inspect 7.7 4.1 300 0   0   true -32 --- inspect 15   8.9 500 .62 0   false(unreach-call) 1 --- inspect 6.7 3.7 280 0     0   false(unreach-call) 1 --- inspect .84 .84 21 .39 0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.2  7.2  64 100   92    0      false(unreach-call) 1 wit inspect 9.4 5.0 300 0   0   true -32 --- inspect 14   8.2 460 .62 0   false(unreach-call) 1 --- inspect 8.0 4.4 270 0     0   false(unreach-call) 1 --- inspect .84 .84 21 .39 0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.8  4.8  53 60   79    0      false(unreach-call) 1 wit inspect 7.7 4.2 300 0   0   true -32 --- inspect 15   8.9 500 .62 0   false(unreach-call) 1 --- inspect 6.4 3.5 280 0     0   false(unreach-call) 1 --- inspect .84 .84 21 .39 0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.0  9.0  70 140   92    0      false(unreach-call) 1 wit inspect 8.9 4.7 300 0   0   true -32 --- inspect 16   9.3 470 .62 0   false(unreach-call) 1 --- inspect 6.1 3.4 280 0     0   false(unreach-call) 1 --- inspect .85 .85 20 .40 0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130    130    420 1600   92    0      true -32 wit inspect 6.7 3.5 290 0   0   true -32 --- inspect 16   9.2 520 .62 0   false(unreach-call) 1 --- inspect 7.0 3.9 290 0     0   false(unreach-call) 1 --- inspect .88 .88 21 .43 0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.8  2.8  48 34   52    0      true -32 wit inspect 6.9 3.7 280 0   0   true -32 --- inspect 15   8.3 470 .62 0   false(unreach-call) 1 --- inspect 6.9 3.8 280 0     0   false(unreach-call) 1 --- inspect .86 .86 21 .37 0     - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.5  2.5  46 37   62    0      true -32 wit inspect 7.2 3.9 270 0   0   true -32 --- inspect 15   8.7 460 .62 0   false(unreach-call) 1 --- inspect 6.6 3.6 280 0     0   false(unreach-call) 1 --- inspect .84 .84 21 .37 0     - --- inspect - --- inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.6  2.6  46 32   62    0