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:51:33 CET [[ 2017-01-15 01:19:13 CET ]] [[ 2017-01-15 01:22:10 CET ]] [[ 2017-01-15 01:20:47 CET ]] [[ 2017-01-15 01:23:25 CET ]]
Run set sv-comp17.MemSafety-Other
Options -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0551.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 1 320    310    4000   2300 .99 0   .53 .36 12 40 5.4 2.9 110 290
ntdrivers/floppy_false-valid-deref.i.cil.c 1 19    19    43   410 .84 0   .54 .34 12 39 6.8 3.6 130 300
ntdrivers/kbfiltr_false-valid-deref.i.cil.c 1 320    320    3900   530 .99 0   .50 .32 11 39 6.9 3.6 130 310
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .78 .78 9.2 45 .99 0   .52 .33 12 39 6.2 3.3 130 300
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .74 .74 8.6 45 .84 0   .53 .33 13 41 6.1 3.2 120 300
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 410    400    5300   15000 .84 0   .51 .32 11 40 6.3 3.3 150 300
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .29 .29 3.7 28 .99 0   .51 .33 10 41 6.5 3.4 140 300
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .26 .26 3.1 28 .84 0   .50 .34 10 40 6.2 3.3 130 300
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .43 .43 4.9 30 .99 0   .50 .33 10 39 7.1 3.8 140 320
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .43 .42 4.6 30 .99 0   .53 .34 13 40 6.3 3.3 130 300
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .16 .16 1.5 25 .84 0   .51 .33 13 40 6.0 3.2 120 300
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .19 .19 2.1 27 .84 0   .51 .33 12 42 5.8 3.1 110 300
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .21 .21 2.2 27 .99 0   .57 .35 12 43 6.2 3.3 120 300
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 0 460    460    5400   15000 .99 0   .56 .36 12 45 5.9 3.1 130 290
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 0 470    470    5700   15000 .99 0   .48 .31 10 39 6.0 3.2 120 300
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 0 470    470    6500   15000 .99 0   .50 .34 11 39 6.0 3.2 120 310
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 0 490    490    6000   15000 .99 0   .54 .34 12 43 5.9 3.1 110 290
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 0 480    480    5800   15000 .84 0   .52 .34 12 40 6.0 3.1 120 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 0 500    490    5500   15000 .99 0   .48 .32 11 40 6.1 3.2 130 300
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 0 490    490    6900   15000 .99 0   .51 .32 12 39 5.8 3.1 120 300
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 0 500    490    5800   15000 .84 0   .52 .34 12 41 6.1 3.2 110 300
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 0 420    420    5000   15000 .99 0   .53 .32 12 40 6.7 3.5 140 320
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 0 420    420    4800   15000 .99 0   .53 .34 12 42 6.5 3.4 130 310
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 0 430    430    6100   15000 .99 0   .48 .31 10 40 6.0 3.2 110 300
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 0 440    440    5700   15000 .84 0   .57 .36 14 43 6.2 3.3 120 300
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 0 450    450    6500   15000 .99 0   .52 .34 12 39 6.1 3.3 120 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 21 7100   7100   89000 210000 24   0   26 1.6 1.0 35 120   26 19 10 360 900   26 12   7.7 270 940   26 140 75 2900 6900  
    correct results 12 21 660   660   7900 3500 11   0   0 1.6 1.0 35 120   0 19 10 360 900   0 4.7 3.0 110 370   0 56 30 1100 2700  
        correct true 9 18 3.5 3.5 40 290 8.3 0   0 0   0   0 0   0 0 0 0 0   0 4.7 3.0 110 370   0 56 30 1100 2700  
        correct false 3 3 660   650   7900 3300 2.8 0   0 1.6 1.0 35 120   0 19 10 360 900   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) 21
Run set sv-comp17.MemSafety-Other