Tool Pinaka 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
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 20:14:43 CET 2018-12-07 17:00:25 CET 2018-12-07 18:15:01 CET 2018-12-07 18:51:03 CET 2018-12-12 20:55:30 CET 2018-12-07 16:17:05 CET 2018-12-07 17:47:50 CET
Run set pinaka.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-pinaka.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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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 .60 .60 72 6.1 .0041 0     false(unreach-call) 1 wit inspect 8.2  4.3  310 0   0     false(unreach-call) 1 --- inspect 29     17     890   .66 0   false(unreach-call) 1 --- inspect 32    19    1600 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .44 .070 - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .60 .60 72 6.6 .0041 0     false(unreach-call) 1 wit inspect 9.7  5.1  320 0   0     false(unreach-call) 1 --- inspect 30     17     880   .66 0   false(unreach-call) 1 --- inspect 48    31    1700 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 .59 .59 72 5.5 .0041 0     false(unreach-call) 1 wit inspect 8.3  4.4  310 0   0     false(unreach-call) 1 --- inspect 30     17     880   .66 0   false(unreach-call) 1 --- inspect 37    23    1800 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 .65 .65 72 5.6 .0041 0     false(unreach-call) 1 wit inspect 8.6  4.5  320 0   0     false(unreach-call) 1 --- inspect 34     19     1100   .66 0   false(unreach-call) 1 --- inspect 38    24    1900 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .47 .074 - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .70 .70 73 7.3 .0041 0     false(unreach-call) 1 wit inspect 11    5.5  330 0   0     false(unreach-call) 1 --- inspect 50     27     1300   .66 0   false(unreach-call) 1 --- inspect 54    38    2300 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    23    .52 0     - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 .65 72 6.3 .0041 0     false(unreach-call) 1 wit inspect 9.4  4.9  310 0   0     false(unreach-call) 1 --- inspect 44     24     1100   .62 0   false(unreach-call) 1 --- inspect 37    23    1800 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 .66 .66 73 7.5 .0041 0     false(unreach-call) 1 wit inspect 9.0  4.7  320 0   0     false(unreach-call) 1 --- inspect 41     23     1300   .62 0   false(unreach-call) 1 --- inspect 43    28    2100 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 .63 .63 73 6.0 .0041 0     false(unreach-call) 1 wit inspect 8.5  4.5  330 0   0     false(unreach-call) 1 --- inspect 46     25     1200   .62 0   false(unreach-call) 1 --- inspect 41    26    2100 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 .67 .67 73 6.2 .0041 0     false(unreach-call) 1 wit inspect 8.9  4.7  330 0   0     false(unreach-call) 1 --- inspect 45     26     1400   .62 0   false(unreach-call) 1 --- inspect 58    41    2400 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    23    .50 .078 - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .63 .63 72 5.9 .0041 0     false(unreach-call) 1 wit inspect 9.4  4.9  310 0   0     false(unreach-call) 1 --- inspect 41     23     970   .66 0   false(unreach-call) 1 --- inspect 37    24    1700 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .45 0     - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 .65 73 6.0 .0041 0     false(unreach-call) 1 wit inspect 9.7  5.1  320 0   0     false(unreach-call) 1 --- inspect 41     24     1300   .66 0   false(unreach-call) 1 --- inspect 50    35    2200 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 .66 .66 73 7.0 .0041 0     false(unreach-call) 1 wit inspect 9.1  4.8  330 0   0     false(unreach-call) 1 --- inspect 37     21     1200   .62 0   false(unreach-call) 1 --- inspect 46    31    2100 0   0   false(unreach-call) 1 --- inspect 1.2    1.1    22    .49 0     - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 .65 73 8.1 .0041 0     false(unreach-call) 1 wit inspect 9.4  4.9  330 0   0     false(unreach-call) 1 --- inspect 54     30     1400   .62 0   false(unreach-call) 1 --- inspect 58    39    2500 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    23    .51 .078 - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .74 .74 74 7.2 .0041 0     false(unreach-call) 1 wit inspect 9.5  5.0  340 0   0     false(unreach-call) 1 --- inspect 57     33     2100   .62 0   timeout (false(unreach-call)) 0 --- inspect 92    69    2700 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    23    .56 .082 - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 .65 72 5.9 .0041 0     false(unreach-call) 1 wit inspect 8.2  4.3  310 0   0     false(unreach-call) 1 --- inspect 44     25     1100   .66 0   false(unreach-call) 1 --- inspect 35    22    1800 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 .65 .65 72 6.0 .0041 0     false(unreach-call) 1 wit inspect 9.7  5.1  320 0   0     false(unreach-call) 1 --- inspect 41     23     1000   .66 0   false(unreach-call) 1 --- inspect 45    29    2200 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .42 0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .63 .62 73 6.7 .0041 0     false(unreach-call) 1 wit inspect 8.4  4.5  320 0   0     false(unreach-call) 1 --- inspect 45     25     1100   .66 0   false(unreach-call) 1 --- inspect 35    23    1800 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 .66 .66 73 7.4 .0041 0     false(unreach-call) 1 wit inspect 9.0  4.8  330 0   0     false(unreach-call) 1 --- inspect 51     29     1400   .66 0   false(unreach-call) 1 --- inspect 61    42    2300 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    23    .31 0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .61 .61 72 5.8 .0041 0     false(unreach-call) 1 wit inspect 8.3  4.4  310 0   0     false(unreach-call) 1 --- inspect 39     22     1200   .66 0   false(unreach-call) 1 --- inspect 45    28    1800 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 .64 .64 73 5.8 .0041 0     false(unreach-call) 1 wit inspect 8.9  4.6  320 0   0     false(unreach-call) 1 --- inspect 39     23     1100   .66 0   false(unreach-call) 1 --- inspect 44    29    2300 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 .65 .65 72 5.8 .0041 0     false(unreach-call) 1 wit inspect 9.6  5.1  330 0   0     false(unreach-call) 1 --- inspect 44     25     1200   .66 0   false(unreach-call) 1 --- inspect 43    29    2000 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    22    .48 .074 - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 .65 73 6.0 .0041 0     false(unreach-call) 1 wit inspect 10    5.4  320 0   0     false(unreach-call) 1 --- inspect 48     27     1400   .62 0   false(unreach-call) 1 --- inspect 63    41    2600 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    22    .50 0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .75 .75 74 7.3 .0041 0     false(unreach-call) 1 wit inspect 10    5.2  340 0   0     false(unreach-call) 1 --- inspect 65     37     2000   .62 0   timeout (false(unreach-call)) 0 --- inspect 90    67    2600 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 .72 .72 73 7.6 .0041 0     false(unreach-call) 1 wit inspect 9.4  4.9  340 0   0     false(unreach-call) 1 --- inspect 46     27     1700   .62 0   false(unreach-call) 1 --- inspect 53    36    2300 0   0   false(unreach-call) 1 --- inspect 1.1    1.2    23    .45 0     - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .72 .72 72 6.6 .0041 0     false(unreach-call) 1 wit inspect 9.9  5.2  350 0   0     false(unreach-call) 1 --- inspect 43     26     1800   .66 0   false(unreach-call) 1 --- inspect 63    42    2500 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 .75 .75 73 8.4 .0041 0     false(unreach-call) 1 wit inspect 9.8  5.1  350 0   0     false(unreach-call) 1 --- inspect 46     27     1900   .62 0   false(unreach-call) 1 --- inspect 61    43    2400 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    23    .47 .074 - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .73 .73 72 11   .0041 0     false(unreach-call) 1 wit inspect 9.5  5.0  360 0   0     false(unreach-call) 1 --- inspect 54     32     2300   .62 0   false(unreach-call) 1 --- inspect 47    32    2400 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    24    .47 0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .78 .78 73 7.6 .0041 0     false(unreach-call) 1 wit inspect 11    5.7  380 0   0     false(unreach-call) 1 --- inspect 61     35     1700   .62 0   false(unreach-call) 1 --- inspect 67    45    2600 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    24    .50 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .79 .79 73 8.4 .0041 0     false(unreach-call) 1 wit inspect 10    5.5  380 0   0     false(unreach-call) 1 --- inspect 60     35     2400   .62 0   false(unreach-call) 1 --- inspect 52    36    2400 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 .73 .73 73 7.2 .0041 0     false(unreach-call) 1 wit inspect 9.9  5.1  340 0   0     false(unreach-call) 1 --- inspect 45     27     1800   .62 0   false(unreach-call) 1 --- inspect 58    38    2600 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 .76 .76 73 6.5 .0041 0     false(unreach-call) 1 wit inspect 9.5  5.1  350 0   0     false(unreach-call) 1 --- inspect 41     25     1800   .62 0   false(unreach-call) 1 --- inspect 58    39    2600 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    24    .48 .074 - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .79 .79 73 9.3 .0041 .057 false(unreach-call) 1 wit inspect 10    5.5  380 0   0     false(unreach-call) 1 --- inspect 68     39     1600   .62 0   false(unreach-call) 1 --- inspect 66    44    2600 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    24    .50 0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .79 .79 73 8.8 .0041 0     false(unreach-call) 1 wit inspect 11    5.6  390 0   0     false(unreach-call) 1 --- inspect 44     25     1900   .62 0   false(unreach-call) 1 --- inspect 88    61    2600 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    24    .50 0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .90 .90 75 9.9 .0041 0     false(unreach-call) 1 wit inspect 11    5.9  410 0   0     false(unreach-call) 1 --- inspect 64     39     2600   .62 0   false(unreach-call) 1 --- inspect 88    65    2600 0   0   false(unreach-call) 1 --- inspect 1.3    1.3    24    .56 .082 - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .60 .60 72 6.8 .0041 0     false(unreach-call) 1 wit inspect 8.5  4.5  320 0   0     false(unreach-call) 1 --- inspect 41     23     1300   .66 0   false(unreach-call) 1 --- inspect 38    25    1900 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .46 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 .65 72 7.2 .0041 0     false(unreach-call) 1 wit inspect 9.5  5.0  290 0   0     false(unreach-call) 1 --- inspect 39     23     1300   .66 0   false(unreach-call) 1 --- inspect 58    42    2300 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .48 0     - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .67 .67 73 6.6 .0041 .057 false(unreach-call) 1 wit inspect 8.8  4.6  330 0   0     false(unreach-call) 1 --- inspect 36     21     1200   .66 0   false(unreach-call) 1 --- inspect 43    30    2100 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    23    .49 .074 - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .68 .68 73 7.2 .0041 0     false(unreach-call) 1 wit inspect 9.7  5.1  330 0   0     false(unreach-call) 1 --- inspect 47     26     1400   .66 0   false(unreach-call) 1 --- inspect 54    40    2400 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    23    .51 0     - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .76 .75 74 7.2 .0041 0     false(unreach-call) 1 wit inspect 10    5.2  350 0   0     false(unreach-call) 1 --- inspect 58     33     2100   .62 0   timeout (false(unreach-call)) 0 --- inspect 92    68    2700 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    23    .57 0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 510    510    15000 6500   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 520    520    15000 6200   .0082 .057 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 630    630    15000 8100   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .35 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0    
elevator_spec13_product24_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 630    630    15000 7700   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 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 510    510    15000 7300   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .028 .028 5.6 0    0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 520    510    15000 6800   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0    
elevator_spec13_product31_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 640    640    15000 8200   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 630    630    15000 7400   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 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 630    630    15000 8600   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .030 5.5 0    0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .73 .73 72 7.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    12    690 0   0   out of memory 0 --- inspect 270     190     7000   .64 .033
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .72 .72 72 6.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    10    690 0   0   out of memory 0 --- inspect 290     210     7000   .62 0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .73 .72 72 6.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    10    680 0   0   out of memory 0 --- inspect 280     200     7000   .66 0    
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .81 .81 72 9.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 26    15    1100 0   0   out of memory 0 --- inspect 250     170     7000   .63 0    
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .72 .72 72 6.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23    13    720 0   0   out of memory 0 --- inspect 300     210     7000   .63 0    
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .80 .80 72 7.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    16    1100 0   0   out of memory 0 --- inspect 220     150     7000   .65 0    
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .62 .62 72 6.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 66    54    1700 0   0   out of memory 0 --- inspect 290     210     7000   .64 0    
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .66 .66 72 7.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 78    67    1700 0   0   out of memory 0 --- inspect 310     220     7000   .65 0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .63 .63 72 6.4 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 73    61    1700 0   0   out of memory 0 --- inspect 250     170     7000   .64 0    
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .69 .69 72 7.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 92    78    1800 0   0   out of memory 0 --- inspect 270     180     7000   .64 0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .63 .63 72 6.2 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 88    76    1800 0   0   out of memory 0 --- inspect 240     170     7000   .64 0    
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .68 .68 73 6.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 100    89    1900 0   0   out of memory 0 --- inspect 290     210     7000   .63 0    
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .69 .69 72 6.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 140    130    2300 0   0   out of memory 0 --- inspect 250     170     7000   .63 0    
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .71 .71 73 7.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 140    130    2300 0   0   out of memory 0 --- inspect 320     230     7000   .64 0    
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .64 .64 72 9.1 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 95    80    1900 0   0   out of memory 0 --- inspect 260     180     7000   .64 0    
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .70 .70 73 8.9 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 94    82    2000 0   0   out of memory 0 --- inspect 310     220     7000   .63 0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .70 .70 72 6.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 280    270    2400 0   0   out of memory 0 --- inspect 190     130     7000   .63 0    
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .72 .73 74 8.1 .0041 .44  - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 170    150    2400 0   0   out of memory 0 --- inspect 310     220     7000   .64 0    
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .56 .56 72 5.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 30    20    1100 0   0   out of memory 0 --- inspect 180     110     7000   .64 0    
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .61 .61 72 5.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    21    1100 0   0   out of memory 0 --- inspect 180     120     7000   .65 0    
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .55 .55 72 7.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    22    1100 0   0   out of memory 0 --- inspect 180     120     7000   .66 0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .57 .57 72 6.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    28    1200 0   0   out of memory 0 --- inspect 210     140     7000   .64 0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .57 .57 72 5.4 .0041 .057 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    24    1200 0   0   out of memory 0 --- inspect 200     130     7000   .65 0    
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .59 .59 73 6.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 34    24    1200 0   0   out of memory 0 --- inspect 220     150     7000   .65 0    
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .58 .58 73 5.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 45    34    1300 0   0   out of memory 0 --- inspect 220     150     7000   .63 0    
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .62 .62 73 5.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 49    38    1500 0   0   out of memory 0 --- inspect 280     200     7000   .64 0    
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .56 .56 71 6.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    29    1200 0   0   out of memory 0 --- inspect 200     130     7000   .65 0    
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .60 .60 73 5.4 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    30    1200 0   0   out of memory 0 --- inspect 230     150     7000   1.0  0    
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .60 .60 73 4.9 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 61    49    1500 0   0   out of memory 0 --- inspect 200     130     7000   .64 0    
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .66 .66 73 5.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 49    37    1600 0   0   out of memory 0 --- inspect 300     210     7000   .64 0    
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .76 .76 72 7.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    660 0   0   out of memory 0 --- inspect 160     100     7000   .63 0    
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .77 .77 72 7.4 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    10    650 0   0   out of memory 0 --- inspect 160     100     7000   .66 0    
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .76 .76 72 7.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    680 0   0   out of memory 0 --- inspect 160     100     7000   .65 0    
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect .76 .76 72 9.2 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    13    840 0   0   out of memory 0 --- inspect 210     140     7000   .63 0    
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .83 .83 73 11   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    900 0   0   out of memory 0 --- inspect 210     140     7000   .64 0    
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect .86 .86 72 11   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    15    1400 0   0   out of memory 0 --- inspect 260     190     7000   .64 0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .77 .77 72 7.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23    13    710 0   0   out of memory 0 --- inspect 170     110     7000   .65 .053
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect .78 .78 73 8.2 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23    13    920 0   0   out of memory 0 --- inspect 210     140     7000   .66 0    
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .84 .84 73 7.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    890 0   0   out of memory 0 --- inspect 250     170     7000   .97 0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect .85 .85 73 9.2 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 29    16    1600 0   0   out of memory 0 --- inspect 220     160     7000   .59 0    
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .61 .61 72 4.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    21    1100 0   0   out of memory 0 --- inspect 170     110     7000   .63 0    
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .58 .58 73 7.4 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 43    30    1100 0   0   out of memory 0 --- inspect 200     130     7000   .65 0    
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .56 .56 72 6.3 .0041 .057 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    24    1200 0   0   out of memory 0 --- inspect 220     150     7000   .65 0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .59 .59 72 6.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    28    1300 0   0   out of memory 0 --- inspect 180     120     7000   .65 0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .61 .61 73 5.2 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 76    62    1500 0   0   out of memory 0 --- inspect 210     140     7000   .64 0    
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .61 .61 73 6.1 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 59    47    1600 0   0   out of memory 0 --- inspect 250     170     7000   .65 0    
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.5  1.5  85 19   .012  0     false(unreach-call) 1 wit inspect 7.5  4.0  310 0   0     unknown 0 --- inspect 74     50     1300   .71 0   unknown 0 --- inspect 8.1  4.4  350 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    21    .48 0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.6  1.6  85 17   .012  0     false(unreach-call) 1 wit inspect 8.5  4.5  300 0   0     unknown 0 --- inspect 84     58     1400   .68 0   unknown 0 --- inspect 12    6.3  430 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .50 0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.4  2.4  110 30   .012  0     false(unreach-call) 1 wit inspect 7.4  3.9  320 0   0     unknown 0 --- inspect 68     49     1200   .71 0   unknown 0 --- inspect 9.1  4.9  430 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .50 0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.5  2.5  110 30   .012  .057 false(unreach-call) 1 wit inspect 7.8  4.1  300 0   0     unknown 0 --- inspect 79     58     1400   .68 0   unknown 0 --- inspect 11    6.1  430 0   0   false(unreach-call) 1 --- inspect 1.1    1.2    22    .52 .066 - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.7  1.6  88 17   .012  0     false(unreach-call) 1 wit inspect 8.1  4.3  300 0   0     unknown 0 --- inspect 77     54     1400   .71 0   unknown 0 --- inspect 8.4  4.6  390 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .51 0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.9  2.9  120 31   .012  0     false(unreach-call) 1 wit inspect 7.7  4.1  290 0   0     timeout 0 --- inspect 95     68     1400   .71 0   unknown 0 --- inspect 10    5.6  410 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .52 0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.7  1.7  90 19   .012  0     false(unreach-call) 1 wit inspect 7.5  4.0  280 0   0     timeout 0 --- inspect 98     70     1500   .75 0   unknown 0 --- inspect 9.5  5.1  430 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .52 0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0  3.0  120 33   .012  0     false(unreach-call) 1 wit inspect 8.4  4.4  310 0   0     timeout 0 --- inspect 97     67     1400   1.2  0   unknown 0 --- inspect 8.8  4.8  430 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    22    .54 0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 19    19    2100 240   .012  0     false(unreach-call) 1 wit inspect 8.6  4.5  320 0   0     timeout 0 --- inspect 97     71     1800   .75 0   unknown 0 --- inspect 13    7.0  440 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    22    .58 .074 - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .97 .97 75 9.4 .012  0     false(unreach-call) 1 wit inspect 7.5  4.0  300 0   0     unknown 0 --- inspect 63     45     1200   .68 0   unknown 0 --- inspect 9.2  5.0  440 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .49 0     - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .98 .98 75 9.8 .012  0     false(unreach-call) 1 wit inspect 7.6  4.1  300 0   0     unknown 0 --- inspect 88     61     1400   .68 0   unknown 0 --- inspect 13    6.7  410 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    22    .41 0     - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .99 .99 75 8.3 .012  0     false(unreach-call) 1 wit inspect 7.2  3.8  280 0   0     unknown 0 --- inspect 79     56     1200   .71 0   unknown 0 --- inspect 11    6.0  410 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .50 0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.0  .99 75 9.2 .012  0     false(unreach-call) 1 wit inspect 8.2  4.3  300 0   0     unknown 0 --- inspect 86     62     1300   .71 0   unknown 0 --- inspect 9.6  5.2  430 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .51 0     - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .97 .96 75 9.3 .012  0     false(unreach-call) 1 wit inspect 7.7  4.1  310 0   0     timeout 0 --- inspect 95     66     1400   .71 0   unknown 0 --- inspect 12    6.5  430 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .51 0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.0  1.0  76 8.3 .012  0     false(unreach-call) 1 wit inspect 7.9  4.2  310 0   0     timeout 0 --- inspect 97     71     1500   1.2  0   unknown 0 --- inspect 9.5  5.1  420 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .52 0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.0  1.0  76 9.5 .012  0     false(unreach-call) 1 wit inspect 7.9  4.2  300 0   0     timeout 0 --- inspect 97     69     1400   .71 0   unknown 0 --- inspect 11    6.1  430 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .51 0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .99 .98 76 9.6 .012  0     false(unreach-call) 1 wit inspect 8.2  4.4  310 0   0     timeout 0 --- inspect 97     68     1400   .77 0   unknown 0 --- inspect 10    5.5  440 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .53 0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.5  3.5  290 42   .012  0     false(unreach-call) 1 wit inspect 9.5  5.0  320 0   0     timeout 0 --- inspect 97     72     1800   1.5  0   unknown 0 --- inspect 15    7.8  440 0   0   false(unreach-call) 1 --- inspect 1.2    1.2    22    .57 0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.9  5.8  350 72   .012  0     false(unreach-call) 1 wit inspect 8.5  4.5  320 0   0     true -32 --- inspect 20     11     520   .62 0   unknown 0 --- inspect 12    6.4  440 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .50 0     - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11    11    630 160   .012  0     false(unreach-call) 1 wit inspect 8.1  4.3  320 0   0     true -32 --- inspect 17     9.3   520   .62 0   unknown 0 --- inspect 12    6.6  440 0   0   false(unreach-call) 1 --- inspect 1.1    1.1    22    .49 .066 - --- inspect - ---