Tool SMACK+Corral 1.7.2
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-14 05:56:27 CET [[ 2017-01-15 04:08:20 CET ]] [[ 2017-01-15 04:18:47 CET ]] [[ 2017-01-15 04:12:29 CET ]] [[ 2017-01-15 04:25:58 CET ]]
Run set sv-comp17.MemSafety-Other
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.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 790   930   6600 1200 13   0   error (invalid witness file) .49 .32 8.1 42 error (invalid witness file) 6.0 3.2 110 300 - -
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 48   48   570 250 12   0   error (invalid witness file) .58 .40 4.9 44 error (invalid witness file) 7.1 3.7 130 300 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 4.5 4.3 49 120 3.2 0   error (invalid witness file) .57 .36 13   44 error (invalid witness file) 6.4 3.4 120 300 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 330   330   4300 260 5.5 0   - - error (invalid witness file) .50 .31 12   40 error (invalid witness file) 6.4 3.4 120 300
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 320   320   4200 260 5.5 0   - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 6.4 3.4 120 300
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 160   160   2300 180 4.0 0   - - error (invalid witness file) .48 .31 4.7 39 error (invalid witness file) 6.1 3.2 110 300
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 130   120   1600 180 4.1 0   - - error (invalid witness file) .56 .36 9.1 40 error (invalid witness file) 7.0 3.7 81 290
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 130   130   2000 180 4.1 0   - - error (invalid witness file) .51 .32 8.4 40 error (invalid witness file) 6.0 3.2 110 300
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 200   200   2700 220 4.9 0   - - error (invalid witness file) .52 .33 14   40 error (invalid witness file) 6.3 3.4 120 300
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 200   190   2300 210 4.9 0   - - error (invalid witness file) .51 .34 3.7 40 error (invalid witness file) 6.2 3.3 120 300
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 26   26   320 120 3.0 0   - - error (invalid witness file) .53 .34 13   40 error (invalid witness file) 6.1 3.2 110 300
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 59   57   770 150 3.8 0   - - error (invalid witness file) .66 .44 6.7 40 error (invalid witness file) 6.1 3.3 130 300
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 58   57   850 150 3.8 0   - - error (invalid witness file) .59 .37 9.4 40 error (invalid witness file) 5.6 3.0 98 290
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.8 3.9 42 83 2.0 0   - - error (invalid witness file) .50 .33 10   39 error (invalid witness file) 7.1 3.7 110 310
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.9 3.9 43 86 2.1 0   - - error (invalid witness file) .52 .34 7.8 40 error (invalid witness file) 5.6 3.0 100 300
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.8 3.9 57 87 2.1 0   - - error (invalid witness file) .50 .32 5.5 39 error (invalid witness file) 5.9 3.2 110 300
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.9 3.9 45 83 2.1 0   - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 5.8 3.1 86 300
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.9 3.9 59 88 2.1 0   - - error (invalid witness file) .49 .32 6.8 39 error (invalid witness file) 5.9 3.2 130 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.9 3.9 60 84 2.1 0   - - error (invalid witness file) .50 .33 4.8 44 error (invalid witness file) 5.9 3.1 120 300
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.9 3.9 52 86 2.2 0   - - error (invalid witness file) .50 .33 9.4 39 error (invalid witness file) 6.0 3.2 110 300
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.0 3.9 60 86 2.2 0   - - error (invalid witness file) .51 .34 4.3 39 error (invalid witness file) 6.4 3.3 120 300
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.6 3.7 46 77 1.9 0   - - error (invalid witness file) .48 .30 10   40 error (invalid witness file) 6.1 3.2 110 300
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.6 3.7 46 75 1.9 0   - - error (invalid witness file) .49 .32 8.7 39 error (invalid witness file) 5.4 3.0 110 290
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.7 3.7 54 81 2.0 0   - - error (invalid witness file) .50 .34 4.3 40 error (invalid witness file) 6.0 3.2 120 300
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.7 3.7 57 90 2.0 0   - - error (invalid witness file) .55 .35 12   39 error (invalid witness file) 5.3 2.9 110 290
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.7 3.7 52 83 2.0 0   - - error (invalid witness file) .46 .31 4.1 39 error (invalid witness file) 6.1 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 48 2500 2600 29000 4500 99 0   26 1.6 1.1  26 130   26 19 10   370 900   26 12 7.7 190 910   26 140 74 2600 6900  
    correct results 25 48 1700 1700 23000 3400 86 0   0 1.2 .76 18 88   0 13 7.1 250 600   0 12 7.7 190 910   0 140 74 2600 6900  
        correct true 23 46 1700 1600 22000 3000 70 0   0 0   0    0 0   0 0 0   0 0   0 12 7.7 190 910   0 140 74 2600 6900  
        correct false 2 2 53 52 620 370 15 0   0 1.2 .76 18 88   0 13 7.1 250 600   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