Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29794 CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux PeSCo 1.7-svn b8d6131600+ SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a VeriAbs 1.3.10
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-04 22:41:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:44:04 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET 2018-12-10 16:50:17 CET
Run set 2ls.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-bam-bnb.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety divine-explicit.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety divine-smt.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety pesco.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety smack.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety ukojak.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety utaipan.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety veriabs.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19-bam-bnb -disable-java-assertions -heap 10000m -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -w error-witness.graphml --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 status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
basename_false-valid-deref.i error (134) .25 32 2.9 0 false(valid-deref) 12    770 130   0 error (134) 28    340 340   0 error (1) .49 42 5.5 0 error 5.2 280 47 0 false(valid-deref) 350 650 5300 0 error - divine failed with exitcode 1 1.3 170 19 0 error - divine failed with exitcode 1 1.3 170 16 0 false(valid-deref) 540    1000 7900   1 error 4.9 270 44 0 disqualified 750 270   9900 0 false(valid-deref) .65 23 8.6 1 unknown 820   2600 9300 0 timeout 900   950 9200 0 timeout 900   2900 9900 0 unknown .024 7.5 .12  0
head_false-valid-deref.i error (6) .40 39 3.8 0 error (134) 3.5  53 50   0 error (134) .76 29 10   0 error (1) .53 42 5.1 0 error 6.5 300 52 0 out of memory (false(valid-deref)) 22 15000 250 0 error - divine failed with exitcode 1 1.2 160 17 0 error - divine failed with exitcode 1 1.2 160 15 0 out of memory 22    15000 260   0 error 6.2 290 58 0 disqualified 900 9.5 12000 0 error(unknown, slicing-finished) 1.8  96 19   0 unknown 8.8 340 61 0 unknown 8.0 320 58 0 unknown 9.5 360 72 0 unknown .020 7.7 .11  0
sleep_false-valid-deref.i error (134) 1.2  39 11   0 error (134) .88 27 11   0 error (134) .63 27 8.5 0 error (1) .53 44 5.8 0 error 6.1 310 51 0 unknown 900 800 10000 0 error - divine failed with exitcode 1 1.2 160 16 0 error - divine failed with exitcode 1 1.2 160 16 0 unknown .22 32 3.2 0 error 6.0 290 47 0 disqualified 750 480   7400 0 error(returned 1, instr-finished) .38 21 3.7 0 unknown 8.6 360 69 0 unknown 8.8 340 74 0 unknown 8.6 360 73 0 unknown .016 7.4 .11  0
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i error (134) .35 37 3.3 0 error (134) .29 13 3.5 0 error (134) .39 20 5.7 0 error (1) .51 43 4.9 0 error 5.9 290 48 0 false(valid-memtrack) 580 980 7000 0 error - divine failed with exitcode 1 1.2 160 14 0 error - divine failed with exitcode 1 1.2 160 15 0 unknown .20 30 2.5 0 error 6.2 290 51 0 disqualified 840 500   8400 0 false(valid-memtrack) 1.2  22 14   0 unknown 9.1 360 75 0 unknown 8.0 340 65 0 unknown 8.6 350 65 0 unknown .021 7.5 .12  0
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) .27 32 2.4 0 error (42) 880    6400 9800   0 error (134) 21    290 320   0 error (1) .50 44 4.5 0 error 5.1 290 50 0 unknown 900 810 12000 0 error - divine failed with exitcode 1 1.3 170 14 0 error - divine failed with exitcode 1 1.3 170 17 0 timeout 900    1100 11000   0 error 4.9 270 44 0 disqualified 750 200   8600 0 timeout (verification) 900    470 9300   0 error (7) 170   2900 2000 0 timeout 900   1000 11000 0 error (7) 200   2800 2500 0 unknown .026 7.3 .14  0
chroot-incomplete_true-no-overflow_true-valid-memsafety.i error (134) .66 38 7.7 0 error (134) .39 16 4.9 0 error (134) .43 23 6.5 0 error (1) .52 43 5.1 0 error 5.8 290 45 0 unknown 900 2200 7100 0 error - divine failed with exitcode 1 1.2 160 16 0 error - divine failed with exitcode 1 1.2 160 15 0 timeout 900    4400 7900   0 error 6.0 300 45 0 disqualified 750 370   6800 0 timeout (verification) 900    68 14000   0 unknown 8.9 340 72 0 unknown 9.1 370 78 0 unknown 7.6 350 61 0 unknown .031 7.8 .11  0
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 15    89 190   0 error (134) 7.1  84 87   0 error (134) 1.3  47 16   0 error (1) .50 42 4.6 0 error 7.1 310 55 0 out of memory (false(no-overflow)) 22 15000 280 0 error - divine failed with exitcode 1 1.2 170 20 0 error - divine failed with exitcode 1 1.2 170 19 0 out of memory 22    15000 230   0 error 6.3 290 52 0 disqualified 900 9.6 12000 0 error(unknown, slicing-finished) 14    180 120   0 unknown 8.4 350 64 0 unknown 8.5 340 65 0 unknown 8.5 330 65 0 unknown .022 7.1 .20  0
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) .47 47 4.5 0 error (134) 3.0  130 40   0 error (134) 2.8  79 39   0 error (1) .50 44 5.2 0 error 6.9 310 57 0 out of memory (false(no-overflow)) 22 15000 280 0 error - divine failed with exitcode 1 1.2 170 16 0 error - divine failed with exitcode 1 1.3 170 19 0 out of memory 22    15000 270   0 error 7.2 300 54 0 disqualified 900 9.8 13000 0 error(unknown, slicing-finished) 16    330 170   0 unknown 9.4 350 68 0 unknown 8.4 340 69 0 unknown 9.0 330 77 0 unknown .021 7.4 .13  0
dirname_true-no-overflow_true-valid-memsafety.i error (134) .24 31 2.6 0 out of memory 590    13000 6700   0 error (134) 1.1  32 15   0 error (1) .52 44 5.0 0 error 5.1 290 42 0 unknown 900 920 11000 0 error - divine failed with exitcode 1 1.3 170 17 0 error - divine failed with exitcode 1 1.3 170 16 0 timeout 900    4400 11000   0 error 5.1 290 41 0 disqualified 880 400   9500 0 error(unknown, cex-confirmation) .65 27 8.1 0 timeout 900   3200 11000 0 timeout 900   940 8700 0 timeout 900   2300 12000 0 unknown .046 7.4 .11  0
du_true-no-overflow_true-valid-memsafety.i error (134) 7.9  72 96   0 error (134) 62    220 710   0 error (134) .70 40 8.4 0 error (1) .55 43 4.7 0 error 6.7 300 56 0 out of memory (false(no-overflow)) 22 15000 240 0 error - divine failed with exitcode 1 1.3 160 15 0 error - divine failed with exitcode 1 1.3 160 17 0 out of memory 22    15000 320   0 error 6.8 310 59 0 disqualified 750 3300   8900 0 error(unknown, slicing-finished) 41    210 440   0 unknown 9.4 370 82 0 unknown 8.9 360 77 0 unknown 8.6 320 63 0 unknown .023 7.8 .18  0
echo_true-no-overflow_true-valid-memsafety.i error (134) .55 38 6.6 0 error (42) 880    7200 7200   0 error (134) .50 22 7.1 0 error (1) .50 42 4.5 0 error 6.0 290 53 0 unknown 900 1700 10000 0 error - divine failed with exitcode 1 1.2 160 15 0 error - divine failed with exitcode 1 1.2 160 18 0 unknown .23 32 2.8 0 error 6.0 300 43 0 disqualified 750 170   11000 0 timeout (verification) 900    680 7900   0 unknown 7.7 330 71 0 unknown 9.0 340 71 0 unknown 8.5 360 72 0 unknown .025 7.7 .088 0
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 35    130 470   0 error (134) 34    210 460   0 error (134) .51 29 6.9 0 error (1) .53 43 4.9 0 error 7.0 300 63 0 out of memory (false(no-overflow)) 24 15000 290 0 error - divine failed with exitcode 1 1.2 170 16 0 error - divine failed with exitcode 1 1.2 170 17 0 out of memory 22    15000 280   0 error 6.9 310 58 0 disqualified 900 9.5 13000 0 error(unknown, slicing-finished) 25    270 220   0 unknown 8.6 360 70 0 unknown 8.9 370 72 0 unknown 9.2 360 70 0 unknown .025 7.8 .15  0
fold_true-no-overflow_true-valid-memsafety.i error (134) 6.2  57 88   0 error (134) 3.7  50 49   0 error (134) .45 26 5.6 0 error (1) .52 43 5.2 0 error 6.5 300 57 0 out of memory (false(no-overflow)) 22 15000 270 0 error - divine failed with exitcode 1 1.3 160 15 0 error - divine failed with exitcode 1 1.2 160 14 0 out of memory 22    15000 280   0 error 6.5 300 58 0 disqualified 900 9.7 11000 0 error(unknown, slicing-finished) 8.9  170 77   0 unknown 9.1 360 80 0 unknown 8.9 350 75 0 unknown 8.7 340 68 0 unknown .021 7.6 .13  0
head_true-no-overflow_true-valid-memsafety.i error (6) .38 40 4.4 0 error (134) 3.5  54 44   0 error (134) .74 27 9.3 0 error (1) .52 42 5.1 0 error 6.6 300 60 0 out of memory (false(no-overflow)) 22 15000 310 0 error - divine failed with exitcode 1 1.2 160 17 0 error - divine failed with exitcode 1 1.7 160 30 0 out of memory 22    15000 260   0 error 6.4 300 56 0 disqualified 900 9.6 12000 0 error(unknown, slicing-finished) 1.8  97 19   0 unknown 8.3 340 72 0 unknown 8.5 330 67 0 unknown 8.4 340 64 0 unknown .050 6.9 .12  0
hostid_true-no-overflow_true-valid-memsafety.i error (134) .26 34 2.2 0 out of memory 570    13000 6600   0 error (134) .26 16 3.1 0 error (1) .52 42 6.2 0 error 5.1 280 45 0 unknown 900 670 10000 0 error - divine failed with exitcode 1 1.3 170 17 0 error - divine failed with exitcode 1 1.3 170 21 0 timeout 900    1600 9200   0 error 5.1 280 47 0 disqualified 880 400   8100 0 timeout (verification) 900    2000 13000   0 timeout 900   2200 11000 0 timeout 900   840 11000 0 timeout 900   1800 10000 0 unknown .026 6.9 .10  0
logname_true-no-overflow_true-valid-memsafety.i error (134) .34 37 4.0 0 error (134) .25 14 3.7 0 error (134) .30 19 2.9 0 error (1) .48 43 5.1 0 error 5.8 300 55 0 false(valid-deref) 830 1500 7200 -16 error - divine failed with exitcode 1 1.2 160 15 0 error - divine failed with exitcode 1 1.2 160 18 0 unknown .19 30 2.7 0 error 5.5 280 46 0 disqualified 890 440   9200 0 error(unknown, cex-confirmation) .67 24 8.2 0 unknown 8.6 370 69 0 unknown 8.6 330 69 0 unknown 8.8 370 76 0 unknown .022 7.3 .11  0
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 300    340 3000   0 error (134) 3.6  55 45   0 error (134) 1.1  58 13   0 error (1) .53 42 4.9 0 error 8.2 330 70 0 out of memory (false(no-overflow)) 23 15000 300 0 error - divine failed with exitcode 1 1.3 170 20 0 error - divine failed with exitcode 1 1.3 170 16 0 out of memory 22    15000 260   0 error 8.6 370 74 0 disqualified 750 3500   9400 0 error(unknown, slicing-finished) 210    1000 1900   0 error (7) 18   350 140 0 error (7) 19   360 160 0 error (7) 18   360 150 0 unknown .026 7.7 .091 0
mkdir_true-no-overflow_true-valid-memsafety.i error (134) 3.1  45 31   0 error 880    1100 3300   0 error (134) 2.4  64 31   0 error (1) .51 43 5.3 0 error 6.5 300 52 0 out of memory (false(no-overflow)) 22 15000 260 0 error - divine failed with exitcode 1 1.2 160 16 0 error - divine failed with exitcode 1 1.3 160 17 0 out of memory 22    15000 300   0 error 7.0 310 60 0 disqualified 900 9.9 14000 0 error(unknown, slicing-finished) 14    180 120   0 unknown 8.8 360 69 0 unknown 9.2 340 75 0 unknown 8.7 350 66 0 unknown .021 7.7 .15  0
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error (134) .31 36 3.3 0 error (134) .28 14 3.9 0 error (134) .22 17 2.6 0 error (1) .51 42 4.8 0 error 5.4 290 40 0 unknown 900 1700 8500 0 error - divine failed with exitcode 1 1.3 170 17 0 error - divine failed with exitcode 1 1.3 170 18 0 unknown .19 30 2.7 0 error 5.8 280 49 0 disqualified 750 450   7500 0 timeout (verification) 900    64 11000   0 unknown 8.8 350 68 0 unknown 8.7 330 73 0 unknown 8.6 350 69 0 unknown .023 7.6 .10  0
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 900    670 11000   0 error 880    670 4700   0 error (134) 3.1  90 42   0 error (1) .51 43 4.6 0 error 9.1 390 79 0 out of memory (false(no-overflow)) 22 15000 250 0 error - divine failed with exitcode 1 1.3 170 15 0 error - divine failed with exitcode 1 1.3 170 16 0 out of memory 22    15000 280   0 error 8.4 380 75 0 disqualified 900 10   13000 0 error(unknown, slicing-finished) 90    860 670   0 unknown 9.4 350 80 0 unknown 9.8 360 79 0 unknown 11   370 81 0 unknown .045 6.7 .080 0
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) .57 43 4.8 0 error (134) 23    110 290   0 error (134) .46 25 4.9 0 error (1) .51 43 5.1 0 error 6.5 300 60 0 unknown 900 2000 7600 0 error - divine failed with exitcode 1 1.3 160 17 0 error - divine failed with exitcode 1 1.2 160 15 0 unknown .24 36 3.0 0 error 6.4 280 56 0 disqualified 750 320   9800 0 error(returned 1, instr-finished) 2.5  110 29   0 unknown 8.8 370 79 0 unknown 8.1 320 66 0 unknown 9.0 370 71 0 unknown .028 7.3 .13  0
readlink_true-no-overflow_true-valid-memsafety.i error (134) 3.2  41 35   0 error (134) .82 27 13   0 error (134) 1.9  53 25   0 error (1) .53 42 4.9 0 error 6.7 300 52 0 out of memory (false(no-overflow)) 22 15000 260 0 error - divine failed with exitcode 1 1.2 160 15 0 error - divine failed with exitcode 1 1.2 160 15 0 out of memory 22    15000 290   0 error 6.5 300 54 0 disqualified 890 760   6400 0 error(unknown, slicing-finished) 5.6  95 66   0 unknown 8.6 350 79 0 unknown 9.0 360 71 0 unknown 8.6 360 65 0 unknown .030 7.1 .10  0
realpath_true-no-overflow_true-valid-memsafety.i error (134) .35 37 3.9 0 error (134) .30 14 5.4 0 error (134) .38 20 4.7 0 error (1) .53 42 4.8 0 error 5.5 280 43 0 unknown 900 1600 8700 0 error - divine failed with exitcode 1 1.2 160 20 0 error - divine failed with exitcode 1 1.2 160 20 0 unknown .22 31 2.2 0 error 6.1 290 58 0 disqualified 750 430   7100 0 timeout (verification) 900    76 11000   0 unknown 8.7 350 63 0 unknown 8.4 350 75 0 unknown 9.0 360 78 0 unknown .024 7.6 .11  0
rm_true-no-overflow_true-valid-memsafety.i error (134) 7.2  68 93   0 error 880    270 12000   0 error (134) 1.2  45 17   0 error (1) .52 42 4.8 0 error 6.8 300 57 0 out of memory (false(no-overflow)) 22 15000 260 0 error - divine failed with exitcode 1 1.2 160 19 0 error - divine failed with exitcode 1 1.2 160 17 0 out of memory 22    15000 260   0 error 6.9 300 57 0 disqualified 140 580   1300 0 error(unknown, slicing-finished) 44    210 450   0 unknown 9.2 360 79 0 unknown 8.9 360 81 0 unknown 8.4 320 71 0 unknown .026 7.6 .13  0
seq_true-no-overflow_true-valid-memsafety.i error (134) 1.8  40 22   0 error (134) .71 21 10   0 error (134) 1.1  41 12   0 error (1) .50 42 4.8 0 error 6.4 310 56 0 out of memory (false(no-overflow)) 22 15000 270 0 error - divine failed with exitcode 1 1.2 160 15 0 error - divine failed with exitcode 1 1.2 160 20 0 out of memory 22    15000 260   0 error 6.3 310 60 0 disqualified 900 9.2 13000 0 error(returned 1, instr-finished) 4.5  83 53   0 unknown 8.5 360 78 0 unknown 8.7 360 82 0 unknown 8.3 330 64 0 unknown .021 7.7 .094 0
sleep_true-no-overflow_true-valid-memsafety.i error (134) 1.2  39 11   0 error (134) .90 27 12   0 error (134) .67 26 9.8 0 error (1) .51 42 4.8 0 error 6.2 300 50 0 unknown 900 870 12000 0 error - divine failed with exitcode 1 1.2 160 16 0 error - divine failed with exitcode 1 1.3 160 13 0 unknown .23 32 2.6 0 error 5.9 280 55 0 disqualified 750 480   8500 0 error(returned 1, instr-finished) .35 21 3.5 0 unknown 8.9 360 77 0 unknown 8.8 370 72 0 unknown 8.3 360 79 0 unknown .023 7.6 .11  0
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 78    210 790   0 error (134) 66    180 800   0 error (134) 1.3  63 18   0 error (1) .51 43 4.8 0 error 10   510 100 0 out of memory (false(no-overflow)) 23 15000 270 0 error - divine failed with exitcode 1 1.3 160 19 0 error - divine failed with exitcode 1 1.3 160 18 0 out of memory 22    15000 310   0 error 10   510 84 0 disqualified 760 660   5500 0 timeout (instrumentation) 900    520 12000   0 unknown 9.5 350 77 0 unknown 10   380 85 0 unknown 9.8 370 83 0 unknown .025 7.8 .092 0
sync_true-no-overflow_true-valid-memsafety.i error (134) .30 35 3.2 0 error (134) .21 11 2.6 0 error (134) .37 21 4.6 0 error (1) .52 42 5.0 0 error 5.4 290 45 0 unknown 900 610 13000 0 error - divine failed with exitcode 1 1.3 170 18 0 error - divine failed with exitcode 1 1.3 170 18 0 unknown .19 30 2.7 0 error 5.3 290 49 0 disqualified 890 460   7800 0 timeout (verification) 900    160 8300   0 unknown 8.1 350 65 0 unknown 7.8 340 68 0 unknown 8.1 340 72 0 unknown .025 7.6 .12  0
tac_true-no-overflow_true-valid-memsafety.i error (134) 6.2  57 68   0 error (134) 2.6  44 35   0 error (134) 1.0  40 15   0 error (1) .49 42 5.2 0 error 6.3 300 51 0 out of memory (false(no-overflow)) 22 15000 290 0 error - divine failed with exitcode 1 1.2 160 15 0 error - divine failed with exitcode 1 1.2 160 16 0 out of memory 22    15000 300   0 error 6.7 300 55 0 disqualified 750 710   7100 0 error(unknown, slicing-finished) 7.1  110 86   0 unknown 9.1 370 73 0 unknown 8.6 360 71 0 unknown 8.0 340 65 0 unknown .023 7.6 .13  0
tee_true-no-overflow_true-valid-memsafety.i error (134) 4.0  49 47   0 error (134) 1.2  32 15   0 error (134) 1.1  46 14   0 error (1) .52 42 5.6 0 error 6.5 290 56 0 out of memory (false(no-overflow)) 22 15000 280 0 error - divine failed with exitcode 1 1.2 160 18 0 error - divine failed with exitcode 1 1.2 160 15 0 out of memory 22    15000 320   0 error 6.4 300 61 0 disqualified 750 3300   9200 0 error(unknown, slicing-finished) 6.2  110 66   0 unknown 8.0 320 66 0 unknown 8.7 360 71 0 unknown 8.0 330 71 0 unknown .025 7.2 .15  0
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 37    130 380   0 error 880    690 5900   0 error (134) .99 35 15   0 error (1) .52 43 4.5 0 error 6.8 300 66 0 unknown 900 15000 5900 0 error - divine failed with exitcode 1 1.2 160 15 0 error - divine failed with exitcode 1 1.2 160 16 0 unknown .24 37 2.8 0 error 6.6 290 61 0 disqualified 750 490   7500 0 error(unknown, slicing-finished) 2.7  87 21   0 unknown 9.3 360 80 0 unknown 9.1 350 83 0 unknown 8.7 340 71 0 unknown .026 7.3 .11  0
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 6.5  67 69   0 error (134) 2.8  110 36   0 error (134) 2.5  69 31   0 error (1) .53 44 5.8 0 error 7.2 310 56 0 out of memory (false(no-overflow)) 22 15000 250 0 error - divine failed with exitcode 1 1.3 160 17 0 error - divine failed with exitcode 1 1.2 160 17 0 out of memory 22    15000 290   0 error 6.8 290 63 0 disqualified 900 9.8 11000 0 error(unknown, slicing-finished) 11    270 100   0 unknown 9.0 320 75 0 unknown 8.6 330 69 0 unknown 9.1 370 71 0 unknown .022 7.3 .11  0
uname_true-no-overflow_true-valid-memsafety.i error (134) 1.9  41 21   0 error (134) 1.1  120 16   0 error (134) 2.3  62 29   0 error (1) .53 44 5.1 0 error 6.7 310 56 0 out of memory (false(no-overflow)) 22 15000 250 0 error - divine failed with exitcode 1 1.2 160 16 0 error - divine failed with exitcode 1 1.3 160 16 0 out of memory 22    15000 300   0 error 6.9 300 58 0 disqualified 890 760   8800 0 error(unknown, slicing-finished) 5.7  110 54   0 unknown 8.6 370 67 0 unknown 8.5 360 70 0 unknown 8.6 360 69 0 unknown .022 7.6 .091 0
uniq_true-no-overflow_true-valid-memsafety.i error (134) 5.8  58 67   0 error (134) 2.0  39 25   0 error (134) 1.2  43 15   0 error (1) .50 42 5.3 0 error 6.6 310 59 0 out of memory (false(no-overflow)) 22 15000 270 0 error - divine failed with exitcode 1 1.2 170 15 0 error - divine failed with exitcode 1 1.2 170 20 0 out of memory 22    15000 290   0 error 6.8 300 52 0 disqualified 900 9.7 11000 0 error(unknown, slicing-finished) 9.7  140 110   0 unknown 9.0 360 76 0 unknown 8.1 340 67 0 unknown 8.3 330 70 0 unknown .030 7.5 .095 0
usleep_true-no-overflow_true-valid-memsafety.i error (134) .48 37 6.1 0 error (134) .25 13 3.5 0 error (134) .73 26 9.2 0 error (1) .53 43 5.3 0 error 5.8 300 48 0 false(valid-deref) 85 350 990 -16 error - divine failed with exitcode 1 1.2 160 17 0 error - divine failed with exitcode 1 1.2 160 15 0 unknown .23 31 2.3 0 error 5.7 290 47 0 disqualified 750 410   9700 0 timeout (verification) 900    180 8000   0 unknown 8.6 360 78 0 unknown 7.9 320 62 0 unknown 7.9 340 65 0 unknown .024 7.5 .11  0
uudecode_true-no-overflow_true-valid-memsafety.i error (134) 12    81 170   0 error (134) 6.1  85 69   0 error (134) 2.0  58 29   0 error (1) .49 42 5.2 0 error 7.0 310 63 0 out of memory (false(no-overflow)) 22 15000 270 0 error - divine failed with exitcode 1 1.2 160 16 0 error - divine failed with exitcode 1 1.3 160 16 0 out of memory 22    15000 290   0 error 7.0 310 55 0 disqualified 900 9.8 13000 0 error(unknown, slicing-finished) 22    250 180   0 unknown 8.8 350 72 0 unknown 8.5 350 81 0 unknown 9.0 330 83 0 unknown .021 7.6 .089 0
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) .37 42 4.5 0 error 880    580 6000   0 error (134) .45 25 6.2 0 error (1) .50 43 5.2 0 error 6.5 300 50 0 out of memory (false(no-overflow)) 22 15000 250 0 error - divine failed with exitcode 1 1.2 160 14 0 error - divine failed with exitcode 1 1.2 160 17 0 out of memory 22    15000 240   0 error 6.2 300 57 0 disqualified 890 840   9800 0 error(unknown, slicing-finished) 7.9  130 68   0 unknown 8.6 340 72 0 unknown 8.4 330 75 0 unknown 8.9 370 66 0 unknown .039 7.2 .13  0
who_true-no-overflow_true-valid-memsafety.i error (134) 2.1  42 21   0 error (134) .78 27 12   0 error (134) 1.7  50 21   0 error (1) .50 42 4.8 0 error 6.5 300 51 0 out of memory (false(no-overflow)) 22 15000 270 0 error - divine failed with exitcode 1 1.3 170 16 0 error - divine failed with exitcode 1 1.2 170 16 0 out of memory 23    15000 350   0 error 6.3 300 55 0 disqualified 750 720   9500 0 error(unknown, slicing-finished) 5.9  100 58   0 unknown 8.6 350 64 0 unknown 8.4 320 70 0 unknown 9.1 360 75 0 unknown .022 7.2 .12  0
whoami-incomplete_true-no-overflow_true-valid-memsafety.i error (134) .35 37 3.2 0 error (134) .22 12 3.3 0 error (134) .33 19 3.2 0 error (1) .54 43 5.1 0 error 5.5 280 53 0 unknown 900 700 9600 0 error - divine failed with exitcode 1 1.2 160 16 0 error - divine failed with exitcode 1 1.2 160 15 0 unknown .20 31 2.3 0 error 5.9 290 46 0 disqualified 890 470   10000 0 timeout (verification) 900    150 8700   0 unknown 8.4 360 64 0 unknown 8.7 360 73 0 unknown 8.5 330 66 0 unknown .023 7.8 .084 0
yes_true-no-overflow_true-valid-memsafety.i error (134) .34 37 3.5 0 error (134) .24 12 3.1 0 error (134) .30 19 3.9 0 error (1) .51 43 4.4 0 error 5.8 300 50 0 unknown 360 1200 3800 0 error - divine failed with exitcode 1 1.2 160 17 0 error - divine failed with exitcode 1 1.2 160 19 0 unknown .21 30 2.5 0 error 6.0 290 53 0 disqualified 760 520   8900 0 timeout (verification) 900    110 11000   0 unknown 8.1 320 63 0 unknown 7.5 330 65 0 unknown 7.9 350 65 0 unknown .025 7.6 .099 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 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 40 1400 3100 17000 0 40 7500 46000 66000 0 40 88 2100 1200 0 40 21 1700 200 0 40 260 12000 2200 0 40 14000 360000 160000 -32 40 50 6600 660 0 40 50 6600 690 0 40 4600 340000 53000 1 40 260 12000 2200 0 40 32000 23000 380000 0 40 10000    9900 120000   1 40 3100 24000 36000 0 40 3900 16000 43000 0 40 3200 22000 37000 0 40 1.0 300 4.7 0
    correct results 0 0 0 0 0 0 0 0 1 540 1000 7900 1 0 0 1 .65 23 8.6 1 0 0 0 0
        correct true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct false 0 0 0 0 0 0 0 0 1 540 1000 7900 1 0 0 1 .65 23 8.6 1 0 0 0 0
    correct-unconfimed results 0 1 12 770 130 0 0 0 0 2 930 1600 12000 0 0 0 0 0 0 1 1.2  22 14   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 1 12 770 130 0 0 0 0 2 930 1600 12000 0 0 0 0 0 0 1 1.2  22 14   0 0 0 0 0
    incorrect results 0 0 0 0 0 2 910 1900 8200 -32 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 0 0 0
        incorrect false 0 0 0 0 0 2 910 1900 8200 -32 0 0 0 0 0 0 0 0 0 0
score (40 tasks, max score: 76) 0 0 0 0 0 -32 0 0 1 0 0 1 0 0 0 0
Run set 2ls.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-bam-bnb.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety divine-explicit.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety divine-smt.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety pesco.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety smack.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety ukojak.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety utaipan.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety veriabs.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety