Tool CPAchecker 1.5-svn 20187M CPAchecker 1.5-svn 20312M CPAchecker 1.5-svn 20187M CPAchecker 1.5-svn 20312M CPAchecker 1.5-svn 20187M
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
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]
OS Linux 4.2.0-30-generic [Linux 4.2.0-34-generic; Linux 4.2.0-30-generic] Linux 4.2.0-30-generic [Linux 4.2.0-34-generic; Linux 4.2.0-30-generic] Linux 4.2.0-30-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-03-11 14:33:18 CET 2016-03-15 20:04:06 CET 2016-03-11 14:33:18 CET 2016-03-15 20:04:06 CET 2016-03-11 14:33:18 CET
Run set MathSAT5-heaparray.ArraysReach25 MathSAT5-oldarray.ArraysReach25 MathSAT5-uf.ArraysReach25 PRINCESS-heaparray-quantifiers.ArraysReach25 PRINCESS-heaparray.ArraysReach25 PRINCESS-oldarray.ArraysReach25 PRINCESS-uf.ArraysReach25 SMTInterpol-heaparray.ArraysReach25 SMTInterpol-oldarray.ArraysReach25 SMTInterpol-uf.ArraysReach25 Z3-heaparray-quantifiers.ArraysReach25 Z3-heaparray.ArraysReach25 Z3-oldarray.ArraysReach25 Z3-uf.ArraysReach25
Options -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop solver.solver=MATHSAT5 -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=MATHSAT5 -setprop cpa.predicate.handleArrays=true -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=MATHSAT5 -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeFloatAs=INTEGER -setprop cpa.predicate.useQuantifiersOnArrays=true -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeFloatAs=INTEGER -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeFloatAs=INTEGER -setprop cpa.predicate.handleArrays=true -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeFloatAs=INTEGER -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop solver.solver=SMTINTERPOL -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=SMTINTERPOL -setprop cpa.predicate.handleArrays=true -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=SMTINTERPOL -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop cpa.predicate.useQuantifiersOnArrays=true -setprop solver.solver=Z3 -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop solver.solver=Z3 -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=Z3 -setprop cpa.predicate.handleArrays=true -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=Z3
test/programs/array-simplified-benchmarks/arrays-size-25/ status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage
25_data_structures_set_multi_proc_false-unreach-call_ground.i 428    418    zeus21 14999998464 29.1  18.4  zeus24 800829440 85.9  72.6  zeus20 877785088 902    829    4544368640 zeus04 901    839    zeus21 4545531904 178    115    zeus14 3104182272 901    837    zeus15 4719341568 106    69.5  zeus13 4467015680 54.4  28.1  zeus14 882352128 79.0  45.5  zeus09 2059399168 320    306    916279296 zeus19 313    300    zeus15 914276352 47.8  36.5  zeus20 824147968 58.2  44.1  zeus15 841441280
25_sorting_bubblesort_false-unreach-call2_ground.i 15.3  9.53 zeus07 543850496 16.5  10.3  zeus24 544849920 26.4  20.5  zeus21 612683776 61.0  32.1  1160421376 zeus01 65.6  34.4  zeus15 1185484800 65.6  34.3  zeus03 1275514880 84.0  47.9  zeus17 2217967616 47.9  24.5  zeus21 849555456 42.5  21.8  zeus21 913608704 48.6  25.8  zeus19 852557824 16.5  11.1  446939136 zeus05 16.6  11.3  zeus14 456282112 15.1  10.2  zeus23 446029824 34.7  29.4  zeus05 509284352
25_sorting_bubblesort_false-unreach-call_ground.i 15.0  9.33 zeus12 546574336 16.6  10.4  zeus10 543154176 25.3  19.4  zeus13 624365568 65.8  34.4  1191985152 zeus01 63.6  33.3  zeus05 1187500032 63.2  32.9  zeus21 1250058240 84.9  48.5  zeus24 1681948672 48.2  24.8  zeus17 844943360 44.2  22.7  zeus20 879693824 54.4  29.8  zeus03 999727104 16.5  11.2  451674112 zeus24 16.9  11.5  zeus22 464863232 14.4  9.68 zeus22 454107136 35.2  29.8  zeus03 519434240
25_sorting_selectionsort_false-unreach-call2_ground.i 12.5  7.22 zeus23 464232448 12.8  7.32 zeus05 459444224 14.7  8.66 zeus01 565735424 97.6  52.6  1540091904 zeus08 98.8  53.4  zeus07 1521758208 96.1  51.6  zeus22 1580716032 100    55.2  zeus06 1928773632 41.9  21.6  zeus18 854618112 46.0  23.7  zeus07 862236672 47.5  24.5  zeus17 928960512 27.3  19.4  671027200 zeus18 26.5  19.2  zeus22 650706944 25.7  18.3  zeus09 643031040 34.9  27.0  zeus08 768151552
25_sorting_selectionsort_false-unreach-call_ground.i 920    911    zeus21 14971637760 893    885    zeus20 14999998464 897    889    zeus24 14999998464 902    734    7755743232 zeus16 901    744    zeus20 7837663232 901    729    zeus21 7781421056 901    746    zeus15 6874566656 149    99.8  zeus08 5751083008 68.3  40.8  zeus11 3447808000 904    870    zeus09 2686177280 901    892    661770240 zeus07 901    893    zeus12 647704576 912    900    zeus14 975835136 901    891    zeus12 1132371968
25_standard_allDiff2_false-unreach-call_ground.i 99.3  80.5  zeus05 1653030912 91.3  73.8  zeus03 1554247680 85.3  66.4  zeus15 1646129152 263    182    4460519424 zeus15 270    186    zeus09 4701396992 261    180    zeus08 4214284288 244    161    zeus04 3979902976 683    630    zeus13 4468551680 496    447    zeus06 4543750144 355    308    zeus19 4536262656 373    349    1066708992 zeus11 377    353    zeus20 1015861248 365    342    zeus01 1031827456 373    349    zeus23 1033551872
25_standard_copy1_false-unreach-call_ground.i 12.6  7.28 zeus02 508874752 11.3  6.64 zeus05 407175168 20.9  15.0  zeus19 647438336 112    62.7  1880461312 zeus16 109    60.3  zeus24 1743355904 115    63.0  zeus09 1938436096 432    368    zeus09 4614221824 35.3  18.4  zeus18 763502592 32.6  17.0  zeus13 863072256 49.3  25.4  zeus22 994435072 12.8  8.20 431882240 zeus21 13.7  8.63 zeus22 429744128 12.9  8.17 zeus21 437846016 25.0  19.5  zeus15 551931904
25_standard_copy2_false-unreach-call_ground.i 123    113    zeus09 1298096128 26.7  17.1  zeus01 784330752 70.7  60.0  zeus06 883638272 270    182    6077411328 zeus13 273    187    zeus06 5804797952 137    81.3  zeus18 2246578176 902    836    zeus21 4530692096 48.1  24.8  zeus22 851828736 46.8  24.3  zeus13 862826496 56.3  30.6  zeus03 1412112384 24.3  17.4  624648192 zeus21 22.3  16.0  zeus04 622653440 20.7  14.6  zeus11 536203264 69.7  61.3  zeus04 794660864
25_standard_copy3_false-unreach-call_ground.i 552    539    zeus17 3556708352 38.1  27.0  zeus23 802885632 187    173    zeus09 962260992 901    614    9482838016 zeus24 230    1030    zeus15 3967209472 281    200    zeus13 6200520704 901    838    zeus24 4590313472 59.2  30.9  zeus15 1126682624 52.2  27.3  zeus18 1242730496 80.6  46.5  zeus10 3158548480 34.4  26.9  785149952 zeus15 33.7  26.2  zeus12 786771968 29.3  22.5  zeus19 635740160 145    136    zeus07 813019136
25_standard_copy4_false-unreach-call_ground.i 902    889    zeus11 6306365440 66.5  50.6  zeus02 897105920 443    425    zeus13 1076727808 902    664    9995771904 zeus09 901    629    zeus18 8836227072 557    1030    zeus24 8357990400 902    818    zeus10 4818771968 65.0  34.2  zeus23 1409601536 64.1  33.7  zeus05 1433690112 95.0  59.9  zeus11 4409217024 46.6  37.8  893878272 zeus17 47.4  38.5  zeus07 916094976 41.5  33.2  zeus11 774000640 272    260    zeus12 931717120
25_standard_copy5_false-unreach-call_ground.i 903    890    zeus17 5806321664 82.4  67.3  zeus19 1440399360 901    886    zeus10 915349504 579    1030    5399769088 zeus24 578    1030    zeus17 5425254400 773    1030    zeus19 9510531072 902    769    zeus11 7897464832 88.7  52.8  zeus08 2667835392 77.3  41.4  zeus22 2450116608 118    82.1  zeus16 4529143808 65.3  55.0  963911680 zeus22 67.6  56.9  zeus06 949805056 53.0  43.8  zeus21 819994624 458    444    zeus18 1424031744
25_standard_copy6_false-unreach-call_ground.i 913    898    zeus23 5843058688 98.7  82.7  zeus08 1615986688 901    887    zeus11 918429696 902    758    6279299072 zeus23 952    795    zeus18 7415685120 901    655    zeus09 10492608512 901    743    zeus20 8769847296 99.5  60.9  zeus23 2751332352 73.8  40.3  zeus22 2095706112 150    110    zeus02 4593438720 81.9  70.8  1020932096 zeus14 83.4  72.2  zeus06 1028534272 68.6  57.6  zeus03 826695680 738    722    zeus13 1453924352
25_standard_copy7_false-unreach-call_ground.i 902    885    zeus04 5949804544 131    115    zeus15 1872896000 901    889    zeus14 887635968 902    754    6717972480 zeus06 902    758    zeus22 6645428224 934    676    zeus18 9261662208 901    680    zeus02 9528557568 119    77.8  zeus08 3864539136 81.2  46.9  zeus12 2954846208 212    172    zeus05 4589293568 106    91.9  1141817344 zeus10 104    90.8  zeus20 1143070720 87.3  74.6  zeus13 844177408 902    890    zeus14 827219968
25_standard_copy8_false-unreach-call_ground.i 902    887    zeus19 6064963584 169    152    zeus09 2933481472 901    888    zeus14 904896512 902    769    6617554944 zeus14 902    766    zeus09 6461001728 640    1030    zeus01 7142457344 901    651    zeus16 10358280192 170    126    zeus18 4515422208 85.1  49.9  zeus13 3858300928 261    214    zeus17 4719624192 137    121    1251110912 zeus14 129    115    zeus08 1239261184 105    91.3  zeus13 916729856 901    890    zeus20 831463424
25_standard_copy9_false-unreach-call_ground.i 902    884    zeus18 5919735808 244    222    zeus16 2914779136 901    888    zeus06 895995904 902    777    6307790848 zeus22 901    769    zeus18 6537183232 547    1030    zeus19 5810151424 901    598    zeus23 11807756288 189    147    zeus10 4517736448 93.2  57.6  zeus12 4426391552 365    316    zeus17 4785709056 164    148    1318789120 zeus18 160    143    zeus02 1377927168 127    113    zeus04 895594496 902    890    zeus23 832425984
25_standard_copyInitSum2_false-unreach-call_ground.i 71.2  61.6  zeus04 1318387712 52.5  40.8  zeus05 973860864 198    180    zeus13 948375552 304    208    5724200960 zeus23 307    210    zeus14 5558325248 901    786    zeus11 6023708672 901    814    zeus04 4966371328 83.0  52.4  zeus15 3158253568 57.1  29.7  zeus15 1320382464 71.5  38.5  zeus17 2083749888 901    894    487624704 zeus02 901    894    zeus11 508227584 901    893    zeus10 1092464640 615    603    zeus07 828166144
25_standard_init1_false-unreach-call_ground.i 13.8  8.19 zeus03 539054080 12.0  7.18 zeus21 416071680 16.1  10.4  zeus13 559804416 94.8  50.0  1533038592 zeus14 92.9  48.8  zeus01 1605206016 94.4  49.3  zeus24 1536401408 107    62.4  zeus21 1949167616 36.0  18.6  zeus02 862347264 35.2  18.2  zeus03 861777920 40.6  21.0  zeus20 871141376 14.1  8.92 444887040 zeus14 13.9  8.79 zeus18 437739520 12.7  7.98 zeus02 346554368 21.1  16.0  zeus07 488509440
25_standard_init2_false-unreach-call_ground.i 27.7  17.4  zeus19 812437504 25.4  16.0  zeus10 769421312 43.3  31.4  zeus15 839282688 114    63.6  2133213184 zeus17 115    64.2  zeus15 1984786432 115    63.4  zeus23 1735569408 151    94.6  zeus12 3224485888 47.5  24.3  zeus11 1219166208 44.6  23.1  zeus13 878657536 47.8  25.4  zeus23 909828096 21.0  14.9  550805504 zeus06 20.4  14.4  zeus16 555200512 20.8  14.7  zeus10 539246592 44.7  38.3  zeus01 628125696
25_standard_init3_false-unreach-call_ground.i 42.1  30.6  zeus01 894525440 38.8  28.5  zeus16 888426496 59.1  46.3  zeus14 869916672 165    103    3008380928 zeus07 160    100    zeus16 2933313536 153    95.0  zeus01 3012530176 216    149    zeus22 4484210688 52.9  27.7  zeus15 949207040 44.6  23.5  zeus03 1204256768 59.3  32.3  zeus09 1168007168 30.2  23.0  650416128 zeus20 30.9  23.5  zeus08 661524480 28.7  22.1  zeus21 654020608 82.5  74.2  zeus07 776818688
25_standard_init4_false-unreach-call_ground.i 60.3  47.8  zeus21 1141620736 59.3  47.2  zeus08 1139179520 95.2  80.9  zeus13 924909568 217    1030    4280074240 zeus18 222    1030    zeus09 4964855808 234    1030    zeus12 5027528704 301    219    zeus10 5324939264 62.2  32.4  zeus11 1177628672 65.7  34.7  zeus13 1449205760 71.2  38.5  zeus13 1334239232 41.3  32.4  778489856 zeus05 40.4  31.9  zeus16 782233600 40.2  31.9  zeus21 774324224 133    123    zeus10 801292288
25_standard_init5_false-unreach-call_ground.i 85.8  72.7  zeus12 1134907392 84.3  70.0  zeus18 1616031744 149    133    zeus08 920322048 253    1030    4867825664 zeus07 253    1030    zeus19 5177495552 210    1030    zeus20 4318384128 435    342    zeus02 5479776256 69.2  36.9  zeus01 1320263680 61.1  32.9  zeus08 1472978944 75.0  42.6  zeus10 1698746368 56.7  46.5  819924992 zeus21 53.0  43.0  zeus06 836849664 52.7  43.4  zeus19 816525312 191    180    zeus13 811180032
25_standard_init6_false-unreach-call_ground.i 146    128    zeus04 1939439616 113    97.5  zeus16 1879916544 208    186    zeus07 962322432 278    1030    5158174720 zeus15 259    1030    zeus03 4709724160 249    1030    zeus11 5178175488 634    527    zeus14 5624184832 72.4  39.8  zeus03 1606946816 68.1  37.1  zeus16 2443468800 82.2  48.0  zeus22 2462507008 71.4  59.6  845692928 zeus02 68.2  56.1  zeus01 868950016 74.2  62.7  zeus07 853102592 260    248    zeus21 852832256
25_standard_init7_false-unreach-call_ground.i 184    167    zeus07 2642587648 155    139    zeus01 2076434432 246    225    zeus21 1237794816 277    1030    5042442240 zeus14 282    1030    zeus03 4746047488 260    1030    zeus07 4670996480 787    674    zeus24 6348439552 75.5  42.3  zeus22 1682542592 81.5  47.1  zeus18 2417811456 88.3  53.6  zeus14 2236239872 85.8  71.8  893161472 zeus08 82.1  69.1  zeus06 899080192 87.1  74.3  zeus05 868970496 341    327    zeus19 908247040
25_standard_init8_false-unreach-call_ground.i 247    228    zeus05 3547152384 189    172    zeus06 2624770048 339    316    zeus15 1023410176 301    1030    4937875456 zeus20 321    1030    zeus03 5064364032 285    1030    zeus19 4879724544 901    802    zeus06 5406109696 86.2  49.2  zeus06 2250903552 79.6  47.9  zeus05 2476113920 97.0  60.0  zeus02 2979987456 98.7  84.2  916475904 zeus24 101    86.4  zeus15 895365120 102    89.3  zeus09 889843712 439    423    zeus19 904351744
25_standard_init9_false-unreach-call_ground.i 294    273    zeus02 3582308352 245    227    zeus08 2836234240 432    409    zeus14 973688832 338    1030    5031497728 zeus14 363    1030    zeus23 5089259520 307    1030    zeus20 4885946368 902    809    zeus15 5201473536 85.8  51.0  zeus18 2338840576 86.8  50.5  zeus23 2950422528 107    67.9  zeus11 3075776512 120    104    952004608 zeus13 121    104    zeus16 960040960 128    114    zeus21 915865600 547    529    zeus15 933978112
25_standard_minInArray_false-unreach-call_ground.i 16.5  9.98 zeus22 560758784 14.0  8.32 zeus13 523116544 14.9  8.82 zeus15 555286528 1000    715    8946290688 zeus16 1000    704    zeus15 9209409536 1000    691    zeus18 8596578304 1000    743    zeus02 8675434496 36.2  18.7  zeus03 873340928 35.0  18.1  zeus08 845807616 33.5  17.4  zeus11 866562048 15.9  10.2  438796288 zeus13 15.0  9.72 zeus15 444166144 14.8  9.62 zeus14 435744768 14.8  9.61 zeus19 453742592
25_standard_partition_false-unreach-call_ground.i 912    898    zeus04 8307322880 917    905    zeus01 11352317952 901    884    zeus17 909131776 902    830    4797480960 zeus24 901    827    zeus24 4805758976 902    827    zeus04 4866564096 901    841    zeus22 4544528384 903    546    zeus03 10134716416 1000    607    zeus02 8579612672 902    751    zeus24 6621245440 901    894    441245696 zeus05 901    893    zeus20 412770304 902    893    zeus13 707928064 901    894    zeus16 579182592
25_standard_running_false-unreach-call.i 56.4  40.2  zeus03 920195072 36.7  23.2  zeus17 836116480 47.6  32.1  zeus14 897806336 170    102    2182713344 zeus09 162    98.5  zeus22 3311628288 164    96.1  zeus13 2220769280 333    263    zeus09 4355002368 159    118    zeus20 4515524608 63.5  33.2  zeus18 1321787392 62.9  33.1  zeus04 1237688320 32.4  24.3  618258432 zeus06 33.4  24.9  zeus18 605020160 31.8  23.3  zeus17 581185536 45.4  35.9  zeus21 748052480
25_data_structures_set_multi_proc_trivial_true-unreach-call_ground.i 45.4  40.6  zeus23 375136256 8.79 5.08 zeus12 285818880 11.1  7.16 zeus21 311238656 902    829    4558516224 zeus19 901    831    zeus13 4581216256 284    207    zeus01 3687890944 901    833    zeus14 4690751488 227    174    zeus20 4499984384 86.5  47.6  zeus03 1939148800 101    57.4  zeus01 2202083328 391    376    829202432 zeus14 424    409    zeus03 837660672 69.0  56.1  zeus07 754753536 83.3  69.9  zeus15 754860032
25_data_structures_set_multi_proc_true-unreach-call_ground.i 503    491    zeus08 14999998464 43.7  29.0  zeus10 861622272 108    93.3  zeus04 883871744 902    832    4540346368 zeus02 902    833    zeus20 4544507904 154    95.3  zeus21 2955915264 902    834    zeus04 4683833344 124    79.1  zeus10 4471754752 231    183    zeus15 4490432512 91.7  48.8  zeus01 1588752384 429    412    913924096 zeus13 407    391    zeus04 914845696 102    89.0  zeus08 817868800 99.3  83.6  zeus22 835330048
25_relax_true-unreach-call.i 4.51 2.60 zeus22 217563136 4.63 2.68 zeus06 218902528 4.27 2.50 zeus11 217952256 5.88 3.37 308449280 zeus01 5.87 3.44 zeus19 309846016 9.73 5.41 zeus24 407937024 5.64 3.26 zeus18 311070720 4.42 2.59 zeus13 219631616 5.00 2.92 zeus11 231604224 4.46 2.60 zeus07 218214400 4.66 2.69 219443200 zeus03 4.33 2.47 zeus08 215764992 4.92 2.83 zeus04 228909056 4.50 2.59 zeus04 215130112
25_sanfoundry_02_true-unreach-call_ground.i 916    909    zeus18 9138851840 918    911    zeus05 11485827072 916    909    zeus12 9137655808 1000    782    8883683328 zeus23 1000    764    zeus13 8858468352 1000    755    zeus21 8795971584 902    682    zeus08 8818794496 902    873    zeus13 1967071232 902    879    zeus15 1003057152 902    875    zeus05 1518358528 902    892    857309184 zeus05 902    892    zeus09 850759680 902    892    zeus13 842543104 902    892    zeus12 856985600
25_sanfoundry_10_true-unreach-call_ground.i 16.7  10.5  zeus09 620965888 22.9  13.6  zeus02 687923200 901    880    zeus06 4567838720 901    790    4701982720 zeus20 901    802    zeus23 4717191168 901    806    zeus08 4743823360 901    799    zeus13 4759572480 51.3  27.6  zeus15 1075937280 53.3  28.1  zeus03 1011904512 901    833    zeus13 5394223104 901    884    1430097920 zeus02 901    884    zeus01 1434165248 901    884    zeus01 2697859072 901    884    zeus04 865685504
25_sanfoundry_24_true-unreach-call.i 3.89 2.37 zeus14 214175744 3.64 2.12 zeus21 207040512 4.07 2.36 zeus02 211308544 11.6  6.28 389177344 zeus18 10.5  5.86 zeus13 383102976 10.5  5.95 zeus14 402731008 9.82 5.45 zeus17 368562176 4.10 2.49 zeus11 220045312 4.25 2.49 zeus24 211701760 4.32 2.59 zeus08 216784896 3.86 2.28 212926464 zeus22 3.80 2.31 zeus14 216727552 4.05 2.40 zeus13 209166336 3.96 2.30 zeus07 215015424
25_sanfoundry_27_true-unreach-call_ground.i 918    911    zeus22 11622240256 649    643    zeus17 14999998464 918    911    zeus20 11606777856 973    689    8952717312 zeus07 964    678    zeus01 8746909696 921    657    zeus16 9038938112 902    659    zeus03 9348960256 903    873    zeus01 1802588160 912    886    zeus20 2449821696 902    872    zeus07 2406297600 902    892    862584832 zeus01 902    892    zeus05 850268160 902    893    zeus17 826761216 902    892    zeus18 833032192
25_sanfoundry_43_true-unreach-call_ground.i 3.71 2.24 zeus18 210341888 4.19 2.50 zeus07 211054592 4.10 2.42 zeus06 211476480 5.72 3.31 316260352 zeus03 6.12 3.54 zeus15 317100032 5.65 3.26 zeus17 305475584 5.66 3.33 zeus02 296865792 4.35 2.60 zeus04 213843968 4.12 2.39 zeus05 211800064 4.07 2.42 zeus07 214917120 4.08 2.41 210141184 zeus04 4.05 2.39 zeus04 210010112 3.74 2.24 zeus11 209158144 4.06 2.42 zeus08 210165760
25_sorting_bubblesort_true-unreach-call_ground.i 13.5  8.42 zeus06 398135296 22.0  14.9  zeus08 636882944 902    889    zeus10 804290560 902    813    4567285760 zeus05 902    810    zeus05 4542943232 902    809    zeus15 4628140032 901    811    zeus08 4585721856 63.3  32.4  zeus17 983367680 902    856    zeus02 5116469248 901    821    zeus13 6392881152 901    891    746352640 zeus14 901    892    zeus06 748793856 902    890    zeus16 848097280 902    891    zeus16 856342528
25_sorting_selectionsort_true-unreach-call_ground.i 474    466    zeus14 14999998464 919    912    zeus13 13549490176 906    897    zeus13 4394471424 902    746    7748993024 zeus08 901    748    zeus13 7829950464 901    728    zeus12 7835807744 902    757    zeus10 7235469312 70.2  40.2  zeus13 1900040192 61.6  36.0  zeus19 2289889280 904    869    zeus11 2325921792 901    892    677990400 zeus14 901    893    zeus08 665772032 122    114    zeus18 696107008 901    891    zeus01 1162592256
25_standard_compareModified_true-unreach-call_ground.i 19.2  14.0  zeus14 532729856 902    887    zeus11 765665280 901    888    zeus10 793112576 902    808    4610117632 zeus23 902    810    zeus08 4656091136 901    818    zeus14 4624986112 902    842    zeus14 4840091648 44.4  22.9  zeus22 884490240 901    557    zeus21 7334543360 901    830    zeus08 5981577216 901    889    825782272 zeus24 901    889    zeus18 832094208 901    887    zeus08 911851520 901    889    zeus22 870854656
25_standard_compare_true-unreach-call_ground.i 902    889    zeus18 822247424 902    888    zeus04 1274675200 902    889    zeus17 770412544 901    816    4555591680 zeus14 901    817    zeus22 4575334400 901    813    zeus16 4617236480 901    826    zeus02 4546633728 901    745    zeus04 8879050752 902    654    zeus08 8744644608 906    588    zeus02 6919565312 901    891    801366016 zeus10 901    890    zeus12 810942464 902    889    zeus16 911982592 901    891    zeus06 876945408
25_standard_copy1_true-unreach-call_ground.i 13.1  8.44 zeus17 427229184 11.5  7.10 zeus13 395468800 544    530    zeus01 786010112 902    815    4604538880 zeus18 902    815    zeus05 4620132352 902    809    zeus24 4827987968 901    817    zeus06 4712890368 34.4  17.9  zeus09 869822464 29.8  15.5  zeus08 846635008 903    650    zeus06 8959299584 901    890    802762752 zeus18 901    890    zeus04 817840128 902    891    zeus22 811728896 901    890    zeus05 831287296
25_standard_copy2_true-unreach-call_ground.i 51.7  43.0  zeus11 1009512448 24.7  15.6  zeus12 738852864 901    885    zeus08 860114944 902    798    4641644544 zeus11 901    798    zeus16 4719882240 902    805    zeus08 4769304576 902    835    zeus03 4524081152 59.3  31.7  zeus01 1305862144 42.7  22.0  zeus21 868646912 902    794    zeus02 7225872384 902    891    790122496 zeus02 902    891    zeus01 793968640 901    892    zeus06 747307008 902    893    zeus20 694546432
25_standard_copy3_true-unreach-call_ground.i 154    144    zeus06 1921470464 35.8  25.6  zeus23 852082688 902    884    zeus19 883113984 902    788    4915273728 zeus11 901    796    zeus17 4870836224 901    804    zeus10 4756299776 901    838    zeus19 4616978432 84.1  53.4  zeus07 2918985728 49.4  26.0  zeus18 1374355456 901    827    zeus18 6407163904 902    891    810332160 zeus17 902    891    zeus14 803622912 901    894    zeus12 477892608 902    894    zeus24 671420416
25_standard_copy4_true-unreach-call_ground.i 430    418    zeus12 3188641792 59.2  46.2  zeus13 1166385152 902    884    zeus02 979771392 202    122    2615300096 zeus23 177    108    zeus13 2815377408 901    802    zeus18 4684406784 901    817    zeus01 4832358400 157    119    zeus10 4472299520 50.8  27.0  zeus07 1409368064 902    843    zeus07 5270011904 902    888    809558016 zeus13 901    889    zeus19 833740800 902    893    zeus24 597889024 901    892    zeus19 734236672
25_standard_copy5_true-unreach-call_ground.i 912    897    zeus02 5335986176 75.0  61.4  zeus24 1537974272 901    886    zeus21 921231360 214    138    2920931328 zeus10 202    130    zeus11 3252289536 901    797    zeus24 4620472320 901    773    zeus17 8018612224 242    202    zeus10 4522442752 63.2  34.8  zeus09 2443759616 902    844    zeus07 4826251264 902    891    761917440 zeus12 902    891    zeus03 765939712 902    893    zeus02 673366016 902    892    zeus19 741343232
25_standard_copy6_true-unreach-call_ground.i 905    890    zeus22 5737467904 101    87.1  zeus18 1763033088 902    887    zeus01 885125120 242    167    3548921856 zeus04 248    169    zeus08 4044660736 197    130    zeus14 3100459008 901    742    zeus02 8534913024 374    331    zeus17 4538384384 68.8  39.2  zeus19 3551268864 902    841    zeus04 4754399232 902    888    821911552 zeus22 902    888    zeus18 824528896 902    892    zeus24 716783616 901    890    zeus12 828887040
25_standard_copy7_true-unreach-call_ground.i 908    894    zeus12 5995823104 139    124    zeus03 1900605440 901    889    zeus08 886824960 306    224    4383916032 zeus06 302    220    zeus06 3795701760 236    166    zeus18 3714957312 902    650    zeus08 8933105664 567    527    zeus11 4583690240 77.7  48.0  zeus20 3949805568 902    843    zeus01 4747829248 902    890    780533760 zeus23 902    889    zeus09 777330688 902    891    zeus07 730292224 902    889    zeus07 833097728
25_standard_copy8_true-unreach-call_ground.i 902    886    zeus14 6881697792 162    147    zeus12 2606391296 901    888    zeus23 899719168 350    268    4821438464 zeus24 350    268    zeus06 4608081920 264    196    zeus11 4522455040 902    666    zeus18 10917715968 902    857    zeus08 4571987968 85.0  51.9  zeus11 3928309760 902    839    zeus02 4897800192 902    888    874876928 zeus03 902    890    zeus23 774156288 902    889    zeus03 731389952 902    891    zeus24 816320512
25_standard_copy9_true-unreach-call_ground.i 906    890    zeus20 6882660352 225    210    zeus24 3373965312 902    888    zeus13 887943168 446    356    4819304448 zeus10 394    313    zeus12 4788461568 303    234    zeus08 4376829952 905    589    zeus21 12306628608 902    857    zeus24 4571340800 79.5  47.9  zeus02 3988508672 902    836    zeus19 4978057216 902    889    828162048 zeus16 902    889    zeus15 831922176 902    889    zeus18 812670976 902    890    zeus05 851644416
25_standard_copyInitSum2_true-unreach-call_ground.i 61.0  51.7  zeus20 1165627392 47.3  35.9  zeus10 1050796032 902    885    zeus04 882511872 902    797    4918386688 zeus10 901    795    zeus13 4835483648 902    785    zeus09 5965676544 901    820    zeus18 5097574400 52.5  27.6  zeus08 1121296384 51.0  26.7  zeus13 1070538752 902    797    zeus15 6790799360 293    285    709664768 zeus03 325    316    zeus19 697311232 901    894    zeus19 473247744 901    892    zeus05 700665856
25_standard_copyInitSum3_true-unreach-call_ground.i 336    325    zeus03 2852601856 147    136    zeus21 1990189056 901    882    zeus12 906973184 901    752    6201995264 zeus07 901    757    zeus09 6575771648 901    778    zeus19 5708513280 901    825    zeus19 4653404160 108    69.3  zeus01 4073455616 61.8  32.3  zeus07 1434288128 902    760    zeus15 7913533440 855    844    786608128 zeus09 870    859    zeus03 791126016 902    893    zeus09 609103872 901    893    zeus09 700223488
25_standard_copyInitSum_true-unreach-call_ground.i 45.1  34.0  zeus01 978690048 40.1  30.2  zeus04 899362816 902    883    zeus21 886341632 902    797    4931784704 zeus14 901    791    zeus21 4875005952 901    784    zeus17 5927178240 902    812    zeus10 5050187776 119    82.8  zeus20 4471857152 64.6  34.4  zeus15 2320433152 902    802    zeus02 7525855232 902    887    829698048 zeus10 901    888    zeus19 816377856 901    895    zeus19 473227264 902    892    zeus17 710393856
25_standard_copyInit_true-unreach-call_ground.i 27.5  18.0  zeus24 767942656 23.6  14.5  zeus16 720162816 901    885    zeus24 840695808 902    793    4897394688 zeus11 902    797    zeus10 4799729664 901    786    zeus20 5942534144 902    811    zeus09 5128716288 55.1  28.7  zeus06 1390800896 40.5  21.1  zeus04 888573952 901    807    zeus19 7063728128 902    888    810807296 zeus20 901    888    zeus02 806817792 902    894    zeus07 1476943872 902    892    zeus09 678879232
25_standard_find_true-unreach-call_ground.i 902    888    zeus06 2386190336 4.13 2.43 zeus13 226623488 901    886    zeus07 2342662144 901    823    4725178368 zeus10 902    827    zeus21 4731367424 902    824    zeus08 4645093376 901    822    zeus15 4762345472 902    829    zeus04 5769551872 902    814    zeus17 6428672000 901    824    zeus10 6276222976 902    888    902471680 zeus07 901    889    zeus12 857067520 901    887    zeus07 886599680 901    888    zeus24 838922240
25_standard_init1_true-unreach-call_ground.i 10.9  6.59 zeus09 393621504 11.2  6.93 zeus04 401207296 145    133    zeus18 798846976 902    806    4879982592 zeus02 902    808    zeus07 4908032000 902    808    zeus05 4758876160 901    796    zeus23 5108469760 34.8  18.0  zeus02 853602304 32.8  16.9  zeus16 859938816 901    664    zeus14 8429690880 902    891    788447232 zeus02 902    891    zeus04 802791424 902    890    zeus07 867835904 901    892    zeus04 728371200
25_standard_init2_true-unreach-call_ground.i 22.9  13.7  zeus06 731799552 23.0  14.2  zeus22 706179072 901    885    zeus04 831557632 902    805    4802707456 zeus20 901    811    zeus06 4777037824 901    810    zeus15 4810743808 902    794    zeus19 5152362496 40.9  21.2  zeus12 868356096 41.1  21.4  zeus04 890429440 904    650    zeus13 10285297664 901    891    779833344 zeus13 901    891    zeus17 778285056 901    887    zeus03 863752192 901    893    zeus11 687775744
25_standard_init3_true-unreach-call_ground.i 31.1  21.2  zeus08 778358784 29.9  20.8  zeus15 762269696 902    883    zeus02 839114752 902    805    4721598464 zeus11 901    811    zeus07 4758859776 901    809    zeus06 4764061696 901    778    zeus19 5856858112 49.8  26.0  zeus16 982847488 45.4  23.7  zeus01 878964736 988    774    zeus09 11665534976 902    889    797290496 zeus10 901    889    zeus17 806105088 902    886    zeus13 816844800 902    892    zeus09 687923200
25_standard_init4_true-unreach-call_ground.i 42.8  31.9  zeus04 831852544 41.9  31.6  zeus17 899690496 901    882    zeus09 875872256 901    803    4812361728 zeus03 902    801    zeus14 4808900608 901    808    zeus09 4775325696 901    753    zeus04 6934691840 52.1  27.4  zeus06 1203441664 56.2  29.7  zeus22 1066446848 901    705    zeus03 11484696576 901    887    783335424 zeus02 901    887    zeus16 795566080 901    886    zeus01 799731712 902    892    zeus16 697540608
25_standard_init5_true-unreach-call_ground.i 61.9  49.2  zeus11 947408896 61.0  47.6  zeus15 1443487744 902    884    zeus24 893861888 902    803    4751691776 zeus05 901    800    zeus23 4837621760 902    800    zeus24 4745916416 902    737    zeus12 7088734208 60.0  32.9  zeus23 1271791616 57.4  31.0  zeus05 1585512448 1000    770    zeus02 11766173696 902    888    803905536 zeus03 902    888    zeus03 796958720 901    885    zeus21 787468288 902    892    zeus18 700583936
25_standard_init6_true-unreach-call_ground.i 81.9  68.1  zeus09 1505058816 71.5  60.1  zeus14 1445724160 901    883    zeus06 907685888 902    801    4785053696 zeus11 901    798    zeus22 4852850688 902    799    zeus10 4805746688 902    731    zeus10 7689134080 60.4  33.5  zeus24 1568608256 60.9  33.8  zeus15 2005012480 903    714    zeus09 10944397312 901    887    778268672 zeus22 901    886    zeus03 797802496 902    885    zeus13 786173952 901    891    zeus24 704585728
25_standard_init7_true-unreach-call_ground.i 99.6  86.1  zeus10 1742376960 95.4  82.7  zeus22 1606598656 902    882    zeus04 911261696 902    794    4799344640 zeus15 902    797    zeus04 4767281152 902    801    zeus02 4792852480 901    768    zeus15 6616072192 64.2  36.5  zeus03 1668263936 69.2  39.9  zeus22 2442428416 902    675    zeus15 9742200832 901    888    784801792 zeus15 901    888    zeus13 792010752 902    886    zeus01 786743296 902    890    zeus21 757067776
25_standard_init8_true-unreach-call_ground.i 125    111    zeus22 1863397376 119    106    zeus21 1750118400 901    881    zeus17 928616448 902    802    4825387008 zeus14 902    800    zeus19 4839137280 902    807    zeus01 4790910976 902    802    zeus16 5435228160 68.4  38.5  zeus21 1794715648 72.5  42.3  zeus15 2379120640 1000    688    zeus22 9256660992 902    886    809271296 zeus01 901    887    zeus01 779612160 902    885    zeus06 783740928 902    889    zeus10 784678912
25_standard_init9_true-unreach-call_ground.i 163    149    zeus23 2952646656 150    136    zeus20 2895220736 902    882    zeus06 935661568 902    796    4810031104 zeus16 902    802    zeus02 4809936896 902    803    zeus19 4889907200 902    800    zeus05 5449084928 74.3  45.4  zeus03 2072264704 81.1  50.7  zeus20 3033858048 901    636    zeus23 9039990784 901    886    810348544 zeus21 901    885    zeus21 826560512 902    886    zeus24 797532160 902    888    zeus20 829825024
25_standard_maxInArray_true-unreach-call_ground.i 521    515    zeus07 14999998464 628    622    zeus02 14999998464 526    520    zeus13 14999998464 1000    710    8823271424 zeus24 1000    704    zeus10 8860434432 1000    707    zeus12 8890634240 901    688    zeus13 8826683392 124    77.5  zeus02 5097345024 976    610    zeus12 10891010048 950    598    zeus09 11231174656 902    891    826744832 zeus02 902    892    zeus23 823767040 902    893    zeus22 873668608 902    892    zeus11 873574400
25_standard_minInArray_true-unreach-call_ground.i 547    541    zeus19 14999998464 710    703    zeus16 14999998464 552    546    zeus15 14999998464 1000    723    9009545216 zeus05 1000    712    zeus24 8850280448 1000    709    zeus19 9113698304 1000    733    zeus17 8754515968 904    572    zeus05 11235819520 368    236    zeus20 7391510528 905    568    zeus08 10989867008 902    892    840753152 zeus04 902    892    zeus01 864681984 902    892    zeus10 820105216 902    892    zeus07 836354048
25_standard_palindrome_true-unreach-call_ground.i 6.09 3.54 zeus08 246054912 6.24 3.59 zeus08 247205888 17.4  12.6  zeus17 443809792 901    798    5243617280 zeus04 901    802    zeus10 5262012416 902    793    zeus16 5407956992 159    109    zeus24 2705477632 10.9  5.96 zeus08 467243008 12.5  6.89 zeus13 361140224 44.2  22.7  zeus13 886603776 901    893    781795328 zeus24 901    893    zeus08 791678976 902    892    zeus04 804970496 902    893    zeus05 808476672
25_standard_partial_init_true-unreach-call_ground.i 903    895    zeus18 1731108864 903    896    zeus22 10577825792 130    124    zeus13 725004288 902    836    4612608000 zeus13 902    836    zeus16 4653854720 902    795    zeus02 5997154304 901    837    zeus20 4544548864 965    720    zeus08 12041363456 901    566    zeus17 11706789888 1000    879    zeus18 6887600128 902    895    882409472 zeus23 902    895    zeus24 874766336 904    897    zeus11 1595383808 902    890    zeus14 1005248512
25_standard_partition_original_true-unreach-call_ground.i 904    896    zeus03 2289618944 905    897    zeus18 5368352768 901    889    zeus05 832667648 901    829    4845576192 zeus02 901    829    zeus01 4850282496 901    823    zeus03 5052010496 901    839    zeus02 4514852864 969    595    zeus08 9091448832 902    557    zeus17 9280872448 901    727    zeus19 6861185024 905    895    882655232 zeus03 902    892    zeus02 874418176 902    890    zeus02 859463680 901    891    zeus15 887042048
25_standard_partition_true-unreach-call_ground.i 902    889    zeus19 2451275776 902    890    zeus23 821686272 901    885    zeus02 887566336 902    828    4638879744 zeus11 901    827    zeus21 4621864960 901    790    zeus09 5852991488 901    826    zeus11 4622696448 901    833    zeus20 6172618752 902    804    zeus24 7365857280 1000    689    zeus21 12249374720 902    893    756609024 zeus09 902    894    zeus14 763060224 902    895    zeus23 897241088 236    228    zeus21 753766400
25_standard_password_true-unreach-call_ground.i 902    889    zeus19 775720960 902    888    zeus03 771502080 902    889    zeus10 759963648 901    820    4574765056 zeus07 902    822    zeus23 4569763840 902    817    zeus10 4617367552 901    825    zeus12 4571283456 901    707    zeus12 8761671680 901    674    zeus12 8860934144 902    622    zeus09 8150769664 901    889    794689536 zeus19 902    891    zeus06 785911808 902    889    zeus23 900325376 902    891    zeus19 885919744
25_standard_reverse_true-unreach-call_ground.i 10.7  6.31 zeus18 378290176 10.2  6.12 zeus10 386859008 902    891    zeus09 780533760 901    809    4561690624 zeus08 901    816    zeus17 4578934784 901    823    zeus18 4586315776 901    826    zeus20 4687228928 29.6  15.5  zeus21 868564992 36.9  19.1  zeus24 856391680 901    839    zeus19 6060285952 901    894    481951744 zeus13 901    894    zeus09 491999232 902    891    zeus17 848089088 901    892    zeus01 737402880
25_standard_running_true-unreach-call.i 903    888    zeus22 2159742976 907    893    zeus01 4266815488 901    885    zeus17 850206720 901    828    4620935168 zeus23 902    829    zeus23 4628598784 902    824    zeus20 4943523840 902    820    zeus07 4921999360 1000    658    zeus09 11717410816 972    580    zeus04 9419419648 901    820    zeus09 5533536256 907    898    4864532480 zeus05 906    897    zeus14 3416276992 907    898    zeus08 4576260096 901    893    zeus12 499970048
25_standard_sentinel_true-unreach-call.i 4.09 2.43 zeus08 218574848 4.14 2.50 zeus12 220381184 4.66 2.74 zeus16 220360704 901    820    5012385792 zeus21 901    821    zeus03 4817575936 910    824    zeus15 5310365696 901    813    zeus18 5033734144 4.48 2.67 zeus10 220082176 4.39 2.58 zeus16 215543808 901    780    zeus21 7427026944 4.33 2.55 213475328 zeus09 4.19 2.51 zeus07 223268864 4.20 2.50 zeus08 212451328 4.69 2.86 zeus24 214564864
25_standard_seq_init_true-unreach-call_ground.i 14.9  9.93 zeus21 516628480 15.7  10.3  zeus02 509116416 14.9  9.76 zeus07 547491840 104    54.3  1447686144 zeus07 103    53.9  zeus05 1558425600 98.6  51.5  zeus06 1403236352 109    63.6  zeus06 1772584960 36.9  19.1  zeus02 849256448 33.7  17.6  zeus19 883486720 44.6  22.8  zeus20 890384384 14.3  9.19 442343424 zeus08 14.0  8.98 zeus21 442884096 13.7  8.82 zeus13 439062528 22.2  16.8  zeus07 483545088
25_standard_strcmp_true-unreach-call_ground.i 104    97.8  zeus06 742498304 14.8  8.57 zeus17 545714176 18.6  10.7  zeus14 614653952 901    801    4539273216 zeus03 901    801    zeus18 4549312512 93.8  49.5  zeus02 1586421760 271    194    zeus22 5207085056 34.8  18.0  zeus23 855547904 39.1  20.2  zeus14 881041408 36.8  19.0  zeus01 837378048 901    891    784470016 zeus01 902    892    zeus16 782417920 18.0  12.4  zeus20 496963584 26.9  18.9  zeus23 627011584
25_standard_strcpy_original_true-unreach-call.i 901    893    zeus09 718692352 901    892    zeus24 718835712 902    890    zeus05 746999808 901    827    4765396992 zeus24 901    825    zeus23 4818608128 901    826    zeus10 4918120448 902    838    zeus01 4597153792 4.34 2.55 zeus01 216518656 902    832    zeus18 5847957504 943    794    zeus21 6841200640 902    891    802783232 zeus05 902    893    zeus18 812273664 902    893    zeus01 827244544 901    890    zeus15 881250304
25_standard_strcpy_true-unreach-call_ground.i 4.31 2.55 zeus24 216453120 3.95 2.34 zeus10 216698880 901    886    zeus22 777981952 901    825    4709154816 zeus22 901    821    zeus01 4715323392 902    827    zeus14 4642996224 901    830    zeus01 4548997120 5.06 2.97 zeus02 221356032 902    842    zeus22 6110777344 902    818    zeus18 6650761216 902    888    815501312 zeus12 901    888    zeus08 822349824 901    887    zeus04 969117696 902    892    zeus03 871981056
25_standard_two_index_01_true-unreach-call.i 13.0  8.48 zeus02 437350400 10.9  6.91 zeus17 420278272 902    888    zeus12 817184768 901    822    4704129024 zeus20 901    819    zeus18 4658900992 901    808    zeus06 4908879872 901    829    zeus17 4569878528 36.7  19.0  zeus18 865935360 35.0  18.1  zeus19 862887936 902    795    zeus21 7772110848 901    889    810156032 zeus13 901    889    zeus24 808587264 902    890    zeus03 840753152 901    890    zeus14 777564160
25_standard_two_index_02_true-unreach-call.i 6.16 3.55 zeus02 252944384 8.19 4.61 zeus19 274370560 108    100    zeus02 725385216 901    827    4623024128 zeus01 901    828    zeus16 4613447680 266    208    zeus06 4073541632 901    830    zeus22 4624003072 13.4  7.36 zeus08 506175488 11.1  6.18 zeus01 378642432 57.0  30.6  zeus10 1174335488 902    893    797716480 zeus22 901    892    zeus06 790011904 901    891    zeus24 778809344 456    449    zeus10 774934528
25_standard_two_index_03_true-unreach-call.i 5.13 2.96 zeus20 232804352 6.51 3.79 zeus12 246595584 22.7  17.3  zeus06 401547264 902    829    4711632896 zeus16 902    831    zeus24 4734668800 87.9  46.3  zeus08 1267073024 902    832    zeus17 4587692032 7.02 4.01 zeus16 271151104 6.52 3.66 zeus01 254685184 39.5  20.5  zeus04 846680064 170    165    670633984 zeus03 205    198    zeus17 682041344 46.0  40.8  zeus01 556384256 56.7  51.6  zeus03 444293120
25_standard_two_index_04_true-unreach-call.i 4.46 2.65 zeus08 219029504 5.44 3.14 zeus07 244973568 13.8  9.26 zeus11 345329664 153    104    2538762240 zeus14 156    106    zeus10 3086254080 63.1  32.2  zeus07 922013696 640    580    zeus23 4486496256 5.53 3.22 zeus13 240615424 5.33 3.09 zeus05 230035456 24.6  13.0  zeus04 723099648 43.8  39.5  417701888 zeus08 40.9  36.8  zeus13 421797888 21.2  17.0  zeus23 339341312 22.7  19.1  zeus13 312664064
25_standard_two_index_05_true-unreach-call.i 4.39 2.60 zeus06 224894976 5.39 3.15 zeus17 226734080 9.52 6.15 zeus24 279212032 87.7  49.2  1498021888 zeus04 96.1  53.6  zeus04 1377529856 54.5  28.0  zeus23 884649984 236    188    zeus23 3677704192 5.13 2.97 zeus08 229638144 4.82 2.84 zeus06 229769216 17.1  9.18 zeus20 608628736 24.0  20.1  335056896 zeus23 22.4  18.8  zeus12 323686400 10.1  6.84 zeus09 273260544 14.4  10.9  zeus20 283840512
25_standard_two_index_06_true-unreach-call.i 4.08 2.44 zeus11 225181696 901    885    zeus04 2308059136 7.76 4.81 zeus13 258097152 55.1  28.7  997625856 zeus11 54.9  28.6  zeus19 952995840 40.5  20.9  zeus08 860905472 131    86.9  zeus13 2744623104 5.03 2.98 zeus09 229056512 4.69 2.83 zeus06 222691328 14.7  7.95 zeus14 534323200 12.0  9.11 267382784 zeus03 11.8  8.96 zeus14 266125312 6.98 4.39 zeus22 244232192 8.60 6.06 zeus22 248725504
25_standard_two_index_07_true-unreach-call.i 4.20 2.51 zeus06 222351360 6.27 3.62 zeus09 260435968 8.89 5.57 zeus01 255664128 55.2  28.6  966168576 zeus09 57.1  29.7  zeus15 959516672 40.4  20.9  zeus05 882728960 141    92.8  zeus02 2760404992 4.87 2.86 zeus06 228085760 4.78 2.83 zeus18 230277120 16.3  8.67 zeus02 523747328 12.4  9.45 262590464 zeus02 12.6  9.56 zeus13 270209024 7.03 4.51 zeus16 238718976 9.85 6.93 zeus08 251760640
25_standard_two_index_08_true-unreach-call.i 3.93 2.33 zeus22 219783168 902    888    zeus09 4199686144 6.42 3.92 zeus21 254681088 43.1  22.2  862380032 zeus11 46.4  23.9  zeus07 879583232 31.4  16.2  zeus03 669822976 88.7  50.8  zeus03 1809965056 4.87 2.85 zeus16 225644544 4.49 2.66 zeus19 222720000 10.4  5.78 zeus06 379936768 7.87 5.33 238030848 zeus02 7.20 4.97 zeus12 237727744 5.66 3.41 zeus04 224768000 6.84 4.35 zeus18 240914432
25_standard_two_index_09_true-unreach-call.i 4.07 2.44 zeus04 222916608 5.24 3.09 zeus24 233549824 5.69 3.47 zeus15 231718912 46.8  24.2  883937280 zeus20 43.5  22.3  zeus24 892579840 30.2  15.8  zeus23 678744064 85.2  48.5  zeus22 1880817664 4.77 2.75 zeus03 219189248 4.61 2.73 zeus11 224706560 10.0  5.54 zeus06 360906752 7.25 4.90 236883968 zeus20 7.10 4.82 zeus17 235401216 5.77 3.62 zeus01 224256000 6.50 4.17 zeus21 244260864
25_standard_vararg_true-unreach-call_ground.i 902    887    zeus18 2486161408 4.21 2.52 zeus18 214962176 901    886    zeus08 2570493952 902    827    4691734528 zeus24 901    824    zeus21 4686434304 902    833    zeus01 4585242624 902    824    zeus09 4603203584 902    771    zeus03 7221383168 902    804    zeus16 8216600576 901    787    zeus05 8428093440 902    888    835371008 zeus02 901    888    zeus15 867016704 902    888    zeus04 900538368 901    888    zeus03 876277760
25_standard_vector_difference_true-unreach-call_ground.i 15.5  11.2  zeus13 488779776 11.6  7.32 zeus09 404512768 902    891    zeus01 788127744 901    815    4639072256 zeus08 901    816    zeus02 4701745152 902    822    zeus02 4643176448 901    838    zeus05 4560912384 41.5  21.3  zeus03 897871872 37.3  19.3  zeus09 864559104 901    833    zeus11 5302317056 902    893    1017118720 zeus23 901    892    zeus13 849760256 901    889    zeus21 973713408 902    892    zeus06 815706112
test/programs/array-simplified-benchmarks/arrays-size-25/ status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage
total tasks 88 28400   27500    260881252352 88 18600   17800   200505901056 88 45700 44600 139837726720 88 55400 52600   399843770368 88 54800 53000   396609683456 88 50900 49900 396560924672 88 62800 53800 465423548416 88 19000 14800   239328399360 88 19100   14200   236629614592 88 45400 37700   406582697984 88 46700 45800 68585709568 88 46700 45900 66988093440 88 44400 43600 68716183552 88 49300 48500 64379318272
    correct results 21 2060   1830    27086008320 31 2090   1750   35349045248 35 3520 3180 23395995648 19 2180 1340   39344771072 19 2190 1350   40386215936 23 2640 1670 44951138304 22 5410 4180 71943938048 29 2820 1980   57903833088 29 2050   1300   49169805312 38 3150 2160   72164950016 38 3840 3520 25283960832 38 3930 3610 25355116544 36 1790 1510 21248000000 34 5040 4750 22144278528
        correct true 3 53.0 45.2  799653888 5 28.1 16.4 1197899776 15 912 841 5734686720 8 459 266   8452333568 8 471 273   8848662528 11 914 604 14635577344 9 1500 1160 20730916864 4 240 182   5153955840 4 99.3 55.0 2578194432 12 343 186   8672047104 13 1830 1770 5390299136 13 1940 1870 5413093376 11 184 144 3486490624 12 678 630 4195999744
        correct false 18 2000   1790    26286354432 26 2060   1740   34151145472 20 2610 2340 17661308928 11 1720 1070   30892437504 11 1720 1080   31537553408 12 1720 1060 30315560960 13 3910 3010 51213021184 25 2580 1800   52749877248 25 1960   1250   46591610880 26 2810 1970   63492902912 25 2010 1750 19893661696 25 1990 1730 19942023168 25 1610 1370 17761509376 22 4360 4130 17948278784
    incorrect results 1 14.9 9.93 516628480 3 74.1 47.9 1916452864 3 142 114 2046017536 1 104 54.3 1447686144 1 103 53.9 1558425600 3 347 196 5945573376 2 379 257 6979670016 2 161 98.2 5321011200 3 304   221   6254960640 3 173 90.6 3316514816 2 443 421 1356267520 2 421 400 1357729792 3 133 110 1753894912 3 148 119 1945886720
        incorrect true 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 1 14.9 9.93 516628480 3 74.1 47.9 1916452864 3 142 114 2046017536 1 104 54.3 1447686144 1 103 53.9 1558425600 3 347 196 5945573376 2 379 257 6979670016 2 161 98.2 5321011200 3 304   221   6254960640 3 173 90.6 3316514816 2 443 421 1356267520 2 421 400 1357729792 3 133 110 1753894912 3 148 119 1945886720
score (88 tasks, max score: 148) 8 -12 2 11 11 -14 -1 1 -15 2 19 19 -1 -2
Run set MathSAT5-heaparray.ArraysReach25 MathSAT5-oldarray.ArraysReach25 MathSAT5-uf.ArraysReach25 PRINCESS-heaparray-quantifiers.ArraysReach25 PRINCESS-heaparray.ArraysReach25 PRINCESS-oldarray.ArraysReach25 PRINCESS-uf.ArraysReach25 SMTInterpol-heaparray.ArraysReach25 SMTInterpol-oldarray.ArraysReach25 SMTInterpol-uf.ArraysReach25 Z3-heaparray-quantifiers.ArraysReach25 Z3-heaparray.ArraysReach25 Z3-oldarray.ArraysReach25 Z3-uf.ArraysReach25