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-Other cbmc.sv-comp19_prop-memsafety.MemSafety-Other cbmc-path.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other depthk.sv-comp19_prop-memsafety.MemSafety-Other divine-explicit.sv-comp19_prop-memsafety.MemSafety-Other divine-smt.sv-comp19_prop-memsafety.MemSafety-Other esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other map2check.sv-comp19_prop-memsafety.MemSafety-Other pesco.sv-comp19_prop-memsafety.MemSafety-Other predatorhp.sv-comp19_prop-memsafety.MemSafety-Other smack.sv-comp19_prop-memsafety.MemSafety-Other symbiotic.sv-comp19_prop-memsafety.MemSafety-Other uautomizer.sv-comp19_prop-memsafety.MemSafety-Other ukojak.sv-comp19_prop-memsafety.MemSafety-Other utaipan.sv-comp19_prop-memsafety.MemSafety-Other
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
loops/invert_string_false-valid-deref.c false(valid-deref) .12  24 1.1  1 false(valid-deref) .077 7.7 .51 1 false(unreach-call) .14  9.2 .52 0 error 2.7 240 22 0 unknown .15 33 1.6 0 unknown 8.2 430 98 0 unknown 1.6 200 21 0 false(valid-deref) .11  26 .86 1 false(valid-deref) .46 83 6.5 1 error 2.7 240 24 0 unknown .16 48 1.7 0 false(valid-deref) 3.5  88 43   1 false(valid-deref) .75  18 7.9  1 false(valid-deref) 8.3 350 63 0 false(valid-deref) 9.4 380 80 0 false(valid-deref) 8.0 360 63 0
loop-acceleration/array3_false-valid-deref.i out of memory 810     15000 5600    0 false(valid-deref) 14     610   180    1 false(valid-deref) 78     660   600    1 timeout 900   1600 11000 0 unknown 120    49 1800   0 unknown 8.8 430 93 0 false(valid-memtrack) 8.4 430 89 -16 false(valid-deref) 19     370 280    1 timeout 900    4600 6500   0 timeout 900   1500 12000 0 timeout 900    88 11000   0 timeout 760    1300 4800   0 false(valid-deref) 13     21 190    1 timeout 900   850 9700 0 timeout 900   1900 7200 0 timeout 900   2400 11000 0
ntdrivers/floppy_false-valid-deref.i.cil.c error (134) 1.0   61 11    0 false(valid-deref) 4.4   150   94    1 false(valid-deref) 1.7   67   20    1 false(valid-deref) 11   550 100 1 false(valid-deref) 5.7  390 74   0 error - divine failed with exitcode 1 1.3 170 16 0 error - divine failed with exitcode 1 1.3 170 16 0 timeout 900     750 12000    0 unknown .92 41 11   0 false(valid-deref) 11   570 110 1 false(valid-deref) 1.2  90 11   1 false(valid-deref) 46    300 600   1 error(unknown, verification-finished) 1.9   110 26    0 false(valid-deref) 69   1400 560 1 false(valid-deref) 64   1600 570 1 false(valid-deref) 53   1100 460 1
ntdrivers/kbfiltr_false-valid-deref.i.cil.c error (134) .31  38 3.1  0 error (134) .74  22   12    0 false(valid-deref) .38  21   5.6  1 false(valid-deref) 5.6 290 46 1 false(valid-memtrack) 24    380 330   -16 error - divine failed with exitcode 1 1.2 170 14 0 error - divine failed with exitcode 1 1.2 170 16 0 false(valid-deref) 9.0   380 110    0 unknown .80 40 10   0 false(valid-deref) 5.3 290 48 1 false(valid-deref) .40 48 3.2 1 false(valid-deref) 6.8  140 89   1 false(valid-deref) .94  31 13    1 false(valid-deref) 26   830 240 1 false(valid-deref) 25   770 200 1 false(valid-deref) 27   800 230 1
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.5   420 17    2 true .93  31   10    2 true 7.4   140   110    2 true 33   1700 260 2 unknown 1.8  66 21   0 unknown 8.3 430 110 0 error - divine failed with signal 11 1.6 200 20 0 true .54  42 6.6  2 timeout 900    4500 6900   0 true 32   1600 300 2 true 2.2  120 22   2 true 320    320 4300   2 true 1.0   120 13    2 true 12   460 90 2 true 25   690 210 2 true 13   460 90 2
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.4   420 20    2 true .91  31   11    2 true 7.3   140   90    2 true 36   1800 270 2 unknown 1.8  67 21   0 unknown 8.5 430 99 0 error - divine failed with signal 11 1.6 200 22 0 true .54  42 8.3  2 timeout 900    4400 9000   0 true 32   1500 280 2 true 2.3  120 22   2 true 320    320 4000   2 true 1.0   120 11    2 true 12   480 98 2 true 23   810 210 2 true 12   450 90 2
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .47  110 5.2  2 error (42) 880     5600   3100    0 error (42) 880     690   11000    0 timeout (segmentation fault) 900   7300 8700 0 unknown 1.1  67 13   0 unknown 8.4 430 99 0 error - divine failed with signal 11 1.6 200 23 0 true .38  31 4.5  2 timeout 900    4400 7600   0 timeout 900   7400 9500 0 true 65    590 690   2 true 160    220 2200   2 true .44  39 5.1  2 true 11   390 88 2 true 21   790 180 2 true 10   360 77 2
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .35  72 4.1  2 true .22  9.8 2.9  2 true 2.5   100   31    2 true 55   3200 470 2 unknown 1.1  65 14   0 unknown 8.3 430 120 0 error - divine failed with signal 11 1.6 200 19 0 true .21  31 2.3  2 timeout 900    4300 8400   0 true 54   3400 490 2 true 7.1  130 75   2 true 150    220 1700   2 true .39  36 4.5  2 true 8.9 360 68 2 true 14   560 110 2 true 11   380 84 2
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .37  72 3.7  2 true .22  9.8 2.6  2 true 2.5   100   30    2 true 51   3300 480 2 unknown 1.2  66 14   0 unknown 8.5 430 110 0 error - divine failed with signal 11 1.6 200 21 0 true .20  31 2.3  2 timeout 900    4400 7800   0 true 59   3400 560 2 true 7.2  130 71   2 true 150    220 1900   2 true .38  36 4.7  2 true 10   370 85 2 true 14   510 100 2 true 11   370 87 2
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .58  140 6.7  2 true .47  16   7.6  2 true 5.6   180   73    2 true 88   4300 770 2 unknown 1.3  65 17   0 unknown 8.3 430 100 0 error - divine failed with signal 11 1.6 200 23 0 true .31  33 3.8  2 timeout 900    4300 10000   0 true 85   4400 760 2 true 8.2  150 85   2 true 230    270 3100   2 true .53  52 6.6  2 true 11   390 87 2 true 16   530 120 2 true 12   430 88 2
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .55  140 6.3  2 true .46  16   7.1  2 true 5.4   170   66    2 true 92   4300 730 2 unknown 1.4  66 16   0 unknown 8.4 430 98 0 error - divine failed with signal 11 1.6 200 19 0 true .31  33 4.0  2 timeout 900    4300 9300   0 true 89   4400 790 2 true 8.6  170 79   2 true 230    260 3400   2 true .53  52 6.6  2 true 11   430 84 2 true 16   600 130 2 true 11   410 92 2
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .19  26 1.5  2 true .17  6.2 1.8  2 true .54  15   6.9  2 true 7.6 420 67 2 unknown .88 66 8.9 0 unknown 8.2 430 97 0 error - divine failed with signal 11 1.6 200 20 0 true .12  28 1.3  2 killed by signal 9 810    4400 7500   0 true 7.8 430 65 2 true .82 47 8.5 2 true 32    130 520   2 true .24  17 3.1  2 true 8.9 370 65 2 true 12   500 97 2 true 9.3 380 78 2
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .31  47 3.8  2 true .17  9.0 2.1  2 true 1.0   21   14    2 true 19   760 150 2 unknown 1.0  67 12   0 unknown 8.4 430 100 0 error - divine failed with signal 11 1.6 200 18 0 true .16  30 1.9  2 timeout 900    4400 9500   0 true 16   670 120 2 true 1.7  70 16   2 true 62    170 1000   2 true .31  22 5.0  2 true 9.9 380 87 2 true 15   600 120 2 true 10   380 73 2
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .26  47 2.8  2 true .18  8.9 2.0  2 true 1.0   21   13    2 true 19   750 150 2 unknown 1.0  66 12   0 unknown 8.3 430 120 0 error - divine failed with signal 11 1.6 200 20 0 true .15  30 2.0  2 timeout 900    4300 9200   0 true 15   680 120 2 true 2.2  72 22   2 true 64    170 950   2 true .31  22 3.8  2 true 10   380 73 2 true 13   570 110 2 true 9.7 380 82 2
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true .11  24 1.0  2 error (42) 870     870   8100    0 out of memory 140     15000   1600    0 timeout 900   11000 5600 0 unknown .96 65 10   0 unknown 8.3 430 110 0 timeout 900   410 9200 0 true .12  27 1.5  2 timeout 900    3900 8100   0 timeout 920   11000 4700 0 true 170    360 1800   2 true 7.2  87 91   2 true .20  17 2.4  2 true 7.6 360 57 2 true 8.7 360 69 2 true 7.6 350 66 2
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true .12  24 1.2  2 error (42) 880     1000   9200    0 out of memory 130     15000   1600    0 timeout 920   11000 4400 0 unknown 1.0  67 10   0 unknown 8.3 430 110 0 timeout 900   400 8400 0 true .12  27 1.6  2 timeout 900    4300 8500   0 timeout 900   11000 5500 0 true 820    1500 7900   2 true 7.7  85 110   2 true .21  16 2.7  2 true 8.5 370 61 2 true 9.0 370 76 2 true 8.1 370 66 2
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true .12  25 1.2  2 error (42) 880     1200   8300    0 out of memory 130     15000   1800    0 timeout 930   11000 4900 0 unknown 1.1  66 12   0 unknown 8.1 430 120 0 timeout 900   400 8600 0 true .16  27 1.4  2 timeout 900    4300 9600   0 timeout 970   11000 4900 0 timeout 900    1300 8100   0 true 8.4  87 100   2 true .21  16 2.3  2 true 8.2 360 63 2 true 9.3 370 70 2 true 8.0 400 63 2
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true .13  25 1.7  2 error (42) 880     1400   9200    0 out of memory 120     15000   1700    0 timeout 930   11000 4700 0 unknown 1.1  67 10   0 unknown 8.0 430 100 0 timeout 900   400 9000 0 true .14  27 1.7  2 timeout 900    4300 11000   0 timeout 910   11000 4500 0 timeout 900    1100 8100   0 true 11    88 130   2 true .21  16 2.4  2 true 7.9 370 63 2 true 7.6 350 69 2 true 8.3 370 65 2
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true .17  24 1.2  2 error (42) 880     460   9700    0 out of memory 240     15000   3500    0 timeout 920   6300 7900 0 unknown 1.2  71 13   0 unknown 8.3 430 80 0 timeout 900   410 9400 0 true .15  27 2.1  2 timeout 900    4300 11000   0 timeout 900   5400 7600 0 timeout 900    1100 7800   0 true 7.1  87 93   2 true .21  16 2.5  2 true 7.5 340 54 2 true 8.6 370 64 2 true 8.1 360 64 2
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true .13  24 1.1  2 error (42) 880     1400   9300    0 out of memory 100     15000   1200    0 timeout 920   11000 4700 0 unknown 1.1  67 13   0 unknown 8.2 430 95 0 timeout 900   400 9200 0 true .17  27 1.8  2 timeout 900    4300 9900   0 timeout 910   11000 5500 0 timeout 900    1000 9800   0 true 14    87 200   2 true .21  16 2.7  2 true 8.4 370 62 2 true 8.7 360 67 2 true 8.1 370 61 2
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true .13  25 1.1  2 error (42) 880     520   10000    0 out of memory 82     15000   1100    0 timeout 910   4200 7200 0 unknown 1.2  78 12   0 unknown 8.3 430 120 0 timeout 900   410 8000 0 true .16  27 1.8  2 timeout 900    4200 12000   0 timeout 900   4400 7800 0 timeout 900    1100 8300   0 true 7.2  87 87   2 true .21  16 2.6  2 true 8.6 360 68 2 true 9.7 370 74 2 true 8.3 370 69 2
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true .12  25 1.3  2 error (42) 880     460   9000    0 out of memory 83     15000   1200    0 timeout 930   11000 5300 0 unknown 1.2  73 15   0 unknown 8.5 430 110 0 timeout 900   400 10000 0 true .17  27 1.8  2 timeout 900    4300 9800   0 timeout 930   11000 5900 0 timeout 900    960 8000   0 true 24    89 330   2 true .21  16 2.3  2 true 7.1 320 61 2 true 8.3 360 71 2 true 8.3 350 61 2
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true .10  24 .88 2 error (42) 880     950   7600    0 out of memory 130     15000   1800    0 timeout 900   11000 4600 0 unknown .88 65 10   0 unknown 8.4 430 84 0 false(valid-memtrack) 420   480 4600 -16 true .097 26 1.0  2 timeout 900    4300 9300   0 timeout 970   11000 4800 0 true .69 52 5.3 2 true 6.6  82 82   2 true .19  16 2.7  2 true 7.0 340 52 2 true 7.8 360 64 2 true 7.7 370 67 2
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true .13  24 .92 2 error (42) 880     1300   9000    0 out of memory 83     15000   1000    0 timeout 930   11000 5100 0 unknown .89 66 11   0 unknown 8.4 430 98 0 timeout 900   430 8500 0 true .098 26 1.2  2 timeout 900    4300 8200   0 timeout 910   11000 5100 0 true 1.9  42 18   2 true 6.6  78 79   2 true .19  17 2.2  2 true 7.8 360 64 2 true 8.2 370 63 2 true 7.3 340 59 2
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true .11  24 1.0  2 error (42) 880     1500   9500    0 out of memory 89     15000   1200    0 timeout 910   11000 4900 0 unknown .87 66 11   0 unknown 8.2 430 100 0 timeout 900   420 8600 0 true .11  26 1.3  2 timeout 900    3800 9000   0 timeout 900   11000 5100 0 true 6.9  80 67   2 true 6.7  79 76   2 true .22  16 2.5  2 true 8.1 360 60 2 true 8.5 370 61 2 true 7.8 370 67 2
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true .11  24 1.4  2 error (42) 880     580   8600    0 out of memory 110     15000   1500    0 timeout 920   11000 5000 0 unknown .93 65 9.7 0 unknown 8.2 430 110 0 timeout 900   410 9400 0 true .12  26 1.2  2 timeout 900    4300 7800   0 timeout 970   11000 5100 0 true 17    85 160   2 true 6.9  80 82   2 true .21  16 2.5  2 true 7.1 340 53 2 true 8.1 340 59 2 true 8.3 370 64 2
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true .13  24 .87 2 error (42) 870     710   8700    0 out of memory 160     15000   2200    0 timeout 930   11000 5500 0 unknown .95 65 10   0 unknown 8.2 430 100 0 timeout 900   410 8900 0 true .13  26 1.3  2 timeout 900    4300 8000   0 timeout 970   11000 5600 0 true 44    120 490   2 true 7.0  86 75   2 true .20  17 2.1  2 true 7.7 360 64 2 true 8.3 360 77 2 true 7.1 330 58 2
memsafety-ext3/derefAfterFree1_false-valid-deref.c error (134) .15  24 1.3  0 false(valid-deref) .076 7.6 .54 1 false(valid-deref) .068 8.0 .62 1 false(valid-deref) 2.7 240 22 1 false(valid-deref) .15 33 1.6 1 false(valid-deref) 8.3 430 100 1 false(valid-deref) 8.4 430 110 1 false(valid-deref) .084 26 1.0  1 false(valid-deref) .43 83 5.0 1 false(valid-deref) 2.8 250 30 1 false(valid-deref) .25 48 1.4 1 false(valid-deref) 2.8  75 38   1 false(valid-deref) .18  16 1.7  1 false(valid-deref) 8.6 380 69 1 false(valid-deref) 8.0 340 60 1 false(valid-deref) 7.6 360 64 1
memsafety-ext3/derefAfterFree2_false-valid-deref.c error (134) .16  25 1.2  0 false(valid-deref) .21  7.6 1.3  1 false(valid-deref) .17  8.0 1.9  1 false(valid-deref) 2.9 240 29 1 false(valid-deref) 1.6  36 19   1 false(valid-deref) 8.1 430 110 1 false(valid-deref) 8.0 430 110 1 false(valid-deref) .15  26 1.8  1 false(valid-deref) .46 83 5.0 1 false(valid-deref) 3.0 250 26 1 false(valid-deref) .15 34 1.6 1 false(valid-deref) 3.0  82 38   1 false(valid-deref) .17  15 1.8  1 false(valid-deref) 11   460 91 1 false(valid-deref) 40   730 350 1 false(valid-deref) 11   510 83 1
memsafety-ext3/derefInLoop1_false-valid-deref.c error (134) .084 24 .71 0 true .13  6.5 .41 -32 true .073 6.9 .47 -32 false(valid-deref) 2.9 250 22 1 unknown .79 66 8.5 0 true 7.9 370 110 -32 true 8.1 370 93 -32 true .084 26 .83 -32 true 340    4300 3700   -32 false(valid-deref) 2.8 250 28 1 false(valid-deref) .14 35 1.4 1 error (1) .44 24 6.5 0 false(valid-deref) .17  16 1.6  1 false(valid-deref) 8.3 380 71 1 false(valid-deref) 7.6 350 62 1 false(valid-deref) 8.8 390 73 1
memsafety-ext3/getNumbers1_false-valid-deref.c error (134) .089 24 .90 0 true .28  8.1 1.9  -32 true .22  8.8 1.7  -32 false(valid-deref) 3.0 240 28 1 unknown 3.3  68 41   0 false(valid-deref) 8.1 430 94 1 false(valid-deref) 8.2 430 100 1 true .19  26 2.1  -32 unknown 110    4400 1400   0 false(valid-deref) 3.1 250 26 1 false(valid-deref) .26 47 1.8 1 error (1) .45 24 5.6 0 error(unknown, verification-finished) .24  17 2.6  0 false(valid-deref) 14   540 99 1 false(valid-deref) 18   720 140 1 false(valid-deref) 13   490 110 1
memsafety-ext3/getNumbers2_false-valid-deref.c error (134) .082 24 1.0  0 false(valid-deref) .11  7.3 1.1  1 false(valid-deref) .21  7.3 .84 1 false(valid-deref) 3.6 280 29 1 unknown .79 67 8.2 0 false(valid-deref) 8.0 430 89 1 false(valid-deref) 8.1 430 110 1 true .091 26 .82 -32 unknown 110    4400 1100   0 false(valid-deref) 3.5 280 29 1 false(valid-deref) .21 35 1.4 1 error (1) .46 24 6.4 0 false(valid-deref) .18  16 1.8  1 false(valid-deref) 22   550 190 1 false(valid-deref) 60   1100 630 1 false(valid-deref) 25   730 220 1
memsafety-ext3/getNumbers4_false-valid-deref.c error (134) .089 24 .83 0 false(valid-deref) .16  7.0 1.7  1 false(valid-deref) .15  7.3 2.0  1 false(valid-deref) 3.4 250 30 1 unknown 3.9  67 56   0 false(valid-deref) 8.3 430 94 1 false(valid-deref) 8.4 430 110 1 true .21  27 2.4  -32 unknown 110    4400 1100   0 false(valid-deref) 3.4 250 29 1 false(valid-deref) .46 48 1.8 1 error (1) .48 24 5.8 0 false(valid-deref) .18  15 2.0  1 false(valid-deref) 59   770 590 1 false(valid-deref) 320   1100 3400 1 false(valid-deref) 60   900 620 1
memsafety-ext3/naturalNumbers1_false-valid-deref.c error (134) .085 24 .87 0 false(valid-deref) .079 7.0 .69 1 false(valid-deref) .15  6.9 .47 1 false(valid-deref) 2.9 240 29 1 false(valid-deref) .57 35 8.0 1 false(valid-deref) 8.1 430 92 1 false(valid-deref) 8.2 430 100 1 false(valid-deref) .095 26 1.1  1 false(valid-deref) .44 82 5.7 1 false(valid-deref) 2.8 250 29 1 false(valid-deref) .19 35 1.3 1 error (1) .46 23 5.2 0 false(valid-deref) .17  15 1.9  1 true 9.8 390 77 -32 true 11   490 110 -32 true 10   410 92 -32
memsafety-ext3/realloc1_false-valid-deref.c error (134) .19  24 1.4  0 false(valid-deref) .19  7.6 1.9  1 error (134) .12  6.8 .44 0 false(valid-deref) 3.1 240 28 1 false(valid-memtrack) 2.6  36 31   -16 false(valid-deref) 8.3 430 100 1 unknown 1.5 200 18 0 false(valid-memtrack) .20  26 2.4  -16 unknown .74 39 11   0 false(valid-deref) 3.0 250 28 1 false(valid-deref) .15 35 1.3 1 false(valid-deref) 3.4  85 41   1 false(valid-deref) .19  16 3.2  1 false(valid-deref) 15   550 120 1 false(valid-deref) 71   1000 810 1 false(valid-deref) 15   600 130 1
memsafety-ext3/scopes1_false-valid-deref.c false(valid-deref) .097 24 .84 1 false(valid-deref) .064 7.8 .35 1 false(valid-deref) .092 7.7 .27 1 false(valid-deref) 2.9 250 25 1 unknown .82 67 8.5 0 false(valid-deref) 8.2 430 98 1 false(valid-deref) 8.1 430 120 1 true .082 26 .84 -32 true 180    4300 2000   -32 false(valid-deref) 2.8 250 26 1 false(valid-deref) .15 34 1.4 1 error (1) .44 24 5.0 0 false(valid-deref) .16  16 2.0  1 false(valid-deref) 7.8 360 71 0 false(valid-deref) 8.1 350 65 0 false(valid-deref) 7.9 370 57 0
memsafety-ext3/scopes2_false-valid-deref.c false(valid-deref) .11  24 .80 1 false(valid-deref) .057 7.4 .34 1 false(valid-deref) .066 7.2 .38 1 false(valid-deref) 2.7 250 25 1 false(valid-deref) .15 34 1.5 1 false(valid-deref) 8.4 430 98 1 false(valid-deref) 8.5 430 120 1 false(valid-deref) .11  26 .96 1 false(valid-deref) .45 83 5.7 1 false(valid-deref) 2.7 250 27 1 false(valid-deref) .36 48 1.3 1 error (1) .45 24 5.4 0 false(valid-deref) .22  18 2.5  1 false(valid-deref) 7.6 350 60 1 false(valid-deref) 7.4 350 55 1 false(valid-deref) 8.1 370 61 1
memsafety-ext3/scopes3_false-valid-deref.c error (134) .091 24 .68 0 false(valid-deref) .12  7.1 1.0  0 false(valid-deref) .12  7.5 1.2  0 false(valid-deref) 3.0 250 27 1 unknown .79 65 8.2 0 false(valid-deref) 8.1 430 100 1 false(valid-deref) 8.2 430 120 1 true .11  26 .90 -32 true 370    4300 4000   -32 false(valid-deref) 3.1 250 26 1 false(valid-deref) .15 34 1.2 1 error (1) .44 24 6.2 0 false(valid-deref) .16  16 2.0  1 false(valid-deref) 12   480 110 1 false(valid-deref) 13   500 110 1 false(valid-deref) 13   570 120 1
memsafety-ext3/scopes4_false-valid-deref.c error (134) .091 24 .79 0 false(valid-deref) .066 11   .76 1 false(valid-deref) .073 11   .56 1 false(valid-deref) 2.7 250 24 1 unknown .83 67 8.4 0 false(valid-deref) 8.0 430 96 1 false(valid-deref) 8.1 430 110 1 true .078 26 .97 -32 unknown 150    4400 1500   0 false(valid-deref) 2.8 250 29 1 false(valid-deref) .19 34 1.3 1 error (1) .45 24 6.2 0 false(valid-deref) .16  16 1.9  1 false(valid-deref) 8.7 370 66 1 false(valid-deref) 8.6 370 72 1 false(valid-deref) 8.6 370 67 1
memsafety-ext3/scopes5_false-valid-deref.c error (134) .085 24 .77 0 false(valid-deref) .060 7.1 .39 0 false(valid-deref) .12  7.1 .29 0 false(valid-deref) 2.8 250 28 1 unknown .81 67 8.6 0 false(valid-deref) 8.1 430 93 1 false(valid-deref) 8.2 430 110 1 true .081 26 .86 -32 true 500    4300 5300   -32 false(valid-deref) 2.7 250 29 1 false(valid-deref) .29 48 1.6 1 error (1) .47 24 5.6 0 false(valid-deref) .15  16 2.0  1 false(valid-deref) 7.7 350 67 1 false(valid-deref) 7.6 370 67 1 false(valid-deref) 6.9 330 57 1
memsafety-ext3/freeAlloca_false-valid-free.c error (134) .16  24 1.6  0 false(valid-free) .24  9.0 1.5  0 true .24  9.1 2.8  -32 false(valid-free) 2.9 250 29 1 unknown 3.1  68 37   0 unknown 8.2 430 92 0 false(valid-memtrack) 8.3 430 110 -16 false(valid-free) .15  26 2.1  1 false(valid-free) .83 86 12   1 false(valid-free) 3.0 250 30 1 false(valid-free) .32 47 1.8 1 error (1) .45 24 5.8 0 error(unknown, verification-finished) .23  18 2.8  0 true 13   430 140 -32 true 27   680 290 -32 true 17   480 160 -32
memsafety-ext3/getNumbers1_true-valid-memsafety.c error (134) .093 24 .67 0 true .10  6.6 .81 2 true .093 6.5 .64 2 true 3.0 250 29 2 unknown 2.7  68 37   0 true 8.3 370 100 2 true 8.2 370 120 2 true .12  26 1.0  2 true 200    4300 2000   2 true 3.0 250 27 2 true .18 35 1.4 2 error (1) .46 24 5.6 0 true .14  15 1.4  2 true 12   530 110 2 true 25   800 230 2 true 12   500 94 2
memsafety-ext3/getNumbers3_true-valid-memsafety.c error (134) .091 24 .69 0 true .096 6.2 .80 2 true .080 6.3 .79 2 true 3.1 270 29 2 unknown .80 65 8.6 0 true 8.3 370 110 2 true 8.1 370 110 2 true .085 26 .88 2 true 160    4300 1900   2 true 3.2 280 32 2 true .18 35 1.2 2 error (1) .45 24 6.6 0 true .14  15 1.5  2 true 9.5 400 73 2 true 11   540 100 2 true 10   470 94 2
memsafety-ext3/getNumbers4_true-valid-memsafety.c error (134) .086 24 .71 0 true .16  6.5 1.8  2 true .17  6.2 1.4  2 true 3.4 250 32 2 unknown 4.0  68 57   0 true 8.2 370 92 2 true 8.3 370 94 2 true .20  27 2.5  2 true 140    4400 1100   2 true 3.4 250 33 2 true .29 35 2.3 2 error (1) .48 24 5.9 0 true .15  16 1.9  2 true 45   1100 480 2 timeout 900   1100 7100 0 true 44   1100 400 2
memsafety-ext3/scopes4_true-valid-memsafety.c error (134) .10  24 .72 0 true .11  6.0 .33 2 true .074 6.0 .32 2 true 2.8 250 23 2 unknown .80 66 9.1 0 true 8.2 370 93 2 true 8.2 370 130 2 true .087 26 .82 2 true 200    4400 1800   2 true 2.7 240 25 2 true .14 34 1.3 2 error (1) .51 24 6.5 0 true .13  17 1.6  2 true 11   400 79 2 true 11   410 95 2 true 15   530 120 2
pthread-memsafety/fillarray1_false-valid-deref.i error (134) .19  28 1.8  0 error (6) .096 7.7 1.3  0 false(valid-free) .12  11   1.3  -16 error 4.4 290 41 0 false(valid-deref) .21 35 2.5 1 unknown 8.4 450 120 0 unknown 1.6 200 21 0 false(valid-deref) .15  27 1.8  1 unknown .94 81 11   0 error 4.3 280 36 0 unknown .26 50 1.6 0 error (1) 1.2  35 15   0 unknown .089 14 1.0  0 error (7) 17   360 120 0 error (7) 16   370 140 0 false(valid-deref) 16   680 120 0
pthread-memsafety/fillarray_false-valid-deref.i error (134) .22  28 2.0  0 error (6) .098 8.0 1.2  0 false(valid-free) .13  10   1.6  -16 error 4.2 280 36 0 false(valid-deref) .21 35 2.6 1 unknown 8.3 450 96 0 unknown 1.6 200 20 0 false(valid-deref) .14  27 1.7  1 unknown 1.0  84 14   0 error 4.3 280 36 0 unknown .15 38 1.4 0 error (1) 1.0  37 15   0 unknown .086 15 .93 0 error (7) 17   370 140 0 error (7) 15   370 120 0 false(valid-deref) 15   500 120 0
pthread-memsafety/list1_false-valid-deref.i error (5) .34  29 4.1  0 error (6) .11  7.8 1.3  0 false(valid-deref) .17  10   1.4  0 error 4.2 280 39 0 unknown 900    5500 9600   0 false(valid-memtrack) 8.5 450 100 -16 false(valid-memtrack) 8.9 450 92 -16 unknown .13  27 1.2  0 false(valid-memtrack) .47 83 5.6 -16 error 4.3 280 36 0 unknown .15 36 1.2 0 error (1) 1.1  37 15   0 unknown .11  19 1.2  0 error (7) 17   390 140 0 error (7) 16   360 140 0 unknown 60   820 580 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 48 820    17000 5800   49 48 12000    19000 120000   -26 48 2600    200000 33000   -91 48 14000 170000 94000 42 48 1100   9000 12000 -26 48 380   20000 4700 -28 48 11000   16000 110000 -77 48 940    2700 12000   -209 48 24000    160000 240000   -130 48 14000 170000 97000 42 48 7500   12000 72000 58 48 2700 5900 30000 52 48 28   1200 370 69 48 1500 22000 15000 3 48 2900 28000 25000 1 48 1600 25000 17000 3
    correct results 26 7.9  1900 89   49 25 24    1000 340   38 24 110    1700 1100   37 29 470 26000 4000 42 6 2.9 210 35 6 16 130   6600 1600 20 15 120   6200 1700 19 36 25    1400 350   63 10 700    18000 6900   14 29 460 26000 4100 42 37 1200   4700 12000 58 29 1900 4200 25000 52 42 25   1000 340 69 40 550 18000 4700 67 39 980 22000 9300 65 40 550 19000 4700 67
        correct true 23 7.6  1800 86   46 13 4.2  160 51   26 13 34    920 430   26 13 410 22000 3500 26 0 4 33   1500 390 8 4 33   1500 450 8 27 5.2  780 62   54 4 700    17000 6800   8 13 400 21000 3600 26 21 1200   4000 12000 42 23 1800 3400 24000 46 27 8.4 780 100 54 27 290 11000 2300 54 26 330 13000 2700 52 27 290 11000 2400 54
        correct false 3 .32 71 2.8 3 12 20    840 290   12 11 81    810 630   11 16 58 4300 520 16 6 2.9 210 35 6 12 98   5200 1200 12 11 90   4700 1200 11 9 20    580 290   9 6 3.1  500 40   6 16 58 4400 550 16 16 4.9 700 35 16 6 65 770 850 6 15 17   260 240 15 13 270 7400 2300 13 13 650 9200 6600 13 13 260 7500 2300 13
    correct-unconfimed results 0 3 .42 23 2.9 0 3 .41 25 2.9 0 0 1 5.7 390 74 0 0 0 1 9.0  380 110   0 0 0 0 0 0 2 16 710 130 0 2 18 730 140 0 4 48 1900 360 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 3 .42 23 2.9 0 3 .41 25 2.9 0 0 1 5.7 390 74 0 0 0 1 9.0  380 110   0 0 0 0 0 0 2 16 710 130 0 2 18 730 140 0 4 48 1900 360 0
    incorrect results 0 2 .41 15 2.3 -64 5 .78 45 7.8 -128 0 2 27   410 360 -32 2 16   820 210 -48 5 460   2100 5000 -96 9 1.1  230 12   -272 5 1400    17000 15000   -144 0 0 0 0 2 23 830 220 -64 2 38 1200 400 -64 2 27 890 260 -64
        incorrect true 0 2 .41 15 2.3 -64 3 .53 25 4.9 -96 0 0 1 7.9 370 110 -32 1 8.1 370 93 -32 8 .92 210 9.7 -256 4 1400    17000 15000   -128 0 0 0 0 2 23 830 220 -64 2 38 1200 400 -64 2 27 890 260 -64
        incorrect false 0 0 2 .25 21 2.9 -32 0 2 27   410 360 -32 1 8.5 450 100 -16 4 450   1800 4900 -64 1 .20 26 2.4 -16 1 .47 83 5.6 -16 0 0 0 0 0 0 0
score (48 tasks, max score: 75) 49 -26 -91 42 -26 -28 -77 -209 -130 42 58 52 69 3 1 3
Run set 2ls.sv-comp19_prop-memsafety.MemSafety-Other cbmc.sv-comp19_prop-memsafety.MemSafety-Other cbmc-path.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other depthk.sv-comp19_prop-memsafety.MemSafety-Other divine-explicit.sv-comp19_prop-memsafety.MemSafety-Other divine-smt.sv-comp19_prop-memsafety.MemSafety-Other esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other map2check.sv-comp19_prop-memsafety.MemSafety-Other pesco.sv-comp19_prop-memsafety.MemSafety-Other predatorhp.sv-comp19_prop-memsafety.MemSafety-Other smack.sv-comp19_prop-memsafety.MemSafety-Other symbiotic.sv-comp19_prop-memsafety.MemSafety-Other uautomizer.sv-comp19_prop-memsafety.MemSafety-Other ukojak.sv-comp19_prop-memsafety.MemSafety-Other utaipan.sv-comp19_prop-memsafety.MemSafety-Other