Tool symbiotic 6.0.3-77d4af47 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* [apollon013; apollon098] 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-07 21:42:05 CET 2018-12-08 23:40:56 CET 2018-12-09 00:46:04 CET 2018-12-09 01:29:54 CET 2018-12-12 21:10:03 CET 2018-12-08 22:46:12 CET 2018-12-08 23:47:25 CET
Run set symbiotic.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options --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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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 .49 .49 31 5.8 0     0     false(unreach-call) 1 wit inspect 8.8 4.6 310 0   0      true -32 --- inspect 15   9.1 500 .62 0   false(unreach-call) 1 --- inspect 7.4 4.0 270 0   0     false(unreach-call) 1 --- inspect .88 .88 20 .34 .070 - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .47 31 6.9 0     0     false(unreach-call) 1 wit inspect 7.6 4.1 320 0   0      true -32 --- inspect 15   8.8 470 .62 0   false(unreach-call) 1 --- inspect 6.1 3.4 270 0   0     false(unreach-call) 1 --- inspect .85 .85 20 .35 0     - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .48 31 5.5 0     0     false(unreach-call) 1 wit inspect 8.1 4.3 310 0   .074  true -32 --- inspect 17   9.8 470 .62 0   false(unreach-call) 1 --- inspect 6.0 3.3 270 0   .074 false(unreach-call) 1 --- inspect .85 .85 20 .34 0     - --- inspect - --- inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .47 32 5.3 0     0     false(unreach-call) 1 wit inspect 8.6 4.5 320 0   0      true -32 --- inspect 18   10   470 .62 0   false(unreach-call) 1 --- inspect 5.8 3.2 270 0   0     false(unreach-call) 1 --- inspect .84 .84 20 .35 .074 - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .60 .59 36 7.3 0     0     false(unreach-call) 1 wit inspect 15   8.2 490 0   0      true -32 --- inspect 19   11   520 .62 0   unknown 0 --- inspect 6.3 3.5 270 0   0     true -32 --- inspect .87 .86 20 .38 0     - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .49 31 5.4 0     0     false(unreach-call) 1 wit inspect 7.7 4.1 310 0   0      true -32 --- inspect 16   9.4 500 .62 0   false(unreach-call) 1 --- inspect 5.9 3.2 280 0   0     false(unreach-call) 1 --- inspect .85 .85 20 .34 .074 - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .48 31 6.1 0     0     false(unreach-call) 1 wit inspect 9.6 5.1 330 0   0      true -32 --- inspect 16   9.0 530 .62 0   false(unreach-call) 1 --- inspect 6.2 3.4 270 0   0     false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .49 31 5.9 0     0     false(unreach-call) 1 wit inspect 9.4 5.0 330 0   0      true -32 --- inspect 16   9.1 520 .62 0   false(unreach-call) 1 --- inspect 5.9 3.3 270 0   0     false(unreach-call) 1 --- inspect .90 .91 20 .23 0     - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .52 .52 32 6.1 0     0     false(unreach-call) 1 wit inspect 8.4 4.5 340 0   0      true -32 --- inspect 15   8.8 530 .62 0   false(unreach-call) 1 --- inspect 6.0 3.3 270 0   0     false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .48 31 5.9 0     0     false(unreach-call) 1 wit inspect 7.4 3.9 320 0   0      true -32 --- inspect 15   8.5 510 .62 0   false(unreach-call) 1 --- inspect 7.4 4.1 280 0   .41  false(unreach-call) 1 --- inspect .84 .84 20 .35 0     - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .50 .50 32 6.8 0     0     false(unreach-call) 1 wit inspect 8.2 4.3 330 0   .074  true -32 --- inspect 15   9.0 510 .62 0   false(unreach-call) 1 --- inspect 5.7 3.2 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 .50 .49 32 7.3 0     0     false(unreach-call) 1 wit inspect 10   5.5 330 0   0      true -32 --- inspect 18   10   480 .62 0   false(unreach-call) 1 --- inspect 7.0 3.8 270 0   .16  false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .50 .49 32 6.9 0     0     false(unreach-call) 1 wit inspect 8.2 4.3 340 0   .053  true -32 --- inspect 16   9.4 470 .62 0   false(unreach-call) 1 --- inspect 6.1 3.4 270 0   .43  false(unreach-call) 1 --- inspect .86 .86 20 .36 0     - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .64 .63 36 7.5 0     0     false(unreach-call) 1 wit inspect 51   36   2000 0   0      true -32 --- inspect 18   11   470 .62 0   unknown 0 --- inspect 6.6 3.7 270 0   0     true -32 --- inspect .87 .87 20 .39 0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .47 30 5.8 0     0     false(unreach-call) 1 wit inspect 7.3 3.9 300 0   0      true -32 --- inspect 16   9.4 510 .62 0   false(unreach-call) 1 --- inspect 6.2 3.4 280 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 .49 .48 30 6.7 0     0     false(unreach-call) 1 wit inspect 8.9 4.7 320 0   0      true -32 --- inspect 15   9.1 460 .62 0   false(unreach-call) 1 --- inspect 6.1 3.4 270 0   0     false(unreach-call) 1 --- inspect .87 .87 20 .36 0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .47 30 5.7 0     0     false(unreach-call) 1 wit inspect 8.2 4.3 320 0   0      true -32 --- inspect 16   9.6 470 .62 0   false(unreach-call) 1 --- inspect 5.9 3.2 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 .50 .50 31 6.0 0     0     false(unreach-call) 1 wit inspect 9.6 5.1 350 0   0      true -32 --- inspect 15   9.0 530 .62 0   false(unreach-call) 1 --- inspect 6.0 3.3 280 0   0     false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .47 30 5.9 0     0     false(unreach-call) 1 wit inspect 7.6 4.0 300 0   0      true -32 --- inspect 16   9.0 460 .62 0   false(unreach-call) 1 --- inspect 6.9 3.8 280 0   .074 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 .49 .48 31 7.3 0     0     false(unreach-call) 1 wit inspect 9.0 4.7 320 0   0      true -32 --- inspect 18   10   460 .62 0   false(unreach-call) 1 --- inspect 6.3 3.5 270 0   0     false(unreach-call) 1 --- inspect .89 .91 20 .36 0     - --- inspect - --- inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .49 31 6.1 0     0     false(unreach-call) 1 wit inspect 9.3 5.0 320 0   0      true -32 --- inspect 16   9.3 510 .62 0   false(unreach-call) 1 --- inspect 6.0 3.3 270 0   0     false(unreach-call) 1 --- inspect .86 .87 20 .34 0     - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .48 31 7.8 0     0     false(unreach-call) 1 wit inspect 7.6 4.1 350 0   0      true -32 --- inspect 18   10   460 .62 0   false(unreach-call) 1 --- inspect 6.5 3.6 280 0   0     false(unreach-call) 1 --- inspect .85 .86 20 .36 0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .60 .59 35 7.0 0     0     false(unreach-call) 1 wit inspect 44   30   2000 0   0      true -32 --- inspect 19   11   520 .62 0   unknown 0 --- inspect 6.7 3.7 270 0   0     true -32 --- inspect .87 .87 20 .39 0     - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .50 .49 34 6.7 0     0     false(unreach-call) 1 wit inspect 9.3 4.8 380 0   0      true -32 --- inspect 14   8.5 510 .62 0   false(unreach-call) 1 --- inspect 6.1 3.4 280 0   0     false(unreach-call) 1 --- inspect .85 .85 21 .34 .074 - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .50 .49 35 5.8 0     0     false(unreach-call) 1 wit inspect 8.4 4.4 370 0   0      true -32 --- inspect 14   8.4 470 .62 0   false(unreach-call) 1 --- inspect 6.0 3.3 270 0   0     false(unreach-call) 1 --- inspect .84 .84 20 .34 0     - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .48 34 7.1 0     0     false(unreach-call) 1 wit inspect 9.7 5.1 370 0   0      true -32 --- inspect 16   9.4 520 .62 0   false(unreach-call) 1 --- inspect 6.0 3.4 270 0   1.9   false(unreach-call) 1 --- inspect .84 .84 20 .35 0     - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .50 35 5.8 0     0     false(unreach-call) 1 wit inspect 8.5 4.5 380 0   0      true -32 --- inspect 16   9.4 470 .62 0   false(unreach-call) 1 --- inspect 6.0 3.4 270 0   .074 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 .53 .52 35 6.0 0     0     false(unreach-call) 1 wit inspect 10   5.5 420 0   0      true -32 --- inspect 15   8.8 530 .62 0   false(unreach-call) 1 --- inspect 5.5 3.1 270 0   .078 false(unreach-call) 1 --- inspect .88 .88 20 .36 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .52 .51 36 6.4 0     0     false(unreach-call) 1 wit inspect 12   6.5 420 0   0      true -32 --- inspect 15   9.1 530 .62 0   false(unreach-call) 1 --- inspect 6.2 3.5 270 0   0     false(unreach-call) 1 --- inspect .88 .88 20 .36 .078 - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .52 .51 35 7.8 0     0     false(unreach-call) 1 wit inspect 8.6 4.6 370 0   0      true -32 --- inspect 15   9.1 470 .62 0   false(unreach-call) 1 --- inspect 5.7 3.2 270 0   0     false(unreach-call) 1 --- inspect .87 .87 20 .35 .074 - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .50 37 5.9 0     0     false(unreach-call) 1 wit inspect 8.9 4.7 390 0   0      true -32 --- inspect 17   10   460 .62 0   false(unreach-call) 1 --- inspect 6.1 3.4 270 0   0     false(unreach-call) 1 --- inspect .85 .85 21 .36 0     - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .50 36 6.2 0     0     false(unreach-call) 1 wit inspect 9.2 4.9 400 0   0      true -32 --- inspect 16   9.5 470 .62 0   false(unreach-call) 1 --- inspect 5.8 3.2 270 0   0     false(unreach-call) 1 --- inspect .89 .91 20 .26 0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .52 .51 37 6.0 0     0     false(unreach-call) 1 wit inspect 10   5.5 440 0   0      true -32 --- inspect 17   9.7 470 .62 0   false(unreach-call) 1 --- inspect 6.0 3.3 270 0   0     false(unreach-call) 1 --- inspect .86 .86 20 .36 .078 - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .64 .63 41 7.4 0     0     false(unreach-call) 1 wit inspect 30   18   840 0   0      true -32 --- inspect 18   10   520 .62 0   unknown 0 --- inspect 6.5 3.7 270 0   0     true -32 --- inspect .87 .87 20 .39 0     - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .47 31 6.5 0     0     false(unreach-call) 1 wit inspect 8.3 4.4 320 0   0      true -32 --- inspect 16   9.4 500 .62 0   false(unreach-call) 1 --- inspect 7.5 4.1 270 0   0     false(unreach-call) 1 --- inspect .85 .85 21 .34 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .48 31 6.6 0     0     false(unreach-call) 1 wit inspect 8.4 4.5 320 0   0      true -32 --- inspect 16   9.3 520 .62 0   false(unreach-call) 1 --- inspect 5.7 3.1 270 0   .074 false(unreach-call) 1 --- inspect .85 .85 20 .36 0     - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .48 31 5.9 0     .28  false(unreach-call) 1 wit inspect 8.3 4.4 330 0   0      true -32 --- inspect 14   8.7 520 .62 0   false(unreach-call) 1 --- inspect 6.3 3.4 270 0   0     false(unreach-call) 1 --- inspect .87 .87 20 .36 0     - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .50 .49 31 6.9 0     0     false(unreach-call) 1 wit inspect 8.7 4.6 350 0   0      true -32 --- inspect 16   9.3 530 .62 0   false(unreach-call) 1 --- inspect 6.0 3.3 270 0   0     false(unreach-call) 1 --- inspect .88 .88 20 .36 0     - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .60 .59 36 7.5 0     0     false(unreach-call) 1 wit inspect 49   33   2000 0   0      true -32 --- inspect 18   10   470 .62 0   unknown 0 --- inspect 6.5 3.6 270 0   0     true -32 --- inspect .88 .88 20 .39 0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 110    120    15000 1600   .14  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 42 0   0     error (2) 0 --- inspect .022 .024 5.6 0    0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 110    120    15000 1800   .16  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 42 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 110    120    15000 1700   .14  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_product24_true-unreach-call_false-termination.cil.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 110    120    15000 1600   .25  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0    
elevator_spec13_product29_true-unreach-call_false-termination.cil.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 110    120    15000 1500   .19  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0     error (2) 0 --- inspect .021 .023 5.7 0    0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 110    120    15000 1700   .26  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0    
elevator_spec13_product31_true-unreach-call_false-termination.cil.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 110    120    15000 1500   .28  4.6   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 40 0   0     error (2) 0 --- inspect .021 .023 5.7 0    0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 110    120    15000 1600   .26  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0    
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 110    120    15000 1600   .14  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 29 3.2 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.9  680 0   0     out of memory 0 --- inspect 300     210     7000   .65 0    
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 30 5.0 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.9  690 0   0     out of memory 0 --- inspect 310     220     7000   1.5  0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 29 5.2 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25    14    710 0   0     out of memory 0 --- inspect 260     180     7000   .63 0    
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 30 4.5 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25    15    1100 0   0     out of memory 0 --- inspect 220     150     7000   .69 0    
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 30 5.2 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    10    710 0   .025 out of memory 0 --- inspect 270     190     7000   .65 0    
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .38 31 4.7 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    16    1100 0   0     out of memory 0 --- inspect 200     130     7000   .66 0    
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 29 4.3 0     .41  - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 73    60    1600 0   0     out of memory 0 --- inspect 270     190     7000   .64 0    
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 30 4.6 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 78    67    1800 0   0     out of memory 0 --- inspect 280     200     7000   .72 0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 29 5.0 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 77    63    1700 0   0     out of memory 0 --- inspect 240     170     7000   .64 0    
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .40 .39 31 4.4 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 97    85    1800 0   .090 out of memory 0 --- inspect 290     200     7000   .66 0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 .39 30 4.2 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 89    76    1700 0   0     out of memory 0 --- inspect 250     170     7000   1.4  0    
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 30 5.0 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 94    83    1900 0   0     out of memory 0 --- inspect 320     220     7000   .65 0    
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 30 4.5 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 160    150    2300 0   0     out of memory 0 --- inspect 220     150     7000   .66 0    
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 31 4.7 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 160    150    2300 0   0     out of memory 0 --- inspect 250     180     7000   .65 0    
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 .38 30 4.9 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 90    76    1900 0   0     out of memory 0 --- inspect 220     150     7000   .66 .020
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 31 5.2 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 120    110    2000 0   0     out of memory 0 --- inspect 290     200     7000   .71 0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 31 4.6 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 360    350    2300 0   0     out of memory 0 --- inspect 280     190     7000   .64 0    
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 32 4.2 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 190    170    2400 0   0     out of memory 0 --- inspect 310     220     7000   1.3  0    
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 28 4.4 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 29    20    1000 0   0     out of memory 0 --- inspect 160     110     7000   .68 0    
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .39 35 4.5 0     5.7   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    21    1100 0   0     out of memory 0 --- inspect 200     130     7000   1.5  0    
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 .35 28 4.2 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    22    1100 0   0     out of memory 0 --- inspect 170     110     7000   .70 0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .37 29 5.0 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    27    1100 0   0     out of memory 0 --- inspect 220     150     7000   .64 0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 28 3.8 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    27    1200 0   0     out of memory 0 --- inspect 170     110     7000   .71 0    
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 30 4.4 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    28    1200 0   0     out of memory 0 --- inspect 240     160     7000   1.7  0    
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 29 4.3 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 57    43    1300 0   0     out of memory 0 --- inspect 190     130     7000   1.3  0    
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .39 35 4.3 0     5.4   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 54    41    1500 0   0     out of memory 0 --- inspect 250     170     7000   .66 0    
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 29 3.8 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    26    1200 0   0     out of memory 0 --- inspect 180     110     7000   .64 0    
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 30 5.0 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 47    35    1200 0   0     out of memory 0 --- inspect 250     160     7000   1.4  0    
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 30 4.4 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 63    49    1500 0   0     out of memory 0 --- inspect 160     100     7000   .72 0    
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .37 31 4.6 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 56    42    1600 0   0     out of memory 0 --- inspect 230     160     7000   .63 0    
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 33 4.9 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    650 0   0     out of memory 0 --- inspect 160     110     7000   1.5  0    
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .43 .42 34 4.5 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    660 0   0     out of memory 0 --- inspect 200     120     7000   .74 .033
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .38 34 4.8 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.7  670 0   .037 out of memory 0 --- inspect 170     110     7000   1.4  0    
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 .38 35 5.6 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    15    840 0   0     out of memory 0 --- inspect 200     130     7000   1.4  0    
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .42 .42 34 4.3 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    900 0   0     out of memory 0 --- inspect 230     160     7000   .64 0    
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect .41 .40 35 5.1 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    18    1400 0   0     out of memory 0 --- inspect 180     120     7000   .65 0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .38 35 4.5 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    10    730 0   0     out of memory 0 --- inspect 180     120     7000   .33 0    
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 .38 35 5.0 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 29    16    910 0   0     out of memory 0 --- inspect 190     130     7000   .71 0    
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 35 4.9 0     .28  - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25    13    900 0   0     out of memory 0 --- inspect 290     190     7000   .64 0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect .44 .44 36 4.9 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    20    1500 0   0     out of memory 0 --- inspect 270     190     7000   .65 0    
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 29 4.2 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    21    1100 0   0     out of memory 0 --- inspect 170     110     7000   1.5  0    
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 30 4.5 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    26    1100 0   0     out of memory 0 --- inspect 190     130     7000   .68 .033
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .37 30 4.2 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 44    30    1200 0   0     out of memory 0 --- inspect 160     110     7000   .72 0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .40 .39 30 4.6 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 43    31    1300 0   .090 out of memory 0 --- inspect 230     150     7000   .29 0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 30 4.4 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 68    56    1500 0   0     out of memory 0 --- inspect 200     140     7000   .65 0    
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .40 .39 31 4.5 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 68    52    1500 0   0     out of memory 0 --- inspect 180     120     7000   .64 0    
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .58 .57 24 7.1 0     0     false(unreach-call) 1 wit inspect 13   6.7 460 0   0      true -32 --- inspect 15   8.5 470 .59 0   unknown 0 --- inspect 5.5 3.1 260 0   0     true -32 --- inspect .83 .83 20 .37 0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .61 .60 31 7.1 0     0     false(unreach-call) 1 wit inspect 15   8.4 500 0   0      true -32 --- inspect 14   7.8 470 .62 0   unknown 0 --- inspect 5.7 3.2 270 0   .066 true -32 --- inspect .84 .84 20 .38 0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .63 .62 25 8.0 0     0     false(unreach-call) 1 wit inspect 9.6 5.2 460 0   0      true -32 --- inspect 14   8.5 490 .62 0   unknown 0 --- inspect 6.0 3.3 280 0   0     true -32 --- inspect .87 .87 20 .37 0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .66 .65 33 9.0 0     0     false(unreach-call) 1 wit inspect 15   8.4 500 0   0      true -32 --- inspect 15   8.7 500 .62 0   unknown 0 --- inspect 5.7 3.2 270 0   0     true -32 --- inspect .85 .85 20 .39 0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .61 .60 27 7.3 0     0     false(unreach-call) 1 wit inspect 13   7.1 460 0   0      true -32 --- inspect 17   9.5 460 .62 0   unknown 0 --- inspect 5.6 3.2 270 0   0     true -32 --- inspect .87 .87 20 .39 0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 .65 28 9.0 0     0     false(unreach-call) 1 wit inspect 10   5.6 470 0   0      true -32 --- inspect 16   9.1 470 .62 0   unknown 0 --- inspect 5.6 3.2 270 0   .066 true -32 --- inspect .85 .85 20 .39 0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .67 .66 35 9.2 0     0     false(unreach-call) 1 wit inspect 14   7.8 520 0   0      true -32 --- inspect 16   9.3 510 .62 0   unknown 0 --- inspect 6.2 3.5 270 0   0     true -32 --- inspect .86 .88 20 .39 0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .69 .68 36 10   0     0     false(unreach-call) 1 wit inspect 14   7.6 520 0   0      true -32 --- inspect 15   8.7 460 .62 0   unknown 0 --- inspect 6.0 3.4 270 0   0     true -32 --- inspect .86 .86 20 .40 0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.3  2.3  84 29   0     0     false(unreach-call) 1 wit inspect 20   11   610 0   0      true -32 --- inspect 15   8.8 510 .62 0   unknown 0 --- inspect 6.2 3.4 270 0   0     true -32 --- inspect .88 .88 20 .43 .074 - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .59 .59 23 7.2 0     0     false(unreach-call) 1 wit inspect 9.7 5.3 460 0   0      true -32 --- inspect 15   8.7 460 .62 0   unknown 0 --- inspect 5.4 3.1 260 0   0     false(unreach-call) 1 --- inspect .83 .83 20 .37 0     - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .60 .60 29 6.6 0     0     false(unreach-call) 1 wit inspect 16   8.1 500 0   0      true -32 --- inspect 15   8.9 490 .62 0   unknown 0 --- inspect 5.8 3.2 270 0   0     false(unreach-call) 1 --- inspect .87 .87 20 .38 0     - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .57 .56 25 8.7 0     0     false(unreach-call) 1 wit inspect 9.1 4.9 460 0   0      true -32 --- inspect 15   8.6 470 .62 0   unknown 0 --- inspect 5.6 3.2 270 0   0     false(unreach-call) 1 --- inspect .83 .83 20 .37 .066 - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .62 .61 32 7.7 0     0     false(unreach-call) 1 wit inspect 15   8.0 510 0   0      true -32 --- inspect 15   8.7 500 .62 0   unknown 0 --- inspect 6.0 3.4 270 0   0     false(unreach-call) 1 --- inspect .86 .86 20 .39 0     - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .61 .60 26 6.7 0     0     false(unreach-call) 1 wit inspect 10   5.5 460 0   0      true -32 --- inspect 14   8.6 510 .62 0   unknown 0 --- inspect 5.5 3.1 270 0   0     false(unreach-call) 1 --- inspect .85 .87 20 .37 .066 - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .61 .61 33 7.7 0     0     false(unreach-call) 1 wit inspect 15   8.1 510 0   0      true -32 --- inspect 15   8.6 500 .62 0   unknown 0 --- inspect 5.9 3.3 270 0   0     false(unreach-call) 1 --- inspect .85 .85 20 .39 0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .59 .59 28 7.8 0     0     false(unreach-call) 1 wit inspect 10   5.4 470 0   0      true -32 --- inspect 16   8.8 470 .62 0   unknown 0 --- inspect 5.9 3.3 270 0   0     false(unreach-call) 1 --- inspect .84 .84 20 .39 0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .63 .62 36 7.4 0     0     false(unreach-call) 1 wit inspect 14   7.6 510 0   0      true -32 --- inspect 15   8.3 460 .62 0   unknown 0 --- inspect 6.0 3.4 270 0   .066 false(unreach-call) 1 --- inspect .85 .85 20 .40 0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  1.3  46 18   0     0     false(unreach-call) 1 wit inspect 28   16   620 0   0      true -32 --- inspect 16   9.1 510 .62 0   unknown 0 --- inspect 6.3 3.5 270 0   0     true -32 --- inspect .89 .89 20 .43 0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .63 .62 27 9.1 0     0     false(unreach-call) 1 wit inspect 12   6.4 470 0   0      true -32 --- inspect 16   8.8 460 .62 0   unknown 0 --- inspect 6.5 3.6 270 0   0     true -32 --- inspect .84 .84 20 .37 0     - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .78 .78 30 11   0     0     false(unreach-call) 1 wit inspect 13   6.7 460 0   0      true -32 --- inspect 14   8.3 470 .62 0   unknown 0 --- inspect 5.6 3.2 260 0   0     true -32 --- inspect .84 .84 20 .37 0     - --- inspect - --- inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .63 .63 24 8.5 0     0     false(unreach-call) 1 wit inspect 10   5.4 460 0   .0041 true -32 --- inspect 15   8.8 460