Tool PeSCo 1.7-svn b8d6131600+ CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon004; apollon069; apollon137; apollon154] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155] 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 12:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET 2018-12-08 13:32:07 CET 2018-12-12 20:37:42 CET 2018-12-08 05:07:50 CET 2018-12-08 09:11:31 CET
Run set pesco.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options -svcomp19-pesco -heap 10000M -stack 2048k -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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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 120 79   2600 1500 .20  0     false(unreach-call) 1 wit inspect 8.8 4.6 320 0   0   false(unreach-call) 1 --- inspect 27   16   910 .62 0     false(unreach-call) 1 --- inspect 6.8 3.7 290 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  25 .43 0     - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130 75   2900 1200 .21  0     false(unreach-call) 1 wit inspect 10   5.5 340 0   0   false(unreach-call) 1 --- inspect 29   16   990 .62 0     false(unreach-call) 1 --- inspect 9.3 5.1 310 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .45 0     - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 87 61   1700 910 .18  0     false(unreach-call) 1 wit inspect 9.9 5.3 310 0   0   false(unreach-call) 1 --- inspect 30   16   910 .62 0     false(unreach-call) 1 --- inspect 7.0 3.8 310 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 130 82   2200 1300 .41  0     false(unreach-call) 1 wit inspect 9.7 5.1 340 0   0   false(unreach-call) 1 --- inspect 28   16   930 .62 0     false(unreach-call) 1 --- inspect 9.3 5.0 290 0   0     false(unreach-call) 1 --- inspect 1.1  1.2  25 .45 0     - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 170 110   2500 1700 .23  0     false(unreach-call) 1 wit inspect 10   5.3 330 0   0   false(unreach-call) 1 --- inspect 31   18   1100 .62 0     false(unreach-call) 1 --- inspect 8.2 4.6 310 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .48 .078 - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 82 58   1600 880 .19  0     false(unreach-call) 1 wit inspect 10   5.3 320 0   0   false(unreach-call) 1 --- inspect 34   20   1200 .62 0     false(unreach-call) 1 --- inspect 7.5 4.1 290 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  25 .35 0     - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 180 110   2600 1700 .23  0     false(unreach-call) 1 wit inspect 11   5.7 350 0   0   false(unreach-call) 1 --- inspect 37   22   1200 .62 0     false(unreach-call) 1 --- inspect 7.7 4.2 300 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .46 0     - --- inspect - --- inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 190 120   2700 1900 .22  0     false(unreach-call) 1 wit inspect 10   5.5 360 0   0   false(unreach-call) 1 --- inspect 37   21   1200 .62 0     false(unreach-call) 1 --- inspect 8.3 4.5 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .47 .074 - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 100 76   1700 1200 .22  0     false(unreach-call) 1 wit inspect 10   5.4 350 0   0   false(unreach-call) 1 --- inspect 37   22   1400 .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_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 71 48   1600 810 .19  0     false(unreach-call) 1 wit inspect 9.7 5.1 330 0   0   false(unreach-call) 1 --- inspect 34   19   1100 .62 0     false(unreach-call) 1 --- inspect 7.9 4.3 300 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  25 .44 0     - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 180 110   2800 2100 .23  0     false(unreach-call) 1 wit inspect 11   5.7 350 0   0   false(unreach-call) 1 --- inspect 36   22   1300 .62 0     false(unreach-call) 1 --- inspect 7.5 4.1 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .47 0     - --- inspect - --- inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 200 120   3000 2000 .22  0     false(unreach-call) 1 wit inspect 9.6 5.1 350 0   0   false(unreach-call) 1 --- inspect 39   23   1200 .62 0     false(unreach-call) 1 --- inspect 7.5 4.0 300 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .47 .074 - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 110 79   1700 1100 .22  0     false(unreach-call) 1 wit inspect 11   5.8 340 0   0   false(unreach-call) 1 --- inspect 39   23   1400 .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_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 190 110   4200 2300 .27  0     false(unreach-call) 1 wit inspect 11   6.0 380 0   0   false(unreach-call) 1 --- inspect 54   32   2100 .62 0     false(unreach-call) 1 --- inspect 7.5 4.1 290 0   0     false(unreach-call) 1 --- inspect 1.3  1.3  26 .54 0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 170 110   2400 1800 .20  0     false(unreach-call) 1 wit inspect 9.7 5.1 320 0   0   false(unreach-call) 1 --- inspect 35   21   1200 .62 0     false(unreach-call) 1 --- inspect 7.8 4.3 300 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  25 .45 0     - --- inspect - --- inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 190 110   3000 1900 .22  0     false(unreach-call) 1 wit inspect 11   5.6 330 0   0   false(unreach-call) 1 --- inspect 33   20   1000 .62 0     false(unreach-call) 1 --- inspect 7.0 3.8 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .46 0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 98 45   2500 1000 .20  0     false(unreach-call) 1 wit inspect 11   5.7 340 0   0   false(unreach-call) 1 --- inspect 36   21   1100 .62 0     false(unreach-call) 1 --- inspect 8.2 4.5 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .47 0     - --- inspect - --- inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 210 120   3500 2200 .23  .090 false(unreach-call) 1 wit inspect 12   6.1 360 0   0   false(unreach-call) 1 --- inspect 39   23   1200 .62 0     false(unreach-call) 1 --- inspect 8.7 4.7 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .49 0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 170 110   2400 1900 .20  0     false(unreach-call) 1 wit inspect 9.7 5.1 330 0   0   false(unreach-call) 1 --- inspect 36   21   1200 .62 0     false(unreach-call) 1 --- inspect 7.5 4.1 310 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  25 .45 0     - --- inspect - --- inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 170 100   2600 1600 .22  0     false(unreach-call) 1 wit inspect 9.3 4.9 330 0   0   false(unreach-call) 1 --- inspect 38   22   1000 .62 0     false(unreach-call) 1 --- inspect 7.9 4.3 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .46 0     - --- inspect - --- inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 190 120   3000 2000 .21  0     false(unreach-call) 1 wit inspect 9.4 5.0 340 0   0   false(unreach-call) 1 --- inspect 44   25   1300 .62 0     false(unreach-call) 1 --- inspect 7.6 4.1 320 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 200 120   2800 2200 .23  .025 false(unreach-call) 1 wit inspect 9.7 5.1 360 0   0   false(unreach-call) 1 --- inspect 44   25   1500 .62 0     false(unreach-call) 1 --- inspect 7.2 3.9 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .49 0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 180 100   3900 1800 .25  0     false(unreach-call) 1 wit inspect 12   6.2 390 0   0   false(unreach-call) 1 --- inspect 54   31   2000 .62 0     false(unreach-call) 1 --- inspect 7.6 4.1 300 0   0     false(unreach-call) 1 --- inspect 1.3  1.3  26 .54 0     - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 32 9.3 1300 260 .32  0     false(unreach-call) 1 wit inspect 13   6.9 400 0   0   false(unreach-call) 1 --- inspect 53   31   1600 .62 0     false(unreach-call) 1 --- inspect 8.0 4.3 290 0   0     false(unreach-call) 1 --- inspect 1.3  1.3  27 .45 0     - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 36 14   1400 340 .32  0     false(unreach-call) 1 wit inspect 12   6.3 410 0   0   false(unreach-call) 1 --- inspect 48   28   1700 .62 0     false(unreach-call) 1 --- inspect 7.6 4.1 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  27 .45 .074 - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 37 11   1800 280 .32  0     false(unreach-call) 1 wit inspect 11   5.7 410 0   0   false(unreach-call) 1 --- inspect 52   30   1600 .62 0     false(unreach-call) 1 --- inspect 7.6 4.1 300 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  27 .45 0     - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 38 12   1500 340 .33  0     false(unreach-call) 1 wit inspect 11   6.0 430 0   0   false(unreach-call) 1 --- inspect 53   31   2000 .62 0     false(unreach-call) 1 --- inspect 7.6 4.1 290 0   0     false(unreach-call) 1 --- inspect 1.3  1.3  28 .47 0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 38 13   1400 290 .34  0     false(unreach-call) 1 wit inspect 11   5.8 450 0   0   false(unreach-call) 1 --- inspect 47   28   1700 .62 0     false(unreach-call) 1 --- inspect 8.2 4.4 310 0   0     false(unreach-call) 1 --- inspect 1.3  1.3  28 .49 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 41 13   1600 320 .35  0     false(unreach-call) 1 wit inspect 11   6.0 450 0   0   false(unreach-call) 1 --- inspect 53   31   1600 .62 0     false(unreach-call) 1 --- inspect 8.5 4.6 300 0   .086 false(unreach-call) 1 --- inspect 1.3  1.3  28 .50 0     - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 39 15   1400 320 .32  0     false(unreach-call) 1 wit inspect 12   6.2 410 0   0   false(unreach-call) 1 --- inspect 49   29   1700 .62 0     false(unreach-call) 1 --- inspect 8.4 4.5 300 0   0     false(unreach-call) 1 --- inspect 1.3  1.3  27 .45 0     - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 35 10   1400 260 .33  0     false(unreach-call) 1 wit inspect 12   6.2 410 0   0   false(unreach-call) 1 --- inspect 45   27   1800 .62 0     false(unreach-call) 1 --- inspect 7.9 4.3 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  28 .47 .074 - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 39 13   1500 320 .34  0     false(unreach-call) 1 wit inspect 11   5.8 510 0   0   false(unreach-call) 1 --- inspect 47   28   1700 .62 0     false(unreach-call) 1 --- inspect 8.0 4.3 300 0   0     false(unreach-call) 1 --- inspect 1.3  1.3  28 .45 0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 41 14   1600 320 .35  0     false(unreach-call) 1 wit inspect 12   6.2 520 0   0   false(unreach-call) 1 --- inspect 33   20   1300 .62 0     false(unreach-call) 1 --- inspect 7.9 4.3 300 0   0     false(unreach-call) 1 --- inspect 1.3  1.3  28 .50 0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130 62   3600 1300 .39  .090 false(unreach-call) 1 wit inspect 13   7.0 530 0   0   false(unreach-call) 1 --- inspect 66   39   3500 .62 0     false(unreach-call) 1 --- inspect 9.1 4.8 300 0   0     false(unreach-call) 1 --- inspect 1.4  1.4  29 .55 .082 - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 180 100   3500 1500 .22  0     false(unreach-call) 1 wit inspect 9.1 4.8 330 0   0   false(unreach-call) 1 --- inspect 38   22   1100 .62 0     false(unreach-call) 1 --- inspect 7.7 4.1 320 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .45 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 170 110   2800 1700 .24  0     false(unreach-call) 1 wit inspect 9.6 5.1 350 0   0   false(unreach-call) 1 --- inspect 37   22   1300 .62 0     false(unreach-call) 1 --- inspect 9.2 4.9 310 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .47 0     - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 180 100   3400 1800 .23  0     false(unreach-call) 1 wit inspect 11   5.6 350 0   0   false(unreach-call) 1 --- inspect 41   23   1200 .62 0     false(unreach-call) 1 --- inspect 7.1 3.9 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  25 .30 0     - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 190 91   4100 1700 .25  0     false(unreach-call) 1 wit inspect 10   5.3 360 0   0   false(unreach-call) 1 --- inspect 43   25   1500 .62 0     false(unreach-call) 1 --- inspect 8.1 4.3 310 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  26 .50 0     - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 210 120   4100 2100 .24  0     false(unreach-call) 1 wit inspect 12   6.3 360 0   0   false(unreach-call) 1 --- inspect 51   30   1500 .62 0     false(unreach-call) 1 --- inspect 7.3 3.9 300 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  26 .52 0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 960 440   6800 9000 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0     error (invalid witness file) 0 --- inspect 6.0 3.5 270 .65 0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c true 1 wit inspect 530 470   4700 5900 0     0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3400 0   0     out of memory 0 --- inspect 220   140   7000 .70 0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c true 1 wit inspect 27 14   1300 300 0     0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4100 0   0     out of memory 0 --- inspect 250   160   7000 .72 0    
elevator_spec13_product24_true-unreach-call_false-termination.cil.c true 1 wit inspect 260 230   2900 2700 0     0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4500 0   0     out of memory 0 --- inspect 250   170   7000 .64 0    
elevator_spec13_product29_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 960 420   6900 8500 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 42 0   0     error (invalid witness file) 0 --- inspect 6.3 3.8 270 .66 0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 960 450   6700 9100 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 42 0   0     error (invalid witness file) 0 --- inspect 5.7 3.5 260 .66 0    
elevator_spec13_product31_true-unreach-call_false-termination.cil.c true 1 wit inspect 18 6.4 1100 140 0     0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3700 0   0     out of memory 0 --- inspect 250   170   7000 .72 0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c true 1 wit inspect 23 10   1200 200 0     0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4400 0   0     out of memory 0 --- inspect 210   150   7000 .63 0    
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c true 1 wit inspect 35 20   1300 370 0     0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3500 0   0     out of memory 0 --- inspect 240   160   7000 .64 0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 40 13   1800 300 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    660 0   0     out of memory 0 --- inspect 250   180   7000 1.6  0    
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 45 13   2100 340 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23    13    710 0   0     out of memory 0 --- inspect 310   220   7000 .64 0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 49 18   1800 460 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    13    730 0   0     out of memory 0 --- inspect 330   240   7000 .72 0    
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 83 37   2400 700 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    20    1100 0   0     out of memory 0 --- inspect 230   150   7000 1.6  0    
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 53 19   2100 450 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    12    710 0   0     out of memory 0 --- inspect 290   210   7000 .64 .033
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 78 31   2400 660 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 30    18    1100 0   0     out of memory 0 --- inspect 200   130   7000 .72 0    
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 210 120   4200 2100 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    88    1700 0   0     timeout 0 --- inspect 960   810   5500 .67 0    
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 260 150   5100 2200 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    94    1900 0   0     timeout 0 --- inspect 960   800   6300 .65 0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 19 7.5 1200 180 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 130    110    1900 0   0     out of memory 0 --- inspect 280   200   7000 .71 0    
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 230 130   4000 2600 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    97    1900 0   0     timeout 0 --- inspect 960   820   3300 .63 0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect 190 94   3800 1900 0     0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 97    81    1600 0   0     timeout 0 --- inspect 960   820   4500 .75 0    
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 290 150   4900 2700 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 140    120    2000 0   0     timeout 0 --- inspect 960   820   6300 .76 0    
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 520 350   5800 5500 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 170    150    2400 0   0     out of memory 0 --- inspect 240   160   7000 .63 0    
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect 200 82   3900 1600 0     0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 30    19    910 0   0     timeout 0 --- inspect 960   830   5000 .66 0    
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect 190 98   3700 1900 0     0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 110    97    1800 0   .053 timeout 0 --- inspect 960   840   2500 .63 0    
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 280 150   5000 2700 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 130    110    2100 0   0     timeout 0 --- inspect 960   830   4600 1.6  0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 510 330   5700 5300 0     0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    840    4900 0   0     out of memory 0 --- inspect 200   130   7000 .66 0    
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 530 350   6100 6300 0     .090 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 210    190    2600 0   0     out of memory 0 --- inspect 240   170   7000 .64 0    
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 94 40   2500 840 0     .090 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 51    34    1100 0   0     out of memory 0 --- inspect 740   600   7000 .72 0    
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 88 32   2400 750 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 130    110    1700 0   0     out of memory 0 --- inspect 580   470   7000 .65 0    
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 91 40   2500 840 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 51    36    1200 0   0     out of memory 0 --- inspect 570   470   7000 .72 0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect 71 18   2700 580 0     0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 27    17    760 0   0     false(unreach-call) -16 --- inspect 440   350   5000 .62 0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 59   2800 1200 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 91    78    1700 0   0     out of memory 0 --- inspect 720   600   7000 .64 0    
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 59   2800 1000 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 56    41    1300 0   0     out of memory 0 --- inspect 710   580   7000 .63 0    
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 160 92   3000 1800 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 55    43    1400 0   0     out of memory 0 --- inspect 260   170   7000 .65 0    
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 100 41   2800 900 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 84    66    1700 0   0     out of memory 0 --- inspect 250   180   7000 .65 0    
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 57   2700 1100 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 140    120    2200 0   0     out of memory 0 --- inspect 640   540   7000 .66 0    
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 130 66   2900 1300 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 58    43    1300 0   0     timeout 0 --- inspect 960   840   3300 .65 0    
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 150 86   3600 1700 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 57    44    1600 0   0     out of memory 0 --- inspect 230   150   7000 .72 0    
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 140 76   2800 1600 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 88    69    1700 0   0     out of memory 0 --- inspect 250   180   7000 .68 0    
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 46 16   1800 400 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    10    660 0   0     out of memory 0 --- inspect 190   120   7000 .66 0    
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 43 14   1700 360 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    680 0   0     out of memory 0 --- inspect 190   130   7000 .68 0    
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 43 14   1700 350 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    13    680 0   0     out of memory 0 --- inspect 150   95   7000 .65 0    
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 67 27   2100 620 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    15    1000 0   0     out of memory 0 --- inspect 170   110   7000 .66 0    
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 68 29   2100 660 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    13    930 0   0     out of memory 0 --- inspect 280   190   7000 .65 0    
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 80 36   2200 840 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    18    1500 0   0     out of memory 0 --- inspect 220   150   7000 .65 0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 49 17   1900 400 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    690 0   0     out of memory 0 --- inspect 160   100   7000 .65 0    
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 72 28   2700 720 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    15    1000 0   0     out of memory 0 --- inspect 230   150   7000 .72 0    
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 55 19   1900 430 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    15    870 0   0     out of memory 0 --- inspect 270   180   7000 1.5  0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 77 32   2400 730 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 34    18    1600 0   0     out of memory 0 --- inspect 180   120   7000 1.7  0    
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 91 40   2400 920 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 50    36    1200 0   0     out of memory 0 --- inspect 410   310   7000 .64 0    
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 95 33   2900 840 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 130    120    1800 0   0     out of memory 0 --- inspect 290   210   7000 .71 0    
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 52   2700 1100 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 52    38    1700 0   0     out of memory 0 --- inspect 180   120   7000 .66 0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 210 120   3100 1900 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 160    150    2200 0   0     out of memory 0 --- inspect 210   140   7000 .65 0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 120 47   2700 1000 0     0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 52    40    1300 0   0     out of memory 0 --- inspect 170   110   7000 1.5  0    
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 120 53   2800 1100 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 180    170    2500 0   0     out of memory 0 --- inspect 200   140   7000 .65 0    
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 200 140   2400 2300 .14  0     false(unreach-call) 1 wit inspect 9.2 4.8 330 0   0   unknown 0 --- inspect 67   47   1300 .68 0     false(unreach-call) 1 --- inspect 7.2 3.9 300 0   0     false(unreach-call) 1 --- 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 280 190   3100 2800 .14  0     false(unreach-call) 1 wit inspect 10   5.5 330 0   0   unknown 0 --- inspect 82   58   1400 .68 0     false(unreach-call) 1 --- inspect 7.5 4.1 300 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  23 .49 .066 - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 99 52   2400 910 .12  0     false(unreach-call) 1 wit inspect 8.8 4.6 330 0   0   unknown 0 --- inspect 73   52   1300 .68 0     false(unreach-call) 1 --- inspect 6.5 3.6 290 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  23 .48 0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 200 130   3300 2000 .13  0     false(unreach-call) 1 wit inspect 9.8 5.2 320 0   0   unknown 0 --- inspect 72   52   1300 .68 0     false(unreach-call) 1 --- inspect 6.8 3.7 300 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  23 .50 0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 250 170   3400 3000 .15  0     false(unreach-call) 1 wit inspect 11   5.8 320 0   0   unknown 0 --- inspect 74   53   1400 .68 0     false(unreach-call) 1 --- inspect 6.8 3.7 300 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  24 .50 0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 210 140   3000 2400 .14  0     false(unreach-call) 1 wit inspect 11   5.5 320 0   0   timeout 0 --- inspect 93   67   1500 .68 0     false(unreach-call) 1 --- inspect 7.2 3.9 300 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  23 .50 0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 300 210   3600 3200 .14  0     false(unreach-call) 1 wit inspect 8.5 4.5 310 0   0   unknown 0 --- inspect 84   62   1400 .68 0     false(unreach-call) 1 --- inspect 8.5 4.6 310 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  24 .50 0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 280 200   4000 3500 .14  0     false(unreach-call) 1 wit inspect 10   5.4 330 0   0   timeout 0 --- inspect 94   70   1500 .68 0     false(unreach-call) 1 --- inspect 7.2 3.9 300 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  23 .51 0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 230 160   3600 2400 0     0     false(unreach-call) 1 wit inspect 10   5.3 330 0   0   timeout 0 --- inspect 97   73   1700 .90 0     false(unreach-call) 1 --- inspect 7.3 4.0 300 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  24 .56 0     - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 78 57   1500 820 .11  0     false(unreach-call) 1 wit inspect 8.9 4.7 320 0   0   unknown 0 --- inspect 79   53   1500 .68 0     false(unreach-call) 1 --- inspect 6.7 3.6 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 400 310   3300 4500 .13  0     false(unreach-call) 1 wit inspect 8.9 4.7 320 0   0   unknown 0 --- inspect 72   53   1300 .68 0     false(unreach-call) 1 --- inspect 6.8 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 240 170   2700 2900 .13  0     false(unreach-call) 1 wit inspect 9.2 4.9 320 0   0   unknown 0 --- inspect 69   50   1200 .71 0     false(unreach-call) 1 --- inspect 6.7 3.7 300 0   0     false(unreach-call) 1 --- inspect 1.1  1.2  23 .49 0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 540 430   3900 6600 .14  0     false(unreach-call) 1 wit inspect 9.0 4.8 330 0   0   unknown 0 --- inspect 77   55   1300 .68 0     false(unreach-call) 1 --- inspect 7.1 3.8 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 100 79   1700 1000 .12  0     false(unreach-call) 1 wit inspect 8.8 4.7 320 0   0   unknown 0 --- inspect 89   61   1600 .68 0     false(unreach-call) 1 --- inspect 7.6 4.2 300 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  23 .47 0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 520 410   4100 6400 .15  .090 false(unreach-call) 1 wit inspect 9.0 4.8 330 0   0   unknown 0 --- inspect 78   58   1400 .68 0     false(unreach-call) 1 --- inspect 7.3 3.9 310 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  24 .51 0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 270 200   2800 2800 .14  0     false(unreach-call) 1 wit inspect 9.3 4.9 330 0   0   unknown 0 --- inspect 76   57   1400 .68 0     false(unreach-call) 1 --- inspect 7.1 3.9 310 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  23 .51 0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 230 160   3700 2600 .14  0     false(unreach-call) 1 wit inspect 10   5.5 330 0   0   unknown 0 --- inspect 86   65   1500 .68 0     false(unreach-call) 1 --- inspect 7.2 3.9 300 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  24 .52 0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 250 170   4800 2200 0     0     false(unreach-call) 1 wit inspect 10   5.3 350 0   0   timeout 0 --- inspect 97   69   1800 1.5  0     false(unreach-call) 1 --- inspect 7.9 4.2 290 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  24 .57 0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 180 120   2200 2000 .15  0     true -32 wit inspect 9.0 4.7 360 0   0   unknown 0 --- inspect 87   60   1400 .68 0     false(unreach-call) 1 --- inspect 7.1 3.9 300 0   0     false(unreach-call) 1 --- inspect 1.2  1.2  24 .48 0     - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 79 58   1500 840 .14  0     false(unreach-call) 1 wit inspect 9.3 4.9 330 0   0   true -32 --- inspect 17   9.3 510 .62 0     false(unreach-call) 1 --- inspect 7.1 3.8 290 0   0     true -32 --- inspect 1.2  1.2  23 .50 .066 - --- inspect - --- inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 150 91   2500 1400 .16  0     true -32