Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux Forester CPAchecker Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 Predator-HP skink symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741 VeriAbs
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-11-30 11:20:26 CET 2017-11-30 16:01:31 CET 2017-12-01 08:49:27 CET 2017-12-01 12:59:33 CET 2017-12-01 17:45:47 CET 2017-12-01 19:00:34 CET 2017-12-01 19:46:39 CET 2017-12-01 20:24:12 CET 2017-12-01 22:03:39 CET 2017-12-01 22:41:19 CET 2017-12-02 01:06:24 CET 2017-12-02 02:33:02 CET 2017-12-02 17:23:13 CET 2017-12-02 18:04:04 CET
Run set 2ls.sv-comp18.ReachSafety-Heap cbmc.sv-comp18.ReachSafety-Heap cpa-bam-bnb.sv-comp18.ReachSafety-Heap cpa-bam-slicing.sv-comp18.ReachSafety-Heap cpa-seq.sv-comp18.ReachSafety-Heap depthk.sv-comp18.ReachSafety-Heap esbmc-incr.sv-comp18.ReachSafety-Heap esbmc-kind.sv-comp18.ReachSafety-Heap forester.sv-comp18 interpchecker.sv-comp18.ReachSafety-Heap map2check.sv-comp18.ReachSafety-Heap predatorhp.sv-comp18 skink.sv-comp18.ReachSafety-Heap symbiotic.sv-comp18.ReachSafety-Heap uautomizer.sv-comp18.ReachSafety-Heap ukojak.sv-comp18.ReachSafety-Heap utaipan.sv-comp18.ReachSafety-Heap veriabs.sv-comp18.ReachSafety-Heap
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction --trace error-witness.graphml -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions --witness error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i .22  28 1.8  0 .73 45 7.0 1 8.4 450 66 1 7.6 430 60 1 950   7800 6600 0 8.4  500 92   1 .48  30 4.2  0 3.5   89 40    0 .056 11   .57 0 9.6 460 79 1 .48  12 5.5  1 1.1  51 14   1 8.2 470 64 0 .21 11 2.9 1 900   1100 13000 0 900   1800 13000 0 51   900 540 0 180   1500 2100 0
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i .20  27 1.7  0 .73 42 7.5 0 900   7500 8600 0 4.7 310 42 0 640   2500 7000 0 6.9  480 83   0 900     9600 5400    0 900     12000 5700    0 .055 11   .52 0 210   3300 2400 0 .56  12 7.1  0 2.3  53 24   0 12   680 89 0 .23 11 3.0 0 900   5300 9200 0 900   2100 10000 0 900   1500 8700 0 750   880 8800 0
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i .32  32 3.4  0 .92 54 11   1 5.6 320 50 1 3.9 290 33 0 5.7 310 51 1 1.9  240 29   0 .77  37 9.0  1 .40  29 3.1  1 .077 11   .52 0 5.4 300 45 1 .49  12 5.9  1 .17 26 2.0 1 8.4 410 77 0 .23 11 2.7 1 9.9 520 86 1 13   540 110 1 11   480 91 1 340   550 4000 0
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i .71  48 8.9  0 .66 42 7.2 1 8.7 450 68 1 32   1200 270 -32 160   3200 1800 0 1.4  410 17   0 .42  29 3.9  0 1.1   30 9.6  0 .32  16   3.7  0 12   500 100 1 .49  12 5.1  1 2.4  69 21   1 8.4 470 73 0 .21 11 2.5 0 130   1100 1600 1 900   2200 11000 0 180   890 2300 0 800   870 8600 0
heap-manipulation/tree_false-unreach-call_false-valid-deref.i .33  30 3.1  0 .64 41 7.1 1 7.6 440 68 1 4.5 300 47 0 18   1100 180 1 1.4  190 18   0 .77  30 9.3  1 .69  29 5.8  0 .071 11   .51 0 87   3000 1100 0 .49  12 5.6  1 900    120 13000   0 7.4 370 68 0 .20 11 2.2 0 74   680 850 1 18   690 180 1 740   820 8900 0 750   570 8000 0
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i .37  31 3.4  0 .67 42 6.4 1 7.4 430 60 1 4.7 300 38 0 18   1200 150 1 1.4  190 17   0 1.2   29 12    0 .73  29 5.2  0 .077 11   .46 0 91   2800 970 0 .51  12 6.0  1 2.1  26 22   1 7.2 370 57 0 .20 11 2.2 0 71   670 950 1 21   730 190 1 84   890 830 0 640   570 7700 0
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i .21  29 1.6  0 870    4600 5500   0 900   6800 10000 0 9.4 500 88 0 900   7600 8100 0 890    930 9300   0 900     5500 7700    0 900     11000 8200    0 .055 11   .61 0 900   3900 11000 0 900     230 12000    0 1.5  49 20   2 8.4 460 71 0 900    520 12000   0 900   1300 9600 0 900   1900 12000 0 50   890 500 0 180   1500 2000 0
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i .19  26 1.4  0 870    980 12000   0 900   6300 9600 0 9.1 460 74 2 900   4100 11000 0 900    190 9000   0 900     3300 8500    0 900     3200 7000    0 .11  14   .90 2 130   3900 1700 -16 .29  11 3.2  0 .29 26 3.2 2 6.6 330 56 0 900    370 11000   0 900   950 13000 0 900   1700 10000 0 500   790 6400 0 900   2700 12000 0
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i .22  27 1.9  0 870    1900 8200   0 900   7600 9700 0 4.6 300 42 0 630   3000 6600 -16 890    680 11000   0 900     9600 5600    0 900     12000 6600    0 .057 11   .57 0 210   3700 2500 -16 900     1600 9200    0 2.5  58 28   2 13   710 97 0 900    6400 4600   0 900   5900 9900 0 900   1900 11000 0 900   1300 11000 0 730   880 10000 0
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i .31  32 3.8  0 370    13000 4500   0 900   5900 11000 0 4.6 280 43 2 900   2500 11000 0 890    800 12000   0 900     3800 9800    0 900     4500 9800    0 .055 11   .62 0 900   4600 9900 0 900     250 11000    0 1.6  68 20   2 7.0 390 60 0 900    600 10000   0 900   1200 12000 0 900   1600 12000 0 900   1300 11000 0 340   540 4300 0
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 91     15000 1100    0 870    7400 5400   0 900   6100 11000 0 45   2000 450 2 900   4800 11000 0 890    430 10000   0 900     3500 9600    0 900     3000 10000    0 1.3   47   16    0 900   4100 14000 0 900     440 10000    0 2.2  73 22   2 8.3 460 69 0 900    4500 9100   0 900   930 12000 0 900   2200 13000 0 900   1200 12000 0 790   850 9000 0
heap-manipulation/tree_true-unreach-call.i .29  31 3.4  0 870    5100 7800   0 900   5600 11000 0 8.6 450 67 2 900   3900 5900 0 890    200 10000   0 900     3900 7900    0 900     4200 8600    0 .054 12   .54 0 900   4100 13000 0 900     2100 9600    0 900    860 5500   0 7.7 390 65 0 900    2200 8100   0 900   1100 9200 0 900   2700 10000 0 420   980 6000 0 700   570 8400 0
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i .31  29 3.0  0 .46 37 4.5 1 5.5 320 50 1 3.9 300 33 0 4.7 280 42 1 1.5  180 22   0 .39  29 3.5  1 .34  29 3.2  1 .083 11   .66 1 8.5 450 75 1 .44  12 4.9  1 .18 25 1.9 1 6.0 320 57 0 .21 11 1.9 1 6.1 290 51 1 6.8 350 49 1 6.2 290 56 1 900   3600 10000 0
list-properties/list_false-unreach-call_false-valid-memcleanup.i .36  31 2.6  0 .49 36 4.9 1 900   4200 5700 0 6.0 330 49 0 12   620 92 0 1.4  240 15   0 .71  31 7.2  0 .57  30 6.1  1 2.3   30   830    0 900   4300 14000 0 .93  13 11    1 1.1  26 11   1 6.1 310 52 0 .18 11 2.4 0 28   810 260 1 18   690 170 1 900   1300 12000 0 450   2800 5500 1
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i .28  28 2.6  0 .49 36 4.3 1 4.8 310 47 1 3.6 290 33 1 4.4 280 34 1 1.2  180 16   1 .46  29 3.7  1 .36  29 2.9  1 .076 10   .47 0 4.8 290 43 1 .58  12 7.4  1 .22 24 2.1 1 6.6 330 48 0 .19 11 2.2 1 6.8 320 59 1 6.6 350 59 1 7.0 310 62 1 22   300 210 1
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i .26  29 2.5  0 1.3  36 12   1 5.1 300 46 1 3.9 280 36 -32 8.5 460 71 1 2.7  100 33   1 1.0   29 9.5  1 .93  29 8.1  1 .099 14   1.1  0 11   470 93 1 .34  11 4.2  1 .17 24 1.8 1 5.3 300 51 0 .18 11 1.7 1 42   990 450 1 900   1800 9700 0 240   1200 2800 1 740   3700 5600 0
list-properties/simple_false-unreach-call_false-valid-memcleanup.i .22  27 2.0  0 .47 36 4.6 1 4.7 320 40 1 3.6 290 29 0 4.0 280 33 1 1.2  160 15   1 .46  29 4.3  1 .37  29 4.0  1 .067 11   .71 1 6.0 310 52 1 .46  12 5.0  1 .15 24 2.0 1 5.8 310 58 0 .20 11 2.0 1 7.0 350 59 1 6.1 310 49 1 8.8 540 84 1 23   290 200 1
list-properties/splice_false-unreach-call_false-valid-memcleanup.i .33  30 4.0  0 .44 37 4.7 1 5.4 330 44 1 4.0 290 35 0 5.4 300 42 1 1.5  210 17   0 .54  29 5.0  1 .39  29 3.5  1 .16  15   2.0  1 100   3700 1300 1 .50  12 6.3  1 .19 23 2.3 1 6.4 340 61 0 .21 11 2.0 1 6.9 300 54 1 7.3 360 52 1 7.3 320 57 1 43   300 380 1
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i .28  29 2.5  0 870    3600 7100   0 900   4200 7900 0 4.7 300 45 2 900   3000 6000 0 900    510 11000   0 900     5300 8300    0 900     5400 8600    0 .21  16   2.2  2 900   4100 11000 0 900     420 8300    0 900    2000 7700   0 6.3 330 58 0 900    1600 7400   0 900   1100 10000 0 900   3400 12000 0 900   940 12000 0 900   4000 9300 0
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i .28  28 3.0  0 870    3500 4100   0 900   7100 8600 0 5.3 300 43 2 900   2400 6900 0 900    340 11000   0 900     3400 9300    0 900     3400 10000    0 .067 10   .51 0 900   4400 9900 0 890     40 13000    0 2.4  24 22   2 6.5 320 58 0 900    260 13000   0 900   1300 13000 0 900   1800 13000 0 900   1300 11000 0 900   2600 8500 0
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i .23  30 2.0  2 1.7  37 18   2 5.6 300 42 -16 4.9 300 39 2 24   1500 240 2 34    480 230   2 .24  27 2.3  2 .30  27 3.0  2 .20  19   2.2  2 21   820 140 2 .41  12 4.0  2 .25 25 2.6 2 6.5 340 57 0 .17 11 1.9 2 56   1200 580 2 900   1600 9300 0 910   13000 3900 0 42   660 320 2
list-properties/list_true-unreach-call_false-valid-memtrack.i .38  32 3.7  0 870    6500 6700   0 900   6400 9700 0 6.8 390 54 2 900   3100 6900 0 890    250 12000   0 900     1700 9800    0 900     1600 10000    0 2.6   30   880    0 900   4300 13000 0 900     110 13000    0 2.7  24 26   2 6.7 320 52 0 900    1300 10000   0 900   1100 11000 0 900   1800 11000 0 690   1100 8300 0 630   270 7100 0
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i .23  26 1.6  0 870    4900 8500   0 900   8000 9700 0 3.4 280 32 2 900   2300 6400 0 900    220 13000   0 900     2800 9400    0 900     2900 9100    0 .079 11   .49 2 900   4100 12000 0 890     60 10000    0 2.7  24 29   2 5.4 310 52 0 900    1500 9900   0 900   1000 11000 0 900   10000 12000 0 470   920 5500 0 900   4500 11000 0
list-properties/simple_true-unreach-call_false-valid-memtrack.i .27  28 2.6  0 880    13000 6700   0 900   6600 11000 0 4.5 290 44 2 900   2100 5800 0 900    420 10000   0 900     3300 8500    0 900     3400 10000    0 .054 11   .60 2 900   4300 12000 0 890     59 10000    0 2.7  24 27   2 5.7 320 50 0 900    1300 7200   0 900   1100 11000 0 900   2600 12000 0 200   930 2500 0 900   4200 12000 0
list-properties/splice_true-unreach-call_false-valid-memtrack.i .35  30 4.1  0 830    13000 7700   0 900   4400 6100 0 5.7 310 45 2 900   3700 5600 0 900    210 11000   0 900     3500 9300    0 900     3400 9500    0 5.5   73   890    0 900   4300 12000 0 890     85 11000    0 900    1400 9200   0 6.4 320 50 0 900    1400 8800   0 900   1300 11000 0 900   1500 12000 0 190   1600 2000 0 900   1600 9300 0
ldv-regression/1_3_true-termination.c_false-unreach-call.i .19  24 1.3  1 .40 36 4.0 1 3.8 310 35 1 3.3 280 29 1 3.4 270 31 1 .48 49 6.2 1 .24  28 1.9  1 .21  28 2.0  1 2.5   36   850    0 3.1 280 31 1 .32  11 3.6  1 .13 22 1.9 1 5.0 300 48 1 .16 11 1.8 1 5.7 300 47 1 5.5 300 46 1 5.5 290 50 1 10   280 82 1
ldv-regression/alt_test_true-termination.c_false-unreach-call.i .19  27 2.0  1 .49 37 4.2 1 5.5 330 45 1 3.9 290 34 1 5.1 300 46 1 4.5  450 32   1 .092 28 1.1  1 .12  29 1.1  1 .085 11   .63 1 4.4 290 39 1 .36  11 4.4  1 .12 25 2.1 1 5.5 320 51 1 .18 11 1.6 1 6.0 290 50 1 6.5 320 58 1 6.0 290 50 1 22   250 170 0
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i .11  22 .76 1 .25 33 2.1 1 3.3 280 30 1 3.1 270 27 1 2.6 250 23 1 16    28 210   0 .078 26 .68 0 .074 26 .79 0 .064 9.8 .52 0 2.8 270 28 1 .30  12 3.6  1 .15 22 1.8 1 5.1 290 51 1 .15 11 1.7 1 4.1 240 37 1 4.2 250 37 1 4.1 240 34 1 6.3 290 46 -32
ldv-regression/fo_test_true-termination.c_false-unreach-call.i .21  27 1.6  1 .51 36 4.3 1 4.8 320 40 1 3.4 280 29 1 3.5 270 30 1 .51 29 5.6 1 .17  28 1.2  1 .18  28 1.1  1 .068 10   .44 0 3.7 280 31 1 .38  12 4.6  -32 .13 24 1.9 1 4.2 320 44 0 .20 11 2.0 1 11   300 84 0 10   270 81 0 10   300 87 0 22   280 170 1
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i .11  22 .86 1 .21 33 1.9 1 3.2 280 31 1 3.1 280 30 1 3.2 270 27 1 .39 48 4.3 1 .10  28 .84 1 .10  28 .84 1 .071 10   .65 0 2.7 270 24 1 .33  11 3.6  1 .12 23 1.8 1 5.1 300 51 1 .16 11 1.8 1 4.9 280 38 1 5.3 290 37 1 5.1 290 36 1 9.0 280 85 1
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i .12  22 .69 1 .23 33 2.3 1 3.3 280 33 1 3.2 280 30 1 3.1 270 28 1 .38 49 4.7 1 .16  28 1.7  1 .20  28 1.6  1 .057 10   .49 0 2.9 260 24 1 .31  11 4.6  1 .12 23 1.8 1 5.2 320 52 1 .16 11 1.6 1 5.0 290 36 1 5.2 290 39 1 4.8 290 40 1 9.1 280 74 1
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i .20  24 1.4  1 .44 34 3.8 1 3.6 290 33 1 3.2 270 28 -32 2.7 260 24 1 .58 49 6.1 0 .18  28 1.7  1 .19  28 1.8  1 .056 10   .61 0 3.0 260 28 1 .31  11 3.9  1 .15 22 2.1 1 5.3 310 45 1 .17 11 1.5 1 4.8 260 38 1 5.5 290 48 1 4.8 260 41 1 10   280 85 1
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i .14  23 .87 1 .25 33 2.6 1 4.2 290 39 1 3.7 290 37 0 2.8 260 23 1 .41 50 4.4 0 .37  28 3.4  0 .34  29 3.4  0 .059 12   .69 0 5.4 310 48 1 .073 11 .41 0 .19 24 2.1 1 6.3 310 59 0 .20 11 2.4 1 5.5 290 42 1 6.0 310 42 1 5.8 290 54 1 11   280 88 1
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i .12  25 .56 0 .27 35 3.2 1 6.0 310 45 1 4.7 300 40 0 4.0 280 32 1 5.0  440 44   0 .26  29 2.9  1 .25  29 2.8  1 .074 10   .52 0 6.5 390 54 1 1.1   12 14    1 .15 25 5.1 1 5.4 300 50 0 .19 11 2.3 1 18   740 150 1 900   1500 11000 0 80   1400 740 1 23   250 150 0
ldv-regression/stateful_check_false-unreach-call_false-termination.i .65  37 7.9  1 .67 33 7.1 0 4.2 290 38 1 4.0 290 38 0 3.3 270 33 1 2.1  77 26   0 .24  28 2.2  1 .24  28 2.2  1 .074 11   .64 0 5.4 300 47 1 34     74 400    0 .16 24 1.9 0 39   700 370 0 .22 11 2.6 1 6.9 320 56 1 8.9 490 63 1 15   600 150 1 19   290 150 1
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i .16  24 1.6  1 .57 33 6.5 1 3.6 290 31 1 3.4 300 30 1 2.7 260 28 1 1.5  75 19   1 .11  28 .72 1 .12  28 .85 1 .057 10   .52 0 3.1 260 27 1 .30  11 4.4  1 .13 23 1.7 1 5.1 310 42 1 .17 11 1.6 1 5.8 310 44 1 5.2 290 48 1 6.2 310 51 1 15   280 110 1
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i .17  24 1.5  1 .62 33 5.6 1 3.5 290 28 1 3.2 280 27 1 2.6 250 26 1 1.5  75 23   1 .077 28 .97 1 .11  28 .74 1 .068 10   .46 0 3.1 270 26 1 .30  11 3.7  1 .13 22 1.8 1 4.7 280 49 1 .15 11 1.9 1 4.7 290 41 1 4.8 260 41 1 5.3 290 47 1 14   280 130 1
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i .097 22 .87 2 .39 33 3.8 2 2.8 270 25 2 3.1 270 26 2 3.2 270 24 2 3.8  270 36   2 .096 26 .80 2 .073 26 .77 2 .062 12   .63 2 2.8 270 24 2 .36  11 4.7  2 .12 21 1.8 2 3.9 260 35 2 .12 11 1.3 2 5.3 300 43 2 4.7 260 44 2 5.1 290 38 2 9.2 280 90 2
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i .10  22 .66 2 .40 33 4.5 2 2.8 270 22 2 2.7 270 28 2 2.9 260 27 2 3.5  270 35   2 .074 26 .87 2 .072 26 .78 2 .062 12   .66 2 2.9 270 27 2 .30  11 3.6  2 .14 23 1.7 2 4.1 250 39 2 .12 11 1.6 2 4.8 290 44 2 4.4 260 36 2 4.7 290 36 2 8.1 270 73 2
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i .087 22 .71 2 .40 33 4.7 2 2.8 270 25 2 2.8 270 26 2 3.2 260 26 2 3.5  270 33   2 .069 26 1.0  2 .10  26 .67 2 .087 12   .63 2 2.9 260 25 2 .30  11 3.5  2 .14 21 1.7 2 4.0 240 36 2 .15 11 1.3 2 4.9 290 35 2 4.5 250 42 2 5.0 290 40 2 9.1 260 71 2
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i .11  22 .51 2 .39 33 4.0 2 2.8 270 23 2 2.8 270 24 2 2.9 270 25 2 3.6  260 34   2 .079 26 .66 2 .072 26 .82 2 .079 13   .57 2 2.8 260 27 2 .31  11 2.7  2 .14 22 1.7 2 3.6 240 33 2 .14 11 1.6 2 4.8 290 38 2 4.4 250 35 2 4.6 280 35 2 7.8 270 68 2
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i .42  33 5.4  -16 .79 33 6.7 2 5.5 300 44 0 6.2 350 53 0 2.6 250 24 2 4.0  260 40   2 .082 27 .84 2 .20  27 1.7  2 .049 9.9 .45 0 14   610 130 2 .36  11 4.3  2 .14 23 2.3 2 5.8 300 51 0 .18 11 1.6 2 27   780 280 2 900   1700 12000 0 40   960 330 2 31   600 260 2
ldv-regression/just_assert_true-termination.c_true-unreach-call.i .12  22 .76 2 .38 33 4.1 2 2.6 270 22 2 2.7 270 27 2 2.5 260 19 2 2.9  220 29   2 .10  26 .70 2 .10  26 .74 2 .079 12   .55 2 2.7 280 24 2 .31  11 3.6  2 .14 20 1.6 2 3.7 230 32 2 .12 11 1.4 2 4.3 270 35 2 4.1 250 32 2 4.3 270 35 2 7.8 280 68 2
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i .098 22 .69 2 .40 33 3.3 2 2.9 270 28 2 2.9 270 27 2 3.1 270 29 2 3.5  260 34   2 .092 26 .75 2 .10  26 .84 2 .084 12   .60 2 2.9 260 25 2 .32  11 4.8  2 .15 21 1.7 2 3.8 260 37 2 .14 11 1.2 2 5.6 300 45 2 4.9 260 42 2 5.4 290 44 2 9.6 270 76 2
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i .10  22 .87 2 .41 33 3.5 2 2.8 270 29 2 2.8 270 30 2 3.2 270 31 2 3.9  270 35   2 .075 26 .72 2 .072 26 .70 2 .088 12   .72 2 3.1 280 26 2 .31  11 3.8  2 .15 27 1.8 2 4.4 270 35 2 .15 11 1.4 2 5.7 300 42 2 5.1 270 42 2 5.1 290 38 2 9.8 280 82 2
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i .080 22 .75 2 .42 33 4.0 2 2.8 270 25 2 2.7 270 23 2 2.3 240 21 2 3.1  260 31   2 .095 26 .82 2 .084 26 .89 2 .079 12   .71 2 2.8 280 28 2 .29  11 3.8  2 .14 22 1.8 2 4.0 240 37 2 .15 11 1.3 2 4.3 280 34 2 4.4 250 34 2 4.4 280 34 2 7.9 270 79 2
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i .10  22 .95 2 .37 33 4.7 2 2.8 270 26 2 2.7 270 28 2 2.3 240 20 2 3.1  250 35   2 .095 26 .73 2 .097 26 .71 2 .061 12   .59 2 2.9 260 23 2 .31  11 3.9  2 .12 22 1.8 2 3.9 240 39 2 .17 11 1.4 2 4.4 280 36 2 4.2 250 33 2 4.8 280 36 2 7.8 270 74 2
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i .12  22 .72 2 .40 35 4.1 2 3.0 300 26 2 2.7 270 25 2 3.2 260 30 2 3.8  270 36   2 .11  26 .71 2 .083 26 .77 2 .061 12   .67 2 2.9 270 26 2 .31  11 3.6  2 .13 21 2.1 2 4.0 240 40 2 .15 11 1.5 2 10   530 96 2 6.2 330 53 2 5.6 320 49 2 10   280 74 2
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i .099 22 .73 2 .42 33 3.8 2 3.1 290 29 2 2.8 270 25 2 3.0 260 25 2 3.7  270 40   2 .088 26 .77 2 .095 27 .78 2 .089 12   .65 2 3.0 260 25 2 .31  12 3.6  2 .12 22 1.7 2 3.7 240 31 2 .16 11 1.6 2 7.4 460 64 2 6.1 320 47 2 5.7 320 41 2 9.5 260 79 2
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i .11  22 .65 2 .42 33 3.5 2 3.0 270 24 2 2.7 270 28 2 3.3 270 29 2 3.9  280 36   2 .10  26 .68 2 .079 26 .69 2 .081 12   .57 2 2.7 270 26 2 .32  11 4.3  2 .11 21 1.8 2 3.9 250 36 2 .15 11 1.4 2 6.3 340 53 2 5.5 280 42 2 5.2 290 41 2 9.7 260 91 2
ldv-regression/nested_structure_true-unreach-call_true-termination.i .12  22 .64 2 .41 33 3.4 2 2.9 270 28 2 2.9 270 26 2 3.0 260 28 2 3.7  270 31   2 .11  26 .61 2 .082 26 .74 2 .065 12   .66 2 2.9 280 27 2 .30  11 3.3  2 .14 22 1.7 2 4.0 240 37 2 .14 11 1.7 2 6.4 360 49 2 5.2 280 46 2 5.1 290 49 2 9.8 260 78 2
ldv-regression/oomInt_true-termination.c_true-unreach-call.i .11  22 .65 2 .42 33 3.7 2 2.8 270 26 2 2.9 270 29 2 2.8 260 22 2 3.3  260 29   2 .092 26 .70 2 .094 26 .74 2 .046 9.9 .44 0 2.9 270 26 2 .32  11 3.4  2 .15 22 1.7 2 4.1 260 41 2 .14 11 1.4 2 4.9 290 41 2 4.2 250 34 2 5.1 290 41 2 8.5 270 77 2
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i .11  22 .71 2 .40 33 3.2 2 2.7 270 27 2 2.8 270 24 2 2.3 250 20 2 3.1  260 32   2 .11  26 .64 2 .11  26 .70 2 .064 9.9 .50 0 2.9 260 28 2 .30  11 4.4  2 .12 21 1.8 2 3.9 260 40 2 .12 11 1.7 2 4.9 290 39 2 4.2 240 38 2 4.7 290 34 2 9.0 270 71 2
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i .11  23 .84 2 .43 33 4.4 2 3.5 300 29 2 3.5 280 36 2 2.5 240 21 2 3.4  270 31   2 .079 27 .91 2 .085 27 1.1  2 .072 10   .46 0 5.6 300 47 -16 .081 11 .36 0 .31 23 3.0 2 7.0 350 62 0 .22 11 2.2 2 6.0 300 49 2 900   1300 14000 0 6.3 300 52 2 12   280 94 2
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i .11  25 .72 0 .47 35 4.7 2 4.3 280 33 2 3.8 280 38 2 2.9 250 25 2 9.3  410 96   2 .12  27 1.3  2 .14  27 1.2  2 .082 11   .60 0 14   620 110 2 1.4   12 16    2 .16 29 2.0 2 6.0 330 55 0 .20 11 2.0 2 17   690 140 2 900   1600 11000 0 86   1400 780 2 22   250 160 0
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i .18  26 1.2  2 .85 36 7.3 2 4.1 300 39 2 3.3 270 30 2 3.9 280 39 2 5.2  280 50   2 .10  27 .88 2 .11  27 .73 2 .066 12   .71 2 4.6 290 42 2 .35  12 4.0  2 .19 22 2.1 2 3.9 240 36 2 .15 11 1.6 2 8.0 420 62 2 7.6 430 60 2 7.4 360 67 2 20   290 160 2
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i .12  24 .83 2 .47 34 3.6 2 3.1 270 30 2 3.3 280 28 2 2.7 250 23 2 3.6  270 37   2 .077 26 .81 2 .11  27 .75 2 .072 10   .48 0 3.2 280 27 2 .34  11 3.6  -16 .15 22 1.7 2 4.2 260 40 2 .15 11 1.4 2 4.9 280 41 2 4.5 260 37 2 4.7 270 42 2 20   270 150 2
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i .11  22 .65 2 .42 33 3.9 2 2.8 270 28 2 2.9 260 25 2 3.0 270 26 2 3.5  270 32   2 .10  26 .75 2 .11  26 .68 2 .079 12   .55 2 2.8 260 25 2 .30  11 3.5  2 .15 21 1.7 2 4.0 240 34 2 .15 11 1.5 2 4.5 280 36 2 4.3 250 36 2 4.7 280 38 2 7.9 270 68 2
ldv-regression/test_address_true-termination.c_true-unreach-call.i .12  24 .79 2 .47 34 4.1 2 3.3 270 31 2 2.9 270 26 2 3.9 280 32 2 5.3  290 52   2 .082 27 .79 2 .079 27 .76 2 .078 12   .67 2 3.2 280 27 2 .32  11 3.7  2 .12 22 1.9 2 4.3 250 39 2 .15 11 1.6 2 4.9 290 42 2 4.7 280 38 2 5.0 280 40 2 19   270 150 2
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i .11  22 .63 2 .42 33 3.5 2 2.7 270 26 2 2.8 270 22 2 2.4 250 20 2 3.0  260 29   2 .071 26 .78 2 .088 26 .65 2 .093 13   .62 2 2.7 270 25 2 .29  11 3.6  2 .15 21 1.7 2 3.9 240 38 2 .12 11 1.3 2 4.7 280 41 2 4.4 260 36 2 4.7 290 37 2 7.9 260 67 2
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i .20  26 1.7  2 .83 36 6.8 2 3.3 270 32 2 2.8 270 25 2 4.1 280 32 2 5.0  280 52   2 .11  27 .62 2 .10  27 .86 2 .063 12   .73 2 3.3 280 32 2 .050 11 .37 0 .17 22 1.9 2 4.0 240 39 2 .14 11 2.0 2 5.3 300 38 2 4.8 280 38 2 5.1 290 43 2 20   280 170 2
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i .11  25 .82 2 .46 35 4.3 2 3.6 300 32 2 2.8 270 28 2 4.2 280 34 2 5.3  280 52   2 .081 27 .81 2 .077 26 .92 2 .060 12   .72 2 3.3 280 27 2 .040 11 .31 0 .14 23 1.7 2 3.9 240 40 2 .16 11 1.7 2 5.3 290 41 2 4.8 290 40 2 4.8 290 36 2 19   280 150 2
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i .096 26 .79 2 .50 36 5.8 2 3.8 300 34 2 2.8 270 24 2 2.9 250 24 2 .99 48 12   2 .088 27 .88 2 .11  27 .78 2 .063 12   .65 2 3.7 290 32 2 .35  12 3.6  2 .16 24 1.8 0 5.4 310 44 2 .14 11 1.9 2 4.7 280 38 2 5.1 280 38 2 5.0 280 41 2 18   280 130 2
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i .12  22 .63 2 .40 33 3.5 2 2.8 280 25 2 2.9 270 25 2 2.5 250 25 2 3.2  260 33   2 .13  29 1.5  2 .17  29 1.8  2 .050 9.7 .53 0 2.8 270 27 2 .30  11 4.1  2 .15 22 1.7 2 4.0 240 36 2 .14 11 1.6 2 4.8 280 41 2 4.6 250 40 2 4.7 290 38 2 7.8 280 65 2
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i .11  22 .77 2 .40 33 3.5 2 2.8 270 30 2 2.9 270 25 2 3.1 260 26 2 4.0  270 39   2 .13  27 1.3  2 .16  27 1.6  2 .064 9.8 .37 0 3.0 270 29 2 .32  11 3.6  2 .12 21 1.7 2 3.9 240 33 2 .14 11 1.6 2 4.9 280 44 2 4.5 260 41 2 4.9 290 42 2 9.6 270 81 2
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i .080 22 .84 2 .41 33 3.4 2 2.7 270 25 2 2.6 270 27 2 3.3 270 29 2 3.9  280 34   2 .14  27 1.7  2 .13  27 1.5  2 .051 11   .51 0 2.8 270 24 2 .33  12 3.8  2 .14 21 1.6 2 3.8 240 38 2 .15 11 1.6 2 4.7 280 38 2 4.7 260 40 2 5.0 280 38 2 9.2 270 82 2
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i .098 22 .65 2 .42 33 3.2 2 2.7 270 25 2 2.7 260 25 2 2.4 250 20 2 3.2  270 30   2 .17  29 1.4  2 .18  29 1.5  2 .044 9.9 .44 0 2.9 270 28 2 .29  11 4.2  2 .12 21 1.7 2 4.0 240 34 2 .14 11 1.2 2 6.7 350 44 2 4.3 250 37 2 4.6 280 40 2 7.7 270 72 2
ldv-regression/test_union_true-termination.c_true-unreach-call.i .082 22 .76 2 .39 33 3.7 2 2.7 270 25 2 2.7 270 25 2 2.3 250 20 2 3.2  260 29   2 .075 26 .76 2 .076 26 .76 2 .064 9.7 .49 0 2.9 270 26 2 .29  11 3.6  2 .15 21 1.8 2 4.1 250 35 2 .14 11 1.5 2 4.6 290 41 2 4.6 260 35 2 4.4 270 39 2 7.6 270 70 2
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i .086 22 .68 2 .40 33 5.2 2 2.8 270 24 2 2.8 280 26 2 2.4 250 20 2 3.1  260 30   2 .10  26 .79 2 .099 26 .79 2 .068 9.8 .43 0 2.9 270 28 -16 .32  11 3.5  2 .14 21 1.7 2 4.2 290 35 2 .15 11 1.3 2 4.7 280 40 2 4.4 250 36 2 4.7 280 37 2 7.6 270 75 2
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i .097 22 .67 2 .41 33 4.1 2 2.8 270 24 2 2.9 270 28 2 3.0 260 28 2 3.6  270 33   2 .10  26 .65 2 .097 26 .76 2 .067 12   .57 2 2.9 270 25 2 .32  11 3.3  2 .15 21 1.7 2 5.2 300 49 2 .15 11 1.6 2 5.2 290 43 2 4.4 250 41 2 4.5 280 34 2 9.5 270 74 2
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i .099 22 .74 2 .41 33 3.9 2 2.7 270 25 2 2.7 270 23 2 3.0 270 24 2 3.6  270 30   2 .075 26 .83 2 .086 26 .77 2 .061 12   .63 2 2.9 260 23 2 .33  11 4.0  2 .11 20 1.7 2 3.9 230 36 2 .12 11 1.1 2 5.2 290 39 2 4.5 250 38 2 4.7 280 39 2 9.7 270 82 2
ldv-regression/test02_false-unreach-call_true-termination.c .10  22 .83 1 .24 33 2.1 1 3.3 280 27 1 3.1 280 26 1 2.5 260 23 1 .38 48 4.7 1 .082 28 .90 1 .12  28 .79 1 .066 9.9 .49 0 2.8 270 25 1 .32  11 3.5  1 .12 22 1.8 1 5.2 290 45 1 .16 11 1.4 1 4.2 240 37 1 4.6 250 32 1 4.4 250 38 1 7.3 270 66 1
ldv-regression/test06_false-unreach-call_true-termination.c .096 22 .97 1 .25 33 1.9 1 3.7 280 33 1 3.4 290 30 1 2.7 250 21 1 .40 48 4.2 0 .086 28 .81 1 .082 28 .76 1 .061 11   .68 0 3.1 260 27 1 .36  11 3.5  1 .12 22 2.1 1 5.1 310 53 1 .14 11 1.5 1 6.5 320 52 1 6.6 320 58 1 6.0 300 50 1 10   280 78 1
ldv-regression/test08_false-unreach-call_true-termination.c .14  22 .85 1 .24 33 2.2 1 3.3 290 29 1 3.2 280 30 1 2.6 260 23 1 .39 48 4.4 1 .084 28 .96 1 .12  28 .88 1 .073 11   .51 0 3.0 270 25 1 .33  11 3.7  1 .12 23 1.9 1 4.7 290 45 0 .16 11 1.9 1 4.5 250 35 1 5.0 260 36 1 4.6 280 39 1 9.5 310 71 1
ldv-regression/test12_false-unreach-call_true-termination.c .13  22 .84 1 .24 33 2.0 1 3.2 280 28 1 3.2 270 25 1 2.7 250 23 1 .37 27 4.2 1 .11  28 1.2  1 .10  28 1.1  1 .051 10   .47 0 2.9 270 25 1 .29  11 3.3  1 .14 23 1.8 1 4.9 300 44 1 .15 11 1.6 1 4.2 250 36 1 4.3 260 36 1 4.3 250 34 1 8.4 270 69 1
ldv-regression/test21_false-unreach-call_true-termination.c .11  22 .80 1 .28 33 2.0 1 3.5 290 31 1 3.5 280 33 1 2.8 250 23 1 .37 39 4.6 1 .41  28 2.8  0 .37  28 3.1  0 .080 11   .47 0 2.9 260 27 1 .28  11 3.5  0 .17 29 1.8 1 5.5 320 50 0 .20 12 2.4 1 4.7 260 42 1 5.6 290 48 1 4.7 280 41 1 10   280 71 1
ldv-regression/test22_false-unreach-call.c .14  25 .87 1 .26 33 2.2 1 4.0 310 33 0 3.5 290 32 0 3.8 280 31 1 .37 66 4.4 0 .46  28 5.2  0 .54  28 4.7  0 .048 10   .53 0 9.5 480 78 1 .30  11 3.1  0 .18 23 1.9 1 5.4 310 42 0 .26 12 2.6 1 8.9 470 76 1 6.1 320 44 1 10   570 77 1 15   280 100 1
ldv-regression/test23_false-unreach-call.c .097 22 .89 0 1.4  36 15   1 3.4 290 29 0 27   1700 230 0 11   290 120 1 16    66 200   0 3.2   32 39    0 2.8   31 39    0 .052 10   .55 0 22   830 170 0 .31  11 4.0  0 .14 23 1.8 0 5.6 320 48 0 .28 13 3.4 1 130   1200 1500 0 54   1300 610 1 260   3300 2700 0 19   220 150 0
ldv-regression/test24_false-unreach-call.c .10  22 .71 0 2.0  38 21   0 4.8 310 47 1 5.5 440 49 0 3.4 270 29 1 1.3  100 15   0 .71  41 8.5  0 2.4   51 33    0 .053 10   .46 0 15   620 120 0 .80  19 12    1 .26 24 3.1 0 7.4 420 61 0 .20 14 2.4 1 37   740 370 1 24   570 220 0 120   830 1600 0 400   740 3100 0
ldv-regression/test25_false-unreach-call_true-termination.c .084 22 .92 0 1.1  36 12   0 4.2 320 33 0 7.2 410 63 1 12   310 130 1 6.9  100 94   0 .60  32 7.2  0 .93  40 11    0 .071 10   .42 0 27   1100 250 1 .73  17 8.4  1 .19 23 2.2 0 6.7 360 59 0 .20 14 2.3 1 89   870 920 1 140   1400 1600 0 36   790 330 1 61   220 610 0
ldv-regression/test26_false-unreach-call_true-termination.c .12  22 .94 1 .26 33 2.0 1 3.3 280 27 1 3.3 280 30 1 2.6 250 22 1 .38 48 4.3 1 .094 28 1.0  1 .079 28 .82 1 .054 10   .55 0 2.8 270 24 1 .30  11 3.6  1 .15 23 1.7 1 4.8 290 41 0 .15 11 1.8 1 4.4 250 34 1 4.6 260 44 1 4.4 260 36 1 10   280 73 1
ldv-regression/test27_false-unreach-call_true-termination.c .12  22 .71 0 1.2  36 12   1 5.2 330 46 1 4.8 310 44 0 3.2 270 28 1 6.4  110 92   0 1.3   29 11    1 .88  28 8.0  1 .076 10   .47 0 7.5 440 59 1 .074 11 .46 0 .16 23 1.9 0 6.5 320 54 0 .52 13 7.1 0 49   580 530 1 45   680 430 0 200   770 2200 0 34   410 280 0
ldv-regression/test28_false-unreach-call_true-termination.c .14  22 .81 1 .24 33 2.1 1 3.5 290 30 1 3.3 280 30 1 3.2 270 30 1 .40 49 4.5 1 .24  28 2.3  1 .23  28 2.7  1 .070 9.9 .43 0 3.2 270 29 1 .33  11 3.9  1 .12 21 1.9 1 5.3 310 43 0 .17 11 1.9 1 5.8 310 50 1 5.0 270 43 1 7.4 360 55 1 7.6 280 71 1
ldv-regression/test29_false-unreach-call_true-termination.c .12  22 .92 0 .26 33 2.1 1 3.6 310 33 1 3.2 290 29 1 3.4 270 28 1 .37 48 4.8 1 .37  28 3.2  1 .40  28 3.6  1 .048 9.9 .54 0 3.5 290 31 1 .34  12 5.2  1 .14 23 1.7 1 5.4 300 48 0 .16 11 1.7 1 5.3 280 42 1 5.2 270 40 1 5.3 290 42 1 7.8 280 70 1
ldv-regression/test30_false-unreach-call_true-termination.c .10  22 .86 1 .27 33 2.1 1 3.4 310 30 1 3.3 280 29 1 2.6 250 21 1 .37 48 4.6 1 .079 28 .87 1 .084 28 .84 1 2.0   32   840    0 2.8 270 24 1 .34  11 3.5  1 .12 23 1.9 1 4.9 290 44 0 .15 11 1.5 1 4.6 260 35 1 5.5 280 46 1 5.1 290 46 1 10   280 76 1
ldv-regression/test01_true-unreach-call_true-termination.c .12  22 .62 2 .43 33 2.8 2 2.7 270 23 2 2.7 270 28 2 2.9 260 27 2 3.5  260 35   2 .10  26 .74 2 .095 26 .79 2 .080 12   .57 2 2.8 280 24 2 .27  11 3.1  0 .14 21 1.6 2 3.8 230 36 2 .12 11 1.3 2 4.8 290 38 2 4.6 250 36 2 4.5 270 33 2 8.1 270 69 2
ldv-regression/test03_true-unreach-call_true-termination.c .090 22 .87 2 .41 33 3.8 2 2.8 270 26 2 2.8 270 23 2 3.1 270 30 2 3.9  280 33   2 .094 26 .71 2 .077 26 .66 2 .091 16   .77 2 2.8 280 28 2 .30  11 3.4  0 .11 23 1.9 2 3.7 240 37 2 .12 11 1.4 2 5.7 320 51 2 4.6 260 37 2 5.3 300 43 2 9.8 270 77 2
ldv-regression/test04_true-unreach-call_true-termination.c .10  22 .89 2 .40 33 3.6 2 3.0 270 22 2 2.9 270 25 2 3.4 280 26 2 3.6  270 33   2 .11  26 .74 2 .095 26 .86 2 .061 12   .64 2 2.9 280 26 2 .27  11 3.0  0 .14 21 1.8 2 3.7 240 33 2 .13 11 1.4 2 5.7 320 44 2 4.8 260 42 2 5.3 290 40 2 11   270 88 2
ldv-regression/test05_true-unreach-call_true-termination.c .13  22 .76 2 .43 33 3.7 2 3.3 280 24 2 3.1 270 32 2 3.6 270 33 2 4.0  280 38   2 .073 26 .86 2 .079 26 .80 2 .078 11   .63 0 3.5 280 31 2 .31  11 2.9  0 .15 22 1.8 2 4.1 260 40 2 .15 11 1.4 2 8.3 520 63 2 7.0 380 55 2 7.4 390 58 2 11   270 87 2
ldv-regression/test07_true-unreach-call_true-termination.c .13  22 .71 2 .45 33 4.0 2 3.2 280 29 2 3.2 280 26 2 3.5 290 29 2 4.0  270 40   2 .093 26 .78 2 .098 26 .71 2 .081 11   .54 0 3.3 270 32 2 .30  11 3.4  0 .11 22 1.8 2 4.1 270 43 2 .12 11 1.4 2 9.0 410 84 2 5.0 280 47 2 8.5 370 66 2 9.8 270 84 2
ldv-regression/test09_true-unreach-call_true-termination.c .12  22 .72 2 .41 33 3.8 2 3.0 270 29 2 2.9 270 29 2 3.1 260 30 2 3.8  280 38   2 .077 26 .81 2 .086 26 .84 2 .071 11   .66 0 3.2 270 28 2 .31  11 3.0  0 .14 22 1.7 2 4.1 250 39 2 .15 11 1.5 2 7.2 370 62 2 5.3 290 42 2 6.4 300 53 2 10   280 79 2
ldv-regression/test10_true-unreach-call_true-termination.c .11  22 .95 2 .42 33 3.7 2 3.0 270 29 2 3.1 270 29 2 3.2 270 29 2 3.9  270 37   2 .11  26 .69 2 .076 26 .78 2 .060 10   .40 0 3.2 270 30 2 .32  11 3.1  0 .15 22 1.7 2 5.1 290 44 0 .14 11 1.6 2 11   700 96 2 8.6 400 71 2 9.4 430 76 2 9.9 270 90 2
ldv-regression/test11_true-unreach-call_true-termination.c .11  22 .93 2 .41 33 4.8 2 3.1 270 28 2 3.0 270 32 2 3.4 280 30 2 4.0  280 34   2 .11  26 .68 2 .073 26 .78 2 .049 9.9 .53 0 3.2 260 27 2 .27  11 3.3  0 .12 22 1.8 2 4.0 250 36 2 .12 11 1.4 2 6.1 300 55 2 5.7 330 51 2 5.7 290 47 2 10   270 84 2
ldv-regression/test13_true-unreach-call_true-termination.c .11  22 .74 2 .43 33 3.4 2 2.8 280 23 2 2.7 270 26 2 3.0 270 27 2 3.5  260 34   2 .073 26 .68 2 .071 26 .92 2 .066 12   .59 2 2.8 270 25 2 .29  11 3.4  2 .15 21 1.8 2 4.9 290 39 0 .15 11 1.6 2 5.1 280 46 2 5.0 260 38 2 5.0 290 38 2 9.7 270 73 2
ldv-regression/test14_true-unreach-call_true-termination.c .098 22 .81 2 .41 33 4.5 2 3.0 270 27 2 2.9 270 25 2 3.2 270 28 2 3.9  270 40   2 .10  26 .75 2 .10  26 .94 2 .073 10   .36 0 2.9 270 26 2 .26  11 2.8  0 .15 21 1.7 2 4.0 250 41 2 .13 11 1.4 2 5.9 290 48 2 5.5 290 44 2 5.4 290 45 2 10   270 78 2
ldv-regression/test15_true-unreach-call_true-termination.c .12  22 .83 2 .40 33 4.8 2 2.9 270 27 2 2.8 270 24 2 3.5 290 26 2 3.7  270 37   2 .072 26 .86 2 .11  26 .63 2 .064 11   .60 0 3.0 280 24 2 .29  11 3.0  0 .13 27 1.8 2 4.0 250 36 2 .14 11 1.4 2 6.2 330 58 2 7.1 350 54 2 4.8 290 42 2 9.8 270 92 2
ldv-regression/test16_true-unreach-call_true-termination.c .12  22 .79 2 .40 33 4.7 2 2.9 270 25 2 2.8 270 26 2 3.1 270 27 2 3.6  270 39   2 .072 26 .80 2 .077 26 .77 2 .079 12   .66 2 2.8 280 23 2 .30  11 3.5  2 .15 21 1.7 2 4.2 260 36 2 .13 11 1.4 2 6.5 340 57 2 4.9 260 45 2 5.4 300 46 2 10   270 89 2
ldv-regression/test17_true-unreach-call_true-termination.c .10  22 .76 2 .42 33 3.8 2 2.8 270 24 2 2.9 270 28 2 2.9 260 29 2 3.6  270 35   2 .10  26 .71 2 .11  26 .71 2 .086 12   .68 2 2.7 270 27 2 .29  11 3.5  2 .11 22 1.7 2 3.9 240 36 2 .14 11 1.4 2 4.6 280 40 2 4.3 260 37 2 4.8 290 38 2 8.7 270 86 2
ldv-regression/test18_true-unreach-call_true-termination.c .10  22 .70 2 .42 33 3.7 2 2.8 270 26 2 3.0 270 26 -16 3.1 270 25 2 4.0  270 36   2 .079 26 .63 2 .11  26 .70 2 .083 12   .62 2 2.9 270 24 2 .29  11 3.4  0 .15 22 1.6 2 3.8 240 38 2 .15 11 1.4 2 6.4 350 53 2 6.2 320 49 2 6.2 320 49 2 9.7 270 69 2
ldv-regression/test19_true-unreach-call_true-termination.c .11  22 .72 2 .43 33 4.0 2 2.9 270 29 2 2.9 270 29 2 3.1 260 28 2 3.6  270 33   2 .096 26 .68 2 .11  26 .65 2 .067 10   .46 0 3.0 270 27 2 .27  11 2.9  0 .11 28 2.3 2 4.0 240 35 2 .15 11 1.2 2 7.6 490 63 2 6.0 320 47 2 6.3 320 47 2 10   280 93 2
ldv-regression/test20_true-unreach-call_true-termination.c .10  22 .74 2 .42 33 3.4 2 2.9 280 26 2 2.8 270 23 2 3.0 270 29 2 3.6  260 32   2 .11  26 .72 2 .11  26 .76 2 .061 12   .62 2 2.8 280 25 2 .32  11 3.0  2 .14 24 1.7 2 3.6 240 36 2 .15 11 1.4 2 4.9 280 43 2 4.4 260 37 2 4.8 290 42 2 9.2 270 82 2
ldv-regression/test21_true-unreach-call_true-termination.c .11  22 .95 2 .41 33 4.2 2 3.1 270 30 2 3.0 270 32 2 3.4 270 29 2 4.2  280 42   2 .097 26 1.0  2 .11  26 1.1  2 .065 10   .52 0 3.3 280 29 2 .26  11 3.5  0 .15 23 1.7 2 4.4 290 41 2 .14 11 1.4 2 6.6 370 54 2 5.1 290 40 2 6.4 340 59 2 12   290 92 2
ldv-regression/test22_true-unreach-call.c .21  25 2.5  2 2.0  35 21   2 6.5 380 53 2 6.0 370 49 2 5.9 290 55 2 6.9  280 57   2 .85  26 10    2 .98  27 13    2 .067 11   .48 0 10   460 92 2 .31  11 3.2  0 .18 24 1.9 -16 4.3 290 38 2 .15 11 1.4 2 17   700 170 2 25   800 280 2 20   750 160 2 17   450 120 2
ldv-regression/test23_true-unreach-call.c .11  22 .65 0 1.6  36 18   2 3.7 300 32 0 29   1700 250 2 11   330 130 2 21    400 220   2 2.2   29 26    2 2.3   30 26    2 .072 10   .44 0 44   2100 470 2 .30  11 3.0  0 .14 22 1.7 0 4.7 300 38 2 .13 11 1.8 2 250   830 3300 2 49   2100 490 2 97   2900 1100 2 18   300 140 2
ldv-regression/test24_true-unreach-call_true-termination.c .11  22 .65 0 1.4  36 16   2 3.5 310 29 0 3.3 290 30 -16 11   300 110 2 44    500 590   2 3.9   32 48    2 4.2   32 57    2 .047 11   .65 0 11   480 86 2 .32  11 3.5  0 .11 22 1.8 0 4.1 350 42 2 .15 11 1.4 2 8.3 460 71 2 22   740 230 2 34   560 370 2 17   290 130 2
ldv-regression/test25_true-unreach-call.c .12  22 .67 0 2.8  36 40   2 4.3 320 36 0 5.6 310 46 2 210   1200 2100 2 220    1200 2400   2 1.7   31 23    2 2.6   39 37    2 .047 10   .50 0 16   600 130 2 .36  15 4.7  0 .21 23 2.1 0 4.5 380 43 2 .15 11 1.4 2 22   610 240 2 160   2000 2100 2 34   730 360 2 56   220 570 0
ldv-regression/test26_true-unreach-call_true-termination.c .11  22 .64 2 .40 33 4.7 2 2.9 270 24 2 2.9 270 28 2 3.0 270 27 2 3.8  270 36   2 .11  26 .63 2 .10  26 .68 2 .051 10   .56 0 3.1 280 27 2 .28  11 3.7  0 .15 21 1.7 2 4.0 250 41 2 .15 11 1.5 2 6.2 340 48 2 4.9 280 40 2 5.9 320 49 2 10   270 76 2
ldv-regression/test27_true-unreach-call_true-termination.c .11  22 .63 0 1.4  36 14   2 6.2 340 54 0 4.9 320 47 -16 40   640 400 2 22    660 280   2 .16  27 1.6  2 .20  27 2.0  2 .077 10   .48 0 38   1600 330 2 .065 11 .40 0 .17 23 1.9 0 4.3 270 44 2 .15 11 1.6 2 130   850 1400 2 170   2800 1700 2 900   1100 10000 0 40   500 390 2
ldv-regression/test28_true-unreach-call_true-termination.c .11  22 1.1  2 .41 33 5.0 2 2.7 270 26 2 2.9 270 27 2 3.2 270 25 2 4.0  270 37   2 .079 26 .83 2 .082 26 .90 2 .075 9.9 .51 0 900   5600 11000 0 .33  12 3.3  0 .13 21 1.8 2 5.5 310 53 0 .18 11 1.7 2 5.9 300 51 2 5.2 260 42 2 5.8 290 50 2 8.1 270 85 2
ldv-regression/test29_true-unreach-call_true-termination.c .12  22 .84 2 .40 33 4.9 2 3.1 300 23 2 2.8 270 26 2 3.3 270 29 2 3.9  270 33   2 .10  26 .75 2 .11  26 .73 2 .076 10   .36 0 3.4 270 32 2 .32  11 3.2  0 .15 22 1.7 2 5.6 330 57 0 .19 11 1.6 2 5.5 280 44 2 4.9 260 37 2 5.8 290 46 2 8.0 270 76 2
ldv-regression/test30_true-unreach-call_true-termination.c .13  22 1.0  -16 .45 33 3.8 2 2.9 280 30 2 3.0 270 27 2 3.2 270 28 2 3.8  270 35   2 .073 26 .71 2 .10  26 .60 2 1.8   32   840    0 3.0 260 32 2 .36  44 3.2  0 .14 22 1.7 2 5.5 310 49 0 .15 11 1.6 2 8.7 470 74 2 5.7 300 47 2 7.3 370 62 2 11   270 83 2
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i .48  40 3.8  0 32    640 380   1 9.0 490 70 1 5.0 310 47 1 9.2 420 76 1 890    1200 9500   0 .21  42 3.0  1 .24  42 2.5  1 .15  18   1.5  0 12   500 91 1 25     15000 330    0 .54 53 4.6 1 27   940 150 0 .47 17 5.3 1 320   1200 1700 0 610   1800 6300 0 590   2500 5800 1 20   280 150 0
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i .38  40 3.4  0 28    630 250   1 9.3 480 78 1 5.0 310 44 1 9.2 420 77 1 890    910 12000   0 .21  42 2.8  1 .21  42 2.8  1 .15  17   1.3  0 13   500 100 1 25     15000 330    0 .49 52 5.1 1 28   920 190 0 .47 15 4.9 1 320   1200 1600 0 650   1700 6800 0 590   2600 5300 1 20   280 160 0
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i .45  40 3.2  0 31    640 380   1 8.9 490 73 1 5.6 310 45 1 9.1 420 77 1 890    1200 11000   0 .20  42 2.2  1 .24  42 2.4  1 .12  17   1.7  0 14   510 110 1 25     15000 360    0 .51 51 4.6 1 29   960 160 0 .45 16 5.2 1 320   1200 2600 0 670   1700 7300 0 590   2500 4500 1 20   280 150 0
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i .37  40 3.5  0 870    1100 7800   0 6.3 310 49 2 2.9 270 26 2 97   2600 1200 2 900    1200 7600   0 900     8100 9900    0 .40  56 4.9  2 .13  17   1.6  0 4.7 290 36 2 900     3600 5900    0 .64 52 5.6 0 24   890 130 2 .32 14 3.9 2 9.6 510 74 2 150   820 1700 2 15   920 120 2 24   340 180 2
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i .38  40 2.8  0 870    1100 7800   0 6.3 300 50 2 3.1 270 29 2 97   3100 1100 2 900    1200 7300   0 900     8100 10000    0 .39  56 4.4  2 .13  17   1.5  0 4.9 290 43 2 900     3700 5700    0 .65 52 6.2 0 24   920 140 2 .32 14 4.3 2 9.2 500 76 2 130   870 1400 2 15   900 130 2 24   350 190 2
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i .38  40 3.1  0 870    1100 7200   0 6.7 310 57 2 2.9 270 25 2 97   3000 1000 2 900    1200 7700   0 900     8100 8600    0 .38  56 5.4  2 .12  17   1.6  0 4.8 290 40 2 900     3500 6000    0 .62 52 6.6 0 25   920 150 2 .35 14 3.9 2 9.8 510 72 2 140   840 1600 2 15   920 120 2 23   340 190 2
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i .40  40 2.9  0 870    1100 7900   0 6.8 310 57 2 2.9 270 30 2 98   2900 1000 2 900    1200 7200   0 900     7800 8800    0 .37  57 5.0  2 .12  17   1.6  0 4.9 300 42 2 900     3500 5700    0 .67 52 6.4 0 24   910 150 2 .32 14 4.0 2 10   520 85 2 140   880 1500 2 15   950 120 2 24   340 190 2
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i .40  40 3.0  0 870    1100 6300   0 6.8 310 56 2 3.0 270 29 2 98   2800 1000 2 900    1200 7500   0 900     8100 9500    0 .42  56 3.8  2 .14  17   1.4  0 4.7 290 42 2 900     3700 7300    0 .64 53 6.4 0 23   920 140 2 .34 14 4.2 2 10   520 81 2 130   850 1300 2 16   920 130 2 23   330 170 2
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i .38  40 2.5  0 870    1100 6500   0 7.0 320 53 2 2.9 270 30 2 98   3100 1200 2 900    1200 7000   0 900     8100 9700    0 .44  56 4.3  2 .15  17   1.1  0 4.7 300 38 2 900     3600 5600    0 .66 52 6.2 0 24   890 150 2 .32 14 4.0 2 9.9 520 83 2 140   850 1600 2 15   930 110 2 24   340 170 2
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i .40  40 3.0  0 870    1100 8000   0 6.8 310 55 2 3.0 260 25 2 97   2800 1100 2 900    1300 7900   0 900     7700 8500    0 .41  56 4.6  2 .15  17   1.6  0 4.9 300 41 2 900     3700 4900    0 .65 52 6.2 0 25   920 150 2 .34 14 3.5 2 9.7 520 70 2 150   880 1600 2 15   930 110 2 24   330 160 2
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i .41  40 3.1  0 870    1100 7900   0 6.8 310 59 2 3.0 260 28 2 98   3000 1100 2 900    1300 8600   0 900     8100 11000    0 .39  56 4.6  2 .12  19   1.4  0 4.6 290 42 2 900     3500 5700    0 .67 54 6.3 0 25   920 160 2 .34 14 4.1 2 10   520 78 2 150   840 1700 2 15   930 120 2 23   320 180 2
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i .41  40 2.9  0 870    1100 6500   0 6.9 320 54 2 2.9 270 25 2 97   2700 950 2 900    1200 10000   0 900     7800 8100    0 .38  56 5.0  2 .15  17   1.3  0 4.7 290 43 2 900     3600 5700    0 .64 52 6.5 0 24   910 150 2 .32 14 4.0 2 10   530 76 2 140   790 1700 2 16   920 110 2 24   340 170 2
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i .43  40 3.3  0 870    1100 7100   0 6.8 310 59 2 2.9 270 26 2 98   2800 1100 2 900    1200 7800   0 900     8100 8200    0 .39  57 4.3  2 .15  17   1.4  0 4.8 290 39 2 900     3600 7100    0 .68 52 6.2 0 24   930 150 2 .31 14 4.8 2 10   510 87 2 120   860 1200 2 16   920 130 2 23   350 160 2
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i .37  30 3.3  1 .49 37 4.6 1 4.6 320 37 1 20   710 170 1 210   720 2900 1 1.2  160 15   1 .43  29 4.1  1 .88  31 7.6  1 .096 13   1.0  1 900   4300 11000 0 82     15000 1000    0 .18 25 2.2 1 6.9 360 54 0 .19 11 2.2 1 14   560 110 1 13   600 110 1 11   540 88 1 900   2000 6700 0
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 92     15000 1200    0 .53 36 4.6 1 4.9 330 47 1 4.5 300 43 1 4.6 280 38 1 .83 130 9.9 1 .32  29 2.7  1 .51  29 5.2  1 .056 12   .64 1 8.9 450 76 1 .36  12 5.1  1 .15 25 1.9 1 6.6 320 60 0 .17 11 1.8 1 8.9 500 76 1 7.8 330 55 1 7.8 380 61 1 900   1000 11000 0
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i .29  29 3.0  1 .47 37 5.4 1 4.8 320 40 1 3.7 290 38 1 3.4 270 28 1 .69 130 8.0 1 .33  29 2.4  1 .35  29 3.4  1 .081 11   .52 1 4.0 290 33 1 .39  12 4.5  1 .17 23 1.9 1 6.7 370 60 0 .18 11 2.5 1 5.8 280 46 1 8.4 400 63 1 6.4 300 51 1 900   3900 8700 0
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i .28  29 2.9  0 1.3  37 15   1 4.7 320 39 0 4.6 300 42 0 17   640 130 0 3.6  140 42   0 1.5   31 13    1 1.1   30 10    1 1.3   25   18    1 34   1400 280 1 .26  12 2.6  0 .20 25 2.0 1 6.9 390 57 0 .22 11 2.2 0 77   1100 880 1 900   1300 12000 0 900   1200 12000 0 900   4100 7700 0
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i .25  30 2.2  1 .58 39 5.7 1 4.5 320 33 1 3.9 300 34 1 3.4 260 30 1 .58 130 7.3 1 .26  29 2.1  1 .57  29 4.9  1 .071 11   .55 1 4.4 290 42 1 .40  12 4.9  1 .14 24 1.8 1 6.9 330 57 0 .17 11 2.0 1 7.2 300 57 1 14   680 130 1 13   710 110 1 630   340 8500 0
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 98     15000 1500    0 .65 43 5.6 1 4.5 320 41 0 4.3 310 40 0 15   640 140 1 1.8  130 24   0 1.3   32 14    1 1.1   30 8.9  1 .50  20   6.5  1 910   4500 11000 0 .61  12 5.4  1 .19 24 2.2 1 7.1 390 59 0 .20 11 1.9 0 50   1000 470 1 48   850 490 1 900   1700 9900 0 660   410 7500 0
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i .24  27 1.9  1 .52 36 6.0 1 5.1 320 40 1 3.5 290 30 1 3.3 270 33 1 .72 190 8.4 1 .51  29 4.2  1 .73  29 6.2  1 .072 12   .84 1 3.7 280 30 1 .44  12 4.9  1 .16 25 1.9 1 6.8 350 58 0 .18 11 2.1 1 5.4 290 46 1 6.7 340 57 1 6.0 290 51 1 900   3000 10000 0
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i .38  31 3.5  0 .50 36 5.7 1 5.0 320 47 1 3.7 290 31 1 4.9 290 41 1 1.8  210 23   1 .78  30 7.4  1 .52  29 4.3  1 .078 12   .87 1 6.9 390 59 1 .50  12 6.1  1 .85 31 11   1 7.5 400 64 0 .21 11 2.4 1 7.6 350 62 1 8.3 400 68 1 7.0 310 55 1 900   820 11000 0
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i .25  29 1.9  1 .50 36 5.2 1 4.6 320 43 1 3.5 290 29 1 4.5 280 44 1 .72 130 9.8 1 .45  29 4.0  1 .44  29 6.7  0 .083 12   .59 1 4.3 290 36 1 .40  12 4.5  1 .13 29 2.1 1 6.7 350 58 0 .20 11 2.1 1 23   540 220 1 9.4 420 68 1 8.1 370 57 1 900   2400 11000 0
forester-heap/sll-01_false-unreach-call_false-valid-deref.i .32  29 2.8  0 .51 36 4.5 1 4.3 310 41 0 30   1200 240 0 240   1700 3100 1 2.1  160 28   1 1.1   33 10    1 .83  30 7.4  1 .086 12   .74 0 900   4200 11000 0 900     3800 5000    0 .15 25 2.3 0 6.6 330 55 0 900    2200 7200   0 21   720 170 1 24   780 250 1 23   910 210 1 900   1900 6200 0
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i .34  29 2.4  0 .56 36 4.9 1 4.9 330 43 0 9.4 470 72 0 270   2300 3600 0 1.7  190 21   0 1.1   31 8.9  1 .73  29 6.6  1 .069 12   .88 1 13   500 110 1 .52  12 5.5  1 .19 25 2.1 0 7.3 380 64 0 .22 15 2.0 0 55   920 630 1 22   740 240 1 40   900 390 -32 65   610 660 0
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i .32  29 3.2  1 .48 36 4.8 1 4.6 320 39 1 4.5 310 39 1 4.4 280 34 1 .82 130 10   1 .29  29 2.2  1 .49  29 4.2  1 .071 11   .54 1 8.7 480 63 1 .38  12 4.2  1 .13 21 1.9 1 6.1 320 54 0 .17 11 1.8 1 9.2 470 66 1 7.1 360 65 1 7.7 380 67 1 900   940 9000 0
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i .31  28 2.6  1 .48 36 4.5 1 4.9 320 44 1 3.7 290 32 1 3.4 260 31 1 .67 130 8.3 1 .26  29 2.8  1 .29  29 3.0  1 .054 11   .52 1 3.9 290 31 1 .42  12 4.9  1 .16 23 2.0 1 6.7 350 52 0 .21 11 2.0 1 5.4 280 41 1 7.6 370 69 1 5.9 300 49 1 900   4100 7800 0
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i .30  30 3.1  0 1.3  37 12   1 4.8 310 46 0 4.4 300 40 0 17   680 130 0 3.4  140 43   0 1.2   31 12    1 .91  30 10    1 .12  14   1.5  1 33   1400 300 1 .26  11 2.5  0 .16 25 2.1 1 7.0 380 63 0 .19 11 2.5 0 150   800 2000 0 64   1400 760 1 140   1300 1600 0 900   3900 7500 0
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i .25  27 2.7  1 .53 37 5.0 1 4.5 320 42 1 3.8 290 36 1 5.8 310 44 1 .57 130 6.4 1 .21  29 1.7  1 .44  29 2.9  1 .056 11   .59 1 4.5 290 39 1 .40  12 4.4  1 .16 23 1.8 1 6.0 310 55 0 .17 11 1.6 1 6.5 290 53 1 11   500 90 1 15   640 97 1 710   290 9000 0
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i .37  33 3.9  0 .52 36 5.4 1 4.6 310 40 0 6.0 340 52 0 9.0 490 68 1 1.5  130 19   0 .95  31 8.1  1 .66  29 8.0  1 .26  18   3.4  1 900   4100 11000 0 .50  12 6.6  1 .21 24 2.3 1 6.1 330 48 0 .19 11 1.8 0 37   890 350 1 28   820 270 1 900   3200 7300 0 620   350 7000 0
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i .25  27 1.9  1 .52 36 4.5 1 4.8 320 44 1 3.6 290 29 1 3.4 270 31 1 .68 190 8.0 1 .44  29 3.7  1 .63  29 5.0  1 .096 12   .69 1 3.7 280 32 1 .44  12 5.1  1 .12 24 2.1 1 6.7 330 57 0 .20 11 2.0 1 5.9 290 43 1 6.3 320 49 1 5.7 300 51 1 900   2800 12000 0
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i .31  30 2.9  0 .49 36 4.9 1 4.9 320 40 1 5.2 310 48 1 35   1600 340 1 1.8  210 26   1 .90  29 7.5  1 .65  29 6.2  0 .14  15   1.3  1 160   3700 1700 1 .52  12 6.7  1 .97 25 11   1 6.6 330 56 0 .21 12 2.0 1 180   1100 2000 1 510   1500 7000 1 900   1300 11000 0 900   1800 11000 0
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i .23  27 2.0  1 .49 37 5.2 1 4.9 320 42 1 3.4 280 32 1 4.1 280 36 1 .68 130 9.0 1 .38  29 3.1  1 .40  29 3.6  0 .071 11   .57 1 4.0 290 34 1 .38  12 4.8  1 .16 23 1.9 1 6.1 320 52 0 .19 11 1.9 1 6.8 300 56 1 6.4 340 49 1 6.2 290 51 1 900   2500 9100 0
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i .33  29 3.4  0 870    2100 8600   0 4.3 310 39 -16 71   2100 730 2 900   2400 7200 0 890    540 10000   0 900     1200 10000    0 900     1200 9600    0 .53  29   6.4  2 900   4300 11000 0 900     3400 9100    0 900    320 9200   0 6.3 330 45 0 900    5500 7800   0 900   1300 10000 0 900   11000 11000 0 370   1300 4600 0 900   1400 6400 0
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i .31  30 3.6  0 390    15000 4500   0 4.9 320 41 -16 7.3 400 64 2 900   2300 5500 0 890    210 9500   0 900     2500 9200    0 900     2500 10000    0 31     130   400    2 900   4100 11000 0 900     370 11000    0 2.3  39 22   2 6.4 320 51 0 900    5200 8600   0 900   1400 7500 0 900   1400 14000 0 900   1200 13000 0 900   1000 10000 0
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i .32  30 3.0  0 870    2600 4400   0 5.6 330 48 -16 12   490 95 2 900   2000 7000 0 900    480 10000   0 900     3900 8000    0 900     4000 10000    0 1.3   41   18    2 900   4100 11000 0 900     2300 13000    0 900    820 5300   0 7.1 340 59 0 900    4200 6000   0 900   1000 11000 0 900   12000 8200 0 900   1600 14000 0 900   4300 9000 0
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i .25  29 2.5  0 870    1500 4000   0 4.7 320 37 -16 4.5 300 39 0 900   2900 8100 0 900    920 11000   0 900     3900 8900    0 900     3900 9100    0 10     78   130    2 900   4200 11000 0 .22  12 2.8  0 2.1  25 20   2 6.7 360 61 0 900    2200 9900   0 900   1200 11000 0 900   1400 13000 0 900   1200 12000 0 900   4000 8300 0
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 71     15000 890    0 870    2900 5700   0 4.5 330 39 -16 8.8 460 71 2 900   2700 6000 0 890    270 9900   0 900     3900 10000    0 900     4100 7800    0 1.4   37   17    2 900   4300 14000 0 900     1400 9200    0 900    3500 5500   0 6.4 330 59 0 900    4900 6200   0 900   1100 11000 0 900   3700 13000 0 900   1400 12000 0 660   420 7100 0
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 98     15000 1400    0 870    3200 5500   0 4.5 320 42 -16 4.3 310 37 -16 900   2300 8300 0 890    380 10000   0 900     6400 9400    0 900     5800 11000    0 1.3   37   18    2 900   4200 12000 0 900     1400 9700    0 900    3500 6500   0 7.0 380 64 0 900    5100 4000   0 900   1200 11000 0 900   2600 10000 0 900   2400 9600 0 680   410 7200 0
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 100     15000 1400    0 880    5300 6700   0 5.1 320 43 -16 29   1200 300 2 900   4000 6600 0 890    190 10000   0 900     2800 11000    0 900     2800 9900    0 240     690   2900    2 900   4100 13000 0 900     420 12000    0 2.2  32 26   2 7.1 360 57 0 900    5900 11000   0 900   1100 13000 0 900   1200 12000 0 900   1200 12000 0 770   300 8600 0
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i .33  30 3.5  0 880    9900 7000   0 6.2 330 49 -16 6.9 450 55 2 900   6100 7200 0 890    190 9700   0 900     1900 9200    0 900     1900 9000    0 1.6   37   23    2 900   4200 13000 0 900     160 10000    0 3.5  30 26   2 6.5 320 60 0 900    5000 10000   0 900   820 12000 0 900   1400 13000 0 900   1200 10000 0 900   3000 11000 0
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i .40  30 4.1  0 870    920 9100   0 5.0 320 46 -16 5.9 310 47 2 910   6200 8500 0 890    210 10000   0 900     1000 10000    0 900     1300 9600    0 120     450   1700    2 900   4200 10000 0 900     2000 12000    0 2.2  37 22   2 7.4 400 63 0 900    330 11000   0 900   1100 14000 0 900   1500 9000 0 900   1300 11000 0 900   820 9100 0
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i .33  30 3.6  0 870    970 10000   0 4.6 320 41 -16 4.4 280 35 2 900   3200 5100 0 890    280 12000   0 900     3200 8400    0 900     3100 7700    0 .14  13   .95 2 900   3900 11000 0 890     80 11000    0 1.8  31 19   2 6.3 350 52 0