Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 skink symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741 VeriAbs
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-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-11-30 11:20:26 CET 2017-11-30 16:01:31 CET 2017-12-01 08:49:27 CET 2017-12-01 12:59:33 CET 2017-12-01 19:00:34 CET 2017-12-01 19:46:39 CET 2017-12-01 22:03:39 CET 2017-12-01 22:41:19 CET 2017-12-02 01:06:24 CET 2017-12-02 02:33:02 CET 2017-12-02 17:23:13 CET 2017-12-02 18:04:04 CET
Run set 2ls.sv-comp18.ReachSafety-BitVectors cbmc.sv-comp18.ReachSafety-BitVectors cpa-bam-bnb.sv-comp18.ReachSafety-BitVectors cpa-bam-slicing.sv-comp18.ReachSafety-BitVectors cpa-seq.sv-comp18.ReachSafety-BitVectors depthk.sv-comp18.ReachSafety-BitVectors esbmc-incr.sv-comp18.ReachSafety-BitVectors esbmc-kind.sv-comp18.ReachSafety-BitVectors interpchecker.sv-comp18.ReachSafety-BitVectors map2check.sv-comp18.ReachSafety-BitVectors skink.sv-comp18.ReachSafety-BitVectors symbiotic.sv-comp18.ReachSafety-BitVectors uautomizer.sv-comp18.ReachSafety-BitVectors ukojak.sv-comp18.ReachSafety-BitVectors utaipan.sv-comp18.ReachSafety-BitVectors veriabs.sv-comp18.ReachSafety-BitVectors
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions --witness witness.graphml --full-output --full-output --full-output
../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
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i .32  28 3.8  1 .70 34 6.7 1 11   470 87 0 12   500 89 0 17   440 180 1 2.2  110 33   1 1.1   29 10    1 1.2   29 14    1 6.7 410 60 0 1.3  13 15   1 47   730 600 0 .31 12 4.0 1 85   880 880 1 31   490 280 1 110   1500 940 1 29   430 260 1
bitvector/sum02_false-unreach-call_true-no-overflow.i 900     1400 10000    0 870    6000 3300   0 3.6 290 32 0 3.3 290 30 0 910   7700 10000 0 70    75 990   0 900     780 11000    0 900     780 11000    0 3.9 270 30 0 900    700 13000   0 110   730 1500 0 900    790 13000   0 14   380 140 0 900   680 10000 0 900   700 11000 0 470   3100 3700 0
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i .33  29 4.3  2 .86 34 8.1 1 9.5 480 75 0 12   530 88 0 12   440 100 2 74    1700 820   2 .18  27 1.6  2 .16  27 1.9  2 9.6 470 72 -16 4.1  13 56   2 35   700 370 0 .32 12 3.9 2 900   1400 12000 0 720   1600 7700 2 900   2600 12000 0 29   570 210 2
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i .34  31 3.7  2 .85 34 8.5 1 13   520 100 0 12   500 95 0 13   470 120 2 28    910 330   2 .17  27 2.0  2 .15  27 1.8  2 8.8 460 68 -16 4.1  13 54   2 31   710 360 0 .35 12 4.0 2 900   1400 10000 0 900   1500 7600 0 900   3100 12000 0 27   480 180 2
bitvector/gcd_1_true-unreach-call_true-no-overflow.i .25  27 2.6  2 .53 36 5.7 1 7.4 310 90 0 5.3 310 56 0 6.8 280 76 2 490    310 7300   2 .97  29 12    2 .38  27 4.3  2 900   2400 11000 0 .64 12 7.9 2 84   950 730 0 .42 12 5.0 2 900   630 13000 0 660   670 4700 0 900   1000 12000 0 21   300 190 2
bitvector/gcd_2_true-unreach-call_true-no-overflow.i .76  39 9.0  2 2.0  42 24   1 3.9 280 31 2 3.7 280 37 2 7.6 280 83 2 230    280 3000   2 27     45 330    2 37     44 420    2 4.5 270 38 -16 28    20 340   2 27   900 250 2 9.8  15 130   2 900   670 12000 0 900   520 11000 0 900   1100 11000 0 53   400 590 2
bitvector/gcd_3_true-unreach-call_true-no-overflow.i .64  40 7.4  2 2.0  42 26   1 5.3 300 49 0 3.5 300 35 0 150   310 2000 2 470    330 5000   2 30     43 370    2 37     45 460    2 3.5 280 32 -16 30    18 380   2 82   870 1200 0 9.4  15 120   2 900   2800 11000 0 900   500 12000 0 510   1200 4100 0 52   410 630 2
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i .56  33 6.0  2 .76 33 9.5 2 3.3 270 32 2 3.2 270 27 2 2.5 260 20 2 490    260 6000   2 .082 27 .78 2 .53  32 8.1  2 8.9 460 71 -16 .36 11 3.6 2 25   700 260 2 .17 11 1.6 2 56   520 590 2 11   580 97 2 240   900 2800 2 17   320 120 2
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i .48  55 5.6  2 1.6  33 14   2 5.9 380 49 0 3.5 290 34 0 7.4 450 75 2 16    410 190   2 .099 26 1.1  2 .12  26 1.2  2 7.6 450 59 -16 .34 11 4.0 2 7.6 370 66 2 .16 12 2.0 2 170   3800 2500 2 100   2600 1100 2 230   1800 3100 2 18   330 120 2
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 900     1500 10000    0 870    970 7200   0 3.0 270 26 2 2.9 270 24 2 3.1 270 28 2 300    290 2800   0 900     1200 9800    0 900     1300 13000    0 3.0 280 29 2 900    89 6500   0 20   690 190 2 900    75 8700   0 4.7 290 40 2 900   1700 12000 0 4.6 290 39 2 370   4800 4000 0
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 900     1500 11000    0 870    1300 5200   0 3.2 280 28 2 3.1 270 28 2 3.2 280 26 2 890    260 7900   0 900     830 10000    0 900     840 12000    0 2.9 270 25 2 900    190 9700   0 26   730 320 2 900    94 8500   0 4.9 290 40 2 16   330 170 2 4.7 290 40 2 510   4300 6100 0
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 900     1900 11000    0 870    1700 6900   0 3.2 270 25 2 3.1 270 29 2 3.3 280 29 2 900    270 11000   0 900     750 9700    0 900     780 11000    0 900   5500 12000 0 900    120 12000   0 4.5 260 38 2 900    15000 13000   0 4.9 290 38 2 6.2 320 50 2 4.8 290 44 2 620   5700 6900 0
bitvector/jain_5_true-unreach-call_true-no-overflow.i 900     1400 13000    0 380    15000 4800   0 900   3900 10000 0 900   3900 11000 0 900   3500 9800 0 59    75 740   0 900     11000 10000    0 900     11000 12000    0 900   4300 12000 0 890    11 11000   0 4.0 320 35 1 900    15000 12000   0 900   700 11000 0 900   5200 13000 0 6.3 310 53 1 8.0 220 63 1
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 900     1800 10000    0 870    1600 4300   0 3.2 280 32 2 3.2 270 29 2 3.4 280 29 2 900    330 7100   0 900     750 9100    0 900     750 8900    0 900   5500 13000 0 890    110 11000   0 4.0 250 39 2 900    15000 13000   0 20   310 230 2 900   2100 10000 0 8.0 300 86 2 620   5400 6600 0
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 900     1700 11000    0 870    1700 5900   0 3.2 280 30 2 3.1 270 27 2 4.6 280 52 2 900    370 8800   0 900     1000 9700    0 900     1000 9300    0 900   5700 12000 0 890    120 11000   0 4.1 250 43 2 900    15000 14000   0 4.9 290 38 2 900   2900 13000 0 5.1 290 44 2 510   5100 6800 0
bitvector/modulus_true-unreach-call_true-no-overflow.i .63  39 8.9  2 460    1100 2100   2 18   310 240 0 3.9 300 34 0 220   2100 2400 2 890    380 7900   0 180     280 2100    2 200     330 2200    2 2.8 270 25 -16 790    63 9900   2 46   730 530 0 640    57 8600   2 14   410 140 2 110   660 1500 2 13   500 110 2 30   610 290 2
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i .12  24 1.2  2 1.2  33 11   2 3.3 280 34 2 3.1 270 29 2 2.4 250 20 2 7.0  260 89   2 .090 26 .92 2 .13  26 .91 2 5.5 290 41 -16 .32 11 3.6 2 3.9 240 37 2 .17 11 1.6 2 270   3300 3300 2 120   470 1700 2 59   670 670 2 16   290 110 2
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i .17  24 1.2  2 1.2  33 12   1 900   330 12000 0 3.4 290 35 0 16   470 140 2 22    550 270   2 .12  26 .88 2 .14  26 .98 2 5.8 310 47 -16 .27 11 4.2 0 5.3 300 47 2 .17 12 2.0 2 900   1300 8800 0 240   780 2900 2 900   1300 12000 0 16   310 140 2
bitvector/parity_true-unreach-call_true-no-overflow.i 2.7   44 30    2 4.1  35 44   1 3.5 290 29 0 3.0 280 27 0 120   980 1400 2 890    150 11000   0 7.0   28 93    2 9.4   33 130    2 2.9 280 25 -16 9.4  13 130   2 150   740 1800 0 7.4  13 99   2 900   1000 12000 0 900   720 13000 0 900   1000 12000 0 32   340 330 2
bitvector/sum02_true-unreach-call_true-no-overflow.i 900     1500 12000    0 880    6300 4400   0 3.4 290 31 0 3.2 290 29 0 910   7000 8100 0 170    480 1700   0 900     760 12000    0 900     740 11000    0 3.7 280 29 -16 900    700 12000   0 130   770 1800 0 900    770 9900   0 900   560 11000 0 900   740 11000 0 900   650 11000 0 390   3200 3100 0
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 9.4   220 77    1 5.9  220 76   1 900   4400 12000 0 21   750 160 1 8.6 320 68 1 34    100 370   1 5.9   87 60    1 4.0   76 42    1 90   3900 920 1 67    19 870   -32 82   780 980 0 .42 13 4.7 1 24   710 180 1 900   6300 13000 0 26   580 210 1 59   420 590 1
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 7.3   240 83    1 5.2  180 70   1 27   1100 210 1 23   1000 160 1 26   810 260 1 55    110 790   1 6.1   96 63    1 7.4   110 79    1 67   3000 500 1 150    42 2200   0 45   720 530 0 .61 14 8.0 1 27   650 210 1 900   6200 13000 0 27   690 210 1 150   880 1700 1
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 7.3   150 67    1 1.5  64 18   1 6.9 400 66 0 7.8 460 72 1 6.1 300 52 1 18    85 220   1 2.6   58 26    1 2.3   51 23    1 7.2 440 59 0 4.1  15 53   -32 39   710 470 0 .28 12 3.5 1 23   580 170 1 88   1000 1100 1 24   610 190 1 130   790 1400 1
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 46     320 410    2 21    360 240   2 900   4400 10000 0 21   720 130 0 15   750 160 2 170    1300 2000   2 22     190 260    2 25     210 240    2 85   3900 870 -16 890    42 11000   0 100   840 1300 0 .59 13 7.6 2 41   1300 380 2 900   6300 11000 0 39   1100 330 2 93   750 900 2
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 8.0   280 95    2 18    290 240   2 38   2000 260 2 36   1700 270 2 14   730 120 2 140    1600 1700   2 11     160 130    2 13     170 120    2 62   3000 570 -16 890    43 11000   0 89   760 940 0 .62 13 6.8 2 43   1900 360 2 900   6300 12000 0 45   1400 360 2 170   900 1800 1
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 9.1   250 84    2 18    280 220   2 27   1100 210 2 23   890 150 2 15   750 160 2 140    1300 2100   2 10     150 110    2 12     160 160    2 94   3800 950 2 890    43 11000   0 54   720 650 0 .62 13 6.4 2 25   1000 190 2 900   6000 13000 0 270   4800 3700 2 160   790 1700 1
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 900     810 9700    0 870    460 8600   0 900   6700 9000 0 900   5200 10000 0 900   4200 8900 0 890    390 7100   0 900     360 11000    0 900     290 11000    0 900   4400 14000 0 .38 12 5.3 0 900   1400 9200 0 900    400 11000   0 900   2100 13000 0 900   6400 12000 0 900   5100 12000 0 550   1000 6400 0
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 900     7600 9900    0 870    940 3500   0 11   510 86 2 41   1800 330 2 17   760 150 2 46    2300 550   2 900     2300 8400    0 900     2400 11000    0 42   2500 400 2 .41 12 4.8 0 62   730 610 0 900    1100 12000   0 53   2200 490 2 900   6500 11000 0 230   4700 2500 2 900   1300 5000 0
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c 900     6700 10000    0 870    800 3200   0 11   500 87 2 20   790 150 2 51   1300 560 2 890    360 11000   0 900     2100 12000    0 900     2100 8500    0 120   3500 1400 2 890    110 13000   0 16   660 130 0 900    130 11000   0 40   1800 350 2 910   6500 11000 0 900   5400 14000 0 900   1400 7400 0
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c 900     6800 11000    0 870    840 5800   0 12   520 95 2 20   790 160 2 56   2400 630 2 890    370 12000   0 900     2100 8300    0 900     2000 10000    0 120   3500 1400 2 900    130 12000   0 12   640 100 0 900    220 10000   0 41   1800 350 2 900   6400 10000 0 900   5000 12000 0 900   1400 7500 0
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 900     7100 10000    0 870    860 5600   0 900   4100 11000 0 43   1700 310 2 17   760 160 2 900    300 11000   0 900     1800 9500    0 900     1700 9600    0 110   3400 1200 2 900    170 9500   0 79   980 990 0 900    210 11000   0 40   1500 390 2 900   6400 11000 0 250   4800 2900 2 900   1300 5600 0
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 900     7000 9700    0 870    840 5600   0 900   4100 11000 0 42   2000 280 2 16   770 170 2 890    300 11000   0 900     1800 12000    0 900     1700 11000    0 74   3000 740 2 890    160 11000   0 15   650 130 0 900    210 13000   0 39   1500 330 2 900   6500 11000 0 230   4800 2800 2 900   1200 5800 0
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c .22  28 2.0  2 6.1  54 72   2 5.0 320 47 0 3.7 290 37 0 12   380 130 2 14    390 150   2 4.3   34 52    2 .35  28 4.4  2 12   630 92 -16 900    220 12000   0 17   650 140 0 680    160 9200   2 110   850 1200 0 900   1700 11000 0 110   870 1400 0 98   820 960 2
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c .17  29 1.4  2 4.5  54 63   2 5.5 300 43 0 7.4 400 59 0 110   1300 1300 2 120    1200 1300   2 .65  32 7.4  2 .37  29 3.7  2 8.0 450 62 -16 900    150 11000   0 20   680 180 0 2.8  15 38   2 26   750 210 2 900   1500 10000 0 84   1300 830 2 40   780 420 1
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c 4.0   160 48    1 4.6  53 63   1 5.2 300 41 0 7.0 490 56 0 100   1300 1100 1 120    1200 1500   1 .47  30 5.5  1 .71  30 7.9  1 8.6 450 71 -16 900    200 11000   0 19   660 170 0 4.7  18 62   1 900   890 9600 0 900   1400 11000 0 900   1100 10000 0 85   740 850 1
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c 1.1   36 12    2 12    52 160   2 4.6 320 41 0 3.4 290 31 0 170   400 2400 2 230    380 3200   2 23     35 310    2 1.8   29 21    2 900   3100 13000 0 900    230 11000   0 18   640 180 0 900    45 12000   0 490   910 6400 0 900   1500 12000 0 860   940 11000 2 100   810 1100 2
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c .17  28 1.3  2 4.6  53 53   2 5.6 320 48 0 6.6 360 52 0 110   1200 1400 2 120    1200 1500   2 .67  32 8.5  2 .36  29 3.8  2 13   580 97 -16 890    150 10000   0 22   700 200 0 2.7  16 35   2 22   680 210 2 900   1600 12000 0 63   1200 620 2 40   740 390 1
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c .090 22 1.2  1 .23 33 1.7 1 3.1 280 27 1 3.0 280 24 1 2.5 250 22 1 .35 48 4.3 1 .11  28 .83 1 .082 28 .86 1 3.0 280 30 1 .31 11 3.8 1 4.9 300 46 1 .14 11 1.6 1 8.0 240 58 1 8.1 240 70 1 8.3 240 67 1 7.5 300 63 1
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c .099 22 .83 1 .23 33 1.6 1 2.8 270 24 -32 2.8 270 25 -32 2.8 270 27 1 .38 48 4.4 1 .11  28 .85 1 .10  28 .91 1 2.9 260 24 -32 .29 11 3.1 1 4.9 290 41 1 .16 11 1.7 1 4.0 240 39 1 4.2 240 39 1 4.0 240 37 1 7.6 300 61 1
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c .12  22 .82 1 .23 33 2.0 1 3.1 280 26 1 2.9 270 27 1 2.5 250 21 1 .38 48 4.2 1 .13  28 1.1  1 .13  28 1.2  1 2.8 280 23 1 .31 11 4.0 1 4.7 290 45 1 .14 11 1.4 1 8.0 240 64 1 8.2 240 74 1 9.6 320 76 1 7.3 270 62 1
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c .11  22 .64 0 2.4  34 22   1 3.3 290 30 0 3.2 280 31 0 64   1600 700 1 4.6  300 46   0 .75  28 8.6  1 .74  28 11    1 2.9 280 26 0 1.9  12 26   1 3.8 240 35 0 900    2500 11000   0 210   1300 2900 1 120   1000 1500 1 290   1200 4000 1 7.1 160 57 0
bitvector-regression/signextension2_false-unreach-call_true-termination.c .13  22 .83 1 .27 33 2.2 1 2.8 270 25 -32 2.7 270 25 -32 2.6 250 25 1 480    70 5800   1 .091 28 .91 1 .11  28 .64 1 2.8 270 27 -32 .32 11 4.0 1 5.0 300 45 1 .13 11 1.7 1 4.0 230 36 1 4.1 250 40 1 4.4 250 34 1 7.7 300 61 1
bitvector-regression/signextension_false-unreach-call_true-termination.c .12  22 .77 1 .24 33 2.5 1 2.8 270 27 -32 2.9 270 25 -32 2.5 260 26 1 .39 48 4.2 1 .080 28 .96 1 .078 28 .85 1 2.8 270 23 -32 .32 11 4.0 1 4.9 300 44 1 .16 11 1.5 1 4.1 240 36 1 4.2 250 36 1 4.1 250 34 1 7.2 280 61 1
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c .10  22 .82 2 .42 33 3.2 2 2.8 270 25 2 2.6 260 25 2 2.6 270 24 2 3.1  260 29   2 .070 26 .89 2 .071 26 .80 2 2.8 280 28 -16 .26 11 3.0 0 3.6 230 34 2 .12 11 1.3 2 4.5 270 38 2 4.2 250 38 2 4.3 270 37 2 7.7 270 71 2
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c .12  22 .84 2 .40 33 4.6 2 3.0 270 25 2 2.8 270 25 2 2.4 250 22 2 3.2  250 28   2 .089 26 .69 2 .076 26 .87 2 2.8 280 25 -16 .30 11 3.4 0 3.7 230 36 2 .15 11 1.4 2 8.7 280 67 2 8.3 250 64 2 8.9 290 70 2 7.8 260 67 2
bitvector-regression/signextension2_true-unreach-call_true-termination.c .12  22 .74 2 .40 33 4.3 2 2.8 270 24 2 2.7 270 23 2 2.3 240 18 2 480    250 6100   2 .072 26 .81 2 .078 26 .77 2 2.9 270 28 -16 .26 11 3.2 0 3.7 220 31 2 .12 11 1.5 2 4.5 280 35 2 4.5 260 36 2 4.7 290 39 2 8.1 270 69 2
bitvector-regression/signextension_true-unreach-call_true-termination.c .12  22 .76 2 .41 33 4.2 2 2.9 270 25 2 2.8 270 29 2 2.3 250 20 2 3.0  250 31   2 .097 26 .74 2 .097 26 .84 2 2.9 280 24 -16 .29 11 3.1 0 3.9 240 33 2 .15 11 1.5 2 4.8 290 37 2 4.4 260 34 2 4.7 290 41 2 8.0 260 71 2
bitvector-loops/diamond_false-unreach-call2.i .12  24 1.1  1 .25 33 2.3 1 9.8 480 78 -32 14   600 100 -32 5.3 280 46 1 1.2  77 14   1 .55  28 4.8  1 .60  28 4.8  1 34   1900 270 -32 .42 11 4.6 1 5.6 320 50 1 .16 11 2.0 1 7.2 340 63 1 5.9 300 52 1 13   550 110 1 23   430 190 1
bitvector-loops/overflow_false-unreach-call1.i 900     1300 11000    0 310    15000 4300   0 3.1 280 27 -32 3.3 270 33 -32 900   6800 9300 0 54    75 710   0 900     11000 11000    0 900     11000 12000    0 2.8 280 29 -32 890    11 13000   0 4.9 300 41 1 .16 11 1.6 1 900   710 12000 0 900   2000 11000 0 900   1500 9700 0 11   280 84 1
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i .54  37 6.0  1 1.0  34 8.9 0 3.4 280 31 -32 3.2 270 28 -32 210   1400 2700 1 8.0  100 100   0 2.1   30 18    0 2.1   29 20    0 7.2 450 62 -32 2.7  14 35   -32 13   460 130 0 .41 13 5.3 0 470   780 5400 1 900   4600 13000 0 550   2000 8400 0 19   280 160 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
total 50 14000   52000 160000 56 50 13000   58000 82000   49 50 6600   45000 78000 -155 50 2300   33000 24000 -149 50 6200 57000 66000 77 50 15000   22000 160000 53 50 14000    40000 160000   56 50 14000    40000 160000   56 50 7400 77000 97000 -508 50 20000   4200 250000 -68 50 2500   29000 28000 36 50 16000    67000 200000   54 50 13000 48000 160000 58 50 28000 110000 340000 33 50 16000   72000 200000 56 50 10000 56000 91000 53
    correct results 33 98   2200 930 55 26 560   3200 3400   41 20 170   9500 1300 37 24 320   16000 2400 43 44 1600 27000 18000 76 31 3900   16000 49000 52 33 330    1800 4000   55 33 350    1900 4000   55 12 730 28000 7600 20 18 880   280 11000 28 21 180   7700 1700 35 32 1400    590 18000   53 35 1800 31000 20000 58 21 1600 12000 19000 33 33 3200   38000 38000 55 29 1100 13000 11000 47
        correct true 22 72   1400 690 44 15 550   2400 3200   30 17 140   7900 1100 34 19 260   13000 2000 38 32 1200 20000 14000 64 21 3300   16000 42000 42 22 320    1300 3800   44 22 340    1400 3800   44 8 570 20000 6100 16 10 870   190 11000 20 14 140   5600 1400 28 21 1400    460 18000   42 23 940 25000 10000 46 12 1300 8300 15000 24 22 2700   31000 32000 44 18 640 7800 6200 36
        correct false 11 26   800 240 11 11 17   740 210   11 3 33   1700 260 3 5 58   2800 440 5 12 350 6400 4100 12 10 590   740 7200 10 11 18    460 180   11 11 17    460 180   11 4 160 7400 1500 4 8 5.2 92 65 8 7 35   2100 310 7 11 2.7  130 32   11 12 880 6500 10000 12 9 270 4100 3200 9 11 520   6400 6000 11 11 440 4700 4500 11
    correct-unconfimed results 1 4.0 160 48 1 9 17   340 200   8 1 3.3 290 30 0 1 3.2 280 31 0 1 100 1300 1100 1 2 130   1300 1600 1 2 2.6  60 24   1 2 2.8  60 28   1 4 21 1400 170 0 0 2 17   770 170 1 2 5.1  31 67   1 0 0 2 560   2300 8500 1 7 530 4400 5300 6
        correct-unconfirmed true 1 4.0 160 48 1 8 16   310 190   8 0 0 1 100 1300 1100 1 1 120   1200 1500 1 1 .47 30 5.5 1 1 .71 30 7.9 1 0 0 1 4.0 320 35 1 1 4.7  18 62   1 0 0 1 6.3 310 53 1 6 510 4200 5200 6
        correct-unconfirmed false 0 1 1.0 34 8.9 0 1 3.3 290 30 0 1 3.2 280 31 0 0 1 8.0 100 100 0 1 2.1  30 18   0 1 2.1  29 20   0 4 21 1400 170 0 0 1 13   460 130 0 1 .41 13 5.3 0 0 0 1 550   2000 8400 0 1 19 280 160 0
    incorrect results 0 0 6 25   1900 210 -192 6 29   2000 240 -192 0 0 0 0 27 320 17000 2800 -528 3 74   47 960 -96 0 0 0 0 0 0
        incorrect true 0 0 6 25   1900 210 -192 6 29   2000 240 -192 0 0 0 0 6 52 3400 440 -192 3 74   47 960 -96 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 21 260 14000 2400 -336 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 56 49 -155 -149 77 53 56 56 -508 -68 36 54 58 33 56 53
Run set 2ls.sv-comp18.ReachSafety-BitVectors cbmc.sv-comp18.ReachSafety-BitVectors cpa-bam-bnb.sv-comp18.ReachSafety-BitVectors cpa-bam-slicing.sv-comp18.ReachSafety-BitVectors cpa-seq.sv-comp18.ReachSafety-BitVectors depthk.sv-comp18.ReachSafety-BitVectors esbmc-incr.sv-comp18.ReachSafety-BitVectors esbmc-kind.sv-comp18.ReachSafety-BitVectors interpchecker.sv-comp18.ReachSafety-BitVectors map2check.sv-comp18.ReachSafety-BitVectors skink.sv-comp18.ReachSafety-BitVectors symbiotic.sv-comp18.ReachSafety-BitVectors uautomizer.sv-comp18.ReachSafety-BitVectors ukojak.sv-comp18.ReachSafety-BitVectors utaipan.sv-comp18.ReachSafety-BitVectors veriabs.sv-comp18.ReachSafety-BitVectors