Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 Predator-HP symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-01 08:19:20 CET 2017-12-01 08:19:34 CET 2017-12-01 08:37:17 CET 2017-12-01 08:43:39 CET 2017-12-01 08:22:21 CET 2017-12-01 09:05:19 CET 2017-12-02 00:00:31 CET 2017-12-02 11:31:00 CET 2017-12-01 23:12:01 CET 2017-12-01 21:45:44 CET 2017-12-02 23:08:57 CET 2017-12-03 04:39:25 CET 2017-12-03 04:40:15 CET 2017-12-03 07:53:44 CET
Run set 2ls.sv-comp18.MemSafety-Arrays cbmc.sv-comp18.MemSafety-Arrays cpa-bam-bnb.sv-comp18.MemSafety-Arrays cpa-bam-slicing.sv-comp18.MemSafety-Arrays cpa-seq.sv-comp18.MemSafety-Arrays depthk.sv-comp18.MemSafety-Arrays esbmc-incr.sv-comp18.MemSafety-Arrays esbmc-kind.sv-comp18.MemSafety-Arrays map2check.sv-comp18.MemSafety-Arrays predatorhp.sv-comp18.MemSafety-Arrays symbiotic.sv-comp18.MemSafety-Arrays uautomizer.sv-comp18.MemSafety-Arrays ukojak.sv-comp18.MemSafety-Arrays utaipan.sv-comp18.MemSafety-Arrays
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction --witness error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
array-memsafety/add_last_unsafe_false-valid-deref.i error (134) .17  26 1.6  0 false(valid-deref) .48 37 4.2 1 error (1) .47 40 3.9 0 error (1) .52 40 4.3 0 error 2.5 220 22 0 false(valid-deref) .52 28 5.7 0 false(valid-deref) .17 29 2.0 1 false(valid-deref) .17 29 2.4 1 false(valid-deref) .54  13 5.9  1 unknown .11 22 1.8 0 false(valid-deref) .28 12 2.4 1 false(valid-deref) 5.2 280 42 1 false(valid-deref) 5.7 320 45 1 false(valid-deref) 5.7 290 45 1
array-memsafety/bubblesort_unsafe_false-valid-deref.i error (134) .086 22 .75 0 false(valid-deref) .25 33 2.0 1 error (1) .47 42 4.0 0 error (1) .42 40 3.9 0 timeout (segmentation fault) 900   12000 7400 0 false(valid-deref) .36 27 3.9 1 false(valid-deref) .17 28 1.5 0 false(valid-deref) .20 28 1.9 1 false(valid-deref) 1.2   13 15    1 false(valid-deref) .15 22 1.7 1 false(valid-deref) .24 11 2.7 1 false(valid-deref) 4.7 270 40 1 false(valid-deref) 5.0 260 45 1 false(valid-deref) 4.4 260 36 1
array-memsafety/count_down_unsafe_false-valid-deref.i error (134) .19  26 1.5  0 false(valid-deref) .49 36 4.4 1 error (1) .50 42 4.2 0 error (1) .46 40 4.0 0 error 2.9 240 24 0 false(valid-deref) .55 29 6.4 0 false(valid-deref) .21 29 1.9 1 false(valid-deref) .26 29 2.4 1 false(valid-deref) .60  13 7.7  1 unknown .14 23 1.7 0 false(valid-deref) .24 12 2.3 1 false(valid-deref) 5.5 290 45 1 false(valid-deref) 5.6 300 45 1 false(valid-deref) 5.8 290 45 1
array-memsafety/cstrcat_unsafe_false-valid-deref.i error (134) .094 22 .78 0 false(valid-deref) .26 33 2.3 1 error (1) .48 41 3.9 0 error (1) .45 40 4.0 0 false(valid-deref) 2.5 240 19 1 false(valid-deref) .36 27 3.8 1 false(valid-deref) .13 28 1.4 1 false(valid-deref) .30 28 3.7 1 false(valid-deref) .57  11 5.7  1 false(valid-deref) .13 21 1.8 1 false(valid-deref) .22 11 2.2 1 false(valid-deref) 4.2 240 35 1 false(valid-deref) 4.6 250 41 1 false(valid-deref) 4.3 260 35 1
array-memsafety/cstrchr_unsafe_false-valid-deref.i error (134) .17  26 1.7  0 false(valid-deref) .45 36 4.3 1 error (1) .48 41 4.2 0 error (1) .43 40 3.6 0 error 2.5 210 24 0 false(valid-deref) .54 28 6.8 1 false(valid-deref) .22 29 2.7 1 false(valid-deref) .23 29 2.2 1 false(valid-deref) .99  14 12    1 unknown .15 23 1.7 0 false(valid-deref) .87 59 8.5 1 false(valid-deref) 11   540 95 1 false(valid-deref) 8.9 470 78 1 false(valid-deref) 16   700 130 1
array-memsafety/cstrlen_unsafe_false-valid-deref.i error (134) .17  26 1.7  0 false(valid-deref) .46 36 4.4 1 error (1) .49 40 4.5 0 error (1) .46 40 4.3 0 error 2.8 240 27 0 false(valid-deref) 1.2  28 17   0 false(valid-deref) .25 29 3.0 1 false(valid-deref) .20 29 2.5 1 false(valid-deref) 1.8   13 25    1 unknown .12 23 1.6 0 false(valid-deref) .86 59 10   0 false(valid-deref) 7.3 360 53 1 false(valid-deref) 10   530 85 1 false(valid-deref) 7.4 380 63 1
array-memsafety/cstrncat_unsafe_false-valid-deref.i error (134) .084 23 .69 0 false(valid-deref) .24 33 2.0 1 error (1) .48 40 4.2 0 error (1) .44 40 4.3 0 false(valid-deref) 2.5 250 21 1 false(valid-deref) .35 27 3.5 1 false(valid-deref) .17 28 1.4 1 false(valid-deref) .28 28 3.2 0 false(valid-deref) .67  12 7.3  1 false(valid-deref) .13 25 1.8 1 false(valid-deref) .23 11 2.7 1 false(valid-deref) 4.4 250 36 1 false(valid-deref) 4.7 260 38 1 false(valid-deref) 4.2 260 35 1
array-memsafety/cstrncpy_unsafe_false-valid-deref.i error (134) .096 22 .82 0 false(valid-deref) .25 35 2.3 1 error (1) .45 41 4.1 0 error (1) .44 42 3.9 0 false(valid-deref) 2.5 250 21 1 false(valid-deref) .36 27 3.9 0 false(valid-deref) .36 28 3.2 0 false(valid-deref) .41 28 4.1 0 false(valid-deref) 1.1   13 16    1 false(valid-deref) .14 23 1.9 1 false(valid-deref) .24 11 2.3 1 false(valid-deref) 4.3 260 35 1 false(valid-deref) 4.7 260 41 1 false(valid-deref) 4.5 260 36 1
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i error (134) .19  26 1.4  0 false(valid-deref) .47 36 4.2 1 error (1) .46 40 4.5 0 error (1) .42 40 4.1 0 error 2.8 240 22 0 false(valid-deref) .70 28 9.5 1 false(valid-deref) .31 29 3.3 1 false(valid-deref) .37 29 3.6 1 false(valid-deref) 1.1   14 14    1 unknown .13 24 1.7 0 false(valid-deref) .62 59 6.4 1 false(valid-deref) 10   530 94 1 false(valid-deref) 9.9 550 79 1 false(valid-deref) 14   580 130 1
array-memsafety/diff_usafe_false-valid-deref.i error (134) .096 22 .64 0 false(valid-deref) .27 33 2.4 1 error (1) .50 43 4.2 0 error (1) .44 40 4.6 0 segmentation fault 810   9700 7300 0 false(valid-deref) .35 27 4.1 1 false(valid-deref) .19 28 3.6 0 false(valid-deref) .27 28 2.6 0 false(valid-deref) 1.8   14 23    1 false(valid-deref) .12 23 1.8 1 false(valid-deref) .25 11 2.9 1 false(valid-deref) 4.7 280 43 1 false(valid-deref) 4.9 290 43 1 false(valid-deref) 4.9 280 44 1
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i error (134) .20  26 1.7  0 false(valid-deref) 1.1  93 10   1 error (1) .48 40 4.1 0 error (1) .45 40 4.2 0 error 2.7 240 25 0 false(valid-deref) .86 29 11   1 false(valid-deref) .32 30 3.0 1 false(valid-deref) .36 31 4.1 1 false(valid-deref) 1.1   14 12    1 unknown .11 24 1.8 0 false(valid-deref) .30 12 3.2 1 false(valid-deref) 6.2 310 48 1 false(valid-deref) 6.8 330 54 1 false(valid-deref) 6.7 290 52 1
array-memsafety/lis_unsafe_false-valid-deref.i error (134) .19  26 1.5  0 false(valid-deref) .48 36 4.4 1 error (1) .49 42 4.1 0 error (1) .44 41 4.1 0 error 2.5 210 22 0 false(valid-deref) .70 28 8.5 1 false(valid-deref) .20 29 2.2 1 false(valid-deref) .40 29 3.9 0 unknown 1.3   14 18    0 unknown .12 23 1.7 0 false(valid-deref) .29 12 3.6 1 false(valid-deref) 11   540 89 1 timeout 900   1500 8600 0 false(valid-deref) 15   820 130 1
array-memsafety/mult_array_unsafe_false-valid-deref.i error (134) .19  26 1.6  0 false(valid-deref) .54 38 5.1 1 error (1) .49 40 4.3 0 error (1) .46 40 4.4 0 error 2.7 240 22 0 false(valid-deref) .66 28 8.2 1 false(valid-deref) .43 33 6.2 1 false(valid-deref) .63 36 7.7 1 false(valid-deref) 1.2   18 16    1 unknown .11 24 1.8 0 false(valid-deref) .55 17 6.4 1 false(valid-deref) 5.4 290 44 1 false(valid-deref) 6.1 330 46 1 false(valid-deref) 6.1 300 44 1
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i error (134) .19  26 1.2  0 false(valid-deref) .65 47 6.8 1 error (1) .49 41 4.3 0 error (1) .43 40 3.8 0 error 2.6 210 23 0 false(valid-deref) 1.8  28 21   0 false(valid-deref) .28 29 3.5 1 false(valid-deref) .40 29 3.7 0 false(valid-deref) .64  79 9.1  1 unknown .14 24 1.7 0 false(valid-deref) .29 12 3.0 1 false(valid-deref) 6.3 280 46 1 false(valid-deref) 11   590 110 0 false(valid-deref) 11   570 89 0
array-memsafety/reverse_array_unsafe_false-valid-deref.i error (134) .18  26 1.4  0 false(valid-deref) .69 47 5.9 1 error (1) .47 41 4.3 0 error (1) .41 38 3.4 0 error 2.5 220 20 0 false(valid-deref) .60 29 7.2 0 false(valid-deref) .23 29 2.0 1 false(valid-deref) .23 29 2.4 1 false(valid-deref) .61  29 7.5  1 unknown .11 24 1.8 0 false(valid-deref) .25 12 2.9 1 false(valid-deref) 5.9 280 51 1 false(valid-deref) 5.8 310 49 1 false(valid-deref) 6.1 280 49 1
array-memsafety/selectionsort_unsafe_false-valid-deref.i error (134) .094 22 .69 0 false(valid-deref) .24 33 2.1 1 error (1) .48 42 4.1 0 error (1) .45 40 4.1 0 segmentation fault 620   7600 5900 0 false(valid-deref) .36 27 3.9 1 false(valid-deref) .14 28 1.3 0 false(valid-deref) .15 28 1.4 1 false(valid-deref) 1.3   14 15    1 false(valid-deref) .16 21 1.8 1 false(valid-deref) .22 12 2.4 1 false(valid-deref) 5.1 290 40 1 false(valid-deref) 5.0 260 45 1 false(valid-deref) 4.4 260 39 1
array-memsafety/stroeder1_unsafe_false-valid-deref.i error (134) .094 22 .64 0 false(valid-deref) .24 33 2.5 1 error (1) .48 45 4.8 0 error (1) .44 40 4.1 0 false(valid-deref) 2.5 250 24 1 false(valid-deref) .36 27 3.8 1 false(valid-deref) .24 28 1.9 1 false(valid-deref) .23 28 1.9 1 false(valid-deref) .83  13 11    1 false(valid-deref) .14 21 2.0 1 false(valid-deref) .24 11 2.2 1 false(valid-deref) 4.2 250 40 1 false(valid-deref) 4.4 250 36 1 false(valid-deref) 4.5 250 34 1
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.8  0 error (42) 880    13000 3400   0 error (1) .47 41 4.8 0 error (1) .46 41 4.1 0 error 2.5 210 26 0 unknown 700    110 9600   0 timeout 900    470 11000   0 timeout 900    440 11000   0 true .83  13 9.5  2 unknown .11 23 1.9 0 true .27 12 2.9 2 timeout 900   2500 11000 0 timeout 900   2300 13000 0 true 41   1200 400 2
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.4  0 error (134) 130    13000 1200   0 error (1) .48 40 4.3 0 error (1) .43 38 3.4 0 error 2.5 220 21 0 unknown 890    280 11000   0 timeout 900    1200 13000   0 timeout 900    520 12000   0 true 1.2   13 16    2 unknown .11 24 1.8 0 timeout (timeout) 900    430 12000   0 timeout 900   770 11000 0 true 22   760 220 2 true 11   550 83 2
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i error (134) .20  26 1.2  0 error (134) 480    13000 3200   0 error (1) .45 41 4.6 0 error (1) .40 40 4.2 0 error 2.8 240 28 0 unknown 890    320 9900   0 timeout 900    550 14000   0 timeout 900    510 13000   0 unknown 890     13 13000    0 unknown .14 24 1.7 0 timeout (timeout) 900    610 13000   0 timeout 900   760 12000 0 true 20   720 180 2 timeout 900   770 12000 0
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i error (134) .15  26 2.2  0 error (134) 160    13000 1500   0 error (1) .49 41 4.2 0 error (1) .44 41 3.9 0 error 2.6 220 23 0 unknown 890    470 11000   0 timeout 900    1400 13000   0 timeout 900    1500 12000   0 true 1.5   13 17    2 unknown .15 24 1.7 0 timeout (timeout) 900    430 12000   0 true 8.3 420 77 2 timeout 900   2000 12000 0 timeout 900   820 10000 0
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.3  0 error (42) 870    5200 4300   0 error (1) .47 40 4.0 0 error (1) .42 40 4.2 0 error 2.4 220 22 0 unknown 890    330 8100   0 timeout 900    1600 8600   0 timeout 900    1200 8800   0 true 2.2   13 30    2 unknown .14 24 1.8 0 true .26 12 2.6 2 true 8.7 400 63 2 true 56   1200 710 2 true 15   690 130 2
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i error (134) .19  26 1.2  0 error (134) 160    13000 1300   0 error (1) .49 40 3.8 0 error (1) .48 40 4.1 0 error 2.8 240 24 0 unknown 890    270 8900   0 timeout 900    530 12000   0 timeout 900    510 13000   0 unknown 900     410 11000    0 unknown .11 22 1.8 0 timeout (timeout) 900    390 11000   0 true 11   530 96 2 true 64   1400 780 2 true 17   810 150 2
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i error (134) .19  26 1.5  0 error (134) 91    14000 950   0 error (1) .49 40 4.2 0 error (1) .45 40 4.2 0 error 2.5 220 25 0 unknown 900    84 13000   0 timeout 900    710 11000   0 timeout 900    730 11000   0 true 370     25 4500    2 unknown .11 23 1.6 0 true .34 12 3.2 2 timeout 900   1600 12000 0 timeout 900   1200 11000 0 timeout 900   14000 5600 0
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.6  0 error (42) 870    3800 7300   0 error (1) .46 40 4.2 0 error (1) .44 41 4.0 0 error 2.6 210 22 0 unknown 160    46 2200   0 timeout 900    840 11000   0 timeout 900    830 12000   0 true 6.4   14 78    2 unknown .11 23 1.7 0 true .26 12 2.8 2 true 10   520 100 2 true 43   1200 610 2 true 17   830 150 2
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.4  0 error (42) 870    1900 8700   0 error (1) .48 40 4.7 0 error (1) .46 40 3.9 0 error 2.6 220 22 0 unknown 39    34 460   0 timeout 900    650 10000   0 timeout 900    660 12000   0 out of memory 36     15000 480    0 unknown .13 23 1.7 0 true .28 12 2.8 2 timeout 900   870 11000 0 true 220   1400 2900 2 timeout 900   890 12000 0
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i error (134) .20  26 1.3  0 error (134) 96    13000 980   0 error (1) .48 40 4.1 0 error (1) .47 40 4.5 0 error 2.6 220 26 0 unknown 140    47 1700   0 timeout 900    1400 11000   0 timeout 900    1400 9400   0 true 2.7   14 30    2 unknown .11 24 1.7 0 true .29 12 2.9 2 timeout 900   1600 12000 0 true 100   1300 1400 2 timeout 900   1100 13000 0
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i error (134) .19  26 1.5  0 error (42) 870    7000 7600   0 error (1) .46 40 3.9 0 error (1) .44 40 4.3 0 error 2.7 240 26 0 unknown 900    190 13000   0 timeout 900    630 10000   0 timeout 900    620 11000   0 true 3.9   15 45    2 unknown .15 23 1.7 0 true .28 12 3.8 2 timeout 900   1000 12000 0 timeout 900   1700 11000 0 timeout 900   880 11000 0
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.3  0 error (42) 870    4100 4700   0 error (1) .48 41 4.9 0 error (1) .48 40 4.2 0 error 2.6 220 26 0 unknown 100    30 1400   0 timeout 900    840 11000   0 timeout 900    850 10000   0 true 2.4   13 30    2 unknown .14 22 1.6 0 true .27 12 3.1 2 true 9.5 540 83 2 true 21   790 230 2 timeout 900   980 12000 0
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.3  0 error (134) 260    14000 1700   0 error (1) .51 40 4.2 0 error (1) .43 39 3.7 0 error 2.7 240 24 0 unknown 890    130 13000   0 timeout 900    570 12000   0 timeout 900    570 11000   0 true 320     41 3900    2 unknown .12 24 1.8 0 true 2.6  16 32   2 timeout 900   870 11000 0 timeout 900   1700 12000 0 timeout 900   2600 13000 0
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i error (134) .20  26 1.4  0 error (42) 870    2000 8900   0 error (1) .48 40 4.6 0 error (1) .45 41 4.1 0 error 2.7 240 22 0 unknown 62    79 800   0 timeout 900    830 11000   0 timeout 900    790 9600   0 true 240     20 2800    2 unknown .12 24 1.7 0 true .30 12 3.1 2 timeout 900   1000 14000 0 true 260   1200 3300 2 timeout 900   900 12000 0
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.4  0 error (134) 260    14000 2600   0 error (1) .52 42 4.6 0 error (1) .46 40 4.6 0 error 2.5 210 23 0 timeout 900    960 12000   0 timeout 900    3400 11000   0 timeout 900    3500 11000   0 true 7.4   14 100    2 unknown .15 23 1.8 0 true .29 12 3.5 2 timeout 900   1200 9900 0 timeout 900   1300 7000 0 true 28   1200 260 2
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.6  0 error (42) 870    7300 6900   0 error (1) .48 41 3.8 0 error (1) .43 40 4.1 0 error 2.5 220 21 0 unknown 890    140 14000   0 timeout 900    620 12000   0 timeout 900    650 12000   0 true 4.9   14 55    2 unknown .14 23 1.7 0 true .27 12 3.1 2 timeout 900   930 12000 0 timeout 900   1600 14000 0 timeout 900   850 11000 0
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i error (134) .19  26 1.4  0 error (42) 870    7500 6000   0 error (1) .45 40 4.1 0 error (1) .42 40 4.1 0 error 2.5 210 23 0 unknown 900    140 12000   0 timeout 900    620 10000   0 timeout 900    640 9700   0 true 5.0   13 52    2 unknown .14 24 1.7 0 true .29 12 3.2 2 timeout 900   890 12000 0 timeout 900   1700 12000 0 timeout 900   890 11000 0
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.7  0 error (42) 880    11000 4700   0 error (1) .49 41 5.0 0 error (1) .47 41 3.9 0 error 2.6 220 23 0 unknown 890    170 10000   0 timeout 900    300 10000   0 timeout 900    310 13000   0 true 5.6   14 76    2 unknown .12 23 1.7 0 true .27 12 2.7 2 timeout 900   1400 12000 0 timeout 900   1200 6500 0 timeout 900   1000 11000 0
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.6  0 error (42) 880    12000 4200   0 error (1) .51 42 4.6 0 error (1) .42 40 4.1 0 error 2.7 240 24 0 unknown 890    190 7900   0 timeout 900    520 12000   0 timeout 900    520 11000   0 true 1.4   13 19    2 unknown .15 23 1.8 0 true .25 12 2.9 2 true 12   540 110 2 true 76   1300 880 2 true 37   1400 360 2
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.4  0 error (42) 870    5200 5500   0 error (1) .47 42 4.2 0 error (1) .42 40 3.8 0 error 2.6 220 22 0 unknown 890    330 9400   0 timeout 900    1500 7500   0 timeout 900    1100 8600   0 true 2.2   13 25    2 unknown .14 22 1.7 0 true .26 12 2.9 2 true 8.8 450 68 2 true 36   970 350 2 true 15   740 120 2
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.5  0 error (42) 870    2500 5600   0 error (1) .47 41 4.1 0 error (1) .43 40 3.7 0 error 2.6 220 21 0 unknown 890    190 8200   0 timeout 900    980 11000   0 timeout 900    990 9000   0 true 2.5   14 33    2 unknown .14 24 1.7 0 true .25 14 3.8 2 timeout 900   870 13000 0 timeout 900   1800 13000 0 timeout 900   1200 11000 0
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i error (134) .15  26 1.8  0 error (134) 73    13000 830   0 error (1) .49 41 3.9 0 error (1) .42 40 4.1 0 error 2.5 220 23 0 unknown 320    90 4000   0 timeout 900    1800 10000   0 timeout 900    1800 11000   0 true 4.1   18 49    2 unknown .13 24 1.7 0 true .58 17 6.8 2 true 12   530 130 2 timeout 900   1300 5700 0 true 54   1400 600 2
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.4  0 error (134) 83    13000 990   0 error (1) .49 41 4.6 0 error (1) .44 40 4.2 0 error 2.7 240 24 0 unknown 100    33 1300   0 timeout 900    1900 9200   0 timeout 900    1900 10000   0 true 120     15 1800    2 unknown .14 24 1.7 0 true .25 12 2.9 2 timeout 900   840 12000 0 true 47   650 540 2 true 19   780 140 2
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i error (134) .19  26 1.2  0 error (42) 870    1300 5400   0 error (1) .50 42 4.9 0 error (1) .43 40 4.1 0 error 2.6 240 26 0 unknown 110    43 1400   0 timeout 900    1300 12000   0 timeout 900    1300 9300   0 true 6.2   14 77    2 unknown .11 24 1.8 0 true .21 11 2.2 2 timeout 900   740 12000 0 true 36   820 460 2 true 14   830 130 2
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.3  0 false(valid-deref) .47 36 3.4 -16 error (1) .48 42 4.2 0 error (1) .44 40 3.8 0 error 2.5 220 25 0 unknown 32    34 460   0 timeout 900    560 9500   0 timeout 900    360 9600   0 true 6.6   14 80    2 unknown .14 22 1.8 0 true .22 11 2.2 2 timeout 900   780 11000 0 true 61   700 720 2 timeout 900   740 10000 0
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i error (134) .15  26 1.5  0 error (134) 82    13000 850   0 error (1) .50 40 4.1 0 error (1) .45 40 4.3 0 error 2.8 240 23 0 unknown 94    31 1000   0 timeout 900    1900 11000   0 true .17 27 1.3 2 true 4.6   13 61    2 unknown .12 24 1.7 0 true .27 12 2.8 2 timeout 900   870 11000 0 true 16   650 140 2 true 13   700 110 2
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.5  0 error (134) 91    13000 1000   0 error (1) .50 43 4.9 0 error (1) .46 40 3.8 0 error 2.5 220 20 0 unknown 130    45 1800   0 timeout 900    1200 10000   0 timeout 900    1300 11000   0 true 2.3   14 28    2 unknown .13 24 1.6 0 true .27 12 3.3 2 timeout 900   980 10000 0 true 77   1400 1000 2 timeout 900   960 12000 0
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.5  0 error (134) 240    14000 2600   0 error (1) .46 40 4.4 0 error (1) .45 40 4.9 0 error 2.9 240 22 0 timeout 900    940 12000   0 timeout 900    3400 11000   0 timeout 900    3500 9900   0 true 7.3   14 78    2 unknown .14 23 1.8 0 true .27 12 3.5 2 timeout 900   960 10000 0 timeout 900   1500 13000 0 timeout 900   2200 11000 0
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.3  0 error (134) 89    14000 910   0 error (1) .51 41 4.2 0 error (1) .47 40 4.8 0 error 2.9 240 24 0 unknown 900    84 11000   0 timeout 900    680 8700   0 timeout 900    660 11000   0 true 370     25 4400    2 unknown .14 23 1.7 0 true .32 12 3.8 2 timeout 900   1600 11000 0 timeout 900   1300 13000 0 timeout 900   2000 9200 0
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i error (134) .20  26 1.4  0 error (42) 870    2200 8400   0 error (1) .48 41 4.2 0 error (1) .46 40 3.6 0 error 2.7 240 29 0 unknown 260    81 2900   0 timeout 900    880 10000   0 timeout 900    860 11000   0 true 5.4   13 64    2 unknown .15 23 1.8 0 true .29 13 2.9 2 timeout 900   860 12000 0 true 260   1400 3900 2 timeout 900   880 11000 0
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.4  0 error (134) 94    13000 1200   0 error (1) .49 41 4.1 0 error (1) .45 40 4.2 0 error 2.7 210 26 0 unknown 130    45 1700   0 timeout 900    1200 12000   0 timeout 900    1300 12000   0 true 2.5   13 37    2 unknown .16 24 1.7 0 true .29 12 3.0 2 timeout 900   1000 12000 0 true 77   1400 1100 2 timeout 900   920 12000 0
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i error (134) .15  26 1.4  0 error (42) 870    430 4000   0 error (1) .48 40 4.7 0 error (1) .43 40 3.9 0 error 2.5 220 23 0 unknown 900    1100 12000   0 timeout 900    1100 11000   0 timeout 900    1000 11000   0 true 9.0   13 100    2 unknown .12 23 1.7 0 true .30 12 3.3 2 timeout 900   1000 12000 0 timeout 900   1200 11000 0 timeout 900   860 12000 0
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.4  0 error (42) 880    8200 4500   0 error (1) .50 41 4.3 0 error (1) .47 40 3.8 0 error 2.7 240 26 0 unknown 900    120 11000   0 timeout 900    360 10000   0 timeout 900    350 11000   0 true 7.3   14 90    2 unknown .13 24 1.7 0 true .28 12 3.4 2 timeout 900   1600 11000 0 true 610   1200 7400 2 true 74   2200 790 2
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i error (134) .20  26 1.3  0 error (42) 870    4300 6100   0 error (1) .49 43 4.3 0 error (1) .47 40 4.3 0 error 2.5 220 25 0 unknown 94    29 1200   0 timeout 900    790 11000   0 timeout 900    790 10000   0 true 2.4   12 31    2 unknown .14 22 1.6 0 true .26 12 3.1 2 true 9.2 520 80 2 true 22   800 260 2 true 16   670 160 2
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i error (134) .20  26 1.4  0 error (134) 250    14000 2100   0 error (1) .45 40 4.2 0 error (1) .47 40 3.7 0 error 2.6 220 26 0 unknown 900    65 12000   0 timeout 900    640 11000   0 timeout 900    640 10000   0 true 330     34 4200    2 unknown .13 24 1.8 0 true 2.1  16 27   2 timeout 900   870 11000 0 timeout 900   1500 11000 0 timeout 900   800 11000 0
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i error (134) .20  26 1.3  0 error (42) 870    1700 7200   0 error (1) .49 42 4.5 0 error (1) .45 40 4.6 0 error 2.5 220 26 0 unknown 220    120 3300   0 timeout 900    1200 13000   0 timeout 900    1200 10000   0 true 230     18 3100    2 unknown .14 23 1.7 0 true .30 12 3.6 2 timeout 900   1100 11000 0 true 270   1500 3600 2 timeout 900   1100 11000 0
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.4  0 error (134) 230    14000 2300   0 error (1) .45 40 4.2 0 error (1) .44 40 4.4 0 error 2.5 220 23 0 timeout 900    940 11000   0 timeout 900    3400 10000   0 timeout 900    3500 10000   0 true 7.1   13 86    2 unknown .11 23 2.0 0 true .29 12 3.0 2 timeout 900   2300 11000 0 timeout 900   1200 6200 0 true 46   1900 450 2
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i error (134) .16  26 1.4  0 error (42) 870    2000 5700   0 error (1) .47 41 4.2 0 error (1) .44 41 4.0 0 error 2.7 240 22 0 unknown 110    32 1500   0 timeout 900    830 9500   0 timeout 900    830 11000   0 true 120     14 1600    2 unknown .12 24 1.7 0 true .27 12 3.1 2 timeout 900   790 13000 0 true 32   980 380 2 true 17   710 140 2
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.4  0 error (42) 870    280 5100   0 error (1) .50 40 4.0 0 error (1) .44 40 4.0 0 error 2.6 220 23 0 unknown 900    370 13000   0 timeout 900    670 11000   0 timeout 900    660 11000   0 true 7.3   13 110    2 unknown .14 21 1.8 0 true .27 12 2.9 2 timeout 900   840 13000 0 timeout 900   1700 12000 0 timeout 900   1100 12000 0
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i error (134) .19  26 1.3  0 error (42) 870    2600 10000   0 error (1) .47 44 4.8 0 error (1) .45 41 4.4 0 error 2.6 220 26 0 unknown 890    120 10000   0 timeout 900    240 13000   0 timeout 900    250 12000   0 true 12     13 160    2 unknown .14 23 1.8 0 true .26 12 3.1 2 timeout 900   900 12000 0 timeout 900   1200 7000 0 timeout 900   890 11000 0
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.8  0 error (42) 870    4000 6200   0 error (1) .49 40 4.1 0 error (1) .42 40 3.9 0 error 2.7 240 25 0 unknown 900    590 12000   0 timeout 900    380 11000   0 timeout 900    390 11000   0 true 11     17 140    2 unknown .16 24 2.0 0 true .28 12 3.2 2 timeout 900   900 9100 0 timeout 900   1100 11000 0 timeout 900   4600 12000 0
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i error (5) .19  26 1.3  0 error (42) 870    9400 5000   0 error (1) .51 41 4.3 0 error (1) .45 40 4.5 0 error 2.6 220 25 0 true 1.1  29 16   2 timeout 900    960 9300   0 timeout 900    960 11000   0 true 3.4   13 39    2 unknown .11 23 1.7 0 true .24 12 3.0 2 true 19   550 200 2 true 27   870 280 2 timeout 900   740 11000 0
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i error (134) .17  26 1.5  0 error (134) 72    14000 750   0 error (1) .45 40 3.8 0 error (1) .47 40 3.8 0 error 2.6 220 26 0 unknown 890    310 8200   0 timeout 900    310 10000   0 timeout 900    310 9900   0 true 1.8   13 20    2 unknown .15 23 1.8 0 true .25 14 2.9 2 true 10   540 88 2 timeout 900   2700 11000 0 true 34   1600 310 2
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i error (134) .19  26 1.3  0 error (42) 870    2400 3600   0 error (1) .50 41 4.0 0 error (1) .45 40 4.6 0 error 2.5 220 22 0 unknown 100    53 1400   0 timeout 900    2000 11000   0 timeout 900    2000 12000   0 true 2.0   14 27    2 unknown .14 23 1.7 0 true .27 12 3.1 2 true 8.7 430 75 2 true 8.7 470 77 2 timeout 900   750 11000 0
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.3  0 error (134) 220    13000 2100   0 error (1) .46 41 4.8 0 error (1) .44 40 4.1 0 error 2.5 220 26 0 unknown 890    260 12000   0 timeout 900    770 11000   0 timeout 900    780 14000   0 true 2.1   13 25    2 unknown .13 24 2.0 0 true 1.2  14 13   2 timeout 900   770 11000 0 true 30   970 310 2 true 12   630 110 2
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.9  0 error (42) 880    12000 4200   0 error (1) .49 41 4.5 0 error (1) .44 40 3.9 0 error 2.5 220 21 0 unknown 890    75 11000   0 timeout 900    270 12000   0 timeout 900    250 9800   0 true 6.6   14 91    2 unknown .11 26 1.7 0 true .25 12 3.2 2 timeout 900   950 12000 0 true 54   1300 630 2 timeout 900   1000 12000 0
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i error (134) .15  26 1.8  0 error (42) 870    1200 5300   0 error (1) .45 41 4.3 0 error (1) .42 40 4.3 0 error 2.9 240 27 0 unknown 890    63 11000   0 timeout 900    320 11000   0 timeout 900    310 13000   0 true 5.9   15 66    2 unknown .14 23 1.8 0 true .26 12 3.2 2 timeout 900   1100 11000 0 true 420   1400 6600 2 timeout 900   1500 13000 0
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i error (134) .18  26 1.4  0 error (42) 870    7800 6500   0 error (1) .47 40 4.3 0 error (1) .46 41 3.9 0 error 2.5 220 22 0 unknown 900    220 11000   0 timeout 900    750 12000   0 timeout 900    720 11000   0 true 5.9   15 67    2 unknown .11 22 1.9 0 true .26 12 3.1 2 timeout 900   1100 14000 0 timeout 900   1300 11000 0 timeout 900   1000 12000 0
array-examples/relax_false-valid-deref.i false(valid-deref) .24  27 1.8  1 false(valid-deref) .49 37 4.4 1 error (1) .49 40 4.7 0 error (1) .44 40 4.2 0 error 2.8 240 24 0 false(valid-deref) .62 29 6.3 0 false(valid-deref) .29 29 2.6 1 false(valid-deref) .28 30 3.2 1 unknown .042 11 .39 0 unknown .13 23 1.8 0 false(valid-deref) .32 13 3.7 1 false(valid-deref) 5.4 290 44 1 false(valid-deref) 6.2 310 53 1 false(valid-deref) 6.5 310 58 1
array-examples/sanfoundry_24_false-valid-deref.i out of memory 170     15000 1200    0 error (42) 870    6100 5300   0 error (1) .49 41 4.4 0 error (1) .47 40 4.0 0 timeout 900   5000 12000 0 unknown 110    100 1500   0 timeout 900    910 12000   0 timeout 900    910 10000   0 unknown 900     470 10000    0 timeout 900    2600 5500   0 timeout (timeout) 900    5500 9700   0 timeout 900   2400 13000 0 timeout 900   5800 12000 0 timeout 900   2000 14000 0
array-examples/standard_strcpy_false-valid-deref_ground.i out of memory 33     15000 420    0 out of memory 67    15000 980   0 error (1) .47 40 4.3 0 error (1) .42 40 4.1 0 false(valid-deref) 2.4 250 22 1 unknown 67    31 850   0 timeout 900    210 13000   0 timeout 900    210 12000   0 false(valid-deref) 18     12 230    0 timeout 900    6000 8600   0 timeout (timeout) 900    1700 9300   0 timeout 900   2700 13000 0 timeout 900   5700 15000 0 timeout 900   1300 12000 0
array-examples/standard_strcpy_original_false-valid-deref.i out of memory 33     15000 430    0 out of memory 67    15000 980   0 error (1) .49 41 4.1 0 error (1) .46 40 4.5 0 false(valid-deref) 2.4 250 22 1 unknown 67    30 820   0 timeout 900    1000 10000   0 timeout 900    1200 12000   0 false(valid-deref) 15     12 220    0 timeout 900    5300 9300   0 timeout (timeout) 900    2000 10000   0 timeout 900   2600 14000 0 timeout 900   5200 11000 0 timeout 900   1200 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
total 69 240    47000 2100   1 69 29000    430000 200000   2 69 33 2800 300 0 69 31 2800 280 0 69 3400 49000 34000 6 69 29000   11000 360000 13 69 46000    53000 560000   14 69 45000    50000 550000   15 69 5100 17000 64000 106 69 2700    15000 24000 7 69 6300    12000 78000   105 69 35000 59000 460000 42 69 26000 85000 310000 70 69 30000 79000 380000 53
    correct results 1 .24 27 1.8 1 18 8.0  710 74   18 0 0 6 15 1500 130 6 12 6.7 330 83 13 14 3.4  410 37   14 14 3.8  410 41   15 61 2300 1000 29000 106 7 .96 160 13 7 61 23    850 260   105 30 240 12000 2100 42 43 3100 34000 40000 70 35 600 25000 5600 53
        correct true 0 0 0 0 0 1 1.1 29 16 2 0 1 .17 27 1.3 2 45 2300 700 29000 90 0 44 17    550 200   88 12 130 6000 1200 24 27 3000 29000 39000 54 18 480 19000 4600 36
        correct false 1 .24 27 1.8 1 18 8.0  710 74   18 0 0 6 15 1500 130 6 11 5.6 310 67 11 14 3.4  410 37   14 13 3.6  380 39   13 16 16 290 200 16 7 .96 160 13 7 17 5.7  300 60   17 18 110 5800 920 18 16 99 5300 820 16 17 120 6100 1000 17
    correct-unconfimed results 0 0 0 0 0 7 5.7 200 68 0 4 .86 110 9.6 0 5 1.7  140 17   0 2 32 25 450 0 0 1 .86 59 10   0 0 1 11 590 110 0 1 11 570 89 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 7 5.7 200 68 0 4 .86 110 9.6 0 5 1.7  140 17   0 2 32 25 450 0 0 1 .86 59 10   0 0 1 11 590 110 0 1 11 570 89 0
    incorrect results 0 1 .47 36 3.4 -16 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 1 .47 36 3.4 -16 0 0 0 0 0 0 0 0 0 0 0 0
score (69 tasks, max score: 117) 1 2 0 0 6 13 14 15 106 7 105 42 70 53
Run set 2ls.sv-comp18.MemSafety-Arrays cbmc.sv-comp18.MemSafety-Arrays cpa-bam-bnb.sv-comp18.MemSafety-Arrays cpa-bam-slicing.sv-comp18.MemSafety-Arrays cpa-seq.sv-comp18.MemSafety-Arrays depthk.sv-comp18.MemSafety-Arrays esbmc-incr.sv-comp18.MemSafety-Arrays esbmc-kind.sv-comp18.MemSafety-Arrays map2check.sv-comp18.MemSafety-Arrays predatorhp.sv-comp18.MemSafety-Arrays symbiotic.sv-comp18.MemSafety-Arrays uautomizer.sv-comp18.MemSafety-Arrays ukojak.sv-comp18.MemSafety-Arrays utaipan.sv-comp18.MemSafety-Arrays