Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-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-12-01 10:20:37 CET 2017-12-01 11:16:27 CET 2017-12-01 08:43:54 CET 2017-12-01 08:51:01 CET 2017-12-01 10:49:29 CET 2017-12-01 13:07:37 CET 2017-12-02 06:23:16 CET 2017-12-02 18:23:42 CET 2017-12-05 13:47:25 CET 2017-12-03 04:09:48 CET 2017-12-03 11:17:40 CET 2017-12-03 08:43:49 CET
Run set 2ls.sv-comp18.Systems_BusyBox_NoOverflows cbmc.sv-comp18.Systems_BusyBox_NoOverflows cpa-bam-bnb.sv-comp18.Systems_BusyBox_NoOverflows cpa-bam-slicing.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq.sv-comp18.Systems_BusyBox_NoOverflows depthk.sv-comp18.Systems_BusyBox_NoOverflows esbmc-incr.sv-comp18.Systems_BusyBox_NoOverflows esbmc-kind.sv-comp18.Systems_BusyBox_NoOverflows interpchecker.sv-comp18 symbiotic.sv-comp18.Systems_BusyBox_NoOverflows uautomizer.sv-comp18.Systems_BusyBox_NoOverflows ukojak.sv-comp18.Systems_BusyBox_NoOverflows utaipan.sv-comp18.Systems_BusyBox_NoOverflows
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/busybox-1.22.0/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
chgrp-incomplete_false-no-overflow.i error (134) .32 37 3.0 0 error (6) .76 44 7.3 0 error (1) .45 42 4.5 0 error (1) .47 40 4.2 0 timeout 900   1700 5700 0 unknown 900 2700 6500 0 unknown 3.5  150 39   0 unknown .14 31 1.7 0 error (1) .42 42 4.1 0 timeout (timeout) 900    330 14000   0 error 270   1600 2800 0 timeout 900   2500 12000 0 timeout 900   6400 12000 0
chroot-incomplete_false-no-overflow.i error (134) .58 37 6.7 0 error (6) 1.0  44 9.8 0 error (1) .46 40 4.6 0 error (1) .46 40 3.9 0 unknown 38   520 430 0 unknown 900 930 8200 0 unknown 3.4  150 50   0 unknown .15 31 2.0 0 error (1) .41 39 4.0 0 timeout (timeout) 900    210 11000   0 error 380   1700 3800 0 error (7) 310   3300 3900 0 timeout 900   6000 13000 0
cut_false-no-overflow.i error (134) 13    51 120   0 error (6) 7.2  93 93   0 error (1) .46 40 4.1 0 error (1) .47 40 4.5 0 timeout 900   6100 12000 0 unknown 48 500 660 0 unknown 3.5  160 52   0 unknown .18 38 2.5 0 error (1) .43 40 3.7 0 error .47 23 6.7 0 timeout 900   2200 7100 0 timeout 900   5200 11000 0 timeout 900   5900 12000 0
date_false-no-overflow.i error (6) .43 46 3.1 0 error (6) 3.5  150 39   0 error (1) .50 41 4.6 0 error (1) .43 40 4.1 0 timeout 900   3300 10000 0 unknown 51 500 660 0 unknown 3.5  170 57   0 unknown .21 40 3.0 0 error (1) .42 41 3.6 0 error .60 33 7.3 0 error (7) 4.3 230 34 0 error (7) 4.3 240 34 0 error (7) 4.5 240 35 0
du_false-no-overflow.i error (5) 6.8  44 58   0 error (6) 55    240 530   0 error (1) .45 40 4.4 0 error (1) .46 40 4.3 0 timeout 900   3400 9900 0 unknown 46 500 700 0 unknown 3.5  160 47   0 unknown .22 38 2.0 0 error (1) .42 40 4.0 0 error .47 24 6.4 0 timeout 900   12000 7400 0 timeout 900   4200 9800 0 timeout 900   5600 8600 0
echo_false-no-overflow.i error (134) .50 38 5.0 0 error (42) 870    4600 4300   0 error (1) .47 41 4.0 0 error (1) .47 40 4.1 0 timeout 900   1100 11000 0 unknown 890 700 9400 0 unknown 4.7  240 57   0 unknown .16 32 1.9 0 error (1) .44 41 3.9 0 timeout (timeout) 900    330 12000   0 timeout 900   3000 7600 0 timeout 900   5200 13000 0 timeout 900   6400 12000 0
expand_false-no-overflow.i error (134) 31    72 300   0 error (6) 30    250 320   0 error (1) .50 43 4.6 0 error (1) .44 40 4.2 0 timeout 900   5900 9200 0 unknown 60 940 730 0 unknown 4.0  190 59   0 unknown .23 39 2.2 0 error (1) .45 40 4.0 0 error .58 30 6.4 0 timeout 900   2700 6000 0 timeout 900   5400 13000 0 timeout 900   5700 12000 0
fold_false-no-overflow.i error (134) 5.6  42 48   0 error (6) 3.9  58 46   0 error (1) .46 41 4.5 0 error (1) .42 40 4.2 0 timeout 900   1100 9800 0 unknown 46 550 630 0 unknown 4.0  180 51   0 unknown .22 37 2.7 0 error (1) .45 40 3.8 0 error .43 19 5.3 0 timeout 900   1900 8000 0 timeout 900   5100 12000 0 timeout 900   4700 12000 0
head_false-no-overflow.i error (6) .39 40 3.2 0 error (6) 4.3  61 54   0 error (1) .47 40 4.2 0 error (1) .46 40 4.6 0 timeout 900   1300 6800 0 unknown 900 2400 10000 0 unknown 3.6  170 47   0 unknown .19 34 2.1 0 error (1) .41 40 3.9 0 error .35 16 5.3 0 timeout 900   5500 8700 0 timeout 900   4900 11000 0 timeout 900   6300 14000 0
logname_false-no-overflow.i error (134) .32 37 3.2 0 error (6) .67 44 6.7 0 error (1) .47 42 4.6 0 error (1) .46 40 4.2 0 timeout 900   1300 5500 0 unknown 900 1000 13000 0 unknown 3.5  150 45   0 unknown .14 31 1.6 0 error (1) .42 40 3.8 0 timeout (timeout) 900    130 13000   0 error 76   1100 800 0 error 47   1000 430 0 timeout 900   6500 11000 0
ls-incomplete_false-no-overflow.i error (5) 230    190 2100   0 error (1) 870    710 3400   0 error (1) .49 40 4.1 0 error (1) .46 40 3.9 0 timeout 900   3100 11000 0 unknown 58 59 710 0 unknown .20 50 2.2 0 unknown .23 50 2.7 0 error (1) .48 40 4.1 0 error .98 64 11   0 error (7) 4.5 230 32 0 error (7) 4.5 230 40 0 error (7) 4.6 230 34 0
mkdir_false-no-overflow.i error (134) 2.6  43 23   0 error (1) 870    2200 2500   0 error (1) .43 40 4.3 0 error (1) .43 40 3.7 0 timeout 900   6200 10000 0 unknown 47 500 560 0 unknown 3.5  160 42   0 unknown .19 38 2.0 0 error (1) .41 40 4.0 0 error .44 19 4.6 0 timeout 900   1900 6700 0 timeout 900   5000 11000 0 timeout 900   5800 13000 0
mkfifo-incomplete_false-no-overflow.i error (134) .30 36 2.8 0 error (6) .74 43 7.6 0 error (1) .49 45 4.6 0 error (1) .41 40 4.5 0 false(no-overflow) 110   780 1100 0 unknown 900 1200 9600 0 unknown 3.5  150 45   0 unknown .18 30 1.5 0 error (1) .43 42 4.0 0 timeout (timeout) 900    220 13000   0 error 130   1200 1600 0 error (7) 69   1500 690 0 timeout 900   6500 12000 0
od_false-no-overflow.i error (134) 750    320 7200   0 error (1) 870    890 7700   0 error (1) .49 41 4.6 0 error (1) .47 40 4.1 0 timeout 900   6300 11000 0 unknown 63 1700 750 0 unknown 3.6  180 46   0 unknown .31 52 2.8 0 error (1) .42 40 3.8 0 error .91 65 10   0 error (7) 6.9 320 52 0 error (7) 5.7 290 41 0 error (7) 5.6 290 47 0
printf_false-no-overflow.i error (6) .54 42 4.4 0 error (6) 20    130 260   0 error (1) .47 41 4.2 0 error (1) .46 40 4.6 0 false(no-overflow) 490   910 3100 0 unknown 900 2000 12000 0 unknown 3.5  150 44   0 unknown .21 37 1.9 0 error (1) .44 41 3.9 0 error (1) .27 13 2.9 0 error 230   2000 1800 0 timeout 900   4800 13000 0 timeout 900   6100 12000 0
readlink_false-no-overflow.i error (134) 2.8  40 23   0 error (6) 1.4  49 16   0 error (1) .51 43 4.4 0 error (1) .45 39 4.1 0 timeout 900   6300 11000 0 unknown 39 43 470 0 unknown 3.5  160 45   0 unknown .18 36 2.0 0 error (1) .43 40 3.8 0 error .37 17 4.4 0 timeout 900   1800 8400 0 timeout 900   5000 11000 0 timeout 900   6000 14000 0
realpath_false-no-overflow.i error (134) .36 37 3.1 0 error (6) .78 44 7.5 0 error (1) .48 41 4.4 0 error (1) .44 40 3.9 0 timeout 900   1500 6000 0 unknown 900 1200 13000 0 unknown 3.5  150 50   0 unknown .18 31 1.6 0 error (1) .42 40 3.8 0 timeout (timeout) 900    400 14000   0 error 160   1500 1600 0 error (7) 110   2300 1200 0 timeout 900   6500 12000 0
rm_false-no-overflow.i error (5) 6.4  44 60   0 error (1) 870    400 11000   0 error (1) .47 40 4.0 0 error (1) .45 40 4.0 0 timeout 900   6200 11000 0 unknown 44 500 520 0 unknown 3.5  160 49   0 unknown .21 38 2.0 0 error (1) .44 40 3.7 0 error .46 21 5.5 0 timeout 900   1300 8900 0 timeout 900   6100 11000 0 timeout 900   6100 11000 0
seq_false-no-overflow.i error (134) 1.6  40 15   0 error (6) 1.3  57 13   0 error (1) .49 41 4.9 0 error (1) .44 40 3.6 0 timeout 900   6400 9900 0 unknown 42 500 630 0 unknown .13 35 1.4 0 unknown .15 35 1.4 0 error (1) .43 41 3.9 0 error (1) .25 13 2.8 0 error (7) 4.4 240 39 0 error (7) 4.5 240 38 0 error (7) 4.3 230 34 0
sleep_false-no-overflow.i error (134) .91 39 12   0 error (6) 1.5  49 15   0 error (1) .46 41 4.4 0 error (1) .43 40 4.2 0 unknown 6.5 320 56 0 unknown 900 1000 9100 0 unknown 4.0  170 51   0 unknown .20 32 1.9 0 error (1) .45 40 3.9 0 error (1) .24 12 3.0 0 error 570   2200 5800 0 error (7) 280   3600 3600 0 timeout 900   5100 12000 0
stty_false-no-overflow.i error (134) 73    120 670   0 error (6) 53    210 670   0 error (1) .50 41 4.3 0 error (1) .43 40 3.8 0 error (parsing failed) 2.5 180 22 0 unknown 900 2000 10000 0 unknown 4.2  200 54   0 unknown .27 51 3.7 0 error (1) .42 40 4.2 0 timeout (timeout) 900    370 13000   0 error (7) 4.6 290 37 0 error (7) 4.4 290 36 0 error (7) 5.0 300 42 0
sync_false-no-overflow.i error (134) .27 35 3.3 0 error (6) .65 42 6.9 0 error (1) .49 40 4.4 0 error (1) .44 40 3.9 0 unknown 46   580 490 0 unknown 890 1300 5700 0 unknown 3.4  140 45   0 unknown .17 30 1.5 0 error (1) .42 40 4.2 0 timeout (timeout) 900    150 15000   0 error 200   1400 2400 0 error (7) 110   1800 1400 0 timeout 910   6300 10000 0
tac_false-no-overflow.i error (134) 5.4  41 51   0 error (6) 3.2  52 37   0 error (1) .50 41 4.4 0 error (1) .44 41 4.7 0 timeout 900   6200 8400 0 unknown 42 500 560 0 unknown 3.5  160 46   0 unknown .19 36 2.1 0 error (1) .43 40 4.7 0 error .39 16 4.0 0 timeout 900   3600 7700 0 timeout 900   5000 12000 0 timeout 900   5800 12000 0
tee_false-no-overflow.i error (6) .35 41 3.3 0 error (6) 1.7  52 19   0 error (1) .46 41 4.4 0 error (1) .42 38 3.7 0 timeout 900   3300 11000 0 unknown 43 500 620 0 unknown 3.5  160 50   0 unknown .21 36 2.3 0 error (1) .43 42 4.0 0 error .38 16 5.3 0 timeout 900   12000 7000 0 timeout 900   4500 11000 0 timeout 900   5300 7900 0
test-incomplete_false-no-overflow.i error (5) 32    74 280   0 error (1) 870    760 7100   0 error (1) .48 42 4.5 0 error (1) .46 40 3.8 0 timeout 900   4300 11000 0 unknown 890 1600 8000 0 unknown 3.8  180 48   0 unknown .18 37 2.1 0 error (1) .41 40 3.5 0 error .41 18 5.0 0 error (7) 4.5 230 33 0 error (7) 4.4 240 38 0 error (7) 4.5 240 33 0
touch_false-no-overflow.i error (134) 5.7  45 49   0 error (6) 3.2  140 38   0 error (1) .46 40 3.5 0 error (1) .45 40 3.7 0 timeout 900   6200 9900 0 unknown 47 500 630 0 unknown 3.5  160 44   0 unknown .23 39 2.4 0 error (1) .44 40 4.2 0 error .52 26 5.6 0 timeout 900   2400 5900 0 timeout 900   5300 13000 0 timeout 900   6200 13000 0
uname_false-no-overflow.i error (134) 1.6  41 14   0 error (6) 1.6  160 18   0 error (1) .46 40 4.1 0 error (1) .45 40 4.3 0 timeout 900   6000 11000 0 unknown 43 510 610 0 unknown 3.5  160 46   0 unknown .18 36 2.1 0 error (1) .43 40 3.9 0 error .57 78 5.8 0 timeout 900   3100 7100 0 timeout 900   5400 10000 0 timeout 900   5900 11000 0
uniq_false-no-overflow.i error (134) 5.5  41 43   0 error (6) 2.6  50 29   0 error (1) .46 40 3.8 0 error (1) .43 40 4.2 0 timeout 900   6300 12000 0 unknown 44 510 550 0 unknown 3.5  160 49   0 unknown .21 37 2.3 0 error (1) .42 40 3.7 0 error .41 19 5.6 0 timeout 900   1300 8600 0 timeout 900   5000 13000 0 timeout 900   6100 12000 0
usleep_false-no-overflow.i error (134) .47 37 4.1 0 error (6) .70 45 6.5 0 error (1) .47 40 4.3 0 error (1) .46 42 4.0 0 timeout 900   1200 5800 0 unknown 890 1400 5800 0 unknown 3.9  180 48   0 unknown .18 31 1.5 0 error (1) .41 41 4.0 0 timeout (timeout) 900    97 12000   0 error 200   3000 2300 0 error (7) 200   2900 2500 0 timeout 900   4800 10000 0
uudecode_false-no-overflow.i error (134) 11    48 94   0 error (6) 6.9  98 73   0 error (1) .48 41 4.1 0 error (1) .46 40 4.3 0 error (parsing failed) 2.6 190 22 0 unknown 50 500 710 0 unknown 3.5  160 51   0 unknown .22 40 2.5 0 error (1) .41 40 3.5 0 error .51 23 5.8 0 error (7) 4.5 230 34 0 error (7) 4.7 240 42 0 error (7) 4.5 240 35 0
wc_false-no-overflow.i error (6) .35 42 3.2 0 error (1) 870    780 5000   0 error (1) .48 41 4.6 0 error (1) .45 40 4.6 0 timeout 900   5800 9600 0 unknown 45 510 550 0 unknown 4.0  180 48   0 unknown .23 37 2.1 0 error (1) .45 40 3.9 0 error .42 18 4.7 0 timeout 900   1800 8200 0 timeout 900   4900 13000 0 timeout 900   5500 11000 0
who_false-no-overflow.i error (134) 1.7  42 14   0 error (6) 1.3  50 16   0 error (1) .50 45 4.3 0 error (1) .44 40 4.4 0 timeout 900   6300 9400 0 unknown 40 44 510 0 unknown 3.5  160 42   0 unknown .20 36 1.9 0 error (1) .44 40 3.9 0 error .40 19 5.1 0 error (7) 4.5 230 37 0 error (7) 4.4 230 35 0 error (7) 4.3 230 34 0
whoami-incomplete_false-no-overflow.i - - - - - - - - error (1) .40 40 3.5 0 - - - -
yes_false-no-overflow.i error (134) .33 37 3.0 0 error (6) .70 44 6.4 0 error (1) .49 43 4.8 0 error (1) .51 40 3.8 0 timeout 900   1300 7900 0 unknown 900 1200 9900 0 unknown 3.9  160 49   0 unknown .16 31 1.9 0 error (1) .44 39 3.8 0 timeout (timeout) 900    140 12000   0 error 190   1500 1900 0 error (7) 53   1100 490 0 timeout 900   6700 11000 0
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) .24 32 2.0 0 error (42) 870    6800 4700   0 error (1) .47 41 4.6 0 error (1) .41 40 4.2 0 timeout 900   3400 11000 0 unknown 890 1300 5800 0 timeout 900    960 8800   0 timeout 900    1100 9000   0 error (1) .44 40 4.0 0 timeout (timeout) 900    130 11000   0 error (7) 3.9 220 33 0 error (7) 4.2 230 36 0 error (7) 4.0 230 33 0
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i error (134) .29 37 3.5 0 error (6) .75 44 7.3 0 error (1) .49 40 4.0 0 error (1) .44 40 4.1 0 out of memory 250   15000 2000 0 unknown 900 2700 7600 0 unknown 3.5  150 50   0 unknown .17 31 1.8 0 error (1) .41 37 3.5 0 timeout (timeout) 900    320 12000   0 error 380   1500 4000 0 timeout 900   2500 10000 0 timeout 900   6400 11000 0
chroot-incomplete_true-no-overflow_true-valid-memsafety.i error (134) .59 37 6.1 0 error (6) 1.0  44 11   0 error (1) .46 40 4.7 0 error (1) .44 41 3.9 0 unknown 33   520 340 0 unknown 900 930 12000 0 unknown 3.5  150 49   0 unknown .15 31 1.7 0 error (1) .42 40 3.9 0 timeout (timeout) 900    210 13000   0 error 340   1800 2900 0 timeout 900   4700 10000 0 timeout 900   6000 14000 0
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 14    51 110   0 error (6) 7.2  93 75   0 error (1) .46 41 3.9 0 error (1) .45 40 4.1 0 timeout 900   6100 11000 0 unknown 48 500 650 0 unknown 3.5  160 57   0 unknown .22 38 2.2 0 error (1) .43 41 3.8 0 error .48 23 5.4 0 timeout 900   2000 6800 0 timeout 900   5200 13000 0 timeout 900   5900 11000 0
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) .45 46 3.4 0 error (6) 3.5  160 40   0 error (1) .47 41 4.4 0 error (1) .44 40 4.1 0 timeout 900   3300 10000 0 unknown 49 49 630 0 unknown 3.5  170 44   0 unknown .22 41 2.4 0 error (1) .44 40 3.8 0 error .62 33 7.9 0 error (7) 4.5 230 35 0 error (7) 4.2 230 37 0 error (7) 4.2 240 37 0
dirname_true-no-overflow_true-valid-memsafety.i error (134) .24 31 1.7 0 error (134) 550    12000 6400   0 error (1) .46 40 3.8 0 error (1) .44 40 4.4 0 timeout 900   5200 9500 0 unknown 890 960 7500 0 timeout 900    9900 11000   0 timeout 900    9300 11000   0 error (1) .45 41 4.2 0 timeout (timeout) 900    790 11000   0 error (7) 4.1 230 32 0 error (7) 3.9 230 36 0 error (7) 3.9 230 34 0
du_true-no-overflow_true-valid-memsafety.i error (5) 6.8  44 57   0 error (6) 52    240 550   0 error (1) .47 40 4.3 0 error (1) .47 40 4.1 0 timeout 900   3300 11000 0 unknown 47 510 540 0 unknown 3.5  160 45   0 unknown .22 39 2.3 0 error (1) .44 40 4.2 0 error .49 24 6.5 0 timeout 900   10000 5600 0 timeout 900   4300 9800 0 timeout 900   5500 9900 0
echo_true-no-overflow_true-valid-memsafety.i error (134) .48 38 5.0 0 error (42) 870    4600 3900   0 error (1) .46 40 4.5 0 error (1) .53 40 4.3 0 timeout 900   1000 9600 0 unknown 890 700 11000 0 unknown 4.7  240 66   0 unknown .20 32 1.9 0 error (1) .44 40 4.2 0 timeout (timeout) 900    320 11000   0 timeout 900   2900 8400 0 timeout 900   5300 11000 0 timeout 900   6500 11000 0
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 30    71 260   0 error (6) 32    250 290   0 error (1) .48 45 4.5 0 error (1) .45 40 4.7 0 timeout 900   5900 11000 0 unknown 61 940 750 0 unknown 4.1  190 41   0 unknown .24 40 2.5 0 error (1) .42 40 4.2 0 error .59 30 7.9 0 timeout 900   2700 7700 0 timeout 900   5100 13000 0 timeout 900   5600 12000 0
fold_true-no-overflow_true-valid-memsafety.i error (134) 5.4  42 41   0 error (6) 4.0  56 48   0 error (1) .47 40 4.0 0 error (1) .46 41 4.2 0 timeout 900   930 10000 0 unknown 46 550 550 0 unknown 4.0  180 50   0 unknown .20 37 2.3 0 error (1) .41 39 3.7 0 error .41 19 4.4 0 timeout 900   2200 6800 0 timeout 900   5000 12000 0 timeout 910   4700 12000 0
head_true-no-overflow_true-valid-deref.i error (6) .42 40 2.6 0 error (6) 4.3  61 49   0 error (1) .46 40 3.8 0 error (1) .44 40 4.1 0 unknown 150   880 1200 0 unknown 900 2400 11000 0 unknown 3.7  170 47   0 unknown .21 34 2.1 0 error (1) .44 40 4.5 0 error .38 16 4.9 0 error 230   4100 2200 0 timeout 900   5000 12000 0 timeout 900   6600 11000 0
hostid_true-no-overflow_true-valid-memsafety.i error (134) .26 34 1.9 0 error (134) 560    12000 7400   0 error (1) .50 44 4.5 0 error (1) .44 40 4.0 0 out of memory 530   15000 5900 0 unknown 900 1100 5300 0 timeout 900    12000 11000   0 timeout 900    12000 10000   0 error (1) .42 40 4.2 0 timeout (timeout) 900    980 13000   0 true 9.6 480 74 2 true 18   700 150 2 true 9.7 450 81 2
logname_true-no-overflow_true-valid-memsafety.i error (134) .34 36 2.6 0 error (6) .68 44 6.3 0 error (1) .48 41 4.6 0 error (1) .46 40 4.2 0 out of memory 290   15000 2000 0 unknown 900 1000 9900 0 unknown 3.5  150 43   0 unknown .18 31 1.7 0 error (1) .44 38 3.9 0 timeout (timeout) 900    140 14000   0 error 130   1000 1500 0 error (7) 65   1200 640 0 timeout 900   6500 12000 0
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (5) 230    190 2000   0 error (1) 870    700 4200   0 error (1) .47 42 4.2 0 error (1) .44 41 4.4 0 timeout 900   3100 9100 0 unknown 58 59 680 0 unknown .22 50 2.3 0 unknown .23 50 2.1 0 error (1) .45 41 4.4 0 error .97 63 14   0 error (7) 4.8 230 38 0 error (7) 4.9 250 39 0 error (7) 4.4 230 34 0
mkdir_true-no-overflow_true-valid-memsafety.i error (134) 2.6  43 20   0 error (1) 870    2400 4500   0 error (1) .42 40 4.5 0 error (1) .47 40 4.2 0 timeout 900   6400 11000 0 unknown 47 510 670 0 unknown 3.5  160 47   0 unknown .19 38 2.5 0 error (1) .44 40 4.0 0 error .41 18 5.7 0 timeout 900   2100 6700 0 timeout 900   5100 12000 0 timeout 900   5900 12000 0
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error (134) .30 36 2.4 0 error (6) .73 43 8.4 0 error (1) .45 40 4.6 0 error (1) .47 41 4.0 0 timeout 900   1300 5800 0 unknown 900 1200 13000 0 unknown 3.5  150 46   0 unknown .17 30 1.8 0 error (1) .42 40 4.1 0 timeout (timeout) 900    230 12000   0 error 160   1100 1600 0 error (7) 81   1700 830 0 timeout 910   6600 12000 0
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 760    320 7400   0 error (1) 870    830 4300   0 error (1) .48 40 4.0 0 error (1) .48 40 4.1 0 timeout 900   6300 10000 0 unknown 64 1700 760 0 unknown 3.6  180 47   0 unknown .31 52 3.1 0 error (1) .45 41 3.6 0 error .89 65 12   0 error (7) 6.2 320 52 0 error (7) 5.9 300 51 0 error (7) 5.9 300 46 0
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) .55 43 4.1 0 error (6) 20    130 220   0 error (1) .50 43 4.5 0 error (1) .47 40 4.3 0 unknown 260   850 2200 0 unknown 900 2000 9500 0 unknown 3.5  150 46   0 unknown .19 37 2.3 0 error (1) .43 40 4.0 0 error (1) .28 13 2.8 0 error 330   1900 2400 0 timeout 900   4800 12000 0 timeout 900   6200 12000 0
readlink_true-no-overflow_true-valid-memsafety.i error (134) 2.5  41 26   0 error (6) 1.4  49 15   0 error (1) .48 42 4.1 0 error (1) .46 41 4.1 0 timeout 900   6200 13000 0 unknown 40 45 500 0 unknown 3.5  160 53   0 unknown .18 36 2.5 0 error (1) .42 40 4.3 0 error .40 17 4.2 0 timeout 900   2400 11000 0 timeout 900   5000 12000 0 timeout 900   6000 13000 0
realpath_true-no-overflow_true-valid-memsafety.i error (134) .33 37 3.5 0 error (6) .77 44 7.7 0 error (1) .47 41 4.2 0 error (1) .43 40 4.7 0 timeout 900   1500 6800 0 unknown 900 1200 12000 0 unknown 3.5  150 51   0 unknown .15 31 1.8 0 error (1) .45 39 3.9 0 timeout (timeout) 900    400 13000   0 error 190   1300 2100 0 error (7) 120   3500 1300 0 timeout 900   6500 14000 0
rm_true-no-overflow_true-valid-memsafety.i error (5) 6.0  43 55   0 error (1) 870    400 10000   0 error (1) .49 43 4.6 0 error (1) .46 40 4.1 0 timeout 900   6400 11000 0 unknown 45 510 540 0 unknown 3.5  160 41   0 unknown .19 38 2.1 0 error (1) .45 40 4.3 0 error .46 21 5.2 0 timeout 900   2000 10000 0 timeout 900   5200 11000 0 timeout 900   6100 13000 0
seq_true-no-overflow_true-valid-memsafety.i error (134) 1.6  40 14   0 error (6) 1.3  57 14   0 error (1) .48 41 4.4 0 error (1) .44 40 4.3 0 timeout 900   6300 12000 0 unknown 42 500 490 0 unknown .13 35 1.5 0 unknown .12 35 1.4 0 error (1) .42 40 3.7 0 error (1) .23 13 2.9 0 error (7) 4.5 240 34 0 error (7) 4.4 230 35 0 error (7) 4.4 240 32 0
sleep_true-no-overflow_true-valid-deref.i error (134) .97 38 8.1 0 error (6) 1.4  47 16   0 error (1) .45 42 3.8 0 error (1) .43 40 4.1 0 unknown 6.5 340 65 0 unknown 900 1500 11000 0 unknown 4.0  170 57   0 unknown .16 32 2.0 0 error (1) .44 41 4.1 0 error (1) .23 12 3.0 0 error 630   3900 6400 0 error (7) 280   3900 3900 0 timeout 900   5100 12000 0
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 70    120 600   0 error (6) 54    210 470   0 error (1) .48 40 4.3 0 error (1) .41 40 3.4 0 error (parsing failed) 2.8 200 27 0 unknown 900 2000 9300 0 unknown 4.2  200 59   0 unknown .32 52 3.2 0 error (1) .44 42 4.1 0 timeout (timeout) 900    210 14000   0 error (7) 4.7 290 44 0 error (7) 5.0 290 39 0 error (7) 4.9 280 37 0
sync_true-no-overflow_true-valid-memsafety.i error (134) .30 35 2.6 0 error (6) .66 42 6.4 0 error (1) .49 41 4.3 0 error (1) .41 40 4.1 0 unknown 40   700 530 0 unknown 890 1300 5700 0 unknown 3.4  140 45   0 unknown .14 30 1.7 0 error (1) .44 40 3.8 0 timeout (timeout) 900    150 12000   0 error 170   1400 1700 0 error (7) 100   1700 1200 0 timeout 900   6400 11000 0
tac_true-no-overflow_true-valid-memsafety.i error (134) 5.4  41 45   0 error (6) 3.2  51 40   0 error (1) .49 43 4.3 0 error (1) .47 41 4.4 0 timeout 900   6300 10000 0 unknown 43 510 490 0 unknown 3.5  160 45   0 unknown .18 36 2.1 0 error (1) .43 40 4.0 0 error .36 16 4.1 0 timeout 900   3100 7600 0 timeout 900   5000 12000 0 timeout 900   6000 13000 0
tee_true-no-overflow_true-valid-memsafety.i error (6) .36 41 2.8 0 error (6) 1.7  53 16   0 error (1) .47 41 4.6 0 error (1) .43 40 4.2 0 timeout 900   3300 13000 0 unknown 43 510 550 0 unknown 3.5  160 45   0 unknown .20 36 2.2 0 error (1) .40 40 3.6 0 error .36 16 4.7 0 timeout 900   9900 6100 0 timeout 900   4500 9800 0 timeout 900   5600 9200 0
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (5) 29    73 330   0 error (1) 870    760 6400   0 error (1) .46 41 4.1 0 error (1) .43 40 4.0 0 timeout 900   4600 10000 0 unknown 890 1600 8300 0 unknown 3.8  180 49   0 unknown .21 37 2.5 0 error (1) .43 39 4.0 0 error .38 18 5.1 0 error (7) 4.1 230 36 0 error (7) 4.4 240 38 0 error (7) 4.3 230 34 0
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 5.7  45 54   0 error (6) 3.2  140 37   0 error (1) .48 40 4.4 0 error (1) .46 40 3.7 0 timeout 900   6200 12000 0 unknown 48 510 650 0 unknown 3.5  170 44   0 unknown .20 39 2.9 0 error (1) .47 40 4.3 0 error .55 26 5.6 0 timeout 900   2200 6800 0 timeout 900   5300 11000 0 timeout 900   6000 12000 0
uname_true-no-overflow_true-valid-memsafety.i error (134) 1.6  41 13   0 error (6) 1.6  160 17   0 error (1) .50 41 4.4 0 error (1) .46 40 3.8 0 timeout 900   6000 12000 0 unknown 43 500 470 0 unknown 3.5  160 45   0 unknown .17 35 2.0 0 error (1) .43 41 3.8 0 error .58 77 6.7 0 timeout 900   3100 6700 0 timeout 900   5300 11000 0 timeout 900   5900 13000 0
uniq_true-no-overflow_true-valid-memsafety.i error (134) 5.0  42 47   0 error (6) 2.6  50 30   0 error (1) .47 42 4.1 0 error (1) .45 40 3.7 0 timeout 900   6200 11000 0 unknown 44 500 650 0 unknown 3.5  160 46   0 unknown .21 37 2.4 0 error (1) .42 40 3.8 0 error .41 18 4.5 0 timeout 900   1400 9000 0 timeout 900   5000 11000 0 timeout 900   6100 11000 0
usleep_true-no-overflow_true-valid-memsafety.i error (134) .46 37 4.1 0 error (6) .74 44 7.1 0 error (1) .49 40 3.8 0 error (1) .44 40 4.3 0 unknown 210   880 1500 0 unknown 890 1400 8500 0 unknown 3.9  180 57   0 unknown .17 31 1.6 0 error (1) .46 39 4.3 0 timeout (timeout) 900    98 13000   0 error 210   2700 2200 0 error (7) 190   2900 2500 0 timeout 900   4800 11000 0
uudecode_true-no-overflow_true-valid-memsafety.i error (134) 11    49 93   0 error (6) 6.7  98 77   0 error (1) .46 40 3.8 0 error (1) .42 40 3.7 0 error (parsing failed) 2.4 170 21 0 unknown 51 500 700 0 unknown 3.5  160 42   0 unknown .21 40 2.4 0 error (1) .44 40 3.8 0 error .53 22 5.4 0 error (7) 4.4 230 38 0 error (7) 4.3 240 38 0 error (7) 4.5 240 36 0
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) .34 42 3.1 0 error (1) 870    800 4800   0 error (1) .49 40 4.4 0 error (1) .40 40 4.2 0 timeout 900   5800 11000 0 unknown 45 500 650 0 unknown 4.0  180 49   0 unknown .22 37 2.0 0 error (1) .43 39 4.3 0 error .41 18 5.6 0 timeout 900   2100 8900 0 timeout 900   5000 12000 0 timeout 900   5400 12000 0
who_true-no-overflow_true-valid-memsafety.i error (134) 1.6  41 15   0 error (6) 1.3  51 17   0 error (1) .50 43 4.4 0 error (1) .45 40 4.1 0 timeout 900   6200 12000 0 unknown 40 44 560 0 unknown 3.5  160 41   0 unknown .20 36 1.9 0 error (1) .43 40 4.0 0 error .43 19 5.1 0 error (7) 4.4 230 33 0 error (7) 4.5 240 36 0 error (7) 4.1 230 31 0
whoami-incomplete_true-no-overflow_true-valid-memsafety.i error (134) .32 37 3.0 0 error (134) 660    12000 6800   0 error (1) .46 40 4.0 0 error (1) .45 40 4.3 0 timeout 900   2200 12000 0 unknown 890 1200 8500 0 unknown 3.5  150 47   0 unknown .17 31 1.9 0 error (1) .43 40 4.1 0 timeout (timeout) 900    940 11000   0 true 13   610 100 2 true 29   860 290 2 true 13   570 110 2
yes_true-no-overflow_true-valid-memsafety.i error (134) .34 36 3.0 0 error (6) .74 45 6.6 0 error (1) .48 40 4.2 0 error (1) .48 41 4.1 0 timeout 900   1200 6900 0 unknown 900 1200 12000 0 unknown 3.9  160 50   0 unknown .15 31 1.8 0 error (1) .43 40 3.9 0 timeout (timeout) 900    130 12000   0 error 170   1600 2000 0 error (7) 57   1100 550 0 timeout 900   6600 12000 0
../sv-benchmarks/c/busybox-1.22.0/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 70 2400 4000 23000 0 70 15000 70000 110000 0 70 33 2900 300 0 70 31 2800 290 0 70 49000 280000 540000 0 70 30000 66000 320000 0 70 2900 33000 35000 0 70 2700 25000 30000 0 71 31 2800 280 0 70 22000 8600 300000 0 70 32000 150000 280000 4 70 34000 210000 430000 4 70 45000 300000 580000 4
    correct results 0 0 0 0 0 0 0 0 0 0 2 23 1100 180 4 2 47 1600 430 4 2 23 1000 190 4
        correct true 0 0 0 0 0 0 0 0 0 0 2 23 1100 180 4 2 47 1600 430 4 2 23 1000 190 4
        correct false 0 0 0 0 0 0 0 0 0 0 0 0 0
    correct-unconfimed results 0 0 0 0 2 600 1700 4200 0 0 0 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 2 600 1700 4200 0 0 0 0 0 0 0 0 0
    incorrect results 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0
score (71 tasks, max score: 108) 0 0 0 0 0 0 0 0 0 0 4 4 4
Run set 2ls.sv-comp18.Systems_BusyBox_NoOverflows cbmc.sv-comp18.Systems_BusyBox_NoOverflows cpa-bam-bnb.sv-comp18.Systems_BusyBox_NoOverflows cpa-bam-slicing.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq.sv-comp18.Systems_BusyBox_NoOverflows depthk.sv-comp18.Systems_BusyBox_NoOverflows esbmc-incr.sv-comp18.Systems_BusyBox_NoOverflows esbmc-kind.sv-comp18.Systems_BusyBox_NoOverflows interpchecker.sv-comp18 symbiotic.sv-comp18.Systems_BusyBox_NoOverflows uautomizer.sv-comp18.Systems_BusyBox_NoOverflows ukojak.sv-comp18.Systems_BusyBox_NoOverflows utaipan.sv-comp18.Systems_BusyBox_NoOverflows