| 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 11:02:28 CET [[ 2017-01-14 22:09:21 CET ]] [[ 2017-01-14 22:27:59 CET ]] [[ 2017-01-14 22:12:16 CET ]] [[ 2017-01-14 22:31:32 CET ]] | 2017-01-11 10:41:01 CET [[ 2017-01-14 21:37:14 CET ]] [[ 2017-01-14 21:52:04 CET ]] | 2017-01-11 13:54:34 CET [[ 2017-01-14 21:55:46 CET ]] [[ 2017-01-14 22:15:53 CET ]] [[ 2017-01-14 21:57:58 CET ]] [[ 2017-01-14 22:18:07 CET ]] | 2017-01-11 10:43:25 CET [[ 2017-01-14 21:26:44 CET ]] [[ 2017-01-14 21:28:35 CET ]] [[ 2017-01-14 21:27:51 CET ]] [[ 2017-01-14 21:29:04 CET ]] | 2017-01-11 10:44:31 CET [[ 2017-01-14 21:49:18 CET ]] [[ 2017-01-14 21:52:02 CET ]] [[ 2017-01-14 21:51:05 CET ]] [[ 2017-01-14 21:53:47 CET ]] | 2017-01-11 11:20:09 CET [[ 2017-01-14 21:49:20 CET ]] [[ 2017-01-14 22:06:43 CET ]] [[ 2017-01-14 21:51:07 CET ]] [[ 2017-01-14 22:08:18 CET ]] | 2017-01-13 07:44:08 CET [[ 2017-01-15 00:24:53 CET ]] [[ 2017-01-15 00:50:42 CET ]] [[ 2017-01-15 00:30:44 CET ]] [[ 2017-01-15 00:56:39 CET ]] | 2017-01-13 09:01:17 CET [[ 2017-01-15 01:00:51 CET ]] [[ 2017-01-15 01:12:27 CET ]] [[ 2017-01-15 01:06:42 CET ]] [[ 2017-01-15 01:18:39 CET ]] | 2017-01-13 08:09:41 CET [[ 2017-01-15 00:46:31 CET ]] [[ 2017-01-15 01:12:25 CET ]] [[ 2017-01-15 00:52:40 CET ]] [[ 2017-01-15 01:18:42 CET ]] | 2017-01-13 08:59:26 CET [[ 2017-01-15 01:13:08 CET ]] [[ 2017-01-15 01:19:20 CET ]] [[ 2017-01-15 01:18:26 CET ]] [[ 2017-01-15 01:22:10 CET ]] | 2017-01-13 09:24:14 CET [[ 2017-01-15 01:24:24 CET ]] [[ 2017-01-15 01:40:44 CET ]] [[ 2017-01-15 01:25:54 CET ]] [[ 2017-01-15 01:44:51 CET ]] | 2017-01-13 09:57:49 CET [[ 2017-01-15 01:31:06 CET ]] [[ 2017-01-15 01:47:27 CET ]] [[ 2017-01-15 01:32:35 CET ]] [[ 2017-01-15 01:49:35 CET ]] | 2017-01-14 07:19:02 CET [[ 2017-01-15 04:32:52 CET ]] [[ 2017-01-15 05:00:11 CET ]] [[ 2017-01-15 04:38:10 CET ]] [[ 2017-01-15 05:08:13 CET ]] | 2017-01-14 13:43:12 CET [[ 2017-01-15 05:08:16 CET ]] [[ 2017-01-15 05:40:54 CET ]] [[ 2017-01-15 05:24:54 CET ]] [[ 2017-01-15 05:42:22 CET ]] | 2017-01-14 07:34:03 CET [[ 2017-01-15 06:02:28 CET ]] [[ 2017-01-15 06:17:25 CET ]] [[ 2017-01-15 06:02:42 CET ]] [[ 2017-01-15 06:18:28 CET ]] | 2017-01-14 07:32:15 CET [[ 2017-01-15 06:03:36 CET ]] [[ 2017-01-15 06:19:08 CET ]] [[ 2017-01-15 06:04:26 CET ]] [[ 2017-01-15 06:20:07 CET ]] | 2017-01-14 16:52:13 CET [[ 2017-01-15 06:05:33 CET ]] [[ 2017-01-15 06:20:29 CET ]] [[ 2017-01-15 06:05:48 CET ]] [[ 2017-01-15 06:21:18 CET ]] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Run set | 2ls.sv-comp17.Systems_BusyBox_Overflows | blast.sv-comp17 | cbmc.sv-comp17.Systems_BusyBox_Overflows | ceagle.sv-comp17.Systems_BusyBox_Overflows | cpa-bam-bnb.sv-comp17.Systems_BusyBox_Overflows | cpa-kind.sv-comp17.Systems_BusyBox_Overflows | cpa-seq.sv-comp17.Systems_BusyBox_Overflows | depthk.sv-comp17.Systems_BusyBox_Overflows | esbmc.sv-comp17.Systems_BusyBox_Overflows | esbmc-falsi.sv-comp17.Systems_BusyBox_Overflows | esbmc-incr.sv-comp17.Systems_BusyBox_Overflows | esbmc-kind.sv-comp17.Systems_BusyBox_Overflows | smack.sv-comp17.Systems_BusyBox_Overflows | symbiotic4.sv-comp17.Systems_BusyBox_Overflows | uautomizer.sv-comp17.Systems_BusyBox_Overflows | ukojak.sv-comp17.Systems_BusyBox_Overflows | utaipan.sv-comp17.Systems_BusyBox_Overflows | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Options | --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_1102.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_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_1102.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_1041.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-11_1041.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_1354.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1354.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_1354.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1354.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_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.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/ceagle.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_1043.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_1044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-11_1044.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_1044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-11_1044.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_1120.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1120.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_1120.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1120.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_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0744.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_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0744.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_0901.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0901.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_0901.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0901.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_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0809.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_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0809.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_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0859.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_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0859.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_0924.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0924.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_0924.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0924.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_0957.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0957.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_0957.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0957.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_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0719.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_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0719.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_1343.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1343.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1343.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1343.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] | [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0734.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_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0734.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_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0732.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_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0732.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_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1652.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_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1652.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) | .27 | 32 | 2.6 | 0 | exception (gremlins) | .073 | 11 | .42 | 0 | error (42) | 850 | 4900 | 7200 | 0 | unknown | .019 | .89 | .026 | 0 | error (1) | .44 | 40 | 4.3 | 0 | error | 5.0 | 280 | 40 | 0 | error | 4.4 | 280 | 37 | 0 | unknown | 890 | 1100 | 7800 | 0 | out of memory | 680 | 15000 | 6200 | 0 | timeout | 900 | 400 | 11000 | 0 | timeout | 900 | 420 | 11000 | 0 | unknown | .16 | 28 | 1.9 | 0 | timeout | 880 | 540 | 7400 | 0 | timeout (timeout) | 900 | 260 | 12000 | 0 | timeout | 900 | 5500 | 12000 | 0 | timeout | 900 | 4600 | 12000 | 0 | timeout | 900 | 2400 | 9500 | 0 |
| basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | .28 | 32 | 2.2 | 0 | exception (gremlins) | .054 | 11 | .47 | 0 | error (42) | 850 | 5000 | 5600 | 0 | unknown | .015 | 1.0 | .032 | 0 | error (1) | .41 | 40 | 4.0 | 0 | error | 4.8 | 280 | 36 | 0 | error | 4.7 | 290 | 37 | 0 | unknown | 890 | 1100 | 6600 | 0 | out of memory | 650 | 15000 | 5300 | 0 | timeout | 900 | 420 | 12000 | 0 | timeout | 900 | 400 | 10000 | 0 | unknown | .16 | 28 | 1.6 | 0 | timeout | 880 | 840 | 8600 | 0 | timeout (timeout) | 900 | 260 | 11000 | 0 | timeout | 900 | 5500 | 12000 | 0 | timeout | 900 | 5100 | 15000 | 0 | timeout | 900 | 2400 | 9500 | 0 |
| chgrp-incomplete_true-no-overflow_false-valid-memtrack.i | error (8) | .33 | 37 | 2.7 | 0 | exception (gremlins) | .061 | 11 | .48 | 0 | error (1) | .35 | 29 | 3.7 | 0 | unknown | .022 | .91 | .044 | 0 | error (1) | .44 | 40 | 3.8 | 0 | error | 5.2 | 280 | 43 | 0 | error | 5.3 | 280 | 45 | 0 | unknown | 900 | 2500 | 5600 | 0 | out of memory | 620 | 15000 | 6100 | 0 | timeout | 900 | 1100 | 8200 | 0 | timeout | 900 | 1200 | 7100 | 0 | unknown | .18 | 31 | 2.3 | 0 | true | 880 | 440 | 9600 | 1 | timeout (timeout) | 900 | 370 | 11000 | 0 | unknown | 6.2 | 330 | 51 | 0 | unknown | 5.9 | 330 | 45 | 0 | unknown | 6.1 | 320 | 48 | 0 |
| chroot-incomplete_true-no-overflow_true-valid-memsafety.i | error (8) | .51 | 72 | 5.0 | 0 | exception (gremlins) | .071 | 11 | .45 | 0 | error (1) | .47 | 31 | 6.0 | 0 | unknown | .016 | .88 | .051 | 0 | error (1) | .40 | 37 | 3.9 | 0 | error | 5.7 | 330 | 46 | 0 | error | 5.2 | 280 | 42 | 0 | unknown | 900 | 930 | 12000 | 0 | out of memory | 820 | 15000 | 5800 | 0 | unknown | 3.4 | 89 | 42 | 0 | unknown | 3.4 | 93 | 40 | 0 | unknown | .19 | 32 | 2.5 | 0 | true | 880 | 480 | 7500 | 1 | timeout (timeout) | 900 | 490 | 12000 | 0 | unknown | 5.4 | 310 | 40 | 0 | unknown | 5.3 | 310 | 46 | 0 | unknown | 5.8 | 320 | 42 | 0 |
| cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i | timeout | 900 | 910 | 12000 | 0 | exception (gremlins) | .077 | 11 | .51 | 0 | error (1) | 4.9 | 96 | 51 | 0 | unknown | .015 | .91 | .069 | 0 | error (1) | .41 | 38 | 4.2 | 0 | error | 7.1 | 450 | 54 | 0 | error | 7.2 | 430 | 56 | 0 | unknown | 48 | 500 | 680 | 0 | unknown | .38 | 38 | 4.0 | 0 | unknown | .23 | 37 | 2.2 | 0 | unknown | .19 | 37 | 2.1 | 0 | unknown | .19 | 38 | 2.0 | 0 | true | 880 | 620 | 7500 | 1 | timeout (timeout) | 900 | 280 | 10000 | 0 | unknown | 5.5 | 310 | 42 | 0 | unknown | 5.6 | 310 | 48 | 0 | unknown | 6.5 | 340 | 49 | 0 |
| date_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | 2.8 | 620 | 30 | 0 | exception (gremlins) | .087 | 15 | .50 | 0 | error (1) | 2.3 | 200 | 26 | 0 | unknown | .018 | .85 | .067 | 0 | error (1) | .43 | 37 | 3.3 | 0 | error | 7.1 | 460 | 57 | 0 | error | 7.5 | 440 | 60 | 0 | unknown | 51 | 500 | 580 | 0 | unknown | .38 | 41 | 4.5 | 0 | unknown | .22 | 40 | 2.3 | 0 | unknown | .22 | 40 | 2.5 | 0 | unknown | .20 | 40 | 2.6 | 0 | timeout | 880 | 800 | 7600 | 0 | false(no-overflow) | 1.3 | 81 | 14 | -16 | unknown | 5.8 | 310 | 46 | 0 | unknown | 6.2 | 330 | 48 | 0 | unknown | 6.2 | 330 | 44 | 0 |
| dirname_true-no-overflow_true-valid-memsafety.i | error (8) | .25 | 31 | 2.1 | 0 | exception (gremlins) | .084 | 13 | .49 | 0 | error (134) | 320 | 14000 | 3900 | 0 | unknown | .016 | 1.0 | .034 | 0 | error (1) | .41 | 37 | 3.5 | 0 | error | 4.7 | 270 | 35 | 0 | error | 4.4 | 280 | 34 | 0 | unknown | 890 | 790 | 7900 | 0 | out of memory | 130 | 15000 | 1300 | 0 | out of memory | 290 | 15000 | 3100 | 0 | timeout | 900 | 310 | 7200 | 0 | unknown | .16 | 28 | 1.8 | 0 | true | 880 | 630 | 10000 | 1 | timeout (timeout) | 900 | 1400 | 11000 | 0 | error (1) | 160 | 1100 | 1500 | 0 | error (1) | 190 | 11000 | 2100 | 0 | error (1) | 400 | 1100 | 3000 | 0 |
| du_true-no-overflow_true-valid-memsafety.i | error (5) | 1.1 | 44 | 12 | 0 | exception (gremlins) | .074 | 11 | .50 | 0 | error (1) | 16 | 140 | 160 | 0 | unknown | .014 | 1.0 | .071 | 0 | error (1) | .39 | 37 | 3.9 | 0 | error | 7.0 | 450 | 56 | 0 | error | 6.6 | 420 | 54 | 0 | unknown | 46 | 500 | 500 | 0 | unknown | .38 | 38 | 4.1 | 0 | unknown | .20 | 39 | 2.5 | 0 | unknown | .21 | 39 | 2.2 | 0 | unknown | .20 | 38 | 1.8 | 0 | timeout | 880 | 3400 | 9500 | 0 | error | 8.1 | 67 | 85 | 0 | unknown | 6.2 | 330 | 46 | 0 | unknown | 5.7 | 320 | 46 | 0 | unknown | 5.8 | 310 | 49 | 0 |
| echo_true-no-overflow_true-valid-memsafety.i | error (8) | .46 | 51 | 3.7 | 0 | exception (gremlins) | .083 | 14 | .47 | 0 | error (42) | 850 | 7300 | 5800 | 0 | unknown | .014 | 1.0 | .071 | 0 | error (1) | .41 | 38 | 4.0 | 0 | error | 5.8 | 290 | 43 | 0 | error | 5.4 | 290 | 48 | 0 | unknown | 890 | 700 | 11000 | 0 | out of memory | 150 | 15000 | 1900 | 0 | timeout | 900 | 2100 | 9900 | 0 | timeout | 900 | 2100 | 11000 | 0 | unknown | .18 | 32 | 2.0 | 0 | timeout | 880 | 570 | 8000 | 0 | timeout (timeout) | 900 | 470 | 10000 | 0 | unknown | 5.4 | 310 | 42 | 0 | unknown | 5.2 | 310 | 36 | 0 | unknown | 5.8 | 310 | 42 | 0 |
| expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | 10 | 1600 | 140 | 0 | exception (gremlins) | .089 | 12 | .46 | 0 | error (1) | 17 | 130 | 200 | 0 | unknown | .021 | 1.0 | .062 | 0 | error (1) | .42 | 37 | 3.8 | 0 | error | 7.9 | 440 | 63 | 0 | error | 7.8 | 440 | 57 | 0 | unknown | 61 | 930 | 710 | 0 | unknown | .39 | 39 | 4.7 | 0 | unknown | .22 | 39 | 2.0 | 0 | unknown | .22 | 39 | 2.0 | 0 | unknown | .23 | 39 | 2.3 | 0 | true | 880 | 550 | 7900 | 1 | timeout (timeout) | 900 | 420 | 10000 | 0 | unknown | 5.8 | 320 | 47 | 0 | unknown | 5.4 | 310 | 47 | 0 | unknown | 5.7 | 310 | 47 | 0 |
| fold_true-no-overflow_true-valid-memsafety.i | timeout | 900 | 470 | 9700 | 0 | exception (gremlins) | .055 | 12 | .45 | 0 | error (1) | 3.2 | 60 | 40 | 0 | unknown | .015 | 1.0 | .081 | 0 | error (1) | .45 | 40 | 4.3 | 0 | error | 7.7 | 460 | 59 | 0 | error | 6.4 | 430 | 54 | 0 | unknown | 46 | 550 | 570 | 0 | unknown | .35 | 37 | 4.3 | 0 | unknown | .19 | 36 | 2.1 | 0 | unknown | .21 | 36 | 2.2 | 0 | unknown | .18 | 36 | 2.5 | 0 | timeout | 880 | 620 | 7100 | 0 | timeout (timeout) | 900 | 360 | 13000 | 0 | unknown | 5.6 | 320 | 43 | 0 | unknown | 5.9 | 320 | 43 | 0 | unknown | 5.8 | 310 | 49 | 0 |
| head_true-no-overflow_false-valid-deref.i | error (8) | 3.6 | 750 | 43 | 0 | exception (gremlins) | .087 | 10 | .45 | 0 | error (1) | 2.8 | 60 | 39 | 0 | unknown | .015 | .77 | .056 | 0 | error (1) | .42 | 40 | 4.5 | 0 | error | 6.0 | 340 | 48 | 0 | error | 6.2 | 350 | 46 | 0 | unknown | 900 | 2400 | 13000 | 0 | out of memory | 700 | 15000 | 5700 | 0 | timeout | 900 | 4600 | 8100 | 0 | timeout | 900 | 4700 | 7300 | 0 | unknown | .23 | 34 | 2.1 | 0 | true | 880 | 400 | 10000 | 1 | timeout (timeout) | 900 | 330 | 12000 | 0 | unknown | 5.3 | 310 | 41 | 0 | unknown | 6.3 | 340 | 49 | 0 | unknown | 5.7 | 320 | 47 | 0 |
| hostid_true-no-overflow_true-valid-memsafety.i | error (8) | .24 | 34 | 1.8 | 0 | exception (gremlins) | .089 | 11 | .51 | 0 | error (134) | 320 | 14000 | 4100 | 0 | unknown | .014 | 1.0 | .048 | 0 | error (1) | .40 | 37 | 3.6 | 0 | error | 4.8 | 280 | 34 | 0 | error | 4.6 | 280 | 39 | 0 | unknown | 900 | 930 | 6400 | 0 | out of memory | 65 | 15000 | 680 | 0 | out of memory | 180 | 15000 | 1700 | 0 | timeout | 900 | 280 | 10000 | 0 | timeout | 900 | 370 | 12000 | 0 | true | 880 | 650 | 12000 | 2 | timeout (timeout) | 900 | 1100 | 13000 | 0 | true | 10 | 380 | 70 | 2 | true | 15 | 500 | 110 | 2 | true | 10 | 380 | 74 | 2 |
| logname_true-no-overflow_true-valid-memsafety.i | error (8) | .33 | 37 | 3.0 | 0 | exception (gremlins) | .051 | 10 | .50 | 0 | error (1) | .30 | 29 | 2.9 | 0 | unknown | .015 | .91 | .065 | 0 | error (1) | .41 | 38 | 3.4 | 0 | error | 5.2 | 280 | 42 | 0 | error | 5.4 | 280 | 44 | 0 | unknown | 900 | 1000 | 11000 | 0 | out of memory | 770 | 15000 | 5400 | 0 | unknown | 1.2 | 55 | 13 | 0 | unknown | 1.3 | 59 | 16 | 0 | unknown | .18 | 31 | 2.2 | 0 | true | 880 | 440 | 10000 | 1 | timeout (timeout) | 900 | 270 | 11000 | 0 | unknown | 6.4 | 330 | 50 | 0 | unknown | 5.4 | 310 | 42 | 0 | unknown | 5.8 | 320 | 43 | 0 |
| ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (5) | 55 | 160 | 340 | 0 | exception (gremlins) | .050 | 13 | .65 | 0 | error (1) | 19 | 150 | 210 | 0 | unknown | .021 | 1.1 | .068 | 0 | error (1) | .40 | 38 | 3.5 | 0 | error | 8.6 | 500 | 80 | 0 | error | 8.9 | 490 | 76 | 0 | unknown | 58 | 59 | 780 | 0 | unknown | .47 | 51 | 4.4 | 0 | unknown | .26 | 51 | 2.2 | 0 | unknown | .24 | 51 | 2.4 | 0 | unknown | .22 | 51 | 2.6 | 0 | timeout | 880 | 3500 | 9600 | 0 | error | 220 | 180 | 2600 | 0 | error (1) | 6.1 | 320 | 53 | 0 | error (1) | 6.0 | 320 | 45 | 0 | error (1) | 5.8 | 310 | 48 | 0 |
| mkdir_true-no-overflow_true-valid-memsafety.i | timeout | 900 | 220 | 12000 | 0 | exception (gremlins) | .085 | 13 | .55 | 0 | error (1) | 1.9 | 180 | 23 | 0 | unknown | .012 | .85 | .057 | 0 | error (1) | .42 | 38 | 3.7 | 0 | error | 6.9 | 470 | 59 | 0 | error | 7.1 | 460 | 54 | 0 | unknown | 47 | 510 | 580 | 0 | unknown | .38 | 38 | 3.8 | 0 | unknown | .21 | 38 | 2.0 | 0 | unknown | .18 | 38 | 2.5 | 0 | unknown | .18 | 38 | 2.5 | 0 | true | 880 | 560 | 7200 | 1 | timeout (timeout) | 900 | 910 | 8200 | 0 | unknown | 6.0 | 310 | 42 | 0 | unknown | 6.0 | 310 | 42 | 0 | unknown | 5.7 | 310 | 43 | 0 |
| mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i | error (8) | .31 | 36 | 3.3 | 0 | exception (gremlins) | .051 | 10 | .58 | 0 | error (1) | .37 | 29 | 3.0 | 0 | unknown | .016 | 1.0 | .052 | 0 | error (1) | .41 | 40 | 3.5 | 0 | error | 5.1 | 280 | 40 | 0 | error | 5.1 | 280 | 40 | 0 | unknown | 900 | 1200 | 11000 | 0 | out of memory | 840 | 15000 | 6600 | 0 | unknown | 550 | 280 | 8100 | 0 | unknown | 540 | 290 | 6000 | 0 | unknown | .21 | 30 | 1.8 | 0 | true | 880 | 440 | 11000 | 1 | timeout (timeout) | 900 | 450 | 11000 | 0 | unknown | 6.0 | 320 | 39 | 0 | unknown | 5.3 | 300 | 41 | 0 | unknown | 6.2 | 340 | 42 | 0 |
| od_false-unreach-call_true-no-overflow_true-valid-memsafety.i | out of memory | 260 | 15000 | 1500 | 0 | exception (gremlins) | .085 | 11 | .47 | 0 | error (1) | 13 | 120 | 130 | 0 | unknown | .013 | 1.0 | .058 | 0 | error (1) | .42 | 37 | 3.6 | 0 | error | 11 | 640 | 86 | 0 | error | 11 | 550 | 92 | 0 | unknown | 63 | 1700 | 900 | 0 | unknown | .48 | 48 | 4.7 | 0 | unknown | .26 | 48 | 3.1 | 0 | unknown | .28 | 48 | 2.6 | 0 | unknown | .28 | 48 | 2.5 | 0 | error (1) | 1.2 | 63 | 17 | 0 | true | 1.5 | 120 | 16 | 1 | unknown | 7.5 | 340 | 48 | 0 | unknown | 6.3 | 310 | 50 | 0 | unknown | 6.2 | 320 | 44 | 0 |
| printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | 6.3 | 890 | 72 | 0 | exception (gremlins) | .081 | 11 | .48 | 0 | error (1) | 15 | 120 | 210 | 0 | unknown | .011 | .88 | .049 | 0 | error (1) | .46 | 40 | 3.7 | 0 | error | 6.8 | 440 | 58 | 0 | error | 7.1 | 430 | 60 | 0 | unknown | 900 | 1900 | 12000 | 0 | timeout | 900 | 770 | 11000 | 0 | timeout | 900 | 3900 | 7700 | 0 | timeout | 900 | 3900 | 9700 | 0 | unknown | .25 | 37 | 2.2 | 0 | error (1) | .66 | 41 | 7.7 | 0 | unknown | .57 | 40 | 7.1 | 0 | unknown | 6.2 | 340 | 46 | 0 | unknown | 6.5 | 330 | 53 | 0 | unknown | 6.9 | 320 | 51 | 0 |
| readlink_true-no-overflow_true-valid-memsafety.i | error (8) | 1.2 | 220 | 17 | 0 | exception (gremlins) | .087 | 11 | .56 | 0 | error (1) | .77 | 40 | 9.9 | 0 | unknown | .011 | .92 | .050 | 0 | error (1) | .40 | 38 | 3.6 | 0 | error | 6.3 | 400 | 55 | 0 | error | 6.4 | 420 | 53 | 0 | unknown | 40 | 43 | 490 | 0 | unknown | .35 | 35 | 3.7 | 0 | unknown | .20 | 35 | 2.0 | 0 | unknown | .18 | 35 | 2.4 | 0 | unknown | .21 | 35 | 2.2 | 0 | true | 880 | 420 | 9400 | 1 | timeout (timeout) | 900 | 1200 | 8200 | 0 | unknown | 6.4 | 330 | 54 | 0 | unknown | 5.8 | 310 | 46 | 0 | unknown | 5.6 | 310 | 45 | 0 |
| realpath_true-no-overflow_true-valid-memsafety.i | error (8) | .36 | 37 | 3.4 | 0 | exception (gremlins) | .085 | 11 | .43 | 0 | error (1) | .34 | 30 | 3.7 | 0 | unknown | .016 | 1.0 | .054 | 0 | error (1) | .39 | 37 | 4.2 | 0 | error | 5.2 | 280 | 43 | 0 | error | 5.2 | 290 | 42 | 0 | unknown | 900 | 1200 | 10000 | 0 | out of memory | 750 | 15000 | 6000 | 0 | unknown | 540 | 300 | 7100 | 0 | unknown | 540 | 310 | 6800 | 0 | unknown | .20 | 31 | 2.5 | 0 | true | 880 | 440 | 7400 | 1 | timeout (timeout) | 900 | 610 | 11000 | 0 | unknown | 5.5 | 310 | 42 | 0 | unknown | 6.3 | 320 | 44 | 0 | unknown | 5.4 | 310 | 42 | 0 |
| rm_true-no-overflow_true-valid-memsafety.i | error (5) | 1.2 | 44 | 10 | 0 | exception (gremlins) | .058 | 10 | .44 | 0 | error (1) | 24 | 130 | 280 | 0 | unknown | .016 | .87 | .054 | 0 | error (1) | .39 | 37 | 3.6 | 0 | error | 6.8 | 450 | 60 | 0 | error | 7.1 | 460 | 52 | 0 | unknown | 45 | 510 | 550 | 0 | unknown | .36 | 38 | 4.9 | 0 | unknown | .20 | 38 | 1.9 | 0 | unknown | .19 | 38 | 1.9 | 0 | unknown | .19 | 38 | 2.0 | 0 | true | 880 | 540 | 6500 | 1 | timeout (timeout) | 900 | 2100 | 9400 | 0 | unknown | 5.5 | 310 | 40 | 0 | unknown | 5.7 | 320 | 40 | 0 | unknown | 5.6 | 310 | 43 | 0 |
| seq_true-no-overflow_true-valid-memsafety.i | error (8) | .93 | 150 | 9.0 | 0 | exception (gremlins) | .056 | 12 | .52 | 0 | error (1) | .73 | 48 | 7.4 | 0 | unknown | .016 | .64 | .056 | 0 | error (1) | .43 | 37 | 4.0 | 0 | error | 6.6 | 410 | 54 | 0 | error | 6.6 | 410 | 51 | 0 | unknown | 42 | 500 | 470 | 0 | unknown | .32 | 35 | 4.4 | 0 | unknown | .20 | 35 | 2.2 | 0 | unknown | .17 | 35 | 1.9 | 0 | unknown | .17 | 35 | 1.9 | 0 | true | 880 | 460 | 7500 | 1 | unknown | .56 | 39 | 6.9 | 0 | error (1) | 6.0 | 310 | 40 | 0 | error (1) | 5.6 | 320 | 43 | 0 | error (1) | 6.0 | 320 | 41 | 0 |
| sleep_true-no-overflow_false-valid-deref.i | error (8) | .70 | 110 | 7.3 | 0 | exception (gremlins) | .089 | 11 | .43 | 0 | error (1) | .89 | 36 | 11 | 0 | unknown | .015 | .99 | .080 | 0 | error (1) | .43 | 38 | 4.0 | 0 | error | 5.9 | 330 | 44 | 0 | error | 5.7 | 290 | 46 | 0 | unknown | 900 | 1000 | 11000 | 0 | out of memory | 870 | 15000 | 8000 | 0 | timeout | 900 | 1100 | 12000 | 0 | timeout | 900 | 1100 | 11000 | 0 | unknown | .23 | 32 | 2.2 | 0 | error (1) | .55 | 31 | 7.0 | 0 | unknown | .42 | 20 | 5.1 | 0 | unknown | 6.1 | 330 | 52 | 0 | unknown | 6.3 | 330 | 46 | 0 | unknown | 5.9 | 320 | 41 | 0 |
| stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | 24 | 3100 | 210 | 0 | exception (gremlins) | .087 | 11 | .44 | 0 | error (1) | 31 | 170 | 300 | 0 | unknown | .013 | .93 | .055 | 0 | error (1) | .43 | 40 | 3.8 | 0 | error | 9.6 | 440 | 84 | 0 | error | 9.9 | 450 | 75 | 0 | unknown | 890 | 2000 | 11000 | 0 | out of memory | 17 | 15000 | 200 | 0 | timeout | 900 | 3900 | 6400 | 0 | timeout | 900 | 3900 | 7000 | 0 | unknown | .33 | 55 | 4.0 | 0 | timeout | 890 | 640 | 6400 | 0 | error | 76 | 110 | 730 | 0 | unknown | 6.2 | 320 | 52 | 0 | unknown | 6.2 | 330 | 50 | 0 | unknown | 6.4 | 320 | 50 | 0 |
| sync_true-no-overflow_true-valid-memsafety.i | error (8) | .30 | 35 | 2.9 | 0 | exception (gremlins) | .085 | 11 | .45 | 0 | error (1) | .30 | 29 | 2.7 | 0 | unknown | .016 | 1.1 | .057 | 0 | error (1) | .41 | 40 | 3.8 | 0 | error | 5.3 | 290 | 41 | 0 | error | 5.0 | 290 | 43 | 0 | unknown | 890 | 1000 | 5900 | 0 | out of memory | 750 | 15000 | 5400 | 0 | timeout | 900 | 310 | 10000 | 0 | timeout | 900 | 260 | 13000 | 0 | unknown | .17 | 30 | 1.9 | 0 | true | 880 | 450 | 8800 | 1 | timeout (timeout) | 900 | 270 | 12000 | 0 | unknown | 5.6 | 310 | 45 | 0 | unknown | 6.2 | 330 | 46 | 0 | unknown | 5.6 | 320 | 40 | 0 |
| tac_true-no-overflow_true-valid-memsafety.i | error (8) | 2.1 | 360 | 24 | 0 | exception (gremlins) | .060 | 11 | .42 | 0 | error (1) | 2.1 | 55 | 27 | 0 | unknown | .017 | 1.0 | .049 | 0 | error (1) | .44 | 40 | 3.9 | 0 | error | 6.7 | 430 | 60 | 0 | error | 6.7 | 390 | 47 | 0 | unknown | 43 | 500 | 490 | 0 | unknown | .32 | 35 | 3.5 | 0 | unknown | .19 | 35 | 1.7 | 0 | unknown | .20 | 35 | 2.0 | 0 | unknown | .18 | 35 | 1.8 | 0 | timeout | 880 | 520 | 8000 | 0 | timeout (timeout) | 900 | 1200 | 12000 | 0 | unknown | 5.6 | 320 | 44 | 0 | unknown | 5.6 | 310 | 47 | 0 | unknown | 6.5 | 350 | 42 | 0 |
| tee_true-no-overflow_true-valid-memsafety.i | error (8) | 1.6 | 310 | 17 | 0 | exception (gremlins) | .051 | 12 | .50 | 0 | error (1) | .98 | 45 | 10 | 0 | unknown | .022 | 1.1 | .052 | 0 | error (1) | .40 | 37 | 3.7 | 0 | error | 6.9 | 340 | 49 | 0 | error | 6.5 | 410 | 54 | 0 | unknown | 43 | 500 | 590 | 0 | unknown | .33 | 36 | 3.5 | 0 | unknown | .17 | 36 | 2.0 | 0 | unknown | .17 | 36 | 1.9 | 0 | unknown | .19 | 36 | 2.4 | 0 | timeout | 880 | 3400 | 11000 | 0 | timeout (timeout) | 900 | 730 | 11000 | 0 | unknown | 6.4 | 330 | 48 | 0 | unknown | 5.8 | 310 | 42 | 0 | unknown | 5.5 | 300 | 47 | 0 |
| test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (5) | 4.2 | 58 | 40 | 0 | exception (gremlins) | .057 | 12 | .42 | 0 | error (1) | 14 | 130 | 170 | 0 | unknown | .014 | .88 | .071 | 0 | error (1) | .42 | 38 | 3.8 | 0 | error | 6.3 | 390 | 56 | 0 | error | 7.0 | 400 | 52 | 0 | unknown | 890 | 1300 | 8200 | 0 | out of memory | 710 | 15000 | 6400 | 0 | timeout | 900 | 510 | 10000 | 0 | timeout | 900 | 450 | 10000 | 0 | unknown | .23 | 37 | 3.0 | 0 | true | 880 | 470 | 7200 | 1 | timeout (timeout) | 900 | 720 | 12000 | 0 | unknown | 5.5 | 300 | 43 | 0 | unknown | 5.6 | 310 | 44 | 0 | unknown | 5.6 | 310 | 43 | 0 |
| touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i | error (8) | 2.4 | 500 | 24 | 0 | exception (gremlins) | .052 | 9.1 | .56 | 0 | error (1) | 2.2 | 180 | 27 | 0 | unknown | .017 | .88 | .061 | 0 | error (1) | .43 | 40 | 3.9 | 0 | error | 7.5 | 420 | 68 | 0 | error | 6.8 | 420 | 58 | 0 | unknown | 47 | 500 | 640 | 0 | unknown | .36 | 39 | 4.2 | 0 | unknown | .19 | 39 | 2.4 | 0 | unknown | .21 | 39 | 1.9 | 0 | unknown | .20 | 39 | 2.2 | 0 | timeout | 880 | 640 | 8100 | 0 | false(no-overflow) | 210 | 420 | 2300 | -16 | unknown | 5.7 | 310 | 46 | 0 | unknown | 6.3 | 340 | 46 | 0 | unknown | 6.3 | 320 | 47 | 0 |
| uname_true-no-overflow_true-valid-memsafety.i | error (8) | .94 | 160 | 9.1 | 0 | exception (gremlins) | .079 | 11 | .51 | 0 | error (1) | 1.1 | 190 | 14 | 0 | unknown | .014 | .86 | .057 | 0 | error (1) | .42 | 38 | 4.6 | 0 | error | 6.8 | 390 | 50 | 0 | error | 6.7 | 400 | 59 | 0 | unknown | 43 | 500 | 500 | 0 | unknown | .33 | 36 | 3.3 | 0 | unknown | .17 | 35 | 1.8 | 0 | unknown | .21 | 35 | 1.8 | 0 | unknown | .17 | 35 | 1.9 | 0 | true | 880 | 490 | 6200 | 1 | timeout (timeout) | 900 | 5100 | 7000 | 0 | unknown | 5.9 | 310 | 49 | 0 | unknown | 5.7 | 310 | 51 | 0 | unknown | 6.6 | 330 | 50 | 0 |
| uniq_true-no-overflow_true-valid-memsafety.i | error (8) | 2.2 | 450 | 25 | 0 | exception (gremlins) | .081 | 11 | .53 | 0 | error (1) | 1.6 | 46 | 19 | 0 | unknown | .012 | .86 | .055 | 0 | error (1) | .43 | 40 | 4.0 | 0 | error | 6.8 | 440 | 54 | 0 | error | 7.0 | 430 | 53 | 0 | unknown | 44 | 510 | 600 | 0 | unknown | .33 | 37 | 4.7 | 0 | unknown | .17 | 36 | 1.9 | 0 | unknown | .20 | 36 | 2.1 | 0 | unknown | .18 | 36 | 1.8 | 0 | true | 880 | 550 | 11000 | 1 | timeout (timeout) | 900 | 310 | 9800 | 0 | unknown | 6.2 | 330 | 46 | 0 | unknown | 5.6 | 320 | 48 | 0 | unknown | 5.9 | 320 | 48 | 0 |
| usleep_true-no-overflow_true-valid-memsafety.i | error (8) | .43 | 51 | 3.5 | 0 | exception (gremlins) | .083 | 12 | .51 | 0 | error (1) | .32 | 29 | 2.8 | 0 | unknown | .016 | .95 | .055 | 0 | error (1) | .42 | 38 | 3.9 | 0 | error | 5.2 | 290 | 41 | 0 | error | 5.2 | 280 | 47 | 0 | unknown | 890 | 1200 | 6200 | 0 | out of memory | 300 | 15000 | 3600 | 0 | timeout | 900 | 300 | 10000 | 0 | timeout | 900 | 290 | 9900 | 0 | unknown | .20 | 31 | 2.0 | 0 | true | 880 | 1200 | 10000 | 1 | timeout (timeout) | 900 | 220 | 10000 | 0 | unknown | 6.1 | 350 | 45 | 0 | unknown | 5.4 | 310 | 36 | 0 | unknown | 5.2 | 300 | 41 | 0 |
| uudecode_true-no-overflow_true-valid-memsafety.i | error (8) | 4.5 | 980 | 46 | 0 | exception (gremlins) | .080 | 12 | .44 | 0 | error (1) | 4.6 | 100 | 47 | 0 | unknown | .014 | .79 | .062 | 0 | error (1) | .40 | 38 | 3.9 | 0 | error | 7.2 | 460 | 55 | 0 | error | 8.0 | 430 | 55 | 0 | unknown | 51 | 500 | 700 | 0 | unknown | .39 | 40 | 3.6 | 0 | unknown | .23 | 40 | 2.1 | 0 | unknown | .20 | 40 | 2.1 | 0 | unknown | .21 | 40 | 2.6 | 0 | timeout | 880 | 1200 | 8000 | 0 | timeout (timeout) | 900 | 620 | 11000 | 0 | unknown | 5.6 | 310 | 45 | 0 | unknown | 5.7 | 310 | 49 | 0 | unknown | 5.7 | 310 | 48 | 0 |
| wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i | timeout | 900 | 270 | 11000 | 0 | exception (gremlins) | .078 | 9.7 | .53 | 0 | error (1) | 2.0 | 58 | 24 | 0 | unknown | .015 | .89 | .050 | 0 | error (1) | .42 | 40 | 4.3 | 0 | error | 6.4 | 450 | 46 | 0 | error | 7.1 | 420 | 54 | 0 | unknown | 44 | 500 | 550 | 0 | unknown | .36 | 36 | 3.2 | 0 | unknown | .19 | 36 | 2.0 | 0 | unknown | .20 | 36 | 1.9 | 0 | unknown | .21 | 36 | 2.1 | 0 | true | 880 | 500 | 7400 | 1 | timeout (timeout) | 900 | 2600 | 11000 | 0 | unknown | 5.4 | 310 | 43 | 0 | unknown | 6.0 | 320 | 51 | 0 | unknown | 5.8 | 300 | 45 | 0 |
| who_true-no-overflow_true-valid-memsafety.i | error (8) | 1.0 | 170 | 12 | 0 | exception (gremlins) | .090 | 12 | .47 | 0 | error (1) | .72 | 42 | 7.8 | 0 | unknown | .015 | .80 | .065 | 0 | error (1) | .41 | 38 | 3.7 | 0 | error | 6.5 | 420 | 54 | 0 | error | 6.0 | 390 | 50 | 0 | unknown | 40 | 44 | 550 | 0 | unknown | .36 | 36 | 3.7 | 0 | unknown | .20 | 36 | 1.9 | 0 | unknown | .17 | 36 | 2.2 | 0 | unknown | .17 | 36 | 2.0 | 0 | timeout | 880 | 540 | 6200 | 0 | timeout (timeout) | 900 | 5100 | 7300 | 0 | unknown | 6.7 | 350 | 49 | 0 | unknown | 5.5 | 320 | 43 | 0 | unknown | 5.8 | 310 | 44 | 0 |
| whoami-incomplete_true-no-overflow_true-valid-memsafety.i | error (8) | .33 | 37 | 3.1 | 0 | exception (gremlins) | .087 | 11 | .46 | 0 | error (134) | 310 | 14000 | 4200 | 0 | unknown | .023 | .93 | .058 | 0 | error (1) | .41 | 37 | 3.8 | 0 | error | 5.2 | 280 | 44 | 0 | error | 5.2 | 280 | 43 | 0 | unknown | 890 | 1100 | 5700 | 0 | out of memory | 850 | 15000 | 6900 | 0 | timeout | 900 | 5100 | 12000 | 0 | timeout | 900 | 360 | 8500 | 0 | unknown | .18 | 31 | 2.6 | 0 | true | 880 | 660 | 12000 | 1 | timeout (timeout) | 900 | 1300 | 11000 | 0 | unknown | 6.1 | 330 | 44 | 0 | unknown | 5.8 | 320 | 47 | 0 | unknown | 5.7 | 320 | 43 | 0 |
| yes_true-no-overflow_true-valid-memsafety.i | error (8) | .32 | 37 | 3.8 | 0 | exception (gremlins) | .086 | 11 | .45 | 0 | error (1) | .34 | 32 | 3.1 | 0 | unknown | .012 | .87 | .045 | 0 | error (1) | .44 | 38 | 3.8 | 0 | error | 5.4 | 330 | 44 | 0 | error | 5.3 | 280 | 39 | 0 | unknown | 900 | 1200 | 11000 | 0 | out of memory | 890 | 15000 | 8200 | 0 | unknown | 1.7 | 66 | 24 | 0 | unknown | 1.8 | 71 | 21 | 0 | unknown | .17 | 31 | 2.4 | 0 | true | 880 | 520 | 8600 | 1 | timeout (timeout) | 900 | 300 | 10000 | 0 | unknown | 5.1 | 310 | 37 | 0 | unknown | 5.3 | 310 | 43 | 0 | unknown | 5.7 | 330 | 43 | 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 | 4000 | 28000 | 48000 | 0 | 38 | 2.8 | 430 | 18 | 0 | 38 | 3700 | 61000 | 33000 | 0 | 38 | .59 | 35 | 2.1 | 0 | 38 | 16 | 1500 | 150 | 0 | 38 | 250 | 14000 | 2000 | 0 | 38 | 240 | 14000 | 2000 | 0 | 38 | 18000 | 34000 | 180000 | 0 | 38 | 11000 | 270000 | 100000 | 0 | 38 | 12000 | 55000 | 140000 | 0 | 38 | 14000 | 21000 | 150000 | 0 | 38 | 910 | 1700 | 12000 | 0 | 38 | 31000 | 29000 | 300000 | 23 | 38 | 27000 | 31000 | 320000 | -31 | 38 | 2200 | 23000 | 27000 | 2 | 38 | 2200 | 32000 | 31000 | 2 | 38 | 2400 | 17000 | 24000 | 2 |
| correct results | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 880 | 650 | 12000 | 2 | 0 | 1 | 10 | 380 | 70 | 2 | 1 | 15 | 500 | 110 | 2 | 1 | 10 | 380 | 74 | 2 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| correct true | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 880 | 650 | 12000 | 2 | 0 | 1 | 10 | 380 | 70 | 2 | 1 | 15 | 500 | 110 | 2 | 1 | 10 | 380 | 74 | 2 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| correct false | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| correct-unconfimed results | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 21 | 19000 | 11000 | 180000 | 21 | 1 | 1.5 | 120 | 16 | 1 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| correct-unconfirmed true | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 21 | 19000 | 11000 | 180000 | 21 | 1 | 1.5 | 120 | 16 | 1 | 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 | 0 | 2 | 210 | 500 | 2300 | -32 | 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 | 0 | 2 | 210 | 500 | 2300 | -32 | 0 | 0 | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| score (38 tasks, max score: 76) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 23 | -31 | 2 | 2 | 2 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Run set | 2ls.sv-comp17.Systems_BusyBox_Overflows | blast.sv-comp17 | cbmc.sv-comp17.Systems_BusyBox_Overflows | ceagle.sv-comp17.Systems_BusyBox_Overflows | cpa-bam-bnb.sv-comp17.Systems_BusyBox_Overflows | cpa-kind.sv-comp17.Systems_BusyBox_Overflows | cpa-seq.sv-comp17.Systems_BusyBox_Overflows | depthk.sv-comp17.Systems_BusyBox_Overflows | esbmc.sv-comp17.Systems_BusyBox_Overflows | esbmc-falsi.sv-comp17.Systems_BusyBox_Overflows | esbmc-incr.sv-comp17.Systems_BusyBox_Overflows | esbmc-kind.sv-comp17.Systems_BusyBox_Overflows | smack.sv-comp17.Systems_BusyBox_Overflows | symbiotic4.sv-comp17.Systems_BusyBox_Overflows | uautomizer.sv-comp17.Systems_BusyBox_Overflows | ukojak.sv-comp17.Systems_BusyBox_Overflows | utaipan.sv-comp17.Systems_BusyBox_Overflows | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||