| Tool | 2LS 0.5.0 | BLAST 2.7.3 | CBMC 5.6 | Ceagle Ceagle 1.3 @ 53cfa89 | CPAchecker 1.6.1-svn 23987 | CPAchecker 1.6.1-svn 24048 | DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 | ESBMC ESBMC version 3.1 64-bit x86_64 linux | SMACK+Corral 1.7.2 | symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a | ULTIMATE Automizer f7c3ed31 | ULTIMATE Kojak f7c3ed31 | ULTIMATE Taipan f7c3ed31 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 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-11 09:48:02 CET [[ 2017-01-14 21:34:09 CET ]] [[ 2017-01-14 21:49:16 CET ]] [[ 2017-01-14 21:34:25 CET ]] [[ 2017-01-14 21:52:20 CET ]] | 2017-01-11 10:12:01 CET [[ 2017-01-14 21:12:06 CET ]] [[ 2017-01-14 21:17:30 CET ]] [[ 2017-01-14 21:14:22 CET ]] [[ 2017-01-14 21:21:19 CET ]] | 2017-01-11 10:20:18 CET [[ 2017-01-14 21:14:41 CET ]] [[ 2017-01-14 21:35:33 CET ]] [[ 2017-01-14 21:19:46 CET ]] [[ 2017-01-14 21:37:38 CET ]] | 2017-01-11 09:49:51 CET [[ 2017-01-14 20:52:01 CET ]] [[ 2017-01-14 21:02:28 CET ]] [[ 2017-01-14 20:57:34 CET ]] [[ 2017-01-14 21:06:31 CET ]] | 2017-01-11 10:34:02 CET [[ 2017-01-14 21:41:36 CET ]] [[ 2017-01-14 21:45:05 CET ]] [[ 2017-01-14 21:43:06 CET ]] [[ 2017-01-14 21:46:49 CET ]] | 2017-01-11 10:43:32 CET [[ 2017-01-14 21:41:35 CET ]] [[ 2017-01-14 21:45:05 CET ]] [[ 2017-01-14 21:43:06 CET ]] [[ 2017-01-14 21:46:49 CET ]] | 2017-01-13 04:38:11 CET [[ 2017-01-14 23:48:17 CET ]] [[ 2017-01-14 23:57:43 CET ]] [[ 2017-01-14 23:52:59 CET ]] [[ 2017-01-15 00:03:21 CET ]] | 2017-01-13 04:51:53 CET [[ 2017-01-15 00:05:22 CET ]] [[ 2017-01-15 00:31:32 CET ]] [[ 2017-01-15 00:11:25 CET ]] [[ 2017-01-15 00:39:18 CET ]] | 2017-01-13 04:52:43 CET [[ 2017-01-15 00:23:14 CET ]] [[ 2017-01-15 00:35:58 CET ]] [[ 2017-01-15 00:29:47 CET ]] [[ 2017-01-15 00:40:29 CET ]] | 2017-01-13 05:20:12 CET [[ 2017-01-15 00:51:08 CET ]] [[ 2017-01-15 01:00:54 CET ]] [[ 2017-01-15 00:55:05 CET ]] [[ 2017-01-15 01:06:26 CET ]] | 2017-01-13 05:51:33 CET [[ 2017-01-15 01:19:13 CET ]] [[ 2017-01-15 01:22:10 CET ]] [[ 2017-01-15 01:20:47 CET ]] [[ 2017-01-15 01:23:25 CET ]] | 2017-01-13 06:35:22 CET [[ 2017-01-15 01:30:25 CET ]] [[ 2017-01-15 01:30:43 CET ]] [[ 2017-01-15 01:30:33 CET ]] [[ 2017-01-15 01:30:54 CET ]] | 2017-01-14 05:56:27 CET [[ 2017-01-15 04:08:20 CET ]] [[ 2017-01-15 04:18:47 CET ]] [[ 2017-01-15 04:12:29 CET ]] [[ 2017-01-15 04:25:58 CET ]] | 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 ]] | 2017-01-14 06:16:04 CET [[ 2017-01-15 05:34:44 CET ]] [[ 2017-01-15 05:49:53 CET ]] [[ 2017-01-15 05:35:06 CET ]] [[ 2017-01-15 05:51:11 CET ]] | 2017-01-14 06:29:29 CET [[ 2017-01-15 05:44:30 CET ]] [[ 2017-01-15 05:59:35 CET ]] [[ 2017-01-15 05:44:48 CET ]] [[ 2017-01-15 06:00:32 CET ]] | 2017-01-14 16:15:06 CET [[ 2017-01-15 05:45:52 CET ]] [[ 2017-01-15 06:00:59 CET ]] [[ 2017-01-15 05:46:10 CET ]] [[ 2017-01-15 06:02:27 CET ]] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Run set | 2ls.sv-comp17.Systems_BusyBox_MemSafety | blast.sv-comp17 | cbmc.sv-comp17.Systems_BusyBox_MemSafety | ceagle.sv-comp17.Systems_BusyBox_MemSafety | cpa-bam-bnb.sv-comp17.Systems_BusyBox_MemSafety | cpa-kind.sv-comp17.Systems_BusyBox_MemSafety | cpa-seq.sv-comp17.Systems_BusyBox_MemSafety | depthk.sv-comp17.Systems_BusyBox_MemSafety | esbmc.sv-comp17.Systems_BusyBox_MemSafety | esbmc-falsi.sv-comp17.Systems_BusyBox_MemSafety | esbmc-incr.sv-comp17.Systems_BusyBox_MemSafety | esbmc-kind.sv-comp17.Systems_BusyBox_MemSafety | smack.sv-comp17.Systems_BusyBox_MemSafety | symbiotic4.sv-comp17.Systems_BusyBox_MemSafety | uautomizer.sv-comp17.Systems_BusyBox_MemSafety | ukojak.sv-comp17.Systems_BusyBox_MemSafety | utaipan.sv-comp17.Systems_BusyBox_MemSafety | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Options | --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-11_1012.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-11_1012.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-11_1012.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-11_1012.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-11_1034.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-11_1034.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-11_1034.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-11_1034.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | --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 ]] | [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ../../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 | status | cpu (s) | mem (MB) | energy (J) | score |
| basename_false-unreach-call_true-no-overflow_false-valid-deref.i | error (8) | .35 | 32 | 3.0 | 0 | unknown | .067 | 9.2 | .65 | 0 | false(valid-deref) | 9.1 | 690 | 110 | 1 | unknown | .052 | 8.4 | .57 | 0 | error (1) | .43 | 40 | 3.9 | 0 | error (1) | .41 | 38 | 4.2 | 0 | error | 4.2 | 280 | 34 | 0 | unknown | 890 | 1200 | 7100 | 0 | out of memory | 360 | 15000 | 3400 | 0 | timeout | 900 | 530 | 6600 | 0 | timeout | 900 | 550 | 6200 | 0 | unknown | .19 | 28 | 1.8 | 0 | timeout | 880 | 290 | 11000 | 0 | false(valid-deref) | 1.3 | 64 | 13 | 1 | error | 44 | 820 | 360 | 0 | error | 760 | 1400 | 10000 | 0 | error | 80 | 1200 | 740 | 0 |
| head_true-no-overflow_false-valid-deref.i | error (8) | 11 | 1100 | 120 | 0 | unknown | .082 | 11 | .48 | 0 | error (1) | 3.4 | 65 | 41 | 0 | unknown | .11 | 9.2 | 1.2 | 0 | error (1) | .42 | 40 | 4.0 | 0 | error (1) | .40 | 38 | 3.4 | 0 | error | 3.5 | 260 | 27 | 0 | unknown | 900 | 2900 | 10000 | 0 | out of memory | 820 | 15000 | 7500 | 0 | timeout | 900 | 5300 | 7000 | 0 | timeout | 900 | 5400 | 7400 | 0 | unknown | .21 | 34 | 2.3 | 0 | timeout | 900 | 7.5 | 12000 | 0 | false(valid-deref) | 22 | 1500 | 230 | 1 | unknown | 5.4 | 310 | 42 | 0 | unknown | 5.8 | 310 | 49 | 0 | unknown | 5.4 | 310 | 43 | 0 |
| sleep_true-no-overflow_false-valid-deref.i | error (8) | 1.7 | 180 | 19 | 0 | unknown | .050 | 7.9 | .41 | 0 | error (1) | 1.0 | 36 | 11 | 0 | unknown | .057 | 9.8 | .48 | 0 | error (1) | .43 | 40 | 4.1 | 0 | error (1) | .43 | 37 | 3.2 | 0 | error | 3.4 | 260 | 28 | 0 | unknown | 900 | 2500 | 12000 | 0 | out of memory | 250 | 15000 | 3400 | 0 | timeout | 900 | 1800 | 12000 | 0 | timeout | 900 | 1800 | 12000 | 0 | unknown | .23 | 32 | 2.3 | 0 | false(valid-deref) | 7.7 | 130 | 98 | 1 | unknown | 5.2 | 700 | 64 | 0 | unknown | 5.9 | 330 | 47 | 0 | unknown | 5.4 | 310 | 43 | 0 | unknown | 5.9 | 310 | 45 | 0 |
| chgrp-incomplete_true-no-overflow_false-valid-memtrack.i | error (8) | .45 | 48 | 4.9 | 0 | unknown | .052 | 8.0 | .46 | 0 | error (1) | .38 | 29 | 4.4 | 0 | unknown | .065 | 9.0 | .69 | 0 | error (1) | .41 | 40 | 4.3 | 0 | error (1) | .41 | 40 | 4.3 | 0 | error | 3.7 | 270 | 28 | 0 | unknown | 900 | 2800 | 5400 | 0 | out of memory | 730 | 15000 | 6900 | 0 | timeout | 900 | 2000 | 6500 | 0 | timeout | 900 | 2000 | 5500 | 0 | unknown | .20 | 31 | 2.4 | 0 | false(valid-memtrack) | 840 | 400 | 8400 | 1 | false(valid-memtrack) | 1.9 | 200 | 25 | 1 | unknown | 5.4 | 310 | 42 | 0 | unknown | 5.9 | 310 | 43 | 0 | unknown | 5.9 | 310 | 40 | 0 |
| basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | .32 | 38 | 3.4 | 0 | unknown | .079 | 9.3 | .45 | 0 | error (42) | 850 | 5300 | 6200 | 0 | unknown | .058 | 8.7 | .48 | 0 | error (1) | .42 | 37 | 3.7 | 0 | error (1) | .40 | 38 | 3.7 | 0 | error | 4.1 | 270 | 33 | 0 | unknown | 890 | 1300 | 8600 | 0 | out of memory | 390 | 15000 | 3400 | 0 | timeout | 900 | 500 | 6600 | 0 | timeout | 900 | 540 | 6500 | 0 | unknown | .16 | 28 | 2.1 | 0 | timeout | 880 | 230 | 12000 | 0 | timeout (timeout) | 900 | 1100 | 12000 | 0 | error | 110 | 1700 | 950 | 0 | timeout | 900 | 1800 | 12000 | 0 | error | 150 | 3300 | 1600 | 0 |
| chroot-incomplete_true-no-overflow_true-valid-memsafety.i | error (8) | 1.0 | 110 | 11 | 0 | unknown | .050 | 8.0 | .45 | 0 | error (1) | .58 | 30 | 5.2 | 0 | unknown | .074 | 8.9 | .72 | 0 | error (1) | .43 | 37 | 3.4 | 0 | error (1) | .38 | 37 | 3.9 | 0 | error | 3.7 | 270 | 30 | 0 | unknown | 900 | 870 | 11000 | 0 | out of memory | 900 | 15000 | 6600 | 0 | unknown | 3.9 | 100 | 47 | 0 | unknown | 3.9 | 110 | 51 | 0 | unknown | .23 | 32 | 2.1 | 0 | false(valid-deref) | 530 | 310 | 6400 | -16 | timeout (timeout) | 900 | 1700 | 9200 | 0 | unknown | 5.2 | 310 | 41 | 0 | unknown | 5.4 | 310 | 40 | 0 | unknown | 6.6 | 350 | 51 | 0 |
| cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i | timeout | 900 | 1300 | 11000 | 0 | unknown | .081 | 9.3 | .41 | 0 | error (1) | 6.2 | 110 | 84 | 0 | unknown | .17 | 9.9 | 1.7 | 0 | error (1) | .43 | 40 | 4.1 | 0 | error (1) | .41 | 41 | 4.4 | 0 | error | 3.9 | 270 | 30 | 0 | unknown | 44 | 46 | 470 | 0 | unknown | .36 | 38 | 4.9 | 0 | unknown | .23 | 38 | 1.8 | 0 | unknown | .22 | 38 | 1.9 | 0 | unknown | .21 | 37 | 1.8 | 0 | timeout | 900 | 7.5 | 12000 | 0 | false(valid-deref) | 26 | 3500 | 280 | -16 | unknown | 5.7 | 310 | 44 | 0 | unknown | 6.0 | 320 | 47 | 0 | unknown | 6.1 | 320 | 51 | 0 |
| date_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | 12 | 990 | 150 | 0 | unknown | .079 | 9.2 | .49 | 0 | error (1) | 2.8 | 210 | 34 | 0 | unknown | .16 | 10 | 1.8 | 0 | error (1) | .42 | 40 | 3.8 | 0 | error (1) | .40 | 40 | 4.4 | 0 | error | 4.0 | 270 | 32 | 0 | unknown | 48 | 48 | 660 | 0 | unknown | .39 | 41 | 4.1 | 0 | unknown | .22 | 41 | 2.0 | 0 | unknown | .23 | 40 | 2.2 | 0 | unknown | .21 | 40 | 1.9 | 0 | timeout | 900 | 9.4 | 11000 | 0 | false(valid-deref) | 85 | 6800 | 1200 | -16 | unknown | 5.6 | 310 | 44 | 0 | unknown | 6.7 | 340 | 54 | 0 | unknown | 5.7 | 310 | 48 | 0 |
| dirname_true-no-overflow_true-valid-memsafety.i | error (8) | .28 | 31 | 3.4 | 0 | unknown | .049 | 8.2 | .47 | 0 | error (134) | 350 | 14000 | 4800 | 0 | unknown | .052 | 8.6 | .47 | 0 | error (1) | .44 | 40 | 3.8 | 0 | error (1) | .42 | 38 | 3.7 | 0 | error | 3.1 | 230 | 27 | 0 | unknown | 890 | 970 | 7900 | 0 | out of memory | 110 | 15000 | 1200 | 0 | timeout | 900 | 330 | 11000 | 0 | timeout | 900 | 310 | 7400 | 0 | unknown | .20 | 28 | 2.0 | 0 | true | 880 | 330 | 7500 | 2 | timeout (timeout) | 900 | 2300 | 10000 | 0 | timeout | 900 | 2600 | 7800 | 0 | timeout | 900 | 2900 | 12000 | 0 | timeout | 900 | 870 | 7000 | 0 |
| du_true-no-overflow_true-valid-memsafety.i | error (5) | 8.7 | 66 | 91 | 0 | unknown | .056 | 8.0 | .45 | 0 | error (1) | 20 | 150 | 260 | 0 | unknown | .27 | 46 | 2.5 | 0 | error (1) | .44 | 39 | 3.9 | 0 | error (1) | .43 | 40 | 4.6 | 0 | error | 15 | 270 | 19 | 0 | unknown | 45 | 46 | 650 | 0 | unknown | .40 | 39 | 3.8 | 0 | unknown | .21 | 38 | 2.2 | 0 | unknown | .19 | 38 | 2.2 | 0 | unknown | .22 | 38 | 2.3 | 0 | timeout | 880 | 3400 | 11000 | 0 | false(valid-deref) | 29 | 3400 | 370 | -16 | unknown | 6.6 | 340 | 48 | 0 | unknown | 6.1 | 320 | 44 | 0 | unknown | 6.8 | 340 | 54 | 0 |
| echo_true-no-overflow_true-valid-memsafety.i | error (8) | .96 | 97 | 8.9 | 0 | unknown | .063 | 9.4 | .47 | 0 | error (134) | 53 | 13000 | 650 | 0 | unknown | .073 | 8.8 | .75 | 0 | error (1) | .44 | 39 | 3.8 | 0 | error (1) | .44 | 40 | 3.6 | 0 | error | 3.5 | 270 | 29 | 0 | unknown | 890 | 750 | 9900 | 0 | out of memory | 110 | 15000 | 1200 | 0 | timeout | 900 | 2200 | 10000 | 0 | timeout | 900 | 2200 | 10000 | 0 | unknown | .18 | 32 | 2.1 | 0 | timeout | 880 | 480 | 8700 | 0 | timeout (timeout) | 900 | 1600 | 10000 | 0 | unknown | 6.1 | 330 | 47 | 0 | unknown | 5.9 | 310 | 44 | 0 | unknown | 5.5 | 310 | 39 | 0 |
| expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | 72 | 2500 | 490 | 0 | unknown | .077 | 10 | .49 | 0 | error (1) | 22 | 140 | 240 | 0 | unknown | .21 | 9.7 | 2.6 | 0 | error (1) | .40 | 37 | 3.3 | 0 | error (1) | .40 | 37 | 3.8 | 0 | error | 16 | 270 | 20 | 0 | unknown | 45 | 49 | 540 | 0 | unknown | .37 | 39 | 4.0 | 0 | unknown | .19 | 39 | 2.7 | 0 | unknown | .21 | 39 | 2.0 | 0 | unknown | .22 | 39 | 2.1 | 0 | timeout | 900 | 7.7 | 10000 | 0 | false(valid-deref) | 130 | 6300 | 1500 | -16 | unknown | 5.8 | 310 | 49 | 0 | unknown | 5.8 | 330 | 46 | 0 | unknown | 5.7 | 310 | 48 | 0 |
| fold_true-no-overflow_true-valid-memsafety.i | timeout | 900 | 760 | 11000 | 0 | unknown | .081 | 9.0 | .42 | 0 | error (1) | 4.2 | 66 | 54 | 0 | unknown | .13 | 9.8 | 1.4 | 0 | error (1) | .41 | 38 | 4.2 | 0 | error (1) | .40 | 37 | 3.9 | 0 | error | 3.9 | 280 | 32 | 0 | unknown | 42 | 44 | 510 | 0 | unknown | .35 | 37 | 3.7 | 0 | unknown | .68 | 37 | 1.4 | 0 | unknown | .21 | 36 | 2.3 | 0 | unknown | .24 | 36 | 1.8 | 0 | timeout | 900 | 7.5 | 11000 | 0 | false(valid-deref) | 67 | 2500 | 710 | -16 | unknown | 5.8 | 310 | 47 | 0 | unknown | 6.3 | 330 | 47 | 0 | unknown | 5.4 | 310 | 43 | 0 |
| hostid_true-no-overflow_true-valid-memsafety.i | error (8) | .26 | 34 | 2.2 | 0 | unknown | .060 | 9.1 | .50 | 0 | error (134) | 340 | 14000 | 3800 | 0 | unknown | .053 | 8.7 | .42 | 0 | error (1) | .43 | 38 | 3.7 | 0 | error (1) | .39 | 37 | 3.5 | 0 | error | 3.2 | 260 | 24 | 0 | unknown | 890 | 1100 | 6500 | 0 | out of memory | 67 | 15000 | 620 | 0 | timeout | 900 | 380 | 7500 | 0 | timeout | 900 | 400 | 6900 | 0 | timeout | 900 | 570 | 7700 | 0 | true | 880 | 320 | 7600 | 2 | timeout (timeout) | 900 | 2300 | 9700 | 0 | timeout | 900 | 1300 | 13000 | 0 | timeout | 900 | 1600 | 13000 | 0 | timeout | 900 | 5800 | 11000 | 0 |
| logname_true-no-overflow_true-valid-memsafety.i | error (8) | .43 | 40 | 4.0 | 0 | unknown | .080 | 9.2 | .45 | 0 | error (1) | .32 | 29 | 3.1 | 0 | unknown | .068 | 9.2 | .55 | 0 | error (1) | .43 | 40 | 4.1 | 0 | error (1) | .42 | 37 | 4.1 | 0 | error | 3.7 | 270 | 29 | 0 | unknown | 900 | 920 | 12000 | 0 | out of memory | 830 | 15000 | 7100 | 0 | unknown | 1.6 | 67 | 19 | 0 | unknown | 1.7 | 74 | 20 | 0 | unknown | .18 | 31 | 2.3 | 0 | true | 880 | 330 | 8600 | 2 | false(valid-deref) | 120 | 420 | 1500 | -16 | unknown | 5.4 | 300 | 46 | 0 | unknown | 6.2 | 340 | 46 | 0 | unknown | 5.6 | 320 | 42 | 0 |
| ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (5) | 740 | 330 | 3700 | 0 | unknown | .047 | 8.1 | .54 | 0 | error (1) | 25 | 180 | 260 | 0 | unknown | .67 | 22 | 8.2 | 0 | error (1) | .42 | 40 | 3.8 | 0 | error (1) | .40 | 37 | 3.9 | 0 | error | 4.8 | 280 | 39 | 0 | unknown | 58 | 59 | 630 | 0 | unknown | .49 | 51 | 4.4 | 0 | unknown | .26 | 51 | 2.2 | 0 | unknown | .23 | 51 | 2.7 | 0 | unknown | .24 | 51 | 2.8 | 0 | timeout | 880 | 3600 | 11000 | 0 | timeout (timeout) | 900 | 380 | 9400 | 0 | error | 9.9 | 310 | 78 | 0 | error | 11 | 310 | 75 | 0 | error | 11 | 320 | 76 | 0 |
| mkdir_true-no-overflow_true-valid-memsafety.i | timeout | 900 | 370 | 12000 | 0 | unknown | .048 | 8.0 | .55 | 0 | error (1) | 2.4 | 190 | 32 | 0 | unknown | .12 | 9.7 | 1.3 | 0 | error (1) | .45 | 40 | 3.8 | 0 | error (1) | .41 | 38 | 3.7 | 0 | error | 4.0 | 270 | 33 | 0 | unknown | 43 | 46 | 530 | 0 | unknown | .36 | 38 | 4.3 | 0 | unknown | .18 | 38 | 2.1 | 0 | unknown | .20 | 38 | 2.2 | 0 | unknown | .21 | 38 | 1.9 | 0 | timeout | 900 | 7.4 | 13000 | 0 | false(valid-deref) | 20 | 2400 | 260 | -16 | unknown | 5.9 | 310 | 46 | 0 | unknown | 5.7 | 310 | 43 | 0 | unknown | 6.3 | 330 | 45 | 0 |
| mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i | error (8) | .42 | 45 | 4.0 | 0 | unknown | .079 | 9.4 | .45 | 0 | error (1) | .41 | 30 | 3.6 | 0 | unknown | .064 | 9.2 | .58 | 0 | error (1) | .42 | 37 | 3.4 | 0 | error (1) | .42 | 37 | 3.7 | 0 | error | 3.5 | 260 | 30 | 0 | unknown | 900 | 3000 | 11000 | 0 | timeout | 900 | 15000 | 6000 | 0 | unknown | 670 | 520 | 9400 | 0 | unknown | 670 | 520 | 8900 | 0 | unknown | .20 | 30 | 2.4 | 0 | timeout | 880 | 300 | 11000 | 0 | false(valid-memtrack) | 110 | 340 | 1200 | -16 | unknown | 5.7 | 320 | 41 | 0 | unknown | 5.4 | 310 | 41 | 0 | unknown | 5.6 | 310 | 40 | 0 |
| od_false-unreach-call_true-no-overflow_true-valid-memsafety.i | timeout | 900 | 270 | 3100 | 0 | unknown | .048 | 8.2 | .57 | 0 | error (1) | 16 | 140 | 230 | 0 | unknown | .091 | 10 | .86 | 0 | error (1) | .42 | 40 | 4.3 | 0 | error (1) | .45 | 38 | 4.3 | 0 | error | 4.6 | 280 | 37 | 0 | unknown | 61 | 56 | 760 | 0 | unknown | .51 | 48 | 4.9 | 0 | unknown | .26 | 48 | 3.1 | 0 | unknown | .26 | 48 | 2.5 | 0 | unknown | .28 | 48 | 2.8 | 0 | timeout | 900 | 7.6 | 12000 | 0 | out of memory | 190 | 15000 | 2300 | 0 | unknown | 6.2 | 320 | 43 | 0 | unknown | 6.8 | 330 | 49 | 0 | unknown | 6.8 | 340 | 48 | 0 |
| printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | 58 | 880 | 420 | 0 | unknown | .049 | 8.1 | .46 | 0 | error (1) | 20 | 130 | 230 | 0 | unknown | .076 | 9.9 | .46 | 0 | error (1) | .43 | 40 | 3.8 | 0 | error (1) | .48 | 37 | 3.4 | 0 | error | 3.9 | 270 | 36 | 0 | unknown | 900 | 2600 | 10000 | 0 | timeout | 900 | 760 | 13000 | 0 | timeout | 900 | 4800 | 9100 | 0 | timeout | 900 | 4800 | 9200 | 0 | unknown | .24 | 37 | 2.8 | 0 | timeout | 880 | 550 | 7300 | 0 | unknown | 32 | 3000 | 410 | 0 | unknown | 6.5 | 340 | 49 | 0 | unknown | 5.6 | 320 | 49 | 0 | unknown | 5.8 | 310 | 43 | 0 |
| readlink_true-no-overflow_true-valid-memsafety.i | error (8) | 4.5 | 360 | 50 | 0 | unknown | .061 | 8.1 | .37 | 0 | error (1) | .89 | 43 | 11 | 0 | unknown | .14 | 46 | 1.5 | 0 | error (1) | .47 | 40 | 3.9 | 0 | error (1) | .40 | 40 | 4.2 | 0 | error | 3.8 | 270 | 32 | 0 | unknown | 40 | 43 | 480 | 0 | unknown | .35 | 35 | 3.8 | 0 | unknown | .18 | 35 | 1.9 | 0 | unknown | .18 | 35 | 1.7 | 0 | unknown | .20 | 35 | 1.9 | 0 | true | 880 | 730 | 7900 | 2 | timeout (timeout) | 900 | 2000 | 9500 | 0 | unknown | 6.4 | 350 | 52 | 0 | unknown | 5.5 | 310 | 44 | 0 | unknown | 6.6 | 350 | 52 | 0 |
| realpath_true-no-overflow_true-valid-memsafety.i | error (8) | .49 | 51 | 4.9 | 0 | unknown | .081 | 9.1 | .56 | 0 | error (1) | .41 | 31 | 3.8 | 0 | unknown | .071 | 9.0 | .59 | 0 | error (1) | .46 | 40 | 3.9 | 0 | error (1) | .43 | 40 | 3.7 | 0 | error | 3.6 | 270 | 27 | 0 | unknown | 900 | 3900 | 12000 | 0 | out of memory | 810 | 15000 | 6300 | 0 | unknown | 670 | 780 | 8800 | 0 | unknown | 660 | 780 | 9000 | 0 | unknown | .19 | 31 | 2.3 | 0 | timeout | 880 | 320 | 12000 | 0 | false(valid-memtrack) | 440 | 780 | 3300 | -16 | unknown | 5.3 | 310 | 39 | 0 | unknown | 5.3 | 310 | 45 | 0 | unknown | 6.0 | 330 | 45 | 0 |
| rm_true-no-overflow_true-valid-memsafety.i | error (5) | 8.6 | 64 | 85 | 0 | unknown | .049 | 8.1 | .49 | 0 | error (1) | 33 | 150 | 370 | 0 | unknown | .21 | 11 | 2.2 | 0 | error (1) | .41 | 37 | 3.6 | 0 | error (1) | .42 | 40 | 4.3 | 0 | error | 3.9 | 270 | 35 | 0 | unknown | 43 | 46 | 570 | 0 | unknown | .36 | 38 | 4.6 | 0 | unknown | .20 | 38 | 2.0 | 0 | unknown | .23 | 38 | 1.9 | 0 | unknown | .21 | 38 | 1.8 | 0 | true | 880 | 740 | 7600 | 2 | false(valid-deref) | 470 | 3000 | 5000 | -16 | unknown | 5.9 | 320 | 43 | 0 | unknown | 5.4 | 310 | 45 | 0 | unknown | 5.9 | 310 | 45 | 0 |
| seq_true-no-overflow_true-valid-memsafety.i | error (8) | 3.2 | 260 | 37 | 0 | unknown | .046 | 8.1 | .59 | 0 | error (1) | .84 | 53 | 9.2 | 0 | unknown | .10 | 9.5 | .46 | 0 | error (1) | .43 | 37 | 3.8 | 0 | error (1) | .46 | 40 | 3.6 | 0 | error | 15 | 260 | 17 | 0 | unknown | 39 | 43 | 520 | 0 | unknown | .32 | 35 | 3.3 | 0 | unknown | .20 | 35 | 1.8 | 0 | unknown | .20 | 35 | 2.1 | 0 | unknown | .17 | 35 | 2.2 | 0 | timeout | 900 | 7.4 | 12000 | 0 | unknown | 16 | 1900 | 190 | 0 | error | 9.6 | 340 | 88 | 0 | error | 9.3 | 310 | 72 | 0 | error | 9.9 | 330 | 76 | 0 |
| stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | 200 | 4700 | 1500 | 0 | unknown | .048 | 8.1 | .47 | 0 | error (1) | 40 | 180 | 460 | 0 | unknown | .36 | 47 | 4.3 | 0 | error (1) | .42 | 40 | 3.6 | 0 | error (1) | .42 | 40 | 4.0 | 0 | error | 4.9 | 290 | 42 | 0 | unknown | 900 | 1100 | 2000 | 0 | out of memory | 17 | 15000 | 200 | 0 | timeout | 900 | 4500 | 7700 | 0 | timeout | 900 | 4600 | 7500 | 0 | unknown | .32 | 55 | 3.5 | 0 | timeout | 890 | 540 | 7200 | 0 | timeout (timeout) | 900 | 11000 | 9900 | 0 | unknown | 6.0 | 320 | 47 | 0 | unknown | 6.6 | 330 | 51 | 0 | unknown | 6.1 | 310 | 46 | 0 |
| sync_true-no-overflow_true-valid-memsafety.i | error (8) | .41 | 38 | 4.0 | 0 | unknown | .046 | 8.2 | .59 | 0 | error (1) | .30 | 27 | 2.9 | 0 | unknown | .070 | 8.9 | .55 | 0 | error (1) | .41 | 40 | 3.8 | 0 | error (1) | .43 | 39 | 3.6 | 0 | error | 3.2 | 230 | 27 | 0 | unknown | 890 | 1200 | 6000 | 0 | out of memory | 820 | 15000 | 6800 | 0 | timeout | 900 | 510 | 6200 | 0 | timeout | 900 | 510 | 7100 | 0 | unknown | .17 | 30 | 2.6 | 0 | true | 880 | 340 | 11000 | 2 | false(valid-memtrack) | 160 | 410 | 1600 | -16 | unknown | 5.8 | 320 | 43 | 0 | unknown | 5.8 | 310 | 42 | 0 | unknown | 5.3 | 310 | 41 | 0 |
| tac_true-no-overflow_true-valid-memsafety.i | error (8) | 8.6 | 580 | 100 | 0 | unknown | .051 | 8.2 | .39 | 0 | error (1) | 2.6 | 62 | 32 | 0 | unknown | .13 | 9.5 | 1.3 | 0 | error (1) | .43 | 40 | 4.0 | 0 | error (1) | .39 | 37 | 4.0 | 0 | error | 3.7 | 270 | 28 | 0 | unknown | 40 | 44 | 480 | 0 | unknown | .33 | 36 | 3.9 | 0 | unknown | .65 | 35 | 1.4 | 0 | unknown | .17 | 35 | 1.8 | 0 | unknown | .17 | 35 | 1.9 | 0 | timeout | 880 | 570 | 8900 | 0 | false(valid-memtrack) | 58 | 2000 | 700 | -16 | unknown | 5.4 | 310 | 41 | 0 | unknown | 5.9 | 310 | 43 | 0 | unknown | 6.1 | 330 | 47 | 0 |
| tee_true-no-overflow_true-valid-memsafety.i | error (8) | 5.3 | 470 | 59 | 0 | unknown | .049 | 8.1 | .51 | 0 | error (1) | 1.2 | 51 | 14 | 0 | unknown | .18 | 45 | 1.4 | 0 | error (1) | .45 | 40 | 3.9 | 0 | error (1) | .42 | 38 | 3.9 | 0 | error | 3.8 | 270 | 30 | 0 | unknown | 40 | 43 | 490 | 0 | unknown | .34 | 36 | 4.6 | 0 | unknown | .17 | 35 | 2.0 | 0 | unknown | .17 | 36 | 2.0 | 0 | unknown | .19 | 36 | 2.2 | 0 | timeout | 880 | 3300 | 11000 | 0 | timeout (timeout) | 900 | 2400 | 8700 | 0 | unknown | 5.8 | 310 | 39 | 0 | unknown | 5.6 | 310 | 43 | 0 | unknown | 5.7 | 310 | 40 | 0 |
| test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (5) | 62 | 120 | 430 | 0 | unknown | .080 | 9.1 | .47 | 0 | error (1) | 18 | 150 | 250 | 0 | unknown | 5.6 | 190 | 63 | 0 | error (1) | .44 | 40 | 4.1 | 0 | error (1) | .42 | 38 | 3.7 | 0 | error | 3.9 | 270 | 27 | 0 | unknown | 890 | 1500 | 5700 | 0 | out of memory | 400 | 15000 | 3400 | 0 | timeout | 900 | 740 | 6900 | 0 | timeout | 900 | 760 | 6600 | 0 | unknown | .22 | 38 | 2.6 | 0 | timeout | 880 | 440 | 11000 | 0 | false(valid-memtrack) | 3.4 | 350 | 41 | -16 | unknown | 6.0 | 330 | 44 | 0 | unknown | 6.5 | 340 | 50 | 0 | unknown | 5.6 | 310 | 41 | 0 |
| touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | 10 | 810 | 110 | 0 | unknown | .047 | 8.3 | .47 | 0 | error (1) | 2.7 | 190 | 37 | 0 | unknown | .15 | 9.9 | 1.8 | 0 | error (1) | .40 | 38 | 3.9 | 0 | error (1) | .39 | 37 | 3.6 | 0 | error | 4.2 | 280 | 33 | 0 | unknown | 45 | 47 | 550 | 0 | unknown | .37 | 39 | 4.2 | 0 | unknown | .21 | 39 | 2.5 | 0 | unknown | .22 | 39 | 1.9 | 0 | unknown | .23 | 39 | 1.9 | 0 | timeout | 900 | 7.4 | 12000 | 0 | false(valid-deref) | 38 | 5000 | 460 | -16 | unknown | 6.5 | 330 | 51 | 0 | unknown | 5.8 | 320 | 48 | 0 | unknown | 5.8 | 310 | 41 | 0 |
| uname_true-no-overflow_true-valid-memsafety.i | error (8) | 2.9 | 280 | 32 | 0 | unknown | .069 | 9.3 | .57 | 0 | error (1) | 1.2 | 190 | 14 | 0 | unknown | .10 | 9.2 | 1.2 | 0 | error (1) | .42 | 38 | 4.4 | 0 | error (1) | .45 | 38 | 3.8 | 0 | error | 3.8 | 270 | 33 | 0 | unknown | 40 | 43 | 540 | 0 | unknown | .34 | 35 | 4.2 | 0 | unknown | .19 | 35 | 2.1 | 0 | unknown | .65 | 35 | 2.0 | 0 | unknown | .18 | 35 | 2.1 | 0 | true | 880 | 730 | 9000 | 2 | timeout (timeout) | 900 | 3400 | 8500 | 0 | unknown | 5.4 | 310 | 46 | 0 | unknown | 5.8 | 310 | 41 | 0 | unknown | 5.6 | 310 | 46 | 0 |
| uniq_true-no-overflow_true-valid-memsafety.i | error (8) | 8.3 | 700 | 99 | 0 | unknown | .080 | 8.6 | .47 | 0 | error (1) | 2.0 | 54 | 24 | 0 | unknown | .13 | 9.5 | 1.5 | 0 | error (1) | .42 | 40 | 3.6 | 0 | error (1) | .42 | 37 | 3.9 | 0 | error | 4.0 | 270 | 33 | 0 | unknown | 170 | 44 | 390 | 0 | unknown | .33 | 36 | 4.7 | 0 | unknown | .21 | 36 | 2.1 | 0 | unknown | .19 | 36 | 1.8 | 0 | unknown | .18 | 36 | 2.0 | 0 | timeout | 900 | 7.4 | 13000 | 0 | false(valid-deref) | 24 | 2500 | 280 | -16 | unknown | 6.2 | 330 | 47 | 0 | unknown | 5.8 | 320 | 49 | 0 | unknown | 5.6 | 330 | 44 | 0 |
| usleep_true-no-overflow_true-valid-memsafety.i | error (8) | .77 | 78 | 8.1 | 0 | unknown | .082 | 8.0 | .37 | 0 | error (1) | .35 | 29 | 3.2 | 0 | unknown | .11 | 45 | 1.1 | 0 | error (1) | .44 | 40 | 3.9 | 0 | error (1) | .41 | 37 | 3.8 | 0 | error | 3.4 | 260 | 29 | 0 | unknown | 890 | 1300 | 5400 | 0 | out of memory | 270 | 15000 | 3300 | 0 | timeout | 900 | 600 | 7900 | 0 | timeout | 900 | 610 | 6300 | 0 | unknown | .18 | 31 | 2.3 | 0 | timeout | 880 | 390 | 10000 | 0 | timeout (timeout) | 900 | 1900 | 11000 | 0 | unknown | 5.7 | 300 | 46 | 0 | unknown | 6.0 | 350 | 51 | 0 | unknown | 5.5 | 310 | 45 | 0 |
| uudecode_true-no-overflow_true-valid-memsafety.i | error (8) | 18 | 1500 | 190 | 0 | unknown | .079 | 9.6 | .51 | 0 | error (1) | 5.8 | 110 | 76 | 0 | unknown | .16 | 10 | 1.5 | 0 | error (1) | .45 | 38 | 3.5 | 0 | error (1) | .39 | 38 | 3.6 | 0 | error | 4.0 | 270 | 36 | 0 | unknown | 46 | 50 | 600 | 0 | unknown | .41 | 40 | 3.9 | 0 | unknown | .22 | 40 | 2.0 | 0 | unknown | .23 | 40 | 2.3 | 0 | unknown | .20 | 40 | 1.9 | 0 | timeout | 900 | 7.4 | 13000 | 0 | false(valid-deref) | 50 | 5200 | 550 | -16 | unknown | 5.7 | 320 | 44 | 0 | unknown | 5.8 | 320 | 50 | 0 | unknown | 5.8 | 320 | 44 | 0 |
| wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i | timeout | 900 | 440 | 9400 | 0 | unknown | .048 | 8.1 | .53 | 0 | error (1) | 2.6 | 65 | 31 | 0 | unknown | .12 | 9.3 | 1.2 | 0 | error (1) | .42 | 37 | 3.8 | 0 | error (1) | .40 | 37 | 3.4 | 0 | error | 3.8 | 270 | 32 | 0 | unknown | 41 | 44 | 500 | 0 | unknown | .37 | 36 | 3.7 | 0 | unknown | .18 | 36 | 2.0 | 0 | unknown | .18 | 36 | 2.2 | 0 | unknown | .17 | 36 | 2.3 | 0 | true | 880 | 800 | 8400 | 2 | timeout (timeout) | 900 | 3800 | 8700 | 0 | unknown | 6.3 | 330 | 43 | 0 | unknown | 5.9 | 310 | 45 | 0 | unknown | 5.5 | 310 | 44 | 0 |
| who_true-no-overflow_true-valid-memsafety.i | error (8) | 3.4 | 300 | 39 | 0 | unknown | .049 | 8.1 | .49 | 0 | error (1) | .86 | 41 | 9.4 | 0 | unknown | .11 | 9.3 | 1.1 | 0 | error (1) | .39 | 37 | 4.0 | 0 | error (1) | .42 | 38 | 3.8 | 0 | error | 4.1 | 270 | 33 | 0 | unknown | 40 | 45 | 520 | 0 | unknown | .37 | 36 | 3.5 | 0 | unknown | .19 | 36 | 2.1 | 0 | unknown | .20 | 36 | 2.1 | 0 | unknown | .18 | 36 | 1.8 | 0 | timeout | 880 | 630 | 6400 | 0 | timeout (timeout) | 900 | 2100 | 7200 | 0 | unknown | 6.1 | 320 | 49 | 0 | unknown | 5.4 | 310 | 38 | 0 | unknown | 6.2 | 330 | 50 | 0 |
| whoami-incomplete_true-no-overflow_true-valid-memsafety.i | error (8) | .43 | 39 | 3.8 | 0 | unknown | .084 | 9.1 | .54 | 0 | error (134) | 340 | 14000 | 3900 | 0 | unknown | .071 | 9.4 | .67 | 0 | error (1) | .45 | 40 | 3.9 | 0 | error (1) | .42 | 40 | 4.0 | 0 | error | 3.5 | 270 | 30 | 0 | unknown | 900 | 1200 | 2000 | 0 | out of memory | 900 | 15000 | 7600 | 0 | timeout | 900 | 450 | 6100 | 0 | timeout | 900 | 450 | 8100 | 0 | unknown | .20 | 31 | 2.3 | 0 | true | 880 | 360 | 8000 | 2 | timeout (timeout) | 900 | 2300 | 10000 | 0 | unknown | 5.6 | 320 | 46 | 0 | unknown | 5.4 | 310 | 38 | 0 | unknown | 5.4 | 310 | 48 | 0 |
| yes_true-no-overflow_true-valid-memsafety.i | error (8) | .45 | 46 | 4.5 | 0 | unknown | .068 | 8.2 | .35 | 0 | error (1) | .38 | 33 | 3.0 | 0 | unknown | .063 | 8.8 | .55 | 0 | error (1) | .44 | 40 | 3.9 | 0 | error (1) | .40 | 38 | 4.0 | 0 | error | 3.3 | 260 | 27 | 0 | unknown | 900 | 490 | 2000 | 0 | out of memory | 560 | 15000 | 5600 | 0 | unknown | 2.1 | 81 | 27 | 0 | unknown | 2.2 | 88 | 31 | 0 | unknown | .18 | 31 | 2.0 | 0 | true | 830 | 370 | 8000 | 2 | false(valid-deref) | 110 | 470 | 1300 | -16 | unknown | 6.1 | 330 | 45 | 0 | unknown | 5.5 | 330 | 43 | 0 | unknown | 5.7 | 320 | 39 | 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 | status | cpu (s) | mem (MB) | energy (J) | score |
| total | 38 | 5800 | 20000 | 54000 | 0 | 38 | 2.4 | 330 | 18 | 0 | 38 | 2200 | 63000 | 22000 | 1 | 38 | 10 | 730 | 110 | 0 | 38 | 16 | 1500 | 150 | 0 | 38 | 16 | 1500 | 150 | 0 | 38 | 180 | 10000 | 1100 | 0 | 38 | 18000 | 33000 | 160000 | 0 | 38 | 10000 | 270000 | 94000 | 0 | 38 | 14000 | 27000 | 130000 | 0 | 38 | 14000 | 27000 | 130000 | 0 | 38 | 910 | 1900 | 7800 | 0 | 38 | 32000 | 21000 | 370000 | 6 | 38 | 15000 | 110000 | 160000 | -269 | 38 | 2200 | 17000 | 23000 | 0 | 38 | 3700 | 18000 | 48000 | 0 | 38 | 2200 | 22000 | 22000 | 0 |
| correct results | 0 | 0 | 1 | 9.1 | 690 | 110 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 12 | 9600 | 5600 | 92000 | 22 | 3 | 25 | 1800 | 270 | 3 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| correct true | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 10 | 8800 | 5000 | 83000 | 20 | 0 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| correct false | 0 | 0 | 1 | 9.1 | 690 | 110 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 2 | 840 | 530 | 8500 | 2 | 3 | 25 | 1800 | 270 | 3 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| correct-unconfimed results | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 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 | 0 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| correct-unconfirmed false | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| incorrect results | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 530 | 310 | 6400 | -16 | 17 | 1900 | 45000 | 20000 | -272 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| incorrect true | 0 | 0 | 0 | 0 | 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 | 1 | 530 | 310 | 6400 | -16 | 17 | 1900 | 45000 | 20000 | -272 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| score (38 tasks, max score: 72) | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 6 | -269 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Run set | 2ls.sv-comp17.Systems_BusyBox_MemSafety | blast.sv-comp17 | cbmc.sv-comp17.Systems_BusyBox_MemSafety | ceagle.sv-comp17.Systems_BusyBox_MemSafety | cpa-bam-bnb.sv-comp17.Systems_BusyBox_MemSafety | cpa-kind.sv-comp17.Systems_BusyBox_MemSafety | cpa-seq.sv-comp17.Systems_BusyBox_MemSafety | depthk.sv-comp17.Systems_BusyBox_MemSafety | esbmc.sv-comp17.Systems_BusyBox_MemSafety | esbmc-falsi.sv-comp17.Systems_BusyBox_MemSafety | esbmc-incr.sv-comp17.Systems_BusyBox_MemSafety | esbmc-kind.sv-comp17.Systems_BusyBox_MemSafety | smack.sv-comp17.Systems_BusyBox_MemSafety | symbiotic4.sv-comp17.Systems_BusyBox_MemSafety | uautomizer.sv-comp17.Systems_BusyBox_MemSafety | ukojak.sv-comp17.Systems_BusyBox_MemSafety | utaipan.sv-comp17.Systems_BusyBox_MemSafety | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||