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-Other cbmc.sv-comp18.MemSafety-Other cpa-bam-bnb.sv-comp18.MemSafety-Other cpa-bam-slicing.sv-comp18.MemSafety-Other cpa-seq.sv-comp18.MemSafety-Other depthk.sv-comp18.MemSafety-Other esbmc-incr.sv-comp18.MemSafety-Other esbmc-kind.sv-comp18.MemSafety-Other map2check.sv-comp18.MemSafety-Other predatorhp.sv-comp18.MemSafety-Other symbiotic.sv-comp18.MemSafety-Other uautomizer.sv-comp18.MemSafety-Other ukojak.sv-comp18.MemSafety-Other utaipan.sv-comp18.MemSafety-Other
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
loop-acceleration/array3_false-valid-deref.i out of memory 640    15000 3900    0 false(valid-deref) 19    1000 250   0 error (1) .49 40 4.3 0 error (1) .46 40 4.2 0 false(valid-deref) 550   3600 6300 1 unknown 54   27 680 0 false(valid-deref) 69    380 790   0 false(valid-deref) 72     370 620    0 unknown 890     33 11000    0 timeout 900    86 9600   0 false(valid-deref) 7.4  15 92   1 timeout 900   4400 12000 0 timeout 900   5200 12000 0 timeout 900   1500 11000 0
ntdrivers/floppy_false-valid-deref.i.cil.c error (134) 23    110 290    0 false(valid-deref) 4.6  210 55   0 error (1) .48 40 4.1 0 error (1) .47 40 4.1 0 false(valid-deref) 7.4 510 65 1 false(valid-deref) 130   790 940 0 unknown 17    510 200   0 timeout 900     1100 12000    0 unknown .15  19 1.6  0 false(valid-deref) 1.2  83 10   1 false(valid-deref) 130    6100 1600   1 unknown 4.6 250 41 0 unknown 4.6 250 39 0 unknown 4.6 260 40 0
ntdrivers/kbfiltr_false-valid-deref.i.cil.c error (134) 1.1  36 13    0 error (6) 1.1  44 12   0 error (1) .49 40 4.0 0 error (1) .45 40 4.0 0 false(valid-deref) 3.9 270 36 1 false(valid-deref) 740   1100 7100 0 unknown 16    370 210   0 unknown 16     370 210    0 unknown .069 15 .85 0 false(valid-deref) .34 41 3.8 1 false(valid-deref) 7.3  880 100   1 unknown 4.0 230 34 0 unknown 4.0 230 39 0 unknown 3.9 230 31 0
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.3  420 15    2 true 1.8  42 20   2 error (1) .50 41 4.6 0 error (1) .45 40 4.0 0 true 37   1800 240 2 true 75   4000 930 2 true .57 44 6.9 2 true .54  44 6.7  2 unknown 900     330 11000    0 true 2.9  86 28   2 true .55 29 6.4 2 true 8.0 480 64 2 true 17   760 130 2 true 7.6 470 64 2
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.3  420 14    2 true 1.8  42 21   2 error (1) .49 40 4.4 0 error (1) .41 40 3.9 0 true 31   1900 210 2 true 79   3900 950 2 true .55 44 8.1 2 true .55  44 6.7  2 unknown 890     330 10000    0 true 2.8  86 26   2 true .53 28 5.7 2 true 7.5 460 57 2 true 17   760 140 2 true 7.7 460 60 2
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .51 110 4.4  2 error (42) 880    5200 4600   0 error (1) .46 40 4.0 0 error (1) .43 40 4.1 0 timeout 900   7700 8700 0 timeout 900   4800 14000 0 timeout 900    1200 12000   0 true .28  31 3.1  2 unknown 900     230 10000    0 true 62    560 670   2 true .38 19 4.6 2 true 6.1 350 50 2 true 14   770 130 2 true 6.5 350 51 2
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .37 73 3.1  2 true .71 36 7.6 2 error (1) .50 40 4.1 0 error (1) .43 41 4.1 0 true 50   4000 410 2 true 68   4000 680 2 true .23 31 2.2 2 true .23  31 2.2  2 unknown 890     170 11000    0 true 7.0  120 64   2 true .63 20 6.7 2 true 6.3 340 53 2 true 9.5 470 83 2 true 5.9 350 52 2
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .34 74 3.3  2 true .73 36 8.5 2 error (1) .49 41 4.4 0 error (1) .45 40 4.0 0 true 46   3600 390 2 true 66   4000 640 2 true .19 31 2.9 2 true .20  31 2.4  2 unknown 890     170 11000    0 true 7.1  120 62   2 true .61 20 8.3 2 true 6.1 340 55 2 true 9.7 470 78 2 true 6.3 350 51 2
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .53 140 6.4  2 true 1.1  38 12   2 error (1) .45 40 4.3 0 error (1) .45 40 4.6 0 true 80   4200 780 2 true 130   4400 1200 2 true .31 33 3.9 2 true .31  33 4.3  2 unknown 900     220 11000    0 true 9.5  130 87   2 true 1.3  30 17   2 true 7.1 400 52 2 true 11   580 92 2 true 7.3 410 60 2
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .52 140 5.9  2 true 1.1  38 12   2 error (1) .46 41 4.5 0 error (1) .45 40 4.2 0 true 80   4400 580 2 true 130   4300 1200 2 true .32 34 4.2 2 true .34  33 4.5  2 unknown 900     210 8600    0 true 10    150 97   2 true 1.4  29 19   2 true 7.2 400 63 2 true 11   550 99 2 true 6.6 400 53 2
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .19 27 1.4  2 true .53 34 5.3 2 error (1) .48 40 4.6 0 error (1) .43 40 3.7 0 true 6.7 350 56 2 true 9.3 610 80 2 true .13 29 1.3 2 true .13  29 1.3  2 true 310     30 3800    2 true 1.7  46 19   2 true .26 11 3.2 2 true 5.3 280 47 2 true 7.7 470 65 2 true 5.3 280 39 2
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .24 47 3.4  2 true .65 36 6.4 2 error (1) .50 45 4.8 0 error (1) .46 40 4.2 0 true 15   690 130 2 true 24   2000 210 2 true .17 31 2.0 2 true .18  30 2.0  2 unknown .047 12 .42 0 true 2.7  64 30   2 true .30 14 4.3 2 true 6.2 320 47 2 true 9.7 470 82 2 true 6.1 320 47 2
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .29 47 2.2  2 true .68 36 6.0 2 error (1) .49 42 4.5 0 error (1) .45 40 4.1 0 true 14   700 110 2 true 23   1800 210 2 true .15 30 1.9 2 true .17  30 1.5  2 unknown .071 12 .44 0 true 2.7  64 30   2 true .32 14 4.0 2 true 5.9 320 49 2 true 10   470 75 2 true 5.9 320 47 2
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true .12 26 1.1  2 error (42) 870    3100 5100   0 error (1) .46 41 4.6 0 error (1) .43 40 4.2 0 timeout 930   11000 5000 0 timeout 900   7100 11000 0 timeout 900    2100 8900   0 true .13  27 .96 2 unknown 900     360 8400    0 true 190    350 1800   2 true .22 11 2.5 2 true 4.1 240 36 2 true 4.8 260 42 2 true 4.1 250 34 2
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true .13 25 1.1  2 error (42) 870    3700 6700   0 error (1) .47 40 4.6 0 error (1) .44 41 4.3 0 timeout 920   11000 5000 0 timeout 900   7200 11000 0 timeout 900    2200 7600   0 true .10  27 1.0  2 unknown 900     430 8100    0 timeout 900    1600 8600   0 true .22 11 2.3 2 true 4.5 250 37 2 true 5.0 260 46 2 true 4.5 250 37 2
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true .13 25 1.1  2 error (42) 870    4300 6200   0 error (1) .49 40 4.3 0 error (1) .44 40 4.0 0 timeout 910   11000 4900 0 timeout 910   7100 11000 0 timeout 900    2300 9600   0 true .12  27 1.1  2 unknown 900     600 7200    0 timeout 900    1300 9600   0 true .20 11 2.2 2 true 4.3 240 39 2 true 5.1 270 45 2 true 4.3 250 35 2
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true .16 26 .98 2 error (42) 870    1400 5900   0 error (1) .49 44 4.8 0 error (1) .44 40 4.4 0 timeout 930   11000 4800 0 timeout 900   7000 10000 0 timeout 900    2300 8600   0 true .10  27 1.5  2 unknown 900     1000 6500    0 timeout 900    1100 7700   0 true .22 11 2.7 2 true 4.4 250 36 2 true 5.1 270 41 2 true 4.5 250 36 2
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true .12 28 1.2  2 error (42) 870    1800 7300   0 error (1) .46 40 4.4 0 error (1) .43 41 4.3 0 timeout 900   10000 7100 0 timeout 900   3800 13000 0 timeout 900    2500 11000   0 true .12  27 1.2  2 unknown 900     500 12000    0 timeout 900    1300 9600   0 true .22 11 2.4 2 true 4.3 250 37 2 true 5.1 270 43 2 true 4.4 240 38 2
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true .15 27 1.0  2 error (42) 870    1600 6000   0 error (1) .46 41 4.5 0 error (1) .45 40 4.0 0 timeout 920   11000 4800 0 timeout 900   6800 10000 0 timeout 900    2400 7400   0 true .11  27 1.2  2 unknown 900     1200 5300    0 timeout 900    950 8400   0 true .22 11 2.9 2 true 4.2 240 38 2 true 5.1 270 45 2 true 4.3 250 34 2
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true .15 26 1.1  2 error (42) 870    2000 9300   0 error (1) .48 41 4.5 0 error (1) .42 40 3.8 0 timeout 900   4500 6800 0 timeout 900   3700 12000 0 timeout 900    2500 7100   0 true .15  27 1.4  2 unknown 900     990 11000    0 timeout 900    1100 8300   0 true .22 11 2.2 2 true 4.4 250 36 2 true 5.4 280 46 2 true 4.7 250 36 2
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true .15 26 1.0  2 error (42) 870    1800 6400   0 error (1) .49 40 4.1 0 error (1) .45 40 4.4 0 timeout 920   11000 5300 0 timeout 900   6700 9900 0 timeout 900    2500 8000   0 true .12  27 1.3  2 unknown 900     1500 6300    0 timeout 900    930 8300   0 true .20 11 2.4 2 true 4.5 250 35 2 true 5.5 290 48 2 true 4.3 250 32 2
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true .13 23 .75 2 error (42) 870    1300 5800   0 error (1) .46 40 4.6 0 error (1) .47 40 3.9 0 timeout 930   11000 4900 0 timeout 910   8300 9200 0 timeout 900    1600 8200   0 true .10  27 .95 2 unknown 900     190 7500    0 true .78 28 9.3 2 true .19 11 2.0 2 true 4.2 240 39 2 true 4.3 250 38 2 true 5.9 320 45 2
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true .14 24 .85 2 error (42) 870    1500 6100   0 error (1) .47 40 3.9 0 error (1) .44 40 3.6 0 timeout 900   11000 5300 0 timeout 900   9100 10000 0 timeout 900    1800 11000   0 true .088 27 1.1  2 unknown 900     230 8500    0 true 3.5  34 28   2 true .19 11 2.3 2 true 4.0 230 37 2 true 4.5 250 36 2 true 4.2 250 35 2
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true .14 24 .77 2 error (42) 870    1700 5500   0 error (1) .47 40 4.2 0 error (1) .45 40 4.0 0 timeout 920   11000 4800 0 timeout 910   8400 9100 0 timeout 900    1900 8700   0 true .11  27 1.0  2 unknown 900     240 11000    0 true 12    60 110   2 true .21 11 2.5 2 true 4.2 250 37 2 true 4.4 250 39 2 true 4.4 250 35 2
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true .14 26 .89 2 error (42) 870    2100 7300   0 error (1) .49 42 4.1 0 error (1) .46 41 4.1 0 timeout 930   11000 4400 0 timeout 900   8300 11000 0 timeout 900    2000 9000   0 true .091 27 .75 2 unknown 900     270 9300    0 true 20    77 190   2 true .21 11 2.6 2 true 4.4 250 35 2 true 4.6 260 38 2 true 4.3 250 37 2
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true .13 24 1.1  2 error (42) 870    2600 7800   0 error (1) .49 40 4.2 0 error (1) .48 41 4.0 0 timeout (exception) 920   11000 5000 0 timeout 900   7700 9900 0 timeout 900    2000 9000   0 true .098 27 .99 2 unknown 900     310 8300    0 true 64    140 600   2 true .21 11 2.2 2 true 4.4 250 39 2 true 4.9 260 44 2 true 4.4 250 34 2
../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 26 670   17000 4300 46 26 12000   36000 91000 18 26 12 1100 110 0 26 12 1000 110 0 26 14000 170000 86000 21 26 14000 130000 170000 18 26 13000   31000 130000 18 26 990   2500 13000 46 26 19000 9700 200000 2 26 7600   11000 74000 34 26 150   7400 1900 49 26 1000 12000 13000 46 26 1100 15000 13000 46 26 1000 9000 12000 46
    correct results 23 7.3 1800 72 46 9 9.1 340 99 18 0 0 12 920 26000 9300 21 9 600 29000 6100 18 9 2.6 310 33 18 23 4.4 690 49 46 1 310 30 3800 2 18 400   2200 3900 34 26 150   7400 1900 49 23 120 6900 1000 46 23 180 9200 1500 46 23 120 7000 990 46
        correct true 23 7.3 1800 72 46 9 9.1 340 99 18 0 0 9 360 22000 2900 18 9 600 29000 6100 18 9 2.6 310 33 18 23 4.4 690 49 46 1 310 30 3800 2 16 400   2100 3900 32 23 9.0 360 110 46 23 120 6900 1000 46 23 180 9200 1500 46 23 120 7000 990 46
        correct false 0 0 0 0 3 560 4400 6400 3 0 0 0 0 2 1.5 120 14 2 3 150   7000 1800 3 0 0 0
    correct-unconfimed results 0 2 24   1200 310 0 0 0 0 2 870 1900 8000 0 1 69   380 790 0 1 72   370 620 0 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 2 24   1200 310 0 0 0 0 2 870 1900 8000 0 1 69   380 790 0 1 72   370 620 0 0 0 0 0 0 0
    incorrect results 0 0 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 0 0 0 0 0 0 0 0 0 0 0 0 0
score (26 tasks, max score: 49) 46 18 0 0 21 18 18 46 2 34 49 46 46 46
Run set 2ls.sv-comp18.MemSafety-Other cbmc.sv-comp18.MemSafety-Other cpa-bam-bnb.sv-comp18.MemSafety-Other cpa-bam-slicing.sv-comp18.MemSafety-Other cpa-seq.sv-comp18.MemSafety-Other depthk.sv-comp18.MemSafety-Other esbmc-incr.sv-comp18.MemSafety-Other esbmc-kind.sv-comp18.MemSafety-Other map2check.sv-comp18.MemSafety-Other predatorhp.sv-comp18.MemSafety-Other symbiotic.sv-comp18.MemSafety-Other uautomizer.sv-comp18.MemSafety-Other ukojak.sv-comp18.MemSafety-Other utaipan.sv-comp18.MemSafety-Other