Tool symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a
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 11:37:51 CET [[ 2017-01-15 04:18:56 CET ]] [[ 2017-01-15 04:38:06 CET ]] [[ 2017-01-15 04:27:27 CET ]] [[ 2017-01-15 04:45:45 CET ]]
Run set sv-comp17.MemSafety-Other
Options --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1137.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 false(valid-deref) 1 wit inspect 9.7  9.7  110   29 .012 0      timeout 97    54    720 3900 timeout 98   58   1200 5800 - -
ntdrivers/floppy_false-valid-deref.i.cil.c unknown 0 wit inspect 21    21    200   2100 .86  0      error (invalid witness file) .52 .34 13 40 error (invalid witness file) 8.1 4.2 140 330 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 1.0  1.0  13   19 .39  0      timeout 96    75    1700 3100 unknown 7.6 4.0 130 310 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.3  7.3  84   580 .21  0      - - true 38    22    440   2300 true 11   6.1 170 420
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.4  7.4  100   580 .21  0      - - true 36    20    480   2200 true 11   5.6 170 400
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9200   1800 .086 0      - - error (invalid witness file) .55 .35 15   41 error (invalid witness file) 5.8 3.1 110 290
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 2.0  2.0  26   150 .098 0      - - true 42    25    380   2700 true 9.6 5.1 160 330
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.9  1.9  25   150 .098 0      - - true 41    25    440   2600 true 9.2 5.0 150 320
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 4.5  4.5  52   320 .15  0      - - true 75    45    1000   3600 true 10   5.5 190 370
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 4.5  4.5  50   320 .15  .0082 - - true 70    42    720   3700 true 10   5.4 190 370
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .48 .48 5.7 32 .061 0      - - true 9.4  5.0  160   400 true 7.7 4.2 150 320
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.1  1.1  13   95 .098 0      - - true 20    10    270   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 1.0  1.0  14   94 .098 0      - - true 20    10    260   1100 true 9.4 5.0 130 330
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    5400   1700 .012 0      - - error (invalid witness file) .51 .33 7.1 39 error (invalid witness file) 5.8 3.0 110 300
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    5600   2300 .016 0      - - error (invalid witness file) .50 .33 4.3 40 error (invalid witness file) 5.7 3.0 85 300
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    5600   3200 .025 0      - - error (invalid witness file) .50 .32 13   39 error (invalid witness file) 6.0 3.2 120 300
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    6200   4100 .025 0      - - error (invalid witness file) .48 .30 4.0 39 error (invalid witness file) 5.6 3.0 110 290
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    5800   3100 .025 0      - - error (invalid witness file) .53 .34 7.5 42 error (invalid witness file) 5.9 3.1 110 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    5600   5200 .025 0      - - error (invalid witness file) .54 .34 13   41 error (invalid witness file) 6.3 3.3 120 300
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    7700   4300 .025 0      - - error (invalid witness file) .55 .35 13   42 error (invalid witness file) 6.6 3.5 100 300
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    4200   4700 .025 0      - - error (invalid witness file) .52 .34 7.6 40 error (invalid witness file) 6.3 3.3 130 320
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    11000   380 .012 0      - - error (invalid witness file) .51 .33 8.3 40 error (invalid witness file) 5.8 3.1 92 300
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    6900   510 .012 0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.1 3.2 110 300
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    6300   690 .012 0      - - error (invalid witness file) .52 .34 9.7 40 error (invalid witness file) 6.2 3.3 100 300
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    6900   950 .012 0      - - error (invalid witness file) .48 .33 3.7 40 error (invalid witness file) 6.0 3.2 110 300
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout (timeout) 0 wit inspect 900    900    6400   1300 .012 0      - - error (invalid witness file) .55 .34 13   41 error (invalid witness file) 6.2 3.3 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 20 13000 13000 94000 39000 2.8  .0082 26 190 130 2500 7100   26 110 66 1400 6400   26 360 210 4300 20000   26 170 91 3000 7400  
    correct results 11 20 41 41 500 2400 1.6  .0082 0 190 130 2500 7000   0 110 62 1300 6100   9 350 200 4200 20000   9 87 47 1500 3200  
        correct true 9 18 30 30 370 2300 1.2  .0082 0 0 0 0 0   0 0 0 0 0   9 350 200 4200 20000   9 87 47 1500 3200  
        correct false 2 2 11 11 130 47 .41 0      0 190 130 2500 7000   0 110 62 1300 6100   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