Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-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-01-13 06:35:22 CET [[ 2017-01-15 01:30:25 CET ]] [[ 2017-01-15 01:30:43 CET ]] [[ 2017-01-15 01:30:33 CET ]] [[ 2017-01-15 01:30:54 CET ]]
Run set sv-comp17.MemSafety-Other
Options -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
loop-acceleration/array3_false-valid-deref.i 0 .075 .075 .81 23 .99 0   .54 .36 12   39 5.7 3.1 120 300
ntdrivers/floppy_false-valid-deref.i.cil.c 0 900     900     11000    230 .84 0   .49 .31 10   39 7.3 3.8 150 320
ntdrivers/kbfiltr_false-valid-deref.i.cil.c 1 320     320     3400    530 .84 0   .60 .38 9.3 42 5.4 2.9 120 290
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .79  .79  9.5  45 .99 0   .48 .32 11   39 7.0 3.7 120 330
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .77  .77  8.9  45 .84 0   .54 .36 12   41 6.4 3.4 140 290
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .75  .75  10    37 .91 0   .49 .31 10   39 6.1 3.2 130 300
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .26  .26  3.2  28 .84 0   .58 .38 11   43 5.9 3.1 120 300
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .30  .30  3.1  28 .99 0   .50 .31 10   41 5.6 3.0 120 290
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .43  .43  5.0  30 .99 0   .57 .40 12   40 6.4 3.4 130 300
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .44  .44  4.1  30 .99 0   .48 .31 10   39 6.3 3.3 120 290
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .12  .12  1.5  25 .99 0   .53 .34 11   39 6.3 3.3 120 300
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .22  .22  2.2  27 .99 0   .53 .34 9.8 40 5.6 3.0 66 300
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .19  .19  2.3  27 .99 0   .52 .33 12   40 6.9 3.6 94 310
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 .11  .11  1.3  24 .99 0   .58 .37 9.2 39 5.8 3.2 120 280
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13  .12  1.3  24 .99 0   .49 .32 10   39 6.1 3.2 120 300
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 .14  .14  1.6  24 .99 0   .50 .32 12   39 6.0 3.2 120 290
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 .15  .15  1.6  24 .99 0   .52 .34 11   41 6.4 3.4 120 310
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 2 .15  .14  1.6  24 .99 0   .50 .31 12   41 6.2 3.3 120 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 .16  .16  1.5  24 .99 0   .49 .32 11   40 5.8 3.1 120 300
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 2 .18  .17  1.6  24 .99 0   .56 .37 12   41 5.7 3.0 120 300
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 .15  .15  1.8  24 .84 0   .50 .32 11   40 5.7 3.0 110 290
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 .087 .087 1.0  23 .84 0   .53 .33 12   40 6.0 3.2 130 300
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 .12  .12  .90 23 .99 0   .53 .36 13   39 6.1 3.2 120 300
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13  .13  1.0  24 .99 0   .50 .33 12   40 5.9 3.1 130 290
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 .11  .11  1.0  24 .99 0   .51 .33 9.4 40 6.2 3.2 120 310
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 .10  .10  1.4  24 .84 0   .50 .32 10   39 7.2 3.9 80 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 26 47 1200   1200   15000 1400 25    0   26 1.6  1.1  32   120   26 18   9.8 390 910   26 12 7.7 250 920   26 140 75 2700 6900  
    correct results 24 47 330   330   3500 1200 23    0   0 .60 .38 9.3 42   0 5.4 2.9 120 290   0 12 7.7 250 920   0 140 75 2700 6900  
        correct true 23 46 6.0 6.0 68 630 22    0   0 0    0    0   0   0 0   0   0 0   0 12 7.7 250 920   0 140 75 2700 6900  
        correct false 1 1 320   320   3400 530 .84 0   0 .60 .38 9.3 42   0 5.4 2.9 120 290   0 0 0   0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (26 tasks, max score: 49) 47
Run set sv-comp17.MemSafety-Other