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 13:43:12 CET [[ 2017-01-15 05:08:16 CET ]] [[ 2017-01-15 05:40:54 CET ]] [[ 2017-01-15 05:24:54 CET ]] [[ 2017-01-15 05:42:22 CET ]]
Run set sv-comp17.Systems_BusyBox_Overflows
Options --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1343.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1343.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_1343.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1343.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 wall energy mem validator uautomizer violation t<90s status cpu wall energy mem 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 timeout (timeout) 0 wit inspect 900    900    12000   260 .20 0      - - error (invalid witness file) .56 .36 12   42 error (invalid witness file) 7.0 3.7 110 300
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   260 .20 0      - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.7 3.6 100 300
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    900    11000   370 .29 0      - - error (invalid witness file) .70 .43 7.4 42 error (invalid witness file) 6.7 3.6 120 310
chroot-incomplete_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    12000   490 .31 0      - - error (invalid witness file) .56 .36 13   40 error (invalid witness file) 6.3 3.4 74 290
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    10000   280 .38 0      - - error (invalid witness file) .68 .43 10   44 error (invalid witness file) 7.1 3.7 140 300
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i false(no-overflow) -16 wit inspect 1.3  1.3  14   81 .44 .029  - - timeout 900    880    18000   3700 unknown 9.2 4.8 120 320
dirname_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   1400 .17 0      - - error (invalid witness file) .53 .35 5.2 42 error (invalid witness file) 6.6 3.5 120 310
du_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 8.1  8.1  85   67 .42 .029  - - error (invalid witness file) .61 .40 8.5 40 error (invalid witness file) 6.2 3.3 120 280
echo_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    10000   470 .31 0      - - error (invalid witness file) .55 .35 11   42 error (invalid witness file) 6.7 3.5 140 300
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    10000   420 .39 .029  - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.9 3.7 140 320
fold_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    13000   360 .37 .13   - - error (invalid witness file) .48 .33 3.4 39 error (invalid witness file) 7.2 3.8 160 300
head_true-no-overflow_false-valid-deref.i timeout (timeout) 0 wit inspect 900    900    12000   330 .33 .029  - - error (invalid witness file) .52 .34 12   41 error (invalid witness file) 7.7 4.0 100 310
hostid_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    13000   1100 .25 0      - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.3 3.4 130 290
logname_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   270 .29 0      - - error (invalid witness file) .48 .32 8.9 39 error (invalid witness file) 6.8 3.6 130 310
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 220    220    2600   180 .58 .029  - - error (invalid witness file) .46 .31 7.8 39 error (invalid witness file) 6.7 3.5 120 300
mkdir_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    8200   910 .39 .49   - - error (invalid witness file) .55 .34 7.1 44 error (invalid witness file) 8.2 4.3 86 290
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   450 .28 0      - - error (invalid witness file) .49 .32 13   40 error (invalid witness file) 6.4 3.4 120 300
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 1.5  1.4  16   120 .57 .26   - - timeout 910    780    13000   6700 unknown 8.4 4.4 140 320
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect .57 .54 7.1 40 .38 .033  - - error (invalid witness file) .52 .35 11   40 error (invalid witness file) 6.5 3.4 130 310
readlink_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    8200   1200 .34 .066  - - error (invalid witness file) .47 .32 7.0 40 error (invalid witness file) 7.7 4.1 84 300
realpath_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   610 .31 0      - - error (invalid witness file) .54 .35 8.4 41 error (invalid witness file) 6.3 3.3 110 300
rm_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9400   2100 .41 0      - - error (invalid witness file) .54 .36 8.2 39 error (invalid witness file) 6.8 3.6 110 310
seq_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect .56 .54 6.9 39 .34 .0041 - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.4 3.4 130 290
sleep_true-no-overflow_false-valid-deref.i unknown 0 wit inspect .42 .39 5.1 20 .33 .033  - - error (invalid witness file) .55 .35 11   41 error (invalid witness file) 6.8 3.6 130 300
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 76    76    730   110 .57 .020  - - error (invalid witness file) .48 .31 6.7 39 error (invalid witness file) 6.7 3.5 130 310
sync_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    12000   270 .26 0      - - error (invalid witness file) .51 .34 8.8 40 error (invalid witness file) 6.2 3.3 130 290
tac_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    12000   1200 .36 .045  - - error (invalid witness file) .53 .34 7.0 40 error (invalid witness file) 6.8 3.6 130 300
tee_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   730 .36 .029  - - error (invalid witness file) .59 .37 10   40 error (invalid witness file) 6.4 3.4 100 290
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    12000   720 .41 0      - - error (invalid witness file) .57 .37 12   41 error (invalid witness file) 6.8 3.6 140 310
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i false(no-overflow) -16 wit inspect 210    210    2300   420 .43 .029  - - timeout 900    880    15000   3700 unknown 7.9 4.1 130 310
uname_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    7000   5100 .36 .029  - - error (invalid witness file) .50 .32 11   41 error (invalid witness file) 6.4 3.4 120 300
uniq_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9800   310 .37 .15   - - error (invalid witness file) .48 .30 8.5 40 error (invalid witness file) 6.8 3.6 110 300
usleep_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    10000   220 .31 .32   - - error (invalid witness file) .53 .34 6.9 40 error (invalid witness file) 7.1 3.8 120 310
uudecode_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   620 .43 .45   - - error (invalid witness file) .51 .34 5.8 40 error (invalid witness file) 7.1 3.7 120 310
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   2600 .36 .020  - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.6 3.5 97 300
who_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    7300   5100 .38 .20   - - error (invalid witness file) .52 .34 5.6 40 error (invalid witness file) 6.7 3.5 130 300
whoami-incomplete_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   1300 .31 0      - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.9 3.6 130 300
yes_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    10000   300 .29 0      - - error (invalid witness file) .50 .32 8.0 39 error (invalid witness file) 7.2 3.8 98 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 wall energy mem validator uautomizer violation t<90s status cpu wall energy mem 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 -31 27000   27000   320000 31000 13    2.4   38 38 38 2700 2600 47000 15000 38 260   140   4500 12000
    correct results 0
        correct true 0
        correct false 0
    correct-unconfimed results 1 1 1.5 1.4 16 120 .57 .26  0 0 0 910 780 13000 6700 0 8.4 4.4 140 320
        correct-unconfirmed true 1 1 1.5 1.4 16 120 .57 .26  0 0 0 910 780 13000 6700 0 8.4 4.4 140 320
        correct-unconfirmed false 0
    incorrect results 2 -32 210   210   2300 500 .87 .057 0 0 0 1800 1800 34000 7400 0 17   8.9 250 630
        incorrect true 0
        incorrect false 2 -32 210   210   2300 500 .87 .057 0 0 0 1800 1800 34000 7400 0 17   8.9 250 630
score (38 tasks, max score: 76) -31
Run set sv-comp17.Systems_BusyBox_Overflows