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+ PredatorHP 3.14 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
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-07 04:08:42 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
Run set 2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup divine-explicit.sv-comp19_prop-memsafety.MemSafety-MemCleanup divine-smt.sv-comp19_prop-memsafety.MemSafety-MemCleanup esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup ukojak.sv-comp19_prop-memsafety.MemSafety-MemCleanup utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup
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 --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
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i false(valid-memcleanup) .39 32 4.2 1 false(valid-memcleanup) .096 7.2 1.3  0 out of memory 330     15000   3600    0 false(valid-memcleanup) 3.2 260 29 1 false(unreach-call) .16 34 2.0 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .027 4.6 .28 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .030 4.6 .16  0 error (1) .020 5.5 .050 0 unknown 84    4300 730   0 error (1) .55 44 5.5 0 false(valid-memcleanup) .16 35 1.2 1 false(valid-memcleanup) 3.4 89 48 1 false(valid-memcleanup) .25 18 2.8 1 true 16   530 140 -32 true 28 800 250 -32 true 33   650 400 -32
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i error (134) .19 28 1.7 0 false(valid-memcleanup) .34  26   5.1  0 out of memory 450     15000   5800    0 false(valid-memcleanup) 4.0 260 33 1 false(unreach-call) .24 35 3.1 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .055 4.6 .24 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .036 4.7 .19  0 error (1) .037 5.3 .083 0 timeout 900    83 11000   0 error (1) .50 42 5.3 0 false(valid-memcleanup) .61 45 6.0 1 false(valid-memcleanup) 3.9 94 48 1 false(valid-memcleanup) .25 18 2.8 1 timeout 900   1100 12000 0 timeout 900 1000 8000 0 timeout 900   1300 9700 0
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error (5) 3.8  43 46   0 false(valid-memcleanup) .51  27   6.6  0 error (134) .12  9.4 1.4  0 error (recursion) 3.6 260 35 0 unknown 900    12000 5700   0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .034 4.6 .18 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .033 4.6 .10  0 error (1) .049 5.5 .078 0 timeout 900    210 11000   0 error (1) .48 42 4.5 0 false(valid-memcleanup) 2.8  63 27   0 false(valid-memcleanup) 8.2 120 110 0 false(valid-memcleanup) .35 22 3.1 0 timeout 900   1200 11000 0 timeout 900 980 8600 0 timeout 900   1000 11000 0
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i error (134) 360    3000 3200   0 false(valid-memcleanup) .55  43   7.0  0 error (134) .12  7.7 1.0  0 false(valid-memcleanup) 3.9 270 36 1 false(unreach-call) .70 38 9.1 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .053 4.7 .16 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .034 4.5 .30  0 error (1) .028 5.5 .17  0 timeout 900    180 11000   0 error (1) .49 42 5.4 0 false(valid-memcleanup) .16 38 1.6 1 false(valid-memcleanup) 3.8 95 45 1 false(valid-memcleanup) .25 17 3.3 1 true 24   610 190 -32 true 71 870 650 -32 true 25   580 190 -32
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i timeout 900    4500 10000   0 false(valid-memcleanup) .26  19   2.9  0 error (134) .097 8.2 .88 0 false(valid-memcleanup) 3.9 260 32 1 false(unreach-call) .19 35 2.3 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .033 4.6 .18 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .036 4.8 .18  0 error (1) .021 5.4 .091 0 timeout 900    140 11000   0 error (1) .51 43 4.8 0 false(valid-memcleanup) .79 58 4.2 1 false(valid-memcleanup) 3.8 97 56 1 false(valid-memcleanup) .27 18 3.4 1 timeout 900   2200 13000 0 timeout 900 1000 7600 0 timeout 900   970 12000 0
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i error (134) 110    1400 1300   0 false(valid-memcleanup) .25  18   3.1  0 error (134) .10  7.9 .96 0 false(valid-memcleanup) 3.8 260 39 1 false(unreach-call) .47 36 6.0 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .030 4.5 .16 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .046 4.6 .17  0 error (1) .034 5.5 .067 0 timeout 900    170 11000   0 error (1) .51 42 5.2 0 false(valid-memcleanup) .54 50 4.1 1 false(valid-memcleanup) 3.7 96 46 1 false(valid-memcleanup) .26 17 2.8 1 timeout 900   2300 11000 0 timeout 900 980 8600 0 timeout 900   930 9800 0
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 13    360 160   1 false(valid-memcleanup) .16  10   1.8  0 error (134) .11  8.8 1.0  0 false(valid-memcleanup) 3.8 270 35 1 false(unreach-call) .21 35 2.5 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .031 4.6 .22 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .029 4.6 .20  0 error (1) .023 5.5 .14  0 timeout 900    170 12000   0 error (1) .53 43 4.6 0 false(valid-memcleanup) .16 37 1.6 1 false(valid-memcleanup) 3.9 130 54 1 false(valid-memcleanup) .25 17 3.0 1 timeout 900   1500 10000 0 timeout 900 970 6700 0 timeout 900   880 11000 0
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 2.5  82 30   1 false(valid-memcleanup) .12  7.6 1.2  0 error (134) .11  8.0 .99 0 false(valid-memcleanup) 3.5 260 32 1 false(unreach-call) .16 34 1.8 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .029 4.5 .19 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .030 4.6 .21  0 error (1) .024 5.4 .054 0 timeout 900    75 9400   0 error (1) .51 42 4.4 0 false(valid-memcleanup) .14 38 1.3 1 false(valid-memcleanup) 3.6 94 48 1 false(valid-memcleanup) .24 19 3.5 1 timeout 900   840 12000 0 timeout 900 1000 8500 0 timeout 900   2000 10000 0
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 9.1  200 100   1 false(valid-memcleanup) .14  8.4 1.5  0 error (134) .11  8.0 1.1  0 false(valid-memcleanup) 3.8 280 36 1 false(unreach-call) .16 34 1.8 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .055 4.6 .16 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .029 4.6 .27  0 error (1) .020 5.5 .093 0 timeout 900    170 10000   0 error (1) .51 42 5.2 0 false(valid-memcleanup) .16 34 1.4 1 false(valid-memcleanup) 3.7 94 44 1 false(valid-memcleanup) .24 18 2.8 1 timeout 900   2100 8800 0 timeout 900 1000 7900 0 timeout 900   960 11000 0
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i error (134) 11    270 98   0 false(valid-memcleanup) .38  16   5.5  0 error (134) .12  9.6 1.6  0 false(valid-memcleanup) 4.2 270 39 1 false(unreach-call) 1.3  37 16   0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .032 4.6 .18 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .054 4.6 .17  0 error (1) .044 5.4 .10  0 timeout 900    170 12000   0 error (1) .49 43 5.3 0 false(valid-memcleanup) .39 49 1.4 1 false(valid-memcleanup) 4.1 100 57 1 false(valid-memcleanup) .26 18 2.4 1 timeout 900   960 9400 0 timeout 900 960 8000 0 timeout 900   960 10000 0
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 20    380 200   0 false(valid-memcleanup) .19  13   2.3  0 error (134) .12  8.6 .98 0 false(valid-memcleanup) 3.5 250 32 1 false(unreach-call) .18 35 2.0 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .031 4.5 .25 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .057 4.6 .18  0 error (1) .026 5.5 .18  0 timeout 900    170 10000   0 error (1) .54 43 5.4 0 false(valid-memcleanup) .19 36 1.3 1 false(valid-memcleanup) 3.7 95 51 1 false(valid-memcleanup) .25 18 3.2 1 timeout 900   1100 11000 0 timeout 900 1000 6900 0 timeout 900   2200 11000 0
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i error (134) 32    410 320   0 false(valid-memcleanup) .18  12   2.0  0 error (134) .12  8.9 1.5  0 false(valid-memcleanup) 4.2 270 34 1 false(unreach-call) .51 36 5.8 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .026 4.8 .26 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .033 4.7 .19  0 error (1) .047 5.3 .14  0 timeout 900    180 11000   0 error (1) .51 42 5.1 0 false(valid-memcleanup) .44 37 4.6 1 false(valid-memcleanup) 4.0 100 39 1 false(valid-memcleanup) .24 18 2.9 1 timeout 900   2300 9800 0 timeout 900 990 7100 0 timeout 900   970 12000 0
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1.2  57 15   1 false(valid-memcleanup) .18  12   1.9  0 error (134) .11  7.9 1.1  0 false(valid-memcleanup) 3.4 250 32 1 false(unreach-call) .19 34 2.2 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .034 4.6 .17 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .029 4.6 .19  0 error (1) .021 5.4 .12  0 timeout 900    170 10000   0 error (1) .55 42 5.4 0 false(valid-memcleanup) .16 37 1.5 1 false(valid-memcleanup) 3.6 95 46 1 false(valid-memcleanup) .23 17 3.0 1 timeout 900   2600 12000 0 timeout 900 960 6900 0 timeout 900   1000 10000 0
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i error (134) 41    720 390   0 false(valid-memcleanup) .22  14   2.0  0 error (134) .10  8.4 .96 0 false(valid-memcleanup) 4.1 280 33 1 false(unreach-call) .65 36 9.9 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .043 4.6 .13 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .029 4.6 .17  0 error (1) .043 5.3 .13  0 timeout 900    160 10000   0 error (1) .50 43 4.7 0 false(valid-memcleanup) .18 37 1.3 1 false(valid-memcleanup) 3.8 97 50 1 false(valid-memcleanup) .27 17 4.1 1 timeout 900   2200 12000 0 timeout 900 870 8900 0 timeout 900   970 12000 0
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1.5  53 18   1 false(valid-memcleanup) .14  7.1 1.1  0 error (134) .092 8.0 1.1  0 false(valid-memcleanup) 3.4 260 29 1 false(unreach-call) .17 34 1.8 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .027 4.6 .19 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .048 4.5 .14  0 error (1) .028 5.3 .17  0 timeout 900    75 9300   0 error (1) .49 42 5.4 0 false(valid-memcleanup) .17 33 1.3 1 false(valid-memcleanup) 3.6 98 42 1 false(valid-memcleanup) .23 17 3.0 1 timeout 900   750 10000 0 timeout 900 1000 7700 0 timeout 900   2100 10000 0
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 5.1  110 54   1 false(valid-memcleanup) .14  7.9 1.4  0 error (134) .099 8.0 1.1  0 false(valid-memcleanup) 3.5 260 30 1 false(unreach-call) .19 35 1.7 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .030 4.6 .13 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .029 4.6 .18  0 error (1) .021 5.4 .083 0 timeout 900    170 9400   0 error (1) .48 43 4.9 0 false(valid-memcleanup) .35 49 1.3 1 false(valid-memcleanup) 3.7 93 43 1 false(valid-memcleanup) .23 18 2.6 1 timeout 900   2200 11000 0 timeout 900 1000 7400 0 timeout 900   820 10000 0
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i error (134) 5.5  150 63   0 false(valid-memcleanup) .35  15   4.0  0 error (134) .15  8.8 1.2  0 false(valid-memcleanup) 4.1 270 33 1 false(unreach-call) 1.3  37 17   0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .030 4.7 .21 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .027 4.6 .21  0 error (1) .024 5.4 .090 0 timeout 900    180 11000   0 error (1) .54 42 5.0 0 false(valid-memcleanup) .18 35 1.4 1 false(valid-memcleanup) 4.1 100 50 1 false(valid-memcleanup) .26 18 3.2 1 timeout 900   2000 10000 0 timeout 900 1000 7200 0 timeout 900   820 11000 0
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i error (5) 23    580 260   0 false(valid-memcleanup) .20  12   1.7  0 error (134) .092 8.5 .88 0 false(valid-memcleanup) 4.1 260 39 1 false(unreach-call) .53 36 7.0 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .049 4.6 .14 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .032 4.6 .22  0 error (1) .027 5.3 .085 0 timeout 900    190 11000   0 error (1) .52 44 4.8 0 false(valid-memcleanup) .37 49 1.9 1 false(valid-memcleanup) 3.8 96 58 1 false(valid-memcleanup) .30 17 2.5 1 timeout 900   2200 9800 0 timeout 900 1100 7800 0 timeout 900   1000 10000 0
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 2.6  92 35   0 false(valid-memcleanup) .16  11   1.7  0 error (134) .095 8.2 .82 0 false(valid-memcleanup) 3.6 250 33 1 false(unreach-call) .18 34 1.9 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .036 4.8 .22 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .030 4.6 .21  0 error (1) .020 5.4 .16  0 timeout 900    180 9900   0 error (1) .51 43 4.7 0 false(valid-memcleanup) .15 34 1.5 1 false(valid-memcleanup) 3.7 97 50 1 false(valid-memcleanup) .26 18 3.2 1 timeout 900   2400 9300 0 timeout 900 1000 7500 0 timeout 900   1400 11000 0
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i error (134) 16    250 180   0 false(valid-memcleanup) .16  11   1.5  0 error (134) .11  8.6 1.1  0 false(valid-memcleanup) 10   480 86 1 false(unreach-call) .49 35 5.9 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .033 4.6 .24 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .044 4.6 .20  0 error (1) .021 5.5 .093 0 timeout 900    190 12000   0 error (1) .49 42 4.6 0 false(valid-memcleanup) .50 49 3.5 1 false(valid-memcleanup) 4.4 110 66 0 false(valid-memcleanup) .26 18 3.5 1 timeout 900   790 11000 0 timeout 900 1000 9000 0 timeout 900   1000 11000 0
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) .58 32 7.7 1 false(valid-memcleanup) .14  10   1.6  0 error (134) .087 7.8 1.1  0 false(valid-memcleanup) 3.4 260 33 1 false(unreach-call) .18 34 2.0 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .045 4.7 .20 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .055 4.6 .15  0 error (1) .020 5.3 .12  0 timeout 900    190 10000   0 error (1) .50 42 4.4 0 false(valid-memcleanup) .38 49 1.2 1 false(valid-memcleanup) 3.6 120 43 1 false(valid-memcleanup) .22 18 2.4 1 timeout 900   2400 11000 0 timeout 900 850 8300 0 timeout 900   720 12000 0
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i error (134) .82 34 9.8 0 false(valid-memcleanup) .10  7.7 1.2  0 out of memory 570     15000   7100    0 false(valid-memcleanup) 3.5 260 32 1 false(unreach-call) .48 35 4.8 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .028 4.7 .41 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .036 4.5 .20  0 error (1) .034 5.5 .11  0 timeout 900    180 9500   0 error (1) .51 44 5.0 0 false(valid-memcleanup) .16 34 1.5 0 false(valid-memcleanup) 3.5 89 39 1 false(valid-memcleanup) .26 18 3.3 1 true 25   740 220 -32 true 750 1000 5900 -32 true 47   640 480 -32
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 4.0  85 44   0 false(valid-memcleanup) .15  10   1.6  0 error (134) .090 7.9 .50 0 false(valid-memcleanup) 3.8 260 34 1 false(unreach-call) .68 36 8.6 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .032 4.7 .15 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .031 4.7 .20  0 error (1) .027 5.4 .15  0 false(valid-memcleanup) .45 83 5.6 0 error (1) .52 44 5.1 0 false(valid-memcleanup) .21 35 1.1 0 false(valid-memcleanup) 3.6 120 40 1 false(valid-memcleanup) .26 18 3.6 1 false(valid-memtrack) 12   580 110 0 false(valid-memtrack) 15 520 140 0 false(valid-memtrack) 13   580 110 0
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) .64 31 8.0 1 false(valid-memcleanup) .097 7.2 1.1  0 error (134) .069 7.5 .48 0 false(valid-memcleanup) 3.4 250 32 1 false(unreach-call) .51 35 5.7 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .038 4.6 .30 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .044 4.7 .20  0 error (1) .020 5.5 .11  0 false(valid-memcleanup) .46 82 6.6 0 error (1) .51 42 5.3 0 false(valid-memcleanup) .16 35 1.2 1 false(valid-memcleanup) 3.4 89 42 1 false(valid-memcleanup) .26 18 3.2 1 false(valid-memtrack) 10   390 79 0 false(valid-memtrack) 13 580 120 0 false(valid-memtrack) 9.8 390 71 0
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) .33 29 4.0 0 false(valid-memcleanup) .20  8.4 2.1  0 error (134) .20  16   2.2  0 false(valid-memcleanup) 3.8 270 36 1 false(unreach-call) 1.0  36 14   0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .031 4.6 .19 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .034 4.6 .19  0 error (1) .020 5.4 .063 0 unknown 40    4500 460   0 error (1) .52 42 4.9 0 false(valid-memcleanup) .18 37 1.5 1 false(valid-memcleanup) 3.5 84 45 1 false(valid-memcleanup) .19 16 2.1 1 true 480   870 6200 -32 true 380 1100 3200 -32 timeout 910   14000 5300 0
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) .64 35 10   1 false(valid-memcleanup) .24  10   3.1  0 false(valid-memcleanup) 430     2200   5900    0 false(valid-memcleanup) 3.9 260 38 1 true 1.4  37 18   -32 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .060 4.7 .19 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .030 4.6 .18  0 error (1) .022 5.4 .050 0 timeout 900    75 9600   0 error (1) .50 42 4.9 0 false(valid-memcleanup) .17 35 1.5 0 false(valid-memcleanup) 3.9 94 47 1 false(valid-memcleanup) .20 16 2.2 1 timeout 900   850 10000 0 timeout 900 980 9400 0 timeout 900   2500 7600 0
list-properties/simple_false-unreach-call_false-valid-memcleanup.i error (134) .40 30 4.1 0 false(valid-memcleanup) .090 7.1 .79 0 false(valid-memcleanup) .14  7.2 1.2  0 false(valid-memcleanup) 3.4 250 32 1 false(unreach-call) .47 35 6.0 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .035 4.6 .29 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .049 4.7 .20  0 error (1) .022 5.5 .097 0 false(valid-memcleanup) .44 83 5.5 0 error (1) .49 42 4.9 0 false(valid-memcleanup) .33 49 1.4 0 false(valid-memcleanup) 3.4 85 50 1 false(valid-memcleanup) .25 19 2.8 1 false(valid-memtrack) 13   510 100 0 false(valid-memtrack) 14 560 110 0 false(valid-memtrack) 14   590 120 0
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 2.3  74 27   1 false(valid-memcleanup) .12  9.1 1.2  0 false(valid-memcleanup) .096 8.0 .88 0 false(valid-memcleanup) 3.7 260 32 1 false(unreach-call) .49 36 6.1 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .026 4.6 .22 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .025 4.6 .26  0 error (1) .024 5.4 .093 0 false(valid-memcleanup) .46 83 6.5 0 error (1) .51 42 4.4 0 false(valid-memcleanup) .28 50 1.8 0 false(valid-memcleanup) 3.5 98 40 1 false(valid-memcleanup) .25 18 2.8 1 false(valid-memtrack) 9.8 390 73 0 false(valid-memtrack) 12 520 94 0 false(valid-memtrack) 9.6 370 70 0
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i error (134) 3.7  77 36   0 false(valid-memcleanup) .26  12   3.2  0 error (42) 880     7100   9900    0 false(valid-memcleanup) 6.8 300 56 1 false(unreach-call) 2.2  39 28   0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .034 4.6 .27 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .045 4.6 .18  0 error (1) .035 5.5 .087 0 timeout 900    2100 7000   0 error (1) .50 42 4.7 0 false(valid-memcleanup) .17 35 1.3 1 false(valid-memcleanup) 4.3 94 54 1 false(valid-memcleanup) .27 17 2.7 1 timeout 900   2300 11000 0 timeout 900 1100 11000 0 timeout 900   1400 11000 0
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i out of memory 150    15000 1300   0 false(valid-memcleanup) .21  10   2.1  0 error (42) 870     7500   13000    0 false(valid-memcleanup) 4.4 290 35 1 false(unreach-call) 1.2  36 14   0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .037 4.6 .12 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .031 4.6 .086 0 error (1) .049 5.4 .13  0 unknown 19    83 290   0 error (1) .52 43 5.0 0 false(valid-memcleanup) .22 37 2.2 1 false(valid-memcleanup) 3.5 86 43 0 false(valid-memcleanup) .30 18 4.1 1 timeout 900   2200 12000 0 timeout 900 930 6100 0 timeout 910   12000 11000 0
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i out of memory 260    15000 2600   0 false(valid-memcleanup) .77  50   8.2  0 out of memory 580     15000   7200    0 false(valid-memcleanup) 4.5 290 38 1 false(unreach-call) 1.3  39 20   0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .028 4.6 .23 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .054 4.6 .12  0 error (1) .038 5.3 .086 0 timeout 900    570 10000   0 error (1) .53 42 5.3 0 false(valid-memcleanup) .46 51 3.5 1 false(valid-memcleanup) 3.6 91 44 0 false(valid-memcleanup) .31 18 3.5 1 timeout 900   1300 11000 0 timeout 900 940 7400 0 timeout 900   1700 12000 0
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i timeout 900    4600 11000   0 false(valid-memcleanup) 16     640   200    0 error (134) .087 8.9 .64 0 false(valid-memcleanup) 7.2 370 59 1 false(unreach-call) 68    1200 730   0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .026 4.6 .25 0 error - missing or conflicting properties 0, 0, 0, 0, 0 at ./divine-svc line 64. .035 4.7 .17  0 error (1) .047 5.4 .090 0 timeout 900    120 13000   0 error (1) .51 41 4.8 0 false(valid-memcleanup) .52 36 5.0 1 false(valid-memcleanup) 7.4 130 88 1 false(valid-memcleanup) .32 18 3.5 1 timeout 900   970 11000 0 timeout 900 980 9000 0 timeout 900   1000 11000 0
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 32 2900 48000 32000 11 32 23 1100 280 0 32 4100 77000 52000 0 32 130 8800 1200 31 32 980   14000 6700 -32 32 1.1 150 6.7 0 32 1.2 150 6.0 0 32 .94 170 3.4 0 32 23000   15000 260000 0 32 16 1400 160 0 32 12   1300 93 26 32 130 3200 1600 28 32 8.2  570 97   31 32 22000 45000 270000 -128 32 23000 30000 200000 -128 32 23000 58000 260000 -96
    correct results 11 37 1100 430 11 0 0 31 130 8500 1100 31 0 0 0 0 0 0 26 7.9 1100 58 26 28 110 2800 1400 28 31 7.9  550 94   31 0 0 0
        correct true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct false 11 37 1100 430 11 0 0 31 130 8500 1100 31 0 0 0 0 0 0 26 7.9 1100 58 26 28 110 2800 1400 28 31 7.9  550 94   31 0 0 0
    correct-unconfimed results 4 27 590 280 0 32 23 1100 280 0 3 430 2200 5900 0 0 0 0 0 0 4 1.8 330 24 0 0 6 3.9 270 34 0 4 20 410 260 0 1 .35 22 3.1 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 4 27 590 280 0 32 23 1100 280 0 3 430 2200 5900 0 0 0 0 0 0 4 1.8 330 24 0 0 6 3.9 270 34 0 4 20 410 260 0 1 .35 22 3.1 0 0 0 0
    incorrect results 0 0 0 0 1 1.4 37 18 -32 0 0 0 0 0 0 0 0 4 550 2700 6800 -128 4 1200 3800 10000 -128 3 110 1900 1100 -96
        incorrect true 0 0 0 0 1 1.4 37 18 -32 0 0 0 0 0 0 0 0 4 550 2700 6800 -128 4 1200 3800 10000 -128 3 110 1900 1100 -96
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (32 tasks, max score: 32) 11 0 0 31 -32 0 0 0 0 0 26 28 31 -128 -128 -96
Run set 2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup divine-explicit.sv-comp19_prop-memsafety.MemSafety-MemCleanup divine-smt.sv-comp19_prop-memsafety.MemSafety-MemCleanup esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup ukojak.sv-comp19_prop-memsafety.MemSafety-MemCleanup utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup