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-Arrays cbmc.sv-comp19_prop-memsafety.MemSafety-Arrays cbmc-path.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq.sv-comp19_prop-memsafety.MemSafety-Arrays depthk.sv-comp19_prop-memsafety.MemSafety-Arrays divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays divine-smt.sv-comp19_prop-memsafety.MemSafety-Arrays esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Arrays map2check.sv-comp19_prop-memsafety.MemSafety-Arrays pesco.sv-comp19_prop-memsafety.MemSafety-Arrays predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays smack.sv-comp19_prop-memsafety.MemSafety-Arrays symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer.sv-comp19_prop-memsafety.MemSafety-Arrays ukojak.sv-comp19_prop-memsafety.MemSafety-Arrays utaipan.sv-comp19_prop-memsafety.MemSafety-Arrays
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
array-memsafety/add_last_unsafe_false-valid-deref.i error (134) .17  26 1.5  0 false(valid-deref) .11  7.1 .77 1 error (134) .056 8.7 .55 0 error 3.7 280 32 0 false(valid-deref) .22 34 2.2 1 unknown 8.5 450 100 0 unknown 1.6 200 22 0 false(valid-deref) .14  27 1.7  1 false(valid-deref) .47 83 5.4 1 error 3.6 280 31 0 false(valid-deref) .17 36 1.1 1 disqualified 3.3 82 38 0 false(valid-deref) .21 18 2.4 1 false(valid-deref) 8.3 340 66 1 false(valid-deref) 9.0 370 70 1 false(valid-deref) 9.5 370 77 1
array-memsafety/bubblesort_unsafe_false-valid-deref.i error (134) .090 24 .68 0 false(valid-deref) .11  7.2 .37 1 false(valid-deref) .11  7.4 .44 1 timeout (segmentation fault) 960   12000 9700 0 false(valid-deref) .14 33 1.7 1 unknown 8.2 430 96 0 false(valid-deref) 8.8 430 110 1 false(valid-deref) .084 26 .81 1 false(valid-deref) .48 83 5.2 1 timeout (segmentation fault) 920   12000 8700 0 false(valid-deref) .15 34 1.5 1 disqualified 3.3 86 44 0 error(unknown, verification-finished) .18 19 2.1 0 false(valid-deref) 6.8 330 58 1 false(valid-deref) 9.1 370 68 1 false(valid-deref) 8.3 370 57 1
array-memsafety/count_down_unsafe_false-valid-deref.i error (134) .18  26 1.4  0 false(valid-deref) .11  7.5 .99 1 error (134) .061 8.8 .58 0 error 3.9 280 36 0 false(valid-deref) .22 34 2.2 1 unknown 8.4 450 100 0 unknown 1.6 200 19 0 false(valid-deref) .12  30 2.0  1 false(valid-deref) .47 83 5.8 1 error 3.6 270 32 0 false(valid-deref) .16 35 1.6 1 disqualified 3.3 83 41 0 false(valid-deref) .21 17 2.9 1 false(valid-deref) 9.5 380 65 1 false(valid-deref) 8.9 360 68 1 false(valid-deref) 9.4 380 72 1
array-memsafety/cstrcat_unsafe_false-valid-deref.i error (134) .083 24 .66 0 false(valid-deref) .064 7.1 .58 1 false(valid-deref) .098 6.9 .29 1 false(valid-deref) 2.7 250 23 1 false(valid-deref) .14 33 1.7 1 false(valid-deref) 8.3 430 110 1 false(valid-deref) 8.3 430 110 1 false(valid-deref) .086 26 1.2  1 false(valid-deref) .52 83 5.9 1 false(valid-deref) 2.7 250 23 1 false(valid-deref) .15 33 2.0 1 disqualified 3.3 87 40 0 error(unknown, verification-finished) .15 15 1.7 0 false(valid-deref) 7.7 360 60 1 false(valid-deref) 7.9 370 68 1 false(valid-deref) 7.6 350 57 1
array-memsafety/cstrchr_unsafe_false-valid-deref.i error (134) .17  26 1.4  0 false(valid-deref) .078 7.5 .95 1 error (134) .069 8.7 .58 0 error 3.6 280 34 0 false(valid-deref) .20 34 2.3 1 unknown 8.3 450 120 0 unknown 1.6 200 22 0 false(valid-deref) .13  27 1.9  1 false(valid-deref) .48 83 5.1 1 error 3.7 280 34 0 false(valid-deref) .27 48 1.7 1 disqualified 3.4 85 48 0 false(valid-deref) .95 17 12   1 false(valid-deref) 14   570 130 1 false(valid-deref) 11   460 86 1 false(valid-deref) 16   590 130 1
array-memsafety/cstrlen_unsafe_false-valid-deref.i error (134) .17  26 1.5  0 false(valid-deref) .091 7.7 .60 1 error (134) .10  7.1 .49 0 error 3.8 280 33 0 false(valid-deref) .55 36 6.6 1 unknown 8.4 440 110 0 unknown 1.6 200 23 0 false(valid-deref) .17  27 1.9  1 false(valid-deref) 39    1100 450   1 error 3.7 280 34 0 false(valid-deref) .14 36 1.4 1 disqualified 3.4 85 45 0 false(valid-deref) .31 18 3.1 0 false(valid-deref) 11   440 87 1 false(valid-deref) 9.4 360 76 1 false(valid-deref) 11   430 81 1
array-memsafety/cstrncat_unsafe_false-valid-deref.i error (134) .089 24 .83 0 false(valid-deref) .067 7.1 .61 1 false(valid-deref) .078 6.8 .31 1 false(valid-deref) 2.6 250 27 1 false(valid-deref) .15 33 1.6 1 unknown 8.1 430 110 0 false(valid-deref) 8.3 430 100 1 false(valid-deref) .084 26 .97 1 false(valid-deref) .44 83 6.4 1 false(valid-deref) 2.9 250 26 1 false(valid-deref) .26 48 1.5 1 disqualified 3.2 82 38 0 error(unknown, verification-finished) .17 16 1.7 0 false(valid-deref) 7.8 360 63 1 false(valid-deref) 8.8 370 72 1 false(valid-deref) 7.9 370 62 1
array-memsafety/cstrncpy_unsafe_false-valid-deref.i error (134) .084 24 .74 0 false(valid-deref) .068 8.0 .72 1 false(valid-deref) .059 7.5 .51 1 false(valid-deref) 2.8 250 27 1 false(valid-deref) .14 33 1.6 1 unknown 8.4 430 110 0 false(valid-deref) 8.5 430 93 1 false(valid-deref) .084 26 .78 1 false(valid-deref) .46 83 5.4 1 false(valid-deref) 2.8 250 25 1 false(valid-deref) .16 33 1.4 1 disqualified 3.3 83 46 0 error(unknown, verification-finished) .17 18 2.4 0 false(valid-deref) 7.3 350 63 1 false(valid-deref) 7.7 350 59 1 false(valid-deref) 7.3 350 58 1
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i error (134) .17  26 1.7  0 false(valid-deref) .10  7.5 1.0  0 error (134) .073 7.4 .59 0 error 3.5 250 32 0 false(valid-deref) .22 34 2.6 1 unknown 8.5 440 120 0 unknown 1.6 200 20 0 false(valid-deref) .18  27 1.9  1 false(valid-deref) .47 83 5.3 1 error 3.7 280 31 0 false(valid-deref) .27 49 2.0 1 disqualified 3.7 88 53 0 false(valid-deref) .76 18 10   1 false(valid-deref) 23   570 240 1 false(valid-deref) 13   560 110 1 false(valid-deref) 23   520 260 1
array-memsafety/diff_usafe_false-valid-deref.i error (134) .084 24 .71 0 false(valid-deref) .074 7.3 .67 1 false(valid-deref) .075 7.2 .56 1 segmentation fault 840   9300 7500 0 false(valid-deref) .14 33 1.6 1 unknown 8.1 430 97 0 false(valid-deref) 8.5 430 120 1 false(valid-deref) .086 26 .86 1 false(valid-deref) .45 83 5.9 1 timeout (exception) 900   9900 11000 0 false(valid-deref) .17 36 1.4 1 disqualified 3.3 84 39 0 error(unknown, verification-finished) .19 18 2.0 0 false(valid-deref) 8.2 370 67 1 false(valid-deref) 8.6 360 65 1 false(valid-deref) 8.0 370 70 1
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i error (134) .17  26 1.7  0 false(valid-deref) .65  74   8.2  1 false(valid-deref) .086 8.3 .96 1 error 4.0 290 35 0 false(valid-deref) .28 34 3.9 1 unknown 8.4 440 110 0 unknown 1.6 200 20 0 false(valid-deref) .23  27 2.4  1 false(valid-deref) .47 83 6.4 1 error 3.7 280 36 0 false(valid-deref) .23 49 1.9 1 disqualified 3.5 89 39 0 false(valid-deref) .25 18 4.3 1 false(valid-deref) 10   390 70 1 false(valid-deref) 10   370 79 1 false(valid-deref) 9.6 380 81 1
array-memsafety/lis_unsafe_false-valid-deref.i error (134) .18  26 1.5  0 false(valid-deref) .11  7.5 .94 1 false(valid-deref) .11  7.3 .88 1 error 3.7 280 34 0 false(valid-deref) .22 34 2.6 1 unknown 8.3 450 120 0 unknown 1.6 200 21 0 false(valid-deref) .16  27 2.1  1 timeout 900    1700 9200   0 error 3.6 280 33 0 unknown .15 36 1.3 0 disqualified 3.6 120 54 0 false(valid-deref) .40 18 5.3 1 false(valid-deref) 12   480 110 1 false(valid-deref) 27   810 250 1 false(valid-deref) 14   510 120 1
array-memsafety/mult_array_unsafe_false-valid-deref.i error (134) .17  26 1.4  0 false(valid-deref) .14  15   1.5  1 error (134) .064 7.4 .55 0 error 3.6 280 29 0 false(valid-deref) .40 38 4.9 1 unknown 8.4 450 110 0 unknown 1.6 200 21 0 false(valid-deref) .20  29 2.4  1 false(valid-deref) .48 83 5.2 1 error 3.7 280 33 0 out of memory (unknown) 19    15000 200   0 disqualified 3.4 86 42 0 false(valid-deref) .31 21 3.8 1 false(valid-deref) 9.6 380 72 1 false(valid-deref) 8.7 360 66 1 false(valid-deref) 9.9 380 78 1
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i error (134) .16  26 1.5  0 false(valid-deref) .28  29   3.0  1 false(valid-deref) .11  7.5 .64 1 error 3.4 250 32 0 false(valid-deref) .64 36 8.0 1 unknown 8.5 450 91 0 unknown 1.6 200 21 0 false(valid-deref) .23  27 2.5  1 false(valid-deref) .46 82 4.9 1 error 3.6 270 30 0 false(valid-deref) .16 36 2.7 0 disqualified 3.4 87 43 0 false(valid-deref) .54 18 8.0 1 false(valid-deref) 11   400 76 1 false(valid-deref) 12   480 98 1 false(valid-deref) 9.9 390 81 1
array-memsafety/reverse_array_unsafe_false-valid-deref.i error (134) .16  26 1.9  0 false(valid-deref) .24  29   2.8  1 error (134) .062 8.3 .61 0 error 3.8 280 30 0 false(valid-deref) .20 34 2.3 1 unknown 8.3 450 120 0 unknown 1.6 200 21 0 false(valid-deref) .16  27 1.5  1 false(valid-deref) .44 83 5.6 1 error 3.6 250 34 0 false(valid-deref) .15 34 1.5 1 disqualified 3.3 87 47 0 false(valid-deref) .23 18 3.0 1 false(valid-deref) 10   370 75 1 false(valid-deref) 8.5 340 63 1 false(valid-deref) 9.9 390 78 1
array-memsafety/selectionsort_unsafe_false-valid-deref.i error (134) .086 24 .70 0 false(valid-deref) .065 7.1 .66 1 false(valid-deref) .058 7.0 .53 1 segmentation fault 630   7600 6700 0 false(valid-deref) .14 33 2.0 1 unknown 8.1 430 98 0 false(valid-deref) 8.7 430 110 1 false(valid-deref) .086 26 .87 1 false(valid-deref) .48 83 5.1 1 timeout 900   8900 8300 0 false(valid-deref) .16 35 1.5 1 disqualified 3.3 84 45 0 error(unknown, verification-finished) .19 17 1.9 0 false(valid-deref) 8.0 360 60 1 false(valid-deref) 8.1 330 65 1 false(valid-deref) 7.1 330 56 1
array-memsafety/stroeder1_unsafe_false-valid-deref.i error (134) .089 24 .76 0 false(valid-deref) .077 7.4 .33 1 false(valid-deref) .069 6.7 .30 1 false(valid-deref) 2.8 250 27 1 false(valid-deref) .14 34 1.9 1 unknown 8.2 430 120 0 error - divine failed with signal 11 1.6 200 20 0 false(valid-deref) .078 26 1.1  1 false(valid-deref) .45 82 5.5 1 false(valid-deref) 2.8 250 25 1 false(valid-deref) .17 35 1.4 1 disqualified 3.3 83 34 0 error(unknown, verification-finished) .18 18 2.3 0 false(valid-deref) 7.9 360 69 1 false(valid-deref) 7.5 350 63 1 false(valid-deref) 7.8 350 56 1
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.5  0 out of memory 710     13000   6100    0 error (42) 880     830   10000    0 error 3.6 280 35 0 unknown 900    190 12000   0 unknown 8.5 440 120 0 unknown 1.6 200 23 0 timeout 900     460 12000    0 true 12    74 170   2 error 3.8 280 30 0 out of memory (unknown) 19    15000 210   0 disqualified 760   370 7300 0 true .22 19 2.4 2 timeout 900   1000 7700 0 timeout 900   860 7700 0 timeout 900   2500 14000 0
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.7  0 out of memory 830     14000   8900    0 error (42) 870     3800   12000    0 error 3.6 280 31 0 unknown 900    260 12000   0 unknown 8.3 450 90 0 unknown 1.5 200 22 0 timeout 900     660 12000    0 true 230    75 3200   2 error 3.6 260 32 0 out of memory (unknown) 19    15000 210   0 disqualified 760   550 7600 0 timeout (verification) 900    1400 12000   0 true 11   450 77 2 true 15   660 130 2 true 10   450 94 2
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i error (134) .15  26 1.9  0 error (134) 270     13000   3000    0 error (42) 880     11000   12000    0 error 3.6 280 31 0 unknown 900    240 13000   0 unknown 8.4 450 100 0 unknown 1.6 200 18 0 timeout 900     530 12000    0 timeout 900    75 9400   0 error 3.6 270 32 0 out of memory (unknown) 19    15000 210   0 disqualified 760   670 9300 0 timeout (verification) 900    6400 13000   0 true 11   490 92 2 true 15   570 130 2 true 12   500 93 2
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.8  0 out of memory 190     14000   2100    0 error (42) 880     5600   12000    0 error 3.8 280 31 0 unknown 900    770 11000   0 unknown 8.2 450 91 0 unknown 1.6 200 22 0 timeout 900     1200 11000    0 true 350    75 4200   2 error 3.7 280 33 0 out of memory (unknown) 19    15000 200   0 disqualified 760   460 10000 0 timeout (verification) 900    1300 10000   0 true 12   500 99 2 true 64   870 750 2 true 13   530 110 2
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.7  0 out of memory 280     13000   3200    0 out of memory 840     15000   13000    0 error 3.6 280 31 0 unknown 900    1100 9800   0 unknown 8.3 450 120 0 unknown 1.6 200 26 0 timeout 900     1300 10000    0 true 18    75 300   2 error 3.3 250 32 0 out of memory (unknown) 19    15000 220   0 disqualified 760   670 5900 0 timeout (verification) 900    130 12000   0 true 11   460 87 2 true 22   730 170 2 true 11   410 89 2
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.6  0 out of memory 850     14000   10000    0 error (42) 880     9000   14000    0 error 3.6 270 31 0 unknown 900    220 13000   0 unknown 8.3 440 100 0 unknown 1.5 200 22 0 timeout 900     510 13000    0 timeout 900    650 8800   0 error 3.5 270 36 0 out of memory (unknown) 19    15000 200   0 disqualified 760   230 9200 0 timeout (verification) 900    470 7500   0 true 13   520 110 2 true 34   860 380 2 true 14   560 120 2
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.5  0 out of memory 110     14000   1100    0 error (134) .082 8.3 .48 0 error 3.5 260 31 0 unknown 300    70 4200   0 unknown 8.4 450 120 0 unknown 1.6 200 20 0 timeout 900     650 13000    0 timeout 900    180 12000   0 error 3.8 260 35 0 unknown .32 49 2.4 0 disqualified 760   330 7900 0 timeout (verification) 900    320 13000   0 timeout 900   2600 13000 0 timeout 900   870 8000 0 timeout 900   8200 5400 0
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.6  0 error (42) 880     2800   11000    0 error (134) .057 7.9 1.0  0 error 3.5 270 32 0 unknown 130    42 1700   0 unknown 8.3 440 100 0 unknown 1.6 200 21 0 timeout 900     800 10000    0 true 76    90 1100   2 error 3.7 280 32 0 unknown .17 35 1.3 0 disqualified 760   220 8200 0 timeout (verification) 900    350 11000   0 true 13   500 100 2 true 25   610 250 2 true 15   610 130 2
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.3  0 error (42) 880     3300   11000    0 error (134) .075 8.5 .57 0 error 3.5 250 35 0 unknown 230    75 3300   0 unknown 8.4 450 100 0 unknown 1.6 200 21 0 timeout 900     580 12000    0 true 34    75 440   2 error 3.8 280 30 0 unknown .17 33 2.3 0 disqualified 760   280 9700 0 timeout (verification) 900    470 11000   0 true 24   740 230 2 timeout 900   950 10000 0 true 35   780 330 2
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.8  0 out of memory 120     13000   1200    0 error (134) .060 8.8 .57 0 error 3.4 250 33 0 unknown 150    46 2300   0 unknown 8.3 450 100 0 unknown 1.6 200 23 0 timeout 900     1400 11000    0 true 160    89 2200   2 error 3.7 280 31 0 unknown .16 32 1.5 0 disqualified 760   250 11000 0 timeout (verification) 900    300 13000   0 true 19   540 160 2 true 100   730 1100 2 true 19   650 160 2
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.3  0 error (42) 880     4700   10000    0 error (134) .094 8.0 .56 0 error 3.8 280 37 0 unknown 900    190 12000   0 unknown 8.4 450 110 0 unknown 1.6 200 24 0 timeout 900     670 11000    0 true 30    75 380   2 error 3.6 280 32 0 unknown .47 49 1.3 0 disqualified 760   730 6900 0 timeout (verification) 900    380 13000   0 true 23   570 220 2 timeout 900   970 9200 0 true 160   760 2300 2
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.3  0 error (42) 880     3400   5900    0 error (134) .062 8.3 .51 0 error 3.7 270 35 0 unknown 66    42 840   0 unknown 8.3 450 99 0 unknown 1.6 200 20 0 timeout 900     780 12000    0 true 16    75 200   2 error 3.6 280 31 0 unknown .36 49 1.4 0 disqualified 760   210 11000 0 timeout (verification) 900    390 11000   0 true 13   520 110 2 true 20   710 160 2 true 14   580 120 2
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.9  0 out of memory 240     14000   2500    0 error (134) .11  7.6 .57 0 error 3.8 280 37 0 unknown 390    62 5200   0 unknown 8.3 450 81 0 unknown 1.6 200 21 0 timeout 900     580 11000    0 timeout 900    210 12000   0 error 3.8 280 33 0 unknown .26 49 2.2 0 disqualified 760   310 9400 0 timeout (verification) 900    140 9400   0 timeout 900   2100 11000 0 timeout 900   970 7300 0 timeout 900   2200 13000 0
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.4  0 error (42) 880     3400   11000    0 error (134) .069 8.7 .55 0 error 3.7 280 35 0 unknown 300    67 4600   0 unknown 8.4 450 110 0 unknown 1.6 200 21 0 timeout 900     890 11000    0 timeout 900    98 11000   0 error 3.7 280 33 0 unknown .28 33 2.1 0 disqualified 760   310 7900 0 timeout (verification) 900    300 13000   0 true 28   780 300 2 true 140   760 1400 2 true 28   610 240 2
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i error (134) .15  26 1.9  0 out of memory 360     14000   3800    0 error (134) .067 8.5 .65 0 error 3.8 280 36 0 unknown 900    310 11000   0 unknown 8.4 450 110 0 unknown 1.6 200 23 0 timeout 900     3800 10000    0 true 43    74 540   2 error 3.7 280 35 0 unknown .17 34 1.5 0 disqualified 760   280 8900 0 timeout (verification) 900    340 9800   0 true 20   550 190 2 true 190   950 1700 2 true 25   710 190 2
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.8  0 error (42) 880     4700   13000    0 error (134) .085 8.0 .40 0 error 3.8 280 31 0 unknown 900    180 12000   0 unknown 8.3 450 120 0 unknown 1.6 200 27 0 timeout 900     700 12000    0 true 30    75 410   2 error 3.7 280 31 0 unknown .17 35 1.5 0 disqualified 760   730 6300 0 timeout (verification) 900    400 11000   0 true 45   690 430 2 timeout 900   940 7600 0 true 33   820 280 2
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.8  0 error (42) 880     4700   10000    0 error (134) .062 8.8 .72 0 error 3.7 280 37 0 unknown 900    180 11000   0 unknown 8.2 450 110 0 unknown 1.6 200 20 0 timeout 900     700 12000    0 true 31    75 430   2 error 3.7 260 34 0 unknown .31 49 1.6 0 disqualified 760   710 8300 0 timeout (verification) 900    390 14000   0 true 67   720 820 2 timeout 900   960 7800 0 true 61   960 640 2
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.5  0 error (42) 880     12000   5000    0 error (42) 880     14000   12000    0 error 3.7 280 32 0 unknown 900    200 12000   0 unknown 8.5 450 100 0 unknown 1.6 200 20 0 timeout 900     290 12000    0 true 41    75 500   2 error 3.9 280 34 0 out of memory (unknown) 20    15000 190   0 disqualified 760   180 11000 0 timeout (verification) 900    1300 11000   0 true 22   670 200 2 timeout 900   1000 9600 0 true 20   690 180 2
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.3  0 out of memory 460     14000   5400    0 error (42) 870     2000   12000    0 error 3.6 270 36 0 unknown 900    270 13000   0 unknown 8.4 450 96 0 unknown 1.6 200 19 0 timeout 900     500 11000    0 true 14    75 220   2 error 3.7 280 32 0 out of memory (unknown) 19    15000 220   0 disqualified 760   520 7800 0 timeout (verification) 900    1400 9800   0 true 15   510 130 2 true 27   630 290 2 true 17   650 150 2
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.4  0 out of memory 270     13000   3800    0 out of memory 830     15000   13000    0 error 3.6 270 34 0 unknown 890    790 9500   0 unknown 8.6 440 110 0 unknown 1.6 200 22 0 timeout 900     1300 10000    0 true 18    70 230   2 error 3.7 280 29 0 out of memory (unknown) 19    15000 200   0 disqualified 760   540 7500 0 timeout (verification) 900    880 11000   0 true 12   490 100 2 true 90   740 790 2 true 12   560 98 2
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.9  0 out of memory 800     14000   8800    0 out of memory 840     15000   14000    0 error 3.8 280 34 0 unknown 900    640 12000   0 unknown 8.2 450 120 0 unknown 1.6 200 22 0 timeout 900     990 10000    0 true 18    75 280   2 error 3.8 280 40 0 out of memory (unknown) 31    15000 290   0 disqualified 750   320 6400 0 timeout (verification) 900    460 12000   0 true 23   750 190 2 timeout 900   1100 6900 0 true 23   550 200 2
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.6  0 out of memory 100     14000   830    0 error (42) 880     260   11000    0 error 3.3 250 29 0 unknown 370    85 4900   0 unknown 8.4 450 120 0 unknown 1.6 200 22 0 timeout 900     2400 11000    0 timeout 900    2100 7000   0 error 3.8 280 35 0 out of memory (unknown) 20    15000 230   0 disqualified 760   350 7500 0 timeout (verification) 900    1100 12000   0 true 23   470 280 2 true 130   590 1400 2 true 26   510 240 2
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.2  0 error (6) 140     13000   1500    0 error (134) .10  7.5 .42 0 error 3.7 280 30 0 unknown 60    40 780   0 unknown 8.3 450 100 0 unknown 1.6 200 20 0 timeout 900     2200 12000    0 true 740    87 8600   2 error 3.8 280 31 0 unknown .15 34 1.4 0 disqualified 760   360 9700 0 timeout (verification) 900    330 10000   0 true 14   500 120 2 true 30   620 280 2 true 16   530 150 2
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.2  0 error (42) 880     1900   9400    0 error (134) .058 8.6 .61 0 error 3.7 280 32 0 unknown 77    42 1100   0 unknown 8.4 450 100 0 unknown 1.5 200 23 0 timeout 900     1500 11000    0 true 310    180 4300   2 error 3.8 280 32 0 unknown .15 36 1.5 0 disqualified 760   390 11000 0 timeout (verification) 900    580 13000   0 true 14   550 120 2 timeout 900   720 10000 0 true 15   590 120 2
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.5  0 false(valid-deref) .079 7.2 .81 -16 error (134) .12  6.8 .49 0 error 3.7 280 33 0 unknown 130    48 1800   0 unknown 8.5 440 110 0 unknown 1.6 200 20 0 timeout 900     310 12000    0 true 320    180 4300   2 error 3.7 280 34 0 unknown .16 35 1.4 0 disqualified 760   400 9900 0 timeout (verification) 900    270 12000   0 true 21   540 220 2 timeout 900   760 12000 0 true 17   640 160 2
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i error (134) .19  26 1.5  0 error (6) 150     13000   1500    0 error (134) .057 8.2 .55 0 error 3.6 280 29 0 unknown 58    40 690   0 unknown 8.3 450 130 0 unknown 1.6 200 23 0 timeout 900     2100 13000    0 unknown 180    130 2500   0 error 3.4 250 30 0 unknown .15 35 1.5 0 disqualified 760   400 9700 0 timeout (verification) 900    1400 11000   0 true 14   520 120 2 true 20   530 180 2 true 13   500 130 2
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.7  0 out of memory 120     13000   1200    0 error (134) .057 7.8 .72 0 error 3.7 280 33 0 unknown 150    46 1800   0 unknown 8.3 450 120 0 unknown 1.5 200 22 0 timeout 900     1200 13000    0 true 160    88 2000   2 error 3.3 250 34 0 unknown .17 35 1.3 0 disqualified 760   260 8700 0 timeout (verification) 900    280 10000   0 true 17   500 150 2 true 45   730 430 2 true 26   590 250 2
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.7  0 out of memory 360     14000   3400    0 error (134) .075 7.5 .48 0 error 3.8 280 35 0 unknown 900    310 10000   0 unknown 8.4 450 96 0 unknown 1.6 200 20 0 timeout 900     4000 10000    0 true 42    75 610   2 error 3.7 280 32 0 unknown .20 36 1.4 0 disqualified 760   260 9500 0 timeout (verification) 900    520 13000   0 true 46   870 400 2 timeout 900   940 10000 0 true 89   820 1100 2
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.5  0 out of memory 110     14000   1100    0 error (134) .071 8.1 .59 0 error 3.9 280 31 0 unknown 300    75 3600   0 unknown 8.5 450 100 0 unknown 1.6 200 21 0 timeout 900     650 12000    0 timeout 900    180 12000   0 error 3.8 280 37 0 unknown .21 36 2.0 0 disqualified 760   320 7800 0 timeout (verification) 900    340 13000   0 timeout 900   2600 13000 0 timeout 900   990 8000 0 timeout 900   2200 11000 0
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i error (134) .20  26 1.5  0 error (42) 880     1800   9900    0 error (134) .089 7.7 .48 0 error 3.5 250 34 0 unknown 240    81 2900   0 unknown 8.3 450 92 0 unknown 1.6 200 22 0 timeout 900     830 11000    0 true 35    75 470   2 error 3.5 250 35 0 unknown .17 36 2.3 0 disqualified 760   270 8100 0 timeout (verification) 900    200 11000   0 true 26   570 230 2 true 190   980 1900 2 true 55   720 600 2
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.5  0 out of memory 120     13000   1400    0 error (134) .088 7.6 .41 0 error 3.8 280 31 0 unknown 150    46 2000   0 unknown 8.2 450 92 0 unknown 1.6 200 19 0 timeout 900     1200 12000    0 true 160    88 1900   2 error 3.6 250 31 0 unknown .29 49 1.7 0 disqualified 760   260 9500 0 timeout (verification) 900    230 12000   0 true 16   520 140 2 true 55   940 530 2 true 18   680 150 2
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 2.6  0 error (42) 870     310   3600    0 error (134) .092 8.0 .52 0 error 3.7 280 34 0 unknown 900    230 11000   0 unknown 8.4 450 110 0 unknown 1.6 200 20 0 timeout 900     1200 13000    0 true 48    75 670   2 error 3.8 280 31 0 unknown .20 36 1.7 0 disqualified 760   280 8400 0 timeout (verification) 900    420 11000   0 error (7) 620   1200 9100 0 timeout 900   850 9600 0 timeout 900   1500 14000 0
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.5  0 error (42) 880     8200   6000    0 error (134) .072 8.5 .52 0 error 3.6 280 32 0 unknown 900    110 12000   0 unknown 8.5 450 110 0 unknown 1.6 200 21 0 timeout 900     380 13000    0 true 41    75 550   2 error 3.8 280 38 0 unknown .21 34 1.5 0 disqualified 760   280 9700 0 timeout (verification) 900    370 11000   0 true 37   690 300 2 timeout 900   940 9300 0 true 41   840 400 2
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.7  0 error (42) 880     3400   4400    0 error (134) .063 7.9 .49 0 error 3.5 270 28 0 unknown 66    40 850   0 unknown 8.5 450 100 0 unknown 1.6 200 21 0 timeout 900     780 13000    0 true 15    75 190   2 error 3.7 270 36 0 unknown .14 34 1.2 0 disqualified 760   210 10000 0 timeout (verification) 900    350 13000   0 true 13   590 96 2 true 22   710 160 2 true 14   600 120 2
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.4  0 out of memory 230     14000   2400    0 error (134) .066 7.8 1.2  0 error 3.9 280 34 0 unknown 370    65 4700   0 unknown 8.2 440 110 0 unknown 1.6 200 18 0 timeout 900     640 11000    0 timeout 900    210 10000   0 error 3.8 280 33 0 unknown .22 36 1.9 0 disqualified 760   350 11000 0 timeout (verification) 900    140 10000   0 timeout 900   2300 12000 0 timeout 900   860 8900 0 timeout 900   2100 12000 0
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.6  0 error (42) 880     3800   9600    0 error (134) .064 8.5 .58 0 error 3.6 280 34 0 unknown 260    75 4000   0 unknown 8.3 450 98 0 unknown 1.5 200 23 0 timeout 900     1200 11000    0 timeout 900    100 14000   0 error 3.7 280 31 0 unknown .23 35 1.4 0 disqualified 760   290 9200 0 timeout (verification) 900    310 11000   0 true 31   810 320 2 true 330   1000 3000 2 true 38   680 340 2
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.5  0 out of memory 350     14000   4200    0 error (134) .10  7.4 .53 0 error 3.6 250 34 0 unknown 900    310 10000   0 unknown 8.4 450 100 0 unknown 1.6 200 20 0 timeout 900     4000 12000    0 true 41    75 570   2 error 3.7 280 33 0 unknown .42 49 1.4 0 disqualified 760   270 10000 0 timeout (verification) 900    490 14000   0 true 27   600 270 2 timeout 900   920 12000 0 true 31   760 300 2
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.4  0 error (42) 880     1600   9000    0 error (134) .067 8.3 .50 0 error 3.7 280 34 0 unknown 71    41 890   0 unknown 8.4 450 100 0 unknown 1.6 200 19 0 timeout 900     810 13000    0 true 620    75 7400   2 error 3.8 280 33 0 unknown .38 49 1.5 0 disqualified 760   250 8900 0 timeout (verification) 900    370 11000   0 true 12   500 100 2 timeout 900   810 11000 0 true 13   580 110 2
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.6  0 error (42) 880     260   7400    0 error (134) .067 7.7 .64 0 error 3.8 280 31 0 unknown 900    190 9700   0 unknown 8.5 450 110 0 unknown 1.6 200 19 0 timeout 900     720 12000    0 true 42    75 550   2 error 3.4 250 34 0 unknown .19 36 1.6 0 disqualified 760   680 7100 0 timeout (verification) 900    330 12000   0 true 30   580 380 2 timeout 900   860 8600 0 true 170   910 2000 2
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.7  0 error (42) 880     1000   10000    0 error (134) .095 7.5 .56 0 error 3.7 280 37 0 unknown 900    160 10000   0 unknown 8.5 450 110 0 unknown 1.6 200 20 0 timeout 900     220 12000    0 true 59    75 870   2 error 3.7 280 31 0 unknown .19 37 1.8 0 disqualified 760   300 7300 0 timeout (verification) 900    360 11000   0 true 26   610 240 2 timeout 900   920 10000 0 true 35   820 340 2
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i error (134) .21  26 1.4  0 error (42) 880     4700   4500    0 error (134) .11  7.4 .56 0 error 3.8 280 35 0 unknown 900    240 11000   0 unknown 8.5 450 93 0 unknown 1.6 200 20 0 timeout 900     400 14000    0 true 53    75 770   2 error 3.6 250 31 0 unknown .30 50 2.3 0 disqualified 750   330 7300 0 timeout (verification) 900    310 12000   0 timeout 900   1200 11000 0 timeout 900   940 8500 0 timeout 900   1200 13000 0
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.5  0 error (42) 880     5000   7500    0 error (134) .091 7.3 .44 0 error 3.7 270 34 0 true .59 36 8.8 2 unknown 8.4 450 110 0 unknown 1.6 200 20 0 timeout 900     990 11000    0 true 21    75 290   2 error 3.6 280 36 0 unknown .14 36 1.3 0 disqualified 760   310 10000 0 timeout (verification) 900    570 11000   0 true 13   490 120 2 true 25   760 240 2 true 14   550 130 2
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.6  0 out of memory 120     14000   1200    0 error (42) 880     12000   11000    0 error 3.7 280 34 0 unknown 900    220 12000   0 unknown 8.4 450 100 0 unknown 1.6 200 24 0 timeout 900     360 14000    0 true 16    75 200   2 error 3.7 280 37 0 out of memory (unknown) 19    15000 190   0 disqualified 760   510 6400 0 timeout (verification) 900    1100 11000   0 true 18   680 150 2 timeout 900   1300 11000 0 true 17   540 150 2
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.5  0 error (42) 880     2500   3900    0 error (42) 880     160   10000    0 error 3.9 280 32 0 unknown 78    52 940   0 unknown 8.4 450 110 0 unknown 1.6 200 20 0 timeout 900     3100 11000    0 true 15    75 220   2 error 3.7 280 30 0 out of memory (unknown) 19    15000 200   0 disqualified 760   260 8900 0 timeout (verification) 900    1400 13000   0 true 11   500 80 2 true 13   570 97 2 true 12   520 92 2
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.4  0 out of memory 240     13000   2400    0 error (42) 870     3300   12000    0 error 3.7 280 36 0 unknown 900    160 11000   0 unknown 8.3 450 100 0 unknown 1.6 200 22 0 timeout 900     550 12000    0 true 15    74 230   2 error 3.4 250 32 0 out of memory (unknown) 20    15000 220   0 disqualified 760   670 7400 0 timeout (verification) 900    1500 11000   0 true 12   510 94 2 true 20   550 170 2 true 12   490 110 2
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.4  0 error (42) 880     11000   9300    0 error (134) .059 7.8 .54 0 error 3.7 280 33 0 unknown 900    230 12000   0 unknown 8.4 440 120 0 unknown 1.6 200 20 0 timeout 900     240 9500    0 unknown 210    140 3000   0 error 3.7 280 31 0 unknown .17 35 2.2 0 disqualified 760   160 9100 0 timeout (verification) 900    350 12000   0 true 18   600 160 2 timeout 900   610 11000 0 true 15   590 130 2
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.7  0 error (42) 880     1200   4700    0 error (134) .071 8.2 .66 0 error 3.7 280 34 0 unknown 690    110 9000   0 unknown 8.3 450 110 0 unknown 1.6 200 21 0 timeout 900     250 13000    0 true 36    75 470   2 error 3.5 250 30 0 unknown .17 35 1.4 0 disqualified 760   240 8200 0 timeout (verification) 900    430 11000   0 true 36   640 420 2 true 220   770 2300 2 true 26   610 270 2
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.8  0 error (42) 880     5300   9600    0 error (134) .088 9.1 .56 0 error 3.7 280 33 0 unknown 900    220 10000   0 unknown 8.4 450 100 0 unknown 1.6 200 20 0 timeout 900     780 10000    0 true 36    74 470   2 error 3.9 280 32 0 unknown .18 35 1.3 0 disqualified 760   710 5700 0 timeout (verification) 900    390 14000   0 true 230   870 2900 2 timeout 900   880 8000 0 true 200   1200 2900 2
array-examples/relax_false-valid-deref.i error (134) .16  26 1.8  0 false(valid-deref) .13  7.9 .76 1 false(valid-deref) .13  7.8 .83 1 error 3.5 250 33 0 false(valid-deref) .23 35 2.6 1 unknown 8.3 450 100 0 unknown 1.6 200 19 0 false(valid-deref) .17  27 1.8  1 false(valid-deref) 320    4000 2800   1 error 3.8 280 32 0 unknown .14 35 1.1 0 disqualified 750   250 9400 0 witness invalid (false(valid-deref)) .67 18 7.8 0 false(valid-deref) 9.5 350 81 1 false(valid-deref) 9.7 370 78 1 false(valid-deref) 9.3 370 76 1
array-examples/sanfoundry_24_false-valid-deref.i error (134) .090 24 .73 0 error (42) 880     4000   7900    0 out of memory 180     15000   1900    0 timeout 900   4800 12000 0 unknown 90    71 1100   0 unknown 8.3 430 88 0 unknown 8.6 430 94 0 timeout 900     1000 8500    0 timeout 900    100 9800   0 timeout 900   4800 13000 0 timeout 900    4200 8700   0 disqualified 7.5 100 100 0 timeout (verification) 900    1100 11000   0 timeout 900   1000 9100 0 timeout 900   1200 7800 0 timeout 900   860 8600 0
array-examples/standard_strcpy_false-valid-deref_ground.i error (134) .092 23 1.2  0 out of memory 56     15000   750    0 out of memory 200     15000   2300    0 timeout 900   5200 11000 0 unknown 66    55 800   0 unknown 8.0 430 110 0 unknown 8.2 430 100 0 timeout 900     220 13000    0 false(valid-deref) 350    4300 4400   0 timeout 900   5200 12000 0 timeout 900    5500 8600   0 disqualified 8.3 100 100 0 false(valid-deref) 2.0  100 31   0 timeout 900   820 10000 0 timeout 900   1100 6600 0 timeout 900   1100 11000 0
array-examples/standard_strcpy_original_false-valid-deref.i error (134) .099 23 .57 0 out of memory 57     15000   720    0 out of memory 410     15000   6300    0 timeout 900   5200 12000 0 unknown 53    54 670   0 unknown 8.2 430 100 0 unknown 8.1 430 98 0 timeout 900     1100 11000    0 false(valid-deref) 340    4300 3500   0 timeout 900   5200 12000 0 timeout 900    4200 9800   0 disqualified 9.6 110 130 0 false(valid-deref) 2.1  100 29   0 timeout 900   930 7800 0 timeout 900   1100 5600 0 timeout 900   980 9100 0
array-memsafety-realloc/array-realloc_false-valid-free.i error (134) .18  26 1.4  0 false(valid-free) .11  8.0 1.3  1 false(valid-free) .16  8.5 1.0  1 error 3.9 280 35 0 unknown 14    49 210   0 unknown 8.3 450 100 0 unknown 9.0 450 110 0 unknown .16  26 1.5  0 unknown .75 39 11   0 true 11   460 110 -32 unknown .19 35 1.4 0 disqualified 760   290 9000 0 false(valid-free) .24 17 2.3 1 false(valid-free) 12   450 92 1 false(valid-free) 13   520 130 1 false(valid-free) 11   420 82 1
array-memsafety-realloc/array-realloc_true-valid-memsafety.i error (134) .17  26 1.6  0 true 10     1300   140    2 error (134) .15  11   1.3  0 error 3.8 280 30 0 unknown 37    74 530   0 unknown 8.4 440 110 0 unknown 9.1 450 130 0 unknown .16  27 1.7  0 unknown .74 39 9.2 0 false(valid-free) 4.2 290 33 -16 unknown .18 37 1.5 0 disqualified 880   240 9800 0 true 1.3  19 18   2 true 27   690 240 2 true 63   950 540 2 timeout 900   1000 12000 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 71 11 1800 100 0 71 29000     460000   280000    4 71 13000   150000 180000   12 71 5400 62000 61000 4 71 27000    10000 350000   20 71 590   31000 7500 1 71 190 17000 2500 6 71 46000   55000 590000 18 71 15000 24000 180000 91 71 5700   64000 66000 -44 71 3000    240000 30000   14 71 39000 21000 440000 0 71 43000   34000 560000 14 71 10000 48000 120000 103 71 26000 52000 260000 69 71 12000 58000 140000 101
    correct results 0 19 13     1500   160    20 12 1.1 89 7.3 12 4 11 990 100 4 19 5.0  650 61   20 1 8.3 430 110 1 6 51 2600 650 6 18 2.5 480 29 18 54 4300 9400 54000 91 4 11   990 99 4 14 2.6  540 22   14 0 12 5.6 220 75 14 61 1300 32000 13000 103 44 2100 26000 20000 69 60 1600 34000 17000 101
        correct true 0 1 10     1300   140    2 0 0 1 .59 36 8.8 2 0 0 0 37 4000 3000 51000 74 0 0 0 2 1.5 38 21 4 42 1100 25000 11000 84 25 1900 19000 19000 50 41 1400 27000 16000 82
        correct false 0 18 2.6   250   26    18 12 1.1 89 7.3 12 4 11 990 100 4 18 4.4  620 52   18 1 8.3 430 110 1 6 51 2600 650 6 18 2.5 480 29 18 17 370 6300 3300 17 4 11   990 99 4 14 2.6  540 22   14 0 10 4.1 180 54 10 19 190 7600 1600 19 19 200 7900 1600 19 19 200 7600 1600 19
    correct-unconfimed results 0 1 .10  7.5 1.0  0 0 0 0 0 0 0 2 700 8700 7900 0 0 1 .16 36 2.7 0 0 3 4.4 220 63 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 0 1 .10  7.5 1.0  0 0 0 0 0 0 0 2 700 8700 7900 0 0 1 .16 36 2.7 0 0 3 4.4 220 63 0 0 0 0
    incorrect results 0 1 .079 7.2 .81 -16 0 0 0 0 0 0 0 2 15   750 140 -48 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 0 1 11   460 110 -32 0 0 0 0 0 0
        incorrect false 0 1 .079 7.2 .81 -16 0 0 0 0 0 0 0 1 4.2 290 33 -16 0 0 0 0 0 0
score (71 tasks, max score: 120) 0 4 12 4 20 1 6 18 91 -44 14 0 14 103 69 101
Run set 2ls.sv-comp19_prop-memsafety.MemSafety-Arrays cbmc.sv-comp19_prop-memsafety.MemSafety-Arrays cbmc-path.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq.sv-comp19_prop-memsafety.MemSafety-Arrays depthk.sv-comp19_prop-memsafety.MemSafety-Arrays divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays divine-smt.sv-comp19_prop-memsafety.MemSafety-Arrays esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Arrays map2check.sv-comp19_prop-memsafety.MemSafety-Arrays pesco.sv-comp19_prop-memsafety.MemSafety-Arrays predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays smack.sv-comp19_prop-memsafety.MemSafety-Arrays symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer.sv-comp19_prop-memsafety.MemSafety-Arrays ukojak.sv-comp19_prop-memsafety.MemSafety-Arrays utaipan.sv-comp19_prop-memsafety.MemSafety-Arrays