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 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 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.Overflows-Other cbmc.sv-comp17.Overflows-Other ceagle.sv-comp17.Overflows-Other cpa-bam-bnb.sv-comp17.Overflows-Other cpa-kind.sv-comp17.Overflows-Other cpa-seq.sv-comp17.Overflows-Other depthk.sv-comp17.Overflows-Other esbmc.sv-comp17.Overflows-Other esbmc-falsi.sv-comp17.Overflows-Other esbmc-incr.sv-comp17.Overflows-Other esbmc-kind.sv-comp17.Overflows-Other smack.sv-comp17.Overflows-Other symbiotic4.sv-comp17.Overflows-Other uautomizer.sv-comp17.Overflows-Other ukojak.sv-comp17.Overflows-Other utaipan.sv-comp17.Overflows-Other
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 ]] --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/ 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
recursive/Addition02WithOverflowBug_false-no-overflow.c .096 22 .87 0 .12 19 1.4  1 .18   44    1.3   0 .41 37 3.9 0 2.2 240 20 0 2.3 240 18 0 .57 50 7.1 1 110    15000 1300   0 .11  23 .73 1 .076 23 1.0  1 .10  23 .94 1 1.6 72 20 1 .16 10   1.8 1 5.5 330 47 1 6.5 340 50 1 6.9 330 48 1
recursive/Addition03_false-no-overflow.c .13  22 .73 0 .16 19 1.2  1 .11   8.2  1.4   0 .43 40 4.0 0 2.3 240 21 0 2.3 240 22 0 .56 49 5.8 1 110    15000 1400   0 .080 23 .83 1 .11  23 .77 1 .081 23 .96 1 1.6 74 22 1 .16 10   1.6 1 6.5 360 49 1 6.3 330 41 1 6.3 330 46 1
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c .11  22 .84 0 .12 17 .96 1 .11   8.4  1.2   0 .45 40 4.3 0 2.5 250 19 1 2.4 250 22 1 64    73 900   0 2.2  160 28   1 .085 23 .87 0 .076 23 .85 0 .080 23 .74 0 1.6 81 21 1 .17 10   2.0 0 6.1 320 46 1 5.5 320 46 1 5.9 320 47 1
recursive/Ackermann01_true-unreach-call_true-no-overflow.c .094 22 .71 0 850    300 2400    0 .11   8.6  1.4   0 .43 40 3.9 0 2.3 240 23 0 2.3 240 20 0 450    15000 6100   0 150    15000 2000   0 900     5600 8100    0 900     4700 10000    0 900     5300 11000    0 880   270 9800 1 900    4300   12000   0 900   7100 11000 0 900   1300 10000 0 910   13000 4600 0
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c .094 22 .64 0 850    320 4200    0 .12   8.5  1.2   0 .41 40 4.0 0 2.3 240 20 0 2.4 240 20 0 450    15000 5900   0 150    15000 2000   0 900     5700 7000    0 900     4700 8000    0 900     5300 9200    0 880   270 7400 1 900    4700   11000   0 900   6500 12000 0 900   1300 10000 0 910   13000 4600 0
recursive/Ackermann03_true-unreach-call_true-no-overflow.c .12  22 .78 0 850    320 3500    0 .11   8.3  1.2   0 .43 39 3.9 0 2.3 250 22 0 2.4 240 21 0 450    15000 6600   0 150    15000 2100   0 900     5700 6900    0 900     4800 9300    0 900     5500 11000    0 880   270 11000 1 900    4300   11000   0 900   6600 12000 0 900   1400 12000 0 910   13000 5100 0
recursive/Ackermann04_true-unreach-call_true-no-overflow.c .095 22 .77 0 850    320 3200    0 .11   8.4  1.3   0 .45 40 4.1 0 2.4 250 20 0 2.4 240 21 0 450    15000 6200   0 150    15000 1900   0 900     5700 7100    0 900     4800 8200    0 900     5500 8400    0 880   270 8900 1 900    4300   11000   0 900   6300 11000 0 900   1500 11000 0 910   13000 4400 0
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c .12  22 .70 0 680    15000 6300    0 .13   44    1.6   0 .43 37 3.6 0 2.4 240 20 0 2.3 240 21 0 400    15000 5100   0 120    15000 1600   0 570     15000 3500    0 370     15000 3400    0 330     15000 2900    0 880   280 9700 1 900    69   11000   0 900   3700 12000 0 900   4300 15000 0 900   3400 11000 0
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c .11  22 .89 0 740    15000 7300    0 .11   8.0  1.2   0 .43 40 4.3 0 2.3 250 21 0 2.3 240 18 0 400    15000 6200   0 120    15000 1300   0 560     15000 4000    0 340     15000 3500    0 320     15000 3700    0 880   280 10000 1 900    190   12000   0 900   4000 13000 0 900   4900 16000 0 900   3500 13000 0
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c .081 22 .81 0 850    6800 7600    0 .074  44    .71  0 .44 40 4.1 0 2.4 250 21 0 2.3 240 19 0 400    15000 5400   0 120    15000 1600   0 570     15000 4100    0 350     15000 3300    0 340     15000 3300    0 880   220 11000 1 900    140   10000   0 900   3500 14000 0 900   2000 13000 0 900   2900 14000 0
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c .089 22 .90 0 .21 17 1.6  2 .11   8.3  1.2   0 .42 37 3.8 0 2.3 250 19 0 2.3 240 21 0 1.3  49 16   0 .49 44 5.9 2 900     920 9100    0 .11  23 .72 2 .12  23 .70 2 1.2 73 15 2 .15 9.2 1.7 2 5.4 320 45 2 5.7 320 44 2 5.5 320 41 2
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c .11  22 .83 0 850    3800 6400    0 .11   7.9  1.0   0 .40 37 3.4 0 2.3 240 23 0 2.4 250 19 0 64    75 820   0 2.4  160 29   1 .11  23 .65 0 .11  23 .66 0 .10  23 .84 0 880   220 11000 1 900    270   13000   0 900   4700 13000 0 900   4600 15000 0 900   3800 13000 0
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c .098 22 .87 0 850    3400 5700    0 .11   7.9  1.2   0 .40 38 3.8 0 2.4 250 20 0 2.3 240 20 0 64    75 970   0 2.4  160 28   1 .11  23 .64 0 .072 23 .90 0 .095 23 .82 0 880   220 12000 1 900    310   11000   0 900   5200 13000 0 900   3900 13000 0 900   4200 13000 0
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c .10  22 .76 0 850    240 2900    0 .13   8.4  1.1   0 .45 38 4.2 0 2.3 240 22 0 2.3 240 20 0 860    15000 11000   0 92    15000 1000   0 900     9700 10000    0 900     1300 10000    0 900     1500 10000    0 880   240 9600 1 900    230   8000   0 900   5800 11000 0 900   1300 11000 0 900   5400 11000 0
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c .11  22 .76 0 .52 18 4.7  2 .12   8.1  1.3   0 .43 39 4.2 0 2.2 240 21 0 2.3 240 18 0 1.5  49 17   0 .14 23 1.8 2 300     15000 4500    0 .99  32 13    2 1.8   46 22    2 31   120 390 2 .16 9.2 1.7 2 27   1400 210 2 900   1100 12000 0 910   13000 5400 0
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c .10  22 .75 0 850    220 2200    0 .12   8.2  1.1   0 .43 37 3.4 0 2.4 250 22 0 2.3 250 19 0 380    15000 5300   0 94    15000 1100   0 900     3900 9600    0 900     1200 8100    0 900     1400 8200    0 880   240 8600 1 900    250   9900   0 900   5800 11000 0 900   1400 13000 0 900   5300 10000 0
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c .10  22 .97 0 850    220 2300    0 .11   8.0  1.1   0 .41 37 3.8 0 2.3 240 19 0 2.4 240 21 0 380    15000 4900   0 97    15000 1100   0 900     9700 9200    0 900     1200 8700    0 900     1400 8500    0 880   250 9000 1 900    300   8600   0 900   5700 13000 0 900   1300 12000 0 900   5300 11000 0
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c .094 22 1.0  0 850    230 2500    0 .11   8.2  1.2   0 .44 40 4.1 0 2.3 250 19 0 2.3 240 21 0 380    15000 4600   0 96    15000 1400   0 900     9700 9700    0 900     2300 9500    0 900     1400 7900    0 880   240 9600 1 900    310   9900   0 900   5600 12000 0 900   1300 12000 0 900   5400 12000 0
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c .084 22 .68 0 850    1900 3800    0 .11   8.5  1.1   0 .40 38 3.5 0 2.4 250 21 0 2.4 240 22 0 510    15000 5900   0 130    15000 1700   0 900     9900 10000    0 900     5700 8400    0 900     6500 10000    0 880   220 10000 2 900    120   10000   0 7.8 390 62 2 7.8 380 60 2 8.4 400 60 2
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c .11  22 .67 0 850    2000 4200    0 .095  7.9  1.2   0 .44 40 3.8 0 2.3 240 20 0 2.3 250 19 0 500    15000 7100   0 130    15000 1800   0 900     10000 8800    0 900     5700 7700    0 900     6100 8400    0 880   220 11000 2 900    120   9300   0 7.8 380 56 2 7.7 390 58 2 7.8 390 59 2
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c .097 22 .85 0 850    400 3300    0 .11   8.3  1.3   0 .42 38 3.3 0 2.3 240 21 0 2.3 240 22 0 480    15000 6400   0 150    15000 1900   0 900     11000 7600    0 900     4300 7100    0 900     4100 7400    0 880   250 12000 1 900    400   9500   0 900   1000 14000 0 900   960 13000 0 400   830 5500 0
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c .13  22 .63 0 850    280 2600    0 .12   8.3  1.5   0 .42 37 3.6 0 2.5 240 24 0 2.5 250 26 0 530    15000 7600   0 190    15000 2400   0 250     15000 1700    0 330     15000 2500    0 410     15000 3400    0 880   230 9500 1 900    53   13000   0 900   1500 11000 0 900   1300 12000 0 900   6900 9800 0
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c .084 22 1.0  0 850    5000 4100    0 .11   8.4  1.2   0 .45 38 3.9 0 2.3 240 21 0 2.3 240 20 0 420    15000 5400   0 120    15000 1400   0 900     960 10000    0 900     980 9500    0 900     1000 9300    0 880   91 10000 2 900    140   14000   0 7.4 340 60 2 8.9 460 64 2 7.3 340 53 2
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c .095 22 .92 0 850    7100 3500    0 .13   8.5  1.2   0 .43 40 4.3 0 2.3 240 24 0 2.4 250 24 0 420    15000 5300   0 110    15000 1500   0 900     500 10000    0 900     930 10000    0 900     950 9500    0 880   120 12000 2 900    68   11000   0 13   510 88 2 11   480 100 2 23   790 220 2
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c .12  22 .67 0 850    1400 2100    0 .12   8.1  1.2   0 .44 38 4.7 0 2.6 260 23 0 2.4 240 21 0 410    15000 5000   0 110    15000 1500   0 610     15000 4800    0 600     15000 5900    0 560     15000 4800    0 84   180 1200 0 900    1800   13000   0 900   5300 13000 0 900   1200 14000 0 910   13000 6000 0
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c .12  22 .72 0 1.1  22 14    1 .11   8.0  1.4   0 .43 40 3.7 0 2.3 240 18 0 2.3 240 21 0 1.9  49 20   0 1.3  50 17   1 900     3300 9400    0 9.1   170 120    1 12     250 170    1 1.9 74 26 0 .52 12   5.8 1 900   2200 13000 0 900   1600 13000 0 900   2700 11000 0
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c .098 22 .77 0 1.2  24 11    1 .11   8.0  1.1   0 .46 40 4.1 0 2.3 240 21 0 2.3 240 23 0 1.7  49 19   0 1.3  50 15   1 900     3300 13000    0 9.0   170 120    1 12     250 140    1 13   85 180 0 .57 12   7.0 1 900   2200 14000 0 900   1800 14000 0 900   2600 11000 0
bitvector/jain_1_false-no-overflow.i .095 22 .86 1 .12 17 1.1  1 .0092 .92 .020 0 .42 38 3.5 0 2.4 240 22 1 2.4 240 22 1 .56 75 5.7 1 52    15000 530   0 .074 23 .75 1 .097 23 .78 1 .081 23 .84 1 1.8 98 22 1 .17 10   2.2 1 5.4 320 38 1 5.5 320 38 1 5.8 340 42 1
bitvector/jain_2_false-no-overflow.i .11  23 .88 1 .11 18 1.2  1 .0044 1.0  .021 0 .43 37 3.9 0 2.5 240 21 1 2.3 250 22 1 .63 76 8.2 1 56    15000 680   0 .11  23 .84 1 .10  23 .89 1 .096 23 .90 1 2.0 110 23 1 .15 10   1.5 1 5.4 320 39 1 5.6 320 45 1 5.6 320 39 1
bitvector/jain_4_false-no-overflow.i .10  23 .93 1 .13 20 1.3  1 .0086 .86 .021 0 .42 38 3.7 0 2.4 240 21 1 2.4 240 19 1 29    85 320   1 67    15000 690   0 .080 23 .86 1 .095 23 .79 1 .12  23 .78 1 1.9 110 29 1 .18 10   1.7 1 5.8 320 48 1 5.5 320 48 1 6.2 320 42 1
bitvector/jain_5_false-no-overflow.i 900     1300 8800    0 260    15000 3600    0 .0071 .88 .020 0 .41 37 4.3 0 900   3900 12000 0 900   1400 11000 0 900    2200 8000   0 3.3  350 40   0 110     15000 1500    0 97     15000 1300    0 150     15000 2100    0 880   300 11000 0 1.8  360   19   0 900   4800 14000 0 900   1200 13000 0 900   740 12000 0
bitvector/jain_6_false-no-overflow.i .12  26 1.1  1 .13 22 1.3  1 .010  .82 .018 0 .42 40 3.7 0 2.4 240 20 1 2.5 250 23 1 24    80 260   1 70    15000 670   0 .11  23 .98 1 .083 23 .89 1 .095 23 .74 1 2.4 120 26 1 .15 10   2.3 1 5.5 320 48 1 5.5 320 50 1 5.3 320 41 1
bitvector/jain_7_false-no-overflow.i .11  24 1.0  1 .15 19 1.1  1 .010  .72 .021 0 .44 39 3.6 0 2.3 240 20 1 2.5 250 20 1 93    96 990   1 65    15000 720   0 .10  23 .86 1 .079 23 .76 1 .10  23 .86 1 2.2 120 27 1 .16 10   1.8 1 5.4 320 45 1 5.7 320 43 1 5.5 320 41 1
bitvector/modulus_false-no-overflow.i .12  25 1.0  1 .10 17 .84 1 .0076 .88 .025 0 .42 38 3.8 0 2.5 250 21 1 2.8 280 27 1 .48 100 6.0 1 880    15000 10000   0 .10  23 .82 0 .091 23 .78 0 .077 23 .83 0 1.8 83 20 1 .20 11   2.5 1 5.6 330 48 0 5.8 320 46 0 6.1 350 50 0
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i .14  24 .94 2 .37 18 3.6  2 .0050 .79 .021 0 .43 40 3.9 0 23   510 180 2 23   590 180 2 1.8  110 21   0 140    15000 1700   0 450     15000 5000    0 .21  25 3.0  2 .12  24 1.5  2 2.6 160 29 2 .16 9.3 2.2 2 6.2 320 47 2 7.4 350 56 2 7.4 370 61 2
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i .14  23 .93 2 .34 18 4.3  2 .0091 .76 .022 0 .42 37 3.5 0 22   460 160 2 21   570 170 2 1.8  110 20   0 140    15000 1800   0 380     15000 5100    0 .26  26 2.7  2 .13  24 1.4  2 2.6 150 34 2 .18 9.4 1.8 2 7.2 340 60 2 7.8 360 59 2 7.0 340 55 2
bitvector/byte_add_false-unreach-call_true-no-overflow.i .13  23 .92 2 .35 18 4.3  2 .011  .93 .020 0 .45 38 3.6 0 86   1500 1100 2 85   1400 900 2 2.1  110 26   0 200    15000 2200   0 450     15000 5300    0 .30  30 3.7  2 .14  24 1.9  2 2.5 140 31 2 .18 9.5 2.1 2 6.7 330 54 2 8.2 360 63 2 6.2 330 48 2
bitvector/gcd_1_true-unreach-call_true-no-overflow.i .12  24 1.1  2 .27 22 2.8  2 .011  1.0  .025 0 .41 40 3.7 0 4.9 290 50 2 5.2 290 55 2 500    98 6600   0 35    15000 400   0 .089 23 .83 0 .11  23 .67 0 .073 23 .88 0 1.4 81 17 2 .16 9.2 1.4 2 6.1 320 44 2 6.4 320 49 2 7.8 380 64 2
bitvector/gcd_2_true-unreach-call_true-no-overflow.i .10  23 .97 2 .80 31 9.6  2 .0095 1.0  .019 0 .39 40 3.9 0 76   430 660 2 74   440 700 2 20    75 240   0 36    15000 430   0 .086 23 .67 0 .076 23 .84 0 .094 23 .72 0 1.4 80 18 2 .15 9.4 1.8 2 7.0 340 49 2 6.3 320 50 2 6.2 330 47 2
bitvector/gcd_3_true-unreach-call_true-no-overflow.i .10  23 .96 2 .83 31 8.8  2 .011  .90 .019 0 .39 37 3.4 0 75   430 740 2 76   430 570 2 20    76 250   0 36    15000 390   0 .071 23 1.0  0 .098 23 .79 0 .10  23 .68 0 1.4 78 17 2 .18 9.4 1.6 2 7.0 340 52 2 6.5 330 50 2 6.6 330 49 2
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 1.2   39 14    2 .30 17 2.7  2 .0098 1.0  .020 0 .43 37 3.5 0 2.8 260 23 2 2.9 250 25 2 500    110 6400   0 .77 100 8.2 2 .083 23 .70 0 .095 23 .93 0 .091 23 1.0  0 1.5 88 21 2 .15 9.2 1.6 2 9.9 480 77 2 20   530 170 2 11   480 97 2
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i .13  24 .85 2 .55 17 6.4  2 .0068 .77 .029 0 .40 37 3.5 0 4.2 280 33 2 4.1 260 36 2 1.4  76 16   0 .70 100 8.6 2 900     2600 14000    0 .13  23 1.3  2 .078 23 1.1  2 1.3 66 14 2 .18 9.4 1.8 2 5.3 320 43 2 5.4 320 43 2 5.9 330 44 2
bitvector/jain_1_true-unreach-call_true-no-overflow.i .11  22 .68 2 850    14000 6500    0 .0090 .99 .017 0 .43 38 3.6 0 910   8800 7900 0 910   8800 7900 0 1.2  75 13   0 74    15000 790   0 900     790 9900    0 320     15000 4300    0 .080 23 .90 2 1.3 80 14 2 .16 9.3 1.7 2 5.8 320 40 2 5.2 310 40 2 5.2 320 43 2
bitvector/jain_2_true-unreach-call_true-no-overflow.i .088 22 .72 2 850    14000 6900    0 .010  1.1  .030 0 .41 37 4.1 0 910   9700 8400 0 910   9500 8200 0 1.2  75 14   0 66    15000 690   0 900     780 11000    0 310     15000 3700    0 .099 23 .75 2 1.3 74 17 2 .15 9.3 1.6 2 5.9 330 42 2 5.1 320 40 2 6.1 330 50 2
bitvector/jain_4_true-unreach-call_true-no-overflow.i .11  22 .73 2 850    14000 8900    0 .010  .96 .027 0 .41 38 4.0 0 910   10000 8500 0 910   10000 9400 0 1.2  75 13   0 61    15000 590   0 900     780 11000    0 310     15000 3800    0 .094 23 .74 2 1.3 79 18 2 .15 9.6 1.6 2 5.5 330 47 2 5.3 330 47 2 6.3 330 43 2
bitvector/jain_5_true-unreach-call_true-no-overflow.i .083 22 .78 2 260    15000 2900    0 .010  1.0  .024 0 .41 40 4.0 0 900   3900 12000 0 900   990 11000 0 1.2  75 15   0 5.1  1200 59   2 900     12000 13000    0 340     15000 5000    0 .099 23 .71 2 1.3 78 15 2 .14 9.6 1.4 2 6.0 330 44 2 5.3 320 40 2 5.2 320 44 2
bitvector/jain_6_true-unreach-call_true-no-overflow.i .10  23 .74 2 850    14000 6300    0 .0097 1.0  .024 0 .40 37 3.4 0 910   10000 9300 0 910   10000 10000 0 1.2  75 13   0 60    15000 660   0 900     760 9500    0 320     15000 4100    0 .10  23 .78 2 1.3 75 17 2 .16 9.2 1.8 2 5.7 330 44 2 6.0 340 42 2 5.8 320 40 2
bitvector/jain_7_true-unreach-call_true-no-overflow.i .12  22 .82 2 850    15000 7800    0 .010  .87 .020 0 .44 40 3.8 0 910   5500 7100 0 910   5600 5300 0 1.2  75 14   0 60    15000 720   0 900     760 10000    0 310     15000 3600    0 .079 23 .76 2 1.3 76 16 2 .15 9.3 1.6 2 6.3 340 52 2 6.0 330 51 2 5.3 320 41 2
bitvector/modulus_true-unreach-call_true-no-overflow.i .13  24 .92 2 160    1000 850    2 .011  1.0  .028 0 .42 37 4.0 0 900   4100 7400 0 900   4200 9100 0 900    620 7100   0 900    15000 10000   2 900     4800 12000    0 900     2700 6500    0 .095 23 .96 2 1.4 72 18 2 270    56   3300   2 5.5 310 40 0 6.0 320 46 0 5.7 320 41 0
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i .089 22 .94 2 .43 17 4.0  2 .010  .88 .015 0 .42 40 3.8 0 3.0 250 24 2 3.1 260 28 2 1.4  76 15   0 1.7  170 18   2 140     15000 1800    0 .12  23 1.2  2 .081 23 .91 2 2.1 87 25 2 .14 9.4 1.4 2 5.4 310 46 2 5.7 320 47 2 5.8 320 48 2
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i .098 22 .89 2 .44 17 4.8  2 .010  .88 .018 0 .40 37 4.3 0 32   760 280 2 32   730 260 2 1.4  76 16   0 1.5  190 16   2 140     15000 1800    0 .16  23 1.5  2 .12  23 .79 2 2.1 95 26 2 .16 9.3 1.7 2 6.8 340 47 2 5.7 320 46 2 6.6 340 54 2
bitvector/parity_true-unreach-call_true-no-overflow.i .097 23 .86 2 .86 21 11    2 .0093 .93 .016 0 .42 38 4.0 0 14   440 120 2 16   430 110 2 1.4  75 15   0 47    15000 520   0 900     700 6900    0 9.7   210 110    2 .087 23 .96 2 1.4 77 17 2 .15 9.4 1.8 2 5.6 320 38 2 5.3 320 46 2 5.6 320 46 2
bitvector/sum02_false-unreach-call_true-no-overflow.i .081 23 .84 2 850    8400 4000    0 .010  .88 .019 0 .43 37 3.9 0 900   1800 9900 0 900   1800 10000 0 1.2  75 13   0 50    15000 540   0 900     770 9000    0 200     15000 2800    0 .091 23 1.0  2 1.3 73 16 2 .16 9.4 1.9 2 5.8 330 45 2 6.0 320 48 2 5.7 320 40 2
bitvector/sum02_true-unreach-call_true-no-overflow.i .11  24 .91 2 850    7000 2600    0 .0092 .89 .027 0 .40 38 3.6 0 900   1800 11000 0 900   1800 11000 0 1.2  75 16   0 50    15000 500   0 900     750 9100    0 210     15000 2500    0 .076 23 1.1  2 1.4 80 15 2 .16 9.5 1.8 2 5.4 320 42 2 16   330 200 2 5.6 320 45 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
total 54 910    2500 8800   46 54 23000   180000 130000 39 54 3.4 350 34 0 54 23 2100 210 0 54 9500 74000 98000 29 54 9500 68000 97000 29 54 11000 280000 140000 8 54 5600   620000 68000 21 54 29000    300000 300000    7 54 17000     260000 170000    27 54 14000     140000 140000    45 54 18000 7900 210000 76 54 18000   23000 220000 54 54 17000 100000 240000 58 54 18000 51000 250000 56 54 18000 150000 190000 56
    correct results 26 4.0  620 36   46 23 160   1500 930 37 0 0 18 360 7300 3500 29 18 360 7400 3200 29 8 150 610 1600 8 9 910   17000 10000 17 7 .67 160 5.9  7 16 13     580 140    25 25 4.2   610 44    43 35 3600 3500 44000 61 30 270   330 3400 52 33 230 12000 1800 58 32 230 11000 1900 56 32 220 11000 1700 56
        correct true 20 3.3  480 30   40 14 160   1300 920 28 0 0 11 340 5600 3300 22 11 340 5600 3000 22 0 8 910   17000 10000 16 0 9 12     410 140    18 18 3.5   440 38    36 26 3600 2600 44000 52 22 270   250 3400 44 25 190 9700 1400 50 24 180 8500 1500 48 24 170 8700 1400 48
        correct false 6 .67 140 5.8 6 9 1.1 170 10 9 0 0 7 17 1700 140 7 7 17 1800 150 7 8 150 610 1600 8 1 2.2 160 28 1 7 .67 160 5.9  7 7 .64  160 5.9  7 7 .68  160 6.0  7 9 17 870 210 9 8 1.3 82 15 8 8 46 2600 360 8 8 46 2600 360 8 8 48 2600 350 8
    correct-unconfimed results 0 2 2.3 46 25 2 0 0 0 0 0 5 11   770 130 4 1 .10 23 .82 0 3 18     370 240    2 3 24     520 310    2 15 13000 3700 150000 15 4 3.1 400 34 2 0 0 0
        correct-unconfirmed true 0 2 2.3 46 25 2 0 0 0 0 0 4 7.4 420 89 4 0 2 18     350 240    2 2 24     500 310    2 15 13000 3700 150000 15 2 1.1 25 13 2 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0 1 3.3 350 40 0 1 .10 23 .82 0 1 .091 23 .78 0 1 .077 23 .83 0 0 2 2.0 370 21 0 0 0 0
    incorrect results 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (54 tasks, max score: 98) 46 39 0 0 29 29 8 21 7 27 45 76 54 58 56 56
Run set 2ls.sv-comp17.Overflows-Other cbmc.sv-comp17.Overflows-Other ceagle.sv-comp17.Overflows-Other cpa-bam-bnb.sv-comp17.Overflows-Other cpa-kind.sv-comp17.Overflows-Other cpa-seq.sv-comp17.Overflows-Other depthk.sv-comp17.Overflows-Other esbmc.sv-comp17.Overflows-Other esbmc-falsi.sv-comp17.Overflows-Other esbmc-incr.sv-comp17.Overflows-Other esbmc-kind.sv-comp17.Overflows-Other smack.sv-comp17.Overflows-Other symbiotic4.sv-comp17.Overflows-Other uautomizer.sv-comp17.Overflows-Other ukojak.sv-comp17.Overflows-Other utaipan.sv-comp17.Overflows-Other