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-05 07:52:24 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 10   470 83 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 200   3400 2600 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.2 300 44 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 96 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 86   3100 990 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 92   3300 940 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 140   4000 1500 -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 220   3700 2600 -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   4500 11000 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 11000 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   4000 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 470 61 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   4200 13000 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.7 290 41 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 85 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.4 330 53 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 95   3700 1000 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 13000 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   4500 12000 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 22   1100 160 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 12000 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 13000 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   4200 13000 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 14000 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.2 270 32 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.5 290 40 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.7 270 27 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.6 280 32 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.8 280 25 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 280 27 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.1 270 30 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.5 300 45 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 7.1 380 55 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.3 300 43 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.2 270 31 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.2 280 29 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.9 280 23 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.7 270 26 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 3.0 270 26 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.7 270 23 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 15   610 120 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.5 270 21 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 270 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 2.9 280 25 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 260 23 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.8 270 27 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 270 29 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.9 280 23 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 270 26 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 3.0 280 27 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.8 270 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.4 300 43 -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 17   630 130 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.7 290 38 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.3 280 29 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.7 270 27 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.3 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.9 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.2 280 29 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 30 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.6 280 31 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.7 260 24 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 2.9 280 26 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 260 28 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 280 22 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.8 270 27 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.7 260 23 -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 280 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.8 280 24 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.7 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.2 270 25 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 280 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.8 280 28 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.8 270 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.4 460 76 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 19   850 150 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 13   610 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   1200 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.7 270 25 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.4 470 61 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 280 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.3 280 33 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 29 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.7 260 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.9 270 24 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.6 280 29 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.5 260 28 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.1 280 26 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.1 280 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.1 270 29 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.9 280 26 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 3.1 270 25 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 270 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.9 270 25 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 280 24 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 3.0 280 28 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 280 26 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.9 280 26 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 30 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 11   460 88 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 46   2200 390 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 9.1 460 72 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   620 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.0 260 24 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 36   1900 320 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 13000 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.6 290 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.1 260 26 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 13   500 110 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 110 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 13   480 94 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.6 290 37 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.6 290 39 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 37 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.8 290 37 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 290 39 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.6 300 37 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.8 290 35 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.8 300 35 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.9 290 42 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   4400 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 9.0 460 72 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 3.9 280 37 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 38   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.6 290 44 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 900   4300 12000 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.8 280 31 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 7.1 380 55 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.4 290 40 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   490 95 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.8 460 61 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 280 33 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 38   1700 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 35 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   4400 12000 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.6 280 33 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 140   3700 2000 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 3.9 290 32 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 13000 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 12000 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   4100 12000 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 11000 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 11000 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   4300 11000 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 13000 0 890     80 11000    0 1.8  31 19   2 6.3 350 52 0 900    110 9200   0 900   730 11000 0 900   1800 11000 0 900   1200 6300 0 900   1900 9500 0
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i .30  29 3.3  0 880    8500 11000   0 4.4 310 40 -16 37   1300 290 2 900   2300 7300 0 900    620 8500   0 900     1100 11000    0 900     1200 9400    0 .93  39   11    2 900   4100 11000 0 900     3700 10000    0 900    280 10000   0 6.3 330 59 0 900    5900 5200   0 900   1400 13000 0 900   5800 11000 0 900   1200 12000 0 900   1500 8800 0
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i .31  29 3.5  0 870    520 12000   0 5.0 330 41 -16 900   5900 9800 0 900   5500 10000 0 890    190 9500   0 900     210 11000    0 900     230 13000    0 660     1600   8100    2 900   4200 12000 0 900     810 11000    0 2.3  39 26   2 7.2 370 62 0 900    4500 5000   0 900   1100 12000 0 260   1100 3200 0 49   1100 540 2 67   610 660 0
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i .31  30 3.1  0 380    15000 4100   0 4.5 320 38 -16 6.5 370 59 2 900   2400 6400 0 890    190 12000   0 900     2100 8900    0 900     2100 8900    0 2.1   47   24    2 900   4000 13000 0 900     410 12000    0 2.3  38 24   2 6.3 320 59 0 900    5000 11000   0 900   1300 12000 0 900   1200 13000 0 900   2200 10000 0 900   940 9000 0
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i .34  29 2.4  0 880    2200 4200   0 5.4 330 45 -16 11   470 89 2 900   1900 6000 0 900    520 11000   0 900     3600 10000    0 900     3700 7800    0 .97  35   13    2 900   4100 13000 0 900     2300 12000    0 900    690 6100   0 6.9 350 56 0 900    4100 6000   0 900   1000 13000 0 900   13000 7900 0 900   1500 13000 0 900   4200 9100 0
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i .32  30 2.5  0 870    1100 3600   0 4.9 320 40 -16 4.7 310 39 0 900   2900 8100 0 900    940 11000   0 900     3500 9800    0 900     3600 8200    0 17     91   240    2 900   4100 12000 0 .23  11 2.9  0 2.1  25 25   2 7.1 370 58 0 900    2500 11000   0 150   820 1900 0 900   1900 14000 0 250   1300 3700 0 900   3900 7400 0
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i .23  28 2.0  0 870    2100 5400   0 4.6 320 41 -16 7.8 460 61 2 900   2100 5800 0 890    190 10000   0 900     3000 12000    0 900     2900 12000    0 6.1   52   76    2 900   4200 13000 0 900     2200 11000    0 900    3600 6700   0 6.2 320 55 0 900    5200 4900   0 900   1100 12000 0 580   2000 6800 0 900   5300 8600 0 550   300 7000 0
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i .36  33 3.4  0 870    2100 5500   0 4.7 320 38 -16 6.8 420 56 0 900   2000 8400 0 890    200 12000   0 900     2800 9900    0 900     3100 12000    0 .49  22   5.8  2 900   4100 11000 0 900     2400 13000    0 900    3500 5900   0 6.8 340 61 0 900    5100 5000   0 900   1100 10000 0 900   980 13000 0 900   2800 8400 0 630   380 7100 0
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i .34  30 3.4  0 870    2200 6900   0 4.9 320 46 -16 29   1200 230 2 900   4100 6900 0 890    190 10000   0 900     2100 10000    0 900     2000 11000    0 4.3   66   58    2 900   4000 11000 0 900     400 10000    0 2.2  29 25   2 6.3 350 53 0 900    6200 11000   0 900   1200 12000 0 900   2100 13000 0 900   1300 13000 0 810   260 9700 0
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i .27  29 2.4  0 880    6000 5700   0 6.4 350 51 -16 8.5 450 64 2 900   5900 6600 0 890    190 9600   0 900     1400 11000    0 900     1600 11000    0 .69  24   9.2  2 900   4100 11000 0 890     160 11000    0 3.7  29 33   2 6.7 360 54 0 900    5000 9400   0 900   760 14000 0 900   1500 13000 0 190   1100 2200 0 900   2800 10000 0
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i .39  32 4.0  0 870    7500 6100   0 5.0 330 51 -16 6.0 330 50 2 900   6700 8200 0 890    210 10000   0 900     1200 10000    0 900     1300 12000    0 190     390   2300    2 900   4300 11000 0 900     1700 11000    0 2.2  37 24   2 7.3 380 65 0 900    400 11000   0 900   1200 11000 0 900   2000 12000 0 350   1200 4100 0 900   920 8800 0
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i .34  30 3.4  0 870    970 9900   0 4.8 320 42 -16 4.8 290 39 2 900   3500 5500 0 890    340 9400   0 900     2700 8800    0 900     2800 7600    0 .10  14   1.1  2 900   3900 11000 0 890     81 12000    0 2.1  32 23   2 6.4 430 56 0 900    110 8200   0 900   790 11000 0 900   2300 12000 0 900   1400 10000 0 900   2400 7700 0
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i .73  37 9.0  1 .50 38 5.7 1 4.8 320 44 1 14   490 100 1 4.7 290 40 1 .93 270 12   1 .21  29 2.0  1 .64  30 5.5  1 .10  12   .85 1 900   4200 13000 0 .41  12 5.3  1 .13 24 1.9 1 8.7 540 66 0 .18 11 2.1 1 5.3 280 42 1 5.9 320 53 1 5.4 280 45 1 900   4200 11000 0
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i .35  32 3.1  0 .48 36 5.4 0 900   6100 10000 0 35   980 300 0 900   3900 7200 0 15    190 230   0 8.4   53 93    0 6.7   44 65    0 .073 11   .55 0 900   4200 11000 0 39     380 410    1 .17 23 2.0 0 6.0 320 53 0 1.9  31 25   0 900   880 11000 0 900   1700 13000 0 900   2900 10000 0 900   1700 8200 0
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i .32  29 2.9  1 .46 36 4.0 1 4.5 290 37 1 4.3 290 39 1 3.3 260 32 1 .79 180 12   1 .19  28 2.1  1 .27  29 2.4  0 .081 10   .45 1 40   2100 350 1 .38  12 4.8  1 .13 24 1.8 1 5.8 340 54 0 .18 11 2.1 1 5.2 280 44 1 5.6 290 47 1 5.3 290 45 1 900   2300 9300 0
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i .60  35 7.0  0 .75 47 8.4 1 900   6500 12000 0 5.8 320 55 1 600   1900 7500 1 1.9  350 24   0 1.3   40 15    0 .88  33 8.2  1 5.0   56   880    0 900   4200 11000 0 1.2   14 15    -32 1.3  25 14   1 7.4 420 63 0 .20 11 2.1 1 36   910 360 1 25   760 230 1 900   2600 11000 0 530   820 6000 0
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i .61  35 6.3  0 870    2000 5100   0 900   5800 11000 0 6.6 390 51 2 900   1500 12000 0 890    370 10000   0 900     2300 11000    0 900     2200 9500    0 5.3   60   920    0 900   4400 13000 0 900     590 12000    0 900    1300 5900   0 7.4 390 59 0 900    1400 10000   0 900   1300 13000 0 900   1500 14000 0 500   2400 6300 0 530   840 5900 0
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i .57  34 6.3  0 .50 36 5.0 1 4.8 310 47 1 3.7 290 30 0 5.3 280 45 1 1.5  270 19   1 .74  32 6.9  1 .51  30 5.3  1 .096 13   .99 1 6.2 310 51 1 .41  12 4.9  1 2.2  63 25   1 7.6 410 73 0 .18 11 2.1 1 7.6 350 64 1 7.9 390 66 1 9.8 550 84 1 750   760 8800 0
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i .50  33 5.8  0 870    350 12000   0 910   7100 10000 0 4.5 290 45 2 900   8200 8600 0 890    270 10000   0 900     2000 8800    0 900     1800 10000    0 .58  31   7.3  2 900   4300 11000 0 900     1200 11000    0 900    1600 8400   0 7.3 380 65 0 900    1300 9200   0 900   1100 12000 0 900   2400 13000 0 290   1100 3200 0 750   760 9200 0
list-ext2-properties/simple_search_value_false-unreach-call.i .37  30 4.0  0 2.2  36 21   1 900   7100 12000 0 12   400 99 0 56   2000 490 1 9.1  160 130   1 4.0   42 41    1 3.3   39 33    1 2.4   44   850    0 900   3500 13000 0 .51  85 6.8  1 1.7  24 20   1 6.2 310 57 0 .18 11 2.0 1 900   4700 12000 0 900   13000 10000 0 900   1900 14000 0 250   3900 3100 0
list-ext2-properties/simple_search_value_true-unreach-call.i .33  30 3.0  0 880    12000 9600   0 900   7200 9500 0 11   400 91 0 900   3200 7200 0 900    550 9000   0 900     4800 11000    0 900     4500 9300    0 2.5   45   920    0 900   3400 11000 0 890     82 10000    0 900    1200 9600   0 6.6 320 58 0 900    590 11000   0 900   2600 10000 0 900   4700 12000 0 900   2100 13000 0 900   3300 9000 0
ldv-sets/test_add_false-unreach-call_true-termination.i .16  26 1.6  0 .50 36 4.2 1 5.4 320 46 1 4.2 300 38 0 4.7 290 40 1 .57 100 6.5 0 .034 15 .27 0 .060 15 .28 0 .053 11   .57 0 6.6 320 43 1 .40  12 5.2  1 .19 26 1.8 1 6.4 350 59 0 .20 11 2.5 1 9.9 550 75 1 900   1600 11000 0 15   710 120 1 22   250 170 0
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i .20  26 2.1  0 .55 37 4.9 1 5.8 310 51 1 4.7 300 39 0 5.1 300 44 1 3.4  270 43   0 .038 15 .23 0 .060 15 .30 0 .13  17   1.9  0 28   990 210 1 .40  12 5.4  1 .18 26 2.2 1 8.8 520 83 0 .22 11 2.1 1 15   620 140 1 12   540 110 1 23   770 190 1 25   270 210 0
ldv-sets/test_mutex_double_unlock_false-unreach-call.i .20  27 2.4  0 1.8  48 17   1 900   7700 12000 0 4.6 300 35 0 750   7900 6600 1 140    310 1300   0 .036 15 .33 0 .036 15 .23 0 .16  18   1.9  0 900   3700 12000 0 .47  12 6.0  0 .21 25 2.3 1 9.5 520 84 0 .21 11 2.4 0 900   1300 12000 0 900   2000 12000 0 170   850 2000 0 26   270 210 0
ldv-sets/test_mutex_unbounded_false-unreach-call.i .20  27 1.8  0 .78 47 7.7 1 900   7600 8600 0 8.6 430 71 0 88   3900 770 1 25    240 250   0 .063 15 .24 0 .061 15 .20 0 .079 12   .60 0 110   3700 1300 1 .56  12 7.3  0 .18 27 2.2 1 9.2 520 68 0 .21 11 2.6 0 900   1100 11000 0 900   1500 10000 0 900   950 9300 0 290   4500 2700 0
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i .20  27 2.1  0 1.6  40 18   1 900   7900 9600 0 4.6 300 38 0 120   1500 1200 1 83    220 790   0 .057 15 .32 0 .036 15 .32 0 .16  17   1.5  0 49   2200 350 0 93     15000 1100    0 .26 26 2.8 1 8.8 520 73 0 .21 11 2.1 0 900   990 10000 0 900   2000 14000 0 210   930 2600 0 24   270 180 0
ldv-sets/test_add_true-unreach-call_true-termination.i .19  27 1.4  0 .90 36 7.6 2 900   7800 12000 0 4.4 290 39 2 5.3 310 48 2 1.4  100 23   2 .032 15 .34 0 .063 15 .28 0 .081 11   .46 0 8.6 450 73 2 .43  12 4.8  2 .20 27 2.2 2 6.6 350 53 0 .20 11 2.2 2 310   970 3700 0 900   1700 11000 0 110   960 1200 0 22   260 160 0
ldv-sets/test_mutex_true-unreach-call.i .20  27 2.1  0 2.2  46 26   2 900   7100 9000 0 4.6 310 41 0 350   3500 3700 2 440    1500 4600   2 .037 15 .25 0 .034 15 .35 0 .16  18   1.6  0 36   2100 310 -16 .48  12 5.9  2 .32 25 3.4 2 9.3 530 71 0 .22 11 2.3 2 900   1400 13000 0 900   2400 11000 0 180   860 2500 0 26   260 230 0
ldv-sets/test_mutex_unbounded_true-unreach-call.i .17  27 1.8  0 870    12000 6000   0 900   7700 9400 0 33   1400 320 0 900   5900 7200 0 890    1200 7600   0 .033 15 .33 0 .058 15 .32 0 .086 11   .57 0 900   4500 11000 0 890     130 13000    0 900    4000 7900   0 8.5 500 67 0 900    8100 8800   0 900   1100 13000 0 900   1600 12000 0 900   930 9400 0 290   4500 3000 0
../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
total 181 590    95000 7800   108 181 40000   210000 330000 192 181 24000 220000 260000 -168 181 2000 74000 20000 71 181 40000 250000 350000 193 181 46000 61000 510000 163 181 42000 210000 440000 174 181 33000 140000 350000 191 181 1300   6300 25000 139 181 44000 280000 570000 113 181 41000    150000 440000   46 181 15000    33000 120000   203 181 1300 67000 11000 135 181 34000   120000 330000 201 181 44000 130000 540000 200 181 54000 220000 690000 186 181 42000 160000 490000 157 181 55000   170000 590000 129
    correct results 86 13    2100 110   140 129 170   6400 1800 192 119 500 36000 4400 184 135 780 48000 7000 231 136 4200 91000 45000 209 100 1000 25000 11000 163 113 41 3200 410 174 120 44 3700 450 191 82 1300   4800 16000 139 124 1200 59000 11000 193 89 75    1500 830   126 140 81    3700 880   219 73 510 26000 4000 135 128 24   1500 260 201 129 2200 57000 23000 200 119 3200 56000 35000 186 119 3300 61000 30000 189 92 1700   30000 16000 161
        correct true 54 6.2  1200 45   108 63 38   2100 390 126 65 230 18000 2100 130 96 600 36000 5400 192 73 1800 51000 19000 146 63 990 20000 10000 126 61 14 1600 160 122 71 20 2200 230 142 57 1300   4400 16000 114 69 380 25000 3200 138 37 13    420 150   74 79 58    2100 620   158 62 450 22000 3400 124 73 13   820 140 146 71 930 29000 9500 142 67 2100 31000 22000 134 70 800 34000 7100 140 69 960   21000 7700 138
        correct false 32 7.1  830 65   32 66 130   4200 1400 66 54 270 18000 2300 54 39 180 12000 1600 39 63 2400 39000 25000 63 37 52 5100 640 37 52 27 1600 260 52 49 24 1500 220 49 25 3.9 320 45 25 55 800 34000 8000 55 52 62    1100 680   52 61 23    1700 260   61 11 56 3300 530 11 55 11   640 120 55 58 1300 28000 13000 58 52 1100 25000 13000 52 49 2500 28000 22000 49 23 750   9100 8000 23
    correct-unconfimed results 3 1.1  99 12   0 4 4.5 150 48 0 6 27 1900 240 0 21 150 9000 1300 0 6 1100 9800 13000 0 30 340 5700 3500 0 10 17 330 180 0 13 18 450 190 0 0 6 460 13000 5200 0 3 1.6  36 20   0 3 2.7  100 28   0 0 14 4.6 180 55 0 1 130 1200 1500 0 1 24 570 220 0 3 580 4900 6400 0 2 280   4300 3300 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 3 1.1  99 12   0 4 4.5 150 48 0 6 27 1900 240 0 21 150 9000 1300 0 6 1100 9800 13000 0 30 340 5700 3500 0 10 17 330 180 0 13 18 450 190 0 0 6 460 13000 5200 0 3 1.6  36 20   0 3 2.7  100 28   0 0 14 4.6 180 55 0 1 130 1200 1500 0 1 24 570 220 0 3 580 4900 6400 0 2 280   4300 3300 0
    incorrect results 2 .55 55 6.4 -32 0 22 110 7100 940 -352 7 54 3000 480 -160 1 630 3000 6600 -16 0 0 0 0 5 400 10000 4400 -80 3 1.9  37 24   -80 1 .18 24 1.9 -16 0 0 0 0 1 40 900 390 -32 1 6.3 290 46 -32
        incorrect true 0 0 0 3 39 1800 340 -96 0 0 0 0 0 0 2 1.6  26 20   -64 0 0 0 0 0 1 40 900 390 -32 1 6.3 290 46 -32
        incorrect false 2 .55 55 6.4 -32 0 22 110 7100 940 -352 4 16 1200 140 -64 1 630 3000 6600 -16 0 0 0 0 5 400 10000 4400 -80 1 .34 11 3.6 -16 1 .18 24 1.9 -16 0 0 0 0 0 0
score (181 tasks, max score: 291) 108 192 -168 71 193 163 174 191 139 113 46 203 135 201 200 186 157 129
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