Tool 2LS 0.5.0 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 Forester Predator-HP 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: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-13 11:23:04 CET [[ 2017-01-15 01:40:02 CET ]] [[ 2017-01-15 01:58:53 CET ]] [[ 2017-01-15 01:41:42 CET ]] [[ 2017-01-15 02:00:15 CET ]] 2017-01-13 12:06:28 CET [[ 2017-01-15 02:02:31 CET ]] [[ 2017-01-15 02:04:15 CET ]] [[ 2017-01-15 02:04:05 CET ]] [[ 2017-01-15 02:06:30 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.MemSafety-LinkedLists cbmc.sv-comp17.MemSafety-LinkedLists ceagle.sv-comp17.MemSafety-LinkedLists cpa-bam-bnb.sv-comp17.MemSafety-LinkedLists cpa-kind.sv-comp17.MemSafety-LinkedLists cpa-seq.sv-comp17.MemSafety-LinkedLists depthk.sv-comp17.MemSafety-LinkedLists esbmc.sv-comp17.MemSafety-LinkedLists esbmc-falsi.sv-comp17.MemSafety-LinkedLists esbmc-incr.sv-comp17.MemSafety-LinkedLists esbmc-kind.sv-comp17.MemSafety-LinkedLists forester.sv-comp17.MemSafety-LinkedLists predatorhp.sv-comp17.MemSafety-LinkedLists smack.sv-comp17.MemSafety-LinkedLists symbiotic4.sv-comp17.MemSafety-LinkedLists uautomizer.sv-comp17.MemSafety-LinkedLists ukojak.sv-comp17.MemSafety-LinkedLists utaipan.sv-comp17.MemSafety-LinkedLists
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 ]] --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 ]] --trace error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/forester.2017-01-13_1123.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/forester.2017-01-13_1123.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/forester.2017-01-13_1123.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/forester.2017-01-13_1123.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/predatorhp.2017-01-13_1206.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/ 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 status cpu (s) mem (MB) energy (J) score
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (134) .47 46 5.0 0 error (1) .30 21 2.4 0 unknown .046 8.2 .37 0 error (1) .41 39 4.2 0 error (1) .43 40 3.8 0 error 11   220 15 0 unknown 890    1100 12000   0 out of memory 490 15000 5900 0 timeout 900    1900 10000   0 timeout 900    1400 9600   0 unknown 3.4  150 44   0 unknown .083 12 .52 0 true 1.5  50 16   2 timeout 880   570 7200 0 timeout (timeout) 900    3100 10000   0 timeout 900   960 12000 0 timeout 900   1300 13000 0 timeout 900   5000 11000 0
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (5) .37 27 3.1 0 error (42) 850    3300 9100   0 unknown .038 8.2 .41 0 error (1) .42 38 4.4 0 error (1) .41 37 3.8 0 error (recursion) 2.7 220 25 0 unknown 890    360 7800   0 out of memory 740 15000 4200 0 timeout 900    830 11000   0 timeout 900    630 9000   0 unknown 2.8  72 34   0 unknown .054 11 .56 0 true 2.5  59 27   2 timeout 880   320 7800 0 timeout (timeout) 900    3900 9500   0 timeout 900   2300 11000 0 timeout 900   2100 9900 0 timeout 900   770 12000 0
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i true 25    1000 260   2 error (134) 400    13000 3700   0 unknown .057 32   .53 0 error (1) .42 37 3.4 0 error (1) .42 41 3.7 0 timeout 910   4400 1500 0 unknown 890    850 12000   0 out of memory 320 15000 3300 0 timeout 900    1100 12000   0 timeout 900    700 11000   0 unknown .34 34 4.0 0 unknown .061 11 .50 0 true 1.6  69 20   2 timeout 880   510 7700 0 timeout (timeout) 900    2100 7400   0 timeout 900   990 12000 0 timeout 900   1200 13000 0 timeout 900   1500 12000 0
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i false(valid-deref) .31 31 3.3 -16 error (42) 850    4300 4500   0 unknown .044 8.1 .30 0 error (1) .44 40 3.9 0 error (1) .39 38 3.7 0 timeout 930   7800 9300 0 unknown 890    310 11000   0 timeout 900 4600 2200 0 timeout 900    430 12000   0 timeout 900    490 9700   0 unknown .55 35 7.0 0 unknown 1.3   49 18    0 true 2.2  72 23   2 timeout 880   250 11000 0 true .44 34 4.8 2 timeout 910   13000 3500 0 timeout 900   1900 12000 0 timeout 900   8500 8900 0
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) .57 46 4.9 1 false(valid-deref) .47 36 4.5 1 unknown .042 7.9 .22 0 error (1) .42 37 4.0 0 error (1) .42 40 4.3 0 false(valid-deref) 3.6 260 32 1 false(valid-deref) 1.4  30 16   1 out of memory 110 15000 1200 0 false(valid-deref) .31 25 3.4 1 false(valid-deref) .26 26 3.4 1 false(valid-deref) .27 26 3.4 1 unknown .053 11 .57 0 false(valid-deref) 2.1  25 24   1 false(valid-deref) 5.1 100 58 1 false(valid-deref) .41 28 5.3 1 false(valid-deref) 290   610 4100 1 false(valid-deref) 570   1800 8000 1 timeout 900   13000 5400 0
heap-manipulation/tree_false-valid-deref.i false(valid-deref) .29 30 2.4 1 false(valid-deref) .44 37 4.9 1 unknown .042 8.0 .24 0 error (1) .43 40 3.9 0 error (1) .41 40 3.9 0 false(valid-deref) 3.1 250 28 1 false(valid-deref) .39 29 4.4 1 out of memory 110 15000 1500 0 false(valid-deref) .15 25 1.1 1 false(valid-deref) .12 25 1.2 1 false(valid-deref) .11 25 1.5 1 false(valid-deref) .094 18 .71 1 false(valid-deref) .15 25 2.1 1 false(valid-deref) 2.2 91 23 1 false(valid-deref) .36 29 4.0 1 false(valid-deref) 6.6 360 53 1 false(valid-deref) 7.7 340 56 1 false(valid-deref) 6.7 360 50 1
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (5) .20 26 1.4 0 false(valid-memtrack) .30 26 2.5 1 unknown .087 44   .51 0 error (1) .46 40 3.9 0 error (1) .40 37 3.8 0 false(valid-memtrack) 3.4 260 27 1 false(valid-memtrack) 4.7  29 13   1 out of memory 300 15000 3500 0 false(valid-memtrack) .18 25 1.8 1 false(valid-memtrack) .20 25 1.7 1 false(valid-memtrack) .19 25 2.1 1 false(valid-memtrack) .078 14 .92 1 false(valid-memtrack) .14 25 2.0 1 false(valid-memtrack) 750   220 8900 1 false(valid-memtrack) .34 17 4.1 1 timeout 900   1000 10000 0 timeout 900   1300 12000 0 timeout 900   1500 10000 0
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) .51 37 5.1 1 false(valid-memtrack) .40 33 4.5 1 unknown .038 8.2 .22 0 error (1) .38 37 3.9 0 error (1) .40 37 3.2 0 timeout 900   7300 9000 0 false(valid-memtrack) 1.7  38 20   1 out of memory 91 15000 1200 0 false(valid-memtrack) 1.8  32 4.0 1 false(valid-memtrack) .48 33 5.5 1 false(valid-memtrack) .50 33 5.4 1 unknown .43  19 5.2  0 false(valid-memtrack) .17 23 1.9 1 false(valid-memtrack) 830   280 6900 1 false(valid-memtrack) .36 27 4.5 1 error 8.4 320 65 0 error 8.5 310 66 0 error 8.6 300 60 0
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (134) .45 31 4.2 0 false(valid-memtrack) .29 27 2.9 1 unknown .069 44   .50 0 error (1) .44 37 3.6 0 error (1) .44 40 4.2 0 false(valid-memtrack) 13   260 16 1 false(valid-memtrack) 5.6  33 20   1 out of memory 500 15000 5900 0 false(valid-memtrack) .32 30 3.2 1 false(valid-memtrack) .30 30 3.7 1 false(valid-memtrack) .30 30 3.7 1 false(valid-memtrack) 1.6   45 33    1 false(valid-memtrack) .17 23 2.6 1 false(valid-memtrack) 830   350 7300 1 false(valid-memtrack) .37 25 4.6 1 unknown 200   1000 2300 0 timeout 900   1700 11000 0 timeout 910   14000 4400 0
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (134) .41 30 3.9 0 false(valid-memtrack) .27 25 2.5 1 unknown .064 43   .52 0 error (1) .42 37 4.0 0 error (1) .41 37 3.2 0 false(valid-memtrack) 3.3 260 25 1 false(valid-memtrack) 1.3  29 16   1 out of memory 760 15000 8200 0 false(valid-memtrack) .25 26 2.9 1 false(valid-memtrack) .28 27 2.9 1 false(valid-memtrack) .28 27 3.5 1 false(valid-memtrack) .70  24 8.3  1 false(valid-memtrack) .16 23 1.8 1 false(valid-memtrack) 830   330 7200 1 false(valid-memtrack) .34 22 3.5 1 unknown 170   1000 2200 0 timeout 900   1700 11000 0 timeout 900   7600 6100 0
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (134) .41 30 4.1 0 error (42) 850    4400 4900   0 unknown .036 8.1 .18 0 error (1) .45 40 3.8 0 error (1) .42 37 3.5 0 timeout 940   9400 9200 0 unknown 890    190 9200   0 timeout 900 3900 7100 0 timeout 900    1400 9700   0 timeout 900    1400 9200   0 unknown .12 24 1.4 0 true .19  16 2.4  2 timeout 900    2000 7100   0 true 880   320 9900 2 timeout (timeout) 900    2100 9700   0 timeout 900   1100 11000 0 timeout 900   2100 14000 0 timeout 900   6400 7300 0
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .21 26 1.8 1 false(valid-memtrack) .24 20 1.8 1 unknown .090 44   .50 0 error (1) .44 40 3.9 0 error (1) .40 37 3.9 0 timeout 900   7500 6800 0 false(valid-memtrack) .47 29 5.2 1 out of memory 240 15000 2600 0 false(valid-memtrack) .16 24 1.3 1 false(valid-memtrack) .12 24 1.3 1 false(valid-memtrack) .12 24 1.7 1 unknown .051 11 .47 0 false(valid-memtrack) .13 24 1.9 1 false(valid-memtrack) 750   320 5400 1 false(valid-memtrack) .30 17 4.2 1 unknown 13   330 100 0 unknown 30   640 290 0 unknown 13   350 97 0
list-properties/list_search_true-unreach-call_false-valid-memtrack.i true .38 32 3.6 -32 false(valid-memtrack) .65 24 5.0 1 unknown .028 8.3 .33 0 error (1) .42 40 3.9 0 error (1) .40 37 3.4 0 error 2.6 220 25 0 false(valid-memtrack) 44    480 350   1 false(valid-memtrack) 39 1100 480 1 false(valid-memtrack) .28 25 3.3 1 false(valid-memtrack) .34 30 3.8 1 false(valid-memtrack) .41 36 6.1 1 false(valid-memtrack) .22  19 2.4  1 false(valid-memtrack) .15 25 2.2 1 false(valid-memtrack) 14   110 210 1 false(valid-memtrack) .33 18 3.6 1 timeout 900   1000 10000 0 timeout 900   1000 11000 0 timeout 900   4400 8800 0
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .21 27 1.9 1 false(valid-memtrack) .28 26 2.6 1 unknown .039 8.0 .22 0 error (1) .42 40 4.1 0 error (1) .42 38 4.3 0 timeout 900   7300 9000 0 false(valid-memtrack) .46 29 4.9 1 out of memory 450 15000 5000 0 false(valid-memtrack) .13 24 1.4 1 false(valid-memtrack) .12 24 1.4 1 false(valid-memtrack) .12 24 1.4 1 timeout 2.6   38 830    0 false(valid-memtrack) .13 23 1.9 1 false(valid-memtrack) 750   290 6500 1 false(valid-memtrack) .32 19 3.6 1 unknown 20   480 170 0 unknown 46   710 470 0 unknown 21   510 170 0
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .29 27 2.8 1 false(valid-memtrack) .22 19 1.6 1 unknown .036 8.1 .21 0 error (1) .42 38 4.0 0 error (1) .42 37 4.0 0 timeout 900   8100 5800 0 false(valid-memtrack) 1.0  29 13   1 out of memory 170 15000 1700 0 false(valid-memtrack) .16 24 1.3 1 false(valid-memtrack) .13 24 1.5 1 false(valid-memtrack) .16 24 1.3 1 false(valid-memtrack) .071 11 .57 1 false(valid-memtrack) .13 23 1.9 1 false(valid-memtrack) 750   310 7800 1 false(valid-memtrack) .27 13 3.2 1 unknown 15   390 100 0 unknown 24   500 250 0 unknown 15   400 110 0
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (134) .23 28 2.9 0 false(valid-memtrack) .23 22 1.5 1 unknown .042 8.0 .21 0 error (1) .43 40 3.8 0 error (1) .43 38 3.7 0 timeout 900   7700 9000 0 false(valid-memtrack) 1.0  29 12   1 out of memory 530 15000 5300 0 false(valid-memtrack) .13 24 1.5 1 false(valid-memtrack) .16 24 1.6 1 false(valid-memtrack) .16 24 1.4 1 false(valid-memtrack) .082 11 .54 1 false(valid-memtrack) .14 23 1.7 1 false(valid-memtrack) 750   270 6300 1 false(valid-memtrack) .29 16 3.3 1 unknown 19   470 180 0 unknown 42   710 530 0 unknown 20   470 160 0
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .21 27 1.9 1 false(valid-memtrack) .26 25 2.0 1 unknown .037 8.2 .22 0 error (1) .42 37 4.2 0 error (1) .40 37 4.1 0 false(valid-memtrack) 3.5 270 33 1 false(valid-memtrack) .47 29 5.1 1 out of memory 530 15000 6100 0 false(valid-memtrack) .12 25 1.4 1 false(valid-memtrack) .12 25 1.4 1 false(valid-memtrack) .13 24 1.4 1 timeout 6.5   84 900    0 false(valid-memtrack) .13 24 1.8 1 false(valid-memtrack) 750   340 6800 1 false(valid-memtrack) .31 20 3.5 1 unknown 14   350 110 0 unknown 20   500 170 0 unknown 14   360 110 0
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(valid-deref) 65    1000 550   -16 true 49    930 580   2 unknown .048 9.9 .41 0 error (1) .43 37 4.0 0 error (1) .42 38 3.6 0 false(valid-memtrack) 7.3 420 56 -16 unknown 890    1100 10000   0 out of memory 120 15000 1300 0 false(valid-memtrack) 230    840 2200   -16 timeout 900    620 11000   0 unknown .38 69 4.1 0 unknown .12  18 1.5  0 true .58 52 5.5 2 true 88   250 1100 2 true 2.1  150 25   2 true 180   1600 1200 2 true 410   5000 5400 2 true 320   1600 1500 2
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(valid-deref) 67    960 450   -16 true 43    910 480   2 unknown .062 10   .34 0 error (1) .44 40 4.0 0 error (1) .41 38 3.7 0 false(valid-memtrack) 6.9 420 50 -16 unknown 890    990 9900   0 out of memory 120 15000 1500 0 false(valid-memtrack) 590    850 6900   -16 false(valid-memtrack) 620    860 6900   -16 unknown .33 68 3.6 0 unknown .12  17 1.3  0 true .55 51 4.8 2 true 87   250 1100 2 true 2.2  160 29   2 true 170   1500 1100 2 true 410   5400 5300 2 true 290   1600 1500 2
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(valid-memtrack) 63    980 480   -16 true 48    920 530   2 unknown .091 45   .88 0 error (1) .43 37 3.4 0 error (1) .42 40 4.1 0 false(valid-memtrack) 6.8 410 54 -16 unknown 890    940 11000   0 out of memory 120 15000 1400 0 false(valid-memtrack) 300    630 3400   -16 timeout 900    1000 10000   0 unknown .34 69 4.0 0 unknown .12  17 1.4  0 true .53 52 4.6 2 true 89   250 1100 2 true 2.1  150 25   2 true 170   1700 1400 2 true 410   5300 6200 2 true 290   1600 1700 2
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) 62    950 490   -16 false(valid-memtrack) 38    1100 430   1 unknown .048 10   .46 0 error (1) .41 37 4.0 0 error (1) .42 38 3.8 0 false(valid-memtrack) 6.8 410 52 1 unknown 890    990 9500   0 out of memory 120 15000 1400 0 false(valid-memtrack) 800    1100 8500   1 false(valid-memtrack) 460    890 5400   1 unknown .33 67 3.7 0 unknown .12  18 1.5  0 false(valid-memtrack) .49 52 4.6 1 false(valid-deref) 680   360 7200 -16 false(valid-memtrack) 2.3  160 24   1 unknown 630   5500 4800 0 timeout 900   7000 11000 0 unknown 480   1600 4300 0
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-deref) 63    960 500   -16 false(valid-memtrack) 39    1100 470   1 unknown .10  34   .58 0 error (1) .44 39 3.8 0 error (1) .42 40 3.5 0 false(valid-memtrack) 6.6 420 57 1 unknown 890    970 11000   0 out of memory 490 15000 1000 0 timeout 900    460 1900   0 timeout 900    630 12000   0 unknown .34 67 3.8 0 unknown .15  18 1.4  0 false(valid-memtrack) .51 53 4.4 1 false(valid-deref) 670   360 7900 -16 false(valid-memtrack) 2.2  160 27   1 unknown 630   4900 5000 0 timeout 900   5800 12000 0 unknown 480   1700 3200 0
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) 62    950 530   -16 false(valid-memtrack) 38    1100 510   1 unknown .046 10   .41 0 error (1) .43 38 3.8 0 error (1) .41 40 4.3 0 false(valid-memtrack) 6.7 420 53 1 unknown 890    970 10000   0 out of memory 120 15000 1400 0 timeout 900    920 13000   0 timeout 900    910 9800   0 unknown .34 67 4.1 0 unknown .15  26 1.3  0 false(valid-memtrack) .52 52 5.2 1 false(valid-deref) 680   360 8100 -16 false(valid-memtrack) 2.3  160 27   1 unknown 630   5500 4800 0 timeout 900   6400 9600 0 unknown 470   1900 2900 0
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-deref) 62    950 530   -16 false(valid-memtrack) 39    1100 460   1 unknown .048 9.6 .35 0 error (1) .46 40 3.9 0 error (1) .41 40 3.8 0 false(valid-memtrack) 6.6 410 54 1 unknown 890    1000 10000   0 out of memory 120 15000 1400 0 timeout 900    800 9600   0 timeout 900    830 12000   0 unknown .32 67 3.7 0 unknown .12  18 1.6  0 false(valid-memtrack) .58 51 4.6 1 false(valid-deref) 680   360 7600 -16 false(valid-memtrack) 2.3  160 26   1 unknown 620   5700 5600 0 error 530   6900 6800 0 unknown 480   1600 3300 0
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) 62    950 450   -16 false(valid-memtrack) 39    1100 450   1 unknown .075 10   .33 0 error (1) .41 37 3.3 0 error (1) .41 38 3.5 0 false(valid-memtrack) 6.9 420 53 1 unknown 890    1000 9400   0 out of memory 120 15000 1400 0 timeout 900    760 13000   0 false(valid-memtrack) 410    810 4900   1 unknown .34 67 3.4 0 unknown .12  17 1.7  0 false(valid-memtrack) .50 53 4.8 1 false(valid-deref) 690   360 7700 -16 timeout (timeout) 900    2100 8100   0 unknown 630   5500 4800 0 error 480   6700 6400 0 unknown 480   1600 3800 0
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) 61    950 510   -16 false(valid-memtrack) 39    1100 440   1 unknown .045 9.9 .53 0 error (1) .42 40 3.7 0 error (1) .39 37 4.1 0 false(valid-memtrack) 28   310 29 1 unknown 890    1200 9800   0 out of memory 120 15000 1400 0 false(valid-memtrack) 660    820 8900   1 false(valid-memtrack) 640    820 6800   1 unknown .32 67 3.7 0 unknown .17  17 1.3  0 false(valid-memtrack) .51 52 4.8 1 false(valid-deref) 650   360 9000 -16 false(valid-memtrack) 2.2  160 28   1 unknown 610   5600 4900 0 timeout 900   6000 11000 0 unknown 470   1600 3800 0
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) 61    940 490   -16 false(valid-memtrack) 39    1100 470   1 unknown .047 9.9 .35 0 error (1) .44 40 3.9 0 error (1) .42 37 3.6 0 false(valid-memtrack) 7.4 420 56 1 unknown 890    1100 9500   0 out of memory 120 15000 1500 0 timeout 900    1000 11000   0 false(valid-memtrack) 690    960 8000   1 unknown .32 67 3.6 0 unknown .12  17 1.4  0 false(valid-memtrack) .50 53 4.5 1 false(valid-deref) 670   360 6900 -16 false(valid-memtrack) 2.2  160 26   1 unknown 640   5500 4800 0 error 560   7100 7500 0 unknown 470   1700 3200 0
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-deref) 63    950 450   -16 false(valid-memtrack) 39    1100 510   1 unknown .082 46   1.1  0 error (1) .42 38 3.8 0 error (1) .40 37 3.4 0 false(valid-memtrack) 6.9 420 55 1 unknown 890    1100 9900   0 out of memory 120 15000 1700 0 timeout 900    870 9900   0 timeout 900    1000 10000   0 unknown .32 67 3.6 0 unknown .15  17 1.3  0 false(valid-memtrack) .49 52 5.1 1 false(valid-deref) 640   360 9400 -16 false(valid-memtrack) 2.2  160 26   1 unknown 620   5600 4600 0 timeout 900   6100 10000 0 unknown 470   1700 3000 0
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) 62    950 420   -16 false(valid-memtrack) 39    1100 460   1 unknown .043 9.9 .38 0 error (1) .42 37 4.0 0 error (1) .43 41 4.2 0 false(valid-memtrack) 7.5 420 54 1 unknown 900    1000 10000   0 out of memory 120 15000 1400 0 timeout 900    760 12000   0 timeout 900    770 10000   0 unknown .32 67 3.5 0 unknown .14  26 1.6  0 false(valid-memtrack) .50 53 4.9 1 false(valid-deref) 680   350 7900 -16 false(valid-memtrack) 2.2  160 26   1 unknown 620   5500 4900 0 error 550   6800 7000 0 unknown 470   1500 3600 0
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-deref) 68    950 500   -16 false(valid-memtrack) 39    1100 420   1 unknown .057 10   .40 0 error (1) .41 39 3.8 0 error (1) .42 40 3.7 0 false(valid-memtrack) 7.1 410 50 1 unknown 900    1100 3100   0 out of memory 120 15000 1400 0 timeout 900    1100 10000   0 false(valid-memtrack) 620    890 6400   1 unknown .35 67 3.4 0 unknown .12  18 1.6  0 false(valid-memtrack) .58 52 5.4 1 false(valid-deref) 660   350 7300 -16 false(valid-memtrack) 2.2  160 30   1 unknown 620   5600 5600 0 timeout 900   6100 11000 0 unknown 470   1600 3500 0
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (134) 1.2  68 12   0 error (42) 850    3900 7900   0 unknown .034 8.1 .33 0 error (1) .45 40 3.8 0 error (1) .39 38 4.1 0 timeout 900   7700 11000 0 unknown 890    220 9600   0 timeout 900 8100 5900 0 timeout 900    600 10000   0 timeout 900    450 9600   0 unknown .49 35 5.9 0 true .54  29 6.4  2 true 2.2  32 23   2 timeout 880   300 6500 0 timeout (timeout) 900    3000 6600   0 timeout 900   820 12000 0 timeout 900   1300 11000 0 timeout 910   11000 7200 0
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 900    1800 5900   0 out of memory 340    15000 3900   0 unknown .097 43   .45 0 error (1) .44 40 4.1 0 error (1) .42 40 4.0 0 timeout 900   7300 8800 0 unknown 890    230 2800   0 out of memory 480 15000 870 0 timeout 900    11000 11000   0 timeout 900    4600 9200   0 unknown .16 27 2.0 0 true 30     120 410    2 true 2.3  38 21   2 true 880   270 6700 2 timeout (timeout) 900    3200 13000   0 timeout 900   700 11000 0 timeout 900   1700 12000 0 timeout 900   700 12000 0
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (134) .58 47 5.4 0 error (1) 98    400 1100   0 unknown .048 8.1 .23 0 error (1) .43 40 3.9 0 error (1) .41 40 3.8 0 timeout 900   6800 11000 0 unknown 890    260 8900   0 timeout 900 12000 6600 0 timeout 900    630 11000   0 timeout 900    420 7700   0 unknown .31 32 4.1 0 true 1.3   41 15    2 timeout 900    900 8600   0 timeout 880   290 6700 0 timeout (timeout) 900    3200 7200   0 timeout 900   820 11000 0 timeout 900   1400 12000 0 timeout 900   2400 9500 0
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 900    8700 9200   0 error (42) 850    2300 4200   0 unknown .037 8.1 .24 0 error (1) .44 40 4.0 0 error (1) .41 40 4.0 0 timeout 900   8200 7900 0 unknown 890    200 9100   0 timeout 900 5900 8000 0 timeout 900    1400 11000   0 timeout 900    1600 9100   0 unknown .13 25 1.5 0 true 10     78 120    2 true 2.1  25 22   2 true 880   330 9300 2 timeout (timeout) 900    2800 10000   0 timeout 900   1500 12000 0 timeout 900   1600 12000 0 timeout 900   8900 7900 0
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (134) .70 48 7.6 0 error (42) 850    3100 5300   0 unknown .036 7.9 .26 0 error (1) .40 38 3.9 0 error (1) .42 37 3.9 0 timeout 900   8000 11000 0 unknown 890    330 9300   0 out of memory 83 15000 980 0 timeout 900    460 9500   0 timeout 900    500 11000   0 unknown .34 36 3.8 0 true 1.4   37 18    2 timeout 900    4200 7500   0 timeout 880   340 10000 0 timeout (timeout) 900    2900 6800   0 timeout 900   880 12000 0 timeout 900   1500 14000 0 timeout 910   12000 5500 0
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 900    7800 6100   0 error (42) 850    3300 6100   0 unknown .062 8.0 .22 0 error (1) .45 40 4.1 0 error (1) .43 40 3.9 0 timeout 920   7500 9700 0 unknown 890    270 9000   0 out of memory 91 15000 1100 0 timeout 900    440 9800   0 timeout 900    510 9100   0 unknown .46 39 5.3 0 true 1.3   45 19    2 timeout 900    3500 6300   0 timeout 880   320 6900 0 timeout (timeout) 900    3000 8500   0 error 9.1 320 65 0 error 8.3 300 85 0 error 8.2 310 66 0
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 900    8900 9300   0 error (42) 850    5400 6000   0 unknown .045 8.1 .26 0 error (1) .42 40 3.6 0 error (1) .39 38 3.2 0 timeout 900   4200 2300 0 unknown 890    170 11000   0 out of memory 190 15000 2100 0 timeout 900    410 9800   0 timeout 900    530 5400   0 unknown .27 32 3.6 0 true 230     710 3100    2 true 2.2  32 23   2 true 880   350 7900 2 timeout (timeout) 900    3300 10000   0 timeout 900   960 11000 0 timeout 900   1700 12000 0 timeout 900   12000 5200 0
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (134) .79 40 8.5 0 error (42) 850    1000 5500   0 unknown .099 44   .68 0 error (1) .43 40 4.0 0 error (1) .45 40 4.2 0 timeout 970   11000 4900 0 unknown 890    150 10000   0 out of memory 110 15000 990 0 timeout 900    440 10000   0 timeout 900    850 12000   0 unknown .15 25 2.0 0 true 120     440 1600    2 true 2.2  38 22   2 timeout 880   330 8200 0 timeout (timeout) 900    3300 7500   0 timeout 900   780 11000 0 timeout 900   1600 12000 0 timeout 900   1600 12000 0
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (134) .36 30 3.7 0 error (42) 850    890 11000   0 unknown .037 8.2 .21 0 error (1) .42 37 3.3 0 error (1) .41 37 3.6 0 timeout 900   7500 9000 0 unknown 890    190 12000   0 timeout 900 10000 7000 0 timeout 900    1100 9500   0 timeout 900    1300 12000   0 unknown .19 29 2.3 0 true .16  23 1.5  2 true 1.8  31 20   2 true 880   340 7200 2 timeout (timeout) 900    2100 9800   0 timeout 900   900 14000 0 timeout 900   1600 11000 0 timeout 910   14000 4500 0
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (134) 1.2  66 14   0 error (42) 850    720 11000   0 unknown .046 7.9 .28 0 error (1) .40 37 4.1 0 error (1) .43 37 3.4 0 timeout 950   8300 8800 0 unknown 890    240 8100   0 timeout 900 5500 2100 0 timeout 900    770 10000   0 timeout 900    420 7700   0 unknown .31 29 4.5 0 true .86  38 10    2 timeout 900    280 10000   0 timeout 880   280 11000 0 timeout (timeout) 900    3100 8200   0 timeout 900   820 11000 0 timeout 900   1700 12000 0 timeout 900   2200 8600 0
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (134) .63 49 6.4 0 error (42) 850    880 6400   0 unknown .035 8.0 .24 0 error (1) .40 37 3.4 0 error (1) .43 37 3.8 0 timeout 900   7500 10000 0 unknown 890    340 8700   0 out of memory 320 15000 760 0 timeout 900    250 13000   0 timeout 900    560 8800   0 unknown .25 28 3.5 0 true 670     1600 10000    2 true 2.3  39 24   2 timeout 880   310 7700 0 timeout (timeout) 900    2600 6800   0 timeout 900   940 14000 0 timeout 900   2400 12000 0 timeout 910   13000 3500 0
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 900    1800 5900   0 out of memory 320    15000 3900   0 unknown .033 7.9 .22 0 error (1) .46 40 4.0 0 error (1) .39 37 3.5 0 timeout 900   8000 10000 0 unknown 890    540 10000   0 out of memory 140 15000 1500 0 timeout 900    9200 5500   0 timeout 900    5100 10000   0 unknown .15 25 1.7 0 true 2.8   53 34    2 true 2.3  38 25   2 true 880   250 10000 2 timeout (timeout) 900    3000 9300   0 timeout 900   940 11000 0 timeout 900   1900 11000 0 timeout 900   1100 13000 0
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (134) .56 38 5.9 0 error (1) 94    390 930   0 unknown .036 7.9 .25 0 error (1) .46 40 3.9 0 error (1) .39 37 3.6 0 timeout 900   6900 9600 0 unknown 890    230 7500   0 timeout 900 11000 6300 0 timeout 900    640 8300   0 timeout 900    430 7700   0 unknown .36 30 4.2 0 true .96  35 13    2 timeout 900    720 8100   0 timeout 880   260 7700 0 timeout (timeout) 900    3400 7800   0 timeout 900   970 10000 0 timeout 900   1700 14000 0 timeout 900   2000 11000 0
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 900    9000 7100   0 error (42) 850    1800 3600   0 unknown .099 43   .47 0 error (1) .43 40 3.8 0 error (1) .42 38 3.6 0 timeout 900   8800 7200 0 unknown 890    190 9200   0 timeout 900 4300 5800 0 timeout 900    1500 8600   0 timeout 900    1700 10000   0 unknown .16 25 1.3 0 true 17     91 230    2 true 2.1  26 23   2 true 880   320 12000 2 timeout (timeout) 900    2800 11000   0 timeout 900   1400 12000 0 timeout 900   1700 14000 0 timeout 900   1100 7000 0
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (134) .41 33 5.0 0 error (42) 850    2100 5600   0 unknown .034 8.0 .24 0 error (1) .44 37 4.1 0 error (1) .40 37 4.1 0 timeout 930   8600 9200 0 unknown 890    410 9800   0 out of memory 340 15000 4400 0 timeout 900    400 11000   0 timeout 900    590 11000   0 unknown .22 28 2.4 0 true 6.0   59 83    2 timeout 900    3300 5800   0 timeout 880   310 11000 0 timeout (timeout) 900    3100 6500   0 timeout 900   1100 12000 0 timeout 900   1300 15000 0 timeout 900   2000 8100 0
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 900    7600 7700   0 error (42) 850    2300 5100   0 unknown .093 44   .64 0 error (1) .42 39 3.7 0 error (1) .40 37 3.7 0 timeout 900   8300 11000 0 unknown 890    360 10000   0 out of memory 880 15000 11000 0 timeout 900    400 13000   0 timeout 900    540 11000   0 unknown .22 29 2.8 0 true .53  22 6.1  2 timeout 900    3300 5600   0 timeout 880   310 7200 0 timeout (timeout) 900    3100 6600   0 error 8.7 330 64 0 error 9.1 340 72 0 error 8.0 310 61 0
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 900    8700 8700   0 error (42) 850    2400 5800   0 unknown .034 7.9 .26 0 error (1) .44 40 4.0 0 error (1) .40 37 3.3 0 timeout 900   4300 1700 0 unknown 890    170 9800   0 out of memory 130 15000 1300 0 timeout 900    580 9700   0 timeout 900    950 9900   0 unknown .24 28 3.0 0 true 4.3   66 55    2 true 2.2  30 23   2 true 880   330 8000 2 timeout (timeout) 900    3400 11000   0 timeout 900   920 11000 0 timeout 900   1700 13000 0 timeout 900   4700 6000 0
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (134) .62 40 7.3 0 error (42) 850    870 7800   0 unknown .031 8.2 .26 0 error (1) .45 40 3.9 0 error (1) .41 37 4.0 0 timeout 960   11000 4600 0 unknown 900    190 13000   0 out of memory 88 15000 1000 0 timeout 900    780 11000   0 timeout 900    1400 11000   0 unknown .15 25 1.9 0 true 190     350 2400    2 true 2.2  37 22   2 timeout 880   340 7800 0 timeout (timeout) 900    3300 6900   0 timeout 900   1100 11000 0 timeout 900   1400 11000 0 timeout 900   2100 8700 0
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (134) .33 30 3.3 0 error (42) 850    910 10000   0 unknown .045 7.9 .24 0 error (1) .41 40 4.1 0 error (1) .44 40 3.8 0 timeout 900   8000 8000 0 unknown 890    200 9000   0 timeout 900 5400 2500 0 timeout 900    1500 9800   0 timeout 900    1600 8100   0 unknown .18 26 1.7 0 true .10  14 1.1  2 true 2.1  32 20   2 true 880   300 7300 2 timeout (timeout) 900    2300 10000   0 timeout 900   1300 13000 0 timeout 900   1200 14000 0 timeout 900   8100 6000 0
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i error (134) .53 37 5.0 0 false(valid-deref) .37 31 3.6 1 unknown .035 7.9 .22 0 error (1) .45 40 3.8 0 error (1) .42 38 3.5 0 false(valid-deref) 3.7 270 27 1 false(valid-deref) 1.5  36 19   1 out of memory 93 15000 1100 0 false(valid-deref) .37 30 4.1 1 false(valid-deref) .39 31 4.7 1 false(valid-deref) .38 31 4.1 1 unknown .079 11 .52 0 false(valid-deref) .18 23 2.3 1 false(valid-deref) 3.6 100 41 1 false(valid-deref) .33 22 4.3 1 false(valid-deref) 48   750 460 1 timeout 900   3400 13000 0 timeout 900   8300 9800 0
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) .28 28 3.1 1 false(valid-deref) .25 23 2.9 1 unknown .047 8.0 .25 0 error (1) .45 40 3.9 0 error (1) .40 38 3.9 0 false(valid-deref) 3.6 260 32 1 false(valid-deref) 2.3  29 5.5 1 timeout 900 6400 8100 0 false(valid-deref) .15 25 2.7 1 false(valid-deref) .16 25 1.8 1 false(valid-deref) .17 25 1.9 1 false(valid-deref) .071 20 .96 1 false(valid-deref) .16 25 2.0 1 false(valid-deref) 4.1 110 48 1 false(valid-deref) .39 28 4.7 1 false(valid-deref) 140   610 1700 1 false(valid-deref) 260   1500 3500 1 false(valid-deref) 130   650 1600 1
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i error (134) .50 34 5.0 0 false(valid-deref) .29 26 2.7 1 unknown .099 44   .45 0 error (1) .44 40 3.7 0 error (1) .42 37 3.8 0 false(valid-deref) 3.5 270 27 1 false(valid-deref) 1.4  30 16   1 out of memory 330 15000 3900 0 false(valid-deref) .28 25 3.3 1 false(valid-deref) .30 26 3.5 1 false(valid-deref) .31 26 2.9 1 unknown .053 11 .64 0 false(valid-deref) .17 23 2.3 1 false(valid-deref) 3.3 92 38 1 false(valid-deref) .31 20 3.7 1 false(valid-deref) 37   840 360 1 false(valid-deref) 260   1400 4200 1 timeout 910   11000 6700 0
../../sv-benchmarks/c/ 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 status cpu (s) mem (MB) energy (J) score
total 52 8100    69000 67000   -246 52 17000 100000 140000 31 52 2.8 880 19 0 52 22 2000 200 0 52 21 2000 200 0 52 25000 220000 220000 -29 52 33000 22000 350000 15 52 21000 680000 170000 1 52 31000 50000 350000 -31 52 31000 40000 340000 4 52 20   2200 240 15 52 1300   4600 20000 48 52 7300   20000 60000 63 52 35000 15000 350000 -121 52 22000   73000 210000 32 52 29000 110000 330000 11 52 34000 130000 460000 10 52 32000 210000 280000 8
    correct results 9 27    1300 290   10 28 530 14000 6300 31 0 0 0 19 130 6400 760 19 15 68 910 520 15 1 39 1100 480 1 17 1500 2300 17000 17 20 2800 4800 31000 20 15 3.6 400 42 15 28 1300   4000 18000 48 44 45   1700 470 63 27 15000 6900 150000 39 28 32   2200 380 32 8 1000 8000 10000 11 7 2300 21000 33000 10 5 1000 5800 6500 8
        correct true 1 25    1000 260   2 3 140 2800 1600 6 0 0 0 0 0 0 0 0 0 20 1300   3900 18000 40 19 35   800 370 38 12 8200 3600 81000 24 4 6.9 480 83 8 3 520 4800 3600 6 3 1200 16000 17000 6 3 890 4800 4800 6
        correct false 8 2.6  250 24   8 25 390 11000 4700 25 0 0 0 19 130 6400 760 19 15 68 910 520 15 1 39 1100 480 1 17 1500 2300 17000 17 20 2800 4800 31000 20 15 3.6 400 42 15 8 3.0 160 47 8 25 9.4 880 100 25 15 7100 3300 64000 15 24 25   1700 300 24 5 520 3200 6700 5 4 1100 5100 16000 4 2 140 1000 1700 2
    correct-unconfimed results 0 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 0
        correct-unconfirmed false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
    incorrect results 15 820    12000 6300   -256 0 0 0 0 3 21 1200 160 -48 0 0 3 1100 2300 13000 -48 1 620 860 6900 -16 0 0 0 10 6700 3600 79000 -160 0 0 0 0
        incorrect true 1 .38 32 3.6 -32 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 14 820    12000 6300   -224 0 0 0 0 3 21 1200 160 -48 0 0 3 1100 2300 13000 -48 1 620 860 6900 -16 0 0 0 10 6700 3600 79000 -160 0 0 0 0
score (52 tasks, max score: 79) -246 31 0 0 0 -29 15 1 -31 4 15 48 63 -121 32 11 10 8
Run set 2ls.sv-comp17.MemSafety-LinkedLists cbmc.sv-comp17.MemSafety-LinkedLists ceagle.sv-comp17.MemSafety-LinkedLists cpa-bam-bnb.sv-comp17.MemSafety-LinkedLists cpa-kind.sv-comp17.MemSafety-LinkedLists cpa-seq.sv-comp17.MemSafety-LinkedLists depthk.sv-comp17.MemSafety-LinkedLists esbmc.sv-comp17.MemSafety-LinkedLists esbmc-falsi.sv-comp17.MemSafety-LinkedLists esbmc-incr.sv-comp17.MemSafety-LinkedLists esbmc-kind.sv-comp17.MemSafety-LinkedLists forester.sv-comp17.MemSafety-LinkedLists predatorhp.sv-comp17.MemSafety-LinkedLists smack.sv-comp17.MemSafety-LinkedLists symbiotic4.sv-comp17.MemSafety-LinkedLists uautomizer.sv-comp17.MemSafety-LinkedLists ukojak.sv-comp17.MemSafety-LinkedLists utaipan.sv-comp17.MemSafety-LinkedLists