Tool VeriAbs 1.3.10 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-10 16:50:17 CET 2018-12-10 20:34:10 CET 2018-12-10 21:22:10 CET 2018-12-10 21:27:56 CET 2018-12-12 21:52:30 CET 2018-12-10 19:33:41 CET 2018-12-10 20:40:20 CET
Run set veriabs.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options -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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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 1 220 160   1500 2000 4.0  0      1 9.4  5.0  310 0   0     1 29     16     980   .66 0     1 6.3  3.4  290 0   0     1 1.0    1.0    24    .40 0     - -
elevator_spec14_product24_false-unreach-call_true-termination.cil.c 1 230 170   1500 1800 4.2  .0041 1 8.8  4.7  330 0   0     1 31     17     990   .62 0     1 6.7  3.7  300 0   0     1 1.0    1.1    24    .43 .074 - -
elevator_spec14_product28_false-unreach-call_true-termination.cil.c 1 220 160   1500 1900 4.1  .012  1 9.8  5.1  310 0   0     1 29     16     990   .62 0     1 6.9  3.7  300 0   0     1 .98   .98   24    .40 0     - -
elevator_spec14_product32_false-unreach-call_true-termination.cil.c 1 230 170   1600 1900 4.2  .23   1 9.3  4.9  330 0   0     1 31     17     960   .66 .074 1 6.8  3.7  290 0   0     1 1.1    1.1    24    .43 0     - -
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c 0 900 840   2100 8300 6.5  0      0 .57 .35 40 0   0     0 .020 .021 5.6 0    0     0 1.0  .66 47 0   0     0 .0017 .0024 .53 0    0     - -
elevator_spec1_product18_false-unreach-call_true-termination.cil.c 1 280 230   920 2600 4.1  0      -32 8.1  4.2  330 0   0     -32 16     9.3   510   .66 0     0 6.4  3.4  300 0   0     1 1.1    1.1    22    .45 0     - -
elevator_spec1_product20_false-unreach-call_true-termination.cil.c 1 290 230   910 3000 4.2  0      -32 9.9  5.1  340 0   0     -32 15     8.5   540   .66 .074 0 7.1  3.8  300 0   0     1 1.1    1.1    22    .47 0     - -
elevator_spec1_product22_false-unreach-call_true-termination.cil.c 1 290 230   990 3200 3.9  0      -32 8.7  4.5  340 0   0     -32 16     9.4   530   .66 0     0 6.8  3.6  300 0   0     1 1.1    1.1    22    .48 0     - -
elevator_spec1_product24_false-unreach-call_true-termination.cil.c 1 290 230   1500 2800 4.3  0      -32 8.8  4.6  350 0   0     -32 23     13     470   .66 0     0 6.6  3.6  300 0   0     1 1.1    1.1    22    .50 0     - -
elevator_spec1_product26_false-unreach-call_true-termination.cil.c 1 280 230   920 2700 4.1  0      -32 8.9  4.7  330 0   0     -32 15     8.6   530   .66 0     0 8.3  4.4  300 0   0     1 1.1    1.1    22    .45 0     - -
elevator_spec1_product28_false-unreach-call_true-termination.cil.c 1 280 230   970 3000 4.2  .81   -32 8.5  4.5  350 0   0     -32 16     9.5   530   .66 0     0 8.3  4.4  300 0   .074 1 1.1    1.1    22    .48 0     - -
elevator_spec1_product30_false-unreach-call_true-termination.cil.c 1 290 230   1100 3100 4.0  0      -32 9.4  4.9  340 0   0     -32 18     10     510   .66 0     0 6.7  3.6  300 0   0     1 1.1    1.1    22    .49 0     - -
elevator_spec1_product32_false-unreach-call_true-termination.cil.c 1 290 230   1100 2900 4.4  14      -32 8.6  4.5  350 0   .078 -32 20     11     530   .66 0     0 6.7  3.6  300 0   0     1 1.1    1.1    22    .51 0     - -
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c 1 810 750   990 8200 6.6  0      -32 49    32    1900 0   0     -32 18     10     470   .66 0     0 6.9  3.7  310 0   0     1 1.2    1.2    22    .56 0     - -
elevator_spec2_product18_false-unreach-call_true-termination.cil.c 1 200 140   1200 1900 4.0  0      1 8.5  4.5  310 0   0     1 36     20     1200   .62 0     1 7.1  3.8  290 0   0     1 1.0    1.0    24    .41 .074 - -
elevator_spec2_product20_false-unreach-call_true-termination.cil.c 1 210 150   1200 1900 4.1  0      1 9.8  5.2  310 0   0     1 37     21     1100   .62 0     1 8.2  4.4  290 0   0     1 1.0    1.0    25    .43 0     - -
elevator_spec2_product22_false-unreach-call_true-termination.cil.c 1 270 210   1400 2600 4.1  .29   1 9.2  4.9  330 0   0     1 35     20     1300   .62 0     1 7.0  3.8  290 0   0     1 1.1    1.1    25    .44 .074 - -
elevator_spec2_product24_false-unreach-call_true-termination.cil.c 1 290 230   1200 2900 4.1  .58   -32 8.9  4.6  350 0   0     -32 17     9.9   530   .66 0     0 7.6  4.1  300 0   0     1 1.2    1.2    22    .50 0     - -
elevator_spec2_product26_false-unreach-call_true-termination.cil.c 1 240 180   1100 2300 4.0  .0041 1 9.1  4.8  280 0   0     1 30     18     1200   .66 .074 1 6.6  3.6  290 0   .074 1 1.0    1.0    24    .42 0     - -
elevator_spec2_product28_false-unreach-call_true-termination.cil.c 1 290 230   1100 2900 4.2  0      -32 8.9  4.6  300 0   0     -32 18     9.9   510   .66 0     0 6.6  3.5  300 0   0     1 1.1    1.1    22    .47 0     - -
elevator_spec2_product30_false-unreach-call_true-termination.cil.c 1 290 230   1100 3300 4.2  0      -32 8.6  4.5  330 0   .074 -32 19     11     520   .66 0     0 7.1  3.8  300 0   0     1 1.1    1.1    22    .48 0     - -
elevator_spec2_product32_false-unreach-call_true-termination.cil.c 1 290 230   1500 2800 4.4  0      -32 8.6  4.5  350 0   0     -32 19     10     460   .66 0     0 6.7  3.6  300 0   0     1 1.2    1.2    22    .50 0     - -
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c 1 690 630   760 8300 4.6  0      -32 48    30    1900 0   0     -32 18     9.9   470   .66 0     0 8.6  4.6  300 0   0     1 1.2    1.2    22    .54 0     - -
elevator_spec3_product03_false-unreach-call_true-termination.cil.c 1 100 49   920 960 4.1  0      1 12    6.2  350 0   0     1 52     30     1800   .66 0     1 7.4  4.0  300 0   0     1 1.1    1.1    27    .43 0     - -
elevator_spec3_product11_false-unreach-call_true-termination.cil.c 1 100 49   930 750 4.1  0      1 9.8  5.1  350 0   0     1 61     35     1600   .62 0     1 7.5  4.1  290 0   0     1 1.1    1.1    27    .29 0     - -
elevator_spec3_product19_false-unreach-call_true-termination.cil.c 1 110 52   1000 990 4.1  0      1 11    5.8  360 0   0     1 46     27     1800   .66 0     1 8.7  4.7  290 0   0     1 1.1    1.1    27    .44 .074 - -
elevator_spec3_product20_false-unreach-call_true-termination.cil.c 1 120 59   1200 1200 4.2  .0041 1 13    6.7  370 0   0     1 64     37     2400   .62 0     1 7.4  4.0  290 0   0     1 1.1    1.2    27    .45 0     - -
elevator_spec3_product23_false-unreach-call_true-termination.cil.c 1 110 60   1200 940 4.3  .0041 1 9.8  5.2  390 0   0     1 45     27     1900   .62 0     1 7.6  4.1  290 0   0     1 1.2    1.2    27    .47 0     - -
elevator_spec3_product24_false-unreach-call_true-termination.cil.c 1 130 70   1400 1100 4.1  0      1 11    5.6  400 0   0     1 55     33     1600   .62 0     1 9.4  5.1  290 0   0     1 1.2    1.2    28    .48 0     - -
elevator_spec3_product27_false-unreach-call_true-termination.cil.c 1 110 54   1100 960 4.2  0      1 9.7  5.2  350 0   0     1 44     27     1700   .66 0     1 7.4  4.0  300 0   0     1 1.1    1.1    27    .44 0     - -
elevator_spec3_product28_false-unreach-call_true-termination.cil.c 1 120 60   1200 1200 4.2  0      1 9.9  5.2  370 0   0     1 47     28     1900   .66 0     1 7.8  4.3  300 0   0     1 1.1    1.1    27    .45 .074 - -
elevator_spec3_product31_false-unreach-call_true-termination.cil.c 1 120 62   1200 1000 4.3  0      1 10    5.4  380 0   0     1 59     34     1700   .62 0     1 7.9  4.2  300 0   0     1 1.2    1.2    27    .47 0     - -
elevator_spec3_product32_false-unreach-call_true-termination.cil.c 1 130 75   1500 1300 4.4  0      1 10    5.3  400 0   0     1 43     24     1300   .66 0     1 7.3  3.9  300 0   0     1 1.2    1.2    28    .48 0     - -
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c 0 900 830   750 8800 4.8  0      0 .57 .35 40 0   0     0 .021 .022 5.6 0    0     0 .89 .58 46 0   0     0 .0053 .0092 .52 0    0     - -
elevator_spec9_product26_false-unreach-call_true-termination.cil.c 1 520 460   960 4400 4.1  .58   -32 8.6  4.5  330 0   .074 -32 16     9.0   470   .62 0     0 6.8  3.6  300 0   0     1 1.1    1.1    22    .46 0     - -
elevator_spec9_product28_false-unreach-call_true-termination.cil.c 1 380 320   1200 2800 4.1  .0041 1 9.0  4.7  320 0   0     1 42     24     1300   .66 0     1 7.0  3.8  290 0   0     1 1.1    1.1    25    .44 .074 - -
elevator_spec9_product30_false-unreach-call_true-termination.cil.c 1 520 470   1100 4600 4.2  .56   -32 8.8  4.6  340 0   0     -32 16     9.2   530   .66 0     0 6.6  3.6  300 0   0     1 1.1    1.1    22    .49 0     - -
elevator_spec9_product32_false-unreach-call_true-termination.cil.c 1 530 470   1100 4500 4.4  0      -32 9.4  4.9  360 0   0     -32 16     9.2   530   .66 0     0 8.6  4.6  300 0   0     1 1.2    1.2    22    .51 0     - -
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c 1 840 780   730 7900 6.6  0      -32 50    32    1900 0   0     -32 22     12     470   .66 0     0 7.2  3.8  310 0   .082 1 1.2    1.2    22    .55 0     - -
elevator_spec13_product21_true-unreach-call_false-termination.cil.c 0 560 480   1200 5000 19    0      - - - - 0 .76 .47 40 0   0     0 .027 .027 5.6 0    0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c 0 580 500   1100 5400 19    0      - - - - 0 .68 .43 40 0   0     0 .021 .022 5.6 0    0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c 0 560 490   1600 5100 13    0      - - - - 0 .60 .37 41 0   0     0 .020 .021 5.6 0    0    
elevator_spec13_product24_true-unreach-call_false-termination.cil.c 0 580 510   1500 4600 13    0      - - - - 0 .78 .47 41 0   0     0 .021 .021 5.6 0    0    
elevator_spec13_product29_true-unreach-call_false-termination.cil.c 0 560 480   1200 5500 19    .074  - - - - 0 .59 .36 40 0   0     0 .020 .020 5.6 0    0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c 0 600 520   1200 5500 19    0      - - - - 0 .59 .36 42 0   0     0 .024 .024 5.6 0    0    
elevator_spec13_product31_true-unreach-call_false-termination.cil.c 0 580 500   1600 5300 13    .0082 - - - - 0 .62 .38 41 0   0     0 .022 .023 5.6 0    0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c 0 590 510   1500 5200 13    0      - - - - 0 .60 .38 41 0   0     0 .021 .022 5.7 0    0    
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c 0 900 840   760 11000 6.6  0      - - - - 0 .66 .40 41 0   0     0 .021 .022 5.6 0    0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c 2 160 68   2300 1600 150    0      - - - - 2 17    9.5  670 0   0     0 260     190     7000   .63 0    
elevator_spec14_product11_true-unreach-call_true-termination.cil.c 2 160 72   2200 1400 160    0      - - - - 2 19    11    700 0   0     0 250     180     7000   .64 0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c 2 170 83   1800 1600 150    6.1    - - - - 2 20    11    740 0   0     0 280     210     7000   .72 0    
elevator_spec14_product23_true-unreach-call_true-termination.cil.c 2 340 220   2600 2900 220    0      - - - - 2 31    18    1100 0   0     0 210     140     7000   .65 0    
elevator_spec14_product27_true-unreach-call_true-termination.cil.c 2 180 80   1900 1500 160    0      - - - - 2 22    12    750 0   0     0 280     200     7000   .65 0    
elevator_spec14_product31_true-unreach-call_true-termination.cil.c 2 280 170   2400 2400 160    0      - - - - 2 33    19    1100 0   .074 0 210     140     7000   .64 0    
elevator_spec1_product01_true-unreach-call_true-termination.cil.c 2 230 88   1800 2000 150    .033  - - - - 2 68    55    1700 0   0     0 220     160     7000   .65 .074
elevator_spec1_product03_true-unreach-call_true-termination.cil.c 2 240 89   2200 2000 150    .68   - - - - 2 89    75    1700 0   0     0 240     170     7000   .63 0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c 2 270 110   2300 2800 150    0      - - - - 2 81    67    1700 0   0     0 230     160     7000   .66 0    
elevator_spec1_product11_true-unreach-call_true-termination.cil.c 2 270 110   1900 2100 160    0      - - - - 2 110    99    1900 0   0     0 960     840     2700   .65 0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c 2 240 89   1900 1900 200    .020  - - - - 2 87    74    1700 0   0     0 220     160     7000   .66 0    
elevator_spec1_product19_true-unreach-call_true-termination.cil.c 2 260 110   1900 2300 150    .020  - - - - 2 90    78    1900 0   .074 0 260     190     7000   .66 0    
elevator_spec1_product21_true-unreach-call_true-termination.cil.c 2 270 110   1900 2500 150    .68   - - - - 2 160    150    2300 0   0     0 270     180     7000   .66 0    
elevator_spec1_product23_true-unreach-call_true-termination.cil.c 2 260 110   1800 2200 150    0      - - - - 2 150    130    2300 0   0     0 330     230     7000   .68 0    
elevator_spec1_product25_true-unreach-call_true-termination.cil.c 2 260 110   2400 1900 150    .15   - - - - 2 100    85    1900 0   0     0 230     160     7000   .63 .094
elevator_spec1_product27_true-unreach-call_true-termination.cil.c 2 270 110   2000 2300 150    .77   - - - - 2 120    110    1900 0   0     0 270     190     7000   .64 0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c 2 270 110   2500 2400 150    .020  - - - - 2 360    350    2300 0   0     0 240     160     7000   .63 0    
elevator_spec1_product31_true-unreach-call_true-termination.cil.c 2 270 110   1900 2400 150    .020  - - - - 2 180    160    2400 0   0     0 290     200     7000   1.5  0    
elevator_spec2_product01_true-unreach-call_true-termination.cil.c 2 220 88   3300 2000 160    0      - - - - 2 33    21    1000 0   0     0 170     110     7000   .66 0    
elevator_spec2_product03_true-unreach-call_true-termination.cil.c 2 250 88   3900 1800 160    .074  - - - - 2 38    26    1100 0   0     0 190     120     7000   1.5  0    
elevator_spec2_product09_true-unreach-call_true-termination.cil.c 2 250 89   3200 2300 150    0      - - - - 2 33    22    1100 0   0     0 160     110     7000   .72 0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c 2 240 89   2800 2000 160    .074  - - - - 2 44    29    1100 0   0     0 210     140     7000   .75 0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c 2 240 88   3100 1800 160    0      - - - - 2 36    24    1100 0   0     0 170     110     7000   .65 .074
elevator_spec2_product19_true-unreach-call_true-termination.cil.c 2 250 89   2700 2000 160    6.1    - - - - 2 38    27    1200 0   0     0 200     130     7000   .63 0    
elevator_spec2_product21_true-unreach-call_true-termination.cil.c 2 220 90   3900 2000 160    0      - - - - 2 57    43    1300 0   0     0 200     130     7000   .65 0    
elevator_spec2_product23_true-unreach-call_true-termination.cil.c 2 230 90   1600 1900 160    0      - - - - 2 52    40    1500 0   0     0 280     190     7000   .63 0    
elevator_spec2_product25_true-unreach-call_true-termination.cil.c 2 230 89   3400 1800 160    51      - - - - 2 39    27    1200 0   0     0 170     110     7000   .63 0    
elevator_spec2_product27_true-unreach-call_true-termination.cil.c 2 250 89   3400 1900 160    6.1    - - - - 2 45    33    1300 0   0     0 200     130     7000   .65 0    
elevator_spec2_product29_true-unreach-call_true-termination.cil.c 2 230 90   4100 1900 160    6.2    - - - - 2 65    52    1500 0   0     0 180     120     7000   .67 0    
elevator_spec2_product31_true-unreach-call_true-termination.cil.c 2 240 91   3000 2200 160    0      - - - - 2 50    38    1600 0   0     0 220     150     7000   .64 .033
elevator_spec3_product01_true-unreach-call_true-termination.cil.c 2 180 66   3900 1400 160    6.3    - - - - 2 18    9.8  670 0   0     0 150     98     7000   .68 0    
elevator_spec3_product09_true-unreach-call_true-termination.cil.c 2 180 66   3800 1600 160    6.1    - - - - 2 19    10    670 0   0     0 150     100     7000   1.6  0    
elevator_spec3_product17_true-unreach-call_true-termination.cil.c 2 170 65   4200 1400 150    6.1    - - - - 2 23    13    690 0   0     0 140     92     7000   .63 0    
elevator_spec3_product18_true-unreach-call_true-termination.cil.c 2 190 68   3900 1400 150    19      - - - - 2 31    17    1000 0   0     0 200     140     7000   .93 0    
elevator_spec3_product21_true-unreach-call_true-termination.cil.c 2 180 69   3200 1600 150    0      - - - - 2 28    15    870 0   0     0 220     150     7000   .65 0    
elevator_spec3_product22_true-unreach-call_true-termination.cil.c 2 190 77   1500 1700 160    7.0    - - - - 2 32    18    1600 0   0     0 210     140     7000   1.5  0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c 2 180 65   4100 1200 160    0      - - - - 2 19    11    690 0   0     0 170     110     7000   .67 .074
elevator_spec3_product26_true-unreach-call_true-termination.cil.c 2 180 68   1900 1500 200    0      - - - - 2 28    16    1100 0   0     0 200     130     7000   .66 .074
elevator_spec3_product29_true-unreach-call_true-termination.cil.c 2 180 70   3700 1800 150    6.7    - - - - 2 27    14    890 0   0     0 200     140     7000   .64 0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c 2 190 76   1800 1700 160    0      - - - - 2 32    18    1600 0   0     0 190     130     7000   .65 0    
elevator_spec9_product09_true-unreach-call_true-termination.cil.c 2 450 320   2000 3700 170    .016  - - - - 2 38    25    1100 0   0     0 190     130     7000   .66 .074
elevator_spec9_product11_true-unreach-call_true-termination.cil.c 2 450 320   3000 3500 160    6.8    - - - - 2 39    28    1200 0   0     0 210     130     7000   1.5  0    
elevator_spec9_product25_true-unreach-call_true-termination.cil.c 2 450 320   1500 3600 160    62      - - - - 2 37    26    1200 0   0     0 210     140     7000   .64 0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c 2 460 320   2900 3800 200    0      - - - - 2 45    32    1300 0   0     0 240     150     7000   .75 0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c 2 450 330   2800 3600 160    19      - - - - 2 89    72    1500 0   0     0 190     130     7000   .63 0    
elevator_spec9_product31_true-unreach-call_true-termination.cil.c 2 460 330   2900 4800 160    0      - - - - 2 61    47    1600 0   0     0 200     130     7000   .64 0    
email_spec0_product16_false-unreach-call_true-termination.cil.c 1 360 300   3600 3800 2.1  0      1 8.0  4.2  320 0   0     0 61     43     1200   .71 0     1 6.4  3.5  290 0   0     1 1.0    1.0    23    .45 0     - -
email_spec0_product21_false-unreach-call_true-termination.cil.c 1 540 480   3800 6900 2.1  0      -32 18    9.4  580 0   0     -32 17     9.6   460   .66 0     0 7.1  3.8  290 0   0     1 1.1    1.1    22    .50 0     - -
email_spec0_product22_false-unreach-call_true-termination.cil.c 1 370 320   3700 4500 2.2  .0041 1 8.1  4.3  320 0   0     0 71     50     1200   .71 0     1 7.7  4.2  290 0   .066 1 1.0    1.0    23    .45 0     - -
email_spec0_product26_false-unreach-call_true-termination.cil.c 1 420 360   3800 4500 2.2  .41   1 8.3  4.4  320 0   0     0 89     64     1300   .71 0     1 8.9  4.8  300 0   0     1 1.1    1.1    23    .48 0     - -
email_spec0_product31_false-unreach-call_true-termination.cil.c 1 540 480   3700 6400 2.3  .033  -32 18    9.1  510 0   0     -32 15     8.5   470   .66 .066 0 6.6  3.6  300 0   0     1 1.1    1.1    22    .51 0     - -
email_spec0_product33_false-unreach-call_true-termination.cil.c 1 360 300   3700 4000 2.2  0      1 8.7  4.6  320 0   0     0 86     62     1400   .71 0     1 7.3  3.9  300 0   0     1 1.1    1.1    23    .48 0     - -
email_spec0_product34_false-unreach-call_true-termination.cil.c 1 550 490   3800 5700 2.4  0      -32 20    10    670 0   0     -32 14     8.1   510   .66 0     0 8.8  4.7  310 0   0     1 1.2    1.1    22    .54 0     - -
email_spec0_product35_false-unreach-call_true-termination.cil.c 1 550 490   3800 6800 2.2  0      -32 26    13    630 0   .066 -32 16     9.2   530   .66 0     0 9.1  4.8  300 0   0     1 1.2    1.2    22    .54 0     - -
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c 0 900 820   3200 11000 2.8  0      0 .61 .40 42 0   0     0 .021 .021 5.7 0    0     0 .93 .60 47 0   0     0 .0017 .0023 .41 0    0     - -
email_spec11_product15_false-unreach-call_true-termination.cil.c 1 350 290   3700 4100 2.1  .0041 1 8.7  4.6  310 0   0     0 59     41     1200   .71 0     1 7.9  4.3  290 0   .061 1 1.0    1.1    23    .45 0     - -
email_spec11_product20_false-unreach-call_true-termination.cil.c 1 540 480   3700 6900 2.3  0      -32 18    9.1  540 0   0     -32 14     7.9   470   .66 0     0 7.6  4.1  290 0   0     1 1.1    1.1    22    .52 0     - -
email_spec11_product22_false-unreach-call_true-termination.cil.c 1 390 330   3700 5000 2.2  13      1 10    5.4  320 0   0     0 73     52     1200   .71 0     1 7.6  4.1  290 0   0     1 1.0    1.0    23    .45 0     - -
email_spec11_product26_false-unreach-call_true-termination.cil.c 1 540 480   3800 5900 2.1  0      -32 18    9.2  620 0   0     -32 15     8.6   470   .66 0     0 6.2  3.3  290 0   0     1 1.1    1.1    21    .51 0     - -
email_spec11_product30_false-unreach-call_true-termination.cil.c 1 360 300   3700 4100 2.2  0      1 9.2  4.9  320 0   0     0 70     51     1400   .68 .066 1 6.6  3.6  300 0   0     1 1.1    1.1    23    .47 0     - -
email_spec11_product32_false-unreach-call_true-termination.cil.c 1 550 490   3700 6400 2.4  0      -32 20    10    640 0   0     -32 16     9.0   550   .62 0     0 7.1  3.8  310 0   .066 1 1.2    1.2    22    .57 0     - -
email_spec11_product33_false-unreach-call_true-termination.cil.c 1 400 340   3700 5300 2.0  .0041 1 9.3  4.9  320 0   0     0 92     66     1400   .71 .19  1 6.7  3.6  300 0   0     1 1.1    1.1    23    .48 0     - -
email_spec11_product35_false-unreach-call_true-termination.cil.c 1 550 490   3800 6500 2.4  0      -32 20    10    640 0   0     -32 15     8.5   530   .62 0     0 8.6  4.6  290 0   0     1 1.2    1.2    21    .54 0     - -
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c 0 900 820   2700 8500 2.6  0      0 .60 .36 40 0   0     0 .025 .026 5.6 0    0     0 .88 .55 46 0   0     0 .0043 .0053 .52 0    0     - -
email_spec1_product14_false-unreach-call_true-termination.cil.c 1 530 470   3700 5800 2.3  0      -32 13    6.7  470 0   0     -32 15     8.3   550   .62 0     0 6.4  3.4  300 0   0     1 1.1    1.1    22    .50 0     - -
email_spec1_product15_false-unreach-call_true-termination.cil.c 1 340 280   3700 3700 2.1  .22   1 8.6  4.5  310 0   0     -32 15     8.5   550   .66 .066 1 8.0  4.4  290 0   0     1 1.0    1.0    24    .46 .066 -