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 Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 Predator-HP 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
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-12-01 08:19:20 CET 2017-12-01 08:19:34 CET 2017-12-01 08:37:17 CET 2017-12-01 08:43:39 CET 2017-12-01 08:22:21 CET 2017-12-01 09:05:19 CET 2017-12-02 00:00:31 CET 2017-12-02 11:31:00 CET 2017-12-01 19:12:21 CET 2017-12-01 23:12:01 CET 2017-12-01 21:45:44 CET 2017-12-02 23:08:57 CET 2017-12-03 04:39:25 CET 2017-12-03 04:40:15 CET 2017-12-03 07:53:44 CET
Run set 2ls.sv-comp18.MemSafety-LinkedLists cbmc.sv-comp18.MemSafety-LinkedLists cpa-bam-bnb.sv-comp18.MemSafety-LinkedLists cpa-bam-slicing.sv-comp18.MemSafety-LinkedLists cpa-seq.sv-comp18.MemSafety-LinkedLists depthk.sv-comp18.MemSafety-LinkedLists esbmc-incr.sv-comp18.MemSafety-LinkedLists esbmc-kind.sv-comp18.MemSafety-LinkedLists forester.sv-comp18.MemSafety-LinkedLists map2check.sv-comp18.MemSafety-LinkedLists predatorhp.sv-comp18.MemSafety-LinkedLists symbiotic.sv-comp18.MemSafety-LinkedLists uautomizer.sv-comp18.MemSafety-LinkedLists ukojak.sv-comp18.MemSafety-LinkedLists utaipan.sv-comp18.MemSafety-LinkedLists
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 --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
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (134) .27 29 2.5 0 error (42) 870    720 8500   0 error (1) .48 41 3.9 0 error (1) .44 40 4.3 0 timeout 910   5300 6700 0 unknown 900    1300 10000   0 timeout 900    6600 6100   0 out of memory 310    15000 2900   0 unknown .058 11 .56 0 unknown 900    210 11000   0 true 1.5  49 18   2 timeout (timeout) 900    850 10000   0 error (7) 410   1200 4800 0 timeout 900   1600 12000 0 timeout 900   840 11000 0
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (5) .38 27 4.4 0 error (42) 870    3300 8700   0 error (1) .49 41 3.9 0 error (1) .42 40 4.3 0 error (recursion) 2.9 260 26 0 unknown 890    360 11000   0 timeout 900    9700 5400   0 timeout 900    12000 5700   0 unknown .055 11 .66 0 unknown 900    420 10000   0 true 2.5  59 29   2 timeout (timeout) 900    2700 6500   0 timeout 900   1600 11000 0 timeout 900   1500 10000 0 error (7) 370   1200 4600 0
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (5) .49 38 5.1 0 error (134) 440    13000 4700   0 error (1) .49 43 4.6 0 error (1) .42 40 4.1 0 timeout (segmentation fault) 910   11000 5600 0 unknown 890    850 12000   0 timeout 900    1600 8000   0 timeout 900    3000 8900   0 unknown .072 11 .46 0 unknown 900    340 11000   0 true 1.6  67 18   2 timeout (timeout) 900    990 12000   0 timeout 900   1200 11000 0 timeout 900   1600 12000 0 timeout 900   1800 12000 0
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i out of memory 13    15000 150   0 error (42) 870    4300 5500   0 error (1) .48 40 4.2 0 error (1) .44 40 4.2 0 timeout 920   5300 6400 0 unknown 890    310 9800   0 timeout 900    840 11000   0 timeout 900    780 12000   0 unknown .14  14 2.0  0 unknown 890    370 12000   0 true 2.2  71 21   2 timeout (timeout) 900    2900 11000   0 timeout 900   960 13000 0 timeout 900   5300 13000 0 timeout 900   930 10000 0
heap-manipulation/tree_false-unreach-call_false-valid-deref.i error (5) .40 31 3.7 0 false(valid-deref) .75 46 7.7 1 error (1) .49 41 4.4 0 error (1) .42 37 3.4 0 timeout 920   11000 5200 0 false(valid-deref) 1.4  29 17   0 false(valid-memtrack) 1.2  32 11   -16 false(valid-deref) .68 29 6.5 1 unknown .055 11 .51 0 false(valid-deref) 2.7  15 31   1 false(valid-deref) 2.1  25 22   1 false(valid-deref) .32 13 3.6 1 false(valid-deref) 320   880 4400 1 false(valid-deref) 490   1900 7600 1 error (7) 140   1200 1500 0
heap-manipulation/tree_false-valid-deref.i false(valid-deref) .41 31 4.2 1 false(valid-deref) .76 47 8.8 1 error (1) .46 41 3.9 0 error (1) .46 41 3.9 0 timeout (segmentation fault) 920   11000 6600 0 false(valid-deref) .39 29 4.6 1 false(valid-deref) .11 27 1.1 1 false(valid-deref) .20 27 1.9 1 false(valid-deref) .073 11 .63 1 false(valid-deref) 1.1  15 15   1 false(valid-deref) .16 25 2.0 1 false(valid-deref) .32 13 3.3 1 false(valid-deref) 5.7 300 47 1 false(valid-deref) 6.9 350 57 1 false(valid-deref) 6.3 320 51 1
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (5) .17 26 1.6 0 false(unreach-call) .56 36 4.8 0 error (1) .49 44 4.3 0 error (1) .41 40 4.2 0 timeout (segmentation fault) 940   11000 5300 0 false(valid-memtrack) 1.2  29 12   0 false(valid-memtrack) .75 30 6.5 0 false(valid-memtrack) .41 29 4.5 0 false(valid-memtrack) .10  15 .94 0 unknown .42 12 5.0 0 false(valid-memtrack) .16 25 1.9 1 false(valid-memtrack) .34 13 3.5 0 timeout 900   1000 11000 0 timeout 900   1400 12000 0 timeout 900   1200 14000 0
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error (5) .35 29 3.5 0 false(unreach-call) .70 44 7.1 0 error (1) .49 41 4.4 0 error (1) .45 40 4.2 0 timeout 930   11000 5700 0 false(valid-memtrack) 1.8  38 20   1 false(valid-memtrack) 1.1  33 12   0 false(valid-memtrack) .64 30 7.5 0 unknown .40  19 5.5  0 false(valid-memtrack) .95 15 11   1 false(valid-memtrack) .17 23 1.9 1 false(valid-memtrack) .27 14 3.0 1 unknown 51   760 490 0 error (7) 230   2100 3300 0 unknown 250   1400 3200 0
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i witness invalid (false(valid-memtrack)) .53 34 5.5 0 false(unreach-call) .59 39 5.6 0 error (1) .49 43 4.5 0 error (1) .45 40 4.2 0 timeout (segmentation fault) 920   11000 5400 0 false(valid-memtrack) 1.4  32 18   0 false(valid-memtrack) 1.3  32 15   0 false(valid-memtrack) .78 30 7.2 0 false(valid-memtrack) 1.6   38 21    0 false(valid-memtrack) 1.3  14 19   1 false(valid-memtrack) .14 23 2.0 1 false(valid-memtrack) .27 14 3.2 1 timeout 900   860 10000 0 timeout 900   2100 12000 0 timeout 900   1500 11000 0
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i witness invalid (false(valid-memtrack)) .42 33 4.1 0 false(unreach-call) .56 36 5.3 0 error (1) .48 41 4.4 0 error (1) .43 37 3.4 0 timeout (segmentation fault) 940   11000 6200 0 false(valid-memtrack) 1.3  29 17   0 false(valid-memtrack) .93 32 10   0 false(valid-memtrack) .74 29 6.2 0 false(valid-memtrack) .71  24 10    0 false(valid-memtrack) 1.2  14 13   1 false(valid-memtrack) .16 23 1.7 1 false(valid-memtrack) .26 13 3.8 1 error (7) 230   880 2600 0 timeout 900   2000 14000 0 timeout 900   1500 11000 0
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (5) .38 30 3.4 0 error (42) 870    4400 6200   0 error (1) .46 40 4.3 0 error (1) .44 42 4.5 0 timeout 910   11000 5600 0 unknown 890    190 8500   0 timeout 900    500 11000   0 timeout 900    600 10000   0 true .19  16 2.0  2 unknown 890    220 14000   0 timeout 900    2000 9700   0 timeout (timeout) 900    2800 11000   0 error (7) 210   850 2400 0 timeout 900   1800 11000 0 timeout 900   1400 11000 0
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i witness invalid (false(valid-memtrack)) .26 27 2.4 0 false(unreach-call) .48 37 5.6 0 error (1) .47 41 4.1 0 error (1) .42 40 4.3 0 timeout 940   11000 5900 0 false(valid-memtrack) .47 28 5.0 0 false(valid-memtrack) .21 28 1.8 0 false(valid-memtrack) .24 28 2.5 0 unknown .051 10 .59 0 false(valid-memtrack) .71 14 9.3 0 false(valid-memtrack) .16 23 1.7 0 false(valid-memtrack) .27 11 3.2 0 unknown 13   320 100 0 unknown 43   720 460 0 unknown 24   540 200 0
list-properties/list_true-unreach-call_false-valid-memtrack.i witness invalid (false(valid-memtrack)) .45 32 4.7 0 false(unreach-call) .56 38 5.0 0 error (1) .47 40 4.0 0 error (1) .47 40 4.2 0 timeout 920   11000 5800 0 false(valid-memtrack) .45 28 5.4 1 false(valid-memtrack) .19 29 1.7 0 false(valid-memtrack) .44 29 4.4 0 timeout 2.6   30 850    0 false(valid-memtrack) .65 13 7.8 1 false(valid-memtrack) .15 24 1.8 1 false(valid-memtrack) .29 15 3.0 1 unknown 20   540 190 0 unknown 69   870 990 0 unknown 54   790 530 0
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i error (5) .23 27 1.8 0 false(unreach-call) .45 36 4.3 0 error (1) .49 44 4.8 0 error (1) .42 40 3.9 0 timeout (segmentation fault) 920   11000 6400 0 false(valid-memtrack) 1.0  28 13   0 false(valid-memtrack) .41 28 3.4 0 false(valid-memtrack) .26 28 2.1 0 witness invalid (false(valid-memtrack)) .080 11 .52 0 false(valid-memtrack) .74 13 8.6 0 false(valid-memtrack) .17 23 1.8 0 false(valid-memtrack) .25 11 2.8 0 unknown 14   340 110 0 unknown 40   700 470 0 unknown 20   600 170 0
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (5) .26 27 2.3 0 false(unreach-call) .51 36 4.4 0 error (1) .46 41 4.1 0 error (1) .44 40 3.8 0 timeout 930   11000 6400 0 false(valid-memtrack) 1.0  29 15   0 false(valid-memtrack) .54 29 4.8 0 false(valid-memtrack) .27 28 2.6 0 false(valid-memtrack) .052 11 .61 0 false(valid-memtrack) .61 13 7.3 1 false(valid-memtrack) .15 23 1.9 1 false(valid-memtrack) .27 11 2.8 1 unknown 18   470 150 0 unknown 69   950 760 0 unknown 32   710 290 0
list-properties/splice_true-unreach-call_false-valid-memtrack.i witness invalid (false(valid-memtrack)) .45 32 5.8 0 false(unreach-call) .54 37 4.7 0 error (1) .49 41 4.2 0 error (1) .48 41 4.1 0 timeout 910   11000 5700 0 false(valid-memtrack) .46 29 5.0 0 false(valid-memtrack) .15 29 1.6 0 false(valid-memtrack) .18 29 1.8 0 timeout 5.5   73 930    0 false(valid-memtrack) .70 14 9.4 1 false(valid-memtrack) .16 24 1.7 1 false(valid-memtrack) .26 11 3.6 1 unknown 13   320 110 0 unknown 19   530 170 0 unknown 17   420 130 0
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error (134) .93 40 12   0 true 71    920 740   2 error (1) .48 41 4.6 0 error (1) .45 41 4.3 0 true 5.6 290 46 2 unknown 900    1100 11000   0 true .22 40 2.8 2 true .21 40 2.2 2 unknown .15  18 1.3  0 out of memory 27    15000 350   0 true .60 53 5.2 2 true 5.2  870 68   2 true 160   1800 950 2 timeout 900   5400 14000 0 true 230   4900 2600 2
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error (134) .93 40 9.3 0 true 58    910 730   2 error (1) .46 41 4.4 0 error (1) .45 40 4.5 0 true 6.2 300 51 2 unknown 890    990 11000   0 true .23 40 2.0 2 true .21 40 2.0 2 unknown .14  17 1.6  0 out of memory 27    15000 380   0 true .57 51 5.1 2 true 4.0  710 49   2 true 150   1900 850 2 timeout 900   5300 11000 0 timeout 900   6200 11000 0
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error (134) 1.0  40 8.5 0 true 64    910 690   2 error (1) .48 40 4.8 0 error (1) .47 40 4.1 0 true 6.2 300 50 2 unknown 890    1200 10000   0 true .24 40 2.4 2 true .20 40 2.2 2 unknown .12  17 1.3  0 out of memory 27    15000 340   0 true .54 52 5.1 2 true 4.6  830 67   2 true 140   1800 1000 2 timeout 900   5300 12000 0 timeout 900   6400 10000 0
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i error (134) .95 40 11   0 false(unreach-call) 50    1100 540   0 error (1) .44 40 4.4 0 error (1) .44 40 4.2 0 false(valid-memtrack) 5.8 310 47 1 unknown 890    990 11000   0 unknown 6.9  230 91   0 unknown 8.7  260 130   0 unknown .15  17 1.4  0 false(valid-memtrack) 6.5  29 78   0 false(valid-memtrack) .48 52 5.1 0 false(valid-memtrack) 4.0  700 49   1 unknown 430   1900 2900 0 timeout 900   4900 13000 0 timeout 900   6400 9900 0
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (134) .93 40 11   0 false(unreach-call) 50    1100 550   0 error (1) .48 45 4.8 0 error (1) .44 40 3.8 0 false(valid-memtrack) 6.1 300 52 1 unknown 890    970 12000   0 unknown 6.9  230 77   0 unknown 6.5  250 92   0 unknown .14  17 1.6  0 false(valid-memtrack) 6.5  29 77   0 false(valid-memtrack) .52 52 4.9 0 false(valid-memtrack) 4.0  700 49   1 unknown 430   1900 2700 0 timeout 900   5300 14000 0 timeout 900   6400 11000 0
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (134) .94 40 9.2 0 false(unreach-call) 49    1100 600   0 error (1) .46 41 4.3 0 error (1) .45 40 4.8 0 false(valid-memtrack) 5.9 300 51 1 unknown 890    970 10000   0 unknown 6.8  230 83   0 unknown 8.7  250 100   0 unknown .15  17 1.4  0 false(valid-memtrack) 6.5  29 74   0 false(valid-memtrack) .53 52 4.4 0 false(valid-memtrack) 4.0  700 53   1 unknown 430   1900 3600 0 timeout 900   5300 14000 0 timeout 900   5800 9500 0
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (134) .95 40 11   0 false(unreach-call) 50    1100 550   0 error (1) .46 40 4.5 0 error (1) .42 41 4.1 0 false(valid-memtrack) 5.9 280 52 1 unknown 890    1000 9600   0 unknown 6.7  230 92   0 unknown 6.6  260 90   0 unknown .14  17 1.6  0 false(valid-memtrack) 6.5  31 83   0 false(valid-memtrack) .50 52 5.0 0 false(valid-memtrack) 4.0  700 62   1 unknown 430   1900 2900 0 timeout 900   5200 13000 0 timeout 900   6400 8300 0
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (134) .92 40 10   0 false(unreach-call) 51    1100 510   0 error (1) .50 41 4.2 0 error (1) .43 40 3.7 0 false(valid-memtrack) 6.2 310 46 1 unknown 890    1000 9900   0 unknown 5.2  230 57   0 unknown 8.7  250 120   0 unknown .14  17 1.5  0 false(valid-memtrack) 6.5  29 81   0 false(valid-memtrack) .53 52 4.7 0 false(valid-memtrack) 4.0  700 43   1 unknown 430   1900 3300 0 timeout 900   5300 12000 0 timeout 900   6600 8900 0
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (134) .94 40 9.2 0 false(unreach-call) 51    1100 560   0 error (1) .48 41 4.4 0 error (1) .43 40 3.6 0 false(valid-memtrack) 5.7 300 51 1 unknown 890    1200 9500   0 unknown 4.7  230 56   0 unknown 6.8  250 83   0 unknown .12  17 1.7  0 false(valid-memtrack) 6.5  29 83   0 false(valid-memtrack) .50 52 5.6 0 false(valid-memtrack) 4.0  700 48   1 unknown 430   1900 3700 0 timeout 900   5100 13000 0 timeout 900   4800 9200 0
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (134) .98 40 8.4 0 false(unreach-call) 49    1100 540   0 error (1) .49 42 4.1 0 error (1) .43 40 4.0 0 false(valid-memtrack) 6.0 300 44 1 unknown 890    1100 9100   0 unknown 6.7  220 75   0 unknown 8.7  250 96   0 unknown .15  17 1.4  0 false(valid-memtrack) 6.5  30 82   0 false(valid-memtrack) .52 52 4.7 0 false(valid-memtrack) 4.0  700 46   1 unknown 440   1800 2500 0 timeout 900   5100 14000 0 timeout 900   6300 9100 0
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (134) .94 42 10   0 false(unreach-call) 50    1100 530   0 error (1) .46 41 4.5 0 error (1) .45 40 3.8 0 false(valid-memtrack) 5.9 300 56 1 unknown 890    1100 10000   0 unknown 5.4  230 68   0 unknown 9.3  260 110   0 unknown .15  17 1.4  0 false(valid-memtrack) 6.5  29 63   0 false(valid-memtrack) .52 51 5.0 0 false(valid-memtrack) 4.0  700 54   1 unknown 430   1800 3200 0 timeout 900   5400 12000 0 timeout 900   6200 11000 0
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error (134) .94 40 10   0 false(unreach-call) 49    1100 650   0 error (1) .48 40 4.2 0 error (1) .43 40 3.8 0 false(valid-memtrack) 5.9 310 46 1 unknown 890    1000 8500   0 unknown 4.8  230 64   0 unknown 8.9  260 100   0 unknown .14  17 1.5  0 false(valid-memtrack) 6.5  29 79   0 false(valid-memtrack) .52 52 5.1 0 false(valid-memtrack) 4.1  700 53   1 unknown 430   1800 3200 0 timeout 900   5000 11000 0 timeout 900   6400 9500 0
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error (134) .95 40 9.1 0 false(unreach-call) 51    1100 610   0 error (1) .46 40 4.2 0 error (1) .45 40 4.1 0 false(valid-memtrack) 5.8 310 42 1 unknown 890    1200 10000   0 unknown 4.8  230 56   0 unknown 8.9  250 110   0 unknown .13  17 1.6  0 false(valid-memtrack) 6.6  29 91   0 false(valid-memtrack) .48 52 4.9 0 false(valid-memtrack) 4.0  700 53   1 unknown 420   1900 3200 0 timeout 900   5100 12000 0 timeout 900   6400 9600 0
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (5) .44 31 5.4 0 error (42) 880    3800 9700   0 error (1) .46 40 4.8 0 error (1) .47 40 4.0 0 timeout (segmentation fault) 900   11000 5600 0 unknown 890    220 9000   0 timeout 900    380 12000   0 timeout 900    400 11000   0 true .54  29 6.4  2 unknown 900    470 12000   0 true 2.2  32 27   2 timeout (timeout) 900    2900 6000   0 timeout 900   1600 12000 0 timeout 900   2200 14000 0 error (7) 360   1200 4600 0
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i error (5) .40 32 5.9 0 out of memory 420    15000 4400   0 error (1) .47 40 4.4 0 error (1) .43 40 3.9 0 timeout 900   9700 4600 0 unknown 890    490 9900   0 timeout 900    2700 12000   0 timeout 900    2700 10000   0 true 31     120 410    2 unknown 890    260 10000   0 true 2.3  38 24   2 timeout (timeout) 900    3400 11000   0 timeout 900   990 13000 0 timeout 900   1700 12000 0 timeout 900   1400 13000 0
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (5) .40 30 3.9 0 error (42) 870    5200 5500   0 error (1) .50 40 4.2 0 error (1) .44 40 4.2 0 timeout (segmentation fault) 940   11000 6200 0 unknown 890    260 9300   0 timeout 900    460 12000   0 timeout 900    380 8400   0 true 1.3   42 15    2 unknown 900    750 11000   0 timeout 900    890 7200   0 timeout (timeout) 900    3300 5500   0 timeout 900   1100 12000 0 timeout 900   3100 12000 0 error (7) 560   1700 6900 0
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (5) .47 33 4.6 0 error (42) 870    2200 4600   0 error (1) .48 40 4.3 0 error (1) .44 41 4.2 0 timeout 970   11000 4800 0 unknown 890    200 11000   0 timeout 900    570 13000   0 timeout 900    580 9300   0 true 1.5   30 19    2 unknown 900    75 11000   0 true 2.1  25 21   2 timeout (timeout) 900    3000 10000   0 timeout 900   960 9300 0 timeout 900   1900 12000 0 timeout 900   1500 14000 0
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (5) .37 30 4.0 0 error (42) 870    3100 5800   0 error (1) .49 40 4.0 0 error (1) .41 40 3.8 0 timeout 930   11000 5600 0 unknown 890    330 9800   0 timeout 900    450 13000   0 timeout 900    390 13000   0 true 1.4   37 18    2 unknown 900    430 11000   0 timeout 900    3900 6000   0 timeout (timeout) 900    3200 5400   0 timeout 900   1200 9200 0 timeout 900   3200 14000 0 timeout 900   1300 9600 0
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (5) .36 31 3.9 0 error (42) 870    3300 5000   0 error (1) .46 41 4.4 0 error (1) .45 40 3.7 0 timeout 930   11000 6200 0 unknown 890    280 11000   0 timeout 900    530 11000   0 timeout 900    480 12000   0 true 1.3   37 20    2 unknown 900    450 11000   0 timeout 900    3500 6300   0 timeout (timeout) 900    2700 6800   0 timeout 900   880 10000 0 timeout 900   2600 14000 0 timeout 900   1500 11000 0
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i out of memory 91    15000 1100   0 error (42) 870    5400 6400   0 error (1) .46 41 4.1 0 error (1) .49 40 3.9 0 timeout (segmentation fault) 930   11000 5800 0 unknown 890    170 11000   0 timeout 900    1100 10000   0 timeout 900    1100 11000   0 true 240     710 3300    2 unknown 890    200 13000   0 true 2.2  33 23   2 timeout (timeout) 900    3700 11000   0 timeout 900   1100 11000 0 timeout 900   2200 13000 0 timeout 900   1500 12000 0
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (5) .54 35 6.9 0 error (42) 870    1000 7500   0 error (1) .48 40 4.7 0 error (1) .43 40 4.4 0 timeout 940   11000 6300 0 unknown 890    160 10000   0 timeout 900    730 12000   0 timeout 900    670 8700   0 true 120     450 1700    2 unknown 900    960 11000   0 true 2.2  38 24   2 timeout (timeout) 900    2000 8300   0 timeout 900   1200 11000 0 timeout 900   2400 12000 0 timeout 900   1600 12000 0
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 900    7900 8500   0 error (42) 870    970 9600   0 error (1) .46 40 4.9 0 error (1) .42 40 3.6 0 timeout 920   11000 5600 0 unknown 890    200 9600   0 timeout 900    600 10000   0 timeout 900    600 10000   0 true .12  14 1.4  2 unknown 890    100 9900   0 true 1.8  32 19   2 timeout (timeout) 900    2700 11000   0 error (7) 250   1300 2700 0 timeout 900   2200 13000 0 timeout 900   1200 10000 0
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (5) .35 30 3.5 0 error (42) 870    700 10000   0 error (1) .45 40 4.9 0 error (1) .44 40 4.6 0 timeout (segmentation fault) 920   11000 5000 0 unknown 890    230 9500   0 timeout 900    390 12000   0 timeout 900    410 13000   0 true .90  39 14    2 unknown 900    390 12000   0 timeout 900    280 9500   0 timeout (timeout) 900    3400 5500   0 timeout 900   1600 11000 0 timeout 910   1900 12000 0 error (7) 510   1100 6600 0
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (5) .36 30 3.9 0 error (42) 870    970 7600   0 error (1) .49 41 4.9 0 error (1) .46 40 4.1 0 timeout 910   11000 4800 0 unknown 890    340 8300   0 timeout 900    210 12000   0 timeout 900    230 11000   0 true 660     1600 7300    2 unknown 900    580 13000   0 true 2.3  39 23   2 timeout (timeout) 900    3300 6700   0 timeout 900   1100 11000 0 timeout 900   2000 12000 0 error (7) 430   1500 5200 0
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i error (5) .44 32 4.0 0 out of memory 410    15000 4900   0 error (1) .45 42 4.0 0 error (1) .45 38 3.8 0 timeout 960   10000 5600 0 unknown 890    540 10000   0 timeout 900    2600 11000   0 timeout 900    2700 11000   0 true 2.1   47 28    2 unknown 900    320 10000   0 true 2.3  38 21   2 timeout (timeout) 900    3400 9900   0 timeout 900   880 9200 0 timeout 900   1800 14000 0 timeout 900   880 10000 0
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (5) .38 30 3.6 0 error (42) 880    4800 6500   0 error (1) .47 40 4.6 0 error (1) .48 41 3.8 0 timeout 940   11000 6100 0 unknown 890    240 9400   0 timeout 900    460 11000   0 timeout 900    390 11000   0 true .94  35 15    2 unknown 900    1000 10000   0 timeout 900    700 7400   0 timeout (timeout) 900    3000 7400   0 true 750   1100 9000 2 timeout 900   2900 13000 0 timeout 900   1700 11000 0
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (5) .47 32 4.9 0 error (42) 870    1900 7000   0 error (1) .49 41 4.2 0 error (1) .45 40 3.9 0 timeout (exception) 920   11000 5300 0 unknown 890    200 9100   0 timeout 900    520 10000   0 timeout 900    460 10000   0 true 17     91 240    2 unknown 890    75 11000   0 true 2.2  25 23   2 timeout (timeout) 900    3200 12000   0 timeout 900   950 9600 0 timeout 900   2500 14000 0 timeout 900   1400 13000 0
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (5) .32 29 2.8 0 error (42) 870    2100 5200   0 error (1) .49 41 4.2 0 error (1) .45 40 4.3 0 timeout (segmentation fault) 910   11000 7700 0 unknown 890    410 9700   0 timeout 900    430 11000   0 timeout 900    410 11000   0 true 6.1   51 73    2 unknown 900    510 11000   0 timeout 900    3300 6200   0 timeout (timeout) 900    2800 7000   0 timeout 900   1200 11000 0 timeout 900   1700 13000 0 timeout 900   1600 14000 0
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (5) .34 30 3.4 0 error (42) 870    2300 7100   0 error (1) .47 40 3.9 0 error (1) .47 40 3.8 0 timeout 910   11000 6300 0 unknown 890    360 9900   0 timeout 900    430 11000   0 timeout 900    420 12000   0 true .48  22 6.0  2 unknown 900    550 12000   0 timeout 900    3300 5400   0 timeout (timeout) 900    3100 5900   0 timeout 900   900 10000 0 timeout 900   1900 12000 0 timeout 900   1900 12000 0
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (5) .43 32 4.7 0 error (42) 870    2400 4700   0 error (1) .47 41 4.1 0 error (1) .45 40 4.4 0 timeout 910   11000 5600 0 unknown 890    170 12000   0 timeout 900    840 11000   0 timeout 900    900 11000   0 true 4.3   66 55    2 unknown 890    200 13000   0 true 2.2  29 24   2 timeout (timeout) 900    3700 11000   0 timeout 900   3000 7600 0 timeout 900   2200 13000 0 timeout 900   1300 12000 0
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (5) .55 33 5.6 0 error (42) 870    800 7600   0 error (1) .47 40 4.6 0 error (1) .41 40 3.6 0 timeout (segmentation fault) 900   11000 6700 0 unknown 890    190 11000   0 timeout 900    760 12000   0 timeout 900    610 11000   0 true 190     390 2900    2 unknown 900    920 11000   0 true 2.2  37 24   2 timeout (timeout) 900    2000 11000   0 timeout 900   1100 12000 0 timeout 900   2300 13000 0 timeout 900   1500 11000 0
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 900    8100 8200   0 error (42) 870    970 9000   0 error (1) .47 41 4.9 0 error (1) .47 40 4.2 0 timeout 900   11000 5600 0 unknown 890    200 9900   0 timeout 900    540 11000   0 timeout 900    520 10000   0 true .10  14 1.3  2 unknown 890    120 9600   0 true 2.1  32 22   2 timeout (timeout) 900    2600 8900   0 error (7) 300   890 3400 0 timeout 900   1900 11000 0 timeout 900   1500 13000 0
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i out of memory 34    15000 270   0 false(valid-deref) .67 42 6.5 1 error (1) .48 41 3.8 0 error (1) .45 40 4.1 0 timeout 970   11000 5900 0 false(valid-deref) 1.5  36 17   0 false(valid-deref) 1.5  32 14   1 false(valid-deref) .86 29 8.0 1 unknown .070 11 .55 0 false(valid-deref) 1.5  15 18   1 false(valid-deref) .17 24 2.4 1 false(valid-deref) .26 13 3.3 1 false(valid-deref) 73   1100 760 1 timeout 900   2000 12000 0 timeout 900   1800 15000 0
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) .37 30 3.3 1 false(valid-deref) .57 36 5.1 1 error (1) .47 40 4.3 0 error (1) .49 40 3.8 0 timeout (segmentation fault) 940   11000 5500 0 false(valid-deref) .60 29 7.2 1 false(valid-deref) .41 29 5.3 1 false(valid-deref) .82 30 7.9 1 false(valid-deref) .071 12 .76 1 false(valid-deref) 1.6  16 20   1 false(valid-deref) .13 25 2.1 1 false(valid-deref) .29 14 3.8 1 false(valid-deref) 130   760 1400 1 false(valid-deref) 510   1700 6800 1 false(valid-deref) 120   1100 1300 1
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i error (5) .30 28 2.8 0 false(valid-deref) .59 37 5.1 1 error (1) .48 41 4.1 0 error (1) .45 38 3.9 0 timeout 970   11000 6200 0 false(valid-deref) 1.4  30 18   0 false(valid-deref) .99 32 12   1 false(valid-deref) .80 29 7.9 1 unknown .071 11 .54 0 false(valid-deref) 1.4  14 19   1 false(valid-deref) .20 23 2.1 1 false(valid-deref) .26 13 3.0 1 false(valid-deref) 42   1000 450 1 false(valid-deref) 480   1300 8100 1 timeout 900   1400 15000 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
total 51 2000    62000 18000   2 51 20000   110000 170000 11 51 24 2100 220 0 51 23 2000 210 0 51 34000 410000 220000 16 51 33000   23000 370000 4 51 22000    37000 260000   -6 51 21000    49000 250000   11 51 1300    4400 18000   42 51 22000 55000 270000 11 51 7300   20000 58000 50 51 22000    77000 210000   27 51 27000 62000 290000 13 51 39000 140000 550000 4 51 36000 130000 440000 4
    correct results 2 .77 61 7.5 2 8 200   2900 2200 11 0 0 13 77 3900 630 16 4 3.2 120 37 4 7 3.7  240 40   10 8 4.0  270 39   11 22 1300    3900 16000   42 11 14 160 170 11 31 39   1100 420 50 24 57    9600 730   27 9 1800 11000 19000 13 4 1500 5300 22000 4 3 360 6300 3900 4
        correct true 0 3 190   2700 2200 6 0 0 3 18 890 150 6 0 3 .69 120 7.2 6 3 .62 120 6.4 6 20 1300    3900 16000   40 0 19 36   800 380 38 3 14    2400 180   6 4 1200 6500 12000 8 0 1 230 4900 2600 2
        correct false 2 .77 61 7.5 2 5 3.3 210 33 5 0 0 10 59 3000 490 10 4 3.2 120 37 4 4 3.0  120 32   4 5 3.4  150 32   5 2 .14 22 1.4 2 11 14 160 170 11 12 3.9 290 44 12 21 43    7200 550   21 5 570 4100 7000 5 4 1500 5300 22000 4 2 120 1400 1400 2
    correct-unconfimed results 0 0 0 0 0 10 11   300 140 0 9 5.6  270 57   0 9 4.0  260 39   0 4 2.5  88 33   0 12 66 320 810 0 12 5.4 560 53 0 3 .86 35 9.6 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 10 11   300 140 0 9 5.6  270 57   0 9 4.0  260 39   0 4 2.5  88 33   0 12 66 320 810 0 12 5.4 560 53 0 3 .86 35 9.6 0 0 0 0
    incorrect results 0 0 0 0 0 0 1 1.2  32 11   -16 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 1 1.2  32 11   -16 0 0 0 0 0 0 0 0
score (51 tasks, max score: 78) 2 11 0 0 16 4 -6 11 42 11 50 27 13 4 4
Run set 2ls.sv-comp18.MemSafety-LinkedLists cbmc.sv-comp18.MemSafety-LinkedLists cpa-bam-bnb.sv-comp18.MemSafety-LinkedLists cpa-bam-slicing.sv-comp18.MemSafety-LinkedLists cpa-seq.sv-comp18.MemSafety-LinkedLists depthk.sv-comp18.MemSafety-LinkedLists esbmc-incr.sv-comp18.MemSafety-LinkedLists esbmc-kind.sv-comp18.MemSafety-LinkedLists forester.sv-comp18.MemSafety-LinkedLists map2check.sv-comp18.MemSafety-LinkedLists predatorhp.sv-comp18.MemSafety-LinkedLists symbiotic.sv-comp18.MemSafety-LinkedLists uautomizer.sv-comp18.MemSafety-LinkedLists ukojak.sv-comp18.MemSafety-LinkedLists utaipan.sv-comp18.MemSafety-LinkedLists