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 1 1.3 1.3 13 64 .20 0      7.8  4.1  150 320 34   19   420 1900
head_true-no-overflow_false-valid-deref.i 1 22   22   230 1500 .34 .020  8.6  4.5  120 320 7.6 4.0 140 310
sleep_true-no-overflow_false-valid-deref.i 0 5.2 5.1 64 700 .33 .033  .52 .35 10 43 6.4 3.4 98 310
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 1 1.9 1.9 25 200 .30 0      7.1  3.8  130 320 7.4 3.9 120 320
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   900   12000 1100 .20 0      .55 .37 6.3 43 6.2 3.3 120 290
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   900   9200 1700 .31 0      .49 .32 7.4 40 6.7 3.5 130 300
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i -16 26   26   280 3500 .39 .29   8.4  4.4  160   320 7.8 4.1 140 310
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i -16 85   85   1200 6800 .45 .41   8.5  4.5  150   340 8.2 4.3 150 310
dirname_true-no-overflow_true-valid-memsafety.i 0 900   900   10000 2300 .18 0      .51 .35 4.8 41 5.6 3.0 94 290
du_true-no-overflow_true-valid-memsafety.i -16 29   29   370 3400 .42 .029  7.7  4.1  150   280 7.9 4.1 130 310
echo_true-no-overflow_true-valid-memsafety.i 0 900   900   10000 1600 .31 0      .53 .33 12   40 6.7 3.5 120 300
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i -16 130   130   1500 6300 .40 .029  8.6  4.5  180   290 8.7 4.5 150 320
fold_true-no-overflow_true-valid-memsafety.i -16 67   67   710 2500 .37 .13   8.1  4.2  160   320 8.1 4.2 160 310
hostid_true-no-overflow_true-valid-memsafety.i 0 900   900   9700 2300 .25 0      .54 .35 15   40 6.6 3.5 140 300
logname_true-no-overflow_true-valid-memsafety.i -16 120   120   1500 420 .30 0      7.4  3.9  120   320 7.5 3.9 160 310
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   900   9400 380 .58 .029  .49 .33 9.2 40 6.8 3.6 120 300
mkdir_true-no-overflow_true-valid-memsafety.i -16 20   20   260 2400 .40 .029  8.5  4.5  180   330 8.2 4.3 160 310
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i -16 110   110   1200 340 .29 0      7.9  4.2  150   310 7.3 3.8 150 310
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 190   190   2300 15000 .57 .029  .54 .36 6.2 42 7.0 3.7 100 290
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 32   32   410 3000 .38 .033  .49 .34 3.9 39 7.1 3.7 150 320
readlink_true-no-overflow_true-valid-memsafety.i 0 900   900   9500 2000 .35 .090  .52 .35 8.3 39 6.6 3.5 140 290
realpath_true-no-overflow_true-valid-memsafety.i -16 440   440   3300 780 .31 .090  7.4  3.9  140   290 7.9 4.2 130 310
rm_true-no-overflow_true-valid-memsafety.i -16 470   470   5000 3000 .41 .029  8.2  4.3  160   330 7.6 4.0 130 300
seq_true-no-overflow_true-valid-memsafety.i 0 16   16   190 1900 .34 .033  .50 .31 10   39 6.9 3.6 120 320
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   900   9900 11000 .57 .0082 .54 .35 6.5 40 6.7 3.5 110 310
sync_true-no-overflow_true-valid-memsafety.i -16 160   160   1600 410 .26 0      7.5  4.0  140   320 7.5 4.0 150 310
tac_true-no-overflow_true-valid-memsafety.i -16 58   58   700 2000 .36 .029  7.6  4.1  150   320 7.6 4.0 140 310
tee_true-no-overflow_true-valid-memsafety.i 0 900   900   8700 2400 .36 0      .52 .35 5.6 40 6.3 3.4 110 290
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i -16 3.4 3.4 41 350 .41 0      8.2  4.3  140   320 7.4 4.0 140 300
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i -16 38   38   460 5000 .43 .029  8.5  4.4  170   310 7.4 3.9 140 300
uname_true-no-overflow_true-valid-memsafety.i 0 900   900   8500 3400 .36 .029  .51 .32 11   39 6.3 3.3 120 290
uniq_true-no-overflow_true-valid-memsafety.i -16 24   24   280 2500 .37 .029  8.3  4.3  170   320 7.9 4.1 160 310
usleep_true-no-overflow_true-valid-memsafety.i 0 900   900   11000 1900 .31 .029  .49 .32 11   39 6.7 3.5 130 300
uudecode_true-no-overflow_true-valid-memsafety.i -16 50   50   550 5200 .43 .029  8.5  4.5  120   330 8.0 4.2 140 310
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   900   8700 3800 .36 .045  .52 .34 6.9 42 6.5 3.4 140 300
who_true-no-overflow_true-valid-memsafety.i 0 900   900   7200 2100 .39 .029  .53 .35 7.6 40 6.6 3.5 120 300
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   900   10000 2300 .31 0      .53 .35 6.7 40 6.5 3.4 110 300
yes_true-no-overflow_true-valid-memsafety.i -16 110   110   1300 470 .30 0      7.8  4.1  170   320 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