Tool 2LS 0.3.4 Cascade 2.0 CBMC CPAchecker 1.4-svcomp16c CPAchecker 1.4-svn 18373 CPAchecker 1.4-svcomp16c ESBMC ESBMC version 2.0.0 64-bit x86_64 linux DepthK ESBMC+DepthK version 2.1 Forest svc_16_20151108 SeaHorn-F16 0.1.0 SMACK+Corral 1.5.2 symbiotic 3.0.1 ULTIMATE Automizer cfb9fd9e ULTIMATE Kojak fd30d3d8
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24] [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23] [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic Linux 4.2.0-23-generic Linux 4.2.0-22-generic Linux 4.2.0-23-generic Linux 4.2.0-22-generic Linux 4.2.0-23-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-02 22:42:27 CET [[ 2016-01-15 21:37:22 CET ]] 2016-01-16 07:57:57 CET [[ 2016-01-16 11:29:59 CET ]] 2016-01-03 00:42:25 CET [[ 2016-01-15 21:54:19 CET ]] 2016-01-04 06:25:51 CET [[ 2016-01-15 21:59:57 CET ]] 2016-01-04 01:42:53 CET [[ 2016-01-15 22:02:40 CET ]] 2016-01-04 20:04:07 CET [[ 2016-01-15 22:05:37 CET ]] 2016-01-04 13:17:38 CET [[ 2016-01-15 22:10:37 CET ]] 2016-01-16 17:45:19 CET [[ 2016-01-17 00:39:38 CET ]] 2016-01-05 14:06:34 CET [[ 2016-01-15 22:17:52 CET ]] 2016-01-09 23:49:59 CET [[ 2016-01-15 22:20:31 CET ]] 2016-01-13 15:22:34 CET [[ 2016-01-15 22:30:28 CET ]] 2016-01-07 09:05:16 CET [[ 2016-01-15 22:36:10 CET ]] 2016-01-07 09:04:54 CET [[ 2016-01-15 22:39:28 CET ]] 2016-01-14 23:51:13 CET [[ 2016-01-15 22:41:15 CET ]] 2016-01-08 15:10:30 CET [[ 2016-01-15 22:43:29 CET ]]
Run set 2ls.sv-comp16.ArraysMemSafety cascade.sv-comp16.ArraysMemSafety cbmc.sv-comp16.ArraysMemSafety cpa-bam.sv-comp16.ArraysMemSafety cpa-kind.sv-comp16.ArraysMemSafety cpa-refsel.sv-comp16.ArraysMemSafety cpa-seq.sv-comp16.ArraysMemSafety esbmc.sv-comp16.ArraysMemSafety esbmcdepthk.sv-comp16.ArraysMemSafety forest.sv-comp16.ArraysMemSafety seahorn.sv-comp16.ArraysMemSafety smack.sv-comp16.ArraysMemSafety symbiotic3.sv-comp16.ArraysMemSafety uautomizer.sv-comp16.ArraysMemSafety ukojak.sv-comp16.ArraysMemSafety
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ ../../results-verified/cascade.2016-01-16_0757.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --graphml-cex error-witness.graphml [[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--k-induction -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -svcomp [[ ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --cex=error-witness.graphml [[ ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -w error-witness.graphml [[ ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/array-memsafety/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
add_last_unsafe_false-valid-deref.i error(signal 6) .22  27 false(valid-deref) 2.8 120 false(valid-deref) .27 27 error .49 48 error .50 49 error .67 50 error 3.7 170 false(valid-deref) 69     130 unknown .069 8.6 true 1.0  38   error (3) .033 5.6 error (1) 1.4 18 error (1) .018 3.8 false(valid-deref) 10   330 false(valid-deref) 10   330
bubblesort_unsafe_false-valid-deref.i true .099 23 false(valid-deref) 1.7 98 false(valid-deref) .13 24 error .64 50 error .52 49 error .53 48 timeout 900   10000 false(valid-deref) 800     12000 unknown .085 8.7 unknown .57 38   error (3) .040 5.6 error (1) 1.4 18 error (1) .035 3.9 false(valid-deref) 8.7 310 false(valid-deref) 9.6 330
count_down_unsafe_false-valid-deref.i error(signal 6) .21  27 false(valid-deref) 4.3 160 false(valid-deref) .38 30 error .54 49 error .59 49 error .58 48 error 3.7 170 unknown 900     10000 unknown .061 8.5 true 3.0  38   error (3) .024 5.5 error (1) 1.5 18 error (1) .020 4.0 false(valid-deref) 8.7 320 false(valid-deref) 9.2 330
cstrcat_unsafe_false-valid-deref.i true .10  23 false(valid-deref) 1.5 93 false(valid-deref) .18 24 error .49 49 error .51 49 error .61 48 false(valid-deref) 3.1 160 false(valid-deref) .77  31 unknown .060 8.6 true .59 38   error (3) .046 5.5 error (1) 1.4 18 error (1) .022 3.8 false(valid-deref) 9.6 330 false(valid-deref) 9.4 330
cstrchr_unsafe_false-valid-deref.i true .16  25 false(valid-memtrack) 2.9 130 false(valid-deref) .18 27 error .49 48 error .54 50 error .61 48 error 3.1 170 false(valid-deref) 1.4   23 unknown .061 8.4 false(valid-free) 1.4  38   error (3) .038 5.6 error (1) 1.4 18 error (1) .017 4.0 false(valid-deref) 15   470 timeout 130   1400
cstrlen_unsafe_false-valid-deref.i error(signal 6) .23  27 false(valid-deref) 3.6 130 false(valid-deref) .28 28 error .56 46 error .51 49 error .61 49 error 3.7 170 false(valid-deref) 1.1   19 unknown .094 8.6 true .59 38   error (3) .026 5.5 error (1) 1.0 18 error (1) .012 4.1 false(valid-deref) 11   330 timeout 140   1300
cstrncat_unsafe_false-valid-deref.i true .10  23 false(valid-deref) 1.6 96 false(valid-deref) .19 25 error .63 50 error .60 49 error .63 48 false(valid-deref) 2.6 170 false(valid-deref) .88  47 unknown .062 8.5 true .63 38   error (3) .024 5.5 error (1) 1.4 18 error (1) .015 4.0 false(valid-deref) 9.4 330 false(valid-deref) 8.8 320
cstrncpy_unsafe_false-valid-deref.i true .079 23 false(valid-deref) 1.7 97 false(valid-deref) .12 25 error .54 49 error .61 47 error .68 53 false(valid-deref) 2.8 160 false(valid-deref) 210     3700 unknown .064 8.3 true .72 38   error (3) .020 5.5 error (1) 1.4 18 error (1) .035 3.8 false(valid-deref) 8.2 320 false(valid-deref) 10   350
cstrpbrk_unsafe_false-valid-deref.i true .16  25 false(valid-free) 3.3 130 false(valid-deref) .20 28 error .60 50 error .60 49 error .65 48 error 3.0 170 false(valid-deref) 100     3600 unknown .064 8.6 false(valid-free) 1.2  39   error (3) .042 5.5 error (1) 1.5 18 error (1) .015 3.9 false(valid-deref) 14   420 timeout 900   540
diff_usafe_false-valid-deref.i true .15  23 false(valid-deref) 1.6 100 false(valid-deref) .17 25 error .59 49 error .63 49 error .63 48 false(valid-deref) 2.6 170 unknown 900     7500 unknown .11  8.9 true .58 38   error (3) .024 5.6 error (1) 1.3 18 error (1) .034 4.0 false(valid-deref) 9.5 330 false(valid-deref) 9.3 330
knapsack_alloca_unsafe_false-valid-deref.i error(signal 6) .24  27 false(valid-deref) 3.5 140 false(valid-deref) 3.4  180 error .51 49 error .59 49 error .67 49 error 3.2 170 out of memory 150     15000 unknown .072 8.7 true .27 7.3 error (3) .029 5.4 error (1) 1.3 18 error (1) .026 3.8 false(valid-deref) 13   340 false(valid-deref) 13   370
lis_unsafe_false-valid-deref.i true .33  35 false(valid-deref) 4.4 170 false(valid-deref) .29 28 error .49 49 error .59 49 error .52 49 error 3.9 170 out of memory 39     15000 unknown .097 8.5 false(valid-free) 23    38   error (3) .026 5.6 error (1) 1.5 18 error (1) .019 3.8 error 16   420 false(valid-deref) 71   750
mult_array_unsafe_false-valid-deref.i error(signal 6) .23  27 false(valid-deref) 4.8 160 false(valid-deref) .33 33 error .49 50 error .53 49 error .57 48 error 3.7 180 false(valid-deref) 4.1   88 unknown .065 8.3 true .50 38   error (3) .020 5.4 error (1) 1.4 18 error (1) .016 4.0 false(valid-deref) 11   360 error 11   340
reverse_array_alloca_unsafe_false-valid-deref.i error(signal 6) .21  27 false(valid-deref) 3.4 150 false(valid-deref) 1.3  75 error .51 49 error .60 49 error .55 49 error 3.8 170 false(valid-deref) 390     690 unknown .086 8.4 unknown .54 38   error (3) .046 5.5 error (1) 1.3 18 error (1) .022 3.9 false(valid-deref) 12   330 false(valid-deref) 13   350
reverse_array_unsafe_false-valid-deref.i error(signal 6) .17  27 false(valid-deref) 4.3 150 false(valid-deref) 1.2  75 error .57 49 error .61 49 error .71 49 error 3.1 170 false(valid-deref) 880     960 unknown .067 8.8 false(valid-free) .91 38   error (3) .019 5.6 error (1) 1.4 18 error (1) .030 3.9 false(valid-deref) 10   350 false(valid-deref) 11   340
selectionsort_unsafe_false-valid-deref.i true .10  23 false(valid-deref) 1.5 99 false(valid-deref) .17 24 error .64 50 error .59 49 error .64 49 false(valid-deref) 3.2 180 false(valid-deref) 65     5800 unknown .063 8.5 false(valid-free) .77 39   error (3) .022 5.5 error (1) 1.3 18 error (1) .011 4.0 false(valid-deref) 9.6 340 false(valid-deref) 9.7 330
stroeder1_unsafe_false-valid-deref.i true .11  23 false(valid-deref) 1.6 93 false(valid-deref) .14 24 error .65 49 error .59 48 error .51 49 false(valid-deref) 3.2 160 false(valid-deref) .30  17 unknown .095 8.6 unknown .53 38   error (3) .038 5.5 error (1) 1.0 18 error (1) .020 3.9 false(valid-deref) 9.9 340 false(valid-deref) 10   350
add_last-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 850   1900 true 850    14000 error .50 48 error .52 48 error .64 48 error 3.9 170 true 120     150 unknown .10  8.7 true .79 38   error (3) .027 5.5 error (1) 1.5 18 error (1) .016 3.9 timeout 900   1000 timeout 500   740
array01-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 860   650 true 470    14000 error .60 49 error .61 49 error .65 49 error 3.9 170 true 590     10000 unknown .066 8.6 false(valid-free) .92 39   error (3) .042 5.5 error (1) 1.3 18 error (1) .034 3.9 true 11   330 true 13   420
array02-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 860   620 true 550    13000 error .49 49 error .59 49 error .63 48 error 3.8 170 out of memory 91     15000 unknown .066 8.4 false(valid-free) 1.2  38   error (3) .031 5.5 error (1) 1.4 19 error (1) .019 3.9 true 12   340 true 14   460
array03-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 860   1400 true 490    13000 error .61 49 error .50 48 error .63 49 error 3.7 180 true 480     15000 unknown .071 8.7 unknown .57 39   error (3) .047 5.5 error (1) 1.4 19 error (1) .024 4.0 true 13   360 true 14   430
bubblesort-alloca_true-valid-memsafety.i error(signal 6) .22  27 unknown 860   610 true 560    13000 error .67 49 error .60 48 error .60 49 error 3.8 180 out of memory 84     15000 unknown .089 8.6 true .90 38   error (3) .044 5.5 error (1) 1.4 19 error (1) .016 3.9 true 20   360 timeout 42   910
count_down-alloca_true-valid-memsafety.i error(signal 6) .26  27 unknown 860   490 true 320    14000 error .58 49 error .60 49 error .64 48 error 3.9 180 true 540     9800 unknown .065 8.3 false(valid-free) 71    38   error (3) .047 5.5 error (1) 1.2 18 error (1) .021 3.9 timeout 900   1400 true 76   410
cstrcat-alloca_true-valid-memsafety.i error(signal 6) .26  27 unknown 860   450 true 140    15000 error .50 49 error .59 47 error .53 49 error 3.7 170 true 15     62 unknown .064 8.6 false(valid-free) 1.0  39   error (3) .028 5.5 error (1) 1.3 18 error (1) .029 3.9 error 43   660 error 110   860
cstrchr-alloca_true-valid-memsafety.i error(signal 6) .16  27 unknown 860   640 true 22    120 error .59 49 error .65 50 error .57 50 error 3.7 170 true 1.5   32 unknown .099 8.6 false(valid-free) .66 38   error (3) .049 5.4 error (1) 1.5 18 error (1) .036 3.9 error 15   350 timeout 140   1200
cstrcmp-alloca_true-valid-memsafety.i error(signal 6) .23  27 unknown 860   670 true 40    250 error .50 49 error .59 49 error .53 49 error 3.8 170 true 3.8   46 unknown .065 8.7 true .56 38   error (3) .040 5.4 error (1) 1.5 18 error (1) .035 4.0 true 19   400 timeout 45   730
cstrcpy-alloca_true-valid-memsafety.i error(signal 6) .17  27 true 200   600 true 57    2500 error .58 49 error .51 49 error .62 46 error 3.1 170 true 1.8   45 unknown .070 8.6 true .61 39   error (3) .049 5.4 error (1) 1.5 18 error (1) .018 4.0 timeout 900   1800 timeout 130   1400
cstrcspn-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 900   1000 true 850    6000 error .59 49 error .59 49 error .61 49 error 3.1 170 unknown 900     6300 unknown .062 8.6 unknown .55 38   error (3) .050 5.5 error (1) 1.4 18 error (1) .036 3.9 error 21   490 timeout 45   650
cstrlen-alloca_true-valid-memsafety.i error(signal 6) .21  27 true 110   470 true 12    65 error .52 46 error .54 47 error .58 50 error 3.3 170 true 1.1   21 unknown .071 8.6 unknown .59 38   error (3) .023 5.5 error (1) 1.5 18 error (1) .021 4.0 true 13   380 timeout 140   1200
cstrncat-alloca_true-valid-memsafety.i error(signal 6) .22  27 unknown 850   1900 true 290    14000 error .64 50 error .55 49 error .61 49 error 3.7 170 true 35     95 unknown .065 8.8 unknown .25 7.4 error (3) .026 5.6 error (1) 1.3 19 error (1) .024 3.8 error 28   480 timeout 350   1200
cstrncmp-alloca_true-valid-memsafety.i error(signal 6) .22  27 unknown 860   660 true 180    580 error .53 49 error .51 49 error .57 48 error 4.1 170 true 6.2   120 unknown .051 8.6 false(valid-free) .76 39   error (3) .045 5.5 error (1) 1.5 19 error (1) .036 3.9 true 22   460 timeout 36   600
cstrncpy-alloca_true-valid-memsafety.i error(signal 6) .26  27 unknown 860   490 true 850    6300 error .62 49 error .59 50 error .72 52 error 3.0 170 true 80     4900 unknown .054 8.5 false(valid-free) .75 38   error (3) .040 5.5 error (1) 1.4 19 error (1) .015 3.9 timeout 900   4400 timeout 140   1200
cstrpbrk-alloca_true-valid-memsafety.i error(signal 6) .17  27 timeout 900   1100 true 850    6000 error .56 49 error .59 49 error .67 49 error 3.3 170 unknown 900     6300 unknown .070 8.8 true .58 38   error (3) .038 5.6 error (1) 1.4 18 error (1) .020 4.0 error 40   460 timeout 39   700
cstrspn-alloca_true-valid-memsafety.i error(signal 6) .21  27 timeout 900   1100 true 850    6000 error .51 49 error .56 49 error .53 48 error 3.3 170 unknown 900     6300 unknown .063 8.3 true .58 38   error (3) .024 5.6 error (1) 1.5 19 error (1) .021 4.0 error 22   480 timeout 42   1100
diff-alloca_true-valid-memsafety.i error(signal 6) .23  27 unknown 870   740 true 230    14000 error .48 49 error .54 49 error .65 50 error 3.9 170 unknown 900     10000 unknown .099 8.8 false(valid-free) 1.5  39   error (3) .043 5.5 error (1) 1.4 19 error (1) .022 3.9 timeout 900   970 error 860   930
insertionsort-alloca_true-valid-memsafety.i error(signal 6) .26  26 timeout 900   1400 true 370    15000 error .50 49 error .51 52 error .63 50 error 3.8 170 true 230     5700 unknown .055 8.6 false(valid-free) .89 38   error (3) .045 5.5 error (1) 1.4 18 error (1) .037 3.8 error 13   340 true 16   370
java_BubbleSort-alloca_true-valid-memsafety.i error(signal 6) .17  27 unknown 860   630 true 560    13000 error .62 50 error .59 49 error .52 48 error 3.7 170 out of memory 260     15000 unknown .096 8.7 false(valid-free) .96 38   error (3) .025 5.5 error (1) 1.4 18 error (1) .016 3.8 true 20   380 true 17   500
lis-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 860   610 true 500    14000 error .60 50 error .51 49 error .52 49 error 4.0 170 out of memory 49     15000 unknown .062 8.6 false(valid-free) 1.2  39   error (3) .050 5.5 error (1) 1.4 18 error (1) .028 3.9 error 180   1200 timeout 120   860
mult_array-alloca_true-valid-memsafety.i error(signal 6) .22  27 unknown 860   500 true 850    12000 error .57 49 error .62 48 error .51 48 error 3.8 170 true 1.9   66 unknown .063 8.5 unknown .53 38   error (3) .030 5.5 error (1) 1.5 19 error (1) .014 3.9 true 17   390 error 9.6 320
openbsd_cbzero-alloca_true-valid-memsafety.i error(signal 6) .22  27 true 27   470 true 41    2300 error .49 46 error .60 49 error .55 52 error 3.8 170 true .58  28 unknown .063 8.6 true 18    39   error (3) .036 5.5 error (1) 1.5 19 error (1) .028 4.1 timeout 900   850 error 530   470
openbsd_cmemchr-alloca_true-valid-memsafety.i error(signal 6) .16  27 true 110   510 true 83    99 error .58 49 error .58 49 error .53 50 error 3.7 180 true 1.1   42 unknown .064 8.4 true 2.0  39   error (3) .030 5.5 error (1) 1.4 18 error (1) .020 3.9 timeout 900   1200 true 13   340
openbsd_cmemrchr-alloca_true-valid-memsafety.i error(signal 6) .21  26 true 160   520 false(valid-deref) .24 28 error .48 49 error .58 49 error .60 48 error 3.7 170 true 4.7   49 unknown .069 8.6 true .60 38   error (3) .027 5.5 error (1) 1.4 19 error (1) .013 3.9 error 14   340 true 11   340
openbsd_cmemset-alloca_true-valid-memsafety.i error(signal 6) .24  27 true 27   480 true 41    2400 error .57 49 error .63 49 error .64 49 error 3.2 170 true .75  26 unknown .065 8.8 true 2.7  39   error (3) .032 5.4 error (1) 1.5 19 error (1) .014 3.9 timeout 900   1800 true 12   370
openbsd_cstpcpy-alloca_true-valid-memsafety.i error(signal 6) .23  27 true 200   600 true 51    2500 error .59 49 error .59 49 error .63 49 error 3.8 170 true 1.8   42 unknown .079 8.7 true .60 38   error (3) .025 5.6 error (1) 1.4 19 error (1) .031 3.9 timeout 900   1000 timeout 130   1400
openbsd_cstpncpy-alloca_true-valid-memsafety.i error(signal 6) .22  27 unknown 860   500 true 850    4900 error .58 46 error .51 50 error .62 48 error 3.2 170 true 80     4400 unknown .070 8.5 unknown .55 38   error (3) .019 5.6 error (1) 1.4 19 error (1) .034 4.1 timeout 900   830 timeout 130   1500
openbsd_cstrcat-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 860   440 true 140    15000 error .58 49 error .50 48 error .65 49 error 3.7 170 true 15     62 unknown .069 8.6 unknown .88 40   error (3) .035 5.5 error (1) 1.4 18 error (1) .021 3.9 error 65   770 timeout 92   1100
openbsd_cstrcmp-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 860   700 true 130    310 error .61 50 error .63 50 error .51 48 error 3.9 170 true 4.4   82 unknown .062 8.6 unknown .49 36   error (3) .023 5.5 error (1) 1.5 19 error (1) .016 4.1 timeout 900   1800 timeout 36   640
openbsd_cstrcpy-alloca_true-valid-memsafety.i error(signal 6) .22  27 true 200   600 true 57    2500 error .49 48 error .51 49 error .62 48 error 3.8 170 true 1.8   42 unknown .10  8.5 false(valid-free) .87 38   error (3) .046 5.5 error (1) 1.5 18 error (1) .021 3.9 error 26   390 timeout 130   1300
openbsd_cstrcspn-alloca_true-valid-memsafety.i error(signal 6) .23  27 unknown 870   700 true 850    350 error .50 52 error .52 47 error .61 47 error 3.1 170 false(valid-deref) 260     8400 unknown .065 8.6 false(valid-free) .81 38   error (3) .051 5.5 error (1) 1.4 19 error (1) .013 3.9 true 39   490 timeout 70   890
openbsd_cstrlcpy-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 860   410 true 130    14000 error .50 49 error .53 49 error .60 49 error 3.8 170 true 190     180 unknown .11  8.6 false(valid-free) .93 38   error (3) .020 5.6 error (1) 1.3 18 error (1) .021 3.9 timeout 900   1600 timeout 72   880
openbsd_cstrlen-alloca_true-valid-memsafety.i error(signal 6) .24  27 true 110   510 true 12    64 error .64 47 error .61 49 error .67 50 error 3.1 170 true 1.2   22 unknown .11  8.5 true .60 38   error (3) .034 5.4 error (1) 1.5 18 error (1) .016 4.0 true 21   460 timeout 130   1200
openbsd_cstrncat-alloca_true-valid-memsafety.i error(signal 6) .23  27 unknown 860   360 true 280    14000 error .51 48 error .64 50 error .63 48 error 3.3 170 true 26     94 unknown .067 8.8 true .59 39   error (3) .023 5.6 error (1) 1.5 19 error (1) .017 3.9 error 70   550 timeout 110   850
openbsd_cstrncmp-alloca_true-valid-memsafety.i error(signal 6) .22  27 unknown 860   710 true 210    500 error .87 49 error .55 50 error .63 49 error 4.0 170 true 4.3   150 unknown .094 8.4 false(valid-free) .94 39   error (3) .030 5.5 error (1) 1.4 18 error (1) .022 3.9 timeout 900   1600 timeout 47   740
openbsd_cstrncpy-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 860   490 true 850    7900 error .52 48 error .60 49 error .61 49 error 2.9 180 true 79     4400 unknown .065 8.7 false(valid-free) .88 39   error (3) .036 5.5 error (1) 1.5 18 error (1) .032 3.9 timeout 900   1100 timeout 140   1200
openbsd_cstrnlen-alloca_true-valid-memsafety.i error(signal 6) .26  27 true 450   620 true 15    94 error .62 49 error .60 48 error .60 49 error 3.6 170 true 1.3   25 unknown .094 8.6 true .62 38   error (3) .051 5.4 error (1) 1.4 18 error (1) .017 4.1 true 22   360 timeout 130   1200
openbsd_cstrpbrk-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 870   830 true 850    100 error .58 47 error .54 49 error .61 49 error 3.3 170 unknown 900     5800 unknown .066 8.6 true .60 38   error (3) .050 5.5 error (1) 1.4 19 error (1) .014 3.9 error 23   360 true 62   780
openbsd_cstrspn-alloca_true-valid-memsafety.i error(signal 6) .23  27 unknown 870   600 true 850    3500 error .56 49 error .52 49 error .58 49 error 3.7 170 unknown .098 18 unknown .072 8.7 false(valid-free) .78 39   error (3) .040 5.4 error (1) 1.5 18 error (1) .025 3.8 error 42   480 error 100   1000
openbsd_cstrstr-alloca_true-valid-memsafety.i error(signal 6) .21  27 unknown 860   2000 true 850    8100 error .57 49 error .61 47 error .64 50 error 3.7 170 out of memory 51     15000 unknown .065 8.7 false(valid-free) .90 39   error (3) .052 5.4 error (1) 1.4 19 error (1) .012 3.9 error 28   560 timeout 45   1000
rec_strlen-alloca_true-valid-memsafety.i error (6) .21  26 unknown 3.1 150 true 18    130 error .59 49 error .64 50 error .68 50 error 3.2 170 true 1.2   26 unknown .095 8.6 false(valid-free) .83 38   error (3) .030 5.4 error (1) 1.5 18 error (1) .031 3.9 error 21   490 timeout 130   1200
selectionsort-alloca_true-valid-memsafety.i error(signal 6) .25  27 unknown 880   1300 true 230    14000 error .58 49 error .63 50 error .62 48 error 3.8 170 unknown 900     9000 unknown .090 8.6 true .52 38   error (3) .020 5.5 error (1) 1.4 18 error (1) .024 3.9 error 14   350 timeout 44   780
stroeder1-alloca_true-valid-memsafety.i error(signal 6) .21  27 true 29   450 true 5.3  60 error .60 49 error .65 49 error .62 48 error 3.8 170 true .65  25 unknown .070 8.6 true .55 38   error (3) .026 5.4 error (1) 1.4 18 error (1) .033 4.0 true 12   340 true 11   340
stroeder2-alloca_true-valid-memsafety.i error(signal 6) .22  27 unknown 860   610 true 250    14000 error .55 50 error .53 50 error .53 48 error 3.8 170 true 860     6900 unknown .069 8.9 true .65 39   error (3) .022 5.6 error (1) 1.4 19 error (1) .016 3.9 true 22   420 true 18   380
strreplace-alloca_true-valid-memsafety.i error(signal 6) .21  26 unknown 850   650 true 180    14000 error .55 49 error .52 50 error .60 48 error 3.9 180 true 1.7   57 unknown .068 8.6 unknown .51 38   error (3) .032 5.5 error (1) 1.4 18 error (1) .015 3.9 error 21   410 timeout 130   1300
subseq-alloca_true-valid-memsafety.i error(signal 6) .24  27 unknown 850   1800 true 850    2000 error .59 49 error .52 49 error .63 49 error 3.7 170 true 81     140 unknown .088 8.6 true .66 39   error (3) .034 5.4 error (1) 1.4 18 error (1) .022 3.9 true 48   430 true 110   980
substring-alloca_true-valid-memsafety.i error(signal 6) .17  27 unknown 880   850 true 850    800 error .59 47 error .60 49 error .63 48 error 3.7 180 unknown 900     9600 unknown .069 8.7 false(valid-free) .77 38   error (3) .037 5.4 error (1) 1.4 18 error (1) .017 3.9 true 60   630 timeout 65   990
../../sv-benchmarks/c/array-memsafety/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
total tasks 65 13   1700 65 33000   38000 65 19000    330000 65 37 3200 65 37 3200 65 39 3200 65 1100 21000 65 15000 280000 65 4.8 560 65 160   2400 65 2.2 360 65 92 1200 65 1.4 260 65 14000 43000 65 6800 49000
    correct results 0 26 1700   7700 64 19000    330000 0 0 0 6 17 1000 47 6000 90000 0 19 33   730 0 0 0 32 540 12000 26 580 11000
        correct true 0 11 1600   5800 47 19000    330000 0 0 0 0 34 3500 63000 0 19 33   730 0 0 0 16 370 6500 13 380 6100
        correct false 0 15 42   1800 17 9.0  710 0 0 0 6 17 1000 13 2500 27000 0 0 0 0 0 16 170 5600 13 190 4800
    incorrect results 10 1.4 240 2 6.2 250 1 .24 28 0 0 0 0 1 260 8400 0 34 120   1300 0 0 0 0 0
        incorrect true 10 1.4 240 0 0 0 0 0 0 0 0 9 7.8 310 0 0 0 0 0
        incorrect false 0 2 6.2 250 1 .24 28 0 0 0 0 1 260 8400 0 25 120   960 0 0 0 0 0
score (65 tasks, max score: 113) -320 5 95 0 0 0 6 65 0 -650 0 0 0 48 39
Run set 2ls.sv-comp16.ArraysMemSafety cascade.sv-comp16.ArraysMemSafety cbmc.sv-comp16.ArraysMemSafety cpa-bam.sv-comp16.ArraysMemSafety cpa-kind.sv-comp16.ArraysMemSafety cpa-refsel.sv-comp16.ArraysMemSafety cpa-seq.sv-comp16.ArraysMemSafety esbmc.sv-comp16.ArraysMemSafety esbmcdepthk.sv-comp16.ArraysMemSafety forest.sv-comp16.ArraysMemSafety seahorn.sv-comp16.ArraysMemSafety smack.sv-comp16.ArraysMemSafety symbiotic3.sv-comp16.ArraysMemSafety uautomizer.sv-comp16.ArraysMemSafety ukojak.sv-comp16.ArraysMemSafety