Tool 2LS 0.3.4 CBMC 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 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]
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 21:37:22 CET ]] 2016-01-03 00:42:25 CET [[ 2016-01-15 21:54:19 CET ]] 2016-01-04 06:25:51 CET [[ 2016-01-15 21:59:57 CET ]] 2016-01-04 01:42:53 CET [[ 2016-01-15 22:02:40 CET ]] 2016-01-04 20:04:07 CET [[ 2016-01-15 22:05:37 CET ]] 2016-01-04 13:17:38 CET [[ 2016-01-15 22:10:37 CET ]] 2016-01-16 17:45:19 CET [[ 2016-01-17 00:39:38 CET ]] 2016-01-05 14:06:34 CET [[ 2016-01-15 22:17:52 CET ]] 2016-01-09 23:49:59 CET [[ 2016-01-15 22:20:31 CET ]] 2016-01-13 07:33:23 CET [[ 2016-01-15 22:28:32 CET ]] 2016-01-13 15:22:34 CET [[ 2016-01-15 22:30:28 CET ]] 2016-01-07 09:05:16 CET [[ 2016-01-15 22:36:10 CET ]] 2016-01-07 09:04:54 CET [[ 2016-01-15 22:39:28 CET ]] 2016-01-14 23:51:13 CET [[ 2016-01-15 22:41:15 CET ]] 2016-01-08 15:10:30 CET [[ 2016-01-15 22:43:29 CET ]]
Run set 2ls.sv-comp16.ArraysReach cbmc.sv-comp16.ArraysReach cpa-bam.sv-comp16.ArraysReach cpa-kind.sv-comp16.ArraysReach cpa-refsel.sv-comp16.ArraysReach cpa-seq.sv-comp16.ArraysReach esbmc.sv-comp16.ArraysReach esbmcdepthk.sv-comp16.ArraysReach forest.sv-comp16.ArraysReach pacman.sv-comp16.ArraysReach seahorn.sv-comp16.ArraysReach smack.sv-comp16.ArraysReach symbiotic3.sv-comp16.ArraysReach uautomizer.sv-comp16.ArraysReach ukojak.sv-comp16.ArraysReach
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --graphml-cex error-witness.graphml [[ ../../results-verified/cbmc.2016-01-03_0042.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 [[ ../../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 [[ ../../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 [[ ../../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 [[ ../../results-verified/cpa-seq.2016-01-04_1317.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 ]] [[ ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -svcomp [[ ../../results-verified/forest.2016-01-09_2349.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 [[ ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -w error-witness.graphml [[ ../../results-verified/smack.2016-01-07_0905.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 ]] [[ ../../results-verified/uautomizer.2016-01-14_2351.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)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i 47    15000 850    13000 3.6 210 4.6 240 3.1 210 160   4000 910     12000 890    380 24     920   45    2200 900    850 5.0 86 900     4300   900   1700 39   700
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 49    15000 22    15000 3.1 210 4.5 240 3.5 210 160   3600 87     15000 890    350 21     130   59    15000 900    520 3.9 99 900     5300   900   1400 54   1300
array-examples/sorting_bubblesort_false-unreach-call_ground.i 50    15000 22    15000 3.1 210 3.7 240 3.5 210 160   3600 88     15000 890    450 330     130   58    15000 900    520 3.8 99 900     5300   900   1400 53   1000
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 46    15000 77    13000 3.5 200 3.8 240 3.7 210 160   3500 51     15000 890    850 29     970   1.6  110 900    1000 28   830 900     810   900   1900 51   850
array-examples/sorting_selectionsort_false-unreach-call_ground.i 46    15000 78    13000 3.0 200 4.6 240 3.5 210 160   2400 51     15000 890    850 24     130   1.8  120 900    970 320   1100 900     870   900   2100 50   1300
array-examples/standard_allDiff2_false-unreach-call_ground.i 520    15000 850    1800 3.5 200 4.4 230 3.4 210 160   3600 45     15000 890    4200 20     140   59    15000 .30 42 8.9 99 900     650   900   2100 55   970
array-examples/standard_copy1_false-unreach-call_ground.i 45    15000 34    15000 2.9 210 4.3 230 2.9 210 150   3500 95     4000 220    76 4.2   130   1.5  120 .26 28 3.1 79 1.2   12   900   1300 53   830
array-examples/standard_copy2_false-unreach-call_ground.i 43    15000 30    15000 3.5 210 4.3 230 3.5 210 150   3500 100     4100 680    130 5.6   120   850    150 .40 40 3.4 75 20     93   900   960 52   1000
array-examples/standard_copy3_false-unreach-call_ground.i 40    15000 38    15000 3.6 210 4.2 230 3.5 200 160   3600 110     4200 890    180 110     270   860    150 .28 40 3.7 79 22     160   900   1700 53   1100
array-examples/standard_copy4_false-unreach-call_ground.i 39    15000 44    15000 3.4 200 4.4 240 3.5 210 150   3600 120     4200 890    210 160     340   870    150 .30 40 3.7 83 22     180   900   1000 52   1500
array-examples/standard_copy5_false-unreach-call_ground.i 37    15000 49    15000 2.9 210 3.8 230 3.5 210 160   2400 130     4200 890    240 10     140   870    160 .29 40 3.8 87 23     200   900   1200 50   990
array-examples/standard_copy6_false-unreach-call_ground.i 35    15000 56    15000 3.5 210 4.4 230 3.5 210 160   3500 140     4200 890    260 12     140   870    160 .28 40 4.1 89 24     230   900   2000 52   1400
array-examples/standard_copy7_false-unreach-call_ground.i 34    15000 46    15000 3.5 210 4.4 240 3.0 210 160   3600 150     4300 890    290 13     150   870    170 .31 40 4.0 87 24     250   900   1900 52   1100
array-examples/standard_copy8_false-unreach-call_ground.i 33    15000 51    15000 3.0 210 4.3 240 3.7 210 160   3600 150     4400 890    310 14     130   880    170 .30 40 3.9 92 26     280   900   1800 63   1200
array-examples/standard_copy9_false-unreach-call_ground.i 32    15000 55    15000 3.6 210 4.5 240 3.5 210 160   3500 160     4400 890    330 170     670   880    180 .36 40 4.4 86 26     300   900   2000 59   820
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 42    15000 32    15000 3.1 210 4.3 230 3.5 210 160   3200 110     3000 690    180 5.0   120   1.6  110 900    430 3.4 81 19     49   900   1000 52   1100
array-examples/standard_init1_false-unreach-call_ground.i 46    12000 32    15000 3.4 200 4.2 230 3.3 200 150   3100 90     1600 200    75 2.6   130   1.6  110 900    410 3.1 79 18     27   900   1000 53   1100
array-examples/standard_init2_false-unreach-call_ground.i 46    15000 26    15000 3.5 210 4.4 240 3.0 200 160   3600 100     1900 510    130 3.0   130   1.5  110 900    460 3.4 77 19     46   900   1600 53   790
array-examples/standard_init3_false-unreach-call_ground.i 46    15000 30    15000 2.9 210 4.3 240 3.5 210 160   3600 110     3000 890    180 4.1   130   1.7  110 900    450 3.4 80 19     65   900   1100 52   770
array-examples/standard_init4_false-unreach-call_ground.i 45    15000 35    15000 3.0 200 4.2 240 2.9 200 160   2400 120     3100 890    190 4.7   130   1.7  110 900    460 3.5 75 20     84   900   1700 49   990
array-examples/standard_init5_false-unreach-call_ground.i 46    15000 40    15000 3.0 210 3.6 240 3.4 210 160   3600 120     3100 890    210 5.6   120   1.7  110 900    450 3.6 79 20     100   900   1600 51   860
array-examples/standard_init6_false-unreach-call_ground.i 46    15000 45    15000 3.0 210 4.3 240 3.4 210 160   3600 140     4000 890    220 6.1   130   1.9  120 900    460 3.6 79 21     120   900   2600 49   1000
array-examples/standard_init7_false-unreach-call_ground.i 47    15000 49    15000 3.4 210 4.3 240 3.4 210 160   3600 150     4000 890    230 7.2   130   1.9  120 900    450 3.8 84 21     140   900   1500 55   890
array-examples/standard_init8_false-unreach-call_ground.i 46    15000 39    15000 3.6 210 4.4 240 3.5 210 160   3600 150     4000 890    240 7.3   130   1.7  120 900    460 3.9 83 22     160   900   1300 59   1200
array-examples/standard_init9_false-unreach-call_ground.i 45    15000 40    15000 3.5 210 3.6 240 3.6 210 160   3200 150     3900 890    250 8.6   130   1.8  120 900    460 3.9 90 22     180   900   1600 60   910
array-examples/standard_minInArray_false-unreach-call_ground.i 410    15000 5.1  420 3.5 210 4.0 240 3.4 210 160   3500 97     4000 51    53 3.4   130   1.7  120 900    400 3.6 78 900     840   900   1100 53   1500
array-examples/standard_partition_false-unreach-call_ground.i 40    15000 110    14000 3.5 210 4.5 240 3.0 220 160   3500 140     4200 890    190 6.8   120   1.7  120 900    540 3.9 93 16     15000   900   1500 55   900
array-examples/standard_running_false-unreach-call.i 45    15000 37    15000 2.9 210 3.6 230 3.0 210 160   3600 97     3900 890    69 6.0   130   860    150 900    310 3.4 81 900     2800   900   1400 54   830
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i 47    15000 1.9  25 3.1 210 3.9 240 3.6 220 160   3600 31     2800 .42 22 7.0   120   850    150 .27 25 4.0 93 900     54   12   340 58   1200
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 47    15000 850    9900 3.5 210 4.5 240 3.2 210 160   3800 900     13000 .79 36 5.5   130   860    150 900    500 880   200 900     1800   900   2100 39   780
array-examples/relax_true-unreach-call.i .73 41 510    14000 4.4 230 5.1 260 4.5 220 95   2300 890     260 10    63 .059 4.0 .17 13 .56 54 880   300 .12  7.0 900   1100 46   520
array-examples/sanfoundry_02_true-unreach-call_ground.i 360    15000 5.6  470 3.6 200 4.4 230 3.6 210 150   3600 890     460 .92 23 7.2   130   870    160 900    510 3.1 70 900     830   900   1800 54   1100
array-examples/sanfoundry_10_true-unreach-call_ground.i 51    15000 130    13000 900   850 900   5600 900   4600 900   3500 610     360 .74 36 .60  38   860    150 900    500 6.9 90 .19  6.5 900   1200 47   950
array-examples/sanfoundry_24_true-unreach-call.i 25    5700 26    780 3.4 200 3.4 240 3.5 210 5.0 360 .32  51 .38 22 3.7   120   690    210 .27 36 2.6 73 900     1700   10   320 9.6 330
array-examples/sanfoundry_27_true-unreach-call_ground.i 530    15000 5.2  420 3.3 210 3.7 240 3.5 210 150   3600 890     310 .50 22 3.8   130   850    150 900    400 3.8 78 900     730   900   1400 54   1400
array-examples/sanfoundry_43_true-unreach-call_ground.i .14 23 1.3  26 3.5 200 3.6 230 2.9 210 94   3500 .15  13 .39 21 43     130   820    150 .16 24 2.5 64 .091 5.9 8.3 330 8.0 310
array-examples/sorting_bubblesort_true-unreach-call_ground.i 49    15000 23    15000 3.5 210 4.3 240 3.4 210 160   3500 88     15000 890    460 22     130   58    15000 900    520 28   140 900     5200   900   1600 55   1200
array-examples/sorting_selectionsort_true-unreach-call_ground.i 47    15000 77    13000 3.6 210 3.9 230 3.4 210 160   3500 51     15000 890    840 15     9.4 44    15000 900    960 880   1000 900     880   900   1700 50   790
array-examples/standard_compareModified_true-unreach-call_ground.i 46    15000 37    15000 3.5 210 3.7 240 2.9 210 160   2400 .46  65 .39 22 7.0   120   870    160 900    520 3.0 74 75     11000   900   1400 55   870
array-examples/standard_compare_true-unreach-call_ground.i 350    15000 7.0  760 3.5 210 4.4 240 3.4 210 150   3600 .30  36 .40 22 3.8   120   800    150 900    390 3.3 79 900     2700   900   1200 57   1100
array-examples/standard_copy1_true-unreach-call_ground.i 48    15000 34    15000 3.5 200 3.7 240 3.3 210 150   3500 .19  16 .38 21 3.5   120   840    150 .39 40 3.4 77 19     110   900   2800 54   890
array-examples/standard_copy2_true-unreach-call_ground.i 43    15000 30    15000 3.5 200 4.2 230 3.4 210 150   2400 .19  18 .46 21 5.7   130   860    150 .30 40 3.5 87 20     130   900   2500 50   1000
array-examples/standard_copy3_true-unreach-call_ground.i 41    15000 36    15000 2.7 210 3.7 240 3.0 210 150   3500 .23  19 .40 21 6.9   130   860    150 .29 40 3.6 80 21     160   900   900 49   970
array-examples/standard_copy4_true-unreach-call_ground.i 39    15000 43    15000 3.4 210 3.7 230 3.4 210 160   3600 .28  21 .42 22 7.8   120   870    150 .33 40 3.7 88 21     180   900   1200 49   900
array-examples/standard_copy5_true-unreach-call_ground.i 37    15000 50    15000 3.6 210 3.8 230 3.4 210 160   3600 .32  22 .48 22 10     140   870    160 .30 40 3.8 91 22     200   900   2600 52   830
array-examples/standard_copy6_true-unreach-call_ground.i 35    15000 56    15000 3.6 210 3.6 240 3.5 210 150   3600 .38  23 .42 22 11     120   880    160 .30 40 4.0 90 23     230   900   1300 49   1600
array-examples/standard_copy7_true-unreach-call_ground.i 34    15000 47    15000 3.6 200 4.5 230 3.4 210 160   3600 .39  25 .49 22 13     120   870    170 .25 40 4.2 93 23     260   900   1400 51   1100
array-examples/standard_copy8_true-unreach-call_ground.i 33    15000 51    15000 3.1 210 3.7 240 3.5 210 160   3600 .43  26 .40 22 14     120   880    170 .31 40 4.4 97 24     280   900   2900 59   820
array-examples/standard_copy9_true-unreach-call_ground.i 32    15000 55    15000 3.6 210 3.8 230 3.4 210 160   3500 .49  27 .42 22 17     130   880    180 .31 40 4.6 90 25     300   900   1600 58   1200
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 43    15000 32    15000 3.5 210 3.7 240 2.8 210 160   2000 .27  19 .44 22 490     150   860    150 900    470 4.0 82 20     110   900   1400 47   1100
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 42    15000 37    15000 2.9 210 3.6 230 2.8 210 160   3600 .32  21 .43 22 7.3   120   870    150 900    450 4.9 91 21     130   900   1800 49   790
array-examples/standard_copyInitSum_true-unreach-call_ground.i 42    15000 33    15000 3.0 210 4.7 230 3.5 210 160   3600 .27  19 .41 22 5.1   120   890    170 900    460 3.8 81 21     150   900   1600 53   1100
array-examples/standard_copyInit_true-unreach-call_ground.i 42    15000 28    15000 3.0 210 3.8 240 3.5 210 160   2300 .19  18 .41 21 3.5   120   860    150 900    410 3.5 75 20     86   900   1400 52   940
array-examples/standard_find_true-unreach-call_ground.i 270    15000 8.4  440 3.5 200 4.1 240 2.9 210 5.7 360 .77  67 .48 23 2.7   130   690    210 .33 43 3.5 78 900     68   900   1200 54   680
array-examples/standard_init1_true-unreach-call_ground.i 46    12000 32    15000 2.9 210 4.3 240 2.8 210 150   3600 .15  16 .37 21 2.2   130   840    150 900    450 3.2 79 19     65   900   1100 51   1100
array-examples/standard_init2_true-unreach-call_ground.i 46    15000 26    15000 2.9 210 3.5 240 3.4 200 160   3600 .17  17 .39 21 2.8   120   860    150 900    460 3.2 77 20     83   900   1300 54   1100
array-examples/standard_init3_true-unreach-call_ground.i 47    15000 31    15000 3.2 210 3.7 230 3.5 210 160   3600 .17  19 .46 22 4.0   130   860    150 900    450 3.3 76 19     100   900   1100 46   970
array-examples/standard_init4_true-unreach-call_ground.i 46    15000 35    15000 3.5 210 4.3 230 3.5 210 160   3600 .18  20 .38 22 110     130   870    160 900    450 3.4 74 20     120   900   2000 49   830
array-examples/standard_init5_true-unreach-call_ground.i 46    15000 39    15000 3.4 210 4.2 230 3.4 210 160   3600 .23  21 .46 22 17     130   870    160 900    450 3.2 79 21     140   900   1200 51   880
array-examples/standard_init6_true-unreach-call_ground.i 46    15000 45    15000 3.5 210 3.6 240 3.4 210 160   2100 .26  22 .44 22 6.0   130   880    160 900    450 3.8 88 22     160   900   1100 57   1200
array-examples/standard_init7_true-unreach-call_ground.i 46    15000 49    15000 3.1 200 3.8 240 3.6 210 160   2400 .27  24 .43 22 78     130   880    160 900    450 4.0 85 22     180   900   1100 52   1100
array-examples/standard_init8_true-unreach-call_ground.i 46    15000 38    15000 3.0 210 4.5 240 3.5 210 160   3600 .29  25 .47 22 7.2   120   880    170 900    460 3.9 86 23     200   900   1200 65   1300
array-examples/standard_init9_true-unreach-call_ground.i 46    15000 41    15000 3.4 210 4.6 230 3.6 210 160   3200 .25  26 .41 22 8.1   120   880    170 900    460 3.8 94 23     220   900   1400 60   1200
array-examples/standard_maxInArray_true-unreach-call_ground.i 540    15000 4.8  410 2.8 200 4.2 230 3.5 210 150   1300 890     280 .47 22 840     130   850    150 900    400 3.7 78 900     810   900   1500 51   1000
array-examples/standard_minInArray_true-unreach-call_ground.i 340    15000 4.9  410 3.5 210 4.3 240 3.4 210 160   2300 890     250 .42 21 3.1   130   850    150 900    390 3.6 82 900     810   900   1300 53   1500
array-examples/standard_palindrome_true-unreach-call_ground.i 50    15000 32    15000 3.6 200 3.7 230 3.4 210 150   3600 .26  17 .44 21 4.1   120   800    150 900    410 3.1 71 18     61   900   1200 51   990
array-examples/standard_partial_init_true-unreach-call_ground.i 45    15000 80    14000 3.5 210 3.7 230 3.4 200 160   3500 890     420 .40 22 850     210   870    150 900    680 150   100 900     2700   900   1200 56   1100
array-examples/standard_partition_original_true-unreach-call_ground.i 38    15000 68    14000 3.5 210 4.0 230 3.5 210 160   3500 890     860 .44 22 6.5   120   850    150 900    240 84   98 15     15000   900   2300 57   1300
array-examples/standard_partition_true-unreach-call_ground.i 40    15000 110    14000 3.6 210 3.6 240 3.4 210 160   3500 890     560 .34 22 13     210   870    150 900    410 27   92 17     15000   900   2500 55   1200
array-examples/standard_password_true-unreach-call_ground.i 350    15000 7.0  760 3.6 200 4.3 230 2.9 210 160   2000 .30  36 .47 21 4.2   120   810    150 900    390 3.3 80 900     2700   900   940 54   790
array-examples/standard_reverse_true-unreach-call_ground.i 49    15000 34    15000 3.0 210 4.2 240 3.6 210 150   3500 93     4000 300    77 3.6   120   840    150 900    480 3.3 78 20     110   900   1900 52   1000
array-examples/standard_running_true-unreach-call.i 44    15000 37    15000 3.5 210 3.7 240 3.6 210 160   3600 890     320 .46 22 6.1   120   860    150 900    320 3.2 72 900     2900   900   1300 55   1300
array-examples/standard_sentinel_true-unreach-call.i 340    15000 850    2500 2.9 200 4.3 230 3.5 210 5.6 340 1.7   17 .62 23 8.7   130   680    210 .24 40 3.2 69 900     730   900   5200 9.3 340
array-examples/standard_seq_init_true-unreach-call_ground.i 49    15000 32    15000 2.8 210 4.3 230 3.4 200 160   3600 .19  17 .48 21 4.6   120   840    150 900    450 3.3 76 20     65   900   1100 53   1200
array-examples/standard_strcmp_true-unreach-call_ground.i 52    11000 12    860 3.6 210 3.6 230 3.5 210 160   3600 .33  21 .55 23 2.4   120   710    130 900    400 3.3 76 900     1500   900   1600 51   1100
array-examples/standard_strcpy_original_true-unreach-call.i 48    15000 39    15000 3.0 200 4.2 240 3.6 200 6.1 600 180     48 5.6  35 490     150   670    210 .23 42 880   310 900     200   900   2000 85   990
array-examples/standard_strcpy_true-unreach-call_ground.i 49    15000 39    15000 3.5 210 4.5 240 3.0 210 5.5 360 180     50 5.0  35 4.5   120   680    200 .35 42 880   320 900     180   900   1500 140   770
array-examples/standard_two_index_01_true-unreach-call.i 900    9500 5.8  2200 3.5 210 3.7 240 3.4 210 150   3500 .16  18 .44 21 .95  40   680    180 .29 40 130   9800 18     16   900   1500 52   860
array-examples/standard_two_index_02_true-unreach-call.i 48    15000 34    15000 2.9 210 4.3 240 3.5 200 160   3500 .19  18 .43 21 3.4   120   800    150 900    400 2.7 71 19     61   900   1300 54   970
array-examples/standard_two_index_03_true-unreach-call.i 900    9800 5.9  2200 3.6 210 3.8 230 3.5 210 130   3700 .17  18 .39 21 .63  14   640    190 900    610 900   4000 18     9.6 900   1400 53   1100
array-examples/standard_two_index_04_true-unreach-call.i 48    15000 34    15000 2.8 200 4.3 230 3.5 200 160   3500 .20  18 .44 21 570     150   750    160 900    400 3.0 73 18     37   900   2300 52   1200
array-examples/standard_two_index_05_true-unreach-call.i 47    15000 33    15000 3.5 210 4.2 240 3.5 200 160   3600 .20  18 .38 21 35     130   730    160 900    420 2.9 73 19     35   900   1100 54   1000
array-examples/standard_two_index_06_true-unreach-call.i 900    7700 5.9  2200 2.8 210 3.6 240 3.4 210 75   2400 .18  18 .39 21 .73  14   650    200 900    560 900   1200 18     7.9 900   980 54   920
array-examples/standard_two_index_07_true-unreach-call.i 48    15000 35    15000 2.9 210 4.2 230 2.9 210 160   3500 .22  18 .49 21 50     130   710    170 900    400 2.2 72 18     27   900   1200 53   1100
array-examples/standard_two_index_08_true-unreach-call.i 48    15000 34    15000 3.0 200 4.3 240 3.4 210 150   3600 .18  18 .41 21 4.3   130   710    180 900    400 3.0 71 18     25   900   1700 53   750
array-examples/standard_two_index_09_true-unreach-call.i 49    15000 35    15000 3.4 210 3.4 230 3.6 210 160   3600 .17  18 .47 21 3.5   120   700    180 900    400 2.9 77 18     24   900   1200 55   910
array-examples/standard_vararg_true-unreach-call_ground.i 330    15000 8.5  430 2.9 210 3.8 230 3.3 210 5.5 360 .26  28 .48 22 1.0   39   840    150 .26 42 880   410 900     69   900   1500 55   1100
array-examples/standard_vector_difference_true-unreach-call_ground.i 46    15000 36    15000 3.4 210 3.6 240 3.5 200 150   3600 .18  17 .39 21 5.4   130   840    150 900    400 3.5 79 20     200   900   1500 51   1000
reducercommutativity/rangesum05_false-unreach-call.i 19    160 .34 25 8.1 420 900   3500 560   710 370   3200 120     4300 3.7  170 .023 3.3 1.6  110 .25 30 3.4 69 36     7.8 13   330 9.4 330
reducercommutativity/rangesum10_false-unreach-call.i 37    210 .48 30 8.3 490 900   3400 8.0 400 440   3300 49     3100 3.7  170 .025 3.3 1.5  110 .20 30 3.6 74 18     8.6 41   440 11   350
reducercommutativity/rangesum20_false-unreach-call.i 57    350 .64 27 15   680 900   4100 13   780 900   4600 820     7800 3.8  170 .025 3.3 1.3  110 75    95 3.3 91 18     19   40   680 9.3 320
reducercommutativity/rangesum40_false-unreach-call.i 150    710 5.1  47 24   990 900   4100 23   930 21   890 820     7100 .40 22 .017 3.2 1.7  110 200    330 4.3 110 35     24   92   1400 11   340
reducercommutativity/rangesum60_false-unreach-call.i 380    1400 12    62 46   1200 900   4500 40   1100 31   970 910     8400 .42 22 .021 3.5 1.1  110 780    730 4.9 140 18     25   200   2000 9.4 330
reducercommutativity/rangesum_false-unreach-call.i 58    510 .55 40 900   980 900   4300 79   860 500   2600 150     3200 160    170 .016 3.4 64    3000 4.3  84 3.7 85 .12  7.0 18   480 9.0 330
reducercommutativity/avg05_true-unreach-call.i 120    390 850    200 900   2200 900   3000 900   1700 900   2700 890     150 2.1  43 .027 3.4 680    210 .21 30 2.8 65 18     5.9 350   1400 360   1000
reducercommutativity/avg10_true-unreach-call.i 900    620 850    310 900   2000 900   3300 900   1200 900   1700 890     190 5.8  45 .024 3.3 660    200 .21 30 2.7 67 18     5.9 420   2100 900   5100
reducercommutativity/avg20_true-unreach-call.i 900    860 850    410 900   2900 900   3900 900   2100 900   2700 890     250 24    50 .022 3.4 670    200 .23 30 2.9 75 18     6.2 900   1600 150   2500
reducercommutativity/avg40_true-unreach-call.i 900    870 850    560 26   1000 900   4400 24   1000 19   930 890     310 890    130 .021 3.3 670    210 370    350 3.2 90 18     6.5 900   2600 60   1100
reducercommutativity/avg60_true-unreach-call.i 900    850 850    690 52   1400 900   4300 38   1100 29   1000 890     290 890    140 .022 3.3 660    200 900    430 3.3 110 18     6.7 900   3300 64   1100
reducercommutativity/avg_true-unreach-call.i 900    1600 850    350 850   15000 900   4500 900   820 900   4100 890     320 890    100 .025 3.4 740    4200 .70 58 880   1200 .11  7.1 900   1000 9.5 320
reducercommutativity/max05_true-unreach-call.i 19    160 12    28 900   1000 540   2900 900   810 900   2900 1.7   16 6.2  27 .021 3.2 660    170 .21 30 2.9 68 640     10   56   930 900   2800
reducercommutativity/max10_true-unreach-call.i 430    490 690    68 900   2400 900   2600 18   700 900   4000 55     40 260    43 .021 3.3 660    170 .23 30 3.1 73 900     84   120   1000 900   2500
reducercommutativity/max20_true-unreach-call.i 900    1000 850    220 900   2100 900   3700 40   920 900   4400 890     110 890    130 .015 3.2 650    160 .22 31 3.6 80 890     210   860   2000 900   5200
reducercommutativity/max40_true-unreach-call.i 900    1500 850    420 190   1000 900   4900 27   920 24   870 890     170 890    330 .024 3.3 660    170 430    400 7.5 120 880     200   900   2000 61   1100
reducercommutativity/max60_true-unreach-call.i 900    1400 850    650 900   1500 900   6200 900   910 38   1400 890     240 890    180 .020 3.2 660    170 900    420 12   170 890     200   900   2300 68   1300
reducercommutativity/max_true-unreach-call.i 900    1400 850    350 900   3600 900   4300 900   790 900   11000 890     180 890    76 .020 3.2 750    4300 .87 64 880   370 .23  7.1 37   510 58   540
reducercommutativity/sep05_true-unreach-call.i 7.2  100 1.2  29 63   780 900   4300 900   920 900   4100 .20  13 2.0  34 .012 3.5 660    210 .18 30 2.8 66 18     6.1 93   1500 130   1700
reducercommutativity/sep10_true-unreach-call.i 16    170 2.3  32 900   890 900   4200 900   850 900   4100 .25  13 7.1  52 .018 3.3 700    210 .21 30 3.8 70 18     6.1 900   7200 900   5000
reducercommutativity/sep20_true-unreach-call.i 44    300 6.1  39 900   880 900   4100 900   940 900   2600 .37  13 630    100 .011 3.2 650    200 .19 30 880   90 18     6.1 910   8400 900   8300
reducercommutativity/sep40_true-unreach-call.i 900    1200 38    99 900   850 900   4600 900   890 900   4700 .57  13 890    190 .023 3.3 680    210 900    390 880   130 18     6.4 900   8400 63   1500
reducercommutativity/sep60_true-unreach-call.i 900    1700 230    180 900   890 900   5500 900   880 900   3200 .79  13 890    250 .020 3.4 660    200 900    290 880   180 18     7.0 900   5400 63   1200
reducercommutativity/sep_true-unreach-call.i 900    4700 850    930 900   890 900   4400 900   860 900   2700 460     4000 900    140 .023 3.6 750    4700 1.3  71 880   180 .15  7.5 900   5900 57   900
reducercommutativity/sum05_true-unreach-call.i 33    250 180    41 900   1600 900   2600 910   8400 900   4900 .076 13 1.5  22 .020 3.3 680    210 .25 30 2.8 69 18     5.8 32   460 900   4900
reducercommutativity/sum10_true-unreach-call.i 900    720 850    250 900   3300 900   3400 900   1200 900   3200 .092 13 3.0  23 .024 3.5 680    200 .21 30 2.8 71 18     6.1 78   1000 54   920
reducercommutativity/sum20_true-unreach-call.i 900    740 850    480 900   3000 900   3500 900   1700 900   2400 .096 13 6.9  23 .023 3.4 680    210 .20 30 2.8 72 18     6.2 300   1800 900   5000
reducercommutativity/sum40_true-unreach-call.i 900    850 850    570 22   980 900   4800 23   920 20   860 .14  13 16    23 .017 3.4 670    210 370    340 3.1 90 18     6.4 900   1900 58   1000
reducercommutativity/sum60_true-unreach-call.i 900    780 850    610 45   1300 900   5900 36   1000 27   930 .17  13 26    24 .018 3.4 660    190 900    430 3.4 120 18     6.6 900   2200 62   910
reducercommutativity/sum_true-unreach-call.i 900    1800 850    390 900   8300 900   5000 900   1100 900   5200 890     200 890    130 .027 3.3 740    4800 .72 59 880   380 .22  7.2 900   910 110   780
../../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)
total tasks 118 27000 1300000 118 22000 1100000 118 19000 84000 118 28000 150000 118 17000 60000 118 32000 370000 118 27000 260000 118 35000    17000 118 4900 13000 118 71000 110000 118 60000    34000 118 14000 30000 118 30000 110000 118 92000 210000 118 13000 150000
    correct results 16 1400 23000 53 18000 120000 6 170 4600 2 540 3200 4 700 3600 6 1500 15000 84 5500 100000 74 1200    2500 35 3500 5200 80 43000 35000 29 1100    2100 111 9000 14000 77 2200 18000 13 940 11000 3 27 980
        correct true 10 740 20000 47 18000 110000 1 63 780 2 540 3200 0 1 94 3500 59 1100 4500 70 1000    1800 22 3400 2600 58 43000 27000 15 3.2  450 77 8500 9300 53 1700 15000 7 530 5700 3 27 980
        correct false 6 710 3300 6 19 230 5 100 3800 0 4 700 3600 5 1400 11000 25 4400 100000 4 170    670 13 91 2500 22 140 7400 14 1100    1600 34 470 4700 24 510 2800 6 410 5300 0
    incorrect results 3 99 23000 6 2000 55000 5 340 5700 0 5 150 4900 6 160 6000 1 93 4000 2 .82 43 5 540 880 1 850 150 25 1200    2100 0 0 0 0
        incorrect true 1 46 12000 6 2000 55000 0 0 0 0 0 2 .82 43 3 200 620 1 850 150 2 .44 60 0 0 0 0
        incorrect false 2 53 11000 0 5 340 5700 0 5 150 4900 6 160 6000 1 93 4000 0 2 340 260 0 23 1200    2000 0 0 0 0
score (118 tasks, max score: 202) -38 -92 -73 4 -76 -89 127 80 -71 106 -388 188 130 20 6
Run set 2ls.sv-comp16.ArraysReach cbmc.sv-comp16.ArraysReach cpa-bam.sv-comp16.ArraysReach cpa-kind.sv-comp16.ArraysReach cpa-refsel.sv-comp16.ArraysReach cpa-seq.sv-comp16.ArraysReach esbmc.sv-comp16.ArraysReach esbmcdepthk.sv-comp16.ArraysReach forest.sv-comp16.ArraysReach pacman.sv-comp16.ArraysReach seahorn.sv-comp16.ArraysReach smack.sv-comp16.ArraysReach symbiotic3.sv-comp16.ArraysReach uautomizer.sv-comp16.ArraysReach ukojak.sv-comp16.ArraysReach