Tool CPAchecker 1.6.1-svn 24048
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 04:38:11 CET [[ 2017-01-14 23:48:17 CET ]] [[ 2017-01-14 23:57:43 CET ]] [[ 2017-01-14 23:52:59 CET ]] [[ 2017-01-15 00:03:21 CET ]]
Run set sv-comp17.MemSafety-Other
Options -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.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   880   14000 3500 0   0   error (invalid witness file) .55 .37 11 40 error (invalid witness file) 5.8 3.1 97 300 - -
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 7.2 2.0 56 330 0   0   true 9.9  5.1  110 340 unknown 7.6 4.0 160 320 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 4.4 1.4 33 270 0   0   false(valid-deref) 7.5  4.0  95 280 unknown 7.3 3.8 93 320 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 76   49   780 3900 0   0   - - true 46    26    350   2400 true 13   6.7 200 450
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 68   45   770 4000 0   0   - - true 36    21    420   2500 true 12   6.6 180 460
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   840   11000 4700 0   0   - - error (invalid witness file) .51 .32 9.7 40 error (invalid witness file) 6.6 3.4 120 310
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 65   41   620 4000 0   0   - - true 44    27    590   2600 true 10   5.4 160 330
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 62   39   580 4100 0   0   - - true 49    30    730   2800 true 10   5.4 140 340
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 120   77   1200 4400 0   0   - - true 72    44    1300   3500 true 9.7 5.3 180 360
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 130   81   1300 4300 0   0   - - true 66    41    580   3900 true 10   5.4 190 360
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 8.5 2.3 63 500 0   0   - - true 9.7  5.1  150   410 true 8.3 4.3 120 340
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 20   8.0 180 1800 0   0   - - true 23    12    250   1100 true 9.0 4.9 140 310
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 20   7.8 200 2000 0   0   - - true 24    12    180   1100 true 8.9 4.7 130 330
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   720   10000 7100 0   0   - - error (invalid witness file) .48 .31 7.7 39 error (invalid witness file) 6.1 3.2 81 300
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   740   11000 6700 0   0   - - error (invalid witness file) .61 .38 6.4 40 error (invalid witness file) 5.4 2.9 65 280
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   740   12000 7100 0   0   - - error (invalid witness file) .54 .35 9.9 39 error (invalid witness file) 6.5 3.4 130 310
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 920   740   10000 7000 0   0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 7.7 4.0 97 310
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   840   2000 2800 0   0   - - error (invalid witness file) .61 .39 5.2 39 error (invalid witness file) 6.4 3.4 110 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   760   11000 6600 0   0   - - error (invalid witness file) .49 .32 9.5 40 error (invalid witness file) 6.7 3.5 74 310
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   860   12000 3700 0   0   - - error (invalid witness file) .53 .34 9.0 39 error (invalid witness file) 6.5 3.5 110 300
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   750   12000 6500 0   0   - - error (invalid witness file) .47 .31 8.1 39 error (invalid witness file) 6.9 3.7 92 300
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   670   10000 8100 0   0   - - error (invalid witness file) .54 .34 10   43 error (invalid witness file) 6.2 3.3 99 300
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   600   10000 8700 0   0   - - error (invalid witness file) .53 .35 8.4 40 error (invalid witness file) 6.6 3.4 100 300
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   620   10000 8300 0   0   - - error (invalid witness file) .52 .34 7.9 41 error (invalid witness file) 5.8 3.1 100 300
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   690   9400 8000 0   0   - - error (invalid witness file) .67 .42 7.6 40 error (invalid witness file) 7.3 3.8 76 300
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   680   11000 7500 0   0   - - error (invalid witness file) .52 .35 9.7 40 error (invalid witness file) 5.8 3.1 93 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 20 14000 12000   160000 130000 0   0   26 18 9.5 220 650   26 21 11   340 930   26 380 220 4700 21000   26 180 97 2800 7500  
    correct results 11 20 580 350   5800 30000 0   0   2 17 9.1 200 610   0 15 7.8 250 640   9 370 220 4500 20000   9 91 49 1400 3300  
        correct true 9 18 570 350   5700 29000 0   0   1 0 0   0 0   0 0 0   0 0   9 370 220 4500 20000   9 91 49 1400 3300  
        correct false 2 2 12 3.5 89 600 0   0   1 17 9.1 200 610   0 15 7.8 250 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) 20
Run set sv-comp17.MemSafety-Other