Tool ESBMC version 6.0.0 64-bit x86_64 linux 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* [apollon004; apollon069; apollon137; apollon154] 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-06 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 02:16:29 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options -s kinduction -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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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 .33  .33  55 4.7  1.0  0   false(unreach-call) 1 wit inspect 8.5 4.5 280 0   0     true -32 --- inspect 16   9.0 500 .62  0   false(unreach-call) 1 --- inspect 5.3 3.0 260 0   0   false(unreach-call) 1 --- inspect .84 .84 20 .34 0     - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .36  56 3.8  1.0  0   false(unreach-call) 1 wit inspect 7.6 4.1 290 0   0     true -32 --- inspect 16   9.0 530 .66  0   false(unreach-call) 1 --- inspect 5.4 3.0 270 0   0   false(unreach-call) 1 --- inspect .84 .84 20 .35 0     - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .33  .33  56 5.2  .85 0   false(unreach-call) 1 wit inspect 8.9 4.7 280 0   0     true -32 --- inspect 18   10   510 .62  0   false(unreach-call) 1 --- inspect 6.3 3.5 270 0   0   false(unreach-call) 1 --- inspect .84 .86 20 .26 0     - --- inspect - --- inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .35  .35  57 4.1  1.0  0   false(unreach-call) 1 wit inspect 8.0 4.4 290 0   0     true -32 --- inspect 18   10   460 .62  0   false(unreach-call) 1 --- inspect 5.3 2.9 270 0   0   false(unreach-call) 1 --- inspect .86 .86 20 .35 0     - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0   3.0   170 37    .85 0   true -32 wit inspect 7.3 3.9 280 0   0     true -32 --- inspect 17   10   520 .62  0   false(unreach-call) 1 --- inspect 7.7 4.2 370 0   0   false(unreach-call) 1 --- inspect .87 .87 21 .38 0     - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37  .37  57 4.6  .85 0   false(unreach-call) 1 wit inspect 7.5 4.0 280 0   0     true -32 --- inspect 16   9.0 510 .62  0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0   0   false(unreach-call) 1 --- inspect .87 .86 20 .34 0     - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39  .39  58 4.7  .85 0   false(unreach-call) 1 wit inspect 9.1 4.9 290 0   0     true -32 --- inspect 16   9.2 480 .62  0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0   0   false(unreach-call) 1 --- inspect .85 .85 21 .36 .074 - --- inspect - --- inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40  .40  58 4.8  .85 0   false(unreach-call) 1 wit inspect 8.0 4.3 310 0   0     true -32 --- inspect 16   9.2 530 .62  0   false(unreach-call) 1 --- inspect 5.5 3.1 270 0   0   false(unreach-call) 1 --- inspect .85 .85 20 .35 0     - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42  .42  60 4.8  1.0  0   false(unreach-call) 1 wit inspect 8.4 4.5 290 0   0     true -32 --- inspect 20   11   470 .62  0   false(unreach-call) 1 --- inspect 5.5 3.1 270 0   0   false(unreach-call) 1 --- inspect .87 .89 20 .36 .078 - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39  .39  59 3.8  1.0  0   false(unreach-call) 1 wit inspect 7.5 4.0 280 0   0     true -32 --- inspect 18   10   510 .66  0   false(unreach-call) 1 --- inspect 5.6 3.2 270 0   0   false(unreach-call) 1 --- inspect .85 .85 20 .35 0     - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37  .37  59 5.3  1.0  0   false(unreach-call) 1 wit inspect 9.2 4.9 290 0   0     true -32 --- inspect 17   9.6 470 .62  0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0   0   false(unreach-call) 1 --- inspect .86 .86 20 .36 0     - --- inspect - --- inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40  .40  59 5.3  1.0  0   false(unreach-call) 1 wit inspect 7.2 3.9 290 0   0     true -32 --- inspect 17   10   480 .57  0   false(unreach-call) 1 --- inspect 5.3 2.9 260 0   0   false(unreach-call) 1 --- inspect .85 .85 20 .36 .074 - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42  .42  61 4.9  1.0  0   false(unreach-call) 1 wit inspect 7.8 4.2 300 0   0     true -32 --- inspect 18   10   540 .62  0   false(unreach-call) 1 --- inspect 5.7 3.2 270 0   0   false(unreach-call) 1 --- inspect .87 .87 21 .36 .078 - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.4   5.4   200 67    1.0  0   true -32 wit inspect 7.5 4.0 280 0   0     true -32 --- inspect 18   10   520 .62  0   false(unreach-call) 1 --- inspect 9.1 4.9 420 0   0   false(unreach-call) 1 --- inspect .87 .87 21 .39 0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .36  55 4.5  .85 0   false(unreach-call) 1 wit inspect 7.8 4.2 280 0   0     true -32 --- inspect 18   11   500 .62  0   false(unreach-call) 1 --- inspect 5.2 2.9 270 0   0   false(unreach-call) 1 --- inspect .84 .84 20 .34 0     - --- inspect - --- inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .36  56 5.3  1.0  0   false(unreach-call) 1 wit inspect 7.5 4.0 280 0   0     true -32 --- inspect 16   9.2 510 .62  0   false(unreach-call) 1 --- inspect 5.0 2.8 270 0   0   false(unreach-call) 1 --- inspect .86 .87 20 .35 0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38  .38  56 4.3  .85 0   false(unreach-call) 1 wit inspect 7.5 4.0 290 0   0     true -32 --- inspect 18   10   460 .62  0   false(unreach-call) 1 --- inspect 5.3 3.0 260 0   0   false(unreach-call) 1 --- inspect .85 .85 20 .35 0     - --- inspect - --- inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .36  57 5.1  1.0  0   false(unreach-call) 1 wit inspect 8.1 4.3 290 0   0     true -32 --- inspect 18   10   520 .62  0   false(unreach-call) 1 --- inspect 5.1 2.9 260 0   0   false(unreach-call) 1 --- inspect .91 .91 20 .36 0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37  .37  56 4.8  1.0  0   false(unreach-call) 1 wit inspect 7.9 4.3 280 0   0     true -32 --- inspect 14   8.5 500 .62  0   false(unreach-call) 1 --- inspect 5.3 3.0 260 0   0   false(unreach-call) 1 --- inspect .85 .85 20 .35 0     - --- inspect - --- inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .36  57 4.6  1.0  0   false(unreach-call) 1 wit inspect 7.4 4.0 280 0   0     true -32 --- inspect 19   11   520 .62  0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0   0   false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37  .37  57 4.5  1.0  0   false(unreach-call) 1 wit inspect 8.0 4.4 290 0   0     true -32 --- inspect 17   9.6 460 .66  0   false(unreach-call) 1 --- inspect 5.4 3.1 270 0   0   false(unreach-call) 1 --- inspect .86 .88 20 .36 0     - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39  .39  58 4.7  .85 0   false(unreach-call) 1 wit inspect 8.6 4.6 300 0   0     true -32 --- inspect 17   9.6 470 .62  0   false(unreach-call) 1 --- inspect 5.6 3.1 270 0   0   false(unreach-call) 1 --- inspect .86 .86 20 .36 .078 - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.2   5.2   200 65    .85 0   true -32 wit inspect 6.6 3.6 280 0   0     true -32 --- inspect 20   11   470 .62  0   false(unreach-call) 1 --- inspect 8.9 4.8 430 0   0   false(unreach-call) 1 --- inspect .87 .87 21 .39 .082 - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .36  56 3.9  1.0  0   false(unreach-call) 1 wit inspect 7.6 4.1 290 0   0     true -32 --- inspect 15   9.1 500 .62  0   false(unreach-call) 1 --- inspect 5.1 2.8 260 0   0   false(unreach-call) 1 --- inspect .85 .84 20 .34 0     - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .33  .33  57 4.8  .85 0   false(unreach-call) 1 wit inspect 8.0 4.3 290 0   0     true -32 --- inspect 15   8.8 510 .62  0   false(unreach-call) 1 --- inspect 5.1 2.8 260 0   0   false(unreach-call) 1 --- inspect .85 .85 21 .34 .074 - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .31  .31  56 4.5  .85 0   false(unreach-call) 1 wit inspect 8.2 4.4 290 0   0     true -32 --- inspect 15   9.0 470 .62  0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0   0   false(unreach-call) 1 --- inspect .88 .87 20 .35 0     - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .33  .33  57 4.0  1.0  0   false(unreach-call) 1 wit inspect 9.0 4.8 300 0   0     true -32 --- inspect 17   9.3 530 .62  0   false(unreach-call) 1 --- inspect 5.4 3.0 270 0   0   false(unreach-call) 1 --- inspect .85 .85 20 .35 0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .33  .33  59 4.8  1.0  0   false(unreach-call) 1 wit inspect 9.1 4.9 310 0   0     true -32 --- inspect 17   9.6 510 .62  0   false(unreach-call) 1 --- inspect 5.2 2.9 270 0   0   false(unreach-call) 1 --- inspect .86 .86 20 .36 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .34  .34  58 5.2  1.0  0   false(unreach-call) 1 wit inspect 8.2 4.4 320 0   0     true -32 --- inspect 15   9.0 530 .62  0   false(unreach-call) 1 --- inspect 6.1 3.5 260 0   0   false(unreach-call) 1 --- inspect .86 .86 21 .36 .078 - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .31  .31  57 3.5  .85 0   false(unreach-call) 1 wit inspect 9.9 5.3 290 0   0     true -32 --- inspect 15   8.2 470 .66  0   false(unreach-call) 1 --- inspect 5.8 3.2 280 0   0   false(unreach-call) 1 --- inspect .85 .85 21 .35 .074 - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36  .36  58 4.9  1.0  0   false(unreach-call) 1 wit inspect 8.1 4.4 290 0   0     true -32 --- inspect 17   10   470 .62  0   false(unreach-call) 1 --- inspect 5.5 3.1 270 0   0   false(unreach-call) 1 --- inspect .86 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .34  .34  59 4.2  .85 0   false(unreach-call) 1 wit inspect 9.6 5.2 310 0   0     true -32 --- inspect 15   8.9 520 .62  0   false(unreach-call) 1 --- inspect 5.4 3.1 270 0   0   false(unreach-call) 1 --- inspect .86 .86 20 .36 0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .35  .35  59 4.2  1.0  0   false(unreach-call) 1 wit inspect 9.3 5.0 320 0   0     true -32 --- inspect 18   10   470 .62  0   false(unreach-call) 1 --- inspect 5.4 3.0 270 0   0   false(unreach-call) 1 --- inspect .86 .86 20 .36 0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.4   5.4   260 66    1.0  0   true -32 wit inspect 8.4 4.5 270 0   0     true -32 --- inspect 19   11   460 .62  0   false(unreach-call) 1 --- inspect 10   5.3 430 0   0   false(unreach-call) 1 --- inspect .88 .88 21 .39 0     - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41  .41  56 4.1  .85 0   false(unreach-call) 1 wit inspect 8.3 4.4 280 0   0     true -32 --- inspect 16   9.4 470 .62  0   false(unreach-call) 1 --- inspect 5.3 2.9 260 0   0   false(unreach-call) 1 --- inspect .84 .84 20 .34 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .35  .35  56 4.6  .85 0   false(unreach-call) 1 wit inspect 7.5 4.0 280 0   0     true -32 --- inspect 18   10   480 .62  0   false(unreach-call) 1 --- inspect 5.4 3.0 270 0   0   false(unreach-call) 1 --- inspect .88 .87 20 .36 0     - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38  .38  57 4.5  1.0  0   false(unreach-call) 1 wit inspect 8.8 4.7 290 0   0     true -32 --- inspect 17   10   510 .62  0   false(unreach-call) 1 --- inspect 5.3 2.9 270 0   0   false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37  .38  58 5.7  .85 0   false(unreach-call) 1 wit inspect 8.9 4.8 290 0   0     true -32 --- inspect 17   9.9 470 .62  0   false(unreach-call) 1 --- inspect 5.3 3.0 270 0   0   false(unreach-call) 1 --- inspect .87 .87 20 .36 0     - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.2   5.2   200 66    1.0  0   true -32 wit inspect 8.4 4.5 270 0   0     true -32 --- inspect 21   12   500 .62  0   false(unreach-call) 1 --- inspect 9.2 4.9 430 0   0   false(unreach-call) 1 --- inspect .87 .87 21 .39 0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     1500 14000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0     
elevator_spec13_product22_true-unreach-call_false-termination.cil.c true 1 wit inspect 3.7   3.7   180 44    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3500 0   0   out of memory 0 --- inspect 240     160     7000   .68 0     
elevator_spec13_product23_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     2100 14000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     
elevator_spec13_product24_true-unreach-call_false-termination.cil.c true 1 wit inspect 4.0   4.0   180 43    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4400 0   0   out of memory 0 --- inspect 260     170     7000   1.5  0     
elevator_spec13_product29_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     1400 14000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .89 .55 40 0   0   error (2) 0 --- inspect .025 .026 5.7 0    0     
elevator_spec13_product30_true-unreach-call_false-termination.cil.c true 1 wit inspect 3.7   3.7   180 42    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3300 0   0   out of memory 0 --- inspect 230     150     7000   .63 0     
elevator_spec13_product31_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     2100 12000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0     
elevator_spec13_product32_true-unreach-call_false-termination.cil.c true 1 wit inspect 4.0   4.0   190 48    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4300 0   0   out of memory 0 --- inspect 200     140     7000   .63 0     
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     3400 9600    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 42 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 1.3   1.3   93 15    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    680 0   0   out of memory 0 --- inspect 280     200     7000   .64 0     
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.4   1.4   99 21    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    700 0   0   out of memory 0 --- inspect 310     230     7000   .63 0     
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.5   1.5   93 18    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    690 0   0   out of memory 0 --- inspect 370     260     7000   .63 .033 
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.9   1.9   110 24    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 30    18    1100 0   0   out of memory 0 --- inspect 260     180     7000   .66 .016 
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 1.5   1.5   99 19    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    11    720 0   0   out of memory 0 --- inspect 310     230     7000   .68 0     
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.0   2.0   120 23    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    19    1100 0   0   out of memory 0 --- inspect 230     150     7000   .63 0     
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.6   2.6   110 33    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 75    62    1600 0   0   out of memory 0 --- inspect 280     190     7000   .62 .0082
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.9   2.9   110 35    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 95    79    1700 0   0   out of memory 0 --- inspect 240     170     7000   .64 0     
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.8   2.8   120 35    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 81    67    1700 0   0   out of memory 0 --- inspect 270     190     7000   .64 0     
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.0   3.0   120 36    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 100    86    1800 0   0   out of memory 0 --- inspect 270     190     7000   .63 0     
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.7   2.7   110 35    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 85    73    1700 0   0   out of memory 0 --- inspect 300     210     7000   .67 0     
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.7   2.7   120 34    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    90    1900 0   0   out of memory 0 --- inspect 310     220     7000   .64 0     
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.4   3.4   130 43    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 160    150    2300 0   0   out of memory 0 --- inspect 290     190     7000   .63 0     
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.8   3.8   140 46    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 170    150    2300 0   0   out of memory 0 --- inspect 350     250     7000   .68 0     
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.8   2.8   120 36    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 89    76    1800 0   0   out of memory 0 --- inspect 290     200     7000   .63 0     
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.5   3.5   140 44    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    95    2000 0   0   out of memory 0 --- inspect 250     170     7000   .68 0     
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 4.0   4.0   150 61    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 360    340    2400 0   0   out of memory 0 --- inspect 310     210     7000   .63 0     
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.9   3.9   150 52    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 200    180    2400 0   0   out of memory 0 --- inspect 320     230     7000   .68 0     
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.4   2.4   120 30    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    26    1000 0   0   out of memory 0 --- inspect 200     130     7000   .63 0     
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.4   2.4   120 33    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    25    1100 0   0   out of memory 0 --- inspect 210     140     7000   1.5  0     
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.0   3.0   130 37    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    25    1100 0   0   out of memory 0 --- inspect 160     110     7000   .66 0     
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.7   2.7   120 36    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 42    29    1200 0   0   out of memory 0 --- inspect 210     140     7000   .65 0     
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.8   2.8   120 33    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    28    1100 0   0   out of memory 0 --- inspect 180     120     7000   .63 0     
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.6   2.6   120 38    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    28    1200 0   0   out of memory 0 --- inspect 210     140     7000   .63 0     
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.6   3.6   140 47    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 50    38    1300 0   0   out of memory 0 --- inspect 210     140     7000   .65 0     
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.3   3.3   140 39    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 59    45    1500 0   0   out of memory 0 --- inspect 310     210     7000   .64 0     
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.6   2.6   120 38    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 43    29    1200 0   0   out of memory 0 --- inspect 210     140     7000   .63 0     
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.2   3.2   140 47    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 47    35    1200 0   0   out of memory 0 --- inspect 210     140     7000   .63 0     
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.2   3.2   140 45    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 72    58    1500 0   0   out of memory 0 --- inspect 220     140     7000   .64 0     
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.5   3.5   150 49    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 58    43    1500 0   0   out of memory 0 --- inspect 260     180     7000   .69 .0041
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.2   2.2   110 29    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    650 0   0   out of memory 0 --- inspect 150     100     7000   .64 0     
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.2   2.2   110 27    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    640 0   0   out of memory 0 --- inspect 160     100     7000   .65 0     
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.3   2.3   110 36    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    670 0   0   out of memory 0 --- inspect 160     110     7000   .63 0     
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.2   2.2   120 27    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    13    850 0   0   out of memory 0 --- inspect 210     140     7000   .66 0     
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.9   2.9   130 31    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 26    14    900 0   0   out of memory 0 --- inspect 220     150     7000   .63 0     
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.5   3.5   160 49    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    20    1500 0   0   out of memory 0 --- inspect 240     170     7000   .64 0     
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.3   2.3   120 37    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    10    700 0   0   out of memory 0 --- inspect 210     130     7000   1.5  0     
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.4   2.4   130 28    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    15    930 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 3.2   3.2   140 42    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    15    880 0   0   out of memory 0 --- inspect 270     180     7000   .68 .033 
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.6   3.6   160 51    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    20    1600 0   0   out of memory 0 --- inspect 210     140     7000   .64 0     
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.4   2.4   120 31    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    26    1000 0   0   out of memory 0 --- inspect 190     130     7000   .78 0     
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 2.6   2.6   120 32    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 44    30    1200 0   0   out of memory 0 --- inspect 200     130     7000   .64 0     
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.1   3.1   130 41    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    28    1200 0   0   out of memory 0 --- inspect 230     160     7000   .64 0     
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.2   3.2   140 48    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 45    32    1200 0   0   out of memory 0 --- inspect 230     140     7000   .63 0     
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.3   3.3   140 43    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 76    62    1500 0   0   out of memory 0 --- inspect 200     130     7000   .64 0     
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.9   4.0   160 59    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 68    54    1500 0   0   out of memory 0 --- inspect 230     150     7000   .64 0     
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.8   1.8   46 26    .85 0   false(unreach-call) 1 wit inspect 7.9 4.3 290 0   0     true -32 --- inspect 14   8.4 470 .62  0   unknown 0 --- inspect 6.3 3.5 270 0   0   false(unreach-call) 1 --- inspect .82 .82 20 .37 0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1   3.1   56 44    1.0  0   false(unreach-call) 1 wit inspect 9.8 5.2 300 0   0     true -32 --- inspect 16   9.3 460 .62  0   unknown 0 --- inspect 7.0 3.8 280 0   0   false(unreach-call) 1 --- inspect .84 .83 21 .38 0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.1   2.1   48 25    .85 0   false(unreach-call) 1 wit inspect 8.0 4.3 290 0   0     true -32 --- inspect 18   10   480 .62  0   unknown 0 --- inspect 6.3 3.5 270 0   0   false(unreach-call) 1 --- inspect .84 .85 20 .37 0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.6   3.6   61 48    1.0  0   false(unreach-call) 1 wit inspect 9.4 5.0 320 0   0     true -32 --- inspect 16   9.4 500 .66  0   unknown 0 --- inspect 7.0 3.9 300 0   0   false(unreach-call) 1 --- inspect .84 .84 21 .39 0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.0   2.0   49 26    .85 0   false(unreach-call) 1 wit inspect 7.4 3.9 300 0   0     true -32 --- inspect 18   10   460 .62  0   unknown 0 --- inspect 6.6 3.7 280 0   0   false(unreach-call) 1 --- inspect .84 .84 21 .39 0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.3   2.3   51 28    .85 0   false(unreach-call) 1 wit inspect 7.6 4.1 300 0   0     true -32 --- inspect 16   9.3 460 .62  0   unknown 0 --- inspect 6.2 3.5 280 0   0   false(unreach-call) 1 --- inspect .84 .83 21 .39 0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.7   3.7   61 56    .85 0   false(unreach-call) 1 wit inspect 10   5.4 310 0   0     true -32 --- inspect 15   8.9 460 .62  0   unknown 0 --- inspect 7.4 4.1 290 0   0   false(unreach-call) 1 --- inspect .84 .84 21 .39 0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.4   4.4   67 68    1.0  0   false(unreach-call) 1 wit inspect 7.9 4.2 300 0   0     true -32 --- inspect 15   8.9 520 .62  0   unknown 0 --- inspect 6.7 3.7 280 0   0   false(unreach-call) 1 --- inspect .84 .84 21 .40 .066 - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 71     71     480 1000    .85 0   true -32 wit inspect 7.0 3.7 280 0   0     true -32 --- inspect 16   9.6 530 .62  0   unknown 0 --- inspect 6.7 3.7 280 0   0   false(unreach-call) 1 --- inspect .87 .87 21 .43 0     - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.6   1.6   44 20    1.0  0   false(unreach-call) 1 wit inspect 7.3 3.9 280 0   0     true -32 --- inspect 17   9.5 480 .62  0   unknown 0 --- inspect 6.1 3.4 280 0   0   false(unreach-call) 1 --- inspect .83 .83 21 .37 .061 - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0   3.0   54 39    .85 0   false(unreach-call) 1 wit inspect 7.7 4.1 300 0   0     true -32 --- inspect 15   8.5 460 .62  0   unknown 0 --- inspect 6.3 3.5 280 0   0   false(unreach-call) 1 --- inspect .83 .83 21 .38 0     - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.0   2.0   48 23    1.0  0   false(unreach-call) 1 wit inspect 7.6 4.1 300 0   0     true -32 --- inspect 13   7.8 470 .62  0   unknown 0 --- inspect 6.1 3.4 270 0   0   false(unreach-call) 1 --- inspect .84 .84 21 .37 0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.9   3.9   61 40    .85 0   false(unreach-call) 1 wit inspect 9.0 4.8 300 0   0     true -32 --- inspect 16   9.2 460 .62  0   unknown 0 --- inspect 6.0 3.3 280 0   0   false(unreach-call) 1 --- inspect .86 .86 21 .39 0     - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.8   1.8   47 23    .85 0   false(unreach-call) 1 wit inspect 7.8 4.1 300 0   0     true -32 --- inspect 17   9.7 460 .62  0   unknown 0 --- inspect 6.4 3.5 280 0   0   false(unreach-call) 1 --- inspect .85 .85 21 .39 0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.5   3.5   59 56    .85 0   false(unreach-call) 1 wit inspect 8.5 4.5 300 0   0     true -32 --- inspect 17   9.8 500 .62  0   unknown 0 --- inspect 6.8 3.8 280 0   0   false(unreach-call) 1 --- inspect .85 .85 21 .39 0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.1   2.1   51 25    1.0  0   false(unreach-call) 1 wit inspect 7.7 4.1 300 0   0     true -32 --- inspect 17   9.6 510 .62  0   unknown 0 --- inspect 6.0 3.4 280 0   0   false(unreach-call) 1 --- inspect .86 .86 20 .39 0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.2   4.2   67 54    1.0  0   false(unreach-call) 1 wit inspect 7.7 4.1 300 0   0     true -32 --- inspect 15   8.9 470 .62  0   unknown 0 --- inspect 8.1 4.4 280 0   0   false(unreach-call) 1 --- inspect .87 .87 20 .40 0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 84     84     530 1000    1.0  0   true -32 wit inspect 7.0 3.8 280 0   0     true -32 --- inspect 18   10   470 .62  0   unknown 0 --- inspect 8.1 4.5 270 0   0   false(unreach-call) 1 --- inspect .88 .88 21 .43 0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .75  .75  47 11    .85 0   true -32 wit inspect 8.7 4.6 290 0   0     true -32 --- inspect 16   9.5 460 .62  0   false(unreach-call) 1 --- inspect 7.5 4.1 290 0   0   false(unreach-call) 1 --- inspect .84 .84 21 .37 .066 - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .67  .67  42 8.4  .85 0   true -32 wit inspect 7.3 3.9 280 0   0     true -32 --- inspect 14   8.5 460 .62  0   false(unreach-call) 1 --- inspect 6.2 3.4 280 0   0   false(unreach-call) 1 --- inspect .85 .86 21 .37 0     - --- inspect - --- inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .70  .70  43 8.3  1.0  0   true -32 wit