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 04:52:43 CET [[ 2017-01-15 00:23:14 CET ]] [[ 2017-01-15 00:35:58 CET ]] [[ 2017-01-15 00:29:47 CET ]] [[ 2017-01-15 00:40:29 CET ]]
Run set sv-comp17.MemSafety-Other
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.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 true -32 wit inspect .61 .61 7.3 80 2.0  0   error (invalid witness file) .50 .34 7.7 40 error (invalid witness file) 5.6 3.1 100 290 - -
ntdrivers/floppy_false-valid-deref.i.cil.c timeout 0 wit inspect 900    900    12000   250 .84 0   error (invalid witness file) .51 .33 7.5 40 error (invalid witness file) 7.6 4.0 130 320 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 17    17    190   1000 1.7  0   error (invalid witness file) .47 .32 5.7 41 error (invalid witness file) 6.6 3.5 120 310 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .89 .89 10   50 1.7  0   - - error (invalid witness file) .50 .35 6.7 40 error (invalid witness file) 7.3 3.8 130 320
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .89 .89 11   50 1.7  0   - - error (invalid witness file) .52 .34 9.0 41 error (invalid witness file) 6.2 3.3 120 310
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.0  1.0  12   120 1.7  0   - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 6.3 3.3 120 300
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .39 .39 4.7 36 1.7  0   - - error (invalid witness file) .52 .34 12   41 error (invalid witness file) 6.5 3.4 120 300
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.5  1.5  4.7 36 1.7  0   - - error (invalid witness file) .49 .31 11   39 error (invalid witness file) 5.5 2.9 99 290
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .54 .54 7.3 44 1.7  0   - - error (invalid witness file) .57 .38 9.8 44 error (invalid witness file) 6.4 3.4 130 310
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .54 .54 6.8 43 1.7  0   - - error (invalid witness file) .51 .33 9.7 40 error (invalid witness file) 6.3 3.3 130 300
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .22 .21 2.2 25 1.7  0   - - error (invalid witness file) .51 .33 7.2 41 error (invalid witness file) 5.7 3.1 110 300
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .26 .26 3.6 27 1.7  0   - - error (invalid witness file) .51 .33 4.2 39 error (invalid witness file) 6.1 3.2 120 310
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .28 .28 3.3 27 1.7  0   - - error (invalid witness file) .48 .32 3.9 41 error (invalid witness file) 6.3 3.3 120 300
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 87    87    970   15000 2.0  0   - - error (invalid witness file) .50 .33 3.8 40 error (invalid witness file) 6.3 3.3 120 310
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 92    92    1300   15000 2.0  0   - - error (invalid witness file) .49 .30 6.3 39 error (invalid witness file) 7.2 3.8 130 330
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 97    96    1100   15000 2.0  0   - - error (invalid witness file) .51 .32 10   40 error (invalid witness file) 5.7 3.1 110 290
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 100    100    1300   15000 2.0  0   - - error (invalid witness file) .47 .32 4.1 39 error (invalid witness file) 5.8 3.1 110 300
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 110    110    1100   15000 1.7  0   - - error (invalid witness file) .48 .33 6.9 39 error (invalid witness file) 5.7 3.0 100 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 110    110    1500   15000 2.0  0   - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 5.9 3.1 100 300
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 110    110    1400   15000 1.7  0   - - error (invalid witness file) .50 .34 8.1 40 error (invalid witness file) 6.0 3.2 120 290
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 110    110    1200   15000 2.0  0   - - error (invalid witness file) .51 .35 4.5 40 error (invalid witness file) 5.5 3.0 100 300
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 140    140    1500   8700 2.0  0   - - error (invalid witness file) .49 .32 7.7 39 error (invalid witness file) 6.1 3.2 120 300
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 200    200    2400   12000 2.0  0   - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.2 3.3 120 290
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 78    78    850   15000 2.0  0   - - error (invalid witness file) .49 .32 3.5 39 error (invalid witness file) 5.6 3.0 130 290
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 79    79    990   15000 2.0  0   - - error (invalid witness file) .49 .32 7.9 40 error (invalid witness file) 6.1 3.2 130 300
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 83    83    930   15000 1.7  0   - - error (invalid witness file) .49 .33 4.6 39 error (invalid witness file) 6.0 3.2 120 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 -7 2300    2300    29000   190000 46   0   26 1.5  .99 21   120   26 20   11   360 920   26 12   7.6 180 920   26 140 75 2700 7000  
    correct results 13 25 370    370    4200   22000 22   0   0 .47 .32 5.7 41   0 6.6 3.5 120 310   0 6.1 4.0 110 480   0 75 40 1400 3600  
        correct true 12 24 350    350    4000   21000 21   0   0 0    0    0   0   0 0   0   0 0   0 6.1 4.0 110 480   0 75 40 1400 3600  
        correct false 1 1 17    17    190   1000 1.7 0   0 .47 .32 5.7 41   0 6.6 3.5 120 310   0 0   0   0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 1 -32 .61 .61 7.3 80 2.0 0   0 .50 .34 7.7 40   0 5.6 3.1 100 290   0 0   0   0 0   0 0 0 0 0  
        incorrect true 1 -32 .61 .61 7.3 80 2.0 0   0 .50 .34 7.7 40   0 5.6 3.1 100 290   0 0   0   0 0   0 0 0 0 0  
        incorrect false 0
score (26 tasks, max score: 49) -7
Run set sv-comp17.MemSafety-Other