Tool CBMC Path 5.10 () 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:45:10 CET 2018-12-06 08:53:36 CET 2018-12-06 10:12:52 CET 2018-12-06 10:22:39 CET 2018-12-12 19:23:37 CET 2018-12-06 07:24:45 CET 2018-12-06 09:28:06 CET
Run set cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-cbmc-path.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/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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 .26  .25  19   2.4  .0082 0      true -32 wit inspect 14    7.4  460 0   0   true -32 --- inspect 15     8.5   540   .66 0   false(unreach-call) 1 --- inspect 19    11    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 .24  .23  19   2.9  .0082 0      true -32 wit inspect 17    8.7  520 0   0   true -32 --- inspect 16     9.3   530   .62 0   false(unreach-call) 1 --- inspect 21    13    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 .23  .22  19   2.3  .0082 0      true -32 wit inspect 16    8.1  460 0   0   true -32 --- inspect 20     11     470   .66 0   false(unreach-call) 1 --- inspect 20    12    1200 0     0     false(unreach-call) 1 --- inspect 1.0    1.0    22    .44  0     - --- inspect - --- inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .24  .23  19   2.7  .0082 0      true -32 wit inspect 14    7.5  510 0   0   true -32 --- inspect 17     9.9   520   .62 0   false(unreach-call) 1 --- inspect 24    14    1300 0     .090 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 13     13     1400   180    8.6    0      true -32 wit inspect 9.6  5.1  300 0   0   true -32 --- inspect 17     9.6   510   .62 0   false(unreach-call) 1 --- inspect 32    19    1600 0     0     false(unreach-call) 1 --- inspect 1.1    1.1    22    .50  0     - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37  .36  19   4.4  .20   0      true -32 wit inspect 8.9  4.7  340 0   0   true -32 --- inspect 17     9.7   460   .66 0   false(unreach-call) 1 --- inspect 18    11    1200 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 .39  .39  19   4.8  .22   0      true -32 wit inspect 12    6.1  350 0   0   true -32 --- inspect 16     9.2   530   .62 0   false(unreach-call) 1 --- inspect 31    18    1500 0     .086 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 .40  .39  19   4.8  .21   0      true -32 wit inspect 11    5.9  350 0   0   true -32 --- inspect 16     9.3   530   .62 0   false(unreach-call) 1 --- inspect 23    14    1300 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 .44  .43  19   4.7  .24   0      true -32 wit inspect 12    6.0  360 0   0   true -32 --- inspect 16     9.3   470   .66 0   false(unreach-call) 1 --- inspect 34    21    1900 0     0     false(unreach-call) 1 --- inspect 1.2    1.1    22    .50  0     - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37  .37  18   5.2  .20   0      true -32 wit inspect 9.9  5.2  340 0   0   true -32 --- inspect 16     9.4   460   .62 0   false(unreach-call) 1 --- inspect 23    14    1300 0     .83  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 .41  .40  19   5.4  .22   0      true -32 wit inspect 11    5.9  350 0   0   true -32 --- inspect 17     9.3   460   .62 0   false(unreach-call) 1 --- inspect 34    20    1600 0     0     false(unreach-call) 1 --- inspect 1.1    1.1    22    .48  0     - --- inspect - --- inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39  .38  19   5.1  .21   0      true -32 wit inspect 9.1  4.7  350 0   0   true -32 --- inspect 16     9.1   470   .66 0   false(unreach-call) 1 --- inspect 23    14    1500 0     .086 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 .42  .41  19   5.8  .24   0      true -32 wit inspect 11    5.6  360 0   0   true -32 --- inspect 19     11     520   .62 0   false(unreach-call) 1 --- inspect 34    21    1800 0     0     false(unreach-call) 1 --- inspect 1.2    1.1    22    .51  0     - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 130     130     15000   1600    120      0      error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .68 47 0     0     error (invalid witness file) 0 --- inspect .0048 .0060 .53 0     0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .35  18   4.2  .19   0      true -32 wit inspect 12    6.3  460 0   0   true -32 --- inspect 18     10     510   .66 0   false(unreach-call) 1 --- inspect 21    12    1200 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 .38  .38  19   5.3  .21   0      true -32 wit inspect 15    7.5  510 0   0   true -32 --- inspect 17     9.7   530   .62 0   false(unreach-call) 1 --- inspect 31    19    1600 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 .39  .38  19   4.3  .20   0      true -32 wit inspect 13    6.5  510 0   0   true -32 --- inspect 18     10     470   .62 0   false(unreach-call) 1 --- inspect 24    14    1400 0     0     false(unreach-call) 1 --- inspect 1.1    1.1    22    .48  .074 - --- inspect - --- inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41  .40  19   4.7  .23   0      true -32 wit inspect 17    8.9  530 0   0   true -32 --- inspect 15     8.6   520   .66 0   false(unreach-call) 1 --- inspect 35    22    1800 0     0     false(unreach-call) 1 --- inspect 1.2    1.1    22    .50  0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40  .39  19   4.3  .19   0      true -32 wit inspect 11    5.8  450 0   0   true -32 --- inspect 16     9.5   470   .66 0   false(unreach-call) 1 --- inspect 21    13    1200 0     0     false(unreach-call) 1 --- inspect 1.1    1.1    22    .45  0     - --- inspect - --- inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38  .37  19   4.9  .21   0      true -32 wit inspect 15    7.8  500 0   0   true -32 --- inspect 18     11     470   .62 0   false(unreach-call) 1 --- inspect 26    16    1500 0     0     false(unreach-call) 1 --- inspect 1.1    1.1    22    .47  0     - --- inspect - --- inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40  .39  19   4.7  .20   0      true -32 wit inspect 14    7.1  510 0   0   true -32 --- inspect 16     9.2   470   .62 0   false(unreach-call) 1 --- inspect 30    18    1600 0     0     false(unreach-call) 1 --- inspect 1.1    1.1    22    .48  .045 - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43  .42  19   5.2  .23   0      true -32 wit inspect 17    8.9  520 0   0   true -32 --- inspect 18     10     470   .66 0   false(unreach-call) 1 --- inspect 33    21    1900 0     0     false(unreach-call) 1 --- inspect 1.2    1.2    22    .50  .078 - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 130     130     15000   1800    120      0      error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .59 46 0     0     error (invalid witness file) 0 --- inspect .0049 .0061 .53 0     0     - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .35  19   3.6  .0082 0      true -32 wit inspect 11    6.0  360 0   0   true -32 --- inspect 15     8.7   470   .66 0   false(unreach-call) 1 --- inspect 34    21    1900 0     1.2   false(unreach-call) 1 --- inspect 1.1    1.1    23    .45  .074 - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .32  .31  19   3.5  .0082 0      true -32 wit inspect 12    6.0  360 0   0   true -32 --- inspect 17     9.7   530   .62 0   false(unreach-call) 1 --- inspect 41    24    1800 0     0     false(unreach-call) 1 --- inspect 1.1    1.1    23    .45  0     - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .34  .33  19   3.7  .0082 0      true -32 wit inspect 11    5.6  360 0   0   true -32 --- inspect 16     9.1   550   .62 0   false(unreach-call) 1 --- inspect 41    26    1800 0     4.8   false(unreach-call) 1 --- inspect 1.1    1.1    23    .47  0     - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .33  .32  19   3.5  .0082 0      true -32 wit inspect 9.9  5.1  370 0   0   true -32 --- inspect 18     10     520   .62 0   false(unreach-call) 1 --- inspect 38    24    1800 0     0     false(unreach-call) 1 --- inspect 1.1    1.2    23    .47  .074 - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .33  .32  20   4.4  .0082 0      true -32 wit inspect 11    5.9  390 0   0   true -32 --- inspect 19     10     470   .62 0   false(unreach-call) 1 --- inspect 41    27    1900 0     4.9   false(unreach-call) 1 --- inspect 1.2    1.2    23    .50  .078 - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .34  .33  20   3.7  .0082 0      true -32 wit inspect 10    5.3  390 0   0   true -32 --- inspect 19     11     470   .66 0   false(unreach-call) 1 --- inspect 38    24    1800 0     .35  false(unreach-call) 1 --- inspect 1.2    1.2    23    .50  0     - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .33  .32  20   3.5  .0082 0      true -32 wit inspect 8.8  4.6  370 0   0   true -32 --- inspect 17     9.7   470   .66 0   false(unreach-call) 1 --- inspect 36    23    1800 0     0     false(unreach-call) 1 --- inspect 1.1    1.1    23    .47  .16  - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .31  .30  19   4.4  .0082 0      true -32 wit inspect 11    5.6  380 0   0   true -32 --- inspect 17     9.9   460   .66 0   false(unreach-call) 1 --- inspect 38    24    2000 0     .086 false(unreach-call) 1 --- inspect 1.1    1.1    23    .48  0     - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .33  .32  19   3.7  .0082 0      true -32 wit inspect 9.3  4.9  380 0   0   true -32 --- inspect 16     8.9   530   .66 0   false(unreach-call) 1 --- inspect 38    24    2100 0     0     false(unreach-call) 1 --- inspect 1.2    1.2    23    .50  0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .35  .34  20   3.9  .0082 0      true -32 wit inspect 13    6.6  390 0   0   true -32 --- inspect 24     13     470   .62 0   false(unreach-call) 1 --- inspect 46    31    2200 0     0     false(unreach-call) 1 --- inspect 1.2    1.2    23    .50  0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 110     110     15000   1100    .033  0      error (invalid witness file) 0 --- inspect .60 .36 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .64 47 0     0     error (invalid witness file) 0 --- inspect .0062 .0080 .53 0     0     - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38  .37  19   4.6  .20   0      true -32 wit inspect 15    8.0  460 0   0   true -32 --- inspect 20     11     470   .66 0   false(unreach-call) 1 --- inspect 23    14    1300 0     4.7   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 .41  .40  19   5.0  .23   0      true -32 wit inspect 15    7.7  510 0   0   true -32 --- inspect 16     9.2   520   .66 0   false(unreach-call) 1 --- inspect 35    21    1700 0     .17  false(unreach-call) 1 --- inspect 1.1    1.1    22    .41  0     - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40  .39  19   5.0  .22   0      true -32 wit inspect 15    7.9  470 0   0   true -32 --- inspect 16     9.1   530   .66 0   false(unreach-call) 1 --- inspect 32    19    1700 0     0     false(unreach-call) 1 --- inspect 1.2    1.2    22    .49  .074 - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42  .41  19   4.8  .25   0      true -32 wit inspect 18    9.5  550 0   0   true -32 --- inspect 18     11     540   .62 0   false(unreach-call) 1 --- inspect 50    32    1900 0     0     false(unreach-call) 1 --- inspect 1.2    1.2    22    .51  0     - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 130     130     15000   1600    130      .0041 error (invalid witness file) 0 --- inspect .74 .46 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .63 47 0     0     error (invalid witness file) 0 --- inspect .0064 .0089 .53 0     0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 270     270     15000   4500    6.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0     
elevator_spec13_product22_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 270     270     15000   3500    6.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 40 0   0   error (2) 0 --- inspect .028 .028 5.6 0    0     
elevator_spec13_product23_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 240     240     15000   3400    3.3    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     
elevator_spec13_product24_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 240     240     15000   3700    3.3    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     
elevator_spec13_product29_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 280     280     15000   3700    6.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0     
elevator_spec13_product30_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 280     280     15000   3700    6.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0     
elevator_spec13_product31_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 240     240     15000   3500    3.3    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .46 42 0   0   error (2) 0 --- inspect .024 .026 5.6 0    0     
elevator_spec13_product32_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 240     240     15000   3600    3.3    .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0     
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 130     130     15000   1600    .025  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0     
elevator_spec14_product03_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .87  .87  19   10    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 43 0   0   error (invalid witness file) 0 --- inspect 5.4   3.2   260   .65 0     
elevator_spec14_product11_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .87  .87  19   12    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 42 0   0   error (invalid witness file) 0 --- inspect 6.5   3.7   270   .61 0     
elevator_spec14_product19_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .88  .88  19   12    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 42 0   0   error (invalid witness file) 0 --- inspect 7.1   4.0   260   .65 0     
elevator_spec14_product23_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .97  .97  20   13    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 43 0   0   error (invalid witness file) 0 --- inspect 5.5   3.5   270   .62 0     
elevator_spec14_product27_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .88  .88  19   12    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .49 43 0   0   error (invalid witness file) 0 --- inspect 5.7   3.5   270   .66 0     
elevator_spec14_product31_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .99  .99  20   12    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 43 0   0   error (invalid witness file) 0 --- inspect 5.3   3.4   260   .62 0     
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect .65  .65  18   9.4  .016  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 70    43    3000 0   0   out of memory 0 --- inspect 270     190     7000   1.4  0     
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect .74  .73  19   10    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 180    120    5300 0   0   out of memory 0 --- inspect 330     230     7000   .65 0     
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect .68  .67  18   8.7  .016  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 110    85    4100 0   0   out of memory 0 --- inspect 270     190     7000   .71 0     
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect .74  .74  19   10    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 180    110    5200 0   0   out of memory 0 --- inspect 290     200     7000   .63 0     
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect .67  .67  18   8.3  .016  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 99    70    4000 0   0   out of memory 0 --- inspect 250     180     7000   .63 0     
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect .77  .77  19   10    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 380    250    5800 0   0   out of memory 0 --- inspect 360     260     7000   .63 0     
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect .75  .74  19   9.1  .016  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 300    230    7000 0   0   out of memory 0 --- inspect 240     170     7000   .70 .086 
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect .83  .82  20   11    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 380     270     7000   .63 .0082
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect .67  .67  19   9.3  .016  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 130    93    4300 0   0   out of memory 0 --- inspect 330     230     7000   .72 0     
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect .84  .83  19   8.3  .016  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 500    320    5900 0   0   out of memory 0 --- inspect 310     220     7000   .65 .0082
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect .77  .77  19   10    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 230    180    7000 0   0   out of memory 0 --- inspect 260     180     7000   .64 0     
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect .84  .84  20   11    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 260     180     7000   .64 0     
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect .36  .36  19   4.2  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 91    64    4000 0   0   out of memory 0 --- inspect 180     120     7000   1.5  0     
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect .37  .37  19   4.3  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 560    370    7000 0   0   out of memory 0 --- inspect 220     150     7000   .64 0     
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect .35  .35  19   4.4  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 69    42    3400 0   0   out of memory 0 --- inspect 200     130     7000   .68 0     
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect .38  .38  19   4.2  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 580    380    7000 0   0   out of memory 0 --- inspect 200     130     7000   .85 0     
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect .36  .36  19   4.3  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 150    100    4800 0   0   out of memory 0 --- inspect 180     120     7000   .65 0     
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect .40  .39  19   5.5  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 760    470    7000 0   0   out of memory 0 --- inspect 210     140     7000   .64 0     
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect .37  .37  19   5.1  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 240    190    6900 0   0   out of memory 0 --- inspect 250     160     7000   .66 0     
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect .41  .40  19   5.2  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 250     170     7000   .63 0     
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect .35  .35  18   4.2  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 120    70    3900 0   0   out of memory 0 --- inspect 190     130     7000   .72 0     
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect .40  .39  19   4.7  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    510    5500 0   0   out of memory 0 --- inspect 230     150     7000   .71 0     
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect .39  .39  19   4.5  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 160    98    4600 0   0   out of memory 0 --- inspect 160     100     7000   .73 .029 
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect .40  .40  19   4.8  .012  .0041 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 900    480    5500 0   0   out of memory 0 --- inspect 260     180     7000   .71 0     
elevator_spec3_product01_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .90  .90  19   11    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 43 0   0   error (invalid witness file) 0 --- inspect 5.3   3.2   270   .61 0     
elevator_spec3_product09_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .90  .90  19   11    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 42 0   0   error (invalid witness file) 0 --- inspect 6.1   3.3   270   .61 0     
elevator_spec3_product17_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .91  .91  20   11    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 43 0   0   error (invalid witness file) 0 --- inspect 6.2   3.7   270   .66 0     
elevator_spec3_product18_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .92  .92  20   12    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0   error (invalid witness file) 0 --- inspect 7.0   3.8   270   .61 0     
elevator_spec3_product21_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect 1.0   1.0   21   12    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .48 42 0   0   error (invalid witness file) 0 --- inspect 6.8   4.1   270   .62 0     
elevator_spec3_product22_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect 1.1   1.1   21   17    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 42 0   0   error (invalid witness file) 0 --- inspect 6.7   3.8   270   .65 0     
elevator_spec3_product25_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .90  .90  19   13    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 43 0   0   error (invalid witness file) 0 --- inspect 5.4   3.5   270   .62 0     
elevator_spec3_product26_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect .95  .95  20   12    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0   error (invalid witness file) 0 --- inspect 6.0   3.6   270   .62 0     
elevator_spec3_product29_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect 1.0   1.0   21   13    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 43 0   0   error (invalid witness file) 0 --- inspect 5.3   3.3   270   .66 0     
elevator_spec3_product30_true-unreach-call_true-termination.cil.c witness invalid (true) 0 wit inspect 1.1   1.1   21   13    .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 42 0   0   error (invalid witness file) 0 --- inspect 5.2   3.1   260   .10 0     
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect .37  .36  19   4.0  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 160    110    4800 0   0   out of memory 0 --- inspect 210     130     7000   1.5  0     
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect .40  .40  19   4.1  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 500    290    5500 0   0   out of memory 0 --- inspect 240     160     7000   .21 3.6   
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect .40  .39  19   4.2  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 240    190    7000 0   0   out of memory 0 --- inspect 200     140     7000   .97 0     
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect .39  .39  19   4.5  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 190     130     7000   .64 0     
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect .37  .37  19   4.4  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 300    230    7000 0   0   out of memory 0 --- inspect 250     170     7000   .64 0     
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect .42  .42  19   4.6  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 940    490    5500 0   0   out of memory 0 --- inspect 230     150     7000   .71 0     
email_spec0_product16_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 220     220     15000   2400    62      0      error (invalid witness file) 0 --- inspect .73 .45 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 47 0     0     error (invalid witness file) 0 --- inspect .0022 .0027 .53 0     0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 360     360     15000   3600    56      .0041 error (invalid witness file) 0 --- inspect .76 .45 42 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .61 47 0     0     error (invalid witness file) 0 --- inspect .0057 .0068 .53 0     0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 230     230     15000   2500    47      0      error (invalid witness file) 0 --- inspect .69 .41 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .64 47 0     0     error (invalid witness file) 0 --- inspect .0051 .0064 .53 0     0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 410     410     15000   5000    43      .0041 error (invalid witness file) 0 --- inspect .90 .54 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .64 48 0     0     error (invalid witness file) 0 --- inspect .0063 .0085 .52 0     0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 230     230     15000   2700    61      0      error (invalid witness file) 0 --- inspect .74 .46 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 47 0     0     error (invalid witness file) 0 --- inspect .0057 .0074 .52 0     0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 250     250     15000   2800    41      0      error (invalid witness file) 0 --- inspect .83 .49 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .64 47 0     0     error (invalid witness file) 0 --- inspect .0021 .0026 .54 0     0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 400     400     15000   4900    58      0      error (invalid witness file) 0 --- inspect .66 .41 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .64 48 0     0     error (invalid witness file) 0 --- inspect .0038 .0048 .53 0     0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 470     470     15000   4600    33      0      error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .026 .028 5.8 0    0   error (invalid witness file) 0 --- inspect .98 .63 47 0     0     error (invalid witness file) 0 --- inspect .0047 .0058 .52 0     0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 85     85     15000   1200    .037  0      error (invalid witness file) 0 --- inspect .85 .52 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .64 47 0     0     error (invalid witness file) 0 --- inspect .0051 .0066 .52 0     0     - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 52     52     700   630    .23   0      unknown 0 wit inspect 8.3  4.4  290 0   0   unknown 0 --- inspect 72     49     1300   .68 0   unknown 0 --- inspect 8.0  4.4  330 0     .012 error (2) 0 --- inspect 1.0    1.0    21    .094 0     - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 170     170     4500   2200    .24   0      unknown 0 wit inspect 7.6  4.0  290 0   0   unknown 0 --- inspect 76     54     1400   .68 0   unknown 0 --- inspect 8.5  4.6  370 0     4.6   error (2) 0 --- inspect 1.0    1.0    21    .098 0     - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 83     83     1300   850    .23   0      unknown 0 wit inspect 7.3  3.8  300 0   0   unknown 0 --- inspect 66     47     1200   .71 0   unknown 0 --- inspect 8.6  4.7  360 0     4.4   error (2) 0 --- inspect 1.0    .99   21    .094 0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 260     260     4900   2600    .24   0      unknown 0 wit inspect 8.7  4.6  290 0   0   unknown 0 --- inspect 81     59     1300   .71 0   unknown 0 --- inspect 10    5.5  440 0     0     error (2) 0 --- inspect 1.0    1.0    22    .098 0     - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 63     63     790   650    .24   0      unknown 0 wit inspect 7.8  4.1  260 0   0   unknown 0 --- inspect 77     56     1400   .71 0   unknown 0 --- inspect 8.5  4.6  360 0     0     error (2) 0 --- inspect 1.0    1.0    22    .098 0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 210     210     5200   2100    .25   0      unknown 0 wit inspect 8.9  4.7  260 0   0   timeout 0 --- inspect 94     69     1500   .68 0   unknown 0 --- inspect 8.8  4.8  410 0     0     error (2) 0 --- inspect 1.0    1.0    22    .098 0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 98     98     1500   1000    .25   0      unknown 0 wit inspect 8.5  4.5  290 0   0   unknown 0 --- inspect 89     63     1400   .68 0   unknown 0 --- inspect 8.7  4.7  350 0     4.5   error (2) 0 --- inspect 1.0    1.0    22    .098 0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 320     320     5600   3000    .25   0      unknown 0 wit inspect 8.0  4.3  290 0   0   unknown 0 --- inspect 90     66     1500   .68 0   unknown 0 --- inspect 8.6  4.7  410 0     .012 error (2) 0 --- inspect 1.0    1.0    22    .098 0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 87     87     15000   1300    .037  0      error (invalid witness file) 0 --- inspect .62 .39 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .71 49 0     0     error (invalid witness file) 0 --- inspect .0052 .0069 .52 0     0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 420     420     15000   3900    62      0      error (invalid witness file) 0 --- inspect .81 .48 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 48 0     0     error (invalid witness file) 0 --- inspect .0056 .0070 .52 0     0     - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c out of memory 0 --- inspect 210     210     15000   2200    29      .0041 error (invalid witness file) 0 --- inspect .67 .40 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .63 47 0     0     error (invalid witness file) 0 --- inspect .0053 .0065 .52 0     0     - --- inspect - ---