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-05 07:52:24 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 false(unreach-call) .32  28 3.8  1 false(unreach-call) .70 34 6.7 1 error 11   470 87 0 unknown 12   500 89 0 false(unreach-call) 17   440 180 1 false(unreach-call) 2.2  110 33   1 false(unreach-call) 1.1   29 10    1 false(unreach-call) 1.2   29 14    1 false(unreach-call) 7.1 400 47 0 false(unreach-call) 1.3  13 15   1 unknown 47   730 600 0 false(unreach-call) .31 12 4.0 1 false(unreach-call) 85   880 880 1 false(unreach-call) 31   490 280 1 false(unreach-call) 110   1500 940 1 false(unreach-call) 29   430 260 1
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 900     1400 10000    0 error (42) 870    6000 3300   0 error 3.6 290 32 0 unknown 3.3 290 30 0 timeout 910   7700 10000 0 unknown 70    75 990   0 timeout 900     780 11000    0 timeout 900     780 11000    0 false(unreach-call) 3.5 270 34 0 unknown 900    700 13000   0 unknown 110   730 1500 0 timeout (timeout) 900    790 13000   0 unknown 14   380 140 0 timeout 900   680 10000 0 timeout 900   700 11000 0 unknown 470   3100 3700 0
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .33  29 4.3  2 true .86 34 8.1 1 error 9.5 480 75 0 unknown 12   530 88 0 true 12   440 100 2 true 74    1700 820   2 true .18  27 1.6  2 true .16  27 1.9  2 false(unreach-call) 9.4 460 78 -16 true 4.1  13 56   2 unknown 35   700 370 0 true .32 12 3.9 2 timeout 900   1400 12000 0 true 720   1600 7700 2 timeout 900   2600 12000 0 true 29   570 210 2
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .34  31 3.7  2 true .85 34 8.5 1 error 13   520 100 0 unknown 12   500 95 0 true 13   470 120 2 true 28    910 330   2 true .17  27 2.0  2 true .15  27 1.8  2 false(unreach-call) 9.1 460 84 -16 true 4.1  13 54   2 unknown 31   710 360 0 true .35 12 4.0 2 timeout 900   1400 10000 0 timeout 900   1500 7600 0 timeout 900   3100 12000 0 true 27   480 180 2
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .25  27 2.6  2 true .53 36 5.7 1 error 7.4 310 90 0 unknown 5.3 310 56 0 true 6.8 280 76 2 true 490    310 7300   2 true .97  29 12    2 true .38  27 4.3  2 timeout 900   2400 11000 0 true .64 12 7.9 2 unknown 84   950 730 0 true .42 12 5.0 2 timeout 900   630 13000 0 error (7) 660   670 4700 0 timeout 900   1000 12000 0 true 21   300 190 2
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true .76  39 9.0  2 true 2.0  42 24   1 true 3.9 280 31 2 true 3.7 280 37 2 true 7.6 280 83 2 true 230    280 3000   2 true 27     45 330    2 true 37     44 420    2 false(unreach-call) 4.5 290 40 -16 true 28    20 340   2 true 27   900 250 2 true 9.8  15 130   2 timeout 900   670 12000 0 timeout 900   520 11000 0 timeout 900   1100 11000 0 true 53   400 590 2
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true .64  40 7.4  2 true 2.0  42 26   1 error 5.3 300 49 0 unknown 3.5 300 35 0 true 150   310 2000 2 true 470    330 5000   2 true 30     43 370    2 true 37     45 460    2 false(unreach-call) 3.4 260 29 -16 true 30    18 380   2 unknown 82   870 1200 0 true 9.4  15 120   2 timeout 900   2800 11000 0 timeout 900   500 12000 0 error (7) 510   1200 4100 0 true 52   410 630 2
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .56  33 6.0  2 true .76 33 9.5 2 true 3.3 270 32 2 true 3.2 270 27 2 true 2.5 260 20 2 true 490    260 6000   2 true .082 27 .78 2 true .53  32 8.1  2 false(unreach-call) 8.6 460 69 -16 true .36 11 3.6 2 true 25   700 260 2 true .17 11 1.6 2 true 56   520 590 2 true 11   580 97 2 true 240   900 2800 2 true 17   320 120 2
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .48  55 5.6  2 true 1.6  33 14   2 error 5.9 380 49 0 unknown 3.5 290 34 0 true 7.4 450 75 2 true 16    410 190   2 true .099 26 1.1  2 true .12  26 1.2  2 false(unreach-call) 7.8 440 64 -16 true .34 11 4.0 2 true 7.6 370 66 2 true .16 12 2.0 2 true 170   3800 2500 2 true 100   2600 1100 2 true 230   1800 3100 2 true 18   330 120 2
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1500 10000    0 error (42) 870    970 7200   0 true 3.0 270 26 2 true 2.9 270 24 2 true 3.1 270 28 2 unknown 300    290 2800   0 timeout 900     1200 9800    0 timeout 900     1300 13000    0 true 2.9 280 23 2 unknown 900    89 6500   0 true 20   690 190 2 timeout (timeout) 900    75 8700   0 true 4.7 290 40 2 timeout 900   1700 12000 0 true 4.6 290 39 2 unknown 370   4800 4000 0
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1500 11000    0 error (42) 870    1300 5200   0 true 3.2 280 28 2 true 3.1 270 28 2 true 3.2 280 26 2 unknown 890    260 7900   0 timeout 900     830 10000    0 timeout 900     840 12000    0 true 3.1 280 31 2 unknown 900    190 9700   0 true 26   730 320 2 timeout (timeout) 900    94 8500   0 true 4.9 290 40 2 true 16   330 170 2 true 4.7 290 40 2 unknown 510   4300 6100 0
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1900 11000    0 error (42) 870    1700 6900   0 true 3.2 270 25 2 true 3.1 270 29 2 true 3.3 280 29 2 unknown 900    270 11000   0 timeout 900     750 9700    0 timeout 900     780 11000    0 timeout 900   5500 12000 0 unknown 900    120 12000   0 true 4.5 260 38 2 timeout (timeout) 900    15000 13000   0 true 4.9 290 38 2 true 6.2 320 50 2 true 4.8 290 44 2 unknown 620   5700 6900 0
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 900     1400 13000    0 out of memory 380    15000 4800   0 timeout 900   3900 10000 0 timeout 900   3900 11000 0 timeout 900   3500 9800 0 unknown 59    75 740   0 timeout 900     11000 10000    0 timeout 900     11000 12000    0 timeout 900   4300 11000 0 unknown 890    11 11000   0 true 4.0 320 35 1 timeout (timeout) 900    15000 12000   0 timeout 900   700 11000 0 timeout 900   5200 13000 0 true 6.3 310 53 1 true 8.0 220 63 1
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1800 10000    0 error (42) 870    1600 4300   0 true 3.2 280 32 2 true 3.2 270 29 2 true 3.4 280 29 2 unknown 900    330 7100   0 timeout 900     750 9100    0 timeout 900     750 8900    0 timeout 900   5500 11000 0 unknown 890    110 11000   0 true 4.0 250 39 2 timeout (timeout) 900    15000 13000   0 true 20   310 230 2 timeout 900   2100 10000 0 true 8.0 300 86 2 unknown 620   5400 6600 0
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1700 11000    0 error (42) 870    1700 5900   0 true 3.2 280 30 2 true 3.1 270 27 2 true 4.6 280 52 2 unknown 900    370 8800   0 timeout 900     1000 9700    0 timeout 900     1000 9300    0 timeout 900   5700 13000 0 unknown 890    120 11000   0 true 4.1 250 43 2 timeout (timeout) 900    15000 14000   0 true 4.9 290 38 2 timeout 900   2900 13000 0 true 5.1 290 44 2 unknown 510   5100 6800 0
bitvector/modulus_true-unreach-call_true-no-overflow.i true .63  39 8.9  2 true 460    1100 2100   2 error 18   310 240 0 unknown 3.9 300 34 0 true 220   2100 2400 2 unknown 890    380 7900   0 true 180     280 2100    2 true 200     330 2200    2 false(unreach-call) 3.0 270 24 -16 true 790    63 9900   2 unknown 46   730 530 0 true 640    57 8600   2 true 14   410 140 2 true 110   660 1500 2 true 13   500 110 2 true 30   610 290 2
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .12  24 1.2  2 true 1.2  33 11   2 true 3.3 280 34 2 true 3.1 270 29 2 true 2.4 250 20 2 true 7.0  260 89   2 true .090 26 .92 2 true .13  26 .91 2 false(unreach-call) 5.6 310 49 -16 true .32 11 3.6 2 true 3.9 240 37 2 true .17 11 1.6 2 true 270   3300 3300 2 true 120   470 1700 2 true 59   670 670 2 true 16   290 110 2
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .17  24 1.2  2 true 1.2  33 12   1 timeout 900   330 12000 0 unknown 3.4 290 35 0 true 16   470 140 2 true 22    550 270   2 true .12  26 .88 2 true .14  26 .98 2 false(unreach-call) 5.8 310 51 -16 unknown .27 11 4.2 0 true 5.3 300 47 2 true .17 12 2.0 2 timeout 900   1300 8800 0 true 240   780 2900 2 timeout 900   1300 12000 0 true 16   310 140 2
bitvector/parity_true-unreach-call_true-no-overflow.i true 2.7   44 30    2 true 4.1  35 44   1 error 3.5 290 29 0 unknown 3.0 280 27 0 true 120   980 1400 2 unknown 890    150 11000   0 true 7.0   28 93    2 true 9.4   33 130    2 false(unreach-call) 2.9 270 26 -16 true 9.4  13 130   2 unknown 150   740 1800 0 true 7.4  13 99   2 timeout 900   1000 12000 0 timeout 900   720 13000 0 timeout 900   1000 12000 0 true 32   340 330 2
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 900     1500 12000    0 error (42) 880    6300 4400   0 error 3.4 290 31 0 unknown 3.2 290 29 0 timeout 910   7000 8100 0 unknown 170    480 1700   0 timeout 900     760 12000    0 timeout 900     740 11000    0 false(unreach-call) 3.8 280 36 -16 unknown 900    700 12000   0 unknown 130   770 1800 0 timeout (timeout) 900    770 9900   0 timeout 900   560 11000 0 timeout 900   740 11000 0 timeout 900   650 11000 0 unknown 390   3200 3100 0
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 9.4   220 77    1 false(unreach-call) 5.9  220 76   1 timeout 900   4400 12000 0 false(unreach-call) 21   750 160 1 false(unreach-call) 8.6 320 68 1 false(unreach-call) 34    100 370   1 false(unreach-call) 5.9   87 60    1 false(unreach-call) 4.0   76 42    1 false(unreach-call) 86   3900 850 1 true 67    19 870   -32 unknown 82   780 980 0 false(unreach-call) .42 13 4.7 1 false(unreach-call) 24   710 180 1 timeout 900   6300 13000 0 false(unreach-call) 26   580 210 1 false(unreach-call) 59   420 590 1
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 7.3   240 83    1 false(unreach-call) 5.2  180 70   1 false(unreach-call) 27   1100 210 1 false(unreach-call) 23   1000 160 1 false(unreach-call) 26   810 260 1 false(unreach-call) 55    110 790   1 false(unreach-call) 6.1   96 63    1 false(unreach-call) 7.4   110 79    1 false(unreach-call) 63   3700 660 1 unknown 150    42 2200   0 unknown 45   720 530 0 false(unreach-call) .61 14 8.0 1 false(unreach-call) 27   650 210 1 timeout 900   6200 13000 0 false(unreach-call) 27   690 210 1 false(unreach-call) 150   880 1700 1
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 7.3   150 67    1 false(unreach-call) 1.5  64 18   1 error 6.9 400 66 0 false(unreach-call) 7.8 460 72 1 false(unreach-call) 6.1 300 52 1 false(unreach-call) 18    85 220   1 false(unreach-call) 2.6   58 26    1 false(unreach-call) 2.3   51 23    1 false(unreach-call) 7.4 450 54 0 true 4.1  15 53   -32 unknown 39   710 470 0 false(unreach-call) .28 12 3.5 1 false(unreach-call) 23   580 170 1 false(unreach-call) 88   1000 1100 1 false(unreach-call) 24   610 190 1 false(unreach-call) 130   790 1400 1
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 46     320 410    2 true 21    360 240   2 timeout 900   4400 10000 0 unknown 21   720 130 0 true 15   750 160 2 true 170    1300 2000   2 true 22     190 260    2 true 25     210 240    2 false(unreach-call) 86   3900 810 -16 unknown 890    42 11000   0 unknown 100   840 1300 0 true .59 13 7.6 2 true 41   1300 380 2 timeout 900   6300 11000 0 true 39   1100 330 2 true 93   750 900 2
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 8.0   280 95    2 true 18    290 240   2 true 38   2000 260 2 true 36   1700 270 2 true 14   730 120 2 true 140    1600 1700   2 true 11     160 130    2 true 13     170 120    2 false(unreach-call) 65   3100 620 -16 unknown 890    43 11000   0 unknown 89   760 940 0 true .62 13 6.8 2 true 43   1900 360 2 timeout 900   6300 12000 0 true 45   1400 360 2 true 170   900 1800 1
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 9.1   250 84    2 true 18    280 220   2 true 27   1100 210 2 true 23   890 150 2 true 15   750 160 2 true 140    1300 2100   2 true 10     150 110    2 true 12     160 160    2 true 88   3800 1000 2 unknown 890    43 11000   0 unknown 54   720 650 0 true .62 13 6.4 2 true 25   1000 190 2 timeout 900   6000 13000 0 true 270   4800 3700 2 true 160   790 1700 1
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     810 9700    0 error (42) 870    460 8600   0 timeout 900   6700 9000 0 timeout 900   5200 10000 0 timeout 900   4200 8900 0 unknown 890    390 7100   0 timeout 900     360 11000    0 timeout 900     290 11000    0 timeout 900   4400 12000 0 unknown .38 12 5.3 0 timeout 900   1400 9200 0 timeout (timeout) 900    400 11000   0 timeout 900   2100 13000 0 timeout 900   6400 12000 0 timeout 900   5100 12000 0 unknown 550   1000 6400 0
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     7600 9900    0 error (42) 870    940 3500   0 true 11   510 86 2 true 41   1800 330 2 true 17   760 150 2 true 46    2300 550   2 timeout 900     2300 8400    0 timeout 900     2400 11000    0 true 40   2400 350 2 unknown .41 12 4.8 0 unknown 62   730 610 0 timeout (timeout) 900    1100 12000   0 true 53   2200 490 2 timeout 900   6500 11000 0 true 230   4700 2500 2 timeout 900   1300 5000 0
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 900     6700 10000    0 error (42) 870    800 3200   0 true 11   500 87 2 true 20   790 150 2 true 51   1300 560 2 unknown 890    360 11000   0 timeout 900     2100 12000    0 timeout 900     2100 8500    0 true 120   3500 1200 2 unknown 890    110 13000   0 unknown 16   660 130 0 timeout (timeout) 900    130 11000   0 true 40   1800 350 2 timeout 910   6500 11000 0 timeout 900   5400 14000 0 timeout 900   1400 7400 0
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 900     6800 11000    0 error (42) 870    840 5800   0 true 12   520 95 2 true 20   790 160 2 true 56   2400 630 2 unknown 890    370 12000   0 timeout 900     2100 8300    0 timeout 900     2000 10000    0 true 120   3300 1600 2 unknown 900    130 12000   0 unknown 12   640 100 0 timeout (timeout) 900    220 10000   0 true 41   1800 350 2 timeout 900   6400 10000 0 timeout 900   5000 12000 0 timeout 900   1400 7500 0
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     7100 10000    0 error (42) 870    860 5600   0 timeout 900   4100 11000 0 true 43   1700 310 2 true 17   760 160 2 unknown 900    300 11000   0 timeout 900     1800 9500    0 timeout 900     1700 9600    0 true 110   3200 1300 2 unknown 900    170 9500   0 unknown 79   980 990 0 timeout (timeout) 900    210 11000   0 true 40   1500 390 2 timeout 900   6400 11000 0 true 250   4800 2900 2 timeout 900   1300 5600 0
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 900     7000 9700    0 error (42) 870    840 5600   0 timeout 900   4100 11000 0 true 42   2000 280 2 true 16   770 170 2 unknown 890    300 11000   0 timeout 900     1800 12000    0 timeout 900     1700 11000    0 true 66   3000 650 2 unknown 890    160 11000   0 unknown 15   650 130 0 timeout (timeout) 900    210 13000   0 true 39   1500 330 2 timeout 900   6500 11000 0 true 230   4800 2800 2 timeout 900   1200 5800 0
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true .22  28 2.0  2 true 6.1  54 72   2 error 5.0 320 47 0 unknown 3.7 290 37 0 true 12   380 130 2 true 14    390 150   2 true 4.3   34 52    2 true .35  28 4.4  2 false(unreach-call) 13   630 100 -16 unknown 900    220 12000   0 unknown 17   650 140 0 true 680    160 9200   2 error (7) 110   850 1200 0 timeout 900   1700 11000 0 error (7) 110   870 1400 0 true 98   820 960 2
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true .17  29 1.4  2 true 4.5  54 63   2 error 5.5 300 43 0 unknown 7.4 400 59 0 true 110   1300 1300 2 true 120    1200 1300   2 true .65  32 7.4  2 true .37  29 3.7  2 false(unreach-call) 8.1 450 62 -16 unknown 900    150 11000   0 unknown 20   680 180 0 true 2.8  15 38   2 true 26   750 210 2 timeout 900   1500 10000 0 true 84   1300 830 2 true 40   780 420 1
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 4.0   160 48    1 true 4.6  53 63   1 error 5.2 300 41 0 unknown 7.0 490 56 0 true 100   1300 1100 1 true 120    1200 1500   1 true .47  30 5.5  1 true .71  30 7.9  1 false(unreach-call) 10   450 71 -16 unknown 900    200 11000   0 unknown 19   660 170 0 true 4.7  18 62   1 timeout 900   890 9600 0 timeout 900   1400 11000 0 timeout 900   1100 10000 0 true 85   740 850 1
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1.1   36 12    2 true 12    52 160   2 error 4.6 320 41 0 unknown 3.4 290 31 0 true 170   400 2400 2 true 230    380 3200   2 true 23     35 310    2 true 1.8   29 21    2 timeout 900   3100 10000 0 unknown 900    230 11000   0 unknown 18   640 180 0 timeout (timeout) 900    45 12000   0 error (7) 490   910 6400 0 timeout 900   1500 12000 0 true 860   940 11000 2 true 100   810 1100 2
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true .17  28 1.3  2 true 4.6  53 53   2 error 5.6 320 48 0 unknown 6.6 360 52 0 true 110   1200 1400 2 true 120    1200 1500   2 true .67  32 8.5  2 true .36  29 3.8  2 false(unreach-call) 13   590 100 -16 unknown 890    150 10000   0 unknown 22   700 200 0 true 2.7  16 35   2 true 22   680 210 2 timeout 900   1600 12000 0 true 63   1200 620 2 true 40   740 390 1
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) .090 22 1.2  1 false(unreach-call) .23 33 1.7 1 false(unreach-call) 3.1 280 27 1 false(unreach-call) 3.0 280 24 1 false(unreach-call) 2.5 250 22 1 false(unreach-call) .35 48 4.3 1 false(unreach-call) .11  28 .83 1 false(unreach-call) .082 28 .86 1 false(unreach-call) 2.9 280 25 1 false(unreach-call) .31 11 3.8 1 false(unreach-call) 4.9 300 46 1 false(unreach-call) .14 11 1.6 1 false(unreach-call) 8.0 240 58 1 false(unreach-call) 8.1 240 70 1 false(unreach-call) 8.3 240 67 1 false(unreach-call) 7.5 300 63 1
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) .099 22 .83 1 false(unreach-call) .23 33 1.6 1 true 2.8 270 24 -32 true 2.8 270 25 -32 false(unreach-call) 2.8 270 27 1 false(unreach-call) .38 48 4.4 1 false(unreach-call) .11  28 .85 1 false(unreach-call) .10  28 .91 1 true 2.7 270 27 -32 false(unreach-call) .29 11 3.1 1 false(unreach-call) 4.9 290 41 1 false(unreach-call) .16 11 1.7 1 false(unreach-call) 4.0 240 39 1 false(unreach-call) 4.2 240 39 1 false(unreach-call) 4.0 240 37 1 false(unreach-call) 7.6 300 61 1
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) .12  22 .82 1 false(unreach-call) .23 33 2.0 1 false(unreach-call) 3.1 280 26 1 false(unreach-call) 2.9 270 27 1 false(unreach-call) 2.5 250 21 1 false(unreach-call) .38 48 4.2 1 false(unreach-call) .13  28 1.1  1 false(unreach-call) .13  28 1.2  1 false(unreach-call) 3.0 280 24 1 false(unreach-call) .31 11 4.0 1 false(unreach-call) 4.7 290 45 1 false(unreach-call) .14 11 1.4 1 false(unreach-call) 8.0 240 64 1 false(unreach-call) 8.2 240 74 1 false(unreach-call) 9.6 320 76 1 false(unreach-call) 7.3 270 62 1
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c error (5) .11  22 .64 0 false(unreach-call) 2.4  34 22   1 false(unreach-call) 3.3 290 30 0 false(unreach-call) 3.2 280 31 0 false(unreach-call) 64   1600 700 1 unknown 4.6  300 46   0 false(unreach-call) .75  28 8.6  1 false(unreach-call) .74  28 11    1 false(unreach-call) 3.0 280 26 0 false(unreach-call) 1.9  12 26   1 unknown 3.8 240 35 0 timeout (timeout) 900    2500 11000   0 false(unreach-call) 210   1300 2900 1 false(unreach-call) 120   1000 1500 1 false(unreach-call) 290   1200 4000 1 error 7.1 160 57 0
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) .13  22 .83 1 false(unreach-call) .27 33 2.2 1 true 2.8 270 25 -32 true 2.7 270 25 -32 false(unreach-call) 2.6 250 25 1 false(unreach-call) 480    70 5800   1 false(unreach-call) .091 28 .91 1 false(unreach-call) .11  28 .64 1 true 2.9 280 26 -32 false(unreach-call) .32 11 4.0 1 false(unreach-call) 5.0 300 45 1 false(unreach-call) .13 11 1.7 1 false(unreach-call) 4.0 230 36 1 false(unreach-call) 4.1 250 40 1 false(unreach-call) 4.4 250 34 1 false(unreach-call) 7.7 300 61 1
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) .12  22 .77 1 false(unreach-call) .24 33 2.5 1 true 2.8 270 27 -32 true 2.9 270 25 -32 false(unreach-call) 2.5 260 26 1 false(unreach-call) .39 48 4.2 1 false(unreach-call) .080 28 .96 1 false(unreach-call) .078 28 .85 1 true 2.8 280 23 -32 false(unreach-call) .32 11 4.0 1 false(unreach-call) 4.9 300 44 1 false(unreach-call) .16 11 1.5 1 false(unreach-call) 4.1 240 36 1 false(unreach-call) 4.2 250 36 1 false(unreach-call) 4.1 250 34 1 false(unreach-call) 7.2 280 61 1
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true .10  22 .82 2 true .42 33 3.2 2 true 2.8 270 25 2 true 2.6 260 25 2 true 2.6 270 24 2 true 3.1  260 29   2 true .070 26 .89 2 true .071 26 .80 2 false(unreach-call) 2.9 280 26 -16 unknown .26 11 3.0 0 true 3.6 230 34 2 true .12 11 1.3 2 true 4.5 270 38 2 true 4.2 250 38 2 true 4.3 270 37 2 true 7.7 270 71 2
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true .12  22 .84 2 true .40 33 4.6 2 true 3.0 270 25 2 true 2.8 270 25 2 true 2.4 250 22 2 true 3.2  250 28   2 true .089 26 .69 2 true .076 26 .87 2 false(unreach-call) 3.1 270 22 -16 unknown .30 11 3.4 0 true 3.7 230 36 2 true .15 11 1.4 2 true 8.7 280 67 2 true 8.3 250 64 2 true 8.9 290 70 2 true 7.8 260 67 2
bitvector-regression/signextension2_true-unreach-call_true-termination.c true .12  22 .74 2 true .40 33 4.3 2 true 2.8 270 24 2 true 2.7 270 23 2 true 2.3 240 18 2 true 480    250 6100   2 true .072 26 .81 2 true .078 26 .77 2 false(unreach-call) 3.0 280 30 -16 unknown .26 11 3.2 0 true 3.7 220 31 2 true .12 11 1.5 2 true 4.5 280 35 2 true 4.5 260 36 2 true 4.7 290 39 2 true 8.1 270 69 2
bitvector-regression/signextension_true-unreach-call_true-termination.c true .12  22 .76 2 true .41 33 4.2 2 true 2.9 270 25 2 true 2.8 270 29 2 true 2.3 250 20 2 true 3.0  250 31   2 true .097 26 .74 2 true .097 26 .84 2 false(unreach-call) 2.8 280 26 -16 unknown .29 11 3.1 0 true 3.9 240 33 2 true .15 11 1.5 2 true 4.8 290 37 2 true 4.4 260 34 2 true 4.7 290 41 2 true 8.0 260 71 2
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) .12  24 1.1  1 false(unreach-call) .25 33 2.3 1 true 9.8 480 78 -32 true 14   600 100 -32 false(unreach-call) 5.3 280 46 1 false(unreach-call) 1.2  77 14   1 false(unreach-call) .55  28 4.8  1 false(unreach-call) .60  28 4.8  1 true 31   2100 230 -32 false(unreach-call) .42 11 4.6 1 false(unreach-call) 5.6 320 50 1 false(unreach-call) .16 11 2.0 1 false(unreach-call) 7.2 340 63 1 false(unreach-call) 5.9 300 52 1 false(unreach-call) 13   550 110 1 false(unreach-call) 23   430 190 1
bitvector-loops/overflow_false-unreach-call1.i timeout 900     1300 11000    0 out of memory 310    15000 4300   0 true 3.1 280 27 -32 true 3.3 270 33 -32 timeout 900   6800 9300 0 unknown 54    75 710   0 timeout 900     11000 11000    0 timeout 900     11000 12000    0 true 2.8 280 25 -32 unknown 890    11 13000   0 false(unreach-call) 4.9 300 41 1 false(unreach-call) .16 11 1.6 1 timeout 900   710 12000 0 timeout 900   2000 11000 0 timeout 900   1500 9700 0 false(unreach-call) 11   280 84 1
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) .54  37 6.0  1 false(unreach-call) 1.0  34 8.9 0 true 3.4 280 31 -32 true 3.2 270 28 -32 false(unreach-call) 210   1400 2700 1 false(unreach-call) 8.0  100 100   0 false(unreach-call) 2.1   30 18    0 false(unreach-call) 2.1   29 20    0 true 7.7 450 60 -32 true 2.7  14 35   -32 false(unreach-call) 13   460 130 0 false(unreach-call) .41 13 5.3 0 false(unreach-call) 470   780 5400 1 timeout 900   4600 13000 0 false(unreach-call) 550   2000 8400 0 false(unreach-call) 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 78000 90000 -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 710 28000 7800 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 550 20000 6200 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 8200 1600 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 160 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 160 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 18000 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 50 3700 390 -192 3 74   47 960 -96 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 21 270 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