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.Systems_BusyBox_MemSafety
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/busybox-1.22.0/ 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)
basename_false-unreach-call_true-no-overflow_false-valid-deref.i false(valid-deref) 1 wit inspect 1.3 1.3 13 64 .20 0      error 7.8  4.1  150 320 true 34   19   420 1900 - -
head_true-no-overflow_false-valid-deref.i false(valid-deref) 1 wit inspect 22   22   230 1500 .34 .020  error 8.6  4.5  120 320 unknown 7.6 4.0 140 310 - -
sleep_true-no-overflow_false-valid-deref.i unknown 0 wit inspect 5.2 5.1 64 700 .33 .033  error (invalid witness file) .52 .35 10 43 error (invalid witness file) 6.4 3.4 98 310 - -
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.9 1.9 25 200 .30 0      error 7.1  3.8  130 320 unknown 7.4 3.9 120 320 - -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   12000 1100 .20 0      - - error (invalid witness file) .55 .37 6.3 43 error (invalid witness file) 6.2 3.3 120 290
chroot-incomplete_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   9200 1700 .31 0      - - error (invalid witness file) .49 .32 7.4 40 error (invalid witness file) 6.7 3.5 130 300
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 26   26   280 3500 .39 .29   - - error 8.4  4.4  160   320 unknown 7.8 4.1 140 310
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 85   85   1200 6800 .45 .41   - - error 8.5  4.5  150   340 unknown 8.2 4.3 150 310
dirname_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   10000 2300 .18 0      - - error (invalid witness file) .51 .35 4.8 41 error (invalid witness file) 5.6 3.0 94 290
du_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 29   29   370 3400 .42 .029  - - error 7.7  4.1  150   280 unknown 7.9 4.1 130 310
echo_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   10000 1600 .31 0      - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 6.7 3.5 120 300
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 130   130   1500 6300 .40 .029  - - error 8.6  4.5  180   290 unknown 8.7 4.5 150 320
fold_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 67   67   710 2500 .37 .13   - - error 8.1  4.2  160   320 unknown 8.1 4.2 160 310
hostid_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   9700 2300 .25 0      - - error (invalid witness file) .54 .35 15   40 error (invalid witness file) 6.6 3.5 140 300
logname_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 120   120   1500 420 .30 0      - - error 7.4  3.9  120   320 unknown 7.5 3.9 160 310
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   9400 380 .58 .029  - - error (invalid witness file) .49 .33 9.2 40 error (invalid witness file) 6.8 3.6 120 300
mkdir_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 20   20   260 2400 .40 .029  - - error 8.5  4.5  180   330 unknown 8.2 4.3 160 310
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 110   110   1200 340 .29 0      - - error 7.9  4.2  150   310 unknown 7.3 3.8 150 310
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 wit inspect 190   190   2300 15000 .57 .029  - - error (invalid witness file) .54 .36 6.2 42 error (invalid witness file) 7.0 3.7 100 290
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 32   32   410 3000 .38 .033  - - error (invalid witness file) .49 .34 3.9 39 error (invalid witness file) 7.1 3.7 150 320
readlink_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   9500 2000 .35 .090  - - error (invalid witness file) .52 .35 8.3 39 error (invalid witness file) 6.6 3.5 140 290
realpath_true-no-overflow_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 440   440   3300 780 .31 .090  - - error 7.4  3.9  140   290 unknown 7.9 4.2 130 310
rm_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 470   470   5000 3000 .41 .029  - - error 8.2  4.3  160   330 unknown 7.6 4.0 130 300
seq_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 16   16   190 1900 .34 .033  - - error (invalid witness file) .50 .31 10   39 error (invalid witness file) 6.9 3.6 120 320
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   9900 11000 .57 .0082 - - error (invalid witness file) .54 .35 6.5 40 error (invalid witness file) 6.7 3.5 110 310
sync_true-no-overflow_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 160   160   1600 410 .26 0      - - error 7.5  4.0  140   320 unknown 7.5 4.0 150 310
tac_true-no-overflow_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 58   58   700 2000 .36 .029  - - error 7.6  4.1  150   320 unknown 7.6 4.0 140 310
tee_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   8700 2400 .36 0      - - error (invalid witness file) .52 .35 5.6 40 error (invalid witness file) 6.3 3.4 110 290
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 3.4 3.4 41 350 .41 0      - - error 8.2  4.3  140   320 unknown 7.4 4.0 140 300
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 38   38   460 5000 .43 .029  - - error 8.5  4.4  170   310 unknown 7.4 3.9 140 300
uname_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   8500 3400 .36 .029  - - error (invalid witness file) .51 .32 11   39 error (invalid witness file) 6.3 3.3 120 290
uniq_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 24   24   280 2500 .37 .029  - - error 8.3  4.3  170   320 unknown 7.9 4.1 160 310
usleep_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   11000 1900 .31 .029  - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.7 3.5 130 300
uudecode_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 50   50   550 5200 .43 .029  - - error 8.5  4.5  120   330 unknown 8.0 4.2 140 310
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   8700 3800 .36 .045  - - error (invalid witness file) .52 .34 6.9 42 error (invalid witness file) 6.5 3.4 140 300
who_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   7200 2100 .39 .029  - - error (invalid witness file) .53 .35 7.6 40 error (invalid witness file) 6.6 3.5 120 300
whoami-incomplete_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900   900   10000 2300 .31 0      - - error (invalid witness file) .53 .35 6.7 40 error (invalid witness file) 6.5 3.4 110 300
yes_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 110   110   1300 470 .30 0      - - error 7.8  4.1  170   320 unknown 6.8 3.6 100 300
../../sv-benchmarks/c/busybox-1.22.0/ 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 38 -269 15000 15000 160000 110000 14    1.5   38 24 13 410 1000   38 55 30 780 2800   38 150 78 2700 6000   38 240 130 4500 10000  
    correct results 3 3 25 25 270 1800 .83 .020 0 23 12 400 960   1 49 27 680 2500   0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 3 3 25 25 270 1800 .83 .020 0 23 12 400 960   0 49 27 680 2500   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 17 -272 1900 1900 20000 45000 6.3  1.1   0 0 0 0 0   0 0 0 0 0   0 140 72 2600 5400   0 130 69 2400 5200  
        incorrect true 0
        incorrect false 17 -272 1900 1900 20000 45000 6.3  1.1   0 0 0 0 0   0 0 0 0 0   0 140 72 2600 5400   0 130 69 2400 5200  
score (38 tasks, max score: 72) -269
Run set sv-comp17.Systems_BusyBox_MemSafety