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 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 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-Other cbmc.sv-comp17.MemSafety-Other ceagle.sv-comp17.MemSafety-Other cpa-bam-bnb.sv-comp17.MemSafety-Other cpa-kind.sv-comp17.MemSafety-Other cpa-seq.sv-comp17.MemSafety-Other depthk.sv-comp17.MemSafety-Other esbmc.sv-comp17.MemSafety-Other esbmc-falsi.sv-comp17.MemSafety-Other esbmc-incr.sv-comp17.MemSafety-Other esbmc-kind.sv-comp17.MemSafety-Other predatorhp.sv-comp17.MemSafety-Other smack.sv-comp17.MemSafety-Other symbiotic4.sv-comp17.MemSafety-Other uautomizer.sv-comp17.MemSafety-Other ukojak.sv-comp17.MemSafety-Other utaipan.sv-comp17.MemSafety-Other
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 ]] --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
loop-acceleration/array3_false-valid-deref.i timeout 900    10000 11000    0 false(valid-deref) 23    930 290   1 unknown .040 7.8 .14 0 error (1) .40 38 3.3 0 error (1) .42 40 3.6 0 timeout 900   3500 14000 0 unknown 53 28 690 0 true .61 80 7.3 -32 false(valid-deref) 300   690 4100 1 false(valid-deref) 320    2300 4000   1 unknown .075 23 .81 0 timeout 900    89 11000   0 timeout 790   1200 6600 0 false(valid-deref) 9.7  29 110   1 timeout 900   1700 13000 0 timeout 900   3200 15000 0 timeout 900   1600 12000 0
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 48    1900 640    1 false(valid-deref) 3.5  200 34   1 unknown .31  12   3.9  0 error (1) .42 37 3.8 0 error (1) .41 38 4.1 0 false(valid-deref) 7.2 330 56 1 false(valid-deref) 130 790 1000 1 timeout 900    250 12000   0 false(valid-deref) 5.1 410 60 1 false(valid-deref) 19    410 43   1 timeout 900     230 11000    0 false(valid-deref) 1.2  84 9.9 1 false(valid-deref) 48   250 570 1 unknown 21    2100 200   0 unknown 5.9 330 43 0 unknown 7.0 340 56 0 unknown 7.3 340 48 0
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 2.0  88 21    1 error (1) .68 35 7.7 0 unknown .20  46   1.4  0 error (1) .44 40 3.8 0 error (1) .42 38 3.8 0 false(valid-deref) 4.4 270 33 1 false(valid-deref) 750 1100 6400 1 false(valid-deref) 17    1000 190   1 false(valid-deref) 340   520 3600 1 false(valid-deref) 320    530 3900   1 false(valid-deref) 320     530 3400    1 false(valid-deref) .36 40 3.1 1 false(valid-deref) 4.5 120 49 1 false(valid-deref) 1.0  19 13   1 unknown 6.2 330 48 0 unknown 5.3 300 41 0 unknown 5.3 310 46 0
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.3  410 12    2 true 1.1  38 11   2 unknown .13  9.4 1.5  0 error (1) .43 39 3.8 0 error (1) .39 37 3.5 0 true 76   3900 780 2 true 79 4000 780 2 true .89 50 10   2 timeout 900   5900 10000 0 true .78 45 9.2 2 true .79  45 9.5  2 true 2.8  86 29   2 true 330   260 4300 2 true 7.3  580 84   2 true 8.1 450 63 2 true 16   650 130 2 true 8.0 460 66 2
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.3  410 14    2 true 1.1  38 12   2 unknown .13  8.7 1.5  0 error (1) .44 40 4.0 0 error (1) .41 40 3.8 0 true 68   4000 770 2 true 74 4000 810 2 true .89 50 11   2 timeout 900   5900 12000 0 true .74 45 8.6 2 true .77  45 8.9  2 true 2.8  86 27   2 true 320   260 4200 2 true 7.4  580 100   2 true 9.2 460 63 2 true 17   620 140 2 true 8.7 460 64 2
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .46 100 4.4  2 error (42) 850    7400 3700   0 unknown .080 8.5 .74 0 error (1) .39 37 4.0 0 error (1) .44 40 3.7 0 timeout 900   4700 11000 0 timeout 900 4800 12000 0 true 1.0  120 12   2 timeout 900   1200 8100 0 out of memory 410    15000 5300   0 true .75  37 10    2 true 62    550 670   2 true 160   180 2300 2 timeout (timeout) 900    1800 9200   0 true 7.3 350 61 2 true 15   750 120 2 true 7.1 360 52 2
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .37 69 2.9  2 true .37 20 4.0 2 unknown .067 8.3 .67 0 error (1) .39 37 4.2 0 error (1) .43 40 4.2 0 true 65   4000 620 2 true 270 4000 380 2 true .39 36 4.7 2 timeout 900   4200 9800 0 true .29 28 3.7 2 true .26  28 3.2  2 true 6.8  120 69   2 true 130   180 1600 2 true 2.0  150 26   2 true 7.4 350 58 2 true 9.8 480 77 2 true 7.1 350 57 2
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .35 67 3.3  2 true .36 21 3.8 2 unknown .066 8.2 .72 0 error (1) .41 40 3.8 0 error (1) .43 37 4.0 0 true 62   4100 580 2 true 67 3900 670 2 true 1.5  36 4.7 2 timeout 900   4200 11000 0 true .26 28 3.1 2 true .30  28 3.1  2 true 9.9  120 87   2 true 130   180 2000 2 true 1.9  150 25   2 true 7.8 370 63 2 true 9.7 460 71 2 true 7.4 360 52 2
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .51 130 4.9  2 true .61 22 6.8 2 unknown .084 8.4 .82 0 error (1) .44 40 4.0 0 error (1) .42 40 4.0 0 true 120   4400 1200 2 true 130 4300 1200 2 true .54 44 7.3 2 timeout 900   4200 12000 0 true .43 30 4.9 2 true .43  30 5.0  2 true 9.3  140 91   2 true 200   220 2700 2 true 4.5  320 52   2 true 7.7 400 69 2 true 12   570 100 2 true 8.1 410 57 2
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .51 130 6.0  2 true .62 22 6.4 2 unknown .088 9.4 .92 0 error (1) .42 37 3.4 0 error (1) .42 40 4.2 0 true 130   4300 1300 2 true 130 4300 1400 2 true .54 43 6.8 2 timeout 900   4200 12000 0 true .43 30 4.6 2 true .44  30 4.1  2 true 10    150 88   2 true 200   210 2300 2 true 4.5  320 50   2 true 7.6 420 57 2 true 11   490 89 2 true 8.1 430 61 2
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .20 26 1.5  2 true .25 18 2.9 2 unknown .043 8.1 .37 0 error (1) .44 39 4.0 0 error (1) .41 37 4.0 0 true 8.5 500 63 2 true 39 460 43 2 true .22 25 2.2 2 timeout 900   10000 14000 0 true .16 25 1.5 2 true .12  25 1.5  2 true 1.7  41 19   2 true 26   120 320 2 true .48 32 5.7 2 true 6.0 320 54 2 true 8.2 460 70 2 true 6.3 320 46 2
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .29 44 2.7  2 true .34 20 3.1 2 unknown .062 8.2 .50 0 error (1) .44 38 3.3 0 error (1) .45 40 3.7 0 true 20   1800 180 2 true 23 1900 230 2 true .26 27 3.6 2 timeout 900   7000 12000 0 true .19 27 2.1 2 true .22  27 2.2  2 true 2.7  64 27   2 true 59   150 770 2 true 1.1  95 13   2 true 7.4 350 52 2 true 9.8 470 70 2 true 6.8 330 52 2
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .29 44 2.6  2 true .32 20 3.2 2 unknown .062 8.2 .51 0 error (1) .40 37 3.4 0 error (1) .41 37 3.7 0 true 20   2000 200 2 true 23 1800 220 2 true .28 27 3.3 2 timeout 900   7000 12000 0 true .21 27 2.2 2 true .19  27 2.3  2 true 2.7  64 25   2 true 58   150 850 2 true 1.0  94 14   2 true 6.4 330 51 2 true 10   470 78 2 true 6.9 330 53 2
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true .13 32 1.2  2 error (42) 850    3100 6100   0 unknown .027 8.0 .19 0 error (1) .42 39 3.7 0 error (1) .42 40 3.5 0 timeout 910   7100 10000 0 timeout 900 7100 12000 0 out of memory 87    15000 970   0 timeout 900   1600 9100 0 out of memory 460    15000 5400   0 true .11  24 1.3  2 true 190    350 1800   2 true 3.8 83 42 2 timeout (timeout) 900    1700 5400   0 true 5.9 330 48 2 true 6.1 330 51 2 true 6.1 330 48 2
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true .16 36 1.0  2 error (42) 850    3700 5000   0 unknown .068 43   .59 0 error (1) .42 37 3.4 0 error (1) .42 37 4.0 0 timeout 900   6700 11000 0 timeout 910 7100 11000 0 out of memory 92    15000 1300   0 timeout 900   1600 11000 0 out of memory 470    15000 5700   0 true .13  24 1.3  2 true 890    1600 7900   2 true 3.9 86 43 2 timeout (timeout) 900    2300 5600   0 true 5.5 320 45 2 true 5.9 320 51 2 true 5.6 320 41 2
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true .13 24 .84 2 error (42) 850    4300 8000   0 unknown .020 8.0 .20 0 error (1) .40 37 3.5 0 error (1) .41 40 4.1 0 timeout 900   7100 12000 0 timeout 910 4600 1600 0 out of memory 97    15000 1100   0 timeout 900   770 3200 0 out of memory 470    15000 6500   0 true .14  24 1.6  2 timeout 900    1300 8500   0 true 3.8 87 57 2 timeout (timeout) 900    3200 5600   0 true 5.9 330 48 2 true 6.2 320 50 2 true 6.3 340 46 2
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true .12 25 .95 2 error (42) 850    2000 7000   0 unknown .071 43   .37 0 error (1) .42 38 4.0 0 error (1) .39 37 4.1 0 timeout 920   7000 10000 0 timeout 900 7000 12000 0 out of memory 100    15000 1300   0 timeout 900   1800 8400 0 out of memory 490    15000 6000   0 true .15  24 1.6  2 timeout 900    1200 8300   0 true 3.9 83 45 2 timeout (timeout) 900    4100 6200   0 true 5.4 320 40 2 true 6.1 320 49 2 true 6.2 330 53 2
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true .13 25 1.2  2 error (42) 850    1800 6900   0 unknown .033 8.0 .15 0 error (1) .43 37 3.4 0 error (1) .41 40 3.9 0 timeout 900   2800 2000 0 timeout 900 3700 15000 0 out of memory 110    15000 1100   0 timeout 900   2000 9000 0 out of memory 480    15000 5800   0 true .15  24 1.6  2 timeout 900    1200 8100   0 true 3.9 88 59 2 timeout (timeout) 900    3100 5800   0 true 5.6 320 47 2 true 6.5 320 49 2 true 6.7 360 53 2
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true .17 33 1.1  2 error (42) 850    1500 7700   0 unknown .039 7.9 .17 0 error (1) .43 39 3.7 0 error (1) .42 37 3.9 0 timeout 900   6600 11000 0 timeout 900 6900 13000 0 out of memory 110    15000 1500   0 timeout 900   1900 9400 0 out of memory 500    15000 5500   0 true .16  24 1.5  2 timeout 900    990 9100   0 true 3.9 84 60 2 timeout (timeout) 900    5200 5600   0 true 6.3 350 47 2 true 6.3 320 55 2 true 6.3 340 46 2
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true .13 25 1.1  2 error (42) 850    2000 6800   0 unknown .030 7.9 .21 0 error (1) .42 37 3.8 0 error (1) .41 38 3.4 0 timeout 900   3700 12000 0 timeout 900 3200 13000 0 out of memory 110    15000 1400   0 timeout 900   2000 9800 0 out of memory 490    15000 6900   0 true .18  24 1.6  2 timeout 900    1200 8000   0 true 3.9 86 52 2 timeout (timeout) 900    4300 7700   0 true 5.5 320 44 2 true 6.6 330 54 2 true 6.0 330 51 2
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true .13 25 1.1  2 error (42) 850    1800 6400   0 unknown .033 7.9 .18 0 error (1) .41 40 3.9 0 error (1) .42 38 3.6 0 timeout 900   6500 12000 0 timeout 900 6600 10000 0 out of memory 110    15000 1200   0 timeout 900   860 1800 0 out of memory 500    15000 5800   0 true .15  24 1.8  2 timeout 900    890 9000   0 true 4.0 86 60 2 timeout (timeout) 900    4700 4200   0 true 5.8 310 49 2 true 6.4 320 48 2 true 5.8 310 44 2
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true .14 31 1.0  2 error (42) 850    5500 6100   0 unknown .026 7.6 .16 0 error (1) .42 39 3.7 0 error (1) .43 39 4.4 0 timeout 900   8100 10000 0 timeout 900 8100 10000 0 true 140    8700 1500   2 timeout 900   1200 11000 0 out of memory 420    15000 5000   0 true .087 23 1.0  2 true .83 28 8.1 2 true 3.6 77 46 2 timeout (timeout) 900    380 11000   0 true 5.3 320 43 2 true 6.2 340 47 2 true 5.5 310 43 2
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true .12 23 .90 2 error (42) 850    1300 5700   0 unknown .025 7.6 .21 0 error (1) .43 37 3.5 0 error (1) .45 38 4.2 0 timeout 910   8700 10000 0 timeout 910 8800 9400 0 true 200    12000 2400   2 timeout 900   1300 9400 0 out of memory 420    15000 4800   0 true .12  23 .90 2 true 3.3  36 36   2 true 3.6 75 46 2 timeout (timeout) 900    510 6900   0 true 5.4 320 43 2 true 5.5 320 46 2 true 6.3 330 47 2
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true .12 25 .93 2 error (42) 850    1700 6000   0 unknown .071 43   .56 0 error (1) .45 40 4.0 0 error (1) .44 38 3.5 0 timeout 900   8300 10000 0 timeout 900 8400 9400 0 out of memory 78    15000 850   0 timeout 900   1400 11000 0 out of memory 430    15000 6100   0 true .13  24 1.0  2 true 7.9  55 81   2 true 3.7 81 54 2 timeout (timeout) 900    690 6300   0 true 5.4 320 41 2 true 6.3 340 49 2 true 5.5 320 38 2
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true .11 23 .99 2 error (42) 850    2000 5300   0 unknown .031 7.9 .15 0 error (1) .44 40 3.9 0 error (1) .42 40 3.7 0 timeout 900   8000 9400 0 timeout 900 8300 12000 0 out of memory 79    15000 990   0 timeout 900   1500 9500 0 out of memory 440    15000 5700   0 true .11  24 1.0  2 true 20    77 180   2 true 3.7 90 57 2 timeout (timeout) 900    950 6900   0 true 5.7 320 43 2 true 5.9 320 45 2 true 5.3 320 43 2
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true .12 24 .92 2 error (42) 850    2600 5000   0 unknown .033 8.0 .18 0 error (1) .39 37 3.9 0 error (1) .42 37 3.7 0 timeout 900   7500 11000 0 timeout 900 7500 10000 0 out of memory 83    15000 930   0 timeout 900   1300 6700 0 out of memory 450    15000 6500   0 true .10  24 1.4  2 true 52    120 460   2 true 3.7 83 52 2 timeout (timeout) 900    1300 6400   0 true 5.2 310 42 2 true 5.9 330 46 2 true 5.8 340 46 2
../../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
total 26 960   14000 12000 48 26 12000   42000 86000 20 26 1.9 360 17 0 26 11 1000 97 0 26 11 1000 100 0 26 14000 130000 160000 20 26 14000 120000 170000 20 26 2300    190000 29000   -7 26 21000 75000 230000 3 26 7100   210000 89000 21 26 1200   1400 15000 47 26 7600   11000 74000 36 26 2500 4500 29000 48 26 13000 39000 94000 20 26 1100 10000 14000 46 26 1100 13000 17000 46 26 1100 10000 13000 46
    correct results 25 57   3800 730 48 11 31   1300 380 20 0 0 0 11 580 30000 5800 20 11 1700 31000 13000 20 13 370    22000 4200   25 3 640 1600 7700 3 12 660   3500 7900 21 24 330   1200 3500 47 19 1300   3800 12000 36 25 1700 3400 23000 48 11 41 2400 500 20 23 150 8000 1200 46 23 200 9700 1600 46 23 150 8100 1200 46
        correct true 23 7.3 1800 68 46 9 5.0 220 53 18 0 0 0 9 570 29000 5700 18 9 840 29000 5800 18 12 350    21000 4000   24 0 9 3.5 290 40 18 23 6.0 630 68 46 17 1300   3700 12000 34 23 1700 3000 22000 46 9 30 2300 370 18 23 150 8000 1200 46 23 200 9700 1600 46 23 150 8100 1200 46
        correct false 2 50   2000 660 2 2 26   1100 320 2 0 0 0 2 12 600 89 2 2 880 1900 7400 2 1 17    1000 190   1 3 640 1600 7700 3 3 660   3300 7900 3 1 320   530 3400 1 2 1.5 120 13 2 2 53 370 620 2 2 11 47 130 2 0 0 0
    correct-unconfimed results 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
    incorrect results 0 0 0 0 0 0 0 1 .61 80 7.3 -32 0 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 1 .61 80 7.3 -32 0 0 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (26 tasks, max score: 49) 48 20 0 0 0 20 20 -7 3 21 47 36 48 20 46 46 46
Run set 2ls.sv-comp17.MemSafety-Other cbmc.sv-comp17.MemSafety-Other ceagle.sv-comp17.MemSafety-Other cpa-bam-bnb.sv-comp17.MemSafety-Other cpa-kind.sv-comp17.MemSafety-Other cpa-seq.sv-comp17.MemSafety-Other depthk.sv-comp17.MemSafety-Other esbmc.sv-comp17.MemSafety-Other esbmc-falsi.sv-comp17.MemSafety-Other esbmc-incr.sv-comp17.MemSafety-Other esbmc-kind.sv-comp17.MemSafety-Other predatorhp.sv-comp17.MemSafety-Other smack.sv-comp17.MemSafety-Other symbiotic4.sv-comp17.MemSafety-Other uautomizer.sv-comp17.MemSafety-Other ukojak.sv-comp17.MemSafety-Other utaipan.sv-comp17.MemSafety-Other