Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux Map2Check v7.2-Flock : Tue Nov 27 22:00:00 -04 2018 PeSCo 1.7-svn b8d6131600+ Pinaka 0.1 skink 2.0 SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a VeriAbs 1.3.10 VeriFuzz 1.0.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:20:21 CET 2018-12-06 12:44:04 CET 2018-12-06 20:14:43 CET 2018-12-07 12:00:55 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET 2018-12-10 16:50:17 CET 2018-12-09 02:47:33 CET
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cbmc.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-BitVectors depthk.sv-comp19_prop-reachsafety.ReachSafety-BitVectors divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-BitVectors map2check.sv-comp19_prop-reachsafety.ReachSafety-BitVectors pesco.sv-comp19_prop-reachsafety.ReachSafety-BitVectors pinaka.sv-comp19_prop-reachsafety.ReachSafety-BitVectors skink.sv-comp19_prop-reachsafety.ReachSafety-BitVectors smack.sv-comp19_prop-reachsafety.ReachSafety-BitVectors symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer.sv-comp19_prop-reachsafety.ReachSafety-BitVectors ukojak.sv-comp19_prop-reachsafety.ReachSafety-BitVectors utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors veriabs.sv-comp19_prop-reachsafety.ReachSafety-BitVectors verifuzz.sv-comp19_prop-reachsafety.ReachSafety-BitVectors
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s --graphml-witness witness.graphml -w error-witness.graphml --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 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 false(unreach-call) .36  24 3.7  1 false(unreach-call) .17  9.5 1.4  1 false(unreach-call) .64  37   8.0  1 false(unreach-call) 19   480 200 1 false(unreach-call) .74 36 8.9 1 unknown 8.2 430 140 0 false(unreach-call) 29   440 320 0 false(unreach-call) .13  27 1.1  1 false(unreach-call) 140    110 1800   1 false(unreach-call) 21 1200 140 1 false(unreach-call) .38 59 3.2 1 unknown 680   5700 11000 0 disqualified 13   170 170 0 false(unreach-call) .35 19 4.1 1 false(unreach-call) 150   830 1600 1 false(unreach-call) 37   480 390 1 false(unreach-call) 180   840 2000 1 false(unreach-call) 28   310 250 1 false(unreach-call) 4.2 160 43 1
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 900     1400 12000    0 error (42) 880     5300   4000    0 error (42) 880     110   13000    0 timeout 970   6100 8600 0 unknown 160    81 2300   0 unknown 8.1 430 110 0 timeout 900   450 7900 0 timeout 900     910 12000    0 false(unreach-call) 5.4  82 61   1 timeout 960 7300 9500 0 timeout 900    520 5000   0 unknown 160   1200 2100 0 disqualified 880   440 11000 0 timeout (verification) 900    370 11000   0 unknown 18   370 200 0 timeout 900   750 12000 0 unknown 12   390 110 0 unknown 530   1400 5200 0 false(unreach-call) 12   150 150 1
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .36  24 3.8  2 true .11  6.7 1.1  1 true .30  12   3.6  1 true 14   500 130 2 unknown 2.3  68 27   0 unknown 8.2 430 110 0 true 25   380 230 2 true .26  27 3.2  2 unknown 1.6  49 17   0 true 24 1300 160 1 true .52 59 5.4 2 unknown 650   5700 11000 0 disqualified 35   190 500 0 true .37 18 4.5 2 timeout 900   1000 14000 0 true 490   1300 6200 2 timeout 900   1000 13000 0 true 79   760 780 2 timeout 900   160 12000 0
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .34  24 4.1  2 true .10  6.4 1.1  1 true .33  12   4.4  1 true 15   450 140 2 unknown 2.3  67 28   0 unknown 8.4 430 110 0 true 27   380 280 2 true .28  27 3.7  2 unknown 1.5  48 22   0 true 23 1300 170 1 true .53 60 4.8 2 unknown 660   5700 8500 0 disqualified 43   190 520 0 true .36 18 4.3 2 timeout 900   1000 11000 0 timeout 900   1700 9400 0 timeout 900   1000 12000 0 true 77   850 720 2 timeout 900   160 11000 0
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .24  24 2.5  2 true .24  8.8 2.2  1 true .28  9.9 3.7  1 true 9.0 300 92 2 unknown 5.3  75 67   0 unknown 8.2 430 99 0 true 14   380 160 2 true .87  28 11    2 true 3.2  75 41   2 true 16 1100 130 2 true .48 60 5.2 2 unknown 250   930 2400 0 disqualified 2.6 78 36 0 true .51 21 7.2 2 timeout 900   570 12000 0 true 71   450 810 2 timeout 900   1400 7900 0 true 55   520 690 2 timeout 900   150 12000 0
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true .68  27 8.5  2 true .83  21   13    1 true 3.6   26   50    1 true 9.8 310 110 2 unknown 65    77 890   0 unknown 8.3 430 110 0 timeout 900   520 8100 0 true 26     46 340    2 timeout 900    4200 8900   0 true 150 1500 1700 2 true 5.9  680 76   2 true 49   950 430 2 disqualified 880   160 13000 0 true 26    42 350   2 timeout 900   740 11000 0 timeout 900   650 14000 0 timeout 900   1200 11000 0 true 81   520 910 2 timeout 900   150 12000 0
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true .67  25 8.1  2 true .86  21   9.7  1 true 3.7   25   52    1 true 94   320 1200 2 unknown 67    76 840   0 unknown 8.1 430 96 0 timeout 900   530 9500 0 true 28     43 430    2 timeout 900    4300 11000   0 true 130 1500 1200 2 true 5.9  690 85   2 unknown 130   990 1300 0 disqualified 880   440 9900 0 true 33    42 530   2 timeout 900   1300 10000 0 timeout 900   1000 12000 0 timeout 900   8700 8700 0 true 81   780 1000 2 timeout 900   150 13000 0
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .34  23 3.8  2 true .064 6.5 .50 2 true .063 6.3 .41 2 true 2.8 250 27 2 unknown 3.8  68 48   0 true 7.9 370 100 2 true 8.0 370 99 2 true .53  32 6.9  2 timeout 900    85 12000   0 true 11 1200 80 2 true .37 58 3.2 2 true 29   770 290 2 disqualified 2.6 82 30 0 true .16 15 1.5 2 true 58   710 670 2 true 15   640 130 2 timeout 900   2300 11000 0 true 57   700 600 2 timeout 900   150 12000 0
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .47  44 5.3  2 true .16  6.3 .86 2 true .12  6.8 1.2  2 true 9.1 480 76 2 unknown 4.9  68 59   0 unknown 8.2 430 87 0 unknown 8.2 430 100 0 true .11  26 1.2  2 timeout 900    4200 10000   0 true 16 1300 130 2 true .39 58 2.9 2 true 12   380 100 2 disqualified 3.2 84 44 0 true .17 18 2.1 2 true 140   700 1800 2 true 40   690 440 2 true 140   710 1700 2 true 64   680 640 2 timeout 900   150 9900 0
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1400 12000    0 error (42) 880     710   5900    0 out of memory 300     15000   3700    0 true 4.1 280 36 2 unknown 900    310 10000   0 unknown 8.3 430 120 0 timeout 900   580 9400 0 timeout 900     1500 11000    0 timeout 900    4600 9100   0 true 13 1000 84 2 out of memory 32    15000 430   0 true 23   1000 240 2 disqualified 900   400 11000 0 timeout (verification) 900    340 8100   0 true 23   380 270 2 timeout 900   730 11000 0 true 80   400 950 2 unknown 69   1100 660 0 error (1) 870   170 9800 0
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1400 11000    0 error (42) 870     1000   5700    0 out of memory 420     15000   5200    0 true 4.2 280 40 2 unknown 900    280 10000   0 unknown 8.0 430 110 0 timeout 900   710 9200 0 timeout 900     980 12000    0 timeout 900    4300 9000   0 true 11 1200 88 2 out of memory 32    15000 490   0 true 33   1200 340 2 disqualified 890   390 8300 0 timeout (verification) 900    440 7300   0 true 19   360 190 2 timeout 900   870 10000 0 true 59   420 830 2 unknown 84   2100 870 0 error (1) 17   230 220 0
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1900 13000    0 error (42) 880     1400   7200    0 out of memory 540     15000   7600    0 true 4.1 280 38 2 unknown 900    260 11000   0 unknown 8.1 430 120 0 timeout 900   730 8400 0 timeout 900     860 11000    0 timeout 900    4700 11000   0 true 11 1200 82 2 out of memory 31    15000 480   0 true 4.0 220 41 2 disqualified 890   370 7200 0 probably out of memory (killed (signal 9, verification)) 170    15000 2400   0 true 21   370 250 2 true 8.6 350 67 2 true 8.7 380 72 2 unknown 100   3000 1100 0 error (1) 17   180 210 0
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 900     1400 13000    0 out of memory 250     15000   3700    0 out of memory 190     15000   2300    0 timeout 960   9300 10000 0 unknown 93    55 1100   0 timeout 900   3400 8600 0 timeout 900   3400 8300 0 timeout 900     13000 10000    0 timeout 900    75 8400   0 timeout 910 6000 9700 0 out of memory 590    15000 7200   0 true 3.9 220 42 1 disqualified 890   350 12000 0 probably out of memory (killed (signal 9, verification)) 180    15000 2400   0 timeout 900   760 12000 0 timeout 900   1000 5800 0 true 9.0 380 69 2 true 5.8 200 46 1 error (1) 53   150 580 0
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1800 10000    0 error (42) 880     1400   4400    0 out of memory 540     15000   8100    0 true 4.3 290 43 2 unknown 900    300 11000   0 unknown 8.2 430 90 0 timeout 900   740 9200 0 timeout 900     870 9200    0 timeout 900    5300 11000   0 true 13 1000 82 2 out of memory 32    15000 390   0 true 4.1 230 38 2 disqualified 890   410 6000 0 probably out of memory (killed (signal 9, verification)) 170    15000 2700   0 true 25   370 310 2 true 9.3 380 79 2 true 11   380 100 2 unknown 110   3000 1100 0 error (1) 17   180 230 0
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1600 13000    0 error (42) 880     1300   6100    0 out of memory 360     15000   4600    0 true 6.1 300 64 2 unknown 900    280 12000   0 unknown 8.3 430 120 0 timeout 900   620 9600 0 timeout 900     1300 11000    0 timeout 900    4200 11000   0 true 14 1100 120 2 out of memory 39    15000 500   0 true 4.1 220 48 2 disqualified 890   460 8900 0 probably out of memory (killed (signal 9, verification)) 170    15000 3000   0 true 110   490 1400 2 true 19   360 200 2 true 11   370 110 2 unknown 88   1900 1100 0 error (1) 17   180 200 0
bitvector/modulus_true-unreach-call_true-no-overflow.i true .69  28 8.1  2 true 250     1100   2300    2 error (42) 880     9600   12000    0 true 230   2500 3100 2 unknown 8.9  160 92   0 unknown 8.1 430 97 0 timeout 900   560 9100 0 true 190     280 2100    2 timeout 900    4300 10000   0 true 34 1600 350 2 out of memory 59    15000 760   0 unknown 140   1400 1700 0 disqualified 3.1 87 50 0 timeout (verification) 900    150 11000   0 true 12   440 110 2 true 30   380 320 2 true 23   480 290 2 true 60   720 790 2 timeout 900   200 11000 0
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .14  23 1.2  2 true .11  6.2 .54 2 true .086 6.6 .72 2 true 2.9 240 26 2 unknown 2.3  68 28   0 true 8.2 370 110 2 true 8.1 370 110 2 true .11  26 1.4  2 timeout 900    85 11000   0 true 11 1200 86 2 true .36 58 3.1 2 true 3.9 220 40 2 disqualified 2.0 71 28 0 true .15 15 1.7 2 true 31   600 310 2 true 20   510 170 2 true 40   660 410 2 true 54   540 590 2 timeout 900   200 9800 0
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .17  24 1.3  2 true .096 6.9 .71 1 true 1.0   63   12    1 true 19   650 220 2 unknown 2.2  68 28   0 unknown 8.3 430 100 0 timeout 900   400 7000 0 true .11  26 1.3  2 timeout 900    2100 9700   0 true 16 1200 120 1 true .91 60 9.6 2 true 3.5 220 35 2 disqualified 2.3 72 31 0 true .19 17 2.2 2 error (7) 740   2200 9200 0 true 70   780 800 2 timeout 900   1900 12000 0 true 53   560 570 2 timeout 900   160 10000 0
bitvector/parity_true-unreach-call_true-no-overflow.i true 2.8   30 40    2 true 4.0   9.1 57    1 true 4.0   9.9 54    1 witness invalid (true) 550   11000 8300 0 unknown 24    68 300   0 unknown 8.3 430 95 0 true 110   380 1200 2 true 6.8   28 80    2 timeout 900    2100 11000   0 true 26 1300 250 2 true 2.5  93 32   2 unknown 490   570 6200 0 disqualified 880   300 11000 0 true 26    25 360   2 timeout 900   1100 13000 0 timeout 900   770 14000 0 timeout 900   1100 12000 0 true 69   560 790 2 timeout 900   160 12000 0
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 900     1500 12000    0 error (42) 880     5200   4000    0 error (42) 880     110   11000    0 timeout 970   6100 8900 0 unknown 170    85 2000   0 unknown 8.0 430 96 0 timeout 900   440 8600 0 timeout 900     870 14000    0 timeout 900    75 10000   0 timeout 970 7300 8000 0 timeout 900    480 6900   0 unknown 92   980 950 0 disqualified 880   260 12000 0 timeout (verification) 900    380 10000   0 unknown 320   620 4700 0 timeout 900   760 10000 0 timeout 900   590 13000 0 unknown 380   650 3800 0 error (1) 890   150 12000 0
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 10     230 86    0 false(unreach-call) 4.6   180   57    1 out of memory 160     15000   2100    0 false(unreach-call) 10   420 90 1 false(unreach-call) 14    88 190   1 unknown 8.4 430 120 0 unknown 16   430 200 0 false(unreach-call) 4.2   89 54    1 timeout 900    2200 7600   0 false(unreach-call) 19 1300 160 1 false(unreach-call) 38    12000 540   1 unknown 150   2600 1600 0 disqualified 50   290 450 0 false(unreach-call) 1.3  20 18   1 false(unreach-call) 28   600 220 1 timeout 900   2900 6300 0 false(unreach-call) 31   620 250 1 false(unreach-call) 43   400 480 1 false(unreach-call) 120   200 1500 1
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 8.9   240 86    0 false(unreach-call) 4.0   150   53    1 out of memory 160     15000   1700    0 false(unreach-call) 19   610 180 1 false(unreach-call) 16    88 180   1 unknown 8.4 430 120 0 unknown 16   440 220 0 false(unreach-call) 4.6   97 56    1 timeout 900    4300 6500   0 false(unreach-call) 24 1400 180 1 false(unreach-call) 28    8700 390   1 unknown 100   2600 1200 0 disqualified 110   360 1100 0 false(unreach-call) 1.8  20 23   1 false(unreach-call) 33   680 280 1 timeout 900   3800 8100 0 false(unreach-call) 34   670 300 1 false(unreach-call) 110   1000 1200 1 false(unreach-call) 140   200 1700 1
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 8.1   160 68    0 false(unreach-call) .89  52   11    1 false(unreach-call) 17     2000   220    1 false(unreach-call) 7.8 290 70 1 false(unreach-call) 4.6  60 73   1 unknown 8.2 430 95 0 unknown 28   440 320 0 false(unreach-call) 1.7   57 21    1 timeout 900    2300 5400   0 false(unreach-call) 19 1300 140 1 false(unreach-call) 2.5  540 36   1 unknown 80   2500 910 0 disqualified 27   230 300 0 false(unreach-call) .52 18 6.5 1 false(unreach-call) 27   650 250 1 false(unreach-call) 110   890 1100 1 false(unreach-call) 29   660 230 1 false(unreach-call) 97   920 1100 1 false(unreach-call) 56   200 700 1
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 78     330 560    2 true 19     290   250    2 out of memory 160     15000   1900    0 true 24   760 260 2 unknown 92    210 1100   0 unknown 8.3 430 130 0 unknown 16   430 210 0 true 21     190 280    2 timeout 900    4300 7300   0 true 20 1400 150 2 out of memory 46    15000 600   0 unknown 220   2400 3200 0 disqualified 290   470 2400 0 true .96 18 12   2 true 45   980 360 2 timeout 900   5100 9700 0 true 47   990 390 2 true 97   1100 1000 2 error (1) 870   200 9400 0
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 8.8   290 93    2 true 17     230   220    2 out of memory 160     15000   2000    0 true 17   660 170 2 unknown 35    160 550   0 unknown 8.4 430 110 0 unknown 16   430 190 0 true 11     160 170    2 timeout 900    4400 8100   0 true 25 1200 200 2 out of memory 46    15000 620   0 unknown 160   2600 1800 0 disqualified 260   450 2600 0 true .91 18 14   2 true 46   1000 390 2 timeout 900   4600 8400 0 true 47   1200 370 2 true 160   1300 1700 2 error (1) 870   200 11000 0
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 9.7   250 88    2 true 16     220   200    2 out of memory 130     15000   1600    0 true 18   690 200 2 unknown 34    160 410   0 unknown 8.2 430 100 0 unknown 28   440 370 0 true 10     160 120    2 timeout 900    2300 8200   0 true 24 1500 200 2 out of memory 46    15000 540   0 unknown 110   2800 1300 0 disqualified 320   480 2200 0 true .92 18 12   2 true 29   900 230 2 timeout 900   3400 6600 0 true 39   1200 310 2 true 130   1000 1500 2 error (1) 870   200 11000 0
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     650 8600    0 error (42) 880     570   10000    0 out of memory 110     15000   1300    0 timeout 940   5000 9000 0 unknown 900    250 11000   0 unknown 8.3 430 100 0 error - divine failed with signal 11 1.6 200 18 0 timeout 900     370 11000    0 timeout 900    4400 6500   0 timeout 930 4700 8700 0 out of memory 51    15000 800   0 unknown 150   3000 1800 0 disqualified 880   730 7200 0 timeout (verification) 900    540 9900   0 timeout 900   2500 13000 0 timeout 900   3100 9600 0 timeout 900   5900 12000 0 unknown 570   690 7600 0 error (1) 860   210 12000 0
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     7400 10000    0 error (42) 880     760   5300    0 out of memory 110     15000   1500    0 true 20   690 200 2 unknown 900    370 11000   0 unknown 8.4 430 100 0 error - divine failed with signal 11 1.6 200 21 0 timeout 900     2600 8700    0 timeout 900    4300 7000   0 true 21 1200 190 2 out of memory 53    15000 700   0 unknown 160   2700 1800 0 disqualified 880   720 6400 0 timeout (verification) 900    880 9400   0 true 64   1700 550 2 timeout 900   5500 7500 0 true 65   1800 500 2 timeout 900   1200 8500 0 error (1) 870   210 12000 0
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 900     6500 11000    0 error (42) 880     660   7000    0 out of memory 370     15000   3900    0 true 59   1300 650 2 unknown 900    350 12000   0 unknown 8.4 430 110 0 error - divine failed with signal 11 1.6 200 22 0 timeout 900     2300 9200    0 timeout 900    4400 7700   0 true 25 1500 210 2 out of memory 49    15000 710   0 unknown 260   3600 3200 0 disqualified 880   730 8500 0 timeout (verification) 900    150 8600   0 true 48   1600 440 2 timeout 900   3700 6300 0 true 52   1800 420 2 timeout 900   680 8600 0 error (1) 870   210 12000 0
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 900     6600 9900    0 error (42) 880     690   5000    0 out of memory 390     15000   3800    0 true 58   1200 700 2 unknown 900    350 9600   0 unknown 8.4 430 91 0 error - divine failed with signal 11 1.5 200 18 0 timeout 900     2300 8700    0 timeout 900    4300 6300   0 true 26 1600 220 2 out of memory 48    15000 650   0 unknown 310   2600 3600 0 disqualified 880   720 9900 0 timeout (verification) 900    160 9100   0 true 44   1400 390 2 timeout 900   4500 6800 0 true 52   1600 480 2 timeout 900   680 8000 0 error (1) 870   210 9500 0
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     7100 9800    0 error (42) 870     690   4800    0 out of memory 110     15000   1500    0 true 21   690 220 2 unknown 900    420 12000   0 unknown 8.2 430 97 0 error - divine failed with signal 11 1.6 200 25 0 timeout 900     1800 13000    0 timeout 900    4300 9300   0 true 19 1400 170 2 out of memory 51    15000 600   0 unknown 260   3000 3200 0 disqualified 880   790 9300 0 timeout (verification) 900    230 11000   0 true 43   1300 370 2 timeout 900   5400 9000 0 true 50   1400 440 2 timeout 900   1200 7700 0 error (1) 870   210 11000 0
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     7000 11000    0 error (42) 880     690   5000    0 out of memory 110     15000   1500    0 true 22   690 250 2 unknown 900    430 11000   0 unknown 8.4 430 110 0 error - divine failed with signal 11 1.6 200 20 0 timeout 900     1900 11000    0 timeout 900    4400 7200   0 true 19 1400 160 2 out of memory 51    15000 670   0 timeout 900   5000 8400 0 disqualified 880   800 6200 0 timeout (verification) 900    220 11000   0 true 43   1300 390 2 timeout 900   3700 6500 0 true 52   1800 440 2 timeout 900   1300 7400 0 error (1) 870   210 11000 0
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true .21  25 1.8  2 true 4.7   35   61    2 error (42) 870     4900   13000    0 true 13   480 140 2 unknown 1.4  66 16   0 unknown 8.2 430 91 0 timeout 900   420 9600 0 true .53  28 6.9  2 timeout 900    4300 10000   0 true 21 1200 190 2 out of memory 57    15000 730   0 unknown 35   1100 340 0 disqualified 3.7 94 52 0 timeout (verification) 900    160 11000   0 true 270   900 2900 2 timeout 900   1000 10000 0 true 270   880 3800 2 true 210   860 2200 2 error (1) 870   160 12000 0
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true .14  25 1.4  2 true 3.0   35   38    2 error (42) 870     1300   9600    0 true 140   1100 1800 2 unknown 1.2  67 14   0 unknown 8.5 430 120 0 timeout 900   450 8900 0 true .36  29 4.3  2 timeout 900    4300 9600   0 true 18 1200 130 1 out of memory 63    15000 830   0 unknown 43   1200 430 0 disqualified 2.6 89 38 0 true 2.8  24 39   2 true 40   800 380 2 timeout 900   1300 11000 0 true 62   940 590 2 true 100   990 1100 2 timeout 900   160 9900 0
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 4.0   160 49    1 true 3.0   36   39    1 error (42) 870     1800   11000    0 true 110   1400 1300 1 unknown 1.1  66 13   0 unknown 8.2 430 100 0 timeout 900   410 9700 0 true .73  30 8.3  1 timeout 900    610 12000   0 true 120 2100 1300 1 out of memory 59    15000 830   0 unknown 39   1000 350 0 disqualified 21   150 290 0 true 9.1  31 130   1 timeout 900   830 12000 0 timeout 900   1200 9900 0 timeout 900   890 11000 0 true 180   940 2000 1 error (1) 860   160 13000 0
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1.2   25 16    2 true 7.8   42   95    2 error (42) 870     3500   12000    0 true 170   450 2800 2 unknown 4.3  65 67   0 unknown 8.3 430 120 0 timeout 900   420 8900 0 true 3.2   30 41    2 timeout 900    4300 10000   0 true 97 1700 960 2 out of memory 96    15000 1600   0 unknown 39   1200 400 0 disqualified 15   99 230 0 timeout (verification) 900    41 11000   0 true 750   850 9400 2 timeout 900   1300 10000 0 true 830   900 9700 2 true 220   850 2400 2 error (1) 860   170 11000 0
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true .15  25 1.2  2 true 3.0   35   38    2 error (42) 870     1300   9100    0 true 140   1100 1500 2 unknown 1.2  67 15   0 unknown 8.1 430 100 0 timeout 900   480 8900 0 true .35  29 4.6  2 timeout 900    4300 9000   0 true 16 1300 120 1 out of memory 63    15000 980   0 unknown 41   1300 380 0 disqualified 2.6 88 31 0 true 2.8  24 34   2 true 26   750 230 2 timeout 900   1200 12000 0 true 50   810 560 2 true 98   800 1200 2 timeout 900   170 12000 0
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) .12  24 .96 1 false(unreach-call) .067 8.9 .46 1 false(unreach-call) .062 9.6 .42 1 false(unreach-call) 2.8 260 27 1 false(unreach-call) .14 34 1.7 1 false(unreach-call) 8.1 430 100 1 false(unreach-call) 8.1 430 100 1 false(unreach-call) .082 26 1.1  1 false(unreach-call) .42 83 6.1 1 false(unreach-call) 12 1200 87 1 false(unreach-call) .35 59 3.3 1 false(unreach-call) 4.7 270 43 1 disqualified 2.6 71 30 0 false(unreach-call) .18 16 1.6 1 false(unreach-call) 13   360 98 1 false(unreach-call) 13   360 97 1 false(unreach-call) 13   350 97 1 false(unreach-call) 8.4 300 69 1 false(unreach-call) 3.4 150 37 1
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) .12  24 .93 1 false(unreach-call) .066 9.8 .48 1 false(unreach-call) .064 9.1 .42 1 false(unreach-call) 2.9 250 24 1 false(unreach-call) .15 33 1.9 1 false(unreach-call) 8.0 430 100 1 false(unreach-call) 8.1 430 110 1 false(unreach-call) .083 26 .80 1 false(unreach-call) .43 83 5.9 1 false(unreach-call) 13 1100 99 1 false(unreach-call) .38 58 3.2 1 false(unreach-call) 5.0 260 49 1 disqualified 2.5 70 39 0 false(unreach-call) .17 16 2.7 1 false(unreach-call) 6.5 320 48 1 false(unreach-call) 7.8 360 61 1 false(unreach-call) 8.0 360 71 1 false(unreach-call) 8.6 270 66 1 false(unreach-call) 3.2 150 36 1
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) .13  24 .94 1 false(unreach-call) .068 9.5 .37 1 false(unreach-call) .066 9.1 .42 1 false(unreach-call) 2.8 260 27 1 false(unreach-call) .14 34 1.9 1 false(unreach-call) 8.1 430 99 1 false(unreach-call) 8.0 430 120 1 false(unreach-call) .081 26 1.1  1 false(unreach-call) .44 83 4.5 1 false(unreach-call) 12 1200 88 1 false(unreach-call) .35 58 3.8 1 false(unreach-call) 5.0 270 48 1 disqualified 2.6 71 30 0 false(unreach-call) .16 16 2.2 1 false(unreach-call) 13   360 100 1 false(unreach-call) 12   360 110 1 false(unreach-call) 12   360 97 1 false(unreach-call) 6.9 270 61 1 false(unreach-call) 3.5 150 39 1
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c error (5) .088 24 .97 0 false(unreach-call) .30  9.8 4.1  1 false(unreach-call) .74  9.6 12    1 false(unreach-call) 64   1300 780 1 unknown .84 66 11   0 unknown 8.2 430 99 0 false(unreach-call) 39   440 440 0 false(unreach-call) .62  26 7.5  1 timeout 900    1800 10000   0 false(unreach-call) 74 1700 800 1 false(unreach-call) .68 77 7.4 1 unknown 7.7 220 81 0 disqualified 21   88 340 0 timeout (verification) 900    660 11000   0 false(unreach-call) 350   810 3200 1 false(unreach-call) 150   830 1800 1 false(unreach-call) 420   870 3900 1 error 9.7 200 69 0 false(unreach-call) 8.7 150 93 1
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) .14  24 .89 1 false(unreach-call) .073 9.7 .43 1 false(unreach-call) .071 9.7 .38 1 false(unreach-call) 2.9 250 29 1 false(unreach-call) .14 34 1.4 1 false(unreach-call) 8.1 430 110 1 false(unreach-call) 8.2 430 79 1 false(unreach-call) .083 26 1.0  1 false(unreach-call) .44 83 4.5 1 false(unreach-call) 12 1200 91 1 false(unreach-call) .36 59 2.4 1 false(unreach-call) 4.9 260 43 1 disqualified 2.5 71 33 0 false(unreach-call) .16 16 1.7 1 false(unreach-call) 6.6 330 53 1 false(unreach-call) 6.5 330 60 1 false(unreach-call) 8.0 350 57 1 false(unreach-call) 8.7 260 81 1 false(unreach-call) 3.3 160 40 1
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) .12  24 1.0  1 false(unreach-call) .14  9.8 .40 1 false(unreach-call) .068 9.5 .49 1 false(unreach-call) 2.9 250 31 1 false(unreach-call) .13 34 1.8 1 false(unreach-call) 8.2 430 95 1 false(unreach-call) 8.2 430 100 1 false(unreach-call) .081 26 1.0  1 false(unreach-call) .41 83 4.6 1 false(unreach-call) 13 1100 96 1 false(unreach-call) .37 59 3.4 1 false(unreach-call) 4.9 270 45 1 disqualified 2.6 71 30 0 false(unreach-call) .21 16 1.7 1 false(unreach-call) 7.7 360 55 1 false(unreach-call) 7.4 360 68 1 false(unreach-call) 7.9 370 61 1 false(unreach-call) 8.9 300 83 1 false(unreach-call) 3.5 150 36 1
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true .096 24 .82 2 true .094 6.1 .23 2 witness invalid (true) .044 6.5 .25 0 true 2.8 250 26 2 unknown .79 66 8.2 0 true 8.2 370 120 2 true 7.9 370 110 2 true .076 26 .88 2 timeout 900    85 9500   0 true 12 1000 81 2 true .36 59 3.4 2 true 3.7 210 36 2 disqualified 1.9 66 24 0 true .14 16 1.4 2 true 7.8 360 63 2 true 8.0 370 57 2 true 8.0 340 49 2 true 12   440 110 2 timeout 900   150 13000 0
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true .11  24 .86 2 true .052 6.7 .37 2 witness invalid (true) .042 6.1 .28 0 true 2.8 260 26 2 unknown .80 66 8.5 0 true 8.0 370 96 2 true 8.0 370 120 2 true .093 26 .63 2 timeout 900    84 9700   0 true 13 1000 79 2 true .40 59 3.1 2 true 3.7 200 35 2 disqualified 1.9 68 24 0 true .14 15 1.4 2 true 13   350 100 2 true 12   340 100 2 true 13   360 96 2 true 15   420 130 2 timeout 900   150 11000 0
bitvector-regression/signextension2_true-unreach-call_true-termination.c true .11  23 .84 2 true .055 6.8 .29 2 witness invalid (true) .043 6.2 .24 0 true 2.8 250 24 2 unknown .80 66 11   0 true 8.2 370 110 2 true 8.1 370 120 2 true .075 26 .90 2 timeout 900    85 10000   0 true 11 1200 83 2 true .37 58 3.3 2 true 3.7 200 41 2 disqualified 2.0 67 22 0 true .17 16 1.6 2 true 7.8 370 62 2 true 8.1 370 70 2 true 8.1 370 63 2 true 13   450 110 2 timeout 900   150 12000 0
bitvector-regression/signextension_true-unreach-call_true-termination.c true .10  24 .78 2 true .058 6.4 .33 2 witness invalid (true) .037 6.2 .29 0 true 2.9 250 25 2 unknown .80 68 9.6 0 true 8.1 370 100 2 true 8.1 370 100 2 true .079 26 .73 2 timeout 900    85 11000   0 true 13 1000 91 2 true .37 59 3.2 2 true 3.7 210 38 2 disqualified 2.0 67 22 0 true .14 17 1.5 2 true 8.3 370 63 2 true 8.6 370 65 2 true 7.6 340 56 2 true 12   450 100 2 timeout 900   150 13000 0
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) .16  24 1.0  1 false(unreach-call) .085 9.7 .69 1 false(unreach-call) 2.8   420   36    1 false(unreach-call) 6.0 290 52 1 false(unreach-call) .38 35 5.2 1 unknown 8.2 430 120 0 false(unreach-call) 21   430 240 1 false(unreach-call) .11  26 .87 1 false(unreach-call) .44 83 4.9 1 false(unreach-call) 13 1200 100 1 false(unreach-call) .40 60 3.6 1 false(unreach-call) 5.9 290 55 1 disqualified 3.5 92 44 0 false(unreach-call) .20 17 2.6 1 false(unreach-call) 17   440 160 1 false(unreach-call) 9.7 380 77 1 false(unreach-call) 26   530 280 1 false(unreach-call) 18   280 160 1 false(unreach-call) 3.5 150 34 1
bitvector-loops/overflow_false-unreach-call1.i timeout 900     1200 11000    0 out of memory 270     15000   4200    0 out of memory 200     15000   3000    0 timeout 970   9200 8900 0 unknown 36    43 470   0 timeout 900   3500 8400 0 timeout 900   3400 8400 0 timeout 900     14000 11000    0 false(unreach-call) .42 83 5.0 1 timeout 970 7600 8900 0 out of memory 790    15000 8600   0 false(unreach-call) 4.7 270 46 1 disqualified 880   930 12000 0 false(unreach-call) .16 16 2.2 1 timeout 900   670 11000 0 timeout 900   960 9200 0 timeout 900   630 10000 0 false(unreach-call) 220   1800 3100 1 error (1) 53   150 740 0
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) .53  28 7.1  1 false(unreach-call) .14  9.6 1.5  1 false(unreach-call) .22  9.3 2.6  0 false(unreach-call) 13   490 130 1 false(unreach-call) 3.5  38 47   1 unknown 8.2 430 98 0 false(unreach-call) 54   450 620 0 false(unreach-call) .26  26 3.3  1 false(unreach-call) .57 84 5.8 1 false(unreach-call) 22 1300 170 1 false(unreach-call) .44 58 4.8 1 false(unreach-call) 16   530 160 1 disqualified 5.7 110 75 0 false(unreach-call) .52 18 7.4 0 false(unreach-call) 250   550 3500 1 timeout 900   700 11000 0 false(unreach-call) 330   590 4300 1 false(unreach-call) 220   770 2800 0 false(unreach-call) 4.9 150 56 1
../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 status cpu (s) mem (MB) energy (J) score
total 50 14000   51000 170000 53 50 12000   53000 86000 50 50 12000    300000   150000   22 50 6700 71000 71000 75 50 11000 6400 130000 11 50 2200 27000 22000 17 50 17000 27000 160000 26 50 14000    47000 170000   57 50 33000   110000 340000 12 50 6000 91000 56000 72 50 4300 350000 43000 40 50 6600   74000 81000 37 50 17000 14000 180000 0 50 13000    65000 150000   50 50 13000 39000 160000 62 50 25000 73000 270000 37 50 14000 55000 170000 62 50 9200 43000 93000 57 50 28000 8600 360000 13
    correct results 30 110   1600 860 52 27 330   2500 3300 42 12 22    2600   280   15 43 1300 23000 16000 74 11 40 510 520 11 11 89 4400 1200 17 16 280 6300 3200 26 34 310    1800 3800   56 11 150   930 2000 12 39 1100 50000 9500 66 26 91 24000 1200 40 22 230   8700 2300 36 0 30 100    590 1400   49 37 2800 26000 31000 62 23 1200 12000 13000 37 37 3100 28000 34000 62 33 2400 22000 26000 55 13 370 2100 4400 13
        correct true 22 110   1400 850 44 15 320   2000 3200 30 3 .26 20   2.3 6 31 1100 18000 14000 62 0 6 49 2200 640 12 10 220 3700 2500 20 22 300    1300 3600   44 1 3.2 75 41 2 27 800 34000 7400 54 14 19 2100 240 28 14 180   6300 1800 28 0 19 97    400 1400   38 25 1900 19000 22000 50 14 810 7300 9500 28 25 2000 21000 23000 50 22 1800 16000 20000 44 0
        correct false 8 1.7 200 17 8 12 11   470 130 12 9 22    2500   280   9 12 150 5100 1600 12 11 40 510 520 11 5 40 2100 510 5 6 62 2600 750 6 12 12    480 150   12 10 150   860 1900 10 12 250 15000 2100 12 12 72 22000 1000 12 8 51   2400 490 8 0 11 5.2  190 66   11 12 890 6300 9600 12 9 350 4400 3700 9 12 1100 6600 12000 12 11 550 6100 6600 11 13 370 2100 4400 13
    correct-unconfimed results 4 31   780 290 1 8 9.3 120 120 8 8 14    170   180   7 1 110 1400 1300 1 0 0 3 120 1300 1400 0 1 .73 30 8.3 1 0 6 220 8400 2000 6 0 1 3.9 220 42 1 0 2 9.6  49 140   1 0 0 0 3 410 1900 4800 2 0
        correct-unconfirmed true 1 4.0 160 49 1 8 9.3 120 120 8 7 13    160   180   7 1 110 1400 1300 1 0 0 0 1 .73 30 8.3 1 0 6 220 8400 2000 6 0 1 3.9 220 42 1 0 1 9.1  31 130   1 0 0 0 2 190 1100 2000 2 0
        correct-unconfirmed false 3 27   630 240 0 0 1 .22 9.3 2.6 0 0 0 0 3 120 1300 1400 0 0 0 0 0 0 0 1 .52 18 7.4 0 0 0 0 1 220 770 2800 0 0
    incorrect results 0 0 0 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 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 53 50 22 75 11 17 26 57 12 72 40 37 0 50 62 37 62 57 13
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cbmc.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-BitVectors depthk.sv-comp19_prop-reachsafety.ReachSafety-BitVectors divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-BitVectors map2check.sv-comp19_prop-reachsafety.ReachSafety-BitVectors pesco.sv-comp19_prop-reachsafety.ReachSafety-BitVectors pinaka.sv-comp19_prop-reachsafety.ReachSafety-BitVectors skink.sv-comp19_prop-reachsafety.ReachSafety-BitVectors smack.sv-comp19_prop-reachsafety.ReachSafety-BitVectors symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer.sv-comp19_prop-reachsafety.ReachSafety-BitVectors ukojak.sv-comp19_prop-reachsafety.ReachSafety-BitVectors utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors veriabs.sv-comp19_prop-reachsafety.ReachSafety-BitVectors verifuzz.sv-comp19_prop-reachsafety.ReachSafety-BitVectors