Tool 2LS 0.7.2-sv-comp19 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*
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-04 22:44:17 CET 2018-12-06 09:36:46 CET 2018-12-06 10:26:50 CET 2018-12-06 10:31:50 CET 2018-12-12 19:28:33 CET 2018-12-06 06:59:33 CET 2018-12-06 09:46:05 CET
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options --graphml-witness witness.graphml -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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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 5.7  5.7  1200 67    0      0      true -32 wit inspect 14   7.3 450 0   0   true -32 --- inspect 16   9.2 540 .62 0   false(unreach-call) 1 --- inspect 22   13   1200 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .44 0     - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.9  9.9  2000 110    0      0      true -32 wit inspect 16   8.5 510 0   0   true -32 --- inspect 15   8.7 470 .62 0   false(unreach-call) 1 --- inspect 24   15   1300 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .47 0     - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.0  6.0  1300 76    0      0      true -32 wit inspect 15   7.7 460 0   0   true -32 --- inspect 17   9.4 530 .62 0   false(unreach-call) 1 --- inspect 23   14   1200 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .44 0     - --- inspect - --- inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11    11    2100 100    0      0      true -32 wit inspect 16   8.5 500 0   0   true -32 --- inspect 19   11   470 .62 0   false(unreach-call) 1 --- inspect 24   15   1400 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .47 0     - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 36    36    7000 390    0      0      true -32 wit inspect 9.6 5.0 300 0   0   true -32 --- inspect 18   11   540 .62 0   false(unreach-call) 1 --- inspect 38   24   1600 0     0    false(unreach-call) 1 --- inspect 1.2  1.2  23 .52 0     - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 41    41    840 330    0      0      true -32 wit inspect 11   5.7 340 0   0   true -32 --- inspect 17   9.6 470 .62 0   unknown 0 --- inspect 14   7.4 570 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .45 0     - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 45    45    900 380    0      0      true -32 wit inspect 11   5.9 330 0   0   true -32 --- inspect 16   9.6 530 .62 0   unknown 0 --- inspect 19   10   820 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .47 0     - --- inspect - --- inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 55    55    1200 520    0      0      true -32 wit inspect 8.9 4.7 350 0   0   true -32 --- inspect 15   8.9 540 .62 0   unknown 0 --- inspect 16   8.6 630 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .48 0     - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 58    58    1300 490    0      0      true -32 wit inspect 11   5.8 360 0   0   true -32 --- inspect 15   8.7 520 .62 0   unknown 0 --- inspect 23   12   910 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  23 .50 0     - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 47    47    900 410    0      0      true -32 wit inspect 11   5.8 340 0   0   true -32 --- inspect 16   9.3 530 .62 0   unknown 0 --- inspect 14   7.3 580 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .45 0     - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 52    52    950 410    0      0      true -32 wit inspect 11   5.5 350 0   0   true -32 --- inspect 17   9.9 520 .62 0   unknown 0 --- inspect 19   10   770 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  23 .48 .074 - --- inspect - --- inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 64    64    1200 560    0      0      true -32 wit inspect 11   5.6 350 0   0   true -32 --- inspect 18   10   470 .62 0   unknown 0 --- inspect 15   8.0 620 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .49 0     - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 65    64    1300 530    0      0      true -32 wit inspect 9.0 4.7 360 0   0   true -32 --- inspect 17   9.5 530 .62 0   unknown 0 --- inspect 20   11   920 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  23 .51 0     - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 160    160    3700 1400    0      0      true -32 wit inspect 9.3 4.9 300 0   0   true -32 --- inspect 22   12   520 .66 0   unknown 0 --- inspect 7.1 3.9 300 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  23 .52 0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 38    38    850 330    0      0      true -32 wit inspect 14   7.1 460 0   0   true -32 --- inspect 16   8.8 520 .62 0   unknown 0 --- inspect 13   6.9 490 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .45 0     - --- inspect - --- inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 41    41    920 350    0      0      true -32 wit inspect 14   7.3 490 0   0   true -32 --- inspect 17   9.7 520 .66 0   unknown 0 --- inspect 15   8.3 680 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .47 0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 49    48    1200 370    0      0      true -32 wit inspect 14   7.4 450 0   0   true -32 --- inspect 17   9.8 530 .62 0   unknown 0 --- inspect 17   8.8 630 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .48 0     - --- inspect - --- inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 56    56    1300 450    0      0      true -32 wit inspect 17   8.6 410 0   0   true -32 --- inspect 15   8.8 530 .62 0   unknown 0 --- inspect 19   10   900 0     0    false(unreach-call) 1 --- inspect 1.2  1.1  23 .50 .078 - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 38    38    900 360    0      0      true -32 wit inspect 13   6.9 420 0   0   true -32 --- inspect 17   9.9 510 .62 0   unknown 0 --- inspect 13   6.9 500 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .32 0     - --- inspect - --- inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 41    41    970 390    0      0      true -32 wit inspect 13   6.8 490 0   0   true -32 --- inspect 16   9.2 470 .62 0   unknown 0 --- inspect 17   9.0 800 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .47 .074 - --- inspect - --- inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 55    55    1300 450    0      0      true -32 wit inspect 13   6.8 460 0   0   true -32 --- inspect 16   9.5 510 .62 0   unknown 0 --- inspect 16   8.1 630 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .48 0     - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 58    58    1300 490    0      0      true -32 wit inspect 17   8.9 520 0   0   true -32 --- inspect 16   9.5 470 .62 0   unknown 0 --- inspect 19   10   900 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  23 .50 0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130    130    3800 1000    0      0      true -32 wit inspect 8.2 4.3 300 0   0   true -32 --- inspect 18   10   520 .62 0   unknown 0 --- inspect 18   10   880 0     0    false(unreach-call) 1 --- inspect 1.2  1.2  23 .54 0     - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.8  2.8  570 35    0      0      true -32 wit inspect 11   5.9 350 0   0   true -32 --- inspect 18   10   470 .62 0   unknown 0 --- inspect 10   5.2 450 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  23 .28 0     - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0  3.0  610 28    0      0      true -32 wit inspect 11   5.7 370 0   0   true -32 --- inspect 15   9.0 520 .62 0   unknown 0 --- inspect 11   5.7 450 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  24 .45 .074 - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.2  3.2  650 34    0      0      true -32 wit inspect 10   5.4 370 0   0   true -32 --- inspect 15   8.8 530 .66 0   unknown 0 --- inspect 9.7 5.1 460 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  24 .47 .074 - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.4  6.3  1200 64    0      0      true -32 wit inspect 13   6.5 370 0   0   true -32 --- inspect 17   9.9 470 .62 0   unknown 0 --- inspect 9.8 5.2 460 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  24 .47 0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.2  5.2  1000 49    0      0      true -32 wit inspect 10   5.2 380 0   0   true -32 --- inspect 16   9.5 530 .62 0   unknown 0 --- inspect 9.6 5.1 460 0     0    false(unreach-call) 1 --- inspect 1.2  1.2  24 .50 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10    10    2000 120    0      0      true -32 wit inspect 10   5.3 400 0   0   true -32 --- inspect 17   9.7 530 .62 0   unknown 0 --- inspect 10   5.3 460 0     0    false(unreach-call) 1 --- inspect 1.2  1.2  24 .50 0     - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.2  3.2  690 34    0      0      true -32 wit inspect 12   6.2 370 0   0   true -32 --- inspect 16   8.8 520 .62 0   unknown 0 --- inspect 10   5.3 460 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  23 .47 0     - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.4  6.4  1300 61    0      0      true -32 wit inspect 12   6.3 370 0   0   true -32 --- inspect 19   11   470 .62 0   unknown 0 --- inspect 9.9 5.2 460 0     0    false(unreach-call) 1 --- inspect 1.2  1.2  24 .48 0     - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.7  5.7  1100 58    0      0      true -32 wit inspect 12   6.3 390 0   0   true -32 --- inspect 15   8.8 520 .62 0   unknown 0 --- inspect 10   5.4 460 0     0    false(unreach-call) 1 --- inspect 1.2  1.2  24 .50 0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11    11    2100 130    0      0      true -32 wit inspect 9.6 5.0 380 0   0   true -32 --- inspect 17   9.7 520 .62 0   unknown 0 --- inspect 10   5.3 460 0     0    false(unreach-call) 1 --- inspect 1.2  1.2  24 .50 0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 41    41    7000 360    0      0      true -32 wit inspect 8.3 4.3 300 0   0   true -32 --- inspect 18   11   520 .66 0   unknown 0 --- inspect 7.4 3.9 300 0     0    true -32 --- inspect 1.2  1.2  24 .52 0     - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 38    38    900 370    0      0      true -32 wit inspect 12   6.2 460 0   0   true -32 --- inspect 16   9.2 470 .62 0   unknown 0 --- inspect 15   7.9 580 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .46 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 40    40    960 390    0      0      true -32 wit inspect 16   8.2 500 0   0   true -32 --- inspect 17   9.8 510 .62 0   unknown 0 --- inspect 17   9.6 810 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  23 .48 .074 - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 53    53    1200 440    0      0      true -32 wit inspect 13   6.6 470 0   0   true -32 --- inspect 16   9.3 520 .62 0   unknown 0 --- inspect 17   8.8 630 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  23 .49 0     - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 53    53    1300 420    0      0      true -32 wit inspect 18   9.1 540 0   0   true -32 --- inspect 19   11   460 .62 0   unknown 0 --- inspect 19   11   1100 0     0    false(unreach-call) 1 --- inspect 1.2  1.2  23 .51 .078 - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 120    120    3700 1000    0      0      true -32 wit inspect 8.6 4.5 300 0   0   true -32 --- inspect 17   9.3 530 .62 0   unknown 0 --- inspect 7.2 3.9 300 0     0    false(unreach-call) 1 --- inspect 1.2  1.1  23 .52 0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c error (5) 0 --- inspect 5.0  5.0  1000 56    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0     0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c error (5) 0 --- inspect 10    10    1900 95    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0     0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c error (5) 0 --- inspect 5.5  5.5  1100 67    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0   error (2) 0 --- inspect .026 .028 5.6 0     0    
elevator_spec13_product24_true-unreach-call_false-termination.cil.c error (5) 0 --- inspect 11    11    2100 140    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .42 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0     0    
elevator_spec13_product29_true-unreach-call_false-termination.cil.c error (5) 0 --- inspect 5.5  5.5  1100 48    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0     0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c error (5) 0 --- inspect 11    11    2000 98    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 41 0   0   error (2) 0 --- inspect .022 .023 5.7 0     0    
elevator_spec13_product31_true-unreach-call_false-termination.cil.c error (5) 0 --- inspect 5.8  5.8  1200 55    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 41 0   0   error (2) 0 --- inspect .020 .021 5.5 0     0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c error (5) 0 --- inspect 12    12    2200 100    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0     0    
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c error (5) 0 --- inspect 48    48    7300 400    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0     0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 21    21    930 220    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 26    14    950 0   0   out of memory 0 --- inspect 260     180     7000   .41  0    
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 21    21    990 180    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    18    1200 0   0   out of memory 0 --- inspect 260     190     7000   .63  0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 23    23    1000 240    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 26    14    1300 0   0   out of memory 0 --- inspect 260     180     7000   .62  0    
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 23    23    1700 160    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 43    25    1800 0   0   out of memory 0 --- inspect 220     150     7000   .63  0    
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 24    24    1100 230    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    17    1400 0   0   out of memory 0 --- inspect 270     190     7000   .62  0    
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 23    23    1800 220    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 44    25    1800 0   0   out of memory 0 --- inspect 240     160     7000   .63  0    
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 27    27    990 300    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 88    71    2000 0   0   out of memory 0 --- inspect 250     170     7000   .62  0    
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 27    27    1000 310    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 100    83    2100 0   0   out of memory 0 --- inspect 260     180     7000   .63  0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 28    28    1000 270    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 89    72    2100 0   0   out of memory 0 --- inspect 240     170     7000   .63  0    
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 29    29    1100 270    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    96    2100 0   0   out of memory 0 --- inspect 260     180     7000   .92  0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 29    29    1100 270    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    88    2100 0   0   out of memory 0 --- inspect 280     200     7000   .65  0    
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 30    30    1100 260    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 100    85    2300 0   0   out of memory 0 --- inspect 260     180     7000   .64  .033
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 41    41    1500 360    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 180    160    3000 0   0   out of memory 0 --- inspect 250     170     7000   .65  0    
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 39    39    1600 380    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 200    170    2900 0   0   out of memory 0 --- inspect 280     200     7000   .62  0    
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 30    30    1100 310    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 100    86    2200 0   0   out of memory 0 --- inspect 270     190     7000   .63  0    
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 31    31    1200 330    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 120    110    2400 0   0   out of memory 0 --- inspect 270     190     7000   .64  0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 41    41    1600 350    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 350    330    2900 0   0   out of memory 0 --- inspect 270     180     7000   .63  0    
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 42    42    1600 380    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 200    180    3000 0   0   out of memory 0 --- inspect 270     190     7000   .64  0    
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 19    19    710 190    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 42    27    1300 0   0   out of memory 0 --- inspect 160     110     7000   .65  0    
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 21    21    760 270    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 42    27    1400 0   0   out of memory 0 --- inspect 200     130     7000   .63  .049
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    22    750 220    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    25    1500 0   0   out of memory 0 --- inspect 160     100     7000   .64  0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    22    790 200    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 48    32    1500 0   0   out of memory 0 --- inspect 210     140     7000   .63  0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 23    23    780 240    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 44    29    1500 0   0   out of memory 0 --- inspect 150     100     7000   .63  0    
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 24    24    820 230    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 43    29    1700 0   0   out of memory 0 --- inspect 200     130     7000   .64  0    
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 29    29    1100 270    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 58    42    1700 0   0   out of memory 0 --- inspect 180     120     7000   .64  0    
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 31    31    1100 310    0      .13   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 58    43    1900 0   0   out of memory 0 --- inspect 220     150     7000   .65  .029
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 25    25    820 210    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 43    29    1500 0   0   out of memory 0 --- inspect 190     130     7000   .64  0    
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 23    23    860 290    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 52    37    1800 0   0   out of memory 0 --- inspect 200     130     7000   .63  .033
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 34    34    1100 250    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 79    60    1900 0   0   out of memory 0 --- inspect 250     170     7000   .64  0    
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 30    30    1200 340    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 69    50    2000 0   0   out of memory 0 --- inspect 220     150     7000   .64  0    
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.9  2.9  630 30    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    15    850 0   0   out of memory 0 --- inspect 160     100     7000   .97  0    
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.0  3.0  680 34    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    15    890 0   0   out of memory 0 --- inspect 150     100     7000   .65  0    
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.2  3.2  720 33    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    16    970 0   0   out of memory 0 --- inspect 200     130     7000   1.0   0    
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.2  6.2  1400 61    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    19    1500 0   0   out of memory 0 --- inspect 200     130     7000   .63  0    
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.5  5.5  1200 55    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 34    18    1400 0   0   out of memory 0 --- inspect 210     140     7000   .63  .029
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 11    11    2300 100    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 51    28    1800 0   0   out of memory 0 --- inspect 220     160     7000   .63  0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.4  3.4  770 39    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    15    940 0   0   out of memory 0 --- inspect 140     94     7000   .64  0    
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.6  6.6  1500 81    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    21    1600 0   0   out of memory 0 --- inspect 230     150     7000   .64  0    
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.5  5.5  1200 69    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    19    1400 0   0   out of memory 0 --- inspect 230     160     7000   .64  0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 11    11    2400 110    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 48    27    1700 0   0   out of memory 0 --- inspect 220     150     7000   .67  0    
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 21    21    740 210    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    26    1300 0   0   out of memory 0 --- inspect 160     110     7000   .65  0    
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    22    790 220    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 45    31    1400 0   0   out of memory 0 --- inspect 180     120     7000   .63  0    
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 24    24    810 170    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    28    1500 0   0   out of memory 0 --- inspect 190     130     7000   .64  0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 25    25    860 210    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 52    36    1700 0   0   out of memory 0 --- inspect 170     110     7000   .65  0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 29    29    1100 260    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 82    66    1900 0   0   out of memory 0 --- inspect 180     120     7000   .63  0    
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 31    31    1200 310    0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 72    55    2000 0   0   out of memory 0 --- inspect 170     110     7000   .63  0    
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 24    24    310 330    .0082 0      true -32 wit inspect 12   6.4 460 0   0   unknown 0 --- inspect 63   44   1300 .68 0   unknown 0 --- inspect 8.4 4.5 370 0     0    true -32 --- inspect 1.1  1.1  22 .48 0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 43    43    510 410    .0082 0      true -32 wit inspect 17   8.9 720 0   0   unknown 0 --- inspect 83   57   1300 .68 0   unknown 0 --- inspect 8.8 4.7 410 0     0    true -32 --- inspect 1.1  1.1  22 .49 0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 28    28    320 250    .0082 0      true -32 wit inspect 14   7.0 440 0   0   unknown 0 --- inspect 75   51   1300 .68 0   unknown 0 --- inspect 8.3 4.5 360 0     0    true -32 --- inspect 1.1  1.1  22 .48 0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 50    50    590 500    .0082 0      true -32 wit inspect 21   11   620 0   0   unknown 0 --- inspect 65   46   1300 .68 0   unknown 0 --- inspect 9.4 5.0 440 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .50 0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 24    24    340 310    .0082 0      true -32 wit inspect 14   7.5 520 0   0   unknown 0 --- inspect 73   52   1400 .68 0   unknown 0 --- inspect 8.7 4.6 440 0     0    true -32 --- inspect 1.1  1.1  22 .51 0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 29    28    360 410    .0082 0      true -32 wit inspect 19   9.7 630 0   0   unknown 0 --- inspect 88   64   1400 .68 0   unknown 0 --- inspect 11   5.9 490 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .52 0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 48    48    640 490    .0082 0      true -32 wit inspect 28   15   1000 0   0   unknown 0 --- inspect 80   59   1500 .68 0   unknown 0 --- inspect 12   6.2 480 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .52 0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 55    55    670 500    .0082 0      true -32 wit inspect 21   11   640 0   0   unknown 0 --- inspect 89   65   1500 .68 0   unknown 0 --- inspect 9.4 5.0 420 0     0    false(unreach-call) 1 --- inspect 1.1  1.2  22 .34 0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 300    300    8000 2000    .0082 0      true -32 wit inspect 7.6 4.0 300 0   0   timeout 0 --- inspect 95   70   1700 .68 0   unknown 0 --- inspect 7.5 4.0 310 0     0    true -32 --- inspect 1.2  1.2  22 .56 .074 - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 26    26    290 280    .0082 0      true -32 wit inspect 14   7.2 430 0   0   unknown 0 --- inspect 60   42   1200 .68 0   unknown 0 --- inspect 8.3 4.5 350 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .49 0     - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 46    46    530 490    .0082 0      true -32 wit inspect 16   8.3 530 0   0   unknown 0 --- inspect 89   62   1300 .68 0   unknown 0 --- inspect 8.3 4.4 420 0     0    true -32 --- inspect 1.1  1.1  22 .50 .066 - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 29    29    330 370    .0082 0      true -32 wit inspect 15   7.6 430 0   0   unknown 0 --- inspect 63   45   1200 .68 0   unknown 0 --- inspect 8.7 4.6 390 0     0    true -32 --- inspect 1.1  1.1  22 .48 .066 - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 51    51    610 510    .0082 0      true -32 wit inspect 24   12   840 0   0   unknown 0 --- inspect 81   59   1300 .68 0   unknown 0 --- inspect 11   5.8 450 0     0    true -32 --- inspect 1.1  1.1  22 .50 .066 - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 27    27    320 310    .0082 0      true -32 wit inspect 15   8.0 460 0   0   unknown 0 --- inspect 73   52   1400 .68 0   unknown 0 --- inspect 8.8 4.6 400 0     0    false(unreach-call) 1 --- inspect 1.1  1.1  22 .50 0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 49    49    560 500    .0082 0      true -32 wit inspect 22   11   580 0   0   unknown 0 --- inspect 80   58   1500 .68 0   unknown 0 --- inspect 9.3 4.9 440 0     0    true -32 --- inspect 1.1  1.1  22 .51 0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 31    31    370 310    .0082 0      true -32 wit inspect 15   7.8 510 0   0   unknown 0 --- inspect 84   59   1400 .68 0   unknown 0 --- inspect 9.0 4.8 440 0     0    true -32 --- inspect 1.1  1.1  22 .50 0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 53    53    690 480    .0082 .23   true -32 wit inspect 24   12   650 0   0   unknown 0 --- inspect 88   65   1500 .68 0   unknown 0 --- inspect 10   5.4 450 0     0    true -32 --- inspect 1.2  1.2  22 .53 .066 - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 470    470    8600 2600    .0082 0      true -32 wit inspect 8.1 4.3 300 0   0   timeout 0 --- inspect 97   71   1800 .72 0   unknown 0 --- inspect 12   6.4 480 0     0    true -32 --- inspect 1.2  1.2  22 .57 0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 35    35    440 450    .0082 .070  true -32 wit inspect 16   8.2 470 0   0   true -32 --- inspect 15   8.8 470 .62 0   unknown 0 --- inspect 9.0 4.8 380 0     0    true -32 --- inspect 1.1  1.1  22 .49 0     - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 25    25    290 260    .0082 0      true -32 wit inspect 14   7.4 530 0   0   true -32 --- inspect 14   8.1 510 .53 0   unknown 0 --- inspect 10   5.3 440 0     0    false(unreach-call) 1 --- inspect 1.1  1.2  22 .50 .066 - --- inspect - --- inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit