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