Tool ULTIMATE Kojak f7c3ed31
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 06:29:29 CET [[ 2017-01-15 05:44:30 CET ]] [[ 2017-01-15 05:59:35 CET ]] [[ 2017-01-15 05:44:48 CET ]] [[ 2017-01-15 06:00:32 CET ]]
Run set sv-comp17.MemSafety-Other
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.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   730   15000 3200 2.3 0   error (invalid witness file) .49 .31 12 39 error (invalid witness file) 6.1 3.3 130 300 - -
ntdrivers/floppy_false-valid-deref.i.cil.c unknown 0 wit inspect 7.0 1.8 56 340 2.5 0   error (invalid witness file) .58 .36 10 39 error (invalid witness file) 6.8 3.6 130 310 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c unknown 0 wit inspect 5.3 1.6 41 300 2.5 0   error (invalid witness file) .50 .32 11 40 error (invalid witness file) 5.8 3.2 120 300 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 16   5.2 130 650 4.4 0   - - true 37   22   620 2400 true 12   6.2 230 440
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 17   5.2 140 620 4.4 0   - - true 39   22   270 2600 true 12   6.3 210 440
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 15   4.6 120 750 3.5 0   - - out of memory 180   110   1500 7000 true 9.9 5.3 190 350
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.8 2.9 77 480 3.1 0   - - true 42   25   330 2600 true 10   5.4 160 340
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.7 2.9 71 460 3.1 0   - - true 40   25   340 2700 true 9.1 4.8 160 330
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 12   3.4 100 570 3.4 0   - - true 81   50   1200 3400 true 13   6.8 140 380
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   3.5 89 490 3.4 0   - - true 71   44   1300 3600 true 10   5.6 210 370
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 8.2 2.5 70 460 2.8 0   - - true 9.5 5.0 130 400 true 8.8 4.7 170 320
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.8 3.0 70 470 3.0 0   - - true 20   10   180 1100 true 13   6.7 140 320
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 10   3.0 78 470 3.0 0   - - true 19   9.8 150 1100 true 9.2 4.9 170 330
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.1 1.9 51 330 2.6 0   - - timeout 910   800   22000 6900 true 7.7 4.1 160 310
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.9 1.9 51 320 2.6 0   - - out of memory 780   670   16000 7000 true 7.8 4.1 140 320
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.2 1.9 50 320 2.6 0   - - out of memory 720   610   13000 7000 true 7.8 4.1 170 320
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.1 1.9 49 320 2.6 0   - - out of memory 600   510   7500 7000 true 7.5 4.0 150 320
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.5 1.9 49 320 2.6 0   - - out of memory 840   740   22000 7000 true 7.1 3.8 140 310
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.3 1.9 55 320 2.6 0   - - timeout 960   860   25000 7000 true 7.8 4.2 130 330
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.6 1.9 54 330 2.6 0   - - timeout 920   830   8600 6700 true 7.9 4.2 140 320
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.4 1.9 48 320 2.6 0   - - timeout 910   840   15000 6100 true 8.0 4.3 140 320
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.2 1.7 47 340 2.6 0   - - timeout 910   810   19000 7000 true 7.2 3.8 140 310
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.5 1.8 46 320 2.6 0   - - timeout 910   810   13000 6800 true 7.7 4.1 160 330
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.3 1.9 49 340 2.6 0   - - timeout 910   830   12000 6600 true 7.2 3.9 140 310
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.9 1.9 45 320 2.6 0   - - timeout 910   830   12000 6500 true 7.5 4.0 160 320
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.9 1.9 46 330 2.6 0   - - timeout 910   810   15000 6700 true 7.0 3.8 130 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 46 1100 790 17000 13000 75 0   26 1.6 .99 34 120   26 19 10 380 910   26 12000 10000 210000 120000 26 200 110 3700 7700
    correct results 23 46 200 61 1600 9700 68 0   0 0   0    0 0   0 0 0 0 0   9 12000 10000 210000 120000 23 200 110 3700 7700
        correct true 23 46 200 61 1600 9700 68 0   0 0   0    0 0   0 0 0 0 0   9 12000 10000 210000 120000 23 200 110 3700 7700
        correct false 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) 46
Run set sv-comp17.MemSafety-Other