Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux Map2Check v7.2-Flock : Tue Nov 27 22:00:00 -04 2018 PeSCo 1.7-svn b8d6131600+ Pinaka 0.1 PredatorHP 3.14 skink 2.0 SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a VeriAbs 1.3.10 VeriFuzz 1.0.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:20:21 CET 2018-12-06 12:44:04 CET 2018-12-06 20:14:43 CET 2018-12-07 04:08:42 CET 2018-12-07 12:00:55 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET 2018-12-10 16:50:17 CET 2018-12-09 02:47:33 CET
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-Heap cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Heap depthk.sv-comp19_prop-reachsafety.ReachSafety-Heap divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Heap divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Heap esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Heap map2check.sv-comp19_prop-reachsafety.ReachSafety-Heap pesco.sv-comp19_prop-reachsafety.ReachSafety-Heap pinaka.sv-comp19_prop-reachsafety.ReachSafety-Heap predatorhp.sv-comp19_prop-reachsafety.ReachSafety-Heap skink.sv-comp19_prop-reachsafety.ReachSafety-Heap smack.sv-comp19_prop-reachsafety.ReachSafety-Heap symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Heap ukojak.sv-comp19_prop-reachsafety.ReachSafety-Heap utaipan.sv-comp19_prop-reachsafety.ReachSafety-Heap veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Heap
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s --graphml-witness witness.graphml --witness error-witness.graphml -w 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 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 error (134) .17  29 1.7  0 false(unreach-call) .21  16   2.3  1 false(unreach-call) .90  66   9.7  1 timeout 900   2300 7400 0 false(unreach-call) .23 35 2.4 1 unknown 8.5 450 120 0 unknown 8.6 450 110 0 false(unreach-call) .17  28 2.4  1 unknown .91 40 11   0 false(unreach-call) 18 1400 140 1 error (8) .76 68 6.7 0 false(unreach-call) .48 53 3.3 1 unknown 15   370 140 0 disqualified 3.6 89 46 0 false(unreach-call) .27 17 2.5 1 timeout 900   1000 7400 0 timeout 900   1000 10000 0 timeout 900   1000 7400 0 false(unreach-call) 330   10000 3200 1 false(unreach-call) 7.1 600 90 1
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error (5) 1.6   27 22    0 false(unreach-call) .23  13   3.1  0 error (134) .16  20   1.7  0 assertion 42   2200 410 0 unknown 900    12000 7600   0 unknown 8.6 460 89 0 unknown 8.7 460 110 0 timeout 900     9200 5600    0 unknown .92 40 12   0 false(unreach-call) 58 1800 580 0 timeout 900    490 9400   0 false(unreach-call) 2.8  64 30   0 unknown 23   580 180 0 disqualified 88   150 1100 0 false(unreach-call) .29 17 3.0 0 timeout 900   2200 9600 0 timeout 900   1600 9800 0 timeout 910   6800 8900 0 false(unreach-call) 340   1300 3700 0 error (1) 7.4 540 72 0
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i timeout 900     3400 6500    0 false(unreach-call) .25  20   3.5  1 error (134) .071 8.9 1.0  0 false(unreach-call) 52   2100 420 0 false(unreach-call) .73 38 9.8 1 false(unreach-call) 8.4 450 100 1 false(unreach-call) 8.4 450 110 1 false(unreach-call) .56  36 8.2  1 unknown .87 41 11   0 false(unreach-call) 66 1700 540 0 timeout 900    300 9200   0 false(unreach-call) .24 36 1.8 1 unknown 14   330 120 0 disqualified 3.5 91 49 0 false(unreach-call) .25 22 3.3 1 false(unreach-call) 14   560 100 1 false(unreach-call) 16   620 130 1 false(unreach-call) 14   500 110 1 false(unreach-call) 340   550 4100 1 false(unreach-call) 6.9 560 70 1
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i timeout 900     5100 11000    0 false(unreach-call) .19  13   2.3  1 error (134) .11  13   1.1  0 false(unreach-call) 8.9 490 70 0 false(unreach-call) .19 35 2.6 0 false(unreach-call) 8.5 460 110 1 false(unreach-call) 8.6 460 93 1 false(unreach-call) .15  27 1.4  0 unknown .88 40 9.3 0 false(unreach-call) 17 1200 110 0 timeout 900    460 9300   0 false(unreach-call) .76 48 7.3 1 unknown 15   370 140 0 disqualified 3.5 94 49 0 false(unreach-call) .25 17 3.0 0 false(unreach-call) 120   840 1300 0 timeout 900   1100 10000 0 timeout 910   14000 4600 0 false(unreach-call) 230   3200 2300 1 false(unreach-call) 12   540 140 1
heap-manipulation/tree_false-unreach-call_false-valid-deref.i error (5) 470     2100 3900    0 false(unreach-call) .17  12   1.9  1 error (134) .12  9.3 .90 0 false(unreach-call) 14   550 110 1 false(unreach-call) .49 35 4.7 1 unknown 8.5 450 100 0 unknown 8.9 450 96 0 false(unreach-call) .22  27 2.9  1 unknown .83 40 8.8 0 false(unreach-call) 22 1200 160 1 timeout 900    650 9400   0 timeout 900    140 12000   0 unknown 14   330 130 0 disqualified 3.4 88 46 0 false(unreach-call) .23 17 2.7 0 false(unreach-call) 23   530 210 1 false(unreach-call) 21   570 190 1 true 580   810 7600 -32 false(unreach-call) 110   760 1400 1 false(unreach-call) 16   660 180 1
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i error (5) 530     2500 4300    0 false(unreach-call) .17  12   2.3  1 error (134) .087 8.9 .80 0 false(unreach-call) 15   550 110 1 false(unreach-call) .48 35 6.5 0 unknown 8.4 450 99 0 false(unreach-call) 9.1 450 110 1 false(unreach-call) .20  27 2.5  0 unknown .83 40 10   0 false(unreach-call) 22 1200 160 1 timeout 900    650 9100   0 false(unreach-call) .63 39 6.1 1 unknown 14   340 140 0 disqualified 3.4 87 49 0 false(unreach-call) .25 19 3.4 0 true 21   730 180 -32 false(unreach-call) 32   800 280 1 false(unreach-call) 670   750 9000 1 false(unreach-call) 110   760 1200 1 false(unreach-call) 17   660 190 1
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (134) .19  29 1.6  0 error (42) 880     3500   7600    0 out of memory 170     15000   2400    0 timeout 900   1800 7300 0 true 470    15000 5300   2 unknown 8.5 450 100 0 timeout 900   570 8100 0 timeout 900     5200 9300    0 unknown .94 41 11   0 timeout 910 2400 7800 0 error (8) .78 68 6.7 0 true .70 68 4.4 2 unknown 15   370 130 0 disqualified 880   400 9000 0 timeout (verification) 900    860 11000   0 timeout 900   1000 7200 0 timeout 900   880 11000 0 timeout 900   1100 7000 0 unknown 660   10000 6600 0 error (1) 880   600 12000 0
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (5) .19  26 1.4  0 error (42) 880     490   9300    0 out of memory 240     15000   3100    0 error (recursion) 7.1 370 63 0 true 5.0  230 64   2 unknown 8.6 450 120 0 timeout 900   410 6500 0 timeout 900     3000 8800    0 unknown .80 39 12   0 unknown 18 1200 150 0 timeout 900    640 9300   0 true .61 50 2.7 2 unknown 12   320 110 0 disqualified 880   420 9800 0 timeout (verification) 900    100 15000   0 error (7) 720   2500 10000 0 timeout 900   1400 10000 0 timeout 900   5600 6600 0 timeout 900   2700 9300 0 error (1) 870   350 10000 0
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (5) 1.6   27 22    0 error (42) 880     1300   6700    0 error (134) .17  20   1.9  0 assertion 44   2200 400 0 unknown 900    12000 5700   0 timeout 900   410 7100 0 timeout 900   410 8600 0 timeout 900     9100 5500    0 unknown .92 40 12   0 false(unreach-call) 66 2300 590 -16 timeout 900    490 11000   0 true .77 46 7.3 2 unknown 22   690 210 0 disqualified 880   370 7500 0 timeout (verification) 900    7500 5000   0 timeout 900   1800 14000 0 timeout 900   1500 13000 0 timeout 900   1000 11000 0 unknown 540   1300 6300 0 error (1) 7.3 540 85 0
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 900     5900 11000    0 out of memory 180     13000   2100    0 error (134) .073 9.1 .71 0 timeout 910   8200 7500 0 unknown 900    2100 10000   0 unknown 8.5 450 120 0 timeout 900   470 7600 0 timeout 900     3800 9900    0 unknown .88 40 13   0 timeout 900 5600 7400 0 timeout 900    300 9700   0 true .88 54 9.0 2 unknown 14   330 130 0 disqualified 880   480 11000 0 timeout (verification) 900    1300 12000   0 timeout 900   4000 11000 0 timeout 900   950 7700 0 timeout 900   2200 15000 0 unknown 560   3300 6600 0 error (1) 880   560 11000 0
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 900     5700 12000    0 error (42) 880     4300   14000    0 out of memory 130     15000   1700    0 timeout 920   6500 7600 0 unknown 900    1900 13000   0 timeout 900   440 8000 0 timeout 900   440 8400 0 timeout 900     3500 11000    0 unknown .89 41 10   0 timeout 910 4100 8900 0 out of memory 130    15000 1600   0 true .85 47 8.2 2 unknown 15   370 130 0 disqualified 880   300 8600 0 timeout (verification) 900    7900 10000   0 timeout 900   840 14000 0 timeout 900   990 11000 0 timeout 900   860 14000 0 unknown 730   4000 4500 0 error (1) 870   540 11000 0
heap-manipulation/tree_true-unreach-call.i error (5) 590     2500 4600    0 error (42) 880     1400   10000    0 error (134) .16  12   1.2  0 timeout 900   3900 6300 0 unknown 900    1600 9500   0 unknown 8.5 450 140 0 timeout 900   430 6800 0 timeout 900     4000 7800    0 unknown .85 40 9.7 0 timeout 900 4300 5800 0 timeout 900    1100 11000   0 timeout 900    830 5500   0 unknown 14   340 140 0 disqualified 880   450 9500 0 timeout (verification) 900    1400 9400   0 true 20   550 170 2 timeout 900   1500 11000 0 timeout 900   810 10000 0 timeout 900   1600 9600 0 timeout 900   170 11000 0
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i error (134) .70  32 7.8  0 false(unreach-call) .097 9.4 .89 1 out of memory 220     15000   3000    0 false(unreach-call) 9.7 490 73 0 false(unreach-call) .48 35 5.9 1 false(unreach-call) 8.5 450 110 1 false(unreach-call) 8.6 440 110 1 false(unreach-call) .17  26 2.5  1 unknown 6.8  350 96   0 false(unreach-call) 19 1300 140 0 timeout 900    420 11000   0 false(unreach-call) .19 36 1.7 1 unknown 13   340 110 0 disqualified 3.2 87 41 0 false(unreach-call) .24 18 2.9 1 false(unreach-call) 10   380 83 1 false(unreach-call) 9.6 360 79 1 false(unreach-call) 8.9 360 72 1 false(unreach-call) 24   280 200 1 false(unreach-call) 6.8 560 77 1
list-properties/list_false-unreach-call_false-valid-memcleanup.i error (134) 2.1   60 29    0 false(unreach-call) .17  9.5 1.0  1 error (134) .095 13   1.1  0 false(unreach-call) 11   510 89 0 false(unreach-call) .68 35 9.5 1 false(unreach-call) 8.4 450 100 0 false(unreach-call) 8.5 440 110 0 false(unreach-call) .33  30 3.7  1 false(no-overflow) 72    240 1000   0 false(unreach-call) 21 1300 150 0 timeout 900    410 9600   0 false(unreach-call) .76 50 4.4 1 unknown 12   310 100 0 disqualified 3.3 89 47 0 false(unreach-call) .29 18 3.5 0 false(unreach-call) 24   630 270 1 false(unreach-call) 25   610 240 1 false(unreach-call) 610   800 8100 1 false(unreach-call) 150   600 2100 1 false(unreach-call) 6.8 560 73 1
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i error (134) .45  28 5.5  0 false(unreach-call) .083 9.9 .96 1 error (134) .091 11   .94 0 false(unreach-call) 8.3 460 65 1 false(unreach-call) .49 35 5.5 1 unknown 8.3 450 100 0 false(unreach-call) 9.9 450 140 1 false(unreach-call) .20  26 1.9  1 false(unreach-call) 22    220 280   1 false(unreach-call) 13 1200 100 1 timeout 900    630 9200   0 false(unreach-call) .45 49 1.9 1 unknown 12   310 110 0 disqualified 3.2 87 38 0 false(unreach-call) .26 17 2.6 1 false(unreach-call) 9.9 390 75 1 false(unreach-call) 9.8 360 78 1 false(unreach-call) 9.7 380 74 1 false(unreach-call) 22   290 170 1 false(unreach-call) 6.9 560 61 1
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) .28  27 3.6  1 false(unreach-call) .20  9.9 1.5  1 false(unreach-call) .83  31   10    1 false(unreach-call) 9.9 500 85 1 false(unreach-call) 1.0  36 13   1 false(unreach-call) 8.3 450 100 1 false(unreach-call) 8.5 450 100 1 false(unreach-call) .27  27 2.8  1 false(unreach-call) .48 83 5.8 1 false(unreach-call) 19 1200 130 1 false(unreach-call) .74 65 6.3 1 false(unreach-call) .21 36 1.8 1 unknown 12   320 100 0 disqualified 3.3 86 40 0 false(unreach-call) .19 16 2.0 1 false(unreach-call) 89   590 1200 1 timeout 900   1200 11000 0 false(unreach-call) 260   830 3300 1 false(unreach-call) 18   280 150 1 false(unreach-call) 5.0 180 48 1
list-properties/simple_false-unreach-call_false-valid-memcleanup.i error (134) .42  29 4.0  0 false(unreach-call) .083 9.9 .82 1 error (42) 880     12000   11000    0 false(unreach-call) 8.2 440 63 0 false(unreach-call) .47 35 6.6 1 false(unreach-call) 8.3 440 110 1 false(unreach-call) 8.6 450 100 1 false(unreach-call) .18  26 2.3  1 false(unreach-call) 6.8  280 87   1 false(unreach-call) 14 1300 110 0 timeout 900    410 10000   0 false(unreach-call) .22 36 1.7 1 unknown 11   290 110 0 disqualified 3.1 83 43 0 false(unreach-call) .28 18 2.5 1 false(unreach-call) 10   380 77 1 false(unreach-call) 11   430 95 1 false(unreach-call) 11   420 95 1 false(unreach-call) 22   280 160 1 false(unreach-call) 7.0 570 62 1
list-properties/splice_false-unreach-call_false-valid-memcleanup.i error (134) 1.9   66 27    0 false(unreach-call) .099 9.7 .88 1 error (42) 870     4300   9100    0 false(unreach-call) 11   390 87 0 false(unreach-call) .50 35 6.5 1 false(unreach-call) 8.7 450 110 1 false(unreach-call) 8.6 450 97 1 false(unreach-call) .17  27 2.0  1 unknown 6.4  320 85   0 false(unreach-call) 21 1200 160 0 timeout 900    420 10000   0 false(unreach-call) .24 33 2.3 1 unknown 12   320 110 0 disqualified 3.3 89 39 0 false(unreach-call) .27 18 3.5 1 false(unreach-call) 9.8 370 72 1 false(unreach-call) 11   390 85 1 false(unreach-call) 10   390 85 1 false(unreach-call) 31   290 310 1 false(unreach-call) 6.8 560 79 1
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (134) .97  38 13    0 error (42) 880     4000   8900    0 out of memory 220     15000   3200    0 timeout 900   3300 8400 0 unknown 900    900 11000   0 timeout 900   400 9500 0 timeout 900   400 8100 0 timeout 900     5300 10000    0 timeout 900    1500 7500   0 timeout 900 3400 7000 0 timeout 900    420 9900   0 timeout 900    1900 8200   0 unknown 13   330 120 0 disqualified 880   260 10000 0 timeout (verification) 900    2100 8900   0 timeout 900   780 12000 0 timeout 900   910 8700 0 timeout 900   740 12000 0 timeout 900   5200 8000 0 error (1) 870   560 9600 0
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i error (134) .42  29 4.2  0 error (6) 830     13000   10000    0 error (134) .12  11   .82 0 timeout 900   2200 6800 0 unknown 900    470 11000   0 unknown 8.4 440 99 0 timeout 900   490 9200 0 timeout 900     3200 11000    0 timeout 900    1400 7700   0 timeout 900 2600 6600 0 timeout 900    620 9900   0 true .83 37 6.9 2 unknown 12   310 110 0 disqualified 880   310 9300 0 timeout (verification) 900    550 8800   0 timeout 900   1100 9900 0 timeout 900   880 8000 0 timeout 900   1000 10000 0 timeout 900   3300 8100 0 error (1) 870   560 10000 0
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i error (8) .25  28 2.3  0 true .17  7.7 2.1  2 true 93     1500   1200    2 true 19   680 180 2 true 1.4  37 17   2 true 8.4 390 120 2 true 8.4 390 100 2 true .21  27 2.9  2 unknown .82 40 9.4 0 true 28 1300 220 2 true .75 68 7.0 2 true .26 37 2.3 2 unknown 12   310 120 0 disqualified 2.7 82 30 0 true .15 15 1.7 2 true 130   790 1500 2 timeout 900   1500 10000 0 timeout 900   5700 11000 0 true 77   1100 650 2 timeout 900   170 9800 0
list-properties/list_true-unreach-call_false-valid-memtrack.i error (134) 2.0   63 30    0 error (42) 880     6400   13000    0 error (134) .11  13   1.1  0 timeout 910   3500 6700 0 unknown 900    740 10000   0 timeout 900   430 8400 0 timeout 900   430 7400 0 timeout 900     1800 13000    0 timeout 900    1500 7100   0 timeout 900 3500 7000 0 timeout 900    410 11000   0 true 1.0  37 8.0 2 unknown 11   290 100 0 disqualified 880   250 9400 0 timeout (verification) 900    3700 8700   0 timeout 900   2500 9800 0 timeout 900   850 7000 0 timeout 900   900 11000 0 timeout 900   13000 8800 0 error (1) 870   570 13000 0
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i true .37  29 4.6  2 error (42) 880     3900   9600    0 error (134) .082 7.7 .44 0 timeout 900   2200 6000 0 unknown 900    530 11000   0 timeout 900   400 8900 0 timeout 900   400 8000 0 timeout 900     2500 9400    0 timeout 900    1400 6700   0 timeout 900 3200 6100 0 timeout 900    410 10000   0 true .87 48 5.0 2 unknown 12   310 120 0 disqualified 880   300 11000 0 timeout (verification) 900    1800 9400   0 timeout 900   1200 11000 0 timeout 900   1700 8400 0 timeout 900   900 11000 0 unknown 830   5900 8100 0 error (1) 870   560 11000 0
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (134) .38  30 3.4  0 error (42) 880     3300   11000    0 error (42) 880     12000   9400    0 timeout 900   2000 6200 0 unknown 900    460 11000   0 timeout 900   400 9300 0 timeout 900   400 8800 0 timeout 900     3200 9100    0 timeout 900    1500 8600   0 timeout 900 2800 6800 0 timeout 900    420 11000   0 true .88 33 7.9 2 unknown 11   290 95 0 disqualified 880   290 11000 0 timeout (verification) 900    1700 9100   0 timeout 900   940 10000 0 timeout 900   980 8700 0 timeout 900   810 11000 0 timeout 900   6100 10000 0 error (1) 870   570 12000 0
list-properties/splice_true-unreach-call_false-valid-memtrack.i error (134) 1.7   60 22    0 error (42) 880     1700   14000    0 error (42) 870     4500   9600    0 timeout 920   3800 6600 0 unknown 900    990 11000   0 timeout 900   440 8500 0 timeout 900   440 7500 0 timeout 900     3300 9900    0 timeout 900    1500 7900   0 timeout 910 4400 5200 0 timeout 900    420 9700   0 timeout 900    1300 11000   0 unknown 12   300 120 0 disqualified 880   380 11000 0 timeout (verification) 900    2800 9100   0 timeout 900   2300 11000 0 timeout 900   1100 8000 0 timeout 900   970 12000 0 timeout 900   5000 9000 0 error (1) 870   610 12000 0
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) .18  24 1.7  1 false(unreach-call) .076 9.8 .56 1 false(unreach-call) .078 9.3 .65 1 false(unreach-call) 3.1 260 26 1 false(unreach-call) .14 34 1.4 1 false(unreach-call) 8.2 430 110 1 false(unreach-call) 8.4 430 110 1 false(unreach-call) .089 26 .86 1 false(unreach-call) .46 83 4.4 1 false(unreach-call) 14 1100 100 1 false(unreach-call) .66 60 8.7 1 false(unreach-call) .19 34 1.6 1 false(unreach-call) 5.3 290 51 1 disqualified 2.6 73 31 0 false(unreach-call) .17 16 2.0 1 false(unreach-call) 8.3 360 75 1 false(unreach-call) 8.1 350 63 1 false(unreach-call) 8.3 370 60 1 false(unreach-call) 8.9 270 85 1 false(unreach-call) 3.5 150 35 1
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) .21  28 1.9  1 false(unreach-call) .090 9.2 .86 1 false(unreach-call) .089 9.4 .92 1 false(unreach-call) 4.3 290 40 1 false(unreach-call) .16 34 1.8 1 false(unreach-call) 8.4 450 100 1 false(unreach-call) 8.5 440 110 1 false(unreach-call) .091 27 1.2  1 false(unreach-call) .45 83 4.7 1 false(unreach-call) 16 1200 110 1 false(unreach-call) .71 67 6.9 1 false(unreach-call) .17 31 1.3 1 false(unreach-call) 5.5 290 56 1 disqualified 2.6 73 34 0 false(unreach-call) .18 16 1.9 1 false(unreach-call) 10   380 79 1 false(unreach-call) 10   390 83 1 false(unreach-call) 10   380 81 1 false(unreach-call) 22   280 170 1 false(unreach-call) 5.0 180 45 1
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) .11  24 .78 1 false(unreach-call) .057 9.3 .48 1 false(unreach-call) .066 9.2 .36 1 false(unreach-call) 2.8 250 28 1 unknown 6.4  37 94   0 false(unreach-call) 8.2 430 93 1 false(unreach-call) 8.3 430 97 1 unknown .076 26 .94 0 false(unreach-call) .43 83 6.3 1 false(unreach-call) 14 1100 110 1 false(unreach-call) .36 58 4.1 1 false(unreach-call) .16 34 2.4 1 false(unreach-call) 5.3 270 50 1 disqualified 2.6 72 30 0 false(unreach-call) .17 16 1.8 1 false(unreach-call) 7.9 370 68 1 false(unreach-call) 7.7 360 56 1 false(unreach-call) 7.4 340 56 1 false(unreach-call) 8.7 270 70 1 false(unreach-call) 3.5 150 36 1
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) .24  27 1.5  1 false(unreach-call) .13  9.6 .91 1 error (134) .074 8.0 .70 0 false(unreach-call) 3.9 290 39 1 false(unreach-call) .14 34 1.9 1 unknown 8.7 440 110 0 error - divine failed with signal 11 1.6 200 22 0 false(unreach-call) .091 26 .86 1 false(unreach-call) .47 83 5.0 1 false(unreach-call) 14 1200 120 1 false(unreach-call) .76 65 7.3 1 false(unreach-call) .18 35 1.6 1 unknown 7.8 240 80 0 disqualified 2.7 74 36 0 false(unreach-call) .20 18 2.4 1 unknown 15   370 130 0 unknown 15   350 120 0 unknown 14   340 120 0 false(unreach-call) 22   280 160 1 false(unreach-call) 4.9 170 43 1
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) .11  23 .95 1 false(unreach-call) .10  9.5 .35 1 false(unreach-call) .14  7.9 .25 1 false(unreach-call) 3.1 260 25 1 false(unreach-call) .14 33 1.5 1 false(unreach-call) 8.1 430 110 1 false(unreach-call) 8.1 430 98 1 false(unreach-call) .080 26 .77 1 false(unreach-call) .42 83 5.2 1 false(unreach-call) 12 1200 87 1 false(unreach-call) .38 58 3.3 1 false(unreach-call) .14 34 1.4 1 false(unreach-call) 5.3 280 50 1 disqualified 2.6 73 37 0 false(unreach-call) .17 15 2.0 1 false(unreach-call) 8.0 370 63 1 false(unreach-call) 8.2 360 61 1 false(unreach-call) 8.5 380 70 1 false(unreach-call) 8.6 270 73 1 false(unreach-call) 3.5 150 37 1
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) .12  24 .77 1 false(unreach-call) .059 9.8 .50 1 false(unreach-call) .064 9.2 .44 1 false(unreach-call) 3.0 260 27 1 false(unreach-call) .14 33 1.6 1 false(unreach-call) 8.1 430 110 1 false(unreach-call) 8.3 430 120 1 false(unreach-call) .090 26 .78 1 false(unreach-call) .43 83 5.2 1 false(unreach-call) 12 1200 84 1 false(unreach-call) .38 58 3.5 1 false(unreach-call) .15 35 2.5 1 false(unreach-call) 4.9 280 45 1 disqualified 2.6 74 32 0 false(unreach-call) .17 15 2.2 1 false(unreach-call) 7.9 360 59 1 false(unreach-call) 8.4 370 61 1 false(unreach-call) 8.4 370 60 1 false(unreach-call) 8.7 270 68 1 false(unreach-call) 3.5 150 39 1
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) .19  24 1.9  1 false(unreach-call) .086 9.5 .56 1 false(unreach-call) .082 9.4 .51 1 false(unreach-call) 3.1 270 30 1 false(unreach-call) .13 34 1.8 1 error - unexpected error: memory error in userspace 8.1 430 110 0 error - unexpected error: memory error in userspace 8.1 430 100 0 false(unreach-call) .081 26 .97 1 false(unreach-call) .43 83 4.7 1 false(unreach-call) 14 1100 100 1 error (8) .69 60 6.8 0 false(unreach-call) .19 35 1.5 1 false(unreach-call) 4.8 280 48 1 disqualified 2.7 75 34 0 false(unreach-call) .17 16 2.0 1 false(unreach-call) 8.3 350 70 1 false(unreach-call) 7.7 350 63 1 false(unreach-call) 8.0 370 63 1 false(unreach-call) 9.0 270 75 1 false(unreach-call) 3.6 150 32 1
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) .27  26 2.4  1 false(unreach-call) .078 9.8 .65 1 false(unreach-call) .083 8.9 .66 1 false(unreach-call) 3.2 260 34 1 false(unreach-call) .17 33 2.7 1 unknown 8.1 430 99 0 false(unreach-call) 8.4 430 100 1 false(unreach-call) .11  26 1.4  1 false(unreach-call) .45 83 5.4 1 false(unreach-call) 16 1200 100 1 false(unreach-call) .70 61 5.8 1 false(unreach-call) .24 36 2.1 1 unknown 12   320 110 0 disqualified 2.8 79 34 0 false(unreach-call) .22 17 2.7 1 false(unreach-call) 9.9 390 70 1 false(unreach-call) 8.6 350 78 1 false(unreach-call) 11   440 93 1 false(unreach-call) 9.8 280 81 1 timeout 900   160 10000 0
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i error (134) .094 26 .87 0 false(unreach-call) .079 8.5 .63 1 error (42) 6.7   45   93    0 false(unreach-call) 4.0 300 34 1 false(unreach-call) .18 35 2.6 1 false(unreach-call) 8.3 430 110 1 false(unreach-call) 8.6 430 97 1 false(unreach-call) .12  27 1.3  1 unknown .76 39 8.7 0 false(unreach-call) 15 1200 110 1 false(unreach-call) .44 62 3.8 1 false(unreach-call) .38 51 1.3 1 unknown 12   300 120 0 disqualified 2.8 80 30 0 false(unreach-call) .25 18 3.3 1 false(unreach-call) 21   750 220 1 timeout 900   840 9900 0 false(unreach-call) 48   930 420 1 false(unreach-call) 21   290 170 1 false(unreach-call) 5.3 170 57 1
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) .97  30 13    1 false(unreach-call) .15  9.4 1.1  1 out of memory 200     15000   2900    0 false(unreach-call) 4.6 290 38 1 false(unreach-call) .89 37 10   1 false(unreach-call) 8.4 430 110 1 false(unreach-call) 8.4 430 100 1 false(unreach-call) .20  26 1.9  1 unknown .83 40 10   0 false(unreach-call) 15 1100 110 1 timeout 900    460 13000   0 false(unreach-call) .16 37 1.5 0 unknown 80   1500 930 0 disqualified 3.5 85 43 0 false(unreach-call) .89 29 11   1 false(unreach-call) 9.4 370 74 1 false(unreach-call) 11   450 91 1 false(unreach-call) 14   570 110 1 false(unreach-call) 16   280 130 1 false(unreach-call) 100   190 1200 1
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) .16  24 1.5  1 false(unreach-call) .086 9.5 .58 1 false(unreach-call) .16  8.3 .35 1 false(unreach-call) 3.6 260 34 1 false(unreach-call) .52 35 6.2 1 false(unreach-call) 8.2 430 95 1 false(unreach-call) 8.2 430 100 1 false(unreach-call) .086 26 .81 1 false(unreach-call) .42 83 5.2 1 false(unreach-call) 14 1100 91 1 false(unreach-call) .38 58 3.0 1 false(unreach-call) .14 33 1.4 1 false(unreach-call) 5.0 260 47 1 disqualified 3.0 79 38 0 false(unreach-call) .17 15 1.6 1 false(unreach-call) 8.2 350 60 1 false(unreach-call) 9.3 370 67 1 false(unreach-call) 9.3 380 75 1 false(unreach-call) 14   270 110 1 false(unreach-call) 3.5 150 36 1
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) .16  24 1.4  1 false(unreach-call) .074 10   .51 1 false(unreach-call) .069 9.4 .59 1 false(unreach-call) 3.6 270 33 1 false(unreach-call) .52 35 6.2 1 false(unreach-call) 8.4 430 120 1 false(unreach-call) 8.2 430 110 1 false(unreach-call) .080 26 .84 1 false(unreach-call) .44 83 6.2 1 false(unreach-call) 13 1100 90 1 false(unreach-call) .37 58 2.9 1 false(unreach-call) .14 36 1.6 1 false(unreach-call) 5.0 260 41 1 disqualified 3.0 78 38 0 false(unreach-call) .17 16 1.7 1 false(unreach-call) 8.3 380 61 1 false(unreach-call) 7.9 350 61 1 false(unreach-call) 8.6 380 61 1 false(unreach-call) 13   280 89 1 false(unreach-call) 3.3 150 34 1
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true .091 24 .88 2 true .053 6.9 .34 2 true .036 6.3 .34 2 true 2.9 260 30 2 unknown .79 66 8.6 0 true 8.0 370 98 2 true 8.3 370 120 2 true .078 26 .80 2 timeout 900    2200 11000   0 true 12 1100 83 2 true .37 58 2.9 2 true .29 47 1.4 2 true 4.0 220 36 2 disqualified 2.0 71 28 0 true .14 16 1.8 2 true 8.4 370 59 2 true 8.1 370 62 2 true 8.1 360 58 2 true 14   460 110 2 timeout 900   150 11000 0
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true .089 24 .83 2 true .049 7.5 .29 2 true .058 5.1 .29 2 true 2.8 250 26 2 unknown .80 66 9.1 0 true 8.2 370 120 2 true 8.2 370 110 2 true .10  26 .90 2 timeout 900    84 11000   0 true 13 1100 90 2 true .39 58 3.0 2 true .13 33 1.3 2 true 4.0 220 38 2 disqualified 1.9 66 25 0 true .15 16 1.6 2 true 8.4 370 59 2 true 7.5 370 59 2 true 8.4 370 65 2 true 13   470 120 2 timeout 900   150 13000 0
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true .093 23 .81 2 true .043 6.6 .38 2 true .042 6.2 .24 2 true 3.0 250 27 2 unknown .80 67 8.5 0 true 8.2 370 110 2 true 8.0 370 120 2 true .082 26 .90 2 timeout 900    84 9500   0 true 13 1100 97 2 true .35 58 3.1 2 true .13 31 1.3 2 true 3.9 220 37 2 disqualified 2.0 73 27 0 true .14 15 1.5 2 true 7.6 340 58 2 true 7.7 360 65 2 true 8.7 360 74 2 true 14   450 110 2 timeout 900   150 12000 0
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true .093 24 .80 2 true .065 6.0 .35 2 true .040 6.2 .24 2 true 2.9 250 26 2 unknown .78 65 9.3 0 true 7.9 370 100 2 true 8.1 370 120 2 true .10  26 .79 2 timeout 900    85 10000   0 true 13 1000 97 2 true .37 58 3.2 2 true .18 33 1.0 2 true 3.8 220 36 2 disqualified 2.0 65 28 0 true .14 16 1.5 2 true 7.7 360 56 2 true 8.0 370 61 2 true 7.3 340 62 2 true 13   450 120 2 timeout 900   150 11000 0
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i false(unreach-call) .43  24 4.7  -16 true .11  6.2 .50 2 true .084 7.2 .69 2 true 2.9 250 31 2 unknown 1.1  67 12   0 error - divine failed with exitcode 1 1.2 170 16 0 error - divine failed with exitcode 1 1.2 170 15 0 true .11  26 .89 2 unknown .82 40 9.3 0 true 14 1200 98 2 true .37 58 3.9 2 true .38 48 1.3 2 unknown 12   310 110 0 disqualified 2.6 81 33 0 error(unknown, verification-finished) .15 15 1.4 0 true 92   690 990 2 timeout 900   1200 10000 0 timeout 900   760 13000 0 true 43   930 380 2 timeout 900   150 12000 0
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true .084 24 1.0  2 true .052 7.1 .29 2 true .056 5.7 .15 2 true 2.7 260 25 2 unknown .79 66 7.7 0 true 8.0 370 94 2 true 8.1 370 120 2 true .076 26 .73 2 timeout 900    85 11000   0 true 12 1000 78 2 true .36 58 2.9 2 true .14 33 1.2 2 true 3.7 210 34 2 disqualified 2.0 67 24 0 true .13 17 1.6 2 true 8.2 370 68 2 true 7.5 360 63 2 true 8.0 360 56 2 true 12   440 110 2 timeout 900   150 10000 0
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true .095 24 .83 2 true .078 6.2 .26 2 true .044 6.1 .23 2 true 3.0 250 25 2 unknown .81 66 9.9 0 true 8.0 370 110 2 true 8.1 370 100 2 true .10  26 .79 2 timeout 900    84 9300   0 true 12 1200 94 2 true .38 58 3.6 2 true .36 47 1.2 2 true 4.2 230 40 2 disqualified 2.0 72 24 0 true .14 15 1.4 2 true 8.5 370 69 2 true 8.4 330 62 2 true 8.0 350 68 2 true 14   470 110 2 timeout 900   150 10000 0
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true .12  24 .73 2 true .049 6.4 .37 2 true .052 6.6 .72 2 true 2.9 250 29 2 unknown .83 67 8.5 0 true 8.1 370 120 2 true 8.2 370 100 2 true .088 26 .82 2 timeout 900    84 11000   0 true 14 1100 96 2 true .36 58 3.6 2 true .15 33 1.4 2 true 4.2 230 36 2 disqualified 2.0 73 25 0 true .14 15 1.9 2 true 8.7 350 72 2 true 8.4 360 69 2 true 8.9 370 72 2 true 14   460 120 2 timeout 900   150 12000 0
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true .11  24 .89 2 true .047 6.5 .36 2 true .039 5.9 .27 2 true 2.9 260 29 2 unknown .80 66 7.8 0 true 8.1 370 91 2 true 8.2 370 100 2 true .081 26 .82 2 timeout 900    85 9300   0 true 13 1000 92 2 true .34 58 3.7 2 true .14 33 1.1 2 true 3.9 210 38 2 disqualified 2.0 71 22 0 true .16 15 1.7 2 true 7.2 350 56 2 true 7.8 370 71 2 true 7.8 370 62 2 true 12   440 110 2 timeout 900   150 11000 0
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true .093 24 .91 2 true .044 6.6 .31 2 true .044 5.7 .23 2 true 2.9 260 26 2 unknown .78 66 9.2 0 true 8.0 370 120 2 true 8.0 370 96 2 true .075 26 .94 2 timeout 900    84 9100   0 true 13 1000 89 2 true .35 58 3.3 2 true .14 33 1.4 2 true 3.9 220 39 2 disqualified 2.0 71 23 0 true .14 16 1.6 2 true 7.9 370 70 2 true 8.1 360 65 2 true 7.7 360 57 2 true 14   480 130 2 timeout 900   150 11000 0
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true .089 24 .93 2 true .076 6.7 .25 2 true .036 6.1 .28 2 true 2.9 260 26 2 unknown .80 67 9.7 0 true 8.0 370 89 2 true 8.1 370 97 2 true .080 26 .80 2 timeout 900    84 10000   0 true 13 1100 87 2 true .35 58 3.6 2 true .15 35 1.5 2 true 3.9 210 39 2 disqualified 2.0 71 26 0 true .14 16 1.6 2 true 8.4 380 63 2 true 8.2 360 61 2 true 8.3 370 65 2 true 16   580 130 2 timeout 900   150 11000 0
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true .090 23 1.1  2 true .043 7.7 .37 2 true .039 6.3 .28 2 true 3.0 250 26 2 unknown .80 66 8.5 0 true 8.3 370 99 2 true 8.1 370 110 2 true .084 26 .72 2 timeout 900    85 11000   0 true 11 1200 84 2 true .36 58 2.9 2 true .14 32 1.3 2 true 4.0 220 39 2 disqualified 2.0 74 27 0 true .14 16 1.8 2 true 7.6 360 61 2 true 8.9 370 64 2 true 7.0 340 53 2 true 16   500 140 2 timeout 900   150 11000 0
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true .097 23 .78 2 true .049 6.3 .67 2 true .042 6.3 .25 2 true 2.9 260 26 2 unknown .80 67 9.7 0 true 8.0 370 97 2 true 8.1 370 100 2 true .082 26 .69 2 timeout 900    85 12000   0 true 13 1100 86 2 true .35 58 3.2 2 true .16 32 1.2 2 true 3.8 210 41 2 disqualified 2.0 72 29 0 true .14 16 1.5 2 true 8.4 370 71 2 true 7.6 350 55 2 true 8.1 370 75 2 true 15   470 120 2 timeout 900   150 14000 0
ldv-regression/nested_structure_true-unreach-call_true-termination.i true .091 24 1.0  2 true .048 7.0 .32 2 true .044 6.7 .24 2 true 3.0 260 28 2 unknown .79 67 8.0 0 true 8.1 370 90 2 true 8.1 370 99 2 true .082 26 .99 2 timeout 900    85 9000   0 true 13 1100 91 2 true .36 58 3.7 2 true .23 47 1.4 2 true 3.9 210 40 2 disqualified 2.0 74 25 0 true .15 16 1.4 2 true 8.1 350 61 2 true 8.2 380 70 2 true 8.3 370 59 2 true 14   450 110 2 timeout 900   150 11000 0
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true .095 23 .88 2 true .040 7.3 .16 2 true .045 5.8 .24 2 true 2.8 260 28 2 unknown .78 65 9.0 0 true 8.3 370 110 2 true 8.1 370 100 2 true .075 26 .98 2 timeout 900    84 10000   0 true 11 1200 81 2 true .34 58 3.9 2 true .16 35 1.2 2 true 3.6 220 39 2 disqualified 2.0 72 25 0 true .14 16 1.5 2 true 7.7 340 58 2 true 8.2 360 61 2 true 8.2 340 62 2 true 13   450 120 2 timeout 900   190 13000 0
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true .12  24 .73 2 true .043 6.6 .40 2 true .086 5.5 .21 2 true 2.9 250 25 2 unknown .79 66 8.7 0 true 8.1 370 94 2 true 8.2 370 92 2 true .084 26 .83 2 timeout 900    84 12000   0 true 11 1200 81 2 true .34 58 3.0 2 true .23 47 1.5 2 true 3.7 220 36 2 disqualified 2.0 73 26 0 true .14 15 2.0 2 true 7.0 340 56 2 true 7.1 350 56 2 true 8.2 360 57 2 true 13   460 110 2 timeout 900   150 11000 0
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true .25  26 3.0  2 true .074 7.5 .61 2 true .096 8.7 .42 2 true 3.4 280 29 2 unknown .83 67 9.7 0 unknown 8.1 430 96 0 true 8.3 370 97 2 true .093 26 1.2  2 timeout 900    4200 9800   0 true 13 1100 95 2 true .69 60 7.3 2 true .38 36 2.6 2 unknown 12   320 120 0 disqualified 2.1 71 27 0 true .20 17 2.6 2 true 10   390 74 2 timeout 900   1200 11000 0 true 9.7 370 75 2 true 16   450 150 2 timeout 900   150 10000 0
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i error (134) .10  26 .83 0 true .056 6.4 .50 2 true .20  15   2.4  2 true 4.0 290 35 2 unknown .95 66 13   0 true 8.2 370 98 2 true 8.3 370 100 2 true .13  27 1.2  2 unknown .76 39 9.9 0 true 14 1200 97 2 true .42 62 3.8 2 true .37 49 1.3 2 unknown 12   310 100 0 disqualified 2.1 76 26 0 true .21 17 2.9 2 true 21   730 200 2 timeout 900   850 9500 0 true 42   950 450 2 true 36   840 340 2 timeout 900   160 11000 0
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true .18  26 1.5  2 true .11  7.0 .62 2 true .11  7.3 .90 2 true 3.8 290 37 2 unknown .83 67 8.6 0 true 8.1 370 100 2 true 8.3 370 100 2 true .12  26 .78 2 unknown .76 39 11   0 true 14 1200 110 2 true .68 64 7.9 2 true .21 36 1.6 2 true 3.8 210 33 2 disqualified 2.1 71 24 0 true .14 15 1.6 2 true 11   440 89 2 true 11   460 83 2 true 10   440 88 2 true 24   520 220 2 timeout 900   170 13000 0
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true .11  26 .80 2 true .053 6.9 .57 2 true .052 7.0 .28 2 true 3.6 280 34 2 unknown .81 66 9.0 0 false(unreach-call) 8.1 430 88 -16 error - divine failed with signal 11 1.7 200 21 0 true .088 26 .96 2 false(unreach-call) .42 83 5.1 -16 true 12 1200 93 2 true .39 61 3.2 2 true .28 48 1.4 2 true 4.1 220 37 2 disqualified 2.0 73 25 0 true .17 15 1.6 2 true 9.1 380 68 2 true 8.8 370 64 2 true 9.2 370 73 2 true 24   440 180 2 timeout 900   160 11000 0
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true .089 23 .87 2 true .044 6.4 .39 2 true .041 5.8 .23 2 true 2.8 260 29 2 unknown .80 67 9.4 0 true 8.3 370 98 2 true 8.3 370 110 2 true .080 26 .89 2 timeout 900    85 8600   0 true 13 1100 89 2 true .34 58 3.4 2 true .22 46 1.4 2 true 3.9 210 39 2 disqualified 2.0 71 26 0 true .13 16 1.6 2 true 8.3 370 67 2 true 8.0 370 58 2 true 8.2 370 61 2 true 12   440 100 2 timeout 900   150 12000 0
ldv-regression/test_address_true-termination.c_true-unreach-call.i true .10  26 .78 2 true .069 6.4 .31 2 true .063 6.2 .29 2 true 3.6 280 37 2 unknown .82 66 9.0 0 true 8.3 370 100 2 true 8.2 370 98 2 true .087 26 .94 2 timeout 900    85 9800   0 true 13 1200 94 2 true .40 62 3.4 2 true .15 34 1.1 2 true 3.9 220 38 2 disqualified 2.0 72 25 0 true .15 16 1.8 2 true 9.3 380 75 2 true 8.2 360 61 2 true 9.5 370 68 2 true 17   450 150 2 timeout 900   210 11000 0
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true .094 23 .75 2 true .051 7.2 .32 2 true .052 6.1 .25 2 true 2.8 250 29 2 unknown .77 66 8.5 0 true 8.1 370 100 2 true 8.0 370 110 2 true .077 26 .78 2 timeout 900    84 9300   0 true 12 1000 79 2 true .34 58 3.8 2 true .14 32 1.2 2 true 3.4 210 36 2 disqualified 1.9 66 25 0 true .14 15 1.6 2 true 7.8 360 68 2 true 7.2 340 66 2 true 8.2 360 71 2 true 13   460 130 2 timeout 900   150 9800 0
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true .18  26 1.6  2 true .12  6.7 .42 2 true .062 7.7 .52 2 true 3.7 290 34 2 unknown .81 66 9.1 0 true 8.0 370 100 2 true 8.3 370 100 2 true .093 26 1.1  2 unknown .50 32 5.7 0 true 14 1100 110 2 true .71 64 6.2 2 true .29 48 1.7 2 true 3.9 220 36 2 disqualified 2.1 73 24 0 true .15 16 1.6 2 true 9.2 380 75 2 true 8.7 370 73 2 true 9.0 360 76 2 true 23   450 180 2 timeout 900   170 12000 0
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true .13  26 .85 2 true .075 6.5 .34 2 true .047 7.4 .32 2 true 3.8 280 31 2 unknown .83 66 9.9 0 true 8.0 370 85 2 true 8.3 370 120 2 true .082 26 1.0  2 unknown .47 32 5.8 0 true 14 1200 94 2 true .41 62 3.1 2 true .14 33 1.5 2 true 3.9 210 40 2 disqualified 2.0 72 26 0 true .14 16 1.5 2 true 9.0 380 70 2 true 8.7 360 69 2 true 9.0 370 70 2 true 23   450 200 2 timeout 900   170 13000 0
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true .11  28 1.0  2 true .058 7.6 .56 2 true .052 8.9 .41 2 true 4.0 280 36 2 true .38 36 4.8 2 true 8.3 390 93 2 true 8.3 390 100 2 true .085 27 .96 2 timeout 900    760 9600   0 true 14 1100 99 2 true .41 64 3.9 2 unknown .16 36 1.4 0 true 5.7 290 57 2 disqualified 2.0 71 30 0 true .15 15 1.6 2 true 9.4 370 77 2 true 8.6 350 68 2 true 9.3 370 64 2 true 19   450 150 2 timeout 900   170 11000 0
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true .14  23 1.3  2 true .046 6.3 .28 2 true .082 5.6 .24 2 true 2.9 260 26 2 unknown .82 66 8.4 0 true 8.0 370 110 2 true 8.2 370 100 2 true .080 26 .83 2 timeout 900    85 10000   0 true 13 1000 92 2 true .36 58 3.3 2 true .17 30 1.2 2 true 4.0 210 37 2 disqualified 2.0 72 21 0 true .14 15 1.8 2 true 8.0 370 61 2 true 7.3 340 58 2 true 7.0 350 63 2 true 12   470 110 2 timeout 900   150 14000 0
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true .089 23 1.1  2 true .050 6.5 .27 2 true .083 6.3 .31 2 true 2.9 260 28 2 unknown .77 66 10   0 true 8.3 370 110 2 true 8.1 370 98 2 true .085 26 1.0  2 timeout 900    85 9900   0 true 14 1100 100 2 true .36 58 2.9 2 true .29 47 1.2 2 true 3.9 210 41 2 disqualified 2.0 72 24 0 true .14 15 1.6 2 true 8.1 370 67 2 true 8.4 370 62 2 true 8.1 360 66 2 true 13   470 120 2 timeout 900   150 11000 0
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true .093 24 .85 2 true .044 7.1 .34 2 true .042 7.1 .39 2 true 3.0 250 29 2 unknown .80 68 8.9 0 true 8.2 370 100 2 true 8.3 370 120 2 true .079 26 1.4  2 timeout 900    85 11000   0 true 11 1200 95 2 true .36 58 3.5 2 true .13 34 1.2 2 true 3.9 210 34 2 disqualified 2.0 71 27 0 true .14 15 1.4 2 true 6.9 330 58 2 true 7.8 360 61 2 true 8.2 370 59 2 true 13   450 100 2 timeout 900   150 11000 0
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true .092 24 .66 2 true .048 6.7 .34 2 true .040 6.0 .25 2 true 2.9 250 25 2 unknown .82 67 9.0 0 true 8.1 370 110 2 true 8.1 370 98 2 true .11  26 .82 2 timeout 900    85 11000   0 true 12 1000 86 2 true .34 58 3.4 2 true .22 46 1.4 2 true 3.5 210 36 2 disqualified 2.0 67 24 0 true .16 15 1.3 2 true 7.9 370 69 2 true 8.2 360 63 2 true 8.0 370 63 2 true 13   470 110 2 timeout 900   150 13000 0
ldv-regression/test_union_true-termination.c_true-unreach-call.i true .098 24 .82 2 true .052 6.6 .30 2 true .039 6.8 .21 2 true 2.8 250 26 2 unknown .82 66 8.7 0 true 8.2 370 100 2 true 8.0 370 120 2 true .10  26 .79 2 timeout 900    85 10000   0 true 11 1200 75 2 true .35 58 3.1 2 true .13 32 1.2 2 true 3.9 210 42 2 disqualified 2.0 67 30 0 true .13 16 1.6 2 true 8.3 360 59 2 true 7.8 350 66 2 true 7.6 340 61 2 true 13   470 100 2 timeout 900   150 11000 0
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true .11  24 .93 2 true .048 7.8 .29 2 true .087 5.9 .18 2 true 2.8 250 27 2 unknown .80 68 9.2 0 true 8.0 370 100 2 true 8.0 370 110 2 true .083 26 1.2  2 timeout 900    85 9500   0 true 13 1000 84 2 true .35 58 3.3 2 true .14 32 2.2 2 true 3.8 220 36 2 disqualified 2.0 67 21 0 true .14 15 1.5 2 true 8.0 360 65 2 true 7.4 370 67 2 true 7.8 380 66 2 true 13   470 110 2 timeout 900   150 13000 0
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true .089 23 .80 2 true .047 6.8 .33 2 true .034 6.2 .52 2 true 3.0 250 32 2 unknown .82 67 8.3 0 true 8.2 370 99 2 true 8.2 370 110 2 true .079 26 .85 2 timeout 900    85 9600   0 true 14 1100 92 2 true .37 58 3.7 2 true .16 34 1.2 2 true 5.5 290 47 2 disqualified 2.0 67 22 0 true .14 15 1.8 2 true 7.4 350 57 2 true 7.0 340 56 2 true 8.2 370 66 2 true 13   470 99 2 timeout 900   150 11000 0
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true .097 24 .97 2 true .050 6.9 .27 2 true .087 5.7 .19 2 true 2.9 260 28 2 unknown .86 66 15   0 true 8.1 370 94 2 true 8.0 370 94 2 true .076 26 1.0  2 timeout 900    84 11000   0 true 13 1100 96 2 true .37 58 2.9 2 true .14 32 2.7 2 true 3.3 210 33 2 disqualified 2.0 67 23 0 true .14 16 1.5 2 true 7.9 360 59 2 true 7.7 360 58 2 true 8.5 370 61 2 true 13   460 120 2 timeout 900   150 11000 0
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) .11  24 .87 1 false(unreach-call) .061 9.2 .55 1 false(unreach-call) .086 8.6 .43 1 false(unreach-call) 2.9 260 28 1 false(unreach-call) .18 33 1.6 1 false(unreach-call) 8.2 430 110 1 false(unreach-call) 8.3 430 98 1 false(unreach-call) .083 26 .92 1 false(unreach-call) .42 83 5.8 1 false(unreach-call) 14 1100 89 1 false(unreach-call) .35 59 3.3 1 false(unreach-call) .16 32 1.2 1 false(unreach-call) 5.1 260 54 1 disqualified 2.6 72 31 0 false(unreach-call) .16 15 1.8 1 false(unreach-call) 7.0 350 53 1 false(unreach-call) 7.6 350 59 1 false(unreach-call) 7.9 370 60 1 false(unreach-call) 8.8 270 77 1 false(unreach-call) 3.3 150 33 1
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) .12  24 1.1  1 false(unreach-call) .069 9.9 .53 1 false(unreach-call) .061 9.4 .88 1 false(unreach-call) 3.1 260 33 1 false(unreach-call) .13 33 1.5 1 false(unreach-call) 8.2 430 110 1 false(unreach-call) 8.2 430 120 1 false(unreach-call) .082 26 .84 1 false(unreach-call) .43 83 5.1 1 false(unreach-call) 14 1100 99 1 false(unreach-call) .38 59 3.3 1 false(unreach-call) .15 35 1.4 1 false(unreach-call) 5.4 280 47 1 disqualified 2.7 76 32 0 false(unreach-call) .19 15 2.1 1 false(unreach-call) 8.8 360 62 1 false(unreach-call) 8.8 330 68 1 false(unreach-call) 8.4 350 67 1 false(unreach-call) 8.4 270 72 1 false(unreach-call) 3.5 150 36 1
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) .12  24 .93 1 false(unreach-call) .14  8.6 .43 1 false(unreach-call) .065 8.5 .51 1 false(unreach-call) 3.0 260 28 1 false(unreach-call) .14 33 1.6 1 false(unreach-call) 8.2 430 110 1 false(unreach-call) 8.2 430 100 1 false(unreach-call) .087 26 1.2  1 false(unreach-call) .44 83 5.6 1 false(unreach-call) 13 1100 96 1 false(unreach-call) .37 59 3.2 1 false(unreach-call) .18 36 1.3 1 unknown 9.4 280 81 0 disqualified 2.6 74 37 0 false(unreach-call) .16 17 1.8 1 false(unreach-call) 7.9 370 59 1 false(unreach-call) 8.1 370 56 1 false(unreach-call) 7.6 340 58 1 false(unreach-call) 8.9 270 69 1 false(unreach-call) 3.3 150 34 1
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) .12  24 .92 1 false(unreach-call) .072 9.6 .41 1 false(unreach-call) .052 9.2 .48 1 false(unreach-call) 2.9 260 27 1 false(unreach-call) .18 33 1.6 1 false(unreach-call) 8.1 430 91 1 false(unreach-call) 8.2 430 99 1 false(unreach-call) .097 26 1.1  1 false(unreach-call) .42 83 5.6 1 false(unreach-call) 13 1100 88 1 false(unreach-call) .38 58 4.2 1 false(unreach-call) .34 48 1.2 1 false(unreach-call) 5.1 270 44 1 disqualified 2.6 71 33 0 false(unreach-call) .16 17 2.1 1 false(unreach-call) 7.3 340 54 1 false(unreach-call) 7.8 360 62 1 false(unreach-call) 8.0 370 66 1 false(unreach-call) 8.8 270 84 1 false(unreach-call) 3.5 150 35 1
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) .12  24 .89 1 false(unreach-call) .12  10   .37 1 false(unreach-call) .065 9.5 .60 1 false(unreach-call) 3.0 270 32 1 false(unreach-call) .16 34 1.9 0 unknown 8.2 430 100 0 error - divine failed with signal 6 (sorts (_ bitvec 32) and (_ bitvec 1) are incompatible) 8.6 370 110 0 false(unreach-call) .096 26 1.1  0 timeout 900    1700 7700   0 false(unreach-call) 14 1100 92 1 false(unreach-call) .37 59 3.7 1 false(unreach-call) .17 36 1.2 1 unknown 10   280 100 0 disqualified 2.7 79 33 0 false(unreach-call) .36 18 5.0 1 false(unreach-call) 7.4 340 52 1 false(unreach-call) 7.3 340 59 1 false(unreach-call) 8.2 370 72 1 false(unreach-call) 9.4 280 82 1 false(unreach-call) 3.6 150 37 1
ldv-regression/test22_false-unreach-call.c false(unreach-call) .13  24 .91 1 false(unreach-call) .077 9.8 .59 1 false(unreach-call) .080 9.5 .51 1 false(unreach-call) 5.1 310 45 1 false(unreach-call) .16 34 1.8 0 unknown 8.1 430 93 0 false(unreach-call) 15   430 190 1 false(unreach-call) .12  26 1.4  0 timeout 900    1400 8300   0 false(unreach-call) 14 1100 100 1 timeout 900    410 3600   0 false(unreach-call) .23 38 2.0 1 unknown 11   300 99 0 disqualified 3.2 84 38 0 false(unreach-call) .45 18 5.2 1 false(unreach-call) 11   470 83 1 false(unreach-call) 9.1 370 70 1 false(unreach-call) 12   560 100 1 false(unreach-call) 13   280 100 1 false(unreach-call) 4.2 160 42 1
ldv-regression/test23_false-unreach-call.c error (134) .091 24 .75 0 false(unreach-call) .41  12   5.2  1 false(unreach-call) 1.3   14   17    0 false(unreach-call) 8.3 470 75 1 false(unreach-call) 9.0  44 100   0 unknown 8.3 430 120 0 false(unreach-call) 15   440 170 1 false(unreach-call) 2.3   32 30    0 false(unreach-call) .44 83 5.3 1 false(unreach-call) 16 1200 120 1 false(unreach-call) .57 89 5.8 1 false(unreach-call) .50 36 5.1 1 unknown 11   290 110 0 disqualified 3.6 88 45 0 false(unreach-call) .70 25 8.6 1 false(unreach-call) 23   600 210 1 false(unreach-call) 19   650 180 1 false(unreach-call) 35   690 280 1 false(unreach-call) 24   300 270 1 false(unreach-call) 3.7 150 39 1
ldv-regression/test24_false-unreach-call.c error (134) .087 24 .65 0 false(unreach-call) .37  16   4.7  1 false(unreach-call) .97  15   12    0 false(unreach-call) 4.7 290 41 1 false(unreach-call) .69 42 9.7 1 unknown 8.2 430 110 0 false(unreach-call) 9.2 430 110 1 witness invalid (false(unreach-call)) .53  37 7.9  0 unknown .78 40 9.3 0 false(unreach-call) 14 1100 110 1 timeout 900    390 3400   0 false(unreach-call) .29 36 2.9 1 false(unreach-call) 16   420 150 1 disqualified 3.8 92 46 0 false(unreach-call) .24 22 3.0 1 false(unreach-call) 25   670 240 1 false(unreach-call) 23   530 210 1 false(unreach-call) 28   740 250 1 false(unreach-call) 22   330 190 1 false(unreach-call) 4.1 150 41 1
ldv-regression/test25_false-unreach-call_true-termination.c error (134) .091 24 .69 0 false(unreach-call) .17  10   1.9  1 false(unreach-call) .66  12   8.1  1 false(unreach-call) 13   600 120 1 false(unreach-call) 4.4  51 69   1 unknown 8.4 430 130 0 false(unreach-call) 12   430 140 1 witness invalid (false(unreach-call)) .37  32 4.3  0 timeout 900    770 13000   0 false(unreach-call) 19 1300 150 1 timeout 900    440 3200   0 false(unreach-call) .32 49 2.1 1 false(unreach-call) 14   360 120 1 disqualified 4.3 120 51 0 false(unreach-call) .28 20 3.0 1 false(unreach-call) 24   550 230 1 error (7) 260   1300 2800 0 false(unreach-call) 45   630 460 1 false(unreach-call) 27   310 240 1 false(unreach-call) 4.1 150 46 1
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) .12  24 1.0  1 false(unreach-call) .063 9.5 .59 1 false(unreach-call) .056 9.4 .56 1 false(unreach-call) 3.1 260 32 1 false(unreach-call) .14 34 1.5 1 false(unreach-call) 8.1 430 100 1 false(unreach-call) 8.2 430 99 1 false(unreach-call) .082 26 1.0  1 false(unreach-call) .41 83 5.7 1 false(unreach-call) 12 1200 89 1 false(unreach-call) .39 59 3.3 1 false(unreach-call) .16 32 1.5 1 unknown 9.5 270 87 0 disqualified 2.6 72 30 0 false(unreach-call) .17 16 2.0 1 false(unreach-call) 7.9 370 64 1 false(unreach-call) 7.3 360 65 1 false(unreach-call) 8.4 360 69 1 false(unreach-call) 7.9 270 70 1 false(unreach-call) 3.5 150 37 1
ldv-regression/test27_false-unreach-call_true-termination.c error (134) .12  25 .65 0 false(unreach-call) .23  11   2.4  1 false(unreach-call) .31  10   4.0  1 false(unreach-call) 4.4 280 41 1 false(unreach-call) 2.8  37 40   1 unknown 8.3 430 100 0 error - unexpected error: memory error in userspace 8.8 430 120 0 false(unreach-call) .19  26 2.5  1 timeout 900    160 12000   0 false(unreach-call) 13 1200 98 1 error (8) .37 59 3.2 0 unknown .21 34 3.7 0 unknown 13   310 120 0 disqualified 4.0 89 47 0 error(unknown, verification-finished) .95 19 12   0 false(unreach-call) 20   580 210 1 error (7) 43   650 430 0 false(unreach-call) 20   580 190 1 false(unreach-call) 22   300 180 1 timeout 900   150 11000 0
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) .12  24 .94 1 false(unreach-call) .059 9.5 .59 1 false(unreach-call) .11  7.5 .35 1 false(unreach-call) 3.0 260 31 1 false(unreach-call) .15 33 2.0 1 unknown 8.3 430 97 0 unknown 8.4 430 97 0 false(unreach-call) .094 26 1.2  1 true 16    83 210   -32 false(unreach-call) 13 1100 110 1 false(unreach-call) .36 58 3.1 1 false(unreach-call) .16 34 1.3 1 false(unreach-call) 5.4 270 52 1 disqualified 2.7 73 35 0 false(unreach-call) .25 22 2.0 1 false(unreach-call) 8.2 360 68 1 false(unreach-call) 8.4 360 52 1 false(unreach-call) 9.1 380 77 1 false(unreach-call) 8.7 280 75 1 timeout 900   150 11000 0
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) .11  24 1.0  0 false(unreach-call) .075 10   .48 1 false(unreach-call) .073 9.6 .41 1 false(unreach-call) 3.0 270 31 1 false(unreach-call) .16 34 1.9 1 unknown 8.1 430 95 0 false(unreach-call) 8.6 430 110 1 false(unreach-call) .11  26 1.1  1 false(unreach-call) .46 81 6.7 1 false(unreach-call) 13 1100 95 1 false(unreach-call) .37 59 3.7 1 false(unreach-call) .16 37 1.3 1 unknown 10   270 92 0 disqualified 2.7 74 32 0 false(unreach-call) .20 18 2.5 1 false(unreach-call) 8.8 370 62 1 false(unreach-call) 8.0 370 69 1 false(unreach-call) 8.8 360 66 1 false(unreach-call) 7.6 270 74 1 false(unreach-call) 3.7 150 46 1
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) .10  24 1.8  1 false(unreach-call) .058 10   .47 1 false(unreach-call) .069 9.2 .66 1 false(unreach-call) 3.0 260 29 1 false(unreach-call) .13 34 1.4 1 false(unreach-call) 8.2 430 100 1 false(unreach-call) 8.1 430 120 1 false(unreach-call) .088 26 1.3  1 false(unreach-call) .43 82 5.3 1 false(unreach-call) 12 1200 91 1 false(unreach-call) .36 59 3.1 1 false(unreach-call) .16 34 1.0 1 unknown 9.5 280 93 0 disqualified 2.6 73 31 0 false(unreach-call) .17 16 2.4 1 false(unreach-call) 6.9 330 57 1 false(unreach-call) 8.6 370 59 1 false(unreach-call) 8.3 370 61 1 false(unreach-call) 8.7 270 76 1 false(unreach-call) 3.6 150 38 1
ldv-regression/test01_true-unreach-call_true-termination.c true .14  24 .77 2 true .048 6.8 .36 2 true .044 6.6 .26 2 true 2.8 250 29 2 unknown .79 66 8.2 0 true 8.1 370 100 2 true 8.0 370 95 2 true .083 26 .86 2 timeout 900    85 9800   0 true 13 1100 88 2 true .35 59 4.2 2 true .33 46 1.2 2 true 3.8 200 37 2 disqualified 2.0 66 28 0 true .15 16 1.5 2 true 8.4 370 64 2 true 8.0 360 63 2 true 8.4 370 73 2 true 13   460 110 2 timeout 900   150 13000 0
ldv-regression/test03_true-unreach-call_true-termination.c true .12  24 1.0  2 true .11  6.4 .25 2 true .047 6.3 .26 2 true 2.8 250 29 2 unknown .80 66 9.0 0 true 8.1 370 110 2 true 8.1 370 100 2 true .071 26 .79 2 timeout 900    85 12000   0 true 13 1100 85 2 true .34 58 3.6 2 true .15 34 1.2 2 true 3.9 210 40 2 disqualified 2.0 71 27 0 true .14 16 1.5 2 true 7.7 360 59 2 true 8.2 370 65 2 true 7.7 350 64 2 true 13   470 110 2 timeout 900   150 12000 0
ldv-regression/test04_true-unreach-call_true-termination.c true .095 24 .90 2 true .050 7.5 .32 2 true .039 6.9 .43 2 true 2.9 250 25 2 unknown .78 65 8.7 0 true 8.2 370 120 2 true 8.0 370 96 2 true .086 26 .80 2 timeout 900    85 11000   0 true 11 1200 90 2 true .36 59 3.3 2 true .21 47 2.1 2 true 3.7 210 40 2 disqualified 2.0 67 22 0 true .14 16 1.5 2 true 8.0 360 69 2 true 7.7 380 64 2 true 8.6 380 74 2 true 14   480 130 2 timeout 900   150 13000 0
ldv-regression/test05_true-unreach-call_true-termination.c true .098 25 .88 2 true .047 7.1 .48 2 true .046 6.9 .39 2 true 2.9 250 27 2 unknown .77 67 8.3 0 true 8.1 370 100 2 true 8.1 370 97 2 true .080 26 .89 2 timeout 900    85 9900   0 true 14 1100 90 2 true .40 59 3.3 2 true .24 47 1.6 2 true 4.0 220 35 2 disqualified 2.0 71 21 0 true .15 16 1.6 2 true 9.9 380 79 2 true 8.7 350 70 2 true 9.4 360 68 2 true 18   680 140 2 timeout 900   150 12000 0
ldv-regression/test07_true-unreach-call_true-termination.c true .095 24 .77 2 true .052 6.6 .36 2 true .041 6.6 .31 2 true 2.9 260 26 2 unknown .80 66 10   0 true 8.1 370 96 2 true 8.0 370 100 2 true .079 26 .97 2 timeout 900    85 11000   0 true 12 1200 84 2 true .37 59 3.1 2 true .14 34 1.2 2 true 4.1 230 41 2 disqualified 2.0 67 25 0 true .15 15 1.6 2 true 9.0 360 73 2 true 7.9 360 66 2 true 10   370 84 2 true 15   520 130 2 timeout 900   150 9700 0
ldv-regression/test09_true-unreach-call_true-termination.c true .098 23 .74 2 true .050 6.7 .44 2 true .074 5.4 .29 2 true 2.9 260 22 2 unknown .77 65 8.2 0 true 8.1 370 120 2 true 8.0 370 100 2 true .080 26 .85 2 timeout 900    84 11000   0 true 13 1100 94 2 true .35 58 3.2 2 true .14 33 1.3 2 true 3.8 230 38 2 disqualified 2.0 67 25 0 true .14 15 1.7 2 true 9.0 360 70 2 true 7.4 330 63 2 true 9.9 380 75 2 true 15   500 140 2 timeout 900   150 14000 0
ldv-regression/test10_true-unreach-call_true-termination.c true .13  24 .71 2 true .12  6.1 .27 2 true .045 6.6 .32 2 true 3.1 250 32 2 unknown .79 66 9.2 0 true 8.2 370 94 2 true 8.4 370 100 2 true .079 26 .85 2 timeout 900    2100 8900   0 true 14 1100 93 2 true .35 59 3.1 2 true .20 47 1.9 2 unknown 10   290 96 0 disqualified 2.0 70 30 0 true .15 16 2.0 2 true 11   500 84 2 true 9.9 350 85 2 true 10   470 80 2 true 20   650 200 2 timeout 900   150 12000 0
ldv-regression/test11_true-unreach-call_true-termination.c true .11  24 .77 2 true .056 6.5 .39 2 true .072 6.1 .31 2 true 3.0 260 29 2 unknown .80 67 8.5 0 unknown 8.2 430 100 0 true 8.4 370 110 2 true .088 26 .91 2 timeout 900    4300 9200   0 true 14 1100 89 2 true .37 59 3.3 2 true .14 33 1.5 2 true 4.0 220 39 2 disqualified 2.0 72 28 0 true .16 16 1.8 2 true 9.1 380 75 2 true 8.9 370 66 2 true 8.9 380 71 2 true 14   460 130 2 timeout 900   150 13000 0
ldv-regression/test13_true-unreach-call_true-termination.c true .093 24 .80 2 true .055 6.9 .39 2 true .038 6.7 .32 2 true 2.9 250 24 2 unknown .79 66 8.5 0 true 8.2 370 100 2 true 8.2 370 120 2 true .084 26 .85 2 timeout 900    85 10000   0 true 13 1100 100 2 true .40 59 2.9 2 true .14 33 1.2 2 unknown 9.4 260 94 0 disqualified 2.0 67 24 0 true .15 16 1.6 2 true 8.1 360 58 2 true 8.8 360 57 2 true 8.5 360 61 2 true 14   460 110 2 timeout 900   150 11000 0
ldv-regression/test14_true-unreach-call_true-termination.c true .098 24 .93 2 true .057 6.5 .38 2 true .044 6.7 .34 2 true 2.9 260 29 2 unknown .79 66 8.5 0 unknown 8.1 430 100 0 true 8.4 370 100 2 true .082 26 .86 2 true 710    4300 8400   2 true 13 1100 86 2 true .37 59 5.0 2 true .14 32 1.3 2 true 3.9 220 38 2 disqualified 2.1 72 29 0 true .15 16 1.9 2 true 9.0 380 75 2 true 8.4 360 72 2 true 8.5 370 65 2 true 14   460 110 2 timeout 900   160 11000 0
ldv-regression/test15_true-unreach-call_true-termination.c true .094 24 .79 2 true .058 7.9 .32 2 true .060 6.7 .25 2 true 2.9 250 26 2 unknown .78 66 8.1 0 unknown 8.2 430 100 0 true 8.4 370 120 2 true .084 26 .91 2 timeout 900    2200 10000   0 true 12 1200 80 2 true .35 59 2.7 2 true .16 33 1.3 2 true 3.9 220 38 2 disqualified 2.0 75 23 0 true .17 20 1.8 2 true 8.5 350 57 2 true 7.7 360 62 2 true 7.6 350 58 2 true 14   460 120 2 timeout 900   150 10000 0
ldv-regression/test16_true-unreach-call_true-termination.c true .12  23 1.3  2 true .049 7.2 .37 2 true .048 6.2 .26 2 true 2.9 250 26 2 unknown .80 67 8.1 0 true 8.1 370 95 2 true 8.2 370 100 2 true .075 26 .77 2 timeout 900    85 9500   0 true 12 1200 86 2 true .37 59 3.0 2 true .13 31 1.3 2 true 4.1 220 36 2 disqualified 2.0 70 24 0 true .17 16 1.8 2 true 8.7 380 71 2 true 8.1 370 59 2 true 8.6 370 70 2 true 14   480 140 2 timeout 900   150 14000 0
ldv-regression/test17_true-unreach-call_true-termination.c true .093 23 .85 2 true .053 7.4 .30 2 true .045 6.6 .21 2 true 2.8 250 29 2 unknown .77 64 8.9 0 true 8.1 370 110 2 true 8.2 370 110 2 true .084 26 .96 2 timeout 900    84 11000   0 true 13 1100 96 2 true .35 59 3.3 2 true .26 47 1.5 2 true 4.0 220 35 2 disqualified 1.9 68 21 0 true .14 16 1.5 2 true 7.9 370 60 2 true 7.2 340 58 2 true 8.6 370 66 2 true 13   450 120 2 timeout 900   150 13000 0
ldv-regression/test18_true-unreach-call_true-termination.c true .096 24 .75 2 true .11  6.2 .26 2 true .074 6.3 .22 2 true 2.8 250 30 2 unknown .82 67 7.8 0 true 8.0 370 98 2 true 8.0 370 99 2 true .11  26 .87 2 timeout 900    84 11000   0 true 13 1100 91 2 true .35 58 3.2 2 true .15 35 1.1 2 true 4.0 220 34 2 disqualified 2.0 72 25 0 true .14 16 1.7 2 true 9.2 360 73 2 true 8.4 360 69 2 true 8.5 370 71 2 true 15   460 120 2 timeout 900   150 12000 0
ldv-regression/test19_true-unreach-call_true-termination.c true .094 24 .94 2 true .047 7.8 .43 2 true .056 6.2 .36 2 true 3.0 250 27 2 unknown .79 67 8.2 0 unknown 8.1 430 130 0 true 8.2 370 90 2 true .082 26 1.2  2 timeout 900    4200 10000   0 true 13 1100 88 2 true .36 59 3.1 2 true .14 34 1.4 2 true 3.9 220 36 2 disqualified 2.0 70 24 0 true .15 16 1.5 2 true 9.4 380 72 2 true 8.4 370 64 2 true 8.5 360 69 2 true 16   510 160 2 timeout 900   150 11000 0
ldv-regression/test20_true-unreach-call_true-termination.c true .099 24 .81 2 true .049 7.7 .36 2 true .039 6.4 .38 2 true 2.8 250 28 2 unknown .79 67 7.5 0 true 8.0 370 110 2 true 8.2 370 110 2 true .077 26 .83 2 timeout 900    85 10000   0 true 12 1200 83 2 true .35 59 3.3 2 true .15 33 1.1 2 true 4.1 220 44 2 disqualified 2.0 67 24 0 true .14 15 1.7 2 true 8.4 370 64 2 true 7.7 370 61 2 true 8.2 380 62 2 true 14   470 120 2 timeout 900   150 12000 0
ldv-regression/test21_true-unreach-call_true-termination.c true .099 24 .81 2 true .10  6.5 .28 2 true .059 6.7 .41 2 true 3.1 260 27 2 unknown .86 66 11   0 unknown 8.3 430 110 0 error - divine failed with signal 6 (sorts (_ bitvec 32) and (_ bitvec 1) are incompatible) 8.6 370 100 0 true .098 26 1.1  2 timeout 900    4300 8600   0 true 14 1100 95 2 true .36 59 3.6 2 true .15 34 1.6 2 true 4.3 270 40 2 disqualified 2.0 72 23 0 true .30 18 4.6 2 true 9.4 370 78 2 true 7.0 330 58 2 true 9.3 380 79 2 true 15   490 130 2 timeout 900   150 10000 0
ldv-regression/test22_true-unreach-call.c true .27  24 3.2  2 true .79  7.6 9.8  2 true .58  7.9 7.7  2 true 11   510 80 2 unknown 1.1  65 12   0 unknown 8.3 430 130 0 true 20   380 230 2 true .83  26 10    2 timeout 900    4300 7400   0 true 20 1300 130 2 true .41 59 4.2 2 false(unreach-call) .22 35 2.0 -16 true 4.2 270 41 2 disqualified 2.7 82 35 0 true .31 18 3.9 2 true 21   740 180 2 true 30   820 300 2 true 150   840 1800 2 true 28   820 290 2 timeout 900   150 12000 0
ldv-regression/test23_true-unreach-call.c error (134) .14  24 .58 0 true .43  12   5.3  2 true 1.3   13   21    2 true 8.3 440 72 2 unknown 1.6  67 18   0 unknown 8.3 430 94 0 true 14   380 140 2 true 1.9   31 24    2 timeout 900    4300 8400   0 true 16 1200 120 2 true .59 100 6.0 2 true .51 37 4.9 2 unknown 11   290 110 0 disqualified 2.8 85 39 0 true .33 19 4.0 2 true 87   860 1100 2 true 30   650 250 2 true 50   860 530 2 true 66   740 650 2 timeout 900   150 13000 0
ldv-regression/test24_true-unreach-call_true-termination.c error (134) .090 24 .80 0 true .33  10   4.1  2 true .96  12   12    2 true 6.6 370 55 2 unknown 1.3  68 14   0 unknown 8.1 430 94 0 true 10   370 120 2 true 1.6   30 21    2 timeout 900    2100 10000   0 true 13 1200 100 2 timeout 900    400 6300   0 true .21 34 1.6 2 true 11   320 110 2 disqualified 2.5 75 30 0 true .20 17 2.5 2 true 33   550 390 2 true 24   590 230 2 true 22   610 240 2 true 21   580 170 2 timeout 900   200 11000 0
ldv-regression/test25_true-unreach-call.c error (134) .087 24 .82 0 true 1.9   13   24    2 true 1.6   12   20    2 true 13   560 110 2 unknown 2.5  66 33   0 unknown 8.1 430 98 0 true 11   370 150 2 true 1.0   30 13    2 timeout 900    4300 11000   0 true 20 1300 170 2 timeout 900    430 3300   0 false(unreach-call) .22 35 1.9 -16 true 4.1 240 38 2 disqualified 3.5 83 51 0 true .19 19 2.1 2 true 23   500 240 2 true 150   850 1500 2 true 15   550 130 2 true 47   690 490 2 timeout 900   150 14000 0
ldv-regression/test26_true-unreach-call_true-termination.c true .10  23 .71 2 true .049 7.4 .32 2 true .045 6.2 .27 2 true 3.0 250 26 2 unknown .79 68 8.7 0 true 8.1 370 93 2 true 8.1 370 98 2 true .10  26 .76 2 timeout 900    85 12000   0 true 12 1200 82 2 true .36 59 3.3 2 true .35 47 1.1 2 true 4.1 220 38 2 disqualified 2.0 66 22 0 true .14 15 1.6 2 true 9.0 370 76 2 true 8.6 360 61 2 true 8.8 380 72 2 true 15   480 120 2 timeout 900   190 14000 0
ldv-regression/test27_true-unreach-call_true-termination.c error (134) .096 24 .74 0 true .23  11   2.7  2 true .79  13   11    2 true 18   510 190 2 unknown .93 67 11   0 unknown 8.3 430 100 0 error - divine failed with signal 6 (sorts (_ bitvec 64) and (_ bitvec 32) are incompatible) 10   370 130 0 true .19  26 2.0  2 timeout 900    4400 7500   0 true 26 1300 210 2 error (8) .37 59 3.3 0 true .44 49 3.0 2 unknown 13   320 120 0 disqualified 3.3 89 39 0 true .73 20 8.9 2 true 80   960 970 2 true 270   1000 2200 2 timeout 900   1100 12000 0 true 75   780 780 2 timeout 900   150 12000 0
ldv-regression/test28_true-unreach-call_true-termination.c true .12  24 .86 2 true .050 7.4 .39 2 true .062 6.9 .37 2 true 3.1 250 29 2 unknown .77 66 8.5 0 unknown 8.4 430 120 0 true 8.4 370 93 2 true .11  26 .79 2 timeout 900    2200 12000   0 true 14 1100 93 2 true .34 59 3.9 2 true .17 32 1.0 2 unknown 11   290 98 0 disqualified 2.0 71 22 0 true .28 19 3.2 2 true 8.4 350 72 2 true 8.6 370 65 2 true 8.7 350 76 2 true 14   470 140 2 timeout 900   150 9700 0
ldv-regression/test29_true-unreach-call_true-termination.c true .10  24 .81 2 true .061 6.7 .41 2 true .053 6.5 .46 2 true 2.9 260 28 2 unknown .79 66 8.6 0 unknown 7.9 430 100 0 true 8.5 370 100 2 true .079 26 1.0  2 timeout 900    2200 10000   0 true 13 1100 98 2 true .38 59 3.5 2 true .14 34 1.3 2 unknown 10   280 110 0 disqualified 2.0 71 27 0 true .17 18 2.2 2 true 8.7 360 67 2 true 8.8 360 85 2 true 9.4 370 65 2 true 12   440 120 2 timeout 900   150 12000 0
ldv-regression/test30_true-unreach-call_true-termination.c false(unreach-call) .11  24 1.1  -16 true .057 7.0 .34 2 true .040 6.7 .29 2 true 2.9 250 29 2 unknown .80 66 8.4 0 true 8.2 370 110 2 true 8.1 370 110 2 true .10  26 .78 2 timeout 900    84 12000   0 true 14 1100 84 2 true .37 59 3.1 2 true .14 34 1.1 2 unknown 9.7 300 100 0 disqualified 2.0 71 23 0 true .15 16 1.5 2 true 10   430 75 2 true 7.2 350 60 2 true 9.9 410 85 2 true 17   620 160 2 timeout 900   150 13000 0
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error (134) .38  42 3.5  0 false(unreach-call) 55     1400   590    1 error (134) .27  28   4.2  0 false(unreach-call) 11   390 99 1 false(unreach-call) 6.1  52 82   1 false(unreach-call) 9.0 450 130 1 error - divine failed with signal 11 1.6 200 18 0 false(unreach-call) .21  38 2.9  1 unknown 1.6  47 17   0 false(unreach-call) 27 1300 240 1 false(unreach-call) 1.2  85 13   1 false(unreach-call) .58 60 4.7 1 unknown 51   1300 420 0 disqualified 23   230 280 0 false(unreach-call) .64 23 7.7 1 unknown 350   2900 3000 0 error (7) 97   1100 950 0 unknown 340   2900 2700 0 error 14   240 120 0 false(unreach-call) 9.6 240 100 1
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error (134) .34  41 3.2  0 false(unreach-call) 46     1400   570    1 error (134) .26  28   3.2  0 false(unreach-call) 10   510 88 1 false(unreach-call) 6.1  51 70   1 false(unreach-call) 9.0 450 100 1 error - divine failed with signal 11 1.6 200 21 0 false(unreach-call) .22  38 2.5  1 unknown 1.6  47 21   0 false(unreach-call) 25 1300 240 1 false(unreach-call) 1.2  84 11   1 false(unreach-call) .52 60 4.5 1 unknown 49   1300 430 0 disqualified 24   250 310 0 false(unreach-call) .73 22 6.7 1 unknown 270   2600 2400 0 error (7) 95   1000 920 0 unknown 280   2600 2100 0 error 15   250 130 0 false(unreach-call) 9.3 250 99 1
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error (134) .35  41 3.0  0 false(unreach-call) 51     1400   610    1 error (134) .26  28   3.2  0 false(unreach-call) 10   510 98 1 false(unreach-call) 6.0  51 73   1 false(unreach-call) 8.9 450 140 1 error - divine failed with signal 11 1.6 200 19 0 false(unreach-call) .22  38 2.1  1 unknown 1.6  47 16   0 false(unreach-call) 25 1200 230 1 false(unreach-call) 1.2  85 13   1 false(unreach-call) .53 60 4.8 1 unknown 49   1300 390 0 disqualified 23   240 270 0 false(unreach-call) .66 23 8.6 1 timeout 900   1600 8800 0 error (7) 110   1000 1100 0 timeout 900   1600 10000 0 error 15   240 130 0 false(unreach-call) 9.1 220 110 1
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i error (134) .33  41 3.2  0 error (42) 880     2400   7100    0 out of memory 280     15000   3200    0 true 96   3800 1100 2 true 5.0  260 58   2 unknown 8.8 450 120 0 error - divine failed with signal 11 1.7 200 22 0 true .43  57 5.4  2 unknown 1.6  47 19   0 true 20 1200 170 2 error (8) 1.2  87 13   0 unknown .82 79 6.2 0 true 23   1300 200 2 disqualified 4.7 130 57 0 true .45 18 5.0 2 true 21   810 160 2 true 23   980 190 2 true 23   830 180 2 true 34   630 300 2 error (1) 870   220 12000 0
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (134) .36  41 3.1  0 error (42) 880     2400   9400    0 out of memory 280     15000   3400    0 true 96   3700 980 2 true 5.0  260 75   2 unknown 8.8 450 99 0 error - divine failed with signal 11 1.6 200 19 0 true .41  57 4.4  2 unknown 1.6  47 20   0 true 20 1200 190 2 error (8) 1.2  87 11   0 unknown .70 62 6.3 0 true 23   1200 200 2 disqualified 4.8 130 67 0 true .44 17 5.9 2 true 21   800 180 2 true 21   790 170 2 true 22   820 170 2 true 34   650 270 2 error (1) 870   240 12000 0
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (134) .35  41 2.8  0 error (42) 880     2400   7500    0 out of memory 280     15000   3800    0 true 96   3800 1100 2 true 5.0  260 59   2 unknown 8.8 450 120 0 error - divine failed with signal 11 1.7 200 23 0 true .41  57 6.1  2 unknown 1.6  47 20   0 true 22 1100 210 2 error (8) 1.2  87 13   0 unknown .72 60 6.8 0 true 23   1200 170 2 disqualified 4.8 130 68 0 true .44 17 5.6 2 true 21   820 180 2 true 23   990 210 2 true 22   820 200 2 true 33   640 270 2 error (1) 870   220 10000 0
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (134) .33  42 3.3  0 error (42) 880     2400   7400    0 out of memory 280     15000   3300    0 true 97   3800 1200 2 true 5.0  260 59   2 unknown 8.7 450 110 0 error - divine failed with signal 11 1.6 200 26 0 true .42  57 4.6  2 unknown 1.6  47 18   0 true 21 1200 190 2 error (8) 1.2  87 12   0 unknown .72 59 5.7 0 true 23   1300 190 2 disqualified 4.8 130 66 0 true .46 17 6.2 2 true 20   810 160 2 true 21   810 180 2 true 23   830 160 2 true 33   620 260 2 error (1) 870   220 13000 0
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (134) .33  42 3.9  0 error (42) 880     2400   7600    0 out of memory 280     15000   3400    0 true 96   3700 1000 2 true 5.1  260 60   2 unknown 8.8 450 84 0 error - divine failed with signal 11 1.6 200 23 0 true .42  57 5.9  2 unknown 1.6  46 20   0 true 21 1200 180 2 error (8) 1.3  87 11   0 unknown .70 60 6.0 0 true 23   1200 190 2 disqualified 4.8 130 67 0 true .47 17 5.2 2 true 21   820 160 2 true 22   820 200 2 true 24   830 180 2 true 35   650 260 2 error (1) 870   230 10000 0
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (134) .33  41 4.3  0 error (42) 880     2400   7100    0 out of memory 280     15000   3200    0 true 96   3800 1100 2 true 5.0  260 62   2 unknown 8.8 450 120 0 error - divine failed with signal 11 1.6 200 24 0 true .42  57 5.9  2 unknown 1.6  47 20   0 true 21 1200 170 2 error (8) 1.2  87 12   0 unknown .77 61 5.7 0 true 23   1200 200 2 disqualified 4.8 130 60 0 true .45 18 6.0 2 true 21   780 180 2 true 22   980 200 2 true 23   770 190 2 true 34   610 280 2 error (1) 870   220 12000 0
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (134) .34  41 3.7  0 error (42) 880     2400   7200    0 out of memory 280     15000   4200    0 true 97   3800 1100 2 true 5.2  260 61   2 unknown 8.8 450 120 0 error - divine failed with signal 11 1.6 200 19 0 true .41  57 4.9  2 unknown 1.6  47 20   0 true 21 1200 180 2 error (8) 1.2  87 10   0 unknown .75 60 6.1 0 true 23   1200 180 2 disqualified 4.8 130 110 0 true .44 17 5.3 2 true 21   800 170 2 true 21   970 200 2 true 22   790 170 2 true 33   620 250 2 error (1) 870   220 11000 0
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (134) .33  42 3.3  0 error (42) 880     2400   8000    0 out of memory 280     15000   2800    0 true 96   3800 1100 2 true 5.2  260 62   2 unknown 8.9 450 110 0 error - divine failed with signal 11 1.6 200 22 0 true .40  57 5.9  2 unknown 1.5  47 17   0 true 21 1200 170 2 error (8) 1.2  87 13   0 unknown .68 60 5.8 0 true 23   1300 190 2 disqualified 4.7 130 59 0 true .45 18 5.7 2 true 20   800 160 2 true 24   970 200 2 true 23   830 200 2 true 33   620 310 2 error (1) 870   220 9400 0
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error (134) .33  41 3.5  0 error (42) 880     2400   9900    0 out of memory 280     15000   3400    0 true 96   3800 1100 2 true 5.0  260 58   2 unknown 8.9 450 130 0 error - divine failed with signal 11 1.6 200 25 0 true .43  57 6.2  2 unknown 1.6  47 19   0 true 20 1200 180 2 error (8) 1.2  87 15   0 unknown .70 60 6.4 0 true 23   1200 180 2 disqualified 4.8 130 61 0 true .45 17 6.1 2 true 20   790 160 2 true 22   960 190 2 true 24   820 190 2 true 33   620 280 2 error (1) 870   270 11000 0
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error (134) .33  41 3.2  0 error (42) 880     2400   9400    0 out of memory 280     15000   3100    0 true 97   3800 1100 2 true 5.0  260 60   2 unknown 8.7 450 100 0 error - divine failed with signal 11 1.6 200 23 0 true .41  57 5.4  2 unknown 1.6  47 17   0 true 20 1200 200 2 error (8) 1.2  86 14   0 unknown 1.1  79 5.4 0 true 23   1200 170 2 disqualified 4.7 130 58 0 true .46 18 5.1 2 true 21   820 170 2 true 23   790 190 2 true 23   820 190 2 true 33   660 270 2 error (1) 870   230 12000 0
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 6.8   230 92    0 false(unreach-call) .15  9.8 .87 1 error (134) .074 7.8 .51 0 false(unreach-call) 7.6 430 65 1 false(unreach-call) .24 35 2.5 1 false(unreach-call) 8.4 450 120 1 false(unreach-call) 8.5 450 98 1 false(unreach-call) .18  27 1.6  1 false(unreach-call) .47 83 5.5 1 false(unreach-call) 17 1200 130 1 timeout 900    900 8400   0 false(unreach-call) .26 37 1.7 1 unknown 12   300 110 0 disqualified 3.5 97 48 0 false(unreach-call) .23 18 3.0 1 false(unreach-call) 15   580 130 1 false(unreach-call) 15   540 120 1 false(unreach-call) 14   510 110 1 false(unreach-call) 27   280 220 1 false(unreach-call) 16   660 180 1
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1.5   53 17    1 false(unreach-call) .10  9.7 .92 1 error (134) .064 7.7 .89 0 false(unreach-call) 6.7 370 51 1 false(unreach-call) .17 34 1.9 1 false(unreach-call) 8.4 440 110 1 false(unreach-call) 8.6 450 100 1 false(unreach-call) .13  27 1.2  1 false(unreach-call) .48 83 5.8 1 false(unreach-call) 16 1200 110 1 false(unreach-call) .73 64 6.4 1 false(unreach-call) .19 34 1.5 1 unknown 12   330 120 0 disqualified 3.3 85 46 0 false(unreach-call) .21 17 2.9 1 false(unreach-call) 9.4 360 73 1 false(unreach-call) 9.9 370 89 1 false(unreach-call) 10   380 77 1 false(unreach-call) 32   270 300 1 false(unreach-call) 4.7 160 44 1
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 8.8   190 96    1 false(unreach-call) .14  9.5 .73 1 error (134) .087 9.7 .78 0 false(unreach-call) 6.5 370 58 1 false(unreach-call) .16 34 2.2 1 false(unreach-call) 8.6 450 99 1 false(unreach-call) 8.5 450 95 1 false(unreach-call) .13  27 1.1  1 false(unreach-call) .47 83 4.7 1 false(unreach-call) 15 1200 100 1 timeout 900    470 11000   0 false(unreach-call) .20 37 1.6 1 unknown 13   310 130 0 disqualified 3.3 85 39 0 false(unreach-call) .21 17 2.6 1 false(unreach-call) 9.3 380 70 1 false(unreach-call) 11   380 83 1 false(unreach-call) 8.9 360 70 1 false(unreach-call) 22   280 180 1 false(unreach-call) 6.8 950 76 1
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i error (5) 56     460 560    0 false(unreach-call) .17  9.4 2.2  1 error (134) .077 8.1 .78 0 false(unreach-call) 16   660 140 0 false(unreach-call) 1.3  37 17   1 false(unreach-call) 8.5 560 88 1 false(unreach-call) 8.8 450 120 1 false(unreach-call) .43  28 6.1  1 unknown 90    260 1300   0 false(unreach-call) 24 1300 180 0 timeout 900    540 10000   0 false(unreach-call) .24 36 2.2 1 unknown 13   320 110 0 disqualified 3.8 93 45 0 false(unreach-call) .25 17 2.9 0 false(unreach-call) 200   930 2400 1 false(unreach-call) 100   1100 1100 1 timeout 900   730 9600 0 false(unreach-call) 25   280 180 1 false(unreach-call) 7.1 940 78 1
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 5.6   190 73    1 false(unreach-call) .15  11   1.3  1 false(unreach-call) .085 9.6 .90 1 false(unreach-call) 6.8 390 62 1 false(unreach-call) .18 34 1.7 1 false(unreach-call) 8.4 450 93 1 false(unreach-call) 8.7 440 110 1 false(unreach-call) .093 27 .98 1 false(unreach-call) .47 83 5.8 1 false(unreach-call) 15 1200 110 1 timeout 900    880 11000   0 false(unreach-call) .39 49 1.6 1 unknown 12   300 100 0 disqualified 3.3 86 39 0 false(unreach-call) .20 17 2.4 1 false(unreach-call) 13   520 100 1 false(unreach-call) 12   470 110 1 false(unreach-call) 13   590 110 1 false(unreach-call) 230   2000 2300 1 false(unreach-call) 6.8 660 82 1
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error (5) 22     470 240    0 false(unreach-call) .17  13   2.0  1 error (134) .066 7.8 .50 0 false(unreach-call) 11   520 81 1 false(unreach-call) .70 37 8.2 1 false(unreach-call) 8.3 450 100 0 false(unreach-call) 8.5 450 130 0 false(unreach-call) .44  31 4.9  1 unknown 13    200 160   0 false(unreach-call) 20 1200 140 1 timeout 900    870 11000   0 false(unreach-call) .26 37 2.3 1 unknown 13   320 110 0 disqualified 3.5 120 41 0 false(unreach-call) .26 18 2.2 0 false(unreach-call) 33   760 290 1 false(unreach-call) 82   970 850 1 timeout 900   1000 11000 0 false(unreach-call) 260   2200 2800 0 false(unreach-call) 7.1 660 82 1
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 10     250 120    0 false(unreach-call) .13  9.8 2.1  1 error (134) .11  14   1.3  0 false(unreach-call) 4.4 290 44 1 false(unreach-call) .22 34 2.1 1 false(unreach-call) 8.4 450 90 1 false(unreach-call) 8.7 440 110 1 false(unreach-call) .12  26 1.5  1 unknown 10    170 120   0 false(unreach-call) 16 1200 100 1 timeout 900    530 9600   0 false(unreach-call) .19 36 1.8 1 unknown 12   310 110 0 disqualified 3.3 86 35 0 false(unreach-call) .23 18 3.5 1 false(unreach-call) 9.7 380 70 1 false(unreach-call) 9.5 360 71 1 false(unreach-call) 8.6 350 63 1 false(unreach-call) 28   280 250 1 false(unreach-call) 6.9 970 67 1
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i error (5) 230     810 2500    0 false(unreach-call) .13  9.7 1.2  1 error (134) .12  16   1.3  0 false(unreach-call) 17   660 150 1 false(unreach-call) .49 36 6.2 1 false(unreach-call) 8.5 450 130 1 false(unreach-call) 8.5 450 110 1 false(unreach-call) .20  27 3.1  1 unknown 41    240 480   0 false(unreach-call) 25 1300 200 1 false(unreach-call) .71 64 6.5 1 false(unreach-call) .44 36 4.5 1 unknown 13   320 120 0 disqualified 3.6 96 42 0 false(unreach-call) .24 18 2.5 1 false(unreach-call) 11   390 79 1 false(unreach-call) 11   370 90 1 false(unreach-call) 10   390 80 1 false(unreach-call) 30   290 260 1 false(unreach-call) 7.1 660 80 1
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) .95  40 11    1 false(unreach-call) .12  9.4 1.1  1 false(unreach-call) .11  9.4 .77 1 false(unreach-call) 7.0 390 56 1 false(unreach-call) .18 34 2.1 1 false(unreach-call) 8.4 450 97 1 false(unreach-call) 8.5 450 110 1 false(unreach-call) .13  27 1.6  1 false(unreach-call) .44 83 4.8 1 false(unreach-call) 16 1200 120 1 timeout 900    530 9700   0 false(unreach-call) .18 36 1.7 1 unknown 12   310 110 0 disqualified 3.3 86 43 0 false(unreach-call) .21 17 2.5 1 false(unreach-call) 10   380 88 1 false(unreach-call) 12   490 97 1 false(unreach-call) 10   370 81 1 false(unreach-call) 25   280 230 1 false(unreach-call) 6.9 1000 72 1
forester-heap/sll-01_false-unreach-call_false-valid-deref.i error (5) 17     350 180    0 false(unreach-call) .10  9.7 1.1  1