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 05:20:12 CET [[ 2017-01-15 00:51:08 CET ]] [[ 2017-01-15 01:00:54 CET ]] [[ 2017-01-15 00:55:05 CET ]] [[ 2017-01-15 01:06:26 CET ]]
Run set sv-comp17.MemSafety-Other
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.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 false(valid-deref) 1 wit inspect 300   290   4100 690 .84 0   error (invalid witness file) .57 .37 14 44 error (invalid witness file) 5.5 3.0 91 300 - -
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 5.1 5.1 60 410 .84 0   error (invalid witness file) .50 .34 11 42 error (invalid witness file) 6.4 3.4 110 290 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 340   340   3600 520 .99 0   error (invalid witness file) .50 .32 12 39 error (invalid witness file) 6.1 3.3 99 290 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   900   10000 5900 .99 0   - - error (invalid witness file) .51 .33 8.7 40 error (invalid witness file) 6.6 3.5 130 300
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   900   12000 5900 .84 0   - - error (invalid witness file) .49 .33 7.1 39 error (invalid witness file) 6.8 3.6 95 310
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   890   8100 1200 .99 0   - - error (invalid witness file) .53 .34 7.0 40 error (invalid witness file) 5.4 2.9 80 290
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   900   9800 4200 .99 0   - - error (invalid witness file) .48 .32 9.0 39 error (invalid witness file) 6.2 3.3 94 290
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   900   11000 4200 .84 0   - - error (invalid witness file) .47 .31 4.3 40 error (invalid witness file) 7.4 3.9 65 300
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   900   12000 4200 .84 0   - - error (invalid witness file) .53 .36 9.7 41 error (invalid witness file) 5.5 3.0 90 290
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   900   12000 4200 .84 0   - - error (invalid witness file) .56 .38 8.9 41 error (invalid witness file) 5.9 3.1 100 300
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   900   14000 10000 .99 0   - - error (invalid witness file) .51 .34 7.0 40 error (invalid witness file) 5.9 3.1 86 300
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   900   12000 7000 .99 0   - - error (invalid witness file) .53 .33 10   40 error (invalid witness file) 6.6 3.5 110 320
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   900   12000 7000 .84 0   - - error (invalid witness file) .48 .31 9.1 40 error (invalid witness file) 7.1 3.7 130 340
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   9100 1600 .99 0   - - error (invalid witness file) .48 .31 12   40 error (invalid witness file) 6.6 3.5 130 310
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   11000 1600 .99 0   - - error (invalid witness file) .49 .33 7.0 40 error (invalid witness file) 5.4 2.9 97 300
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   3200 770 .99 0   - - error (invalid witness file) .55 .36 9.1 42 error (invalid witness file) 6.6 3.5 92 310
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   8400 1800 .99 0   - - error (invalid witness file) .52 .32 11   39 error (invalid witness file) 5.9 3.1 110 300
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   9000 2000 .84 0   - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 6.0 3.2 96 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   9400 1900 .99 0   - - error (invalid witness file) .49 .32 8.3 41 error (invalid witness file) 6.1 3.2 86 290
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   9800 2000 .99 0   - - error (invalid witness file) .46 .30 6.0 40 error (invalid witness file) 8.0 4.2 98 310
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   1800 860 .84 0   - - error (invalid witness file) .52 .34 10   41 error (invalid witness file) 6.8 3.5 120 320
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   11000 1200 .84 0   - - error (invalid witness file) .50 .33 7.1 39 error (invalid witness file) 5.2 2.8 84 290
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   9400 1300 .99 0   - - error (invalid witness file) .52 .35 4.4 40 error (invalid witness file) 5.3 2.8 90 290
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   11000 1400 .99 0   - - error (invalid witness file) .50 .32 7.7 39 error (invalid witness file) 5.7 3.0 110 290
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   9500 1500 .84 0   - - error (invalid witness file) .50 .34 5.8 40 error (invalid witness file) 5.8 3.1 98 290
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   900   6700 1300 .99 0   - - error (invalid witness file) .51 .33 9.2 40 error (invalid witness file) 5.4 2.9 87 290
../../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 3 21000 21000 230000 75000 24   0   26 1.6 1.0 36 130 26 18 9.7 300 880 26 12 7.6 190 920   26 140 75 2300 6900  
    correct results 3 3 640 640 7700 1600 2.7 0   0 1.6 1.0 36 130 0 18 9.7 300 880 0 0 0   0 0   0 0 0 0 0  
        correct true 0
        correct false 3 3 640 640 7700 1600 2.7 0   0 1.6 1.0 36 130 0 18 9.7 300 880 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) 3
Run set sv-comp17.MemSafety-Other