Tool 2LS 0.3.4 CBMC Ceagle AbsRef 1.0.0 CPAchecker 1.4-svcomp16c CPAchecker 1.4-svn 18373 CPAchecker 1.4-svcomp16c ESBMC ESBMC version 2.0.0 64-bit x86_64 linux DepthK ESBMC+DepthK version 2.1 Forest svc_16_20151108 impara 0.45 LCTD PAC-MAN SeaHorn-F16 0.1.0 SMACK+Corral 1.5.2 symbiotic 3.0.1 ULTIMATE Automizer cfb9fd9e ULTIMATE Kojak fd30d3d8
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24] [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23] [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24] [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24] [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic Linux 4.2.0-23-generic Linux 4.2.0-22-generic Linux 4.2.0-23-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]] 2016-01-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]] 2016-01-04 05:59:47 CET [[ 2016-01-15 08:28:20 CET ]] [[ 2016-01-15 21:58:46 CET ]] 2016-01-04 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]] 2016-01-04 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]] 2016-01-04 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]] 2016-01-04 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]] 2016-01-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]] 2016-01-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 CET ]] 2016-01-09 23:49:59 CET [[ 2016-01-15 09:05:13 CET ]] [[ 2016-01-15 22:20:31 CET ]] 2016-01-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]] 2016-01-07 07:06:46 CET [[ 2016-01-15 09:15:21 CET ]] [[ 2016-01-15 22:25:37 CET ]] 2016-01-13 07:33:23 CET [[ 2016-01-15 09:22:08 CET ]] [[ 2016-01-15 22:28:32 CET ]] 2016-01-13 15:22:34 CET [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]] 2016-01-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]] 2016-01-07 09:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 CET ]] 2016-01-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 CET ]] 2016-01-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 CET ]]
Run set 2ls.sv-comp16.BitVectorsReach cbmc.sv-comp16.BitVectorsReach ceagle-absref.sv-comp16.BitVectorsReach cpa-bam.sv-comp16.BitVectorsReach cpa-kind.sv-comp16.BitVectorsReach cpa-refsel.sv-comp16.BitVectorsReach cpa-seq.sv-comp16.BitVectorsReach esbmc.sv-comp16.BitVectorsReach esbmcdepthk.sv-comp16.BitVectorsReach forest.sv-comp16.BitVectorsReach impara.sv-comp16.BitVectorsReach lctd.sv-comp16 pacman.sv-comp16.BitVectorsReach seahorn.sv-comp16.BitVectorsReach smack.sv-comp16.BitVectorsReach symbiotic3.sv-comp16.BitVectorsReach uautomizer.sv-comp16.BitVectorsReach ukojak.sv-comp16.BitVectorsReach
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ceagle-absref.2016-01-04_0559.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ceagle-absref.2016-01-04_0559.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--k-induction -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -svcomp [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/lctd.2016-01-07_0706.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lctd.2016-01-07_0706.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/pacman.2016-01-13_0733.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/pacman.2016-01-13_0733.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
bitvector/byte_add_false-unreach-call.i witness unconfirmed .44  28 false(reach) .30  25 unknown .32  5.9 timeout 900   1400 false(reach) 16   590 timeout 900   1300 false(reach) 87   3700 false(reach) 810     5100 witness timeout 4.2  170 true 2.5  39 false(reach) 3.5   24 witness unconfirmed 9.5   280   witness unconfirmed 1.6 110 witness timeout .64 62 false(reach) 6.8 140 witness timeout 35     9.1 false(reach) 51   530 timeout 46   720
bitvector/byte_add_1_true-unreach-call.i true .60  31 true 5.8   100 unknown .21  5.9 true 47   920 true 23   640 timeout 900   810 true 38   1500 true .81  69 true 1.4  26 true .69 38 true 7.7   24 unknown 1.6   38   true 640   160 false(reach) .57 47 true 23   160 true 250     8.2 timeout 900   2300 timeout 34   540
bitvector/byte_add_2_true-unreach-call.i true .61  30 true 6.0   110 unknown .21  5.7 timeout 900   1500 true 22   540 timeout 900   810 true 92   3800 true .78  70 true 1.3  26 true 130    1800 true 8.2   24 unknown 7.3   150   true 660   160 false(reach) .58 49 true 24   160 true 460     8.4 timeout 900   5100 timeout 31   430
bitvector/gcd_1_true-unreach-call.i true .35  27 true 12     570 true .30  5.9 true 9.6 240 true 19   730 true 9.9 230 true 21   790 true 2.3   160 true 3.9  110 true .48 39 true 1.1   29 unknown 1.1   68   true 680   200 false(reach) .29 39 true 2.9 73 true 36     7.9 error 28   400 error 8.4 320
bitvector/gcd_2_true-unreach-call.i true 1.1   39 true 12     580 unknown .43  6.0 true 8.5 230 true 300   3800 true 11   250 true 270   3000 true 54     240 true 85    110 true 1.6  38 true 2.2   27 true 1.3   85   true 710   210 false(reach) .33 39 true 2.9 71 unknown .51  8.2 error 170   570 error 10   350
bitvector/gcd_3_true-unreach-call.i true 1.2   40 true 13     570 unknown .54  6.1 true 420   680 true 270   3700 true 380   340 true 280   2800 true 49     240 true 200    120 true 1.7  38 timeout 900     4000 unknown .50  37   true 680   210 false(reach) .30 39 true 2.8 70 unknown .60  8.2 timeout 900   1000 error 8.6 320
bitvector/gcd_4_true-unreach-call.i true 1.5   41 true .88  24 unknown .21  9.1 true 4.3 230 true 6.7 340 true 3.7 210 true 2.9 180 true .067 13 true .69 22 true 1.0  39 true .15  23 unknown .55  41   true 670   200 false(reach) .49 41 true 3.4 75 true 18     5.8 error 52   430 error 9.5 330
bitvector/interleave_bits_true-unreach-call.i true 1.1   57 true 1.1   24 unknown .084 5.6 true 7.0 420 true 18   570 true 8.2 400 true 22   700 true .12  13 true 4.9  31 true .55 38 true .22  23 unknown .52  41   true 690   210 false(reach) .38 42 true 2.2 73 true 8.0   6.5 error 100   430 true 38   520
bitvector/jain_1_true-unreach-call.i timeout 900     1300 true 29     5800 unknown .080 5.5 true 3.9 230 timeout 900   11000 true 3.9 220 true 310   6200 true .23  19 true .54 41 false(reach) 56    38 timeout 900     290 true .88  55   out of memory 14   15000 true .28 37 true 880   110 timeout 870     110   true 9.0 320 true 8.2 320
bitvector/jain_2_true-unreach-call.i timeout 900     1600 true 59     12000 unknown .11  5.8 true 4.0 220 timeout 900   13000 true 4.0 220 true 310   6000 true .27  27 true 11    79 true 110    84 timeout 900     280 unknown .60  45   out of memory 19   15000 true .28 37 true 880   100 timeout 900     61   true 12   350 true 9.4 320
bitvector/jain_4_true-unreach-call.i timeout 900     1800 true 74     14000 unknown .070 6.0 true 3.9 230 timeout 900   14000 true 4.2 220 true 310   7000 true .33  33 true 150    170 unknown .53 38 timeout 900     250 unknown .44  34   out of memory 20   15000 true .19 27 timeout 880   140 timeout 900     79   true 23   370 true 10   320
bitvector/jain_5_true-unreach-call.i timeout 900     1500 true 1.1   24 unknown .13  5.7 timeout 900   880 timeout 900   7900 timeout 900   4600 timeout 900   5500 true .098 12 true .41 21 true 16    38 timeout 900     77 true .90  52   out of memory 42   15000 true .23 28 timeout 900   700 timeout 900     5.7 true 9.7 330 timeout 62   1200
bitvector/jain_6_true-unreach-call.i timeout 900     1900 true 58     11000 unknown .12  5.9 true 4.1 230 timeout 900   13000 true 4.0 220 true 310   7000 true .42  34 true 140    170 true .50 38 timeout 900     200 true 1.0   76   out of memory 21   15000 true .22 28 timeout 880   110 timeout 900     80   error 36   390 true 9.1 320
bitvector/jain_7_true-unreach-call.i timeout 900     1800 true 30     4200 unknown .069 5.6 true 5.8 230 timeout 900   10000 true 14   230 true 310   5500 true .36  28 true 12    55 unknown .59 38 timeout 900     110 unknown .78  47   out of memory 21   15000 true .15 28 timeout 880   94 timeout 900     73   error 29   360 true 9.4 340
bitvector/modulus_true-unreach-call.i true 1.2   41 true 220     14000 unknown .15  5.8 timeout 900   470 true 45   3700 timeout 900   480 true 46   3700 unknown 900     3400 true 130    720 true .64 39 timeout 900     350 unknown .59  42   true 670   180 false(reach) .31 40 true 47   160 timeout 900     54   error 95   400 error 67   380
bitvector/num_conversion_1_true-unreach-call.i true .24  25 true 1.1   24 unknown .12  5.7 true 3.7 230 true 6.2 280 true 3.7 210 true 3.3 190 true .075 13 true 1.7  22 true 1.4  38 true .16  23 unknown .50  38   true 680   210 true .19 30 true 2.6 64 true 18     5.6 timeout 900   530 true 55   390
bitvector/num_conversion_2_true-unreach-call.i true .26  25 true 1.1   24 unknown .098 5.6 true 16   640 true 6.4 290 timeout 900   1700 true 13   660 true .075 13 true 2.4  22 unknown .50 38 true 170     43 unknown .32  19   true 660   170 false(reach) .26 38 true 2.6 67 true 460     10   timeout 900   540 timeout 270   870
bitvector/parity_true-unreach-call.i true 3.7   40 true 7.5   42 unknown .12  5.9 timeout 900   2100 true 74   1300 timeout 900   2000 true 67   1000 true 1.3   15 unknown 890    240 true 3.0  38 timeout 900     11000 true 1.4   56   true 660   170 false(reach) .27 39 true 880   290 true 130     8.9 timeout 900   1300 timeout 43   360
bitvector/sum02_true-unreach-call.i timeout 900     1300 true 2.5   40 unknown .087 5.7 timeout 900   970 timeout 900   5900 timeout 900   860 timeout 900   4900 error (1) 14     490 unknown 47    27 unknown .61 38 timeout 900     80 unknown .59  36   out of memory 17   15000 false(reach) .31 40 true 880   390 timeout 900     17   unknown 9.2 320 error 33   320
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c false(reach) 86     340 false(reach) 5.1   180 unknown .26  6.3 timeout 900   2500 false(reach) 44   1100 false(reach) 19   690 false(reach) 13   660 false(reach) 810     6200 witness timeout 64    290 true 3.2  39 witness timeout 4.7   27 unknown 6.9   130   out of memory 29   15000 false(reach) 3.1  81 witness timeout 17   210 witness unconfirmed 5.3   21   false(reach) 40   530 timeout 30   490
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c false(reach) 54     330 false(reach) 4.6   150 unknown .46  6.3 false(reach) 51   1300 false(reach) 53   1400 false(reach) 33   900 false(reach) 17   710 timeout 910     7300 false(reach) 54    230 unknown .81 39 witness timeout 9.9   29 unknown 6.5   140   true 670   170 witness timeout 9.9  81 witness timeout 40   240 timeout 900     19   false(reach) 150   560 timeout 30   500
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c witness timeout 32     220 witness timeout 1.0   55 unknown .50  6.3 timeout 900   1300 false(reach) 31   900 false(reach) 10   490 false(reach) 9.9 390 witness timeout 810     7000 false(reach) 53    230 true 11    39 witness timeout .93  26 unknown 1.0   37   witness unconfirmed 1.9 110 false(reach) 1.4  76 witness timeout 11   180 true 500     20   unknown 30   390 timeout 45   560
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c timeout 900     310 true 850     1100 unknown .27  6.3 timeout 900   1500 true 48   1100 true 34   830 true 28   1200 true 70     1800 true 7.5  280 true 2.9  39 true 69     33 unknown .98  40   true 670   170 true 10    72 true 210   320 timeout 900     38   true 43   550 timeout 28   500
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 59     360 true 850     1100 unknown .45  6.3 true 60   1100 true 41   1000 true 32   840 true 27   1300 true 61     1500 true 5.2  220 true .43 17 true 33     29 unknown .62  19   true 660   160 true 77    110 true 170   290 true 93     43   true 55   610 timeout 28   480
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 61     340 true 850     3000 unknown .45  6.4 timeout 900   2500 true 35   930 true 32   870 true 30   1500 true 73     1600 true 6.8  210 unknown .75 39 true 41     31 unknown .91  20   true 680   170 true 33    94 true 180   300 true 510     20   true 29   780 timeout 31   500
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c timeout 900     880 true 850     600 unknown .38  6.3 timeout 900   3600 timeout 900   4800 timeout 900   1200 timeout 900   3900 unknown 890     2800 unknown 890    430 true .98 39 timeout 900     390 unknown 1.1   44   out of memory 69   15000 true 59    77 true 880   430 timeout 900     22   timeout 900   1200 timeout 580   940
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c timeout 900     7400 true 850     770 unknown .43  6.3 timeout 900   3600 true 35   890 timeout 900   1900 true 38   2400 true 70     1900 true 6.1  280 true .90 39 timeout 900     130 unknown .76  19   true 670   170 true 170    93 true 880   530 timeout 900     21   true 31   690 timeout 60   1000
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c timeout 900     6700 true 850     670 unknown .57  6.3 timeout 900   1400 true 190   3400 true 720   2000 true 100   3700 unknown 890     1600 true 11    240 true 1.3  39 timeout 900     250 unknown .94  27   out of memory 19   15000 true 140    85 true 880   520 timeout 900     20   true 72   3900 timeout 53   1000
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c timeout 900     6700 true 850     700 unknown .38  6.4 timeout 900   910 true 200   4100 true 700   1900 true 100   3600 unknown 890     1700 true 13    250 true 600    110 timeout 900     250 unknown 1.2   40   true 660   160 true 91    86 true 880   560 timeout 900     20   true 68   2900 timeout 56   860
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c timeout 900     7200 true 850     700 unknown .40  6.3 timeout 900   2500 timeout 900   5900 true 32   880 true 35   2300 true 70     1900 true 9.6  300 true 3.0  40 timeout 900     130 unknown .87  19   true 670   170 true 50    96 true 880   650 timeout 900     20   true 28   640 timeout 53   520
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c timeout 900     7200 true 850     710 unknown .51  6.3 timeout 900   2500 timeout 900   5900 true 31   860 true 34   2300 true 65     1900 true 11    300 unknown .83 39 timeout 900     130 unknown .94  41   true 670   160 true 140    140 true 880   610 timeout 900     19   true 28   550 timeout 53   540
bitvector/soft_float_1_true-unreach-call.c.cil.c true .25  30 true 850     190 unknown .23  5.9 timeout 900   3700 timeout 900   5200 timeout 900   750 true 320   4300 true 1.2   120 true 1.9  43 true 410    39 true 16     34 unknown 35     42   true 660   150 false(reach) .51 59 true 3.4 88 timeout 900     140   error 140   630 timeout 38   590
bitvector/soft_float_2_true-unreach-call.c.cil.c true .21  29 true 850     190 unknown .22  5.9 timeout 900   4300 true 21   540 true 42   800 true 21   610 true .77  120 true .71 41 true 1.6  39 timeout 900     160 unknown 1.3   39   true 660   150 true .47 53 true 3.2 87 timeout 900     9.5 true 17   470 timeout 41   660
bitvector/soft_float_3_true-unreach-call.c.cil.c true 18     210 true 850     170 unknown .29  6.0 timeout 900   3800 timeout 900   7100 timeout 900   490 timeout 900   7600 true .98  120 true 17    45 true 2.4  39 timeout 900     110 true 1.9   77   true 650   150 false(reach) .45 54 true 21   130 timeout 900     9.1 timeout 900   1500 timeout 42   660
bitvector/soft_float_4_true-unreach-call.c.cil.c true 1.3   32 true 850     190 false(reach) .29  5.8 true 150   840 true 760   4200 timeout 900   740 true 510   4100 true 8.4   130 true 25    49 true .74 39 true 9.3   28 unknown 1.4   78   true 650   150 false(reach) .55 62 true 12   88 timeout 900     22   true 700   850 timeout 36   640
bitvector/soft_float_5_true-unreach-call.c.cil.c true .17  28 true 850     180 unknown .15  5.7 timeout 900   4600 true 22   540 true 7.9 290 true 24   680 true 1.0   120 true .75 41 unknown .66 39 true 1.7   31 unknown 1.6   69   true 660   160 true .48 52 true 2.7 87 timeout 900     9.4 true 16   340 timeout 42   610
bitvector-regression/implicitfloatconversion_false-unreach-call.i false(reach) .10  22 false(reach) .16  24 witness unconfirmed .096 5.9 false(reach) 3.2 230 false(reach) 4.1 230 false(reach) 3.8 230 false(reach) 3.6 200 false(reach) 3.2   220 false(reach) 3.1  170 false(reach) .51 38 false(reach) .12  23 unknown .64  40   witness unconfirmed 1.5 110 witness unconfirmed .19 34 false(reach) 2.9 68 witness unconfirmed .18  6.5 error 7.0 300 error 7.9 310
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) .12  22 false(reach) .11  24 true .085 5.6 false(reach) 3.9 220 false(reach) 4.0 230 false(reach) 3.2 220 false(reach) 3.0 200 false(reach) 3.7   210 false(reach) 2.9  160 false(reach) .61 38 false(reach) .087 23 unknown .72  38   witness unconfirmed 1.5 110 witness unconfirmed .20 34 false(reach) 2.8 72 witness unconfirmed .13  6.7 false(reach) 8.4 330 false(reach) 8.5 320
bitvector-regression/integerpromotion_false-unreach-call.i false(reach) .15  27 false(reach) .13  26 unknown .095 6.1 false(reach) 5.2 240 false(reach) 5.2 240 false(reach) 5.6 270 false(reach) 5.1 240 false(reach) 7.8   280 false(reach) 4.7  170 true .62 38 false(reach) .12  25 unknown .67  37   witness unconfirmed 1.5 110 witness unconfirmed .22 35 false(reach) 3.0 72 witness unconfirmed .18  6.8 false(reach) 14   350 false(reach) 15   350
bitvector-regression/signextension2_false-unreach-call.i false(reach) .11  25 false(reach) .12  26 unknown .090 6.0 false(reach) 5.1 250 false(reach) 5.1 240 false(reach) 5.6 260 false(reach) 4.9 230 false(reach) 8.5   300 false(reach) 4.3  180 unknown .50 38 false(reach) .092 25 unknown .62  41   witness unconfirmed 1.6 110 witness unconfirmed .20 34 false(reach) 3.1 70 witness unconfirmed .22  6.7 false(reach) 9.3 330 false(reach) 8.7 320
bitvector-regression/signextension_false-unreach-call.i false(reach) .11  25 false(reach) .10  26 unknown .11  6.0 false(reach) 5.2 240 false(reach) 5.1 240 false(reach) 4.7 260 false(reach) 4.3 240 false(reach) 11     340 false(reach) 4.9  170 unknown .55 39 false(reach) .12  25 witness unconfirmed .62  49   witness unconfirmed 1.5 110 witness unconfirmed .23 35 false(reach) 3.0 74 witness unconfirmed .23  6.7 false(reach) 8.5 320 false(reach) 11   360
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true .099 23 true 1.1   24 false(reach) .075 5.6 true 3.6 210 true 3.5 200 true 2.8 200 true 3.0 180 true .064 13 true .33 21 true .55 38 true .11  22 unknown .60  40   true 690   210 true .17 29 true 2.5 61 true .17  5.9 true 9.3 340 timeout 130   1100
bitvector-regression/integerpromotion_true-unreach-call.i true .11  25 true 1.2   26 unknown .088 6.0 true 3.5 220 true 4.4 210 true 4.2 220 true 4.0 190 true .096 17 true .70 28 true .72 39 true .11  25 unknown .62  40   true 710   210 true .19 29 true 2.0 65 true .076 5.7 true 15   350 timeout 150   1100
bitvector-regression/signextension2_true-unreach-call.i true .12  25 true 1.0   26 unknown .074 6.0 true 3.6 220 true 4.3 200 true 4.2 210 true 3.2 190 true .081 17 true .54 27 unknown .60 39 true .15  25 true .74  51   true 690   200 true .25 29 true 2.7 67 true .10  5.6 true 8.8 320 timeout 130   1300
bitvector-regression/signextension_true-unreach-call.i true .16  25 true 1.2   26 unknown .056 6.0 true 3.5 220 true 3.7 200 true 3.9 210 true 3.7 190 true .086 17 true .51 27 true .71 39 true .092 25 true .83  50   true 680   200 true .22 29 true 2.8 67 true .11  5.7 true 8.3 330 timeout 140   1100
bitvector-loops/diamond_false-unreach-call2.i false(reach) .15  25 false(reach) .19  25 unknown .19  5.7 false(reach) 6.0 360 false(reach) 6.7 380 false(reach) 5.1 250 false(reach) 4.4 230 false(reach) 13     360 false(reach) 3.5  160 false(reach) 1.8  39 false(reach) .68  23 unknown .56  41   witness unconfirmed 1.6 110 false(reach) .38 39 false(reach) 3.6 85 false(reach) .13  6.5 false(reach) 12   360 false(reach) 9.5 320
bitvector-loops/overflow_false-unreach-call1.i timeout 900     1200 true 1.2   24 unknown .098 5.6 timeout 900   780 timeout 900   8300 timeout 900   4600 timeout 900   4900 error (1) 78     3900 unknown 31    22 true .56 38 timeout 900     29 witness unconfirmed .64  50   out of memory 65   15000 witness timeout .20 34 error (1) 890   830 witness timeout .20  6.8 timeout 900   1100 timeout 42   630
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i false(reach) 2.5   49 false(reach) .47  25 unknown .082 5.9 timeout 900   12000 false(reach) 23   1400 timeout 900   14000 false(reach) 26   1100 error (1) 30     720 false(reach) 3.5  160 true .68 38 false(reach) 3.2   32 error (1) .058 2.6 true 670   160 true .34 38 witness unconfirmed 7.0 93 witness timeout 210     8.8 timeout 900   570 timeout 900   520
../../sv-benchmarks/c/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
total tasks 48 14000 51000 48 12000   74000 48 11     290   48 21000 69000 48 14000 150000 48 16000 52000 48 8400 110000 48 7600 54000 48 2900 6900 48 1400   3700 48 17000   19000 48 100   2600 48 20000 170000 48 800    2500 48 14000 10000 48 22000    1100   48 11000 38000 48 3600 27000
    correct results 31 300 2400 46 12000   74000 1 .30  5.9 26 850 10000 35 2400 40000 33 2200 16000 43 3900 87000 39 2200 25000 42 1000 5800 30 1300   3000 26 360   700 8 8.9 500 27 18000 4800 25 780    1500 39 9600 7400 15 2000    150   27 1500 18000 12 190 4200
        correct true 22 150 1500 36 12000   74000 1 .30  5.9 19 770 7600 24 2200 33000 24 2100 13000 32 3700 79000 31 530 12000 33 870 4100 27 1300   2900 18 360   500 8 8.9 500 27 18000 4800 22 770    1300 32 9600 6800 14 2000    150   19 1200 15000 7 140 2500
        correct false 9 140 870 10 11   540 0 7 79 2800 11 200 7000 9 90 3600 11 180 7900 8 1700 13000 9 130 1600 3 2.9 110 8 7.9 200 0 0 3 4.9  200 7 25 580 1 .13 6.5 8 290 3300 5 53 1700
    incorrect results 0 1 1.2 24 3 .45  17   0 0 0 0 0 0 7 74   270 0 0 2 1300 330 15 6.0  660 0 1 500    20   0 0
        incorrect true 0 1 1.2 24 1 .085 5.6 0 0 0 0 0 0 6 18   230 0 0 2 1300 330 1 .34 38 0 1 500    20   0 0
        incorrect false 0 0 2 .36  11   0 0 0 0 0 0 1 56   38 0 0 0 14 5.6  630 0 0 0 0
score (48 tasks, max score: 84) 53 50 -62 45 59 57 75 70 75 -151 44 16 -10 -209 71 -3 46 19
Run set 2ls.sv-comp16.BitVectorsReach cbmc.sv-comp16.BitVectorsReach ceagle-absref.sv-comp16.BitVectorsReach cpa-bam.sv-comp16.BitVectorsReach cpa-kind.sv-comp16.BitVectorsReach cpa-refsel.sv-comp16.BitVectorsReach cpa-seq.sv-comp16.BitVectorsReach esbmc.sv-comp16.BitVectorsReach esbmcdepthk.sv-comp16.BitVectorsReach forest.sv-comp16.BitVectorsReach impara.sv-comp16.BitVectorsReach lctd.sv-comp16 pacman.sv-comp16.BitVectorsReach seahorn.sv-comp16.BitVectorsReach smack.sv-comp16.BitVectorsReach symbiotic3.sv-comp16.BitVectorsReach uautomizer.sv-comp16.BitVectorsReach ukojak.sv-comp16.BitVectorsReach