Tool CBMC 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:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-06 10:22:39 CET 2018-12-12 19:29:48 CET 2018-12-06 07:35:27 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-cbmc.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.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.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.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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 .20  .19  15   2.4  .0082 0      true -32 wit inspect 16    8.1  530 0   0   true -32 --- inspect 16     9.1   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_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .22  .21  15   2.7  .0082 0      true -32 wit inspect 18    9.3  550 0   0   true -32 --- inspect 18     10     530   .66 0   false(unreach-call) 1 --- inspect 29    17    1500 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    22    .47  .074 - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .21  .20  15   2.4  .0082 0      true -32 wit inspect 18    9.3  540 0   0   true -32 --- inspect 17     9.2   530   .66 0   false(unreach-call) 1 --- inspect 21    13    1100 0   .086  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 .22  .21  15   2.4  .0082 0      true -32 wit inspect 19    9.8  540 0   0   true -32 --- inspect 18     10     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_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13     13     360   170    .0082 0      true -32 wit inspect 19    9.6  650 0   0   true -32 --- inspect 18     10     540   .66 0   false(unreach-call) 1 --- inspect 36    23    1600 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    22    .52  0     - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38  .37  15   4.6  .20   0      true -32 wit inspect 15    7.8  500 0   0   true -32 --- inspect 15     8.5   530   .62 0   false(unreach-call) 1 --- inspect 21    13    1200 0   0      false(unreach-call) 1 --- inspect 1.1    1.2    22    .29  .074 - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39  .38  16   4.9  .22   0      true -32 wit inspect 17    8.7  600 0   0   true -32 --- inspect 16     9.0   480   .66 0   false(unreach-call) 1 --- inspect 35    22    1700 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 .36  .35  15   4.5  .21   0      true -32 wit inspect 15    7.7  540 0   0   true -32 --- inspect 18     10     530   .66 0   false(unreach-call) 1 --- inspect 23    14    1300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    22    .48  .074 - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38  .37  15   5.3  .24   0      true -32 wit inspect 21    11    600 0   0   true -32 --- inspect 21     12     540   .66 0   false(unreach-call) 1 --- inspect 35    21    1900 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    22    .50  0     - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .35  .34  15   4.1  .20   0      true -32 wit inspect 14    7.1  510 0   0   true -32 --- inspect 17     10     470   .62 0   false(unreach-call) 1 --- inspect 29    17    1700 0   .086  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 .38  .37  15   5.0  .22   0      true -32 wit inspect 16    8.4  600 0   0   true -32 --- inspect 17     9.2   530   .62 0   false(unreach-call) 1 --- inspect 31    18    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 .36  .35  15   4.3  .21   0      true -32 wit inspect 20    10    530 0   0   true -32 --- inspect 15     9.1   530   .66 0   false(unreach-call) 1 --- inspect 24    15    1500 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 .43  .42  16   4.8  .24   0      true -32 wit inspect 18    9.1  620 0   0   true -32 --- inspect 17     9.7   530   .66 0   false(unreach-call) 1 --- inspect 35    22    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 false(unreach-call) 1 wit inspect 130     130     960   1100    .26   0      true -32 wit inspect 19    9.9  600 0   0   true -32 --- inspect 18     11     470   .66 0   false(unreach-call) 1 --- inspect 35    23    2000 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    22    .55  0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .33  .33  15   3.7  .19   0      true -32 wit inspect 17    9.0  500 0   0   true -32 --- inspect 17     9.8   510   .62 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 .40  .39  15   4.7  .21   0      true -32 wit inspect 19    10    550 0   0   true -32 --- inspect 19     11     530   .62 0   false(unreach-call) 1 --- inspect 34    20    1700 0   0      false(unreach-call) 1 --- inspect 1.1    1.2    22    .47  0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .35  .34  15   4.5  .20   0      true -32 wit inspect 17    8.9  550 0   0   true -32 --- inspect 18     10     480   .66 0   false(unreach-call) 1 --- inspect 25    16    1500 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 .39  .38  15   4.9  .23   0      true -32 wit inspect 19    9.6  620 0   0   true -32 --- inspect 19     11     530   .62 0   false(unreach-call) 1 --- inspect 39    24    1900 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    22    .50  0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .35  .34  15   4.8  .19   0      true -32 wit inspect 15    7.9  510 0   0   true -32 --- inspect 19     11     510   .66 0   false(unreach-call) 1 --- inspect 25    15    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 .39  .38  15   4.5  .21   0      true -32 wit inspect 16    8.3  600 0   0   true -32 --- inspect 16     9.5   460   .62 0   false(unreach-call) 1 --- inspect 36    23    1600 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 .34  .33  15   4.5  .20   0      true -32 wit inspect 21    11    530 0   0   true -32 --- inspect 19     11     470   .66 0   false(unreach-call) 1 --- inspect 24    14    1500 0   0      false(unreach-call) 1 --- inspect 1.2    1.1    22    .48  0     - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41  .40  15   5.7  .23   0      true -32 wit inspect 21    11    600 0   0   true -32 --- inspect 16     9.3   520   .66 0   false(unreach-call) 1 --- inspect 35    22    1700 0   0      false(unreach-call) 1 --- inspect 1.2    1.1    22    .50  0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 68     68     730   590    .27   0      true -32 wit inspect 19    10    670 0   0   true -32 --- inspect 16     9.2   520   .62 0   false(unreach-call) 1 --- inspect 51    35    2300 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    23    .56  0     - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .32  .31  15   3.4  .0082 0      true -32 wit inspect 14    7.1  530 0   0   true -32 --- inspect 16     9.0   530   .62 0   false(unreach-call) 1 --- inspect 34    21    1700 0   0      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 .28  .27  15   3.7  .0082 0      true -32 wit inspect 13    6.9  520 0   0   true -32 --- inspect 17     9.4   520   .66 0   false(unreach-call) 1 --- inspect 38    24    1700 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    23    .46  0     - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .29  .28  15   3.6  .0082 0      true -32 wit inspect 16    8.3  510 0   0   true -32 --- inspect 18     9.9   540   .66 0   false(unreach-call) 1 --- inspect 48    29    1800 0   0      false(unreach-call) 1 --- inspect 1.1    1.2    23    .47  0     - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .30  .29  15   3.4  .0082 0      true -32 wit inspect 18    9.1  540 0   0   true -32 --- inspect 18     10     510   .62 0   false(unreach-call) 1 --- inspect 38    23    1700 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    23    .47  0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .30  .29  16   4.2  .0082 0      true -32 wit inspect 17    8.9  510 0   0   true -32 --- inspect 22     12     470   .66 0   false(unreach-call) 1 --- inspect 45    28    1900 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    23    .50  0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .30  .29  15   3.7  .0082 0      true -32 wit inspect 17    8.6  520 0   0   true -32 --- inspect 17     10     530   .66 0   false(unreach-call) 1 --- inspect 42    27    1800 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 .32  .31  15   3.3  .0082 0      true -32 wit inspect 14    7.1  530 0   0   true -32 --- inspect 20     11     540   .66 0   false(unreach-call) 1 --- inspect 37    23    1800 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 .30  .29  15   3.7  .0082 0      true -32 wit inspect 16    8.2  530 0   0   true -32 --- inspect 20     11     530   .66 0   false(unreach-call) 1 --- inspect 37    24    1900 0   0      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 .31  .30  16   3.5  .0082 0      true -32 wit inspect 14    7.1  520 0   0   true -32 --- inspect 19     10     520   .62 0   false(unreach-call) 1 --- inspect 42    27    1800 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 .33  .32  15   4.9  .0082 0      true -32 wit inspect 18    9.3  550 0   0   true -32 --- inspect 21     12     470   .66 0   false(unreach-call) 1 --- inspect 38    24    2100 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    23    .50  .078 - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 64     64     710   530    .0082 0      true -32 wit inspect 16    8.5  540 0   0   true -32 --- inspect 17     9.6   470   .66 0   false(unreach-call) 1 --- inspect 51    36    2300 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    23    .53  .082 - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .34  .33  15   4.8  .20   0      true -32 wit inspect 15    7.6  520 0   0   true -32 --- inspect 15     8.2   520   .62 0   false(unreach-call) 1 --- inspect 22    14    1500 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    22    .46  .074 - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .35  15   4.6  .23   0      true -32 wit inspect 16    8.4  610 0   0   true -32 --- inspect 17     10     520   .66 0   false(unreach-call) 1 --- inspect 33    20    1700 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    22    .48  .074 - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .36  15   3.9  .22   0      true -32 wit inspect 18    9.1  560 0   0   true -32 --- inspect 15     8.7   540   .62 0   false(unreach-call) 1 --- inspect 30    19    1400 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    22    .49  0     - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38  .37  15   4.2  .25   0      true -32 wit inspect 19    9.7  610 0   0   true -32 --- inspect 20     11     470   .66 0   false(unreach-call) 1 --- inspect 38    25    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 false(unreach-call) 1 wit inspect 65     65     720   550    .27   0      true -32 wit inspect 21    11    610 0   0   true -32 --- inspect 19     11     510   .66 0   false(unreach-call) 1 --- inspect 49    34    2200 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    23    .54  0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 330     330     15000   4100    53      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .39 43 0   0   error (2) 0 --- inspect .027 .029 5.6 0    0     
elevator_spec13_product22_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 330     330     15000   5500    58      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 40 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0     
elevator_spec13_product23_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 290     290     15000   3900    28      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 40 0   0   error (2) 0 --- inspect .028 .030 5.6 0    0     
elevator_spec13_product24_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 290     290     15000   3600    29      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0     
elevator_spec13_product29_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 330     330     15000   4500    51      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0   error (2) 0 --- inspect .024 .026 5.6 0    0     
elevator_spec13_product30_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 330     330     15000   4200    53      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0     
elevator_spec13_product31_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 290     290     15000   4500    33      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 40 0   0   error (2) 0 --- inspect .026 .027 5.7 0    0     
elevator_spec13_product32_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 290     290     15000   4000    33      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 40 0   0   error (2) 0 --- inspect .028 .029 5.5 0    0     
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c error (42) 0 --- inspect 880     880     350   10000    .090  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .92 .57 42 0   0   error (2) 0 --- inspect .026 .027 5.5 0    0     
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect .84  .84  15   9.9  .75   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 940    490    5500 0   0   out of memory 0 --- inspect 310     220     7000   .72 0     
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect .84  .83  15   12    .76   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 930    490    5500 0   0   out of memory 0 --- inspect 290     200     7000   1.4  0     
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect .85  .85  16   13    .77   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    490    5500 0   0   out of memory 0 --- inspect 340     240     7000   .65 0     
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect .93  .93  17   12    .93   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 940    490    5500 0   0   out of memory 0 --- inspect 260     180     7000   .63 0     
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect .85  .85  16   13    .77   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 900    470    5500 0   0   out of memory 0 --- inspect 300     220     7000   .63 0     
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect .93  .93  17   12    .93   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 900    480    5500 0   0   out of memory 0 --- inspect 230     150     7000   .65 0     
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect .63  .63  15   8.8  .57   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 300     210     7000   .64 0     
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect .70  .70  15   7.9  .67   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    490    5500 0   0   out of memory 0 --- inspect 300     210     7000   .64 0     
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect .62  .62  15   8.8  .58   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 300     210     7000   .65 .0082
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect .71  .70  15   12    .68   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    490    5500 0   0   out of memory 0 --- inspect 260     180     7000   .64 .012 
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect .63  .63  15   7.9  .59   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 930    480    5500 0   0   out of memory 0 --- inspect 260     180     7000   .63 0     
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect .72  .71  15   9.6  .69   0      - --- inspect - --- inspect - --- inspect - --- inspect out of java memory 0 --- inspect 770    410    5500 0   0   out of memory 0 --- inspect 280     200     7000   .72 0     
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect .71  .70  15   9.3  .66   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 940    490    5500 0   0   out of memory 0 --- inspect 320     220     7000   .63 0     
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect .80  .79  16   11    .75   0      - --- inspect - --- inspect - --- inspect - --- inspect out of java memory 0 --- inspect 700    370    5500 0   0   out of memory 0 --- inspect 320     230     7000   .66 0     
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect .64  .64  15   8.7  .60   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 900    480    5500 0   0   out of memory 0 --- inspect 290     200     7000   .63 0     
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect .73  .72  15   9.1  .70   .0041 - --- inspect - --- inspect - --- inspect - --- inspect out of java memory 0 --- inspect 790    420    5500 0   0   out of memory 0 --- inspect 350     240     7000   .64 0     
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect .71  .71  15   9.4  .67   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    490    5500 0   0   out of memory 0 --- inspect 190     130     7000   .65 0     
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect .79  .79  16   11    .77   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 350     240     7000   .65 0     
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect .31  .31  15   3.7  .20   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 200     130     7000   .64 0     
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect .35  .35  15   4.1  .23   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 230     150     7000   .78 0     
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect .31  .31  15   3.7  .20   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 190     120     7000   .64 0     
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect .39  .38  15   4.0  .23   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 210     140     7000   .66 0     
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect .33  .33  15   3.8  .20   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 180     110     7000   .69 0     
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect .37  .36  15   4.2  .23   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 220     150     7000   .71 0     
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect .33  .33  15   5.3  .22   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 940    490    5500 0   0   out of memory 0 --- inspect 210     140     7000   .64 0     
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect .37  .37  15   4.6  .25   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 940    500    5500 0   0   out of memory 0 --- inspect 280     190     7000   .62 0     
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect .33  .32  15   4.7  .21   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 190     120     7000   .65 0     
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect .41  .40  15   4.4  .24   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 190     130     7000   1.4  0     
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect .35  .34  15   4.3  .22   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960    500    5500 0   0   out of memory 0 --- inspect 200     130     7000   .71 0     
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect .42  .42  15   4.5  .25   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 340     230     7000   .63 0     
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect .89  .88  16   12    .83   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 190     120     7000   .72 .012 
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect .87  .87  16   12    .84   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 190     120     7000   .63 0     
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect .87  .87  16   12    .84   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960    500    5500 0   0   out of memory 0 --- inspect 180     120     7000   .66 0     
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 1 wit inspect .92  .91  17   13    .88   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 940    490    5500 0   0   out of memory 0 --- inspect 180     120     7000   .66 .033 
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect .99  .98  17   16    .97   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 940    490    5500 0   0   out of memory 0 --- inspect 280     180     7000   .63 0     
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.0   1.0   18   13    1.0    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 220     150     7000   .64 0     
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect .87  .86  16   12    .85   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    490    5500 0   0   out of memory 0 --- inspect 200     130     7000   .64 0     
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 1 wit inspect .93  .93  17   10    .88   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960    500    5500 0   0   out of memory 0 --- inspect 230     160     7000   .65 0     
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.0   1.0   18   12    .98   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 220     150     7000   .70 0     
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.0   1.0   18   11    1.0    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 200     140     7000   .63 0     
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect .36  .35  15   3.6  .22   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 210     140     7000   .84 0     
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect .36  .35  15   4.5  .25   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    480    5500 0   0   out of memory 0 --- inspect 220     150     7000   .63 0     
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect .33  .33  15   4.7  .23   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 230     150     7000   .81 0     
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect .35  .35  15   4.6  .25   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 930    490    5500 0   0   out of memory 0 --- inspect 230     150     7000   .66 0     
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect .34  .34  15   4.1  .23   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    480    5500 0   0   out of memory 0 --- inspect 220     140     7000   .64 0     
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect .38  .38  16   5.5  .26   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 940    490    5500 0   0   out of memory 0 --- inspect 220     150     7000   .64 0     
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 1.2   1.2   32   14    .19   0      unknown 0 wit inspect 8.6  4.5  300 0   0   true -32 --- inspect 15     8.7   520   .66 0   unknown 0 --- inspect 10    5.5  450 0   0      error (2) 0 --- inspect 1.0    1.0    22    .094 0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.4   2.4   46   31    .25   0      unknown 0 wit inspect 9.8  5.1  310 0   0   true -32 --- inspect 14     8.1   550   .66 0   unknown 0 --- inspect 12    6.5  450 0   0      error (2) 0 --- inspect 1.1    1.1    22    .098 0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 1.2   1.2   33   16    .19   0      unknown 0 wit inspect 7.9  4.1  300 0   0   true -32 --- inspect 17     9.6   460   .62 0   unknown 0 --- inspect 12    6.1  450 0   0      error (2) 0 --- inspect 1.0    1.0    22    .094 0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.6   2.6   50   40    .21   0      unknown 0 wit inspect 7.7  4.0  300 0   0   true -32 --- inspect 17     9.6   470   .66 0   unknown 0 --- inspect 11    5.8  440 0   0      error (2) 0 --- inspect 1.1    1.1    22    .098 0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 1.5   1.5   36   23    .21   0      unknown 0 wit inspect 9.5  5.0  300 0   0   true -32 --- inspect 15     8.5   510   .62 0   unknown 0 --- inspect 10    5.5  450 0   0      error (2) 0 --- inspect 1.0    1.0    22    .098 0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 1.6   1.6   37   23    .20   0      unknown 0 wit inspect 8.5  4.5  270 0   0   true -32 --- inspect 16     8.7   530   .66 0   unknown 0 --- inspect 11    5.6  450 0   0      error (2) 0 --- inspect 1.0    1.0    22    .098 0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.6   3.6   59   49    .21   0      unknown 0 wit inspect 8.4  4.4  300 0   0   true -32 --- inspect 17     9.6   530   .66 0   unknown 0 --- inspect 11    6.1  450 0   0      error (2) 0 --- inspect 1.0    1.0    22    .098 0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.9   3.9   61   54    .23   0      unknown 0 wit inspect 9.2  4.8  300 0   0   true -32 --- inspect 21     11     530   .66 0   unknown 0 --- inspect 14    7.4  450 0   0      error (2) 0 --- inspect 1.1    1.1    22    .098 0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c error (42) 0 --- inspect 880     880     1400   5400    .070  0      error (invalid witness file) 0 --- inspect .65 .40 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .61 47 0   0      error (invalid witness file) 0 --- inspect .0025 .0028 .40 0     0     - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 1.1   1.1   31   14    .16   0      unknown 0 wit inspect 8.1  4.3  260 0   0   true -32 --- inspect 15     8.3   510   .66 0   unknown 0 --- inspect 8.5  4.6  340 0   0      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 2.1   2.1   43   27    .24   0      unknown 0 wit inspect 8.6  4.5  310 0   0   true -32 --- inspect 17     10     540   .62 0   unknown 0 --- inspect 12    6.1  450 0   0      error (2) 0 --- inspect 1.1    1.1    22    .098 0     - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 1.2   1.2   32   21    .17   0      unknown 0 wit inspect 6.6  3.5  260 0   0   true -32 --- inspect 16     9.0   460   .62 0   unknown 0 --- inspect 9.2  5.0  440 0   0      error (2) 0 --- inspect .99   .99   21    .094 0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.7   2.6   50   34    .18   0      unknown 0 wit inspect 7.0  3.7  270 0   0   true -32 --- inspect 16     9.1   500   .66 0   unknown 0 --- inspect 9.0  4.8  410 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 1.3   1.3   35   17    .18   0      unknown 0 wit inspect 8.9  4.7  290 0   0   true -32 --- inspect 17     9.4   530   .66 0   unknown 0 --- inspect 8.6  4.6  350 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 3.1   3.1   54   34    .27   0      unknown 0 wit inspect 9.3  4.9  310 0   0   true -32 --- inspect 15     8.8   520   .62 0   unknown 0 --- inspect 13    6.9  450 0   0      error (2) 0 --- inspect 1.1    1.1    22    .098 0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 1.6   1.6   37   20    .20   0      unknown 0 wit inspect 9.6  5.0  300 0   0   true -32 --- inspect 15     8.3   460   .66 0   unknown 0 --- inspect 9.4  5.1  400 0   0      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 4.0   4.0   61   59    .29   0      unknown 0 wit inspect 9.3  4.9  310 0   0   true -32 --- inspect 17     9.7   530   .62 0   unknown 0 --- inspect 14    7.2  510 0   0      error (2) 0 --- inspect 1.2    1.2    23    .098 0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c error (42) 0 --- inspect 880     880     1600   7100    .074  0      error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .021 .023 5.8 0    0   error (invalid witness file) 0 --- inspect .93 .59 47 0   0      error (invalid witness file) 0 --- inspect .0053 .0071 .53 0     0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 1.1   1.1   30   12    .23   0      unknown 0 wit inspect 8.4  4.4  310 0   0   true -32 --- inspect 15     8.4   520   .62 0   unknown 0 --- inspect 13    6.8  500 0   0      error (2) 0 --- inspect 1.1    1.1    22    .094 .066 - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 1.1   1.1   30   13    .23   0      unknown 0 wit inspect 9.1  4.8  300 0   0   true -32 --- inspect 15     8.6   530   .62 0   unknown 0 --- inspect 12    6.1  450 0   0      error (2) 0 ---