Tool 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-05 05:46:16 CET 2018-12-06 09:44:44 CET 2018-12-06 10:50:29 CET 2018-12-06 10:57:45 CET 2018-12-12 19:32:16 CET 2018-12-06 08:37:23 CET 2018-12-06 09:52:34 CET
Run set cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options -svcomp19 -heap 10000M -benchmark -timelimit 900s -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/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.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/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.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 9.5 2.8 470 93 .18  0   false(unreach-call) 1 wit inspect 11    6.0  310 0   0   false(unreach-call) 1 --- inspect 28   16   920 .62 0   false(unreach-call) 1 --- inspect 7.4  4.0  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    24    .42 0     - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.9 2.9 480 78 .19  0   false(unreach-call) 1 wit inspect 12    6.1  320 0   0   false(unreach-call) 1 --- inspect 31   17   1100 .62 0   false(unreach-call) 1 --- inspect 7.1  3.9  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .45 0     - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.6 2.8 470 87 .18  0   false(unreach-call) 1 wit inspect 9.4  4.9  330 0   0   false(unreach-call) 1 --- inspect 29   17   920 .66 0   false(unreach-call) 1 --- inspect 7.4  4.0  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    24    .42 0     - --- inspect - --- inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   3.0 370 89 .19  0   false(unreach-call) 1 wit inspect 10    5.4  350 0   0   false(unreach-call) 1 --- inspect 34   19   970 .62 0   false(unreach-call) 1 --- inspect 7.4  4.0  290 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .45 0     - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.1 470 88 .20  0   false(unreach-call) 1 wit inspect 10    5.3  330 0   0   false(unreach-call) 1 --- inspect 33   19   1000 .62 0   unknown 0 --- inspect 7.7  4.2  310 0   0      true -32 --- inspect 1.1    1.1    25    .46 .27  - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   2.9 490 95 .18  0   false(unreach-call) 1 wit inspect 10    5.3  320 0   0   false(unreach-call) 1 --- inspect 32   19   1100 .62 0   false(unreach-call) 1 --- inspect 7.1  3.9  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    24    .44 0     - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.0 380 86 .20  0   false(unreach-call) 1 wit inspect 11    5.5  330 0   0   false(unreach-call) 1 --- inspect 46   26   1300 .62 0   false(unreach-call) 1 --- inspect 7.1  3.9  290 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .45 0     - --- inspect - --- inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   3.0 480 87 .20  0   false(unreach-call) 1 wit inspect 10    5.2  340 0   0   false(unreach-call) 1 --- inspect 42   24   1300 .62 0   false(unreach-call) 1 --- inspect 7.3  3.9  290 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .46 0     - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.0 500 100 .21  0   false(unreach-call) 1 wit inspect 9.4  5.0  350 0   0   false(unreach-call) 1 --- inspect 36   21   1500 .62 0   false(unreach-call) 1 --- inspect 7.4  4.0  300 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    25    .48 0     - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.8 2.9 480 81 .18  0   false(unreach-call) 1 wit inspect 9.6  5.1  320 0   0   false(unreach-call) 1 --- inspect 34   20   1100 .62 0   false(unreach-call) 1 --- inspect 7.0  3.8  310 0   0      false(unreach-call) 1 --- inspect 1.1    1.2    25    .39 0     - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   3.0 490 84 .20  0   false(unreach-call) 1 wit inspect 9.6  5.0  330 0   0   false(unreach-call) 1 --- inspect 36   21   1200 .62 0   false(unreach-call) 1 --- inspect 7.1  3.9  290 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .45 0     - --- inspect - --- inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   2.9 480 83 .20  0   false(unreach-call) 1 wit inspect 10    5.5  340 0   0   false(unreach-call) 1 --- inspect 40   23   1200 .62 0   false(unreach-call) 1 --- inspect 7.4  4.0  290 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .47 0     - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   3.0 480 91 .21  0   false(unreach-call) 1 wit inspect 12    6.4  360 0   0   false(unreach-call) 1 --- inspect 45   25   1500 .66 0   false(unreach-call) 1 --- inspect 7.4  4.0  290 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    25    .48 0     - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   3.3 460 95 .21  0   false(unreach-call) 1 wit inspect 9.9  5.1  350 0   0   false(unreach-call) 1 --- inspect 47   27   1500 .62 0   unknown 0 --- inspect 7.9  4.3  310 0   0      true -32 --- inspect 1.2    1.2    25    .50 0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.9 2.9 470 75 .18  0   false(unreach-call) 1 wit inspect 9.4  5.0  320 0   0   false(unreach-call) 1 --- inspect 37   21   1200 .66 0   false(unreach-call) 1 --- inspect 7.2  3.9  290 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    24    .44 .074 - --- inspect - --- inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   2.9 470 90 .20  0   false(unreach-call) 1 wit inspect 11    5.7  320 0   0   false(unreach-call) 1 --- inspect 32   19   1100 .62 0   false(unreach-call) 1 --- inspect 7.5  4.0  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .45 0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.9 2.9 480 75 .19  0   false(unreach-call) 1 wit inspect 12    6.2  340 0   0   false(unreach-call) 1 --- inspect 36   21   1200 .62 0   false(unreach-call) 1 --- inspect 7.3  4.0  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .47 0     - --- inspect - --- inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   3.0 480 80 .20  0   false(unreach-call) 1 wit inspect 12    6.2  350 0   0   false(unreach-call) 1 --- inspect 42   24   1500 .62 0   false(unreach-call) 1 --- inspect 7.0  3.8  290 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    25    .48 0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.9 2.8 490 93 .18  0   false(unreach-call) 1 wit inspect 11    5.6  320 0   0   false(unreach-call) 1 --- inspect 38   22   1200 .62 0   false(unreach-call) 1 --- inspect 7.0  3.8  290 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    24    .44 0     - --- inspect - --- inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   3.1 490 88 .20  0   false(unreach-call) 1 wit inspect 12    6.2  330 0   0   false(unreach-call) 1 --- inspect 35   20   1100 .62 0   false(unreach-call) 1 --- inspect 7.6  4.2  290 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .45 0     - --- inspect - --- inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   2.9 480 84 .19  0   false(unreach-call) 1 wit inspect 10    5.4  320 0   0   false(unreach-call) 1 --- inspect 37   21   1100 .62 0   false(unreach-call) 1 --- inspect 7.5  4.1  300 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    25    .47 0     - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   3.1 360 94 .20  0   false(unreach-call) 1 wit inspect 10    5.3  350 0   0   false(unreach-call) 1 --- inspect 41   23   1200 .62 0   false(unreach-call) 1 --- inspect 7.0  3.8  290 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    25    .48 0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   3.3 480 91 .20  0   false(unreach-call) 1 wit inspect 11    5.7  330 0   0   false(unreach-call) 1 --- inspect 47   28   1500 .62 0   unknown 0 --- inspect 7.3  4.0  290 0   0      true -32 --- inspect 1.1    1.1    25    .50 0     - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 380 91 .28  0   false(unreach-call) 1 wit inspect 11    6.0  380 0   0   false(unreach-call) 1 --- inspect 40   24   1800 .66 0   false(unreach-call) 1 --- inspect 7.9  4.3  300 0   .086  false(unreach-call) 1 --- inspect 1.2    1.2    27    .44 0     - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 380 90 .28  0   false(unreach-call) 1 wit inspect 11    5.9  380 0   0   false(unreach-call) 1 --- inspect 41   25   1900 .62 0   false(unreach-call) 1 --- inspect 8.0  4.4  300 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    27    .44 0     - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 490 99 .28  0   false(unreach-call) 1 wit inspect 11    5.6  390 0   0   false(unreach-call) 1 --- inspect 41   25   1700 .62 0   false(unreach-call) 1 --- inspect 8.5  4.5  320 0   .086  false(unreach-call) 1 --- inspect 1.2    1.2    27    .45 .074 - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 490 93 .29  0   false(unreach-call) 1 wit inspect 13    6.7  400 0   0   false(unreach-call) 1 --- inspect 50   30   2400 .62 0   false(unreach-call) 1 --- inspect 7.8  4.2  290 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    27    .45 0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 500 89 .30  0   false(unreach-call) 1 wit inspect 12    6.4  420 0   0   false(unreach-call) 1 --- inspect 53   31   1800 .62 0   false(unreach-call) 1 --- inspect 7.9  4.3  300 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    27    .47 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.3 480 95 .31  0   false(unreach-call) 1 wit inspect 13    7.0  420 0   0   false(unreach-call) 1 --- inspect 61   36   1900 .62 0   false(unreach-call) 1 --- inspect 7.7  4.2  290 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    27    .48 0     - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 490 100 .28  0   false(unreach-call) 1 wit inspect 11    5.7  390 0   0   false(unreach-call) 1 --- inspect 46   27   1600 .62 0   false(unreach-call) 1 --- inspect 7.2  3.9  290 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    27    .45 0     - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 490 98 .29  0   false(unreach-call) 1 wit inspect 11    5.7  390 0   0   false(unreach-call) 1 --- inspect 43   26   1800 .62 0   false(unreach-call) 1 --- inspect 8.1  4.4  300 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    27    .45 0     - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 490 83 .30  0   false(unreach-call) 1 wit inspect 12    6.3  410 0   0   false(unreach-call) 1 --- inspect 57   33   1900 .62 0   false(unreach-call) 1 --- inspect 7.7  4.2  300 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    27    .47 0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 490 100 .31  0   false(unreach-call) 1 wit inspect 11    6.0  430 0   0   false(unreach-call) 1 --- inspect 38   22   1900 .62 0   false(unreach-call) 1 --- inspect 7.8  4.2  290 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    27    .48 0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   3.7 460 120 .31  0   false(unreach-call) 1 wit inspect 10    5.4  410 0   0   false(unreach-call) 1 --- inspect 63   37   2300 .62 0   unknown 0 --- inspect 8.4  4.6  300 0   0      true -32 --- inspect 1.2    1.2    27    .50 .082 - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   2.9 490 91 .19  0   false(unreach-call) 1 wit inspect 11    5.5  330 0   0   false(unreach-call) 1 --- inspect 34   20   1100 .62 0   false(unreach-call) 1 --- inspect 7.2  4.0  290 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .45 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   3.0 480 84 .21  0   false(unreach-call) 1 wit inspect 9.7  5.1  330 0   0   false(unreach-call) 1 --- inspect 38   22   1400 .62 0   false(unreach-call) 1 --- inspect 7.5  4.1  290 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    25    .46 0     - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   2.9 490 90 .20  0   false(unreach-call) 1 wit inspect 9.3  5.0  340 0   0   false(unreach-call) 1 --- inspect 39   23   1200 .62 0   false(unreach-call) 1 --- inspect 7.3  4.0  290 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    25    .48 0     - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   3.0 490 90 .22  0   false(unreach-call) 1 wit inspect 12    6.2  350 0   0   false(unreach-call) 1 --- inspect 40   24   1300 .62 0   false(unreach-call) 1 --- inspect 7.4  4.0  290 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    25    .49 0     - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   3.4 470 100 .22  0   false(unreach-call) 1 wit inspect 12    6.2  340 0   0   false(unreach-call) 1 --- inspect 47   28   1600 .62 0   unknown 0 --- inspect 7.7  4.2  300 0   0      true -32 --- inspect 1.2    1.2    25    .50 0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c true 1 wit inspect 6.5 2.0 320 54 0     0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900   890   2800 0   0   out of memory 0 --- inspect 210 140   7000 .70 0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c true 1 wit inspect 6.4 2.0 320 56 0     0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900   880   3300 0   0   out of memory 0 --- inspect 230 150   7000 .72 0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c true 1 wit inspect 6.7 2.1 300 57 0     0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900   880   3800 0   0   out of memory 0 --- inspect 210 140   7000 .65 0    
elevator_spec13_product24_true-unreach-call_false-termination.cil.c true 1 wit inspect 6.7 2.0 360 57 0     0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900   880   4500 0   0   out of memory 0 --- inspect 210 140   7000 .65 0    
elevator_spec13_product29_true-unreach-call_false-termination.cil.c true 1 wit inspect 6.5 2.0 320 59 0     0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900   890   2900 0   0   out of memory 0 --- inspect 170 110   7000 .65 0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c true 1 wit inspect 6.5 2.0 320 55 0     0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900   880   3600 0   0   out of memory 0 --- inspect 200 130   7000 1.4  0    
elevator_spec13_product31_true-unreach-call_false-termination.cil.c true 1 wit inspect 6.7 2.0 350 55 0     0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900   880   4000 0   0   out of memory 0 --- inspect 230 150   7000 .65 0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c true 1 wit inspect 6.6 2.1 350 54 0     0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900   880   4500 0   0   out of memory 0 --- inspect 210 140   7000 .69 0    
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c true 1 wit inspect 9.0 2.7 430 77 0     0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900   890   3700 0   0   out of memory 0 --- inspect 260 180   7000 .72 0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.4 2.2 310 58 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19   10   700 0   0   out of memory 0 --- inspect 270 190   7000 .71 0    
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.3 2.3 420 66 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25   14   730 0   0   out of memory 0 --- inspect 310 220   7000 .69 0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.2 2.3 410 61 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21   11   740 0   0   out of memory 0 --- inspect 360 260   7000 2.0  0    
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.7 2.3 420 60 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33   20   1100 0   0   out of memory 0 --- inspect 240 160   7000 .65 0    
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.4 2.3 420 58 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24   13   770 0   0   out of memory 0 --- inspect 240 180   7000 .66 0    
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.6 2.3 420 63 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33   19   1100 0   0   out of memory 0 --- inspect 240 160   7000 .63 0    
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.1 2.2 410 62 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 130   110   1800 0   0   out of memory 0 --- inspect 240 170   7000 .66 0    
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.3 2.2 300 56 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 150   130   2000 0   0   out of memory 0 --- inspect 240 170   7000 1.6  0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.4 2.2 420 58 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 130   110   1900 0   0   out of memory 0 --- inspect 250 170   7000 .63 0    
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.3 2.3 420 60 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 150   140   2100 0   0   out of memory 0 --- inspect 290 200   7000 .64 0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.3 2.3 420 63 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 140   120   2000 0   0   out of memory 0 --- inspect 230 160   7000 .65 .033
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.2 2.3 420 62 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 150   140   2100 0   0   out of memory 0 --- inspect 320 220   7000 .64 0    
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.4 2.3 420 66 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 390   370   2700 0   0   out of memory 0 --- inspect 260 180   7000 .64 0    
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.3 2.3 290 58 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 230   220   2900 0   0   out of memory 0 --- inspect 300 210   7000 .64 0    
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.0 2.2 420 66 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 140   120   2100 0   0   out of memory 0 --- inspect 230 160   7000 .66 0    
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.0 2.2 300 61 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 170   160   2300 0   0   out of memory 0 --- inspect 250 180   7000 .65 0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.0 2.2 420 60 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 460   450   2800 0   0   out of memory 0 --- inspect 260 170   7000 .66 .025
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.2 2.2 420 63 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 280   270   2800 0   0   out of memory 0 --- inspect 360 260   7000 .79 0    
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.7 2.1 340 62 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37   27   1100 0   0   out of memory 0 --- inspect 150 99   7000 .65 0    
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.7 2.1 300 62 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 44   32   1200 0   0   out of memory 0 --- inspect 210 140   7000 .66 0    
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.7 2.1 340 63 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 46   34   1200 0   0   out of memory 0 --- inspect 160 110   7000 .71 0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.7 2.0 360 62 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 54   40   1200 0   0   out of memory 0 --- inspect 230 150   7000 .71 0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.8 2.1 300 63 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 44   33   1200 0   0   out of memory 0 --- inspect 170 110   7000 .66 .020
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.9 2.2 370 60 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 52   40   1300 0   0   out of memory 0 --- inspect 240 160   7000 .64 .033
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.6 2.1 340 62 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 86   70   1500 0   0   out of memory 0 --- inspect 170 120   7000 .65 0    
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.8 2.2 360 62 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 67   53   1600 0   0   out of memory 0 --- inspect 280 200   7000 .74 0    
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.5 2.0 340 54 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 51   38   1300 0   0   out of memory 0 --- inspect 180 120   7000 .71 0    
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.8 2.1 370 64 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 54   43   1300 0   0   out of memory 0 --- inspect 190 130   7000 .65 0    
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.7 2.1 340 54 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 93   79   1400 0   0   out of memory 0 --- inspect 180 120   7000 .66 0    
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.9 2.1 370 62 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 77   64   1600 0   0   out of memory 0 --- inspect 240 170   7000 .65 .033
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.5 2.4 420 61 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19   10   680 0   0   out of memory 0 --- inspect 170 110   7000 .74 0    
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.3 2.3 420 59 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23   12   680 0   0   out of memory 0 --- inspect 140 89   7000 .65 0    
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.6 2.3 300 61 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20   11   690 0   0   out of memory 0 --- inspect 170 110   7000 1.6  0    
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.9 2.4 420 71 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32   18   1000 0   0   out of memory 0 --- inspect 200 140   7000 .65 0    
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.9 2.4 420 67 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28   16   880 0   0   out of memory 0 --- inspect 200 140   7000 .72 0    
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.6 2.4 420 67 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41   22   1600 0   0   out of memory 0 --- inspect 210 140   7000 .66 0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.5 2.4 420 55 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21   11   720 0   0   out of memory 0 --- inspect 160 100   7000 .66 0    
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 7.4 2.4 290 66 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27   15   1100 0   0   out of memory 0 --- inspect 210 140   7000 .64 0    
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.0 2.5 420 65 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23   13   900 0   0   out of memory 0 --- inspect 220 150   7000 .66 0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.0 2.6 420 69 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37   21   1600 0   0   out of memory 0 --- inspect 220 150   7000 .64 0    
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.6 2.0 340 53 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 44   32   1100 0   0   out of memory 0 --- inspect 170 120   7000 .65 0    
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.7 2.1 360 56 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 50   38   1200 0   0   out of memory 0 --- inspect 230 150   7000 .65 0    
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.6 2.0 340 57 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 55   41   1300 0   0   out of memory 0 --- inspect 210 140   7000 .65 0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.9 2.1 370 62 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 60   46   1400 0   0   out of memory 0 --- inspect 180 120   7000 1.5  0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.6 2.1 350 60 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 78   66   1700 0   0   out of memory 0 --- inspect 190 130   7000 .71 0    
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.9 2.1 370 65 0     0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 92   77   1600 0   0   out of memory 0 --- inspect 190 120   7000 .66 0    
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   5.5 480 130 .11  0   false(unreach-call) 1 wit inspect 8.5  4.5  310 0   0   unknown 0 --- inspect 88   57   1600 .68 0   false(unreach-call) 1 --- inspect 7.1  3.9  300 0   0      true -32 --- inspect 1.1    1.1    23    .48 0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   4.8 490 130 .12  0   false(unreach-call) 1 wit inspect 8.7  4.6  320 0   0   timeout 0 --- inspect 97   66   1700 .81 0   false(unreach-call) 1 --- inspect 6.8  3.7  300 0   0      true -32 --- inspect 1.1    1.1    23    .49 0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   4.9 480 130 .11  0   false(unreach-call) 1 wit inspect 9.1  4.8  320 0   0   unknown 0 --- inspect 82   56   1600 .68 0   false(unreach-call) 1 --- inspect 6.8  3.7  300 0   0      true -32 --- inspect 1.1    1.1    23    .49 0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   4.6 470 130 .12  0   false(unreach-call) 1 wit inspect 8.6  4.6  320 0   0   unknown 0 --- inspect 89   62   1600 .71 0   false(unreach-call) 1 --- inspect 7.1  3.9  300 0   0      true -32 --- inspect 1.1    1.1    23    .50 .066 - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   5.6 590 130 .13  0   false(unreach-call) 1 wit inspect 8.9  4.8  330 0   0   timeout 0 --- inspect 98   66   1800 1.6  0   false(unreach-call) 1 --- inspect 6.7  3.7  300 0   0      true -32 --- inspect 1.1    1.1    23    .50 .066 - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   4.8 400 120 .13  0   false(unreach-call) 1 wit inspect 9.4  5.0  320 0   0   timeout 0 --- inspect 92   65   1700 .68 0   false(unreach-call) 1 --- inspect 7.3  4.0  300 0   0      true -32 --- inspect 1.1    1.1    23    .51 0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   5.3 600 150 .12  0   false(unreach-call) 1 wit inspect 11    5.7  320 0   0   timeout 0 --- inspect 91   65   1600 .68 0   false(unreach-call) 1 --- inspect 7.0  3.8  300 0   0      true -32 --- inspect 1.1    1.1    23    .50 .066 - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   5.2 620 130 .13  0   false(unreach-call) 1 wit inspect 11    5.6  320 0   0   timeout 0 --- inspect 97   69   1700 1.1  0   false(unreach-call) 1 --- inspect 7.1  3.8  300 0   0      true -32 --- inspect 1.2    1.2    23    .52 .066 - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 960   760   6800 12000 0     0   error (invalid witness file) 0 --- inspect .76 .46 43 0   0   error (invalid witness file) 0 --- inspect 5.9 3.3 260 .65 0   error (invalid witness file) 0 --- inspect .98 .65 48 0   0      error (invalid witness file) 0 --- inspect .0019 .0025 .53 0    0     - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   4.4 490 120 .11  0   false(unreach-call) 1 wit inspect 8.9  4.7  320 0   0   unknown 0 --- inspect 79   53   1500 .71 0   false(unreach-call) 1 --- inspect 7.0  3.8  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    23    .48 0     - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   4.1 500 110 .11  0   false(unreach-call) 1 wit inspect 10    5.3  310 0   0   unknown 0 --- inspect 86   59   1600 .68 0   false(unreach-call) 1 --- inspect 6.7  3.7  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    23    .50 0     - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   4.5 480 130 .11  0   false(unreach-call) 1 wit inspect 10    5.3  320 0   0   unknown 0 --- inspect 79   55   1500 .68 0   false(unreach-call) 1 --- inspect 6.8  3.7  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    23    .48 0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   4.1 500 110 .11  0   false(unreach-call) 1 wit inspect 10    5.4  320 0   0   timeout 0 --- inspect 92   64   1600 .68 0   false(unreach-call) 1 --- inspect 7.3  4.0  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    23    .50 0     - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   4.4 480 110 .12  0   false(unreach-call) 1 wit inspect 8.9  4.7  320 0   0   unknown 0 --- inspect 88   62   1700 .68 0   false(unreach-call) 1 --- inspect 6.9  3.8  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    23    .50 0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   5.0 580 140 .12  0   false(unreach-call) 1 wit inspect 9.1  4.8  330 0   0   timeout 0 --- inspect 98   68   1800 .69 0   false(unreach-call) 1 --- inspect 6.9  3.8  300 0   0      false(unreach-call) 1 --- inspect 1.2    1.2    23    .51 0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   4.5 480 130 .12  0   false(unreach-call) 1 wit inspect 11    5.6  340 0   0   timeout 0 --- inspect 98   68   1700 1.1  0   false(unreach-call) 1 --- inspect 6.8  3.7  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    23    .51 0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   4.2 480 110 .12  0   false(unreach-call) 1 wit inspect 10    5.5  320 0   0   timeout 0 --- inspect 97   71   1800 1.0  0   false(unreach-call) 1 --- inspect 6.8  3.7  300 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    23    .52 0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 960   760   6500 11000 0     0   error (invalid witness file) 0 --- inspect .69 .41 44 0   0   error (invalid witness file) 0 --- inspect 6.2 3.6 270 .66 0   error (invalid witness file) 0 --- inspect .99 .66 49 0   0      error (invalid witness file) 0 --- inspect .0043 .0054 .52 0    0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   5.1 510 140 .14  0   false(unreach-call) 1 wit inspect 8.8  4.6  330 0   0   true -32 --- inspect 16   9.0 460 .66 0   false(unreach-call) 1 --- inspect 6.8  3.7  290 0   0      true -32 --- inspect 1.1    1.1    24    .49 .066 - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   3.9 510 130 .14  0   false(unreach-call) 1 wit inspect 9.4  5.0  330 0   0   true -32 --- inspect 16   9.0 520 .66 0   false(unreach-call) 1 --- inspect 7.0  3.9  300 0   0      true -32 --- inspect 1.1    1.1    23    .50 0     - --- inspect - --- inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   4.3 500 140 .15  0   false(unreach-call) 1