Tool 2LS 0.5.0
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-11 09:48:02 CET [[ 2017-01-14 21:34:09 CET ]] [[ 2017-01-14 21:49:16 CET ]] [[ 2017-01-14 21:34:25 CET ]] [[ 2017-01-14 21:52:20 CET ]]
Run set sv-comp17.MemSafety-Other
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.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 timeout 0 wit inspect 900    900    11000    10000 0      .10 error (invalid witness file) .54 .34 11 41 error (invalid witness file) 6.5 3.4 96 310 - -
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 48    48    640    1900 .012  .27 error 11    5.6  220 370 unknown 10   5.3 91 320 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 2.0  1.9  21    88 .012  .20 error 6.6  3.5  100 270 unknown 10   5.3 110 320 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.3  1.3  12    410 .0041 7.9  - - true 44 26   420 2300 true 16   8.5 160 470
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.3  1.3  14    410 .0041 12    - - true 46 26   580 2400 true 14   7.3 180 460
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .46 .46 4.4  100 .0041 0    - - out of memory 190 120   2300 7000 true 11   5.8 180 360
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .37 .37 2.9  69 .0041 2.1  - - true 42 25   610 2700 true 12   6.4 150 350
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .35 .34 3.3  67 .0041 0    - - true 46 27   640 2700 true 12   6.3 140 350
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .51 .50 4.9  130 .0041 0    - - true 66 40   540 3300 true 14   7.4 120 380
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .51 .50 6.0  130 .0041 0    - - true 65 40   740 3600 true 11   5.9 210 400
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .20 .19 1.5  26 .0041 0    - - true 10 5.2 150 410 true 10   5.5 130 320
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .29 .29 2.7  44 .0041 0    - - true 22 11   350 1100 true 8.9 4.8 170 320
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .29 .28 2.6  44 .0041 0    - - true 22 11   310 940 true 11   6.0 160 340
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 .15 1.2  32 .0041 8.0  - - timeout 910 810   19000 6700 true 9.3 4.9 110 310
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .16 .20 1.0  36 .0041 12    - - out of memory 840 730   18000 7000 true 9.3 5.0 86 310
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 .13 .84 24 .0041 0    - - out of memory 800 680   21000 7000 true 7.6 4.1 120 320
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12 .12 .95 25 .0041 0    - - out of memory 840 730   15000 7000 true 9.1 4.9 87 320
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 .13 1.2  25 .0041 0    - - timeout 910 800   19000 7000 true 8.3 4.4 120 310
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .17 .20 1.1  33 .0041 8.0  - - timeout 920 820   16000 6200 true 7.5 4.0 140 310
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 .13 1.1  25 .0041 0    - - timeout 960 880   19000 5800 true 8.5 4.5 130 320
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 .13 1.1  25 .0041 0    - - timeout 920 860   22000 5600 true 7.4 4.0 140 310
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 .16 1.0  31 .0041 7.9  - - timeout 910 810   25000 7000 true 8.8 4.7 110 320
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12 .11 .90 23 .0041 0    - - timeout 950 850   19000 6600 true 9.3 5.0 93 310
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12 .12 .93 25 .0041 0    - - timeout 910 830   22000 6300 true 6.6 3.6 140 310
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .11 .11 .99 23 .0041 .16 - - timeout 910 840   19000 6300 true 9.6 5.1 94 320
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12 .12 .92 24 .0041 .16 - - timeout 910 830   18000 6400 true 8.1 4.4 120 320
../../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 48 960   960   12000 14000 .12  59    26 18 9.5 330 690   26 27 14 300 940   26 12000 11000 260000 110000   26 230 120 3100 7800  
    correct results 25 48 57   57   730 3800 .12  59    0 17 9.1 320 650   0 20 11 200 640   9 12000 11000 260000 110000   23 230 120 3100 7800  
        correct true 23 46 7.3 7.3 68 1800 .094 59    0 0 0   0 0   0 0 0 0 0   9 12000 11000 260000 110000   23 230 120 3100 7800  
        correct false 2 2 50   50   660 2000 .025 .47 0 17 9.1 320 650   0 20 11 200 640   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) 48
Run set sv-comp17.MemSafety-Other