Tool CBMC 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 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-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 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 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 cbmc.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] cpa-bam.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] cpa-kind.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] cpa-seq.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] esbmc.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] esbmcdepthk.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] forest.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] seahorn.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] smack.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] symbiotic3.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] uautomizer.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] ukojak.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety]
Options --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 -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 ]] --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)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i unreach-call true 850    13000 unknown 3.6  210 error 4.6  240 unknown 160   4000 timeout 910     12000 unknown 890     380   unknown 24     920   timeout 900     850   false(reach) 5.0 86 timeout 900     4300   timeout 900   1700 timeout 39   700
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call out of memory 22    15000 unknown 3.1  210 error 4.5  240 unknown 160   3600 out of memory 87     15000 unknown 890     350   true 21     130   timeout 900     520   false(reach) 3.9 99 timeout 900     5300   timeout 900   1400 timeout 54   1300
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call out of memory 22    15000 unknown 3.1  210 error 3.7  240 unknown 160   3600 out of memory 88     15000 unknown 890     450   false(valid-free) 330     130   timeout 900     520   false(reach) 3.8 99 timeout 900     5300   timeout 900   1400 timeout 53   1000
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call true 77    13000 unknown 3.5  200 error 3.8  240 unknown 160   3500 out of memory 51     15000 unknown 890     850   false(reach) 29     970   timeout 900     1000   false(reach) 28   830 timeout 900     810   timeout 900   1900 timeout 51   850
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call true 78    13000 unknown 3.0  200 error 4.6  240 unknown 160   2400 out of memory 51     15000 unknown 890     850   unknown 24     130   timeout 900     970   false(reach) 320   1100 timeout 900     870   timeout 900   2100 timeout 50   1300
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call true 850    1800 unknown 3.5  200 error 4.4  230 unknown 160   3600 out of memory 45     15000 unknown 890     4200   unknown 20     140   false(reach) .30  42   false(reach) 8.9 99 timeout 900     650   timeout 900   2100 timeout 55   970
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call out of memory 34    15000 unknown 2.9  210 error 4.3  230 unknown 150   3500 false(reach) 95     4000 unknown 220     76   false(reach) 4.2   130   false(reach) .26  28   false(reach) 3.1 79 false(reach) 1.2   12   timeout 900   1300 timeout 53   830
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call out of memory 30    15000 unknown 3.5  210 error 4.3  230 unknown 150   3500 false(reach) 100     4100 unknown 680     130   unknown 5.6   120   false(reach) .40  40   false(reach) 3.4 75 false(reach) 20     93   timeout 900   960 timeout 52   1000
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call out of memory 38    15000 unknown 3.6  210 error 4.2  230 unknown 160   3600 false(reach) 110     4200 unknown 890     180   error (134) 110     270   false(reach) .28  40   false(reach) 3.7 79 false(reach) 22     160   timeout 900   1700 timeout 53   1100
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call out of memory 44    15000 unknown 3.4  200 error 4.4  240 unknown 150   3600 false(reach) 120     4200 unknown 890     210   true 160     340   false(reach) .30  40   false(reach) 3.7 83 false(reach) 22     180   timeout 900   1000 timeout 52   1500
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call out of memory 49    15000 unknown 2.9  210 error 3.8  230 unknown 160   2400 false(reach) 130     4200 unknown 890     240   unknown 10     140   false(reach) .29  40   false(reach) 3.8 87 false(reach) 23     200   timeout 900   1200 timeout 50   990
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call out of memory 56    15000 unknown 3.5  210 error 4.4  230 unknown 160   3500 false(reach) 140     4200 unknown 890     260   unknown 12     140   false(reach) .28  40   false(reach) 4.1 89 false(reach) 24     230   timeout 900   2000 timeout 52   1400
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call out of memory 46    15000 unknown 3.5  210 error 4.4  240 unknown 160   3600 false(reach) 150     4300 unknown 890     290   true 13     150   false(reach) .31  40   false(reach) 4.0 87 false(reach) 24     250   timeout 900   1900 timeout 52   1100
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call out of memory 51    15000 unknown 3.0  210 error 4.3  240 unknown 160   3600 false(reach) 150     4400 unknown 890     310   unknown 14     130   false(reach) .30  40   false(reach) 3.9 92 false(reach) 26     280   timeout 900   1800 timeout 63   1200
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call out of memory 55    15000 unknown 3.6  210 error 4.5  240 unknown 160   3500 false(reach) 160     4400 unknown 890     330   error (139) 170     670   false(reach) .36  40   false(reach) 4.4 86 false(reach) 26     300   timeout 900   2000 timeout 59   820
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call out of memory 32    15000 unknown 3.1  210 error 4.3  230 unknown 160   3200 false(reach) 110     3000 unknown 690     180   false(reach) 5.0   120   timeout 900     430   false(reach) 3.4 81 false(reach) 19     49   timeout 900   1000 timeout 52   1100
array-examples/standard_init1_false-unreach-call_ground.i unreach-call out of memory 32    15000 unknown 3.4  200 error 4.2  230 unknown 150   3100 false(reach) 90     1600 unknown 200     75   false(reach) 2.6   130   timeout 900     410   false(reach) 3.1 79 false(reach) 18     27   timeout 900   1000 timeout 53   1100
array-examples/standard_init2_false-unreach-call_ground.i unreach-call out of memory 26    15000 unknown 3.5  210 error 4.4  240 unknown 160   3600 false(reach) 100     1900 unknown 510     130   false(reach) 3.0   130   timeout 900     460   false(reach) 3.4 77 false(reach) 19     46   timeout 900   1600 timeout 53   790
array-examples/standard_init3_false-unreach-call_ground.i unreach-call out of memory 30    15000 unknown 2.9  210 error 4.3  240 unknown 160   3600 false(reach) 110     3000 unknown 890     180   false(reach) 4.1   130   timeout 900     450   false(reach) 3.4 80 false(reach) 19     65   timeout 900   1100 timeout 52   770
array-examples/standard_init4_false-unreach-call_ground.i unreach-call out of memory 35    15000 unknown 3.0  200 error 4.2  240 unknown 160   2400 false(reach) 120     3100 unknown 890     190   false(reach) 4.7   130   timeout 900     460   false(reach) 3.5 75 false(reach) 20     84   timeout 900   1700 timeout 49   990
array-examples/standard_init5_false-unreach-call_ground.i unreach-call out of memory 40    15000 unknown 3.0  210 error 3.6  240 unknown 160   3600 false(reach) 120     3100 unknown 890     210   false(reach) 5.6   120   timeout 900     450   false(reach) 3.6 79 false(reach) 20     100   timeout 900   1600 timeout 51   860
array-examples/standard_init6_false-unreach-call_ground.i unreach-call out of memory 45    15000 unknown 3.0  210 error 4.3  240 unknown 160   3600 false(reach) 140     4000 unknown 890     220   unknown 6.1   130   timeout 900     460   false(reach) 3.6 79 false(reach) 21     120   timeout 900   2600 timeout 49   1000
array-examples/standard_init7_false-unreach-call_ground.i unreach-call out of memory 49    15000 unknown 3.4  210 error 4.3  240 unknown 160   3600 false(reach) 150     4000 unknown 890     230   false(reach) 7.2   130   timeout 900     450   false(reach) 3.8 84 false(reach) 21     140   timeout 900   1500 timeout 55   890
array-examples/standard_init8_false-unreach-call_ground.i unreach-call out of memory 39    15000 unknown 3.6  210 error 4.4  240 unknown 160   3600 false(reach) 150     4000 unknown 890     240   false(reach) 7.3   130   timeout 900     460   false(reach) 3.9 83 false(reach) 22     160   timeout 900   1300 timeout 59   1200
array-examples/standard_init9_false-unreach-call_ground.i unreach-call out of memory 40    15000 unknown 3.5  210 error 3.6  240 unknown 160   3200 false(reach) 150     3900 unknown 890     250   false(reach) 8.6   130   timeout 900     460   false(reach) 3.9 90 false(reach) 22     180   timeout 900   1600 timeout 60   910
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call true 5.1  420 unknown 3.5  210 error 4.0  240 unknown 160   3500 false(reach) 97     4000 unknown 51     53   false(reach) 3.4   130   timeout 900     400   false(reach) 3.6 78 timeout 900     840   timeout 900   1100 timeout 53   1500
array-examples/standard_partition_false-unreach-call_ground.i unreach-call true 110    14000 unknown 3.5  210 error 4.5  240 unknown 160   3500 false(reach) 140     4200 unknown 890     190   false(reach) 6.8   120   timeout 900     540   false(reach) 3.9 93 out of memory 16     15000   timeout 900   1500 timeout 55   900
array-examples/standard_running_false-unreach-call.i unreach-call out of memory 37    15000 unknown 2.9  210 error 3.6  230 unknown 160   3600 false(reach) 97     3900 unknown 890     69   unknown 6.0   130   timeout 900     310   false(reach) 3.4 81 timeout 900     2800   timeout 900   1400 timeout 54   830
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i unreach-call true 1.9  25 unknown 3.1  210 error 3.9  240 unknown 160   3600 true 31     2800 true .42  22   unknown 7.0   120   true .27  25   true 4.0 93 timeout 900     54   true 12   340 timeout 58   1200
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call true 850    9900 unknown 3.5  210 error 4.5  240 unknown 160   3800 unknown 900     13000 true .79  36   unknown 5.5   130   timeout 900     500   true 880   200 timeout 900     1800   timeout 900   2100 timeout 39   780
array-examples/relax_true-unreach-call.i unreach-call true 510    14000 exception 4.4  230 exception 5.1  260 exception 95   2300 unknown 890     260 true 10     63   error (139) .059 4.0 false(reach) .56  54   true 880   300 unknown .12  7.0 timeout 900   1100 timeout 46   520
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call true 5.6  470 unknown 3.6  200 error 4.4  230 unknown 150   3600 unknown 890     460 true .92  23   unknown 7.2   130   timeout 900     510   true 3.1 70 timeout 900     830   timeout 900   1800 timeout 54   1100
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call true 130    13000 timeout 900    850 timeout 900    5600 timeout 900   3500 true 610     360 true .74  36   true .60  38   timeout 900     500   true 6.9 90 unknown .19  6.5 timeout 900   1200 timeout 47   950
array-examples/sanfoundry_24_true-unreach-call.i unreach-call true 26    780 unknown 3.4  200 error 3.4  240 unknown 5.0 360 true .32  51 true .38  22   unknown 3.7   120   true .27  36   true 2.6 73 timeout 900     1700   true 10   320 true 9.6 330
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call true 5.2  420 unknown 3.3  210 error 3.7  240 unknown 150   3600 unknown 890     310 true .50  22   unknown 3.8   130   timeout 900     400   true 3.8 78 timeout 900     730   timeout 900   1400 timeout 54   1400
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call true 1.3  26 unknown 3.5  200 true 3.6  230 true 94   3500 true .15  13 true .39  21   true 43     130   true .16  24   true 2.5 64 true .091 5.9 true 8.3 330 true 8.0 310
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call out of memory 23    15000 unknown 3.5  210 error 4.3  240 unknown 160   3500 out of memory 88     15000 unknown 890     460   unknown 22     130   timeout 900     520   true 28   140 timeout 900     5200   timeout 900   1600 timeout 55   1200
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call true 77    13000 unknown 3.6  210 error 3.9  230 unknown 160   3500 out of memory 51     15000 unknown 890     840   error (134) 15     9.4 timeout 900     960   timeout 880   1000 timeout 900     880   timeout 900   1700 timeout 50   790
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call out of memory 37    15000 unknown 3.5  210 error 3.7  240 unknown 160   2400 true .46  65 true .39  22   unknown 7.0   120   timeout 900     520   true 3.0 74 true 75     11000   timeout 900   1400 timeout 55   870
array-examples/standard_compare_true-unreach-call_ground.i unreach-call true 7.0  760 unknown 3.5  210 error 4.4  240 unknown 150   3600 true .30  36 true .40  22   unknown 3.8   120   timeout 900     390   true 3.3 79 timeout 900     2700   timeout 900   1200 timeout 57   1100
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call out of memory 34    15000 unknown 3.5  200 error 3.7  240 unknown 150   3500 true .19  16 true .38  21   unknown 3.5   120   false(reach) .39  40   true 3.4 77 true 19     110   timeout 900   2800 timeout 54   890
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call out of memory 30    15000 unknown 3.5  200 error 4.2  230 unknown 150   2400 true .19  18 true .46  21   unknown 5.7   130   false(reach) .30  40   true 3.5 87 true 20     130   timeout 900   2500 timeout 50   1000
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call out of memory 36    15000 unknown 2.7  210 error 3.7  240 unknown 150   3500 true .23  19 true .40  21   true 6.9   130   false(reach) .29  40   true 3.6 80 true 21     160   timeout 900   900 timeout 49   970
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call out of memory 43    15000 unknown 3.4  210 error 3.7  230 unknown 160   3600 true .28  21 true .42  22   unknown 7.8   120   false(reach) .33  40   true 3.7 88 true 21     180   timeout 900   1200 timeout 49   900
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call out of memory 50    15000 unknown 3.6  210 error 3.8  230 unknown 160   3600 true .32  22 true .48  22   unknown 10     140   false(reach) .30  40   true 3.8 91 true 22     200   timeout 900   2600 timeout 52   830
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call out of memory 56    15000 unknown 3.6  210 error 3.6  240 unknown 150   3600 true .38  23 true .42  22   unknown 11     120   false(reach) .30  40   true 4.0 90 true 23     230   timeout 900   1300 timeout 49   1600
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call out of memory 47    15000 unknown 3.6  200 error 4.5  230 unknown 160   3600 true .39  25 true .49  22   unknown 13     120   false(reach) .25  40   true 4.2 93 true 23     260   timeout 900   1400 timeout 51   1100
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call out of memory 51    15000 unknown 3.1  210 error 3.7  240 unknown 160   3600 true .43  26 true .40  22   unknown 14     120   false(reach) .31  40   true 4.4 97 true 24     280   timeout 900   2900 timeout 59   820
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call out of memory 55    15000 unknown 3.6  210 error 3.8  230 unknown 160   3500 true .49  27 true .42  22   unknown 17     130   false(reach) .31  40   true 4.6 90 true 25     300   timeout 900   1600 timeout 58   1200
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call out of memory 32    15000 unknown 3.5  210 error 3.7  240 unknown 160   2000 true .27  19 true .44  22   true 490     150   timeout 900     470   true 4.0 82 true 20     110   timeout 900   1400 timeout 47   1100
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call out of memory 37    15000 unknown 2.9  210 error 3.6  230 unknown 160   3600 true .32  21 true .43  22   unknown 7.3   120   timeout 900     450   true 4.9 91 true 21     130   timeout 900   1800 timeout 49   790
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call out of memory 33    15000 unknown 3.0  210 error 4.7  230 unknown 160   3600 true .27  19 true .41  22   unknown 5.1   120   timeout 900     460   true 3.8 81 true 21     150   timeout 900   1600 timeout 53   1100
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call out of memory 28    15000 unknown 3.0  210 error 3.8  240 unknown 160   2300 true .19  18 true .41  21   true 3.5   120   timeout 900     410   true 3.5 75 true 20     86   timeout 900   1400 timeout 52   940
array-examples/standard_find_true-unreach-call_ground.i unreach-call true 8.4  440 unknown 3.5  200 error 4.1  240 unknown 5.7 360 true .77  67 true .48  23   true 2.7   130   false(reach) .33  43   true 3.5 78 timeout 900     68   timeout 900   1200 timeout 54   680
array-examples/standard_init1_true-unreach-call_ground.i unreach-call out of memory 32    15000 unknown 2.9  210 error 4.3  240 unknown 150   3600 true .15  16 true .37  21   true 2.2   130   timeout 900     450   true 3.2 79 true 19     65   timeout 900   1100 timeout 51   1100
array-examples/standard_init2_true-unreach-call_ground.i unreach-call out of memory 26    15000 unknown 2.9  210 error 3.5  240 unknown 160   3600 true .17  17 true .39  21   true 2.8   120   timeout 900     460   true 3.2 77 true 20     83   timeout 900   1300 timeout 54   1100
array-examples/standard_init3_true-unreach-call_ground.i unreach-call out of memory 31    15000 unknown 3.2  210 error 3.7  230 unknown 160   3600 true .17  19 true .46  22   unknown 4.0   130   timeout 900     450   true 3.3 76 true 19     100   timeout 900   1100 timeout 46   970
array-examples/standard_init4_true-unreach-call_ground.i unreach-call out of memory 35    15000 unknown 3.5  210 error 4.3  230 unknown 160   3600 true .18  20 true .38  22   error (134) 110     130   timeout 900     450   true 3.4 74 true 20     120   timeout 900   2000 timeout 49   830
array-examples/standard_init5_true-unreach-call_ground.i unreach-call out of memory 39    15000 unknown 3.4  210 error 4.2  230 unknown 160   3600 true .23  21 true .46  22   true 17     130   timeout 900     450   true 3.2 79 true 21     140   timeout 900   1200 timeout 51   880
array-examples/standard_init6_true-unreach-call_ground.i unreach-call out of memory 45    15000 unknown 3.5  210 error 3.6  240 unknown 160   2100 true .26  22 true .44  22   unknown 6.0   130   timeout 900     450   true 3.8 88 true 22     160   timeout 900   1100 timeout 57   1200
array-examples/standard_init7_true-unreach-call_ground.i unreach-call out of memory 49    15000 unknown 3.1  200 error 3.8  240 unknown 160   2400 true .27  24 true .43  22   true 78     130   timeout 900     450   true 4.0 85 true 22     180   timeout 900   1100 timeout 52   1100
array-examples/standard_init8_true-unreach-call_ground.i unreach-call out of memory 38    15000 unknown 3.0  210 error 4.5  240 unknown 160   3600 true .29  25 true .47  22   unknown 7.2   120   timeout 900     460   true 3.9 86 true 23     200   timeout 900   1200 timeout 65   1300
array-examples/standard_init9_true-unreach-call_ground.i unreach-call out of memory 41    15000 unknown 3.4  210 error 4.6  230 unknown 160   3200 true .25  26 true .41  22   unknown 8.1   120   timeout 900     460   true 3.8 94 true 23     220   timeout 900   1400 timeout 60   1200
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call true 4.8  410 unknown 2.8  200 error 4.2  230 unknown 150   1300 unknown 890     280 true .47  22   true 840     130   timeout 900     400   true 3.7 78 timeout 900     810   timeout 900   1500 timeout 51   1000
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call true 4.9  410 unknown 3.5  210 error 4.3  240 unknown 160   2300 unknown 890     250 true .42  21   true 3.1   130   timeout 900     390   true 3.6 82 timeout 900     810   timeout 900   1300 timeout 53   1500
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call out of memory 32    15000 unknown 3.6  200 error 3.7  230 unknown 150   3600 true .26  17 true .44  21   true 4.1   120   timeout 900     410   true 3.1 71 true 18     61   timeout 900   1200 timeout 51   990
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call true 80    14000 unknown 3.5  210 error 3.7  230 unknown 160   3500 unknown 890     420 true .40  22   true 850     210   timeout 900     680   true 150   100 timeout 900     2700   timeout 900   1200 timeout 56   1100
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call true 68    14000 unknown 3.5  210 error 4.0  230 unknown 160   3500 unknown 890     860 true .44  22   unknown 6.5   120   timeout 900     240   true 84   98 out of memory 15     15000   timeout 900   2300 timeout 57   1300
array-examples/standard_partition_true-unreach-call_ground.i unreach-call true 110    14000 unknown 3.6  210 error 3.6  240 unknown 160   3500 unknown 890     560 true .34  22   true 13     210   timeout 900     410   true 27   92 out of memory 17     15000   timeout 900   2500 timeout 55   1200
array-examples/standard_password_true-unreach-call_ground.i unreach-call true 7.0  760 unknown 3.6  200 error 4.3  230 unknown 160   2000 true .30  36 true .47  21   true 4.2   120   timeout 900     390   true 3.3 80 timeout 900     2700   timeout 900   940 timeout 54   790
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call out of memory 34    15000 unknown 3.0  210 error 4.2  240 unknown 150   3500 false(reach) 93     4000 unknown 300     77   unknown 3.6   120   timeout 900     480   true 3.3 78 true 20     110   timeout 900   1900 timeout 52   1000
array-examples/standard_running_true-unreach-call.i unreach-call out of memory 37    15000 unknown 3.5  210 error 3.7  240 unknown 160   3600 unknown 890     320 true .46  22   unknown 6.1   120   timeout 900     320   true 3.2 72 timeout 900     2900   timeout 900   1300 timeout 55   1300
array-examples/standard_sentinel_true-unreach-call.i unreach-call true 850    2500 unknown 2.9  200 error 4.3  230 unknown 5.6 340 true 1.7   17 true .62  23   false(valid-free) 8.7   130   false(reach) .24  40   true 3.2 69 timeout 900     730   timeout 900   5200 true 9.3 340
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call out of memory 32    15000 unknown 2.8  210 error 4.3  230 unknown 160   3600 true .19  17 true .48  21   unknown 4.6   120   timeout 900     450   true 3.3 76 true 20     65   timeout 900   1100 timeout 53   1200
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call true 12    860 unknown 3.6  210 error 3.6  230 unknown 160   3600 true .33  21 true .55  23   unknown 2.4   120   timeout 900     400   true 3.3 76 timeout 900     1500   timeout 900   1600 timeout 51   1100
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call out of memory 39    15000 unknown 3.0  200 error 4.2  240 unknown 6.1 600 true 180     48 true 5.6   35   true 490     150   false(reach) .23  42   true 880   310 timeout 900     200   timeout 900   2000 timeout 85   990
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call out of memory 39    15000 unknown 3.5  210 error 4.5  240 unknown 5.5 360 true 180     50 true 5.0   35   unknown 4.5   120   false(reach) .35  42   true 880   320 timeout 900     180   timeout 900   1500 timeout 140   770
array-examples/standard_two_index_01_true-unreach-call.i unreach-call true 5.8  2200 unknown 3.5  210 error 3.7  240 unknown 150   3500 true .16  18 true .44  21   unknown .95  40   false(reach) .29  40   error (1) 130   9800 true 18     16   timeout 900   1500 timeout 52   860
array-examples/standard_two_index_02_true-unreach-call.i unreach-call out of memory 34    15000 unknown 2.9  210 error 4.3  240 unknown 160   3500 true .19  18 true .43  21   unknown 3.4   120   timeout 900     400   true 2.7 71 true 19     61   timeout 900   1300 timeout 54   970
array-examples/standard_two_index_03_true-unreach-call.i unreach-call true 5.9  2200 unknown 3.6  210 error 3.8  230 unknown 130   3700 true .17  18 true .39  21   true .63  14   timeout 900     610   timeout 900   4000 true 18     9.6 timeout 900   1400 timeout 53   1100
array-examples/standard_two_index_04_true-unreach-call.i unreach-call out of memory 34    15000 unknown 2.8  200 error 4.3  230 unknown 160   3500 true .20  18 true .44  21   true 570     150   timeout 900     400   true 3.0 73 true 18     37   timeout 900   2300 timeout 52   1200
array-examples/standard_two_index_05_true-unreach-call.i unreach-call out of memory 33    15000 unknown 3.5  210 error 4.2  240 unknown 160   3600 true .20  18 true .38  21   error (134) 35     130   timeout 900     420   true 2.9 73 true 19     35   timeout 900   1100 timeout 54   1000
array-examples/standard_two_index_06_true-unreach-call.i unreach-call true 5.9  2200 unknown 2.8  210 error 3.6  240 unknown 75   2400 true .18  18 true .39  21   true .73  14   timeout 900     560   true 900   1200 true 18     7.9 timeout 900   980 timeout 54   920
array-examples/standard_two_index_07_true-unreach-call.i unreach-call out of memory 35    15000 unknown 2.9  210 error 4.2  230 unknown 160   3500 true .22  18 true .49  21   error (134) 50     130   timeout 900     400   true 2.2 72 true 18     27   timeout 900   1200 timeout 53   1100
array-examples/standard_two_index_08_true-unreach-call.i unreach-call out of memory 34    15000 unknown 3.0  200 error 4.3  240 unknown 150   3600 true .18  18 true .41  21   unknown 4.3   130   timeout 900     400   true 3.0 71 true 18     25   timeout 900   1700 timeout 53   750
array-examples/standard_two_index_09_true-unreach-call.i unreach-call out of memory 35    15000 unknown 3.4  210 error 3.4  230 unknown 160   3600 true .17  18 true .47  21   true 3.5   120   timeout 900     400   true 2.9 77 true 18     24   timeout 900   1200 timeout 55   910
array-examples/standard_vararg_true-unreach-call_ground.i unreach-call true 8.5  430 unknown 2.9  210 error 3.8  230 unknown 5.5 360 true .26  28 true .48  22   true 1.0   39   false(reach) .26  42   true 880   410 timeout 900     69   timeout 900   1500 timeout 55   1100
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call out of memory 36    15000 unknown 3.4  210 error 3.6  240 unknown 150   3600 true .18  17 true .39  21   unknown 5.4   130   timeout 900     400   true 3.5 79 true 20     200   timeout 900   1500 timeout 51   1000
reducercommutativity/rangesum05_false-unreach-call.i unreach-call false(reach) .34 25 false(reach) 8.1  420 timeout 900    3500 false(reach) 370   3200 error (1) 120     4300 false(reach) 3.7   170   error (139) .023 3.3 true .25  30   false(reach) 3.4 69 false(reach) 36     7.8 false(reach) 13   330 error 9.4 330
reducercommutativity/rangesum10_false-unreach-call.i unreach-call false(reach) .48 30 false(reach) 8.3  490 timeout 900    3400 false(reach) 440   3300 false(reach) 49     3100 false(reach) 3.7   170   error (139) .025 3.3 true .20  30   false(reach) 3.6 74 false(reach) 18     8.6 false(reach) 41   440 error 11   350
reducercommutativity/rangesum20_false-unreach-call.i unreach-call false(reach) .64 27 false(reach) 15    680 timeout 900    4100 timeout 900   4600 false(reach) 820     7800 false(reach) 3.8   170   error (139) .025 3.3 false(reach) 75     95   false(reach) 3.3 91 false(reach) 18     19   false(reach) 40   680 error 9.3 320
reducercommutativity/rangesum40_false-unreach-call.i unreach-call false(reach) 5.1  47 false(reach) 24    990 timeout 900    4100 false(reach) 21   890 false(reach) 820     7100 true .40  22   error (139) .017 3.2 false(reach) 200     330   false(reach) 4.3 110 false(reach) 35     24   false(reach) 92   1400 error 11   340
reducercommutativity/rangesum60_false-unreach-call.i unreach-call false(reach) 12    62 false(reach) 46    1200 timeout 900    4500 false(reach) 31   970 timeout 910     8400 true .42  22   error (139) .021 3.5 false(reach) 780     730   false(reach) 4.9 140 false(reach) 18     25   false(reach) 200   2000 error 9.4 330
reducercommutativity/rangesum_false-unreach-call.i unreach-call false(reach) .55 40 timeout 900    980 timeout 900    4300 false(reach) 500   2600 error (1) 150     3200 false(reach) 160     170   error (139) .016 3.4 false(reach) 4.3   84   false(reach) 3.7 85 unknown .12  7.0 false(reach) 18   480 error 9.0 330
reducercommutativity/avg05_true-unreach-call.i unreach-call true 850    200 timeout 900    2200 timeout 900    3000 timeout 900   2700 unknown 890     150 true 2.1   43   error (139) .027 3.4 true .21  30   true 2.8 65 true 18     5.9 error 350   1400 timeout 360   1000
reducercommutativity/avg10_true-unreach-call.i unreach-call true 850    310 timeout 900    2000 timeout 900    3300 timeout 900   1700 unknown 890     190 true 5.8   45   error (139) .024 3.3 true .21  30   true 2.7 67 true 18     5.9 error 420   2100 timeout 900   5100
reducercommutativity/avg20_true-unreach-call.i unreach-call true 850    410 timeout 900    2900 timeout 900    3900 timeout 900   2700 unknown 890     250 true 24     50   error (139) .022 3.4 true .23  30   true 2.9 75 true 18     6.2 timeout 900   1600 error 150   2500
reducercommutativity/avg40_true-unreach-call.i unreach-call true 850    560 false(reach) 26    1000 timeout 900    4400 false(reach) 19   930 unknown 890     310 unknown 890     130   error (139) .021 3.3 false(reach) 370     350   true 3.2 90 true 18     6.5 timeout 900   2600 timeout 60   1100
reducercommutativity/avg60_true-unreach-call.i unreach-call true 850    690 false(reach) 52    1400 timeout 900    4300 false(reach) 29   1000 unknown 890     290 unknown 890     140   error (139) .022 3.3 timeout 900     430   true 3.3 110 true 18     6.7 timeout 900   3300 timeout 64   1100
reducercommutativity/avg_true-unreach-call.i unreach-call true 850    350 out of memory 850    15000 timeout 900    4500 timeout 900   4100 unknown 890     320 unknown 890     100   error (139) .025 3.4 false(reach) .70  58   timeout 880   1200 unknown .11  7.1 timeout 900   1000 error 9.5 320
reducercommutativity/max05_true-unreach-call.i unreach-call true 12    28 timeout 900    1000 true 540    2900 timeout 900   2900 true 1.7   16 true 6.2   27   error (139) .021 3.2 true .21  30   true 2.9 68 true 640     10   error 56   930 timeout 900   2800
reducercommutativity/max10_true-unreach-call.i unreach-call true 690    68 timeout 900    2400 timeout 900    2600 timeout 900   4000 true 55     40 true 260     43   error (139) .021 3.3 true .23  30   true 3.1 73 timeout 900     84   error 120   1000 timeout 900   2500
reducercommutativity/max20_true-unreach-call.i unreach-call true 850    220 timeout 900    2100 timeout 900    3700 timeout 900   4400 unknown 890     110 unknown 890     130   error (139) .015 3.2 true .22  31   true 3.6 80 timeout 890     210   error 860   2000 timeout 900   5200
reducercommutativity/max40_true-unreach-call.i unreach-call true 850    420 false(reach) 190    1000 timeout 900    4900 false(reach) 24   870 unknown 890     170 unknown 890     330   error (139) .024 3.3 false(reach) 430     400   true 7.5 120 timeout 880     200   timeout 900   2000 timeout 61   1100
reducercommutativity/max60_true-unreach-call.i unreach-call true 850    650 timeout 900    1500 timeout 900    6200 false(reach) 38   1400 unknown 890     240 unknown 890     180   error (139) .020 3.2 timeout 900     420   true 12   170 timeout 890     200   timeout 900   2300 timeout 68   1300
reducercommutativity/max_true-unreach-call.i unreach-call true 850    350 timeout 900    3600 timeout 900    4300 timeout 900   11000 unknown 890     180 unknown 890     76   error (139) .020 3.2 false(reach) .87  64   true 880   370 unknown .23  7.1 error 37   510 error 58   540
reducercommutativity/sep05_true-unreach-call.i unreach-call true 1.2  29 true 63    780 timeout 900    4300 timeout 900   4100 true .20  13 true 2.0   34   error (139) .012 3.5 true .18  30   true 2.8 66 true 18     6.1 true 93   1500 timeout 130   1700
reducercommutativity/sep10_true-unreach-call.i unreach-call true 2.3  32 timeout 900    890 timeout 900    4200 timeout 900   4100 true .25  13 true 7.1   52   error (139) .018 3.3 true .21  30   true 3.8 70 true 18     6.1 timeout 900   7200 timeout 900   5000
reducercommutativity/sep20_true-unreach-call.i unreach-call true 6.1  39 timeout 900    880 timeout 900    4100 timeout 900   2600 true .37  13 true 630     100   error (139) .011 3.2 true .19  30   timeout 880   90 true 18     6.1 timeout 910   8400 timeout 900   8300
reducercommutativity/sep40_true-unreach-call.i unreach-call true 38    99 timeout 900    850 timeout 900    4600 timeout 900   4700 true .57  13 unknown 890     190   error (139) .023 3.3 timeout 900     390   timeout 880   130 true 18     6.4 timeout 900   8400 timeout 63   1500
reducercommutativity/sep60_true-unreach-call.i unreach-call true 230    180 timeout 900    890 timeout 900    5500 timeout 900   3200 true .79  13 unknown 890     250   error (139) .020 3.4 timeout 900     290   timeout 880   180 true 18     7.0 timeout 900   5400 timeout 63   1200
reducercommutativity/sep_true-unreach-call.i unreach-call true 850    930 timeout 900    890 timeout 900    4400 timeout 900   2700 error (1) 460     4000 unknown 900     140   error (139) .023 3.6 false(reach) 1.3   71   true 880   180 unknown .15  7.5 timeout 900   5900 timeout 57   900
reducercommutativity/sum05_true-unreach-call.i unreach-call true 180    41 timeout 900    1600 timeout 900    2600 timeout 900   4900 true .076 13 true 1.5   22   error (139) .020 3.3 true .25  30   true 2.8 69 true 18     5.8 true 32   460 timeout 900   4900
reducercommutativity/sum10_true-unreach-call.i unreach-call true 850    250 timeout 900    3300 timeout 900    3400 timeout 900   3200 true .092 13 true 3.0   23   error (139) .024 3.5 true .21  30   true 2.8 71 true 18     6.1 true 78   1000 timeout 54   920
reducercommutativity/sum20_true-unreach-call.i unreach-call true 850    480 timeout 900    3000 timeout 900    3500 timeout 900   2400 true .096 13 true 6.9   23   error (139) .023 3.4 true .20  30   true 2.8 72 true 18     6.2 true 300   1800 timeout 900   5000
reducercommutativity/sum40_true-unreach-call.i unreach-call true 850    570 false(reach) 22    980 timeout 900    4800 false(reach) 20   860 true .14  13 true 16     23   error (139) .017 3.4 false(reach) 370     340   true 3.1 90 true 18     6.4 timeout 900   1900 timeout 58   1000
reducercommutativity/sum60_true-unreach-call.i unreach-call true 850    610 false(reach) 45    1300 timeout 900    5900 false(reach) 27   930 true .17  13 true 26     24   error (139) .018 3.4 timeout 900     430   true 3.4 120 true 18     6.6 timeout 900   2200 timeout 62   910
reducercommutativity/sum_true-unreach-call.i unreach-call true 850    390 timeout 900    8300 timeout 900    5000 timeout 900   5200 unknown 890     200 unknown 890     130   error (139) .027 3.3 false(reach) .72  59   true 880   380 unknown .22  7.2 timeout 900   910 timeout 110   780
array-memsafety/add_last_unsafe_false-valid-deref.i valid-deref false(valid-deref) .27 27 error .49 48 error .50 49 error 3.7 170 false(valid-deref) 69     130 unknown .069 8.6 true 1.0   38   error (3) .033 5.6 error (1) 1.4 18 error (1) .018 3.8 false(valid-deref) 10   330 false(valid-deref) 10   330
array-memsafety/bubblesort_unsafe_false-valid-deref.i valid-deref false(valid-deref) .13 24 error .64 50 error .52 49 timeout 900   10000 false(valid-deref) 800     12000 unknown .085 8.7 unknown .57  38   error (3) .040 5.6 error (1) 1.4 18 error (1) .035 3.9 false(valid-deref) 8.7 310 false(valid-deref) 9.6 330
array-memsafety/count_down_unsafe_false-valid-deref.i valid-deref false(valid-deref) .38 30 error .54 49 error .59 49 error 3.7 170 unknown 900     10000 unknown .061 8.5 true 3.0   38   error (3) .024 5.5 error (1) 1.5 18 error (1) .020 4.0 false(valid-deref) 8.7 320 false(valid-deref) 9.2 330
array-memsafety/cstrcat_unsafe_false-valid-deref.i valid-deref false(valid-deref) .18 24 error .49 49 error .51 49 false(valid-deref) 3.1 160 false(valid-deref) .77  31 unknown .060 8.6 true .59  38   error (3) .046 5.5 error (1) 1.4 18 error (1) .022 3.8 false(valid-deref) 9.6 330 false(valid-deref) 9.4 330
array-memsafety/cstrchr_unsafe_false-valid-deref.i valid-deref false(valid-deref) .18 27 error .49 48 error .54 50 error 3.1 170 false(valid-deref) 1.4   23 unknown .061 8.4 false(valid-free) 1.4   38   error (3) .038 5.6 error (1) 1.4 18 error (1) .017 4.0 false(valid-deref) 15   470 timeout 130   1400
array-memsafety/cstrlen_unsafe_false-valid-deref.i valid-deref false(valid-deref) .28 28 error .56 46 error .51 49 error 3.7 170 false(valid-deref) 1.1   19 unknown .094 8.6 true .59  38   error (3) .026 5.5 error (1) 1.0 18 error (1) .012 4.1 false(valid-deref) 11   330 timeout 140   1300
array-memsafety/cstrncat_unsafe_false-valid-deref.i valid-deref false(valid-deref) .19 25 error .63 50 error .60 49 false(valid-deref) 2.6 170 false(valid-deref) .88  47 unknown .062 8.5 true .63  38   error (3) .024 5.5 error (1) 1.4 18 error (1) .015 4.0 false(valid-deref) 9.4 330 false(valid-deref) 8.8 320
array-memsafety/cstrncpy_unsafe_false-valid-deref.i valid-deref false(valid-deref) .12 25 error .54 49 error .61 47 false(valid-deref) 2.8 160 false(valid-deref) 210     3700 unknown .064 8.3 true .72  38   error (3) .020 5.5 error (1) 1.4 18 error (1) .035 3.8 false(valid-deref) 8.2 320 false(valid-deref) 10   350
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i valid-deref false(valid-deref) .20 28 error .60 50 error .60 49 error 3.0 170 false(valid-deref) 100     3600 unknown .064 8.6 false(valid-free) 1.2   39   error (3) .042 5.5 error (1) 1.5 18 error (1) .015 3.9 false(valid-deref) 14   420 timeout 900   540
array-memsafety/diff_usafe_false-valid-deref.i valid-deref false(valid-deref) .17 25 error .59 49 error .63 49 false(valid-deref) 2.6 170 unknown 900     7500 unknown .11  8.9 true .58  38   error (3) .024 5.6 error (1) 1.3 18 error (1) .034 4.0 false(valid-deref) 9.5 330 false(valid-deref) 9.3 330
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i valid-deref false(valid-deref) 3.4  180 error .51 49 error .59 49 error 3.2 170 out of memory 150     15000 unknown .072 8.7 true .27  7.3 error (3) .029 5.4 error (1) 1.3 18 error (1) .026 3.8 false(valid-deref) 13   340 false(valid-deref) 13   370
array-memsafety/lis_unsafe_false-valid-deref.i valid-deref false(valid-deref) .29 28 error .49 49 error .59 49 error 3.9 170 out of memory 39     15000 unknown .097 8.5 false(valid-free) 23     38   error (3) .026 5.6 error (1) 1.5 18 error (1) .019 3.8 error 16   420 false(valid-deref) 71   750
array-memsafety/mult_array_unsafe_false-valid-deref.i valid-deref false(valid-deref) .33 33 error .49 50 error .53 49 error 3.7 180 false(valid-deref) 4.1   88 unknown .065 8.3 true .50  38   error (3) .020 5.4 error (1) 1.4 18 error (1) .016 4.0 false(valid-deref) 11   360 error 11   340
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i valid-deref false(valid-deref) 1.3  75 error .51 49 error .60 49 error 3.8 170 false(valid-deref) 390     690 unknown .086 8.4 unknown .54  38   error (3) .046 5.5 error (1) 1.3 18 error (1) .022 3.9 false(valid-deref) 12   330 false(valid-deref) 13   350
array-memsafety/reverse_array_unsafe_false-valid-deref.i valid-deref false(valid-deref) 1.2  75 error .57 49 error .61 49 error 3.1 170 false(valid-deref) 880     960 unknown .067 8.8 false(valid-free) .91  38   error (3) .019 5.6 error (1) 1.4 18 error (1) .030 3.9 false(valid-deref) 10   350 false(valid-deref) 11   340
array-memsafety/selectionsort_unsafe_false-valid-deref.i valid-deref false(valid-deref) .17 24 error .64 50 error .59 49 false(valid-deref) 3.2 180 false(valid-deref) 65     5800 unknown .063 8.5 false(valid-free) .77  39   error (3) .022 5.5 error (1) 1.3 18 error (1) .011 4.0 false(valid-deref) 9.6 340 false(valid-deref) 9.7 330
array-memsafety/stroeder1_unsafe_false-valid-deref.i valid-deref false(valid-deref) .14 24 error .65 49 error .59 48 false(valid-deref) 3.2 160 false(valid-deref) .30  17 unknown .095 8.6 unknown .53  38   error (3) .038 5.5 error (1) 1.0 18 error (1) .020 3.9 false(valid-deref) 9.9 340 false(valid-deref) 10   350
array-memsafety/add_last-alloca_true-valid-memsafety.i valid-deref true 850    14000 error .50 48 error .52 48 error 3.9 170 true 120     150 unknown .10  8.7 true .79  38   error (3) .027 5.5 error (1) 1.5 18 error (1) .016 3.9 timeout 900   1000 timeout 500   740
array-memsafety/array01-alloca_true-valid-memsafety.i valid-deref true 470    14000 error .60 49 error .61 49 error 3.9 170 true 590     10000 unknown .066 8.6 false(valid-free) .92  39   error (3) .042 5.5 error (1) 1.3 18 error (1) .034 3.9 true 11   330 true 13   420
array-memsafety/array02-alloca_true-valid-memsafety.i valid-deref true 550    13000 error .49 49 error .59 49 error 3.8 170 out of memory 91     15000 unknown .066 8.4 false(valid-free) 1.2   38   error (3) .031 5.5 error (1) 1.4 19 error (1) .019 3.9 true 12   340 true 14   460
array-memsafety/array03-alloca_true-valid-memsafety.i valid-deref true 490    13000 error .61 49 error .50 48 error 3.7 180 true 480     15000 unknown .071 8.7 unknown .57  39   error (3) .047 5.5 error (1) 1.4 19 error (1) .024 4.0 true 13   360 true 14   430
array-memsafety/bubblesort-alloca_true-valid-memsafety.i valid-deref true 560    13000 error .67 49 error .60 48 error 3.8 180 out of memory 84     15000 unknown .089 8.6 true .90  38   error (3) .044 5.5 error (1) 1.4 19 error (1) .016 3.9 true 20   360 timeout 42   910
array-memsafety/count_down-alloca_true-valid-memsafety.i valid-deref true 320    14000 error .58 49 error .60 49 error 3.9 180 true 540     9800 unknown .065 8.3 false(valid-free) 71     38   error (3) .047 5.5 error (1) 1.2 18 error (1) .021 3.9 timeout 900   1400 true 76   410
array-memsafety/cstrcat-alloca_true-valid-memsafety.i valid-deref true 140    15000 error .50 49 error .59 47 error 3.7 170 true 15     62 unknown .064 8.6 false(valid-free) 1.0   39   error (3) .028 5.5 error (1) 1.3 18 error (1) .029 3.9 error 43   660 error 110   860
array-memsafety/cstrchr-alloca_true-valid-memsafety.i valid-deref true 22    120 error .59 49 error .65 50 error 3.7 170 true 1.5   32 unknown .099 8.6 false(valid-free) .66  38   error (3) .049 5.4 error (1) 1.5 18 error (1) .036 3.9 error 15   350 timeout 140   1200
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i valid-deref true 40    250 error .50 49 error .59 49 error 3.8 170 true 3.8   46 unknown .065 8.7 true .56  38   error (3) .040 5.4 error (1) 1.5 18 error (1) .035 4.0 true 19   400 timeout 45   730
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i valid-deref true 57    2500 error .58 49 error .51 49 error 3.1 170 true 1.8   45 unknown .070 8.6 true .61  39   error (3) .049 5.4 error (1) 1.5 18 error (1) .018 4.0 timeout 900   1800 timeout 130   1400
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i valid-deref true 850    6000 error .59 49 error .59 49 error 3.1 170 unknown 900     6300 unknown .062 8.6 unknown .55  38   error (3) .050 5.5 error (1) 1.4 18 error (1) .036 3.9 error 21   490 timeout 45   650
array-memsafety/cstrlen-alloca_true-valid-memsafety.i valid-deref true 12    65 error .52 46 error .54 47 error 3.3 170 true 1.1   21 unknown .071 8.6 unknown .59  38   error (3) .023 5.5 error (1) 1.5 18 error (1) .021 4.0 true 13   380 timeout 140   1200
array-memsafety/cstrncat-alloca_true-valid-memsafety.i valid-deref true 290    14000 error .64 50 error .55 49 error 3.7 170 true 35     95 unknown .065 8.8 unknown .25  7.4 error (3) .026 5.6 error (1) 1.3 19 error (1) .024 3.8 error 28   480 timeout 350   1200
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i valid-deref true 180    580 error .53 49 error .51 49 error 4.1 170 true 6.2   120 unknown .051 8.6 false(valid-free) .76  39   error (3) .045 5.5 error (1) 1.5 19 error (1) .036 3.9 true 22   460 timeout 36   600
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i valid-deref true 850    6300 error .62 49 error .59 50 error 3.0 170 true 80     4900 unknown .054 8.5 false(valid-free) .75  38   error (3) .040 5.5 error (1) 1.4 19 error (1) .015 3.9 timeout 900   4400 timeout 140   1200
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i valid-deref true 850    6000 error .56 49 error .59 49 error 3.3 170 unknown 900     6300 unknown .070 8.8 true .58  38   error (3) .038 5.6 error (1) 1.4 18 error (1) .020 4.0 error 40   460 timeout 39   700
array-memsafety/cstrspn-alloca_true-valid-memsafety.i valid-deref true 850    6000 error .51 49 error .56 49 error 3.3 170 unknown 900     6300 unknown .063 8.3 true .58  38   error (3) .024 5.6 error (1) 1.5 19 error (1) .021 4.0 error 22   480 timeout 42   1100
array-memsafety/diff-alloca_true-valid-memsafety.i valid-deref true 230    14000 error .48 49 error .54 49 error 3.9 170 unknown 900     10000 unknown .099 8.8 false(valid-free) 1.5   39   error (3) .043 5.5 error (1) 1.4 19 error (1) .022 3.9 timeout 900   970 error 860   930
array-memsafety/insertionsort-alloca_true-valid-memsafety.i valid-deref true 370    15000 error .50 49 error .51 52 error 3.8 170 true 230     5700 unknown .055 8.6 false(valid-free) .89  38   error (3) .045 5.5 error (1) 1.4 18 error (1) .037 3.8 error 13   340 true 16   370
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i valid-deref true 560    13000 error .62 50 error .59 49 error 3.7 170 out of memory 260     15000 unknown .096 8.7 false(valid-free) .96  38   error (3) .025 5.5 error (1) 1.4 18 error (1) .016 3.8 true 20   380 true 17   500
array-memsafety/lis-alloca_true-valid-memsafety.i valid-deref true 500    14000 error .60 50 error .51 49 error 4.0 170 out of memory 49     15000 unknown .062 8.6 false(valid-free) 1.2   39   error (3) .050 5.5 error (1) 1.4 18 error (1) .028 3.9 error 180   1200 timeout 120   860
array-memsafety/mult_array-alloca_true-valid-memsafety.i valid-deref true 850    12000 error .57 49 error .62 48 error 3.8 170 true 1.9   66 unknown .063 8.5 unknown .53  38   error (3) .030 5.5 error (1) 1.5 19 error (1) .014 3.9 true 17   390 error 9.6 320
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i valid-deref true 41    2300 error .49 46 error .60 49 error 3.8 170 true .58  28 unknown .063 8.6 true 18     39   error (3) .036 5.5 error (1) 1.5 19 error (1) .028 4.1 timeout 900   850 error 530   470
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i valid-deref true 83    99 error .58 49 error .58 49 error 3.7 180 true 1.1   42 unknown .064 8.4 true 2.0   39   error (3) .030 5.5 error (1) 1.4 18 error (1) .020 3.9 timeout 900   1200 true 13   340
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i valid-deref false(valid-deref) .24 28 error .48 49 error .58 49 error 3.7 170 true 4.7   49 unknown .069 8.6 true .60  38   error (3) .027 5.5 error (1) 1.4 19 error (1) .013 3.9 error 14   340 true 11   340
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i valid-deref true 41    2400 error .57 49 error .63 49 error 3.2 170 true .75  26 unknown .065 8.8 true 2.7   39   error (3) .032 5.4 error (1) 1.5 19 error (1) .014 3.9 timeout 900   1800 true 12   370
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i valid-deref true 51    2500 error .59 49 error .59 49 error 3.8 170 true 1.8   42 unknown .079 8.7 true .60  38   error (3) .025 5.6 error (1) 1.4 19 error (1) .031 3.9 timeout 900   1000 timeout 130   1400
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i valid-deref true 850    4900 error .58 46 error .51 50 error 3.2 170 true 80     4400 unknown .070 8.5 unknown .55  38   error (3) .019 5.6 error (1) 1.4 19 error (1) .034 4.1 timeout 900   830 timeout 130   1500
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i valid-deref true 140    15000 error .58 49 error .50 48 error 3.7 170 true 15     62 unknown .069 8.6 unknown .88  40   error (3) .035 5.5 error (1) 1.4 18 error (1) .021 3.9 error 65   770 timeout 92   1100
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i valid-deref true 130    310 error .61 50 error .63 50 error 3.9 170 true 4.4   82 unknown .062 8.6 unknown .49  36   error (3) .023 5.5 error (1) 1.5 19 error (1) .016 4.1 timeout 900   1800 timeout 36   640
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i valid-deref true 57    2500 error .49 48 error .51 49 error 3.8 170 true 1.8   42 unknown .10  8.5 false(valid-free) .87  38   error (3) .046 5.5 error (1) 1.5 18 error (1) .021 3.9 error 26   390 timeout 130   1300
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i valid-deref true 850    350 error .50 52 error .52 47 error 3.1 170 false(valid-deref) 260     8400 unknown .065 8.6 false(valid-free) .81  38   error (3) .051 5.5 error (1) 1.4 19 error (1) .013 3.9 true 39   490 timeout 70   890
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i valid-deref true 130    14000 error .50 49 error .53 49 error 3.8 170 true 190     180 unknown .11  8.6 false(valid-free) .93  38   error (3) .020 5.6 error (1) 1.3 18 error (1) .021 3.9 timeout 900   1600 timeout 72   880
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i valid-deref true 12    64 error .64 47 error .61 49 error 3.1 170 true 1.2   22 unknown .11  8.5 true .60  38   error (3) .034 5.4 error (1) 1.5 18 error (1) .016 4.0 true 21   460 timeout 130   1200
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i valid-deref true 280    14000 error .51 48 error .64 50 error 3.3 170 true 26     94 unknown .067 8.8 true .59  39   error (3) .023 5.6 error (1) 1.5 19 error (1) .017 3.9 error 70   550 timeout 110   850
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i valid-deref true 210    500 error .87 49 error .55 50 error 4.0 170 true 4.3   150 unknown .094 8.4 false(valid-free) .94  39   error (3) .030 5.5 error (1) 1.4 18 error (1) .022 3.9 timeout 900   1600 timeout 47   740
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i valid-deref true 850    7900 error .52 48 error .60 49 error 2.9 180 true 79     4400 unknown .065 8.7 false(valid-free) .88  39   error (3) .036 5.5 error (1) 1.5 18 error (1) .032 3.9 timeout 900   1100 timeout 140   1200
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i valid-deref true 15    94 error .62 49 error .60 48 error 3.6 170 true 1.3   25 unknown .094 8.6 true .62  38   error (3) .051 5.4 error (1) 1.4 18 error (1) .017 4.1 true 22   360 timeout 130   1200
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i valid-deref true 850    100 error .58 47 error .54 49 error 3.3 170 unknown 900     5800 unknown .066 8.6 true .60  38   error (3) .050 5.5 error (1) 1.4 19 error (1) .014 3.9 error 23   360 true 62   780
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i valid-deref true 850    3500 error .56 49 error .52 49 error 3.7 170 unknown .098 18 unknown .072 8.7 false(valid-free) .78  39   error (3) .040 5.4 error (1) 1.5 18 error (1) .025 3.8 error 42   480 error 100   1000
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i valid-deref true 850    8100 error .57 49 error .61 47 error 3.7 170 out of memory 51     15000 unknown .065 8.7 false(valid-free) .90  39   error (3) .052 5.4 error (1) 1.4 19 error (1) .012 3.9 error 28   560 timeout 45   1000
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i valid-deref true 18    130 error .59 49 error .64 50 error 3.2 170 true 1.2   26 unknown .095 8.6 false(valid-free) .83  38   error (3) .030 5.4 error (1) 1.5 18 error (1) .031 3.9 error 21   490 timeout 130   1200
array-memsafety/selectionsort-alloca_true-valid-memsafety.i valid-deref true 230    14000 error .58 49 error .63 50 error 3.8 170 unknown 900     9000 unknown .090 8.6 true .52  38   error (3) .020 5.5 error (1) 1.4 18 error (1) .024 3.9 error 14   350 timeout 44   780
array-memsafety/stroeder1-alloca_true-valid-memsafety.i valid-deref true 5.3  60 error .60 49 error .65 49 error 3.8 170 true .65  25 unknown .070 8.6 true .55  38   error (3) .026 5.4 error (1) 1.4 18 error (1) .033 4.0 true 12   340 true 11   340
array-memsafety/stroeder2-alloca_true-valid-memsafety.i valid-deref true 250    14000 error .55 50 error .53 50 error 3.8 170 true 860     6900 unknown .069 8.9 true .65  39   error (3) .022 5.6 error (1) 1.4 19 error (1) .016 3.9 true 22   420 true 18   380
array-memsafety/strreplace-alloca_true-valid-memsafety.i valid-deref true 180    14000 error .55 49 error .52 50 error 3.9 180 true 1.7   57 unknown .068 8.6 unknown .51  38   error (3) .032 5.5 error (1) 1.4 18 error (1) .015 3.9 error 21   410 timeout 130   1300
array-memsafety/subseq-alloca_true-valid-memsafety.i valid-deref true 850    2000 error .59 49 error .52 49 error 3.7 170 true 81     140 unknown .088 8.6 true .66  39   error (3) .034 5.4 error (1) 1.4 18 error (1) .022 3.9 true 48   430 true 110   980
array-memsafety/substring-alloca_true-valid-memsafety.i valid-deref true 850    800 error .59 47 error .60 49 error 3.7 180 unknown 900     9600 unknown .069 8.7 false(valid-free) .77  38   error (3) .037 5.4 error (1) 1.4 18 error (1) .017 3.9 true 60   630 timeout 65   990
../../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)
total tasks 183 40000    1400000 183 19000 87000 183 28000 150000 183 33000 390000 183 42000 540000 183 35000    18000 183 5100 16000 183 60000    35000 183 14000 32000 183 30000 110000 183 110000 250000 183 20000 200000
    correct results 117 36000    450000 6 170 4600 2 540 3200 12 1500 16000 131 12000 190000 74 1200    2500 54 3600 5900 29 1100    2100 111 9000 14000 77 2200 18000 45 1500 23000 29 600 12000
        correct true 94 36000    440000 1 63 780 2 540 3200 1 94 3500 93 4600 67000 70 1000    1800 41 3500 3400 15 3.2  450 77 8500 9300 53 1700 15000 23 900 12000 16 410 7100
        correct false 23 28    940 5 100 3800 0 11 1400 12000 38 7000 130000 4 170    670 13 91 2500 14 1100    1600 34 470 4700 24 510 2800 22 580 11000 13 190 4800
    incorrect results 7 2000    55000 5 340 5700 0 6 160 6000 2 350 12000 2 .82 43 39 660 2200 25 1200    2100 0 0 0 0
        incorrect true 6 2000    55000 0 0 0 0 2 .82 43 12 210 930 2 .44 60 0 0 0 0
        incorrect false 1 .24 28 5 340 5700 0 6 160 6000 2 350 12000 0 27 460 1200 23 1200    2000 0 0 0 0
Run set cbmc.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] cpa-bam.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] cpa-kind.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] cpa-seq.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] esbmc.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] esbmcdepthk.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] forest.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] seahorn.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] smack.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] symbiotic3.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] uautomizer.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety] ukojak.[sv-comp16.ArraysReach; sv-comp16.ArraysMemSafety]