Tool 2LS 0.5.0 BLAST 2.7.3 CBMC 5.6 Ceagle Ceagle 1.3 @ 53cfa89 CPAchecker 1.6.1-svn 23987 CPAchecker 1.6.1-svn 24048 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 3.1 64-bit x86_64 linux skink 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-57-generic [Linux 4.4.0-57-generic; Linux 4.4.0-59-generic] 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-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:51:44 CET ]] [[ 2017-01-14 18:06:48 CET ]] [[ 2017-01-14 19:59:41 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:52:12 CET ]] [[ 2017-01-14 18:07:02 CET ]] [[ 2017-01-14 19:59:19 CET ]] 2017-01-10 20:44:08 CET [[ 2017-01-14 18:01:01 CET ]] [[ 2017-01-14 20:09:29 CET ]] [[ 2017-01-14 18:26:00 CET ]] [[ 2017-01-14 20:41:28 CET ]] 2017-01-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]] 2017-01-11 11:18:39 CET [[ 2017-01-14 21:32:33 CET ]] [[ 2017-01-14 22:21:46 CET ]] [[ 2017-01-14 21:35:07 CET ]] [[ 2017-01-14 22:35:09 CET ]] 2017-01-11 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]] 2017-01-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]] 2017-01-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]] 2017-01-11 16:16:17 CET [[ 2017-01-14 22:37:08 CET ]] [[ 2017-01-15 00:13:18 CET ]] [[ 2017-01-14 22:52:42 CET ]] [[ 2017-01-15 00:24:59 CET ]] 2017-01-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]] 2017-01-13 11:09:20 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 01:53:26 CET ]] [[ 2017-01-15 01:38:17 CET ]] [[ 2017-01-15 01:54:04 CET ]] 2017-01-13 11:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]] 2017-01-13 11:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]] 2017-01-13 12:41:58 CET [[ 2017-01-15 02:09:41 CET ]] [[ 2017-01-15 04:03:21 CET ]] [[ 2017-01-15 02:31:54 CET ]] [[ 2017-01-15 04:27:36 CET ]] 2017-01-13 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]] 2017-01-14 09:46:18 CET [[ 2017-01-15 02:18:39 CET ]] [[ 2017-01-15 04:12:25 CET ]] [[ 2017-01-15 02:37:40 CET ]] [[ 2017-01-15 04:38:18 CET ]]
Run set 2ls.sv-comp17.ReachSafety-BitVectors blast.sv-comp17.ReachSafety-BitVectors cbmc.sv-comp17.ReachSafety-BitVectors ceagle.sv-comp17.ReachSafety-BitVectors cpa-bam-bnb.sv-comp17.ReachSafety-BitVectors cpa-kind.sv-comp17.ReachSafety-BitVectors cpa-seq.sv-comp17.ReachSafety-BitVectors depthk.sv-comp17.ReachSafety-BitVectors esbmc.sv-comp17.ReachSafety-BitVectors esbmc-falsi.sv-comp17.ReachSafety-BitVectors esbmc-incr.sv-comp17.ReachSafety-BitVectors esbmc-kind.sv-comp17.ReachSafety-BitVectors skink.sv-comp17.ReachSafety-BitVectors smack.sv-comp17.ReachSafety-BitVectors symbiotic4.sv-comp17.ReachSafety-BitVectors uautomizer.sv-comp17.ReachSafety-BitVectors ukojak.sv-comp17.ReachSafety-BitVectors utaipan.sv-comp17.ReachSafety-BitVectors
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.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-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.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-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.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-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.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-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.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-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.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-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.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-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.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-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.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-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.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-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.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-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.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-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.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-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.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-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.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-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/skink.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/skink.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/skink.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/skink.2017-01-13_1109.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-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.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-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.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_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.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_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.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
bitvector/byte_add_false-unreach-call_true-no-overflow.i false(unreach-call) .33  27 4.2  1 exception (gremlins) 34     40 430    0 false(unreach-call) .28 18 3.0  1 false(unreach-call) 1.1   41   9.2  0 error 13   530 95 0 false(unreach-call) 8.6 480 53 1 false(unreach-call) 76   1700 1000 1 false(unreach-call) 2.2  110 28   1 false(unreach-call) 51    2200 620   1 false(unreach-call) .14  24 1.5  0 false(unreach-call) .14  24 1.9  0 false(unreach-call) .15  24 1.7  0 unknown 11   680 87 0 false(unreach-call) 4.7 130 59 1 false(unreach-call) .20 11   2.3 0 false(unreach-call) 55   750 540 1 false(unreach-call) 29   480 270 1 false(unreach-call) 92   940 1000 1
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 900     1500 10000    0 exception (gremlins) .20  23 2.1  0 error (42) 850    7900 4000    0 timeout 900     13000   11000    0 error 3.5 300 30 0 segmentation fault 71   2800 570 0 timeout 900   4000 7600 0 unknown 69    76 840   0 false(unreach-call) 2.2  150 24   0 timeout 900     6700 1700    0 out of memory 300     15000 3900    0 out of memory 250     15000 3400    0 unknown 4.9 340 39 0 error (1) 880   450 11000 0 timeout (timeout) 900    800   10000   0 timeout 900   340 11000 0 timeout 900   660 13000 0 unknown 180   370 2200 0
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true .40  28 5.8  2 exception (gremlins) 11     33 140    0 true .35 18 3.9  2 true 1.7   9.0 21    2 error 10   470 82 0 true 14   590 87 2 true 70   1700 770 2 true 74    1800 870   2 true 41    2200 540   2 out of memory 750     15000 8200    0 true .32  24 4.1  2 true .43  28 5.2  2 unknown 11   680 81 0 true 12   150 130 2 true .22 10   2.2 2 timeout 900   4100 11000 0 timeout 900   3500 12000 0 timeout 900   1200 11000 0
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true .42  28 4.5  2 false(unreach-call) 34     35 430    -16 true .36 18 3.9  2 true 2.0   9.7 28    2 error 15   540 100 0 true 15   640 110 2 true 25   920 260 2 true 28    840 300   2 true 42    2200 530   2 out of memory 750     15000 9400    0 true .33  24 4.4  2 true .47  28 6.0  2 unknown 11   680 95 0 true 15   150 180 2 true .31 18   2.5 2 true 580   1400 6800 2 timeout 900   4500 11000 0 timeout 900   1200 13000 0
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .29  25 3.4  2 false(unreach-call) .83  23 8.5  -16 true .32 21 3.7  2 true 29     490   380    2 error 8.3 310 95 0 true 9.5 330 80 2 true 6.5 280 87 2 true 490    280 6000   2 true 120    1200 1200   2 timeout 900     6900 2100    0 true .47  26 5.7  2 true .46  26 5.7  2 unknown 6.0 350 49 0 true 1.7 77 20 2 true .21 11   2.1 2 timeout 900   530 11000 0 true 110   480 950 2 timeout 900   460 12000 0
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true .69  32 9.9  2 false(unreach-call) .90  22 8.8  -16 true 1.2  31 17    2 true .59  47   12    2 true 3.6 290 31 2 true 240   660 1500 2 true 7.1 280 77 2 true 240    290 2400   2 true 360    1300 3800   2 timeout 900     310 10000    0 true 180     150 2000    2 true 190     200 2100    2 unknown 6.4 350 54 0 true 860   300 13000 2 true 2.0  14   25   2 timeout 900   730 11000 0 timeout 900   720 11000 0 timeout 900   560 11000 0
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true .64  32 8.9  2 false(unreach-call) 1.0   21 10    -16 true 1.2  31 13    2 true .68  11   7.5  2 error 4.8 300 50 0 true 220   630 1500 2 true 150   310 2000 2 true 460    320 5000   2 true 230    1400 2500   2 timeout 900     250 11000    0 timeout 900     150 2300    0 true 250     200 3100    2 unknown 5.7 340 46 0 timeout 880   190 11000 0 true 2.1  14   27   2 timeout 900   560 11000 0 timeout 900   640 11000 0 timeout 900   610 11000 0
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true .81  33 10    2 true 1.9   22 19    1 true .30 17 3.1  2 true 1.7   22   23    2 true 2.9 270 30 2 true 2.9 270 25 2 true 2.3 240 20 2 true 490    260 6400   2 true .16 23 1.4 2 timeout 900     9900 13000    0 true .079 23 .99 2 true .16  30 1.6  2 unknown 6.0 350 50 0 true 1.5 70 18 2 true .13 9.4 1.9 2 timeout 900   670 11000 0 true 13   480 110 2 timeout 900   1100 11000 0
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .58  44 7.3  2 timeout 900     230 8500    0 true .56 17 6.9  2 true .26  8.3 2.9  2 error 5.6 350 47 0 true 9.4 450 79 2 true 6.9 400 58 2 true 17    410 210   2 true .16 23 2.0 2 out of memory 92     15000 1400    0 true .15  23 1.3  2 true .69  74 8.7  2 unknown 5.9 340 43 0 true 1.3 68 18 2 true .18 10   2.0 2 true 120   1700 1200 2 true 91   1800 1100 2 true 340   1600 3400 2
bitvector/jain_1_true-unreach-call_true-no-overflow.i timeout 900     1400 11000    0 exception (gremlins) .13  19 .71 0 error (134) 94    14000 1200    0 true .23  7.8 2.2  2 true 2.9 270 27 2 true 4.3 310 29 2 true 2.8 270 28 2 unknown 300    290 3400   0 true 5.3  510 70   2 out of memory 230     15000 2300    0 out of memory 180     15000 1500    0 out of memory 280     15000 3300    0 unknown 4.6 330 37 0 true 890   240 11000 2 timeout (timeout) 900    75   9100   0 true 6.7 340 55 2 timeout 900   890 9500 0 true 6.2 340 48 2
bitvector/jain_2_true-unreach-call_true-no-overflow.i timeout 900     1500 9900    0 exception (gremlins) .12  20 .95 0 error (134) 58    14000 790    0 true .23  7.7 2.4  2 true 2.8 270 27 2 true 4.3 300 31 2 true 2.7 260 26 2 unknown 900    290 7700   0 true 6.8  730 91   2 out of memory 170     15000 1300    0 out of memory 150     15000 1700    0 timeout 900     4600 7100    0 unknown 4.7 330 43 0 true 890   250 8500 2 timeout (timeout) 900    93   8300   0 true 7.2 340 56 2 timeout 900   850 11000 0 true 6.7 350 51 2
bitvector/jain_4_true-unreach-call_true-no-overflow.i timeout 900     2000 10000    0 exception (gremlins) .12  21 1.3  0 error (134) 69    14000 730    0 true .24  43   3.1  2 true 2.9 270 29 2 true 5.0 320 32 2 true 2.8 270 25 2 unknown 890    240 7000   0 true 8.6  890 110   2 out of memory 270     15000 2100    0 out of memory 260     15000 2000    0 timeout 900     3100 7600    0 unknown 4.8 330 42 0 true 880   260 9300 2 timeout (timeout) 900    15000   12000   0 true 5.7 330 49 2 true 6.4 320 46 2 true 6.2 320 43 2
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 900     1500 9900    0 timeout 900     5500 10000    0 out of memory 250    15000 3600    0 true .21  7.7 2.4  1 timeout 900   3900 12000 0 timeout 910   7500 8500 0 timeout 900   7200 8900 0 unknown 59    75 680   0 true .25 40 3.3 1 timeout 900     12000 13000    0 out of memory 340     15000 4900    0 out of memory 140     15000 1400    0 unknown 4.6 330 35 0 true 880   200 8900 1 timeout (timeout) 890    15000   13000   0 timeout 900   2200 13000 0 timeout 900   800 14000 0 true 7.2 360 59 1
bitvector/jain_6_true-unreach-call_true-no-overflow.i timeout 900     1900 12000    0 exception (gremlins) .15  21 1.4  0 error (134) 150    14000 1600    0 true .24  7.7 2.6  2 true 2.9 270 25 2 true 4.6 300 36 2 true 2.9 270 24 2 unknown 890    270 8400   0 true 8.8  890 96   2 out of memory 200     15000 1600    0 out of memory 170     15000 1400    0 timeout 900     5700 7600    0 unknown 4.9 330 44 0 true 880   270 7900 2 timeout (timeout) 890    15000   12000   0 true 5.9 330 48 2 true 9.7 330 96 2 true 6.3 330 51 2
bitvector/jain_7_true-unreach-call_true-no-overflow.i timeout 900     1700 9600    0 exception (gremlins) .14  21 1.2  0 error (134) 110    14000 1300    0 true .24  7.5 3.1  2 true 3.0 270 28 2 true 8.8 400 73 2 true 4.4 270 48 2 unknown 900    290 6700   0 true 8.2  760 88   2 out of memory 230     15000 2500    0 out of memory 580     15000 1400    0 timeout 900     7500 8300    0 unknown 4.9 340 42 0 true 890   290 8700 2 timeout (timeout) 890    15000   12000   0 true 5.9 320 50 2 timeout 900   770 10000 0 true 6.6 340 56 2
bitvector/modulus_true-unreach-call_true-no-overflow.i true .77  36 11    2 false(unreach-call) .070 18 .75 -16 true 380    1100 2100    2 true 1.8   49   20    2 error 21   310 240 0 true 21   1500 160 2 true 230   1700 3100 2 unknown 890    380 7500   0 timeout 900    5600 8700   0 timeout 900     1000 7900    0 timeout 900     1400 6300    0 true .43  25 5.4  2 unknown 5.7 340 45 0 true 340   260 2200 2 true 270    56   3400   2 unknown 29   330 420 0 timeout 900   830 8600 0 unknown 9.7 330 99 0
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .17  24 1.3  2 false(unreach-call) .77  24 8.2  -16 true .40 17 5.9  2 true .26  7.7 2.7  2 true 3.2 290 31 2 true 2.9 270 25 2 true 2.3 240 20 2 true 7.0  260 77   2 true .16 23 1.8 2 timeout 900     1700 14000    0 true .10  23 1.1  2 true .14  23 1.7  2 unknown 5.1 340 39 0 true 1.2 68 16 2 true .15 9.4 1.4 2 true 270   2300 3800 2 true 300   2600 3800 2 true 110   2400 1300 2
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .15  24 1.4  2 false(unreach-call) 1.6   34 17    -16 true .47 17 3.9  2 true .28  7.5 3.6  2 error 14   490 130 0 true 5.7 340 39 2 true 17   540 160 2 true 22    600 230   2 true .18 23 2.0 2 out of memory 530     15000 6700    0 true .17  23 1.4  2 true .21  23 2.1  2 unknown 5.3 320 43 0 true 1.3 65 16 2 true .15 9.8 1.7 2 timeout 900   880 11000 0 timeout 900   840 12000 0 timeout 900   740 12000 0
bitvector/parity_true-unreach-call_true-no-overflow.i true 2.5   33 30    2 false(unreach-call) .072 18 .64 -16 true 2.5  22 32    2 true .68  7.8 6.9  2 error 3.0 280 29 0 true 25   650 210 2 true 120   730 1600 2 unknown 890    150 10000   0 true 2.3  160 25   2 timeout 900     280 11000    0 timeout 900     340 12000    0 timeout 900     200 2600    0 unknown 5.2 340 42 0 true 880   280 12000 2 true 1.4  11   20   2 timeout 900   1000 11000 0 timeout 900   1400 12000 0 timeout 900   940 13000 0
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 900     1500 11000    0 exception (gremlins) .61  26 10    0 error (42) 850    7300 3500    0 timeout 900     5200   11000    0 error 3.3 300 32 0 segmentation fault 140   3800 1200 0 timeout 900   6300 9800 0 unknown 170    490 1800   0 false(unreach-call) 2.6  150 34   -16 out of memory 690     15000 7600    0 out of memory 390     15000 5300    0 out of memory 290     15000 2600    0 unknown 4.6 330 36 0 true 880   330 11000 1 timeout (timeout) 900    800   12000   0 timeout 900   510 12000 0 timeout 900   800 8900 0 unknown 37   370 450 0
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 26     240 220    1 false(unreach-call) 23     38 230    1 false(unreach-call) 4.3  220 58    1 false(unreach-call) .028 8.1 .26 1 false(unreach-call) 18   740 140 0 false(unreach-call) 47   1700 290 1 false(unreach-call) 8.3 440 62 1 false(unreach-call) 33    100 470   1 out of memory 310    15000 3900   0 false(unreach-call) 3.0   110 35    1 false(unreach-call) 5.0   240 80    1 false(unreach-call) 8.5   410 120    1 unknown 17   750 140 0 false(unreach-call) 16   220 170 1 false(unreach-call) .37 11   4.6 0 false(unreach-call) 24   570 200 1 timeout 900   4900 15000 0 false(unreach-call) 24   580 170 1
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 16     240 150    1 false(unreach-call) 250     100 2300    1 false(unreach-call) 3.7  180 47    1 false(unreach-call) .064 8.1 .17 1 false(unreach-call) 23   1000 170 1 false(unreach-call) 70   3000 490 1 false(unreach-call) 11   510 100 1 false(unreach-call) 56    110 830   1 false(unreach-call) 890    15000 12000   1 false(unreach-call) 5.8   150 68    1 false(unreach-call) 9.8   390 110    1 false(unreach-call) 16     680 240    1 unknown 17   780 140 0 false(unreach-call) 38   240 420 1 false(unreach-call) .48 12   5.7 0 false(unreach-call) 28   720 220 1 timeout 900   4200 13000 0 false(unreach-call) 28   630 210 1
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 21     170 190    1 false(unreach-call) .98  35 9.9  0 false(unreach-call) .91 75 12    1 false(unreach-call) .040 8.1 .22 1 false(unreach-call) 8.8 460 64 1 false(unreach-call) 25   920 160 1 false(unreach-call) 6.7 330 53 1 false(unreach-call) 18    85 210   1 false(unreach-call) 890    15000 8200   1 false(unreach-call) 5.7   66 14    1 false(unreach-call) 2.2   120 33    1 false(unreach-call) 3.5   190 47    1 unknown 17   760 140 0 false(unreach-call) 9.1 190 100 1 false(unreach-call) .29 11   2.8 1 false(unreach-call) 22   560 170 1 false(unreach-call) 87   860 960 1 false(unreach-call) 22   560 160 1
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     760 9000    0 timeout 900     420 9300    0 true 16    360 170    2 true 4.0   8.7 37    2 error 18   740 130 0 true 57   1800 350 2 true 21   1600 220 2 true 170    1300 2100   2 out of memory 330    15000 3600   0 timeout 900     5500 8500    0 true 34     1200 470    2 true 59     1900 780    2 unknown 17   740 150 0 true 150   380 1400 2 true .62 20   7.2 2 true 35   840 280 2 timeout 900   4700 14000 0 true 36   850 280 2
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 17     280 160    2 true 300     160 2900    2 true 14    290 160    2 true 3.7   8.2 43    2 true 39   1600 260 2 true 36   1300 240 1 true 19   1500 210 2 true 140    1600 1800   2 true 900    15000 7100   2 timeout 900     5300 13000    0 true 28     1000 300    2 true 43     1600 590    2 unknown 17   780 160 0 true 120   340 1000 2 true .52 11   6.3 2 true 42   1100 360 2 timeout 900   4400 12000 0 true 42   1000 320 2
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 21     250 170    2 timeout 900     270 9500    0 true 14    270 150    2 true 3.7   8.2 41    2 true 21   890 160 2 true 28   970 180 1 true 22   2100 210 2 true 140    2200 1800   2 true 900    15000 7500   2 timeout 900     4800 9800    0 true 29     1000 360    2 true 45     1600 490    2 unknown 17   750 140 0 true 130   360 1200 2 true .52 12   6.7 2 true 25   1100 190 2 timeout 900   1700 12000 0 true 130   4800 1500 2
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     1400 7600    0 exception (gremlins) 4.6   35 40    0 error (42) 850    430 11000    0 true 3.3   8.3 37    1 timeout 900   6400 11000 0 timeout 900   3600 4600 0 timeout 910   4200 11000 0 unknown 890    390 9900   0 timeout 900    2800 8500   0 timeout 900     400 11000    0 timeout 900     1000 11000    0 timeout 900     1800 10000    0 unknown 20   840 180 0 true 880   580 6900 1 timeout (timeout) 900    370   9700   0 timeout 900   2400 13000 0 timeout 900   4500 14000 0 timeout 900   2700 12000 0
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     8700 9900    0 timeout 900     340 11000    0 error (42) 850    910 3600    0 true 3.3   8.3 35    2 true 56   2300 340 2 true 130   3800 1100 2 true 27   2300 270 2 true 46    2300 520   2 out of memory 410    15000 4400   0 timeout 900     4000 9800    0 timeout 900     11000 11000    0 timeout 900     15000 10000    0 unknown 20   820 180 0 true 880   630 6100 2 timeout (timeout) 900    580   10000   0 true 47   1900 460 2 timeout 900   1300 13000 0 timeout 900   4500 12000 0
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     7400 11000    0 timeout 900     330 11000    0 error (42) 850    790 4600    0 true 3.3   8.3 37    2 true 26   970 180 2 segmentation fault 39   1300 250 0 true 94   2300 1200 2 unknown 890    370 11000   0 out of memory 420    15000 4500   0 timeout 900     2400 11000    0 timeout 900     6500 11000    0 timeout 900     9700 11000    0 unknown 18   820 140 0 true 880   540 6400 2 timeout (timeout) 900    190   12000   0 true 39   1500 340 2 timeout 900   1300 12000 0 timeout 900   4700 12000 0
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     7600 9200    0 timeout 900     330 8400    0 error (42) 850    820 3600    0 true 3.2   8.3 40    2 true 25   970 200 2 true 160   4400 1400 2 true 93   2300 1100 2 unknown 890    380 11000   0 out of memory 450    15000 4800   0 timeout 900     2600 9700    0 timeout 900     6700 10000    0 timeout 900     10000 12000    0 unknown 18   820 160 0 true 880   640 6800 2 timeout (timeout) 900    160   9300   0 true 38   1600 290 2 timeout 900   1100 14000 0 timeout 900   4700 12000 0
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     8000 9700    0 true 160     87 1700    2 error (42) 850    850 3400    0 true 3.4   8.2 37    2 true 46   2200 350 2 true 190   4900 1600 2 true 25   2300 250 2 unknown 890    310 13000   0 out of memory 430    15000 5100   0 timeout 900     3700 8800    0 timeout 900     9200 9600    0 timeout 900     12000 9900    0 unknown 19   830 170 0 true 880   710 6200 2 timeout (timeout) 900    270   9800   0 true 36   1400 300 2 timeout 900   4800 13000 0 timeout 900   3600 12000 0
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     8300 11000    0 true 160     74 1700    2 error (42) 850    830 4000    0 true 3.1   8.3 34    2 true 40   2200 320 2 timeout 910   5700 7100 0 true 26   2300 270 2 unknown 890    300 12000   0 out of memory 410    15000 4300   0 timeout 900     3700 11000    0 timeout 900     3600 2000    0 timeout 900     12000 10000    0 unknown 19   800 150 0 true 880   720 6400 2 timeout (timeout) 900    270   10000   0 true 36   1500 310 2 timeout 900   4700 13000 0 timeout 900   4100 12000 0
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c true .22  38 1.7  2 false(unreach-call) 2.4   23 29    -16 true 4.2  41 47    2 true 79     120   890    2 error 4.1 300 36 0 true 87   2300 750 2 true 11   390 110 1 true 15    400 140   2 true 900    2900 12000   2 timeout 900     3800 11000    0 true 19     280 260    1 true 1.0   26 15    2 unknown 14   710 100 0 true 1.7 83 20 2 true 500    190   6200   2 witness invalid (true) 160   890 1900 0 timeout 900   1900 11000 0 witness invalid (true) 130   830 1700 0
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c true .15  26 1.6  2 exception (gremlins) 23     40 240    0 true 2.8  43 30    2 true 3.3   9.1 34    2 error 13   500 96 0 true 13   610 100 1 true 110   1300 1500 2 true 120    1200 1300   2 true 890    2900 12000   2 timeout 900     4200 12000    0 true .66  51 8.8  2 true .11  24 1.2  2 unknown 12   700 100 0 true 1.5 87 20 2 true 2.6  15   32   2 true 220   1000 2500 2 timeout 900   1300 12000 0 true 110   1500 1100 2
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c true 6.7   150 80    1 exception (gremlins) 13     39 170    0 true 2.8  42 41    1 true 3.0   8.6 35    1 error 7.7 450 59 0 segmentation fault 36   1100 270 0 true 100   1300 1500 1 true 120    1400 1500   1 true 890    2900 11000   1 timeout 900     4100 11000    0 true 2.0   53 23    1 true 7.0   210 88    1 unknown 13   710 110 0 true 11   120 140 1 true 4.4  17   66   1 timeout 900   1600 10000 0 timeout 900   1300 13000 0 timeout 900   840 12000 0
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c true .79  32 9.2  2 false(unreach-call) 5.5   29 37    -16 true 9.9  44 130    2 true 42     51   400    2 error 3.5 290 35 0 true 380   2500 3800 2 true 200   370 2500 2 true 230    360 2600   2 true 890    2900 13000   2 timeout 900     1400 12000    0 true 220     360 3200    2 true 19     38 240    2 unknown 13   710 110 0 true 16   95 200 2 timeout (timeout) 900    150   13000   0 true 510   1000 5400 2 timeout 900   2200 9900 0 witness invalid (true) 610   1900 7500 0
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c true .13  26 1.6  2 exception (gremlins) 59     48 630    0 true 2.8  52 36    2 true 2.9   8.7 29    2 error 22   720 170 0 true 8.4 430 59 1 true 110   1300 1200 2 true 110    1200 1500   2 true 900    2900 12000   2 timeout 900     3100 8700    0 true .65  47 7.9  2 true .13  24 .97 2 unknown 12   730 93 0 true 1.5 86 22 2 true 2.6  23   28   2 true 15   610 110 2 timeout 900   1400 13000 0 true 46   910 470 2
bitvector-regression/implicitfloatconversion_false-unreach-call.c false(unreach-call) .14  22 .78 1 false(unreach-call) .063 19 .65 1 false(unreach-call) .14 17 .86 1 false(unreach-call) .053 7.6 .33 1 false(unreach-call) 3.1 280 28 1 false(unreach-call) 3.4 290 31 1 false(unreach-call) 2.3 250 21 1 false(unreach-call) .38 48 3.8 1 false(unreach-call) .13 23 1.3 1 false(unreach-call) .086 23 .76 1 false(unreach-call) .071 23 .79 1 false(unreach-call) .079 23 .65 1 unknown 4.3 300 35 0 false(unreach-call) 1.5 71 16 1 false(unreach-call) .13 9.2 1.5 1 false(unreach-call) 9.1 320 69 1 error 4.8 310 38 0 false(unreach-call) 8.7 310 63 1
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) .12  24 .99 1 true .088 15 .51 -32 false(unreach-call) .14 17 .95 1 false(unreach-call) .047 7.6 .40 1 true 2.6 270 22 -32 false(unreach-call) 3.1 280 26 1 false(unreach-call) 2.5 270 20 1 false(unreach-call) .37 48 3.9 1 false(unreach-call) .14 23 1.4 1 false(unreach-call) .27  23 .72 1 false(unreach-call) .071 23 .90 1 false(unreach-call) .11  23 .74 1 false(unreach-call) 4.4 320 36 1 false(unreach-call) 1.4 73 22 1 false(unreach-call) .16 9.1 1.4 1 false(unreach-call) 5.4 320 45 1 false(unreach-call) 5.9 330 48 1 false(unreach-call) 6.4 350 52 1
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) .12  22 .82 1 true .052 17 .53 -32 false(unreach-call) .12 17 .85 1 false(unreach-call) .050 7.8 .40 1 false(unreach-call) 2.8 270 24 1 false(unreach-call) 3.1 270 27 1 false(unreach-call) 2.5 260 21 1 false(unreach-call) .35 48 4.1 1 false(unreach-call) .13 24 1.4 1 false(unreach-call) .071 23 .86 1 false(unreach-call) .10  23 .75 1 false(unreach-call) .11  23 .66 1 false(unreach-call) 4.6 340 40 1 false(unreach-call) 1.5 69 18 1 false(unreach-call) .13 9.2 1.7 1 false(unreach-call) 8.9 320 74 1 false(unreach-call) 9.8 340 70 1 false(unreach-call) 9.0 330 75 1
bitvector-regression/recHanoi03_false-unreach-call.c error (5) .12  22 .69 0 false(unreach-call) .067 20 .65 0 false(unreach-call) .97 23 11    1 aborted .19  7.8 2.5  0 error 3.0 280 26 0 error 3.1 290 22 0 false(unreach-call) 3.2 300 25 0 unknown 4.6  300 49   0 false(unreach-call) 4.1  300 51   0 false(unreach-call) 1.6   46 22    0 false(unreach-call) 2.0   83 28    0 false(unreach-call) 2.4   120 30    0 unknown 3.9 300 34 0 false(unreach-call) 8.6 78 130 1 timeout (timeout) 900    2800   12000   0 false(unreach-call) 87   880 1200 0 false(unreach-call) 110   840 1500 0 false(unreach-call) 220   810 2600 0
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) .12  22 .97 1 true .088 15 .37 -32 false(unreach-call) .12 17 .84 1 false(unreach-call) .087 7.9 .87 1 true 2.6 270 22 -32 false(unreach-call) 3.3 280 28 1 false(unreach-call) 2.5 240 25 1 false(unreach-call) 480    70 6200   1 false(unreach-call) .13 23 1.5 1 false(unreach-call) .11  23 .62 1 false(unreach-call) .073 23 .66 1 false(unreach-call) .10  23 .71 1 false(unreach-call) 4.9 310 45 1 false(unreach-call) 1.5 72 19 1 false(unreach-call) .16 9.4 1.6 1 false(unreach-call) 5.8 320 43 1 false(unreach-call) 5.6 320 43 1 false(unreach-call) 5.4 320 41 1
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) .11  22 .75 1 true .053 15 .63 -32 false(unreach-call) .13 17 .97 1 false(unreach-call) .11  7.7 .87 1 true 2.5 270 21 -32 false(unreach-call) 3.3 270 26 1 false(unreach-call) 2.4 250 20 1 false(unreach-call) .37 48 4.1 1 false(unreach-call) .15 23 1.4 1 false(unreach-call) .086 23 .91 1 false(unreach-call) .088 23 .83 1 false(unreach-call) .098 23 .83 1 false(unreach-call) 4.9 310 35 1 false(unreach-call) 1.5 70 18 1 false(unreach-call) .16 9.3 1.4 1 false(unreach-call) 6.7 330 51 1 false(unreach-call) 5.6 320 43 1 false(unreach-call) 5.3 310 43 1
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true .097 22 .77 2 false(unreach-call) .064 19 .73 -16 true .19 17 1.6  2 true .038 7.7 .35 2 true 2.6 260 25 2 true 2.7 270 21 2 true 2.1 220 19 2 true 3.2  260 29   2 true .17 23 1.3 2 timeout 900     10000 10000    0 true .27  23 .83 2 true .10  23 .63 2 true 4.5 320 35 2 true 1.2 75 17 2 true .16 9.4 1.3 2 true 5.6 330 44 2 true 6.4 330 53 2 true 5.8 330 46 2
bitvector-regression/integerpromotion_true-unreach-call.c true .11  22 .76 2 false(unreach-call) .062 17 .58 -16 true .19 17 1.6  2 true .040 7.7 .29 2 true 2.6 270 20 2 true 2.7 270 26 2 true 2.3 250 20 2 true 3.2  260 28   2 true .15 23 1.4 2 out of memory 50     15000 690    0 true .075 23 .74 2 true .11  23 .58 2 true 5.0 340 42 2 true 1.1 68 15 2 true .13 9.3 1.3 2 true 9.0 310 75 2 true 8.9 320 70 2 true 9.7 320 83 2
bitvector-regression/signextension2_true-unreach-call.c true .095 22 .74 2 false(unreach-call) .064 20 .79 -16 true .18 17 1.9  2 true .083 7.9 .88 2 true 2.6 270 26 2 true 2.7 260 23 2 true 2.2 240 19 2 true 480    270 5800   2 true .15 23 1.4 2 timeout 900     6800 14000    0 true .10  23 .87 2 true .072 23 .74 2 true 5.3 330 40 2 true 1.2 72 15 2 true .16 9.2 1.4 2 true 5.7 320 49 2 true 5.6 320 44 2 true 6.0 330 46 2
bitvector-regression/signextension_true-unreach-call.c true .11  22 .68 2 false(unreach-call) .063 16 .67 -16 true .19 17 2.0  2 true .12  7.9 .77 2 true 2.7 260 21 2 true 2.8 270 23 2 true 2.2 240 19 2 true 3.1  260 29   2 true .16 23 1.5 2 timeout 900     4900 12000    0 true .072 23 .82 2 true .11  23 .77 2 true 5.5 340 45 2 true 1.2 81 13 2 true .13 9.3 1.6 2 true 6.1 330 43 2 true 6.6 340 49 2 true 5.6 330 44 2
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) .13  24 1.1  1 false(unreach-call) 28     35 290    0 false(unreach-call) .14 18 .93 1 false(unreach-call) .54  7.7 5.5  1 true 13   580 110 -32 false(unreach-call) 6.3 370 42 1 false(unreach-call) 3.0 260 26 1 false(unreach-call) 1.2  78 17   1 false(unreach-call) 16    1000 190   1 false(unreach-call) .085 23 .90 1 false(unreach-call) .11  23 .81 1 false(unreach-call) .086 23 .97 1 unknown 5.7 350 48 0 false(unreach-call) 1.9 93 29 1 false(unreach-call) .16 9.3 1.6 1 false(unreach-call) 8.1 370 61 1 false(unreach-call) 6.4 330 50 1 false(unreach-call) 12   450 98 1
bitvector-loops/overflow_false-unreach-call1.i timeout 900     1400 11000    0 true .16  20 1.1  -32 error (1) 280    15000 3300    0 unknown .067 7.8 .23 0 true 3.0 270 28 -32 timeout 910   7100 7500 0 timeout 910   7800 9700 0 unknown 54    75 780   0 false(unreach-call) .15 23 1.5 0 timeout 900     9100 11000    0 out of memory 310     15000 3600    0 out of memory 200     15000 2200    0 unknown 4.7 330 38 0 timeout 880   930 12000 0 false(unreach-call) .13 9.3 1.7 0 timeout 900   1500 15000 0 timeout 900   980 13000 0 timeout 900   870 14000 0
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(unreach-call) .94  37 12    1 true .36  22 3.7  -32 false(unreach-call) .40 21 3.7  1 aborted .13  7.7 .97 0 true 3.2 290 29 -32 false(unreach-call) 13   500 91 1 false(unreach-call) 210   890 2500 1 false(unreach-call) 7.9  100 97   1 false(unreach-call) 2.1  220 24   1 false(unreach-call) .16  24 1.4  1 false(unreach-call) .18  25 1.9  1 false(unreach-call) 1.1   59 13    1 unknown 5.5 340 47 0 false(unreach-call) 4.7 110 62 1 false(unreach-call) .23 12   2.8 0 false(unreach-call) 160   740 2000 0 error 670   650 7500 0 false(unreach-call) 190   740 2300 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 50 15000   59000 160000 54 50 7400    8800 79000   -406 50 8300   120000 53000 57 50 2000   19000 25000   76 50 2300 37000 28000 -150 50 5800 73000 45000 67 50 6400   66000 69000 75 50 15000 24000 160000 54 50 14000   200000 150000 46 50 28000   280000 320000 10 50 11000   180000 110000 48 50 12000   170000 120000 53 50 460 25000 3900 12 50 17000 12000 170000 78 50 15000   67000 180000 50 50 14000 46000 180000 56 50 29000 76000 380000 27 50 17000   59000 220000 43
    correct results 32 110   1900 1000 53 6 890    470 8800   9 34 460   3100 3000 56 41 200   1100 2200   73 23 330 17000 2400 42 37 1800 37000 14000 63 42 1700   35000 21000 73 32 3900 17000 47000 53 35 8100   87000 94000 60 10 15   490 120 10 28 510   5100 6600 46 31 640   7400 7800 52 8 39 2600 320 12 43 11000 9200 110000 74 28 780   550 9700 49 33 2200 26000 24000 56 17 710 10000 7800 27 26 1100   21000 11000 42
        correct true 21 47   1100 440 42 3 620    320 6300   6 22 450   2400 2900 44 32 200   1000 2200   64 19 290 14000 2100 38 26 1600 29000 13000 52 31 1400   29000 17000 62 21 3300 17000 39000 42 25 6200   54000 73000 50 0 18 490   4200 6400 36 21 610   6000 7400 42 4 20 1300 160 8 31 11000 7800 110000 62 21 780   480 9700 42 23 2100 22000 23000 46 10 560 7300 6300 20 16 880   16000 8800 32
        correct false 11 64   850 580 11 3 270    160 2600   3 12 11   640 140 12 9 1.0 71 9.0 9 4 38 2000 290 4 11 190 8300 1300 11 11 330   5400 3900 11 11 600 850 7900 11 10 1900   33000 21000 10 10 15   490 120 10 10 18   920 230 10 10 30   1500 430 10 4 19 1300 160 4 12 90 1400 1100 12 7 1.2 66 12 7 10 170 4600 1500 10 7 150 3000 1500 7 10 210   4800 2000 10
    correct-unconfimed results 1 6.7 150 80 1 4 31    110 310   1 1 2.8 42 41 1 4 7.6 65 83   3 1 18 740 140 0 4 86 3300 580 4 3 120   2000 1600 2 1 120 1400 1500 1 5 900   3400 11000 2 2 1.7 70 23 0 4 23   440 320 2 3 9.5 360 120 1 0 4 2700 1200 27000 4 6 5.8 72 83 1 2 250 1600 3200 0 1 110 840 1500 0 3 420   1900 5000 1
        correct-unconfirmed true 1 6.7 150 80 1 1 1.9  22 19   1 1 2.8 42 41 1 3 6.5 25 74   3 0 4 86 3300 580 4 2 110   1700 1600 2 1 120 1400 1500 1 2 890   2900 11000 2 0 2 21   330 290 2 1 7.0 210 88 1 0 4 2700 1200 27000 4 1 4.4 17 66 1 0 0 1 7.2 360 59 1
        correct-unconfirmed false 0 3 29    90 300   0 0 1 1.1 41 9.2 0 1 18 740 140 0 0 1 3.2 300 25 0 0 3 6.5 470 76 0 2 1.7 70 23 0 2 2.1 110 30 0 2 2.5 140 32 0 0 0 5 1.4 55 17 0 2 250 1600 3200 0 1 110 840 1500 0 2 410   1500 4900 0
    incorrect results 0 20 48    420 560   -416 0 0 6 27 1900 230 -192 0 0 0 1 2.6 150 34 -16 0 0 0 0 0 0 0 0 0
        incorrect true 0 6 .80 100 6.8 -192 0 0 6 27 1900 230 -192 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 14 47    320 550   -224 0 0 0 0 0 0 1 2.6 150 34 -16 0 0 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 54 -406 57 76 -150 67 75 54 46 10 48 53 12 78 50 56 27 43
Run set 2ls.sv-comp17.ReachSafety-BitVectors blast.sv-comp17.ReachSafety-BitVectors cbmc.sv-comp17.ReachSafety-BitVectors ceagle.sv-comp17.ReachSafety-BitVectors cpa-bam-bnb.sv-comp17.ReachSafety-BitVectors cpa-kind.sv-comp17.ReachSafety-BitVectors cpa-seq.sv-comp17.ReachSafety-BitVectors depthk.sv-comp17.ReachSafety-BitVectors esbmc.sv-comp17.ReachSafety-BitVectors esbmc-falsi.sv-comp17.ReachSafety-BitVectors esbmc-incr.sv-comp17.ReachSafety-BitVectors esbmc-kind.sv-comp17.ReachSafety-BitVectors skink.sv-comp17.ReachSafety-BitVectors smack.sv-comp17.ReachSafety-BitVectors symbiotic4.sv-comp17.ReachSafety-BitVectors uautomizer.sv-comp17.ReachSafety-BitVectors ukojak.sv-comp17.ReachSafety-BitVectors utaipan.sv-comp17.ReachSafety-BitVectors