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.ArraysReach50 MathSAT5-oldarray.ArraysReach50 MathSAT5-uf.ArraysReach50 PRINCESS-heaparray-quantifiers.ArraysReach50 PRINCESS-heaparray.ArraysReach50 PRINCESS-oldarray.ArraysReach50 PRINCESS-uf.ArraysReach50 SMTInterpol-heaparray.ArraysReach50 SMTInterpol-oldarray.ArraysReach50 SMTInterpol-uf.ArraysReach50 Z3-heaparray-quantifiers.ArraysReach50 Z3-heaparray.ArraysReach50 Z3-oldarray.ArraysReach50 Z3-uf.ArraysReach50
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-50/ 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) 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) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage
50_data_structures_set_multi_proc_false-unreach-call_ground.i 902    895    zeus11 740634624 135    120    zeus10 1638154240 901    887    zeus20 819564544 901    841    4781756416 zeus21 902    833    4775464960 zeus16 861    722    zeus17 8336441344 903    772    zeus15 7933288448 902    844    zeus18 5128691712 102    66.3  zeus22 2741690368 148    107    zeus01 4518244352 901    893    579194880 zeus09 901    893    zeus04 623591424 395    376    zeus10 910446592 433    414    zeus10 1066893312
50_sorting_bubblesort_false-unreach-call2_ground.i 64.5  52.6  zeus02 1252904960 54.5  42.3  zeus03 1064689664 191    174    zeus10 1027887104 121    69.4  2036822016 zeus04 119    67.8  1999511552 zeus04 115    65.9  zeus19 1985622016 239    176    zeus12 4692434944 91.3  52.7  zeus17 2308165632 88.6  52.3  zeus23 3710373888 132    97.0  zeus05 2917679104 80.1  68.2  807424000 zeus10 76.1  64.8  zeus11 794640384 73.6  62.5  zeus09 809615360 826    812    zeus24 869691392
50_sorting_bubblesort_false-unreach-call_ground.i 70.4  55.6  zeus21 1282592768 54.9  42.6  zeus14 1041551360 185    171    zeus09 987455488 124    70.9  1967923200 zeus02 115    66.0  2422329344 zeus04 123    69.9  zeus08 2138533888 247    185    zeus17 4678324224 89.4  48.8  zeus21 2470670336 77.3  43.8  zeus21 2629132288 116    81.4  zeus20 2741186560 80.8  68.8  811081728 zeus05 77.4  65.9  zeus14 830709760 74.0  62.7  zeus21 810594304 874    857    zeus24 879607808
50_sorting_selectionsort_false-unreach-call2_ground.i 31.4  20.7  zeus04 804970496 31.0  20.2  zeus14 804794368 41.1  28.6  zeus09 965345280 227    165    3606597632 zeus03 230    168    4477317120 zeus08 233    169    zeus10 3567677440 245    183    zeus14 4284182528 74.2  44.5  zeus07 1585475584 74.4  42.2  zeus15 2164494336 75.0  45.1  zeus18 2223226880 149    136    820854784 zeus14 142    130    zeus11 827334656 132    120    zeus16 823705600 239    222    zeus16 875347968
50_sorting_selectionsort_false-unreach-call_ground.i 896    883    zeus07 14999998464 914    901    zeus11 14186868736 903    888    zeus19 7880376320 901    727    6669606912 zeus08 903    751    7094157312 zeus16 903    745    zeus07 6890622976 901    741    zeus07 6910033920 327    257    zeus15 6119747584 223    155    zeus16 6440890368 902    833    zeus10 5798670336 287    276    869953536 zeus06 412    400    zeus24 872579072 322    310    zeus08 780701696 901    882    zeus10 1878855680
50_standard_allDiff2_false-unreach-call_ground.i 902    880    zeus20 2529947648 902    881    zeus23 2830225408 902    875    zeus18 4616749056 902    790    5472690176 zeus23 902    790    5324546048 zeus01 902    797    zeus01 5327147008 902    799    zeus17 5275123712 902    851    zeus14 4669313024 902    859    zeus10 4602494976 902    859    zeus17 4608217088 902    880    1113923584 zeus17 902    879    zeus10 1002844160 902    880    zeus16 1133461504 902    880    zeus24 1115783168
50_standard_copy1_false-unreach-call_ground.i 31.7  21.0  zeus04 834519040 31.1  20.8  zeus14 835403776 127    114    zeus07 923004928 664    504    8811642880 zeus07 617    488    8690794496 zeus18 558    434    zeus16 8585789440 902    838    zeus04 4546048000 71.1  42.4  zeus23 1438085120 60.9  34.4  zeus02 1799471104 84.0  51.6  zeus14 4018843648 51.0  42.1  789278720 zeus13 48.7  40.9  zeus17 760094720 45.9  38.3  zeus11 779460608 483    472    zeus03 829763584
50_standard_copy2_false-unreach-call_ground.i 913    899    zeus02 10407968768 186    172    zeus21 1946025984 799    779    zeus11 1305403392 407    1030    4985479168 zeus20 411    1030    5078999040 zeus19 672    1030    zeus13 8213897216 902    834    zeus06 4657504256 96.6  60.0  zeus01 2959060992 78.5  50.0  zeus04 3532783616 142    106    zeus11 4508868608 126    113    1025638400 zeus05 124    111    zeus24 1023459328 114    101    zeus13 890568704 902    890    zeus07 782188544
50_standard_copy3_false-unreach-call_ground.i 913    898    zeus22 11325829120 388    368    zeus13 3732439040 901    886    zeus23 905744384 939    777    6494097408 zeus08 925    776    6413627392 zeus10 981    720    zeus19 8993988608 901    779    zeus12 7819849728 130    89.9  zeus17 4109996032 113    77.7  zeus10 4435140608 270    227    zeus13 4658860032 248    233    1253969920 zeus04 232    217    zeus12 1245786112 201    187    zeus22 938176512 901    889    zeus05 788783104
50_standard_copy4_false-unreach-call_ground.i 902    887    zeus22 6946975744 701    677    zeus20 4844167168 901    888    zeus22 911335424 902    775    5389058048 zeus24 902    776    5396127744 zeus03 902    713    zeus24 6984445952 902    664    zeus01 9292558336 253    206    zeus03 4599500800 144    102    zeus15 4496928768 512    457    zeus10 4950839296 385    367    1489637376 zeus06 389    369    zeus21 1513439232 321    303    zeus19 995139584 901    891    zeus21 787472384
50_standard_copy5_false-unreach-call_ground.i 907    889    zeus12 4900454400 902    884    zeus10 4856107008 901    891    zeus12 871374848 918    787    5413310464 zeus20 902    776    5405892608 zeus13 909    717    zeus10 7007682560 902    609    zeus14 11848429568 322    271    zeus02 4617199616 199    155    zeus13 4512190464 895    833    zeus14 5131472896 582    561    1715228672 zeus15 552    531    zeus23 1732775936 468    449    zeus04 1005744128 902    893    zeus22 754864128
50_standard_copy6_false-unreach-call_ground.i 901    882    zeus21 4742561792 904    885    zeus23 4810928128 901    892    zeus09 851296256 902    796    5133242368 zeus23 902    795    5152059392 zeus23 911    790    zeus11 5478739968 924    581    zeus14 11011186688 645    590    zeus07 4659306496 211    169    zeus01 4512059392 901    838    zeus05 5127692288 794    769    2044735488 zeus01 782    756    zeus17 2037444608 666    644    zeus11 1034723328 902    893    zeus18 762298368
50_standard_copy7_false-unreach-call_ground.i 902    882    zeus03 3581022208 909    886    zeus05 4421640192 902    893    zeus17 848449536 902    803    4635705344 zeus19 902    808    4784119808 zeus07 902    808    zeus18 4696301568 954    621    zeus07 11171323904 869    808    zeus13 4718346240 356    306    zeus07 4622082048 902    843    zeus12 5099778048 902    882    1241075712 zeus16 902    885    zeus13 1273749504 845    822    zeus23 1044340736 902    893    zeus12 725561344
50_standard_copy8_false-unreach-call_ground.i 901    878    zeus02 2439876608 902    880    zeus16 3196366848 902    894    zeus03 844021760 902    806    4712173568 zeus15 902    811    4690812928 zeus06 902    812    zeus21 4687343616 903    643    zeus07 12602630144 903    843    zeus04 4769079296 270    219    zeus21 4626001920 902    846    zeus18 5009506304 902    885    1097793536 zeus18 902    882    zeus15 1075019776 902    885    zeus21 980582400 902    893    zeus01 761118720
50_standard_copy9_false-unreach-call_ground.i 902    878    zeus20 2437365760 901    880    zeus03 2405281792 902    896    zeus06 1544798208 902    812    4717572096 zeus16 902    810    4711292928 zeus12 902    809    zeus09 4638224384 902    695    zeus11 12469207040 902    843    zeus16 4760870912 387    339    zeus23 4632403968 901    845    zeus10 5054570496 902    886    1067327488 zeus08 902    885    zeus04 1072521216 902    886    zeus16 970960896 902    894    zeus10 764383232
50_standard_copyInitSum2_false-unreach-call_ground.i 660    646    zeus01 7109541888 646    625    zeus10 4390129664 902    885    zeus21 977276928 1000    737    8640765952 zeus02 955    705    9104728064 zeus03 292    217    zeus14 4230950912 901    840    zeus13 4562604032 879    823    zeus16 4622643200 117    78.3  zeus01 4440567808 180    136    zeus22 4526231552 901    889    846163968 zeus12 901    888    zeus05 857153536 902    889    zeus08 805392384 901    889    zeus18 790732800
50_standard_init1_false-unreach-call_ground.i 43.7  32.8  zeus21 880832512 43.5  32.8  zeus20 851927040 67.7  55.4  zeus16 876457984 206    144    3807342592 zeus21 209    146    3851616256 zeus08 219    151    zeus12 3268206592 419    338    zeus24 5319024640 76.5  43.9  zeus09 1709502464 62.2  35.0  zeus18 2096832512 76.7  46.9  zeus08 2275901440 50.5  41.6  804257792 zeus01 49.2  40.9  zeus16 805851136 47.4  39.1  zeus22 805572608 344    332    zeus24 819445760
50_standard_init2_false-unreach-call_ground.i 159    143    zeus11 1918717952 149    135    zeus21 1991675904 225    206    zeus09 958918656 398    1030    5519839232 zeus08 385    1030    5476704256 zeus02 350    1030    zeus08 5537722368 856    709    zeus01 6835212288 89.5  54.6  zeus09 2351669248 83.3  53.3  zeus11 4358012928 113    77.6  zeus10 3636461568 125    108    899108864 zeus23 116    101    zeus14 883924992 116    102    zeus01 889556992 901    889    zeus06 780222464
50_standard_init3_false-unreach-call_ground.i 391    375    zeus01 4780507136 381    364    zeus13 4791746560 489    465    zeus03 1011830784 415    1030    5856501760 zeus22 410    1030    5908926464 zeus08 399    1030    zeus03 5891682304 901    794    zeus03 5344460800 115    76.1  zeus18 2795286528 109    75.1  zeus06 4399689728 140    102    zeus12 4490678272 193    178    956567552 zeus11 194    180    zeus16 940273664 196    182    zeus04 946565120 901    888    zeus05 790175744
50_standard_init4_false-unreach-call_ground.i 774    753    zeus19 7120252928 801    781    zeus14 7063625728 861    837    zeus24 1200881664 478    1030    5808570368 zeus23 466    1030    5802786816 zeus22 496    1030    zeus17 5770264576 902    809    zeus09 5139292160 138    101    zeus09 3565142016 119    84.0  zeus11 4434034688 171    131    zeus16 4525957120 312    293    1023627264 zeus21 302    284    zeus07 1026686976 312    294    zeus06 1003298816 901    889    zeus10 777879552
50_standard_init5_false-unreach-call_ground.i 902    883    zeus22 6972428288 903    886    zeus01 6095499264 902    881    zeus04 877162496 661    1030    5645303808 zeus23 601    1030    5640052736 zeus12 588    1030    zeus18 5613473792 903    812    zeus20 5206605824 152    111    zeus01 4504117248 147    110    zeus03 4485902336 209    168    zeus16 4597194752 457    436    1052221440 zeus14 432    414    zeus18 1051164672 455    437    zeus14 1061896192 901    888    zeus03 796925952
50_standard_init6_false-unreach-call_ground.i 902    884    zeus13 7143747584 910    890    zeus24 7153979392 902    879    zeus18 835375104 753    1030    5816573952 zeus21 726    1030    5790240768 zeus02 730    1030    zeus15 5623312384 902    808    zeus07 5295869952 179    138    zeus19 4501737472 170    130    zeus22 4502265856 269    222    zeus15 4554158080 589    567    1128050688 zeus06 583    559    zeus23 1092599808 619    597    zeus21 1081368576 901    887    zeus18 816672768
50_standard_init7_false-unreach-call_ground.i 902    879    zeus10 3880140800 912    892    zeus12 6138376192 902    881    zeus18 818089984 875    1030    5707853824 zeus09 863    1030    5652021248 zeus17 902    785    zeus04 5583212544 902    815    zeus11 5415632896 214    172    zeus10 4541734912 210    165    zeus19 4553564160 323    275    zeus11 4665786368 797    772    1152106496 zeus07 767    744    zeus11 1156440064 811    788    zeus18 1141223424 901    889    zeus17 792641536
50_standard_init8_false-unreach-call_ground.i 902    880    zeus14 2623901696 903    882    zeus02 3831799808 902    881    zeus17 834125824 902    809    4615233536 zeus06 902    806    4641665024 zeus03 902    814    zeus08 4584325120 902    810    zeus02 5406998528 252    206    zeus09 4509184000 238    195    zeus07 4527833088 369    317    zeus11 4581134336 902    884    835846144 zeus03 902    884    zeus20 821903360 902    886    zeus23 817053696 901    888    zeus17 814514176
50_standard_init9_false-unreach-call_ground.i 901    878    zeus10 2398302208 902    878    zeus24 1325400064 902    881    zeus07 829739008 901    814    4593090560 zeus08 902    808    4622594048 zeus04 902    814    zeus02 4579450880 902    819    zeus05 5078937600 271    224    zeus05 4560654336 192    146    zeus21 4572135424 571    511    zeus20 4659490816 902    885    818540544 zeus24 902    884    zeus15 830476288 902    884    zeus09 808046592 901    887    zeus12 822878208
50_standard_minInArray_false-unreach-call_ground.i 44.6  33.2  zeus12 993550336 41.5  30.9  zeus08 797413376 37.5  25.7  zeus17 945917952 927    668    9056301056 zeus09 992    700    8760360960 zeus15 1000    703    zeus22 8723759104 1000    716    zeus21 8881647616 903    638    zeus20 12839874560 937    649    zeus13 12879224832 901    628    zeus05 11927957504 65.6  55.1  800333824 zeus16 67.0  55.6  zeus01 795779072 64.3  53.7  zeus16 795537408 67.2  55.7  zeus21 805879808
50_standard_partition_false-unreach-call_ground.i 914    897    zeus19 11383283712 903    887    zeus10 4039471104 902    885    zeus23 909430784 902    814    4786573312 zeus09 902    816    4758827008 zeus07 902    818    zeus22 4704239616 902    827    zeus19 4922511360 1000    632    zeus17 11075166208 902    546    zeus20 9904889856 902    850    zeus13 5394251776 901    889    772284416 zeus14 901    888    zeus05 774918144 902    888    zeus05 751534080 901    889    zeus19 795492352
50_standard_running_false-unreach-call.i 535    511    zeus01 2214952960 193    173    zeus01 1686925312 218    192    zeus17 1031708672 462    1030    4801306624 zeus01 483    1030    4853354496 zeus17 576    474    zeus05 6590545920 901    843    zeus13 4568788992 888    829    zeus12 4567228416 160    120    zeus14 4481757184 153    104    zeus07 4503605248 286    268    962445312 zeus02 256    240    zeus15 947294208 247    230    zeus13 906489856 720    700    zeus13 913776640
50_data_structures_set_multi_proc_trivial_true-unreach-call_ground.i 227    222    zeus12 649695232 7.57 4.26 zeus16 271294464 32.4  26.1  zeus06 400211968 901    844    4790923264 zeus03 901    842    4708708352 zeus21 902    800    zeus16 4627918848 901    765    zeus11 7846174720 902    838    zeus09 5212340224 240    192    zeus07 4485177344 393    335    zeus02 4527448064 901    892    653524992 zeus13 901    891    zeus06 642854912 431    413    zeus06 795709440 598    578    zeus02 824987648
50_data_structures_set_multi_proc_true-unreach-call_ground.i 902    895    zeus09 708571136 903    880    zeus24 2524729344 901    888    zeus14 810885120 901    842    4715192320 zeus08 901    844    4675633152 zeus02 519    434    zeus05 4646510592 901    769    zeus17 7903158272 903    843    zeus11 5200064512 149    102    zeus16 4468531200 192    141    zeus13 4524081152 902    894    607178752 zeus19 901    893    zeus18 591024128 901    886    zeus11 748994560 902    887    zeus11 808775680
50_relax_true-unreach-call.i 5.04 2.90 zeus06 222810112 4.45 2.60 zeus03 222064640 4.76 2.79 zeus19 213704704 5.67 3.28 311341056 zeus12 5.59 3.21 309112832 zeus12 9.67 5.42 zeus11 410107904 5.63 3.26 zeus01 309276672 4.37 2.58 zeus15 220073984 5.05 2.89 zeus06 230555648 4.20 2.51 zeus07 221319168 4.14 2.43 218210304 zeus14 4.38 2.53 zeus08 214110208 5.16 3.01 zeus06 224321536 4.34 2.53 zeus13 219086848
50_sanfoundry_02_true-unreach-call_ground.i 919    907    zeus02 14693990400 911    899    zeus12 8000012288 881    869    zeus23 14999998464 903    668    8984436736 zeus15 1000    705    8705748992 zeus02 954    682    zeus09 8799895552 1000    703    zeus09 8869662720 912    878    zeus08 2492289024 902    865    zeus18 4450488320 904    869    zeus22 2215280640 901    886    806268928 zeus12 901    887    zeus02 798015488 901    886    zeus17 797233152 901    886    zeus20 798670848
50_sanfoundry_10_true-unreach-call_ground.i 63.7  52.5  zeus07 1431248896 84.0  70.5  zeus18 1656815616 902    875    zeus20 5063540736 901    782    4979224576 zeus18 902    787    5091581952 zeus14 902    789    zeus22 5079646208 901    755    zeus14 7240589312 181    145    zeus03 3699748864 161    125    zeus12 4463636480 902    835    zeus13 4787671040 901    880    2246205440 zeus07 901    881    zeus12 2244653056 901    881    zeus17 3428573184 901    884    zeus02 873107456
50_sanfoundry_24_true-unreach-call.i 3.92 2.30 zeus03 210259968 3.82 2.29 zeus12 212180992 3.85 2.31 zeus18 216637440 11.0  6.10 413884416 zeus22 11.0  5.98 395804672 zeus07 11.2  6.15 zeus06 385728512 10.9  5.98 zeus10 386506752 4.29 2.52 zeus19 218587136 4.10 2.50 zeus02 216133632 4.29 2.53 zeus16 221609984 3.80 2.27 209899520 zeus10 3.80 2.23 zeus03 210145280 3.86 2.30 zeus12 213512192 3.96 2.33 zeus06 212942848
50_sanfoundry_27_true-unreach-call_ground.i 490    479    zeus23 14999998464 913    901    zeus19 11830669312 502    491    zeus15 14999998464 904    668    10006081536 zeus14 940    649    9048752128 zeus10 994    671    zeus18 8827211776 912    614    zeus15 8692965376 909    866    zeus03 3187585024 911    863    zeus10 4500246528 273    202    zeus16 5879685120 901    886    866832384 zeus08 901    886    zeus09 861401088 901    886    zeus22 892379136 901    886    zeus06 809840640
50_sanfoundry_43_true-unreach-call_ground.i 3.80 2.25 zeus24 208236544 3.59 2.14 zeus12 205398016 4.05 2.41 zeus22 216018944 6.19 3.62 331628544 zeus06 5.92 3.40 331407360 zeus08 5.21 3.11 zeus23 315551744 5.41 3.14 zeus08 305037312 3.94 2.37 zeus04 216801280 3.97 2.34 zeus15 207601664 4.26 2.53 zeus13 214700032 4.20 2.54 208097280 zeus17 3.84 2.26 zeus11 213995520 3.77 2.26 zeus11 214523904 3.99 2.35 zeus23 207380480
50_sorting_bubblesort_true-unreach-call_ground.i 48.2  35.9  zeus05 754999296 48.6  34.7  zeus21 765419520 902    882    zeus14 959684608 901    797    4635926528 zeus09 901    799    4566315008 zeus17 901    802    zeus19 4551512064 901    801    zeus11 4715655168 901    846    zeus09 4886073344 902    852    zeus14 4628164608 901    839    zeus11 4701589504 902    887    834015232 zeus05 901    888    zeus14 833908736 901    886    zeus24 939814912 902    887    zeus12 814837760
50_sorting_selectionsort_true-unreach-call_ground.i 913    899    zeus02 14856306688 671    659    zeus17 14999998464 908    892    zeus22 6475882496 903    735    6841724928 zeus08 901    742    6853394432 zeus04 902    752    zeus03 7452053504 909    742    zeus11 6852386816 478    388    zeus13 6492987392 152    107    zeus10 5420490752 903    834    zeus11 5731262464 902    887    1098346496 zeus14 902    888    zeus17 967520256 151    140    zeus08 761884672 904    884    zeus02 1728978944
50_standard_compareModified_true-unreach-call_ground.i 130    120    zeus04 2238885888 901    884    zeus16 1331220480 901    888    zeus15 885805056 392    311    4667191296 zeus15 337    269    4196118528 zeus22 902    810    zeus24 4567289856 902    810    zeus13 5731328000 78.0  48.6  zeus24 1664720896 902    701    zeus14 8098660352 901    837    zeus05 5498630144 902    888    863817728 zeus24 902    888    zeus24 859840512 901    885    zeus17 966184960 901    888    zeus07 797986816
50_standard_compare_true-unreach-call_ground.i 901    886    zeus10 1317224448 901    886    zeus14 1303867392 901    886    zeus12 1416372224 901    807    4567617536 zeus09 902    809    4582920192 zeus14 901    806    zeus05 4553355264 901    816    zeus18 4581773312 901    761    zeus15 6870278144 1000    761    zeus15 6783991808 901    719    zeus10 7227342848 901    886    853393408 zeus20 901    885    zeus10 859234304 901    885    zeus17 948133888 901    886    zeus10 909783040
50_standard_copy1_true-unreach-call_ground.i 67.2  57.4  zeus23 1326354432 36.5  26.6  zeus19 808161280 901    886    zeus08 879837184 902    795    4771078144 zeus05 902    795    4735574016 zeus12 901    795    zeus18 4995092480 901    840    zeus07 4509745152 67.5  38.6  zeus05 1895497728 61.6  34.7  zeus13 2100092928 901    700    zeus22 7916109824 901    888    828813312 zeus08 901    888    zeus12 829644800 902    887    zeus05 920653824 902    892    zeus15 715808768
50_standard_copy2_true-unreach-call_ground.i 667    653    zeus14 5887250432 109    95.0  zeus04 1707663360 902    886    zeus02 1032671232 278    204    4708036608 zeus03 279    201    3766943744 zeus18 262    189    zeus10 3787067392 902    837    zeus05 4721446912 152    116    zeus07 4524363776 83.0  53.8  zeus24 3611500544 902    801    zeus04 7449714688 901    888    828620800 zeus08 902    888    zeus20 830226432 902    890    zeus02 769867776 902    890    zeus02 783630336
50_standard_copy3_true-unreach-call_ground.i 902    888    zeus09 7041613824 227    211    zeus18 3272257536 901    886    zeus15 905322496 425    329    4764643328 zeus04 354    274    4760465408 zeus21 295    221    zeus12 4519358464 902    760    zeus15 7427067904 428    382    zeus13 4634853376 152    115    zeus08 4432322560 902    833    zeus13 5359669248 902    889    853426176 zeus11 902    889    zeus10 859860992 902    888    zeus15 812023808 901    889    zeus13 789864448
50_standard_copy4_true-unreach-call_ground.i 902    886    zeus12 7013593088 403    388    zeus09 4455104512 902    888    zeus13 932610048 595    502    4839096320 zeus18 589    497    4840914944 zeus16 446    365    zeus01 4616224768 902    706    zeus19 9200447488 902    844    zeus16 4698722304 121    85.6  zeus23 4425969664 901    834    zeus04 5243138048 902    888    894701568 zeus16 901    887    zeus05 894124032 901    886    zeus15 842678272 902    892    zeus05 777236480
50_standard_copy5_true-unreach-call_ground.i 902    883    zeus09 4716453888 782    763    zeus06 7215300608 901    891    zeus20 872857600 795    698    4902604800 zeus14 779    676    4893159424 zeus23 535    451    zeus23 4794343424 901    664    zeus03 11407187968 902    846    zeus10 4647612416 134    100    zeus14 4474937344 902    827    zeus22 5234229248 901    887    1001402368 zeus08 902    885    zeus09 1007652864 901    886    zeus21 911888384 901    892    zeus07 777359360
50_standard_copy6_true-unreach-call_ground.i 902    882    zeus12 4740145152 902    882    zeus24 5674913792 902    892    zeus10 850296832 902    798    4959105024 zeus16 902    797    4998438912 zeus12 778    686    zeus19 4927004672 966    610    zeus18 11524612096 903    846    zeus03 4715855872 213    173    zeus13 4573851648 902    846    zeus05 5107335168 902    885    1042575360 zeus15 902    886    zeus22 1049255936 902    886    zeus21 936116224 901    892    zeus08 768847872
50_standard_copy7_true-unreach-call_ground.i 902    880    zeus20 2996027392 902    879    zeus12 4897341440 902    896    zeus08 1280471040 902    810    4660256768 zeus07 902    809    4729135104 zeus24 901    808    zeus20 4785524736 903    603    zeus06 12218601472 902    844    zeus14 4722954240 243    203    zeus09 4558274560 902    847    zeus10 4980723712 902    885    1073864704 zeus01 902    885    zeus18 1055932416 902    886    zeus13 965881856 902    893    zeus17 760143872
50_standard_copy8_true-unreach-call_ground.i 902    879    zeus01 2944143360 902    879    zeus02 2396393472 902    897    zeus18 1430704128 902    806    4755521536 zeus09 902    810    4676456448 zeus17 902    807    zeus12 4713918464 960    671    zeus15 13080363008 902    845    zeus19 4765765632 168    130    zeus21 4502155264 902    844    zeus04 5172162560 902    885    1099272192 zeus24 902    884    zeus08 1089626112 902    885    zeus22 968675328 902    894    zeus16 759681024
50_standard_copy9_true-unreach-call_ground.i 901    878    zeus16 2378051584 902    878    zeus03 2447740928 902    894    zeus08 868012032 902    806    4712222720 zeus10 902    808    4675006464 zeus06 902    810    zeus19 4669755392 902    696    zeus03 11453571072 902    845    zeus06 4814049280 616    567    zeus12 4681617408 901    846    zeus11 5118730240 902    885    1058226176 zeus17 902    882    zeus08 1065467904 902    886    zeus20 973971456 902    893    zeus24 766283776
50_standard_copyInitSum2_true-unreach-call_ground.i 445    431    zeus03 5154615296 902    884    zeus08 7353753600 902    885    zeus01 1039532032 901    784    4944396288 zeus03 902    784    4922286080 zeus02 307    229    zeus13 4042579968 901    841    zeus03 4590080000 107    73.2  zeus17 3246170112 102    67.8  zeus15 4310818816 902    802    zeus15 6423789568 902    889    834486272 zeus18 902    889    zeus22 831758336 902    889    zeus15 816087040 901    889    zeus12 797929472
50_standard_copyInitSum3_true-unreach-call_ground.i 912    895    zeus14 7131648000 902    884    zeus06 5968896000 902    885    zeus16 854290432 521    433    4775006208 zeus01 522    434    4779802624 zeus04 462    380    zeus07 4630175744 901    839    zeus18 4571852800 902    839    zeus12 4864573440 130    91.1  zeus17 4445851648 902    805    zeus18 5319069696 902    887    959430656 zeus16 901    886    zeus06 986488832 902    888    zeus02 858193920 901    889    zeus15 805494784
50_standard_copyInitSum_true-unreach-call_ground.i 411    397    zeus16 4994826240 283    265    zeus09 4313460736 902    885    zeus15 968527872 902    782    4941688832 zeus18 902    788    4933300224 zeus18 302    224    zeus01 4537184256 901    843    zeus08 4529352704 902    845    zeus13 4630994944 326    276    zeus15 4557189120 902    804    zeus03 6318678016 902    889    841428992 zeus11 901    886    zeus13 854278144 902    889    zeus09 824406016 901    889    zeus17 786513920
50_standard_copyInit_true-unreach-call_ground.i 149    137    zeus24 2519937024 104    88.3  zeus03 1702694912 901    885    zeus23 971063296 901    784    4955316224 zeus15 902    783    5000060928 zeus08 902    789    zeus18 5213458432 901    842    zeus24 4580749312 113    76.9  zeus08 3963572224 88.5  55.6  zeus19 4274364416 902    805    zeus19 7210676224 901    887    799899648 zeus04 901    887    zeus11 817389568 901    890    zeus05 766472192 901    889    zeus23 800608256
50_standard_find_true-unreach-call_ground.i 901    886    zeus15 2404167680 3.77 2.20 zeus21 215400448 901    885    zeus16 2450706432 901    825    4763774976 zeus04 901    825    4629639168 zeus18 901    821    zeus21 4748894208 901    823    zeus02 4640608256 902    825    zeus18 6230179840 902    788    zeus16 6370336768 901    826    zeus03 6440722432 901    888    871366656 zeus14 902    889    zeus04 833581056 901    887    zeus22 892960768 901    887    zeus08 873476096
50_standard_init1_true-unreach-call_ground.i 32.8  23.5  zeus12 805625856 34.6  25.1  zeus05 820142080 901    884    zeus02 929656832 902    791    5029621760 zeus23 902    795    5108666368 zeus15 902    801    zeus02 4864745472 901    767    zeus13 6596136960 58.5  33.6  zeus01 1930473472 59.0  33.8  zeus24 2100764672 902    766    zeus16 7907745792 901    888    796618752 zeus07 902    888    zeus09 811167744 902    886    zeus01 861937664 901    893    zeus22 706527232
50_standard_init2_true-unreach-call_ground.i 80.9  68.1  zeus18 1589776384 92.6  80.0  zeus16 1604947968 901    883    zeus09 941785088 901    794    4866080768 zeus03 901    795    4917923840 zeus03 902    798    zeus22 4787482624 829    689    zeus02 6983176192 84.2  52.9  zeus01 2412924928 72.7  47.1  zeus02 3416268800 902    752    zeus09 9271422976 902    887    770101248 zeus15 901    888    zeus20 768602112 902    887    zeus04 783597568 901    885    zeus01 780496896
50_standard_init3_true-unreach-call_ground.i 170    157    zeus07 2984968192 191    177    zeus06 3040505856 902    884    zeus06 970616832 902    792    4828909568 zeus12 902    794    4856631296 zeus15 902    796    zeus05 4859838464 902    800    zeus04 5251350528 104    73.8  zeus09 2828009472 90.8  61.9  zeus02 4351504384 963    761    zeus14 8462962688 901    887    763703296 zeus03 901    888    zeus10 768815104 902    889    zeus11 763187200 901    888    zeus03 793001984
50_standard_init4_true-unreach-call_ground.i 310    295    zeus12 3464691712 291    278    zeus12 3702370304 902    882    zeus23 911151104 902    789    4779933696 zeus23 902    797    4818685952 zeus12 901    795    zeus02 4794212352 902    811    zeus12 5307002880 110    80.0  zeus22 3716841472 120    87.6  zeus05 4426821632 902    739    zeus18 8102932480 902    888    770650112 zeus19 901    886    zeus21 784400384 901    886    zeus12 762433536 901    889    zeus02 794722304
50_standard_init5_true-unreach-call_ground.i 489    472    zeus22 4834607104 521    506    zeus15 4678643712 902    884    zeus03 819052544 902    791    4763226112 zeus09 902    792    4782780416 zeus09 902    796    zeus24 4773756928 902    811    zeus21 5307305984 137    103    zeus02 4464672768 139    106    zeus14 4460601344 1000    848    zeus12 7621603328 901    885    808861696 zeus21 901    886    zeus17 812531712 902    883    zeus06 810680320 901    888    zeus14 815775744
50_standard_init6_true-unreach-call_ground.i 751    733    zeus21 6870474752 700    683    zeus10 4677988352 902    880    zeus13 823627776 902    793    4691906560 zeus06 902    792    4769763328 zeus11 902    799    zeus12 4696588288 903    815    zeus06 5270970368 193    157    zeus03 4458188800 149    118    zeus09 4470337536 902    791    zeus04 7490293760 901    885    814804992 zeus03 901    885    zeus08 846471168 902    887    zeus15 820932608 902    889    zeus13 800268288
50_standard_init7_true-unreach-call_ground.i 902    880    zeus10 3210645504 902    882    zeus14 6705254400 903    882    zeus23 805928960 902    798    4636475392 zeus11 902    794    4657774592 zeus17 902    799    zeus03 4654198784 902    814    zeus15 5348151296 191    155    zeus19 4514443264 190    154    zeus20 4507103232 903    788    zeus16 7057874944 902    885    836386816 zeus10 901    885    zeus14 830042112 901    886    zeus10 812896256 901    888    zeus11 782454784
50_standard_init8_true-unreach-call_ground.i 902    879    zeus11 2431229952 904    880    zeus10 2771951616 902    882    zeus08 820764672 902    804    4606750720 zeus20 902    806    4592308224 zeus08 902    815    zeus17 4584701952 902    809    zeus06 5547323392 216    176    zeus12 4525252608 230    192    zeus23 4537483264 902    795    zeus13 6823796736 902    885    828862464 zeus03 902    884    zeus02 857145344 901    885    zeus02 821985280 902    888    zeus21 821747712
50_standard_init9_true-unreach-call_ground.i 902    878    zeus17 1340387328 902    880    zeus02 2411057152 901    881    zeus24 858198016 902    814    4607234048 zeus05 902    810    4587171840 zeus24 902    816    zeus16 4587102208 902    812    zeus18 5318758400 333    288    zeus10 4560588800 340    297    zeus10 4525748224 902    821    zeus06 4933435392 902    884    821096448 zeus19 902    884    zeus07 825749504 902    885    zeus16 825667584 902    887    zeus12 831492096
50_standard_maxInArray_true-unreach-call_ground.i 872    860    zeus17 14999998464 516    506    zeus12 14999998464 854    842    zeus24 14999998464 901    639    8790257664 zeus02 943    665    8802635776 zeus01 1000    695    zeus13 8895356928 916    650    zeus08 8706678784 922    652    zeus12 11424612352 903    641    zeus18 13014654976 909    699    zeus09 10279645184 901    885    827531264 zeus22 901    886    zeus04 833478656 901    886    zeus19 876208128 901    886    zeus19 853495808
50_standard_minInArray_true-unreach-call_ground.i 632    621    zeus15 14999998464 906    893    zeus17 14592212992 624    613    zeus04 14999998464 942    681    9122856960 zeus08 1000    699    8697733120 zeus14 1000    699    zeus21 8815538176 940    662    zeus13 8668315648 902    611    zeus10 11916259328 929    652    zeus14 12845129728 902    644    zeus18 13098610688 901    887    818728960 zeus01 901    886    zeus05 829161472 901    886    zeus08 866197504 901    886    zeus15 869920768
50_standard_palindrome_true-unreach-call_ground.i 11.7  7.61 zeus12 418512896 12.3  8.13 zeus03 474181632 445    431    zeus12 791785472 901    822    4703518720 zeus22 902    819    4732252160 zeus11 901    819    zeus02 4691103744 902    797    zeus09 5217861632 35.0  18.2  zeus05 737529856 34.8  18.0  zeus07 857526272 901    646    zeus16 8981192704 902    890    829530112 zeus18 901    889    zeus14 831393792 902    890    zeus01 865296384 902    892    zeus20 813895680
50_standard_partial_init_true-unreach-call_ground.i 902    889    zeus10 3451441152 906    894    zeus10 9011535872 901    889    zeus12 805126144 901    808    4821336064 zeus24 902    811    4787474432 zeus17 902    810    zeus10 5157093376 901    817    zeus05 5158023168 957    557    zeus02 8729329664 1000    569    zeus18 11465146368 901    851    zeus01 5509410816 902    891    820711424 zeus02 902    890    zeus22 832606208 903    891    zeus04 1882857472 901    891    zeus08 736641024
50_standard_partition_original_true-unreach-call_ground.i 905    893    zeus05 3959554048 908    896    zeus17 5845839872 902    888    zeus16 805613568 902    819    4603527168 zeus20 901    817    4615708672 zeus23 902    820    zeus03 4600696832 901    822    zeus19 4987412480 1000    643    zeus16 9097891840 901    551    zeus23 8504410112 902    861    zeus01 5091639296 901    887    814575616 zeus22 901    887    zeus14 808054784 901    886    zeus14 854388736 901    889    zeus04 777236480
50_standard_partition_true-unreach-call_ground.i 902    885    zeus08 2875494400 913    898    zeus02 1851269120 902    884    zeus05 1148235776 902    812    4703862784 zeus13 902    817    4643520512 zeus23 903    793    zeus10 5439524864 902    835    zeus05 4538580992 1000    719    zeus06 8909697024 1000    618    zeus21 9527816192 902    844    zeus15 6032650240 901    887    968937472 zeus18 902    889    zeus19 985194496 902    889    zeus24 1336934400 902    885    zeus17 831500288
50_standard_password_true-unreach-call_ground.i 901    885    zeus07 1310011392 901    886    zeus22 1305038848 902    887    zeus08 1365000192 902    803    4573118464 zeus24 901    809    4580016128 zeus09 902    802    zeus13 4574715904 902    814    zeus19 4550516736 902    777    zeus10 7674245120 903    629    zeus20 7067746304 902    720    zeus19 7405674496 901    886    853532672 zeus14 901    887    zeus17 847421440 901    885    zeus12 949805056 901    885    zeus13 928636928
50_standard_reverse_true-unreach-call_ground.i 29.6  20.2  zeus03 756441088 28.3  19.4  zeus16 741060608 902    885    zeus18 833912832 902    802    4609748992 zeus02 901    804    4583776256 zeus16 901    813    zeus12 4608921600 901    842    zeus14 4580839424 68.2  40.5  zeus03 1466109952 72.1  39.6  zeus07 1518821376 902    843    zeus02 5523034112 901    893    713388032 zeus07 901    893    zeus23 707817472 901    889    zeus17 760315904 902    892    zeus04 718917632
50_standard_running_true-unreach-call.i 903    883    zeus03 3160190976 903    883    zeus13 2039287808 901    880    zeus14 959098880 902    812    4766298112 zeus24 901    810    4713504768 zeus06 902    814    zeus12 4645019648 901    843    zeus20 4547805184 902    844    zeus09 4757491712 902    848    zeus13 4941443072 901    838    zeus05 4847869952 902    887    1370247168 zeus13 902    888    zeus16 1377021952 901    887    zeus11 1820192768 901    886    zeus13 880766976
50_standard_sentinel_true-unreach-call.i 4.10 2.45 zeus19 219598848 4.13 2.45 zeus09 215961600 4.57 2.79 zeus07 223125504 901    822    4864417792 zeus12 901    821    5002727424 zeus21 901    822    zeus14 4822552576 901    821    zeus10 4718768128 4.55 2.67 zeus16 222572544 4.42 2.70 zeus19 219701248 930    753    zeus19 6855036928 4.32 2.56 211714048 zeus05 4.27 2.51 zeus15 210956288 4.23 2.54 zeus04 210903040 4.40 2.69 zeus12 219541504
50_standard_seq_init_true-unreach-call_ground.i 102    90.8  zeus06 1251237888 94.1  83.5  zeus15 1133957120 67.7  55.7  zeus18 912994304 227    158    3533041664 zeus22 220    153    3611676672 zeus24 211    148    zeus21 3353923584 444    361    zeus14 5295476736 66.3  37.1  zeus15 2301493248 64.9  36.9  zeus23 1471725568 77.7  47.2  zeus06 2176118784 54.1  45.4  817504256 zeus20 51.5  43.3  zeus22 794488832 47.3  39.3  zeus03 792059904 282    273    zeus19 795574272
50_standard_strcmp_true-unreach-call_ground.i 905    898    zeus23 4919922688 45.1  33.1  zeus01 841895936 43.5  30.6  zeus11 871550976 902    802    4524920832 zeus01 901    806    4533616640 zeus24 209    144    zeus02 3296673792 902    758    zeus04 7202459648 60.5  37.5  zeus15 2845462528 61.5  35.5  zeus06 2030727168 64.0  37.4  zeus01 1520664576 901    887    1007628288 zeus12 902    886    zeus24 1011257344 74.9  63.1  zeus21 799436800 151    135    zeus08 849711104
50_standard_strcpy_original_true-unreach-call.i 902    892    zeus14 733052928 902    893    zeus10 715210752 902    891    zeus18 740032512 901    829    4802441216 zeus02 901    824    4737871872 zeus22 902    825    zeus02 4939288576 901    836    zeus20 4550529024 4.28 2.56 zeus11 220712960 901    827    zeus07 6445981696 902    786    zeus02 7607521280 901    892    826552320 zeus06 902    893    zeus03 825262080 902    892    zeus20 823398400 902    891    zeus23 869027840
50_standard_strcpy_true-unreach-call_ground.i 4.31 2.54 zeus18 210989056 3.87 2.32 zeus13 217985024 901    887    zeus06 803557376 902    822    4749381632 zeus02 901    821    4748136448 zeus13 901    826    zeus05 4629741568 902    831    zeus08 4597862400 4.28 2.54 zeus19 218873856 902    839    zeus16 5742649344 902    833    zeus04 6854381568 901    888    819261440 zeus20 901    889    zeus07 825139200 902    888    zeus22 976211968 902    891    zeus12 881782784
50_standard_two_index_01_true-unreach-call.i 55.9  46.9  zeus15 1322655744 45.7  36.4  zeus08 1030471680 902    888    zeus12 859115520 902    807    4773933056 zeus17 902    809    4733915136 zeus08 901    786    zeus12 5094453248 901    841    zeus24 4547891200 62.4  35.5  zeus08 1714348032 67.7  38.8  zeus22 2433236992 911    817    zeus05 7156256768 901    888    856055808 zeus17 901    888    zeus03 835432448 902    888    zeus21 786571264 901    892    zeus24 701214720
50_standard_two_index_02_true-unreach-call.i 12.5  8.21 zeus02 436064256 13.7  8.53 zeus02 453267456 901    889    zeus11 803704832 902    812    4687187968 zeus20 902    821    4639780864 zeus05 902    812    zeus11 4749627392 901    839    zeus23 4575281152 34.0  17.5  zeus20 861442048 32.8  17.0  zeus21 887189504 901    799    zeus21 7465267200 901    890    824672256 zeus18 901    889    zeus10 807411712 901    889    zeus22 837521408 901    891    zeus20 758296576
50_standard_two_index_03_true-unreach-call.i 9.12 5.25 zeus06 308994048 9.70 5.61 zeus18 328560640 901    890    zeus10 787406848 901    820    4673146880 zeus17 901    824    4666753024 zeus01 902    820    zeus15 4735078400 902    840    zeus06 4572336128 19.1  10.2  zeus10 663056384 16.8  9.07 zeus13 532668416 408    355    zeus11 5830725632 901    892    824451072 zeus20 902    891    zeus24 819249152 902    891    zeus20 799940608 901    891    zeus10 819273728
50_standard_two_index_04_true-unreach-call.i 7.35 4.22 zeus01 270454784 8.54 4.89 zeus13 300756992 421    412    zeus03 759173120 902    829    4673884160 zeus19 901    833    4589809664 zeus07 323    265    zeus17 4057182208 901    835    zeus16 4581531648 13.7  7.46 zeus19 534712320 11.8  6.47 zeus10 427528192 72.5  42.4  zeus12 2752073728 902    892    785530880 zeus03 902    891    zeus15 778543104 901    891    zeus21 795414528 902    892    zeus03 847843328
50_standard_two_index_05_true-unreach-call.i 5.90 3.41 zeus16 244088832 6.70 3.87 zeus20 255029248 96.9  91.1  zeus03 594620416 901    826    4625506304 zeus01 902    830    4607950848 zeus11 128    77.6  zeus18 1828691968 901    824    zeus08 4613206016 8.58 4.77 zeus24 328105984 8.94 4.98 zeus06 307941376 53.2  27.3  zeus08 938323968 902    892    781082624 zeus22 902    892    zeus06 782282752 275    268    zeus23 679878656 165    158    zeus11 693067776
50_standard_two_index_06_true-unreach-call.i 5.11 2.99 zeus10 237203456 6.47 3.72 zeus07 250974208 63.3  57.3  zeus18 494899200 902    826    4646830080 zeus21 901    831    4657790976 zeus24 97.1  52.3  zeus22 1364656128 902    828    zeus02 4617863168 7.64 4.29 zeus20 279564288 7.77 4.47 zeus03 272629760 50.9  26.1  zeus03 1120587776 485    477    747724800 zeus14 406    399    zeus05 743727104 94.5  88.3  zeus22 661553152 102    95.3  zeus03 611291136
50_standard_two_index_07_true-unreach-call.i 4.94 2.89 zeus08 233680896 5.53 3.21 zeus05 237248512 35.8  30.3  zeus21 408424448 483    422    4572667904 zeus05 503    438    4542910464 zeus16 72.7  37.5  zeus09 1130893312 901    827    zeus23 4582719488 7.00 4.07 zeus12 260304896 5.67 3.27 zeus12 240205824 36.7  18.9  zeus01 896311296 85.8  80.5  616419328 zeus16 92.4  87.2  zeus07 615206912 24.5  20.3  zeus21 393846784 39.1  34.2  zeus08 382177280
50_standard_two_index_08_true-unreach-call.i 5.38 3.14 zeus12 229216256 5.74 3.34 zeus07 242319360 30.3  25.4  zeus23 361930752 495    434    4492840960 zeus18 465    409    4561858560 zeus04 68.5  35.3  zeus24 1096101888 901    826    zeus14 4574400512 5.96 3.46 zeus10 245788672 5.77 3.35 zeus03 242315264 37.4  19.3  zeus09 881348608 86.4  81.2  614862848 zeus01 84.7  79.6  zeus07 624119808 24.9  20.5  zeus12 394412032 41.1  35.9  zeus12 381235200
50_standard_two_index_09_true-unreach-call.i 4.52 2.70 zeus15 220794880 5.78 3.40 zeus02 237449216 24.2  19.1  zeus17 351789056 162    111    2336182272 zeus07 167    115    2544640000 zeus01 58.9  30.3  zeus03 965410816 901    829    zeus22 4537630720 5.87 3.41 zeus07 238084096 5.17 3.04 zeus24 231817216 29.2  15.3  zeus03 879775744 42.5  38.2  427491328 zeus14 41.6  37.5  zeus03 417935360 14.3  10.7  zeus19 332554240 26.3  21.7  zeus10 334557184
50_standard_vararg_true-unreach-call_ground.i 901    887    zeus05 2291314688 3.83 2.30 zeus15 213135360 901    886    zeus01 4225630208 902    828    4686827520 zeus13 901    827    4693610496 zeus08 901    832    zeus14 4546383872 902    825    zeus13 4603068416 902    793    zeus12 7497900032 902    800    zeus14 7636049920 902    796    zeus16 8721367040 901    888    857288704 zeus24 902    887    zeus14 877232128 902    889    zeus13 889913344 901    888    zeus02 876339200
50_standard_vector_difference_true-unreach-call_ground.i 109    98.3  zeus12 1918787584 36.8  27.6  zeus17 818405376 901    887    zeus13 895860736 901    795    4936200192 zeus22 901    787    4841046016 zeus04 901    812    zeus19 4651909120 901    826    zeus23 4972208128 71.5  41.9  zeus19 2271436800 63.3  35.7  zeus12 2365095936 902    832    zeus05 5130874880 901    889    959627264 zeus10 901    885    zeus06 905736192 901    885    zeus14 861892608 901    890    zeus18 787828736
test/programs/array-simplified-benchmarks/arrays-size-50/ 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) 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) 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 46300 45100   330700943360 88 40000   38900    287291281408 88 60600 59300   158088732672 88 66300 61900 437264928768 88 66200 61900 436050034688 88 60500 55100 426724134912 88 74100   63400    542089355264 88 36300   30800    346602586112 88 26500 20700 376394600448 88 54600 47900 460980264960 88 60500   59300   78438113280 88 60400   59200   78203502592 88 56400 55200 77423923200 88 66700 65700 69475368960
    correct results 13 2380 2220   23151992832 18 3850   3610    38169542656 22 4400 4150   16053428224 10 2500 1930 32377532416 10 2440 1910 33818189824 15 3450 2590 45617033216 7 2020   1600    26500722688 23 5030   4180    71730024448 27 3900 2970 95955394560 30 6040 4940 100948725760 25 6080   5760   22572777472 25 5830   5520   22501785600 29 7080 6720 22570917888 17 4970 4790 10927587328
        correct true 3 234 227   1068191744 3 15.0 8.69 688873472 11 1160 1100   4818616320 5 1160 977 12147204096 5 1150 972 12376621056 8 764 507 11144216576 2 16.4 9.11 691544064 3 12.8 7.57 657960960 4 253 200 5128613888 10 1090 845 18262904832 7 712   684   3036209152 7 637   610   3036086272 9 876 828 3896893440 9 983 930 3867181056
        correct false 10 2150 2000   22083801088 15 3840   3610    37480669184 11 3240 3050   11234811904 5 1340 953 20230328320 5 1290 936 21441568768 7 2680 2090 34472816640 5 2010   1590    25809178624 20 5020   4170    71072063488 23 3650 2770 90826780672 20 4950 4100 82685820928 18 5370   5080   19536568320 18 5190   4910   19465699328 20 6200 5890 18674024448 8 3990 3860 7060406272
    incorrect results 1 102 90.8 1251237888 2 139   117    1975853056 2 111 86.2 1784545280 1 227 158 3533041664 1 220 153 3611676672 3 939 726 11297107968 1 444   361    5295476736 1 66.3 37.1  2301493248 3 275 174 7970983936 3 333 226 8220864512 1 54.1 45.4 817504256 1 51.5 43.3 794488832 2 122 102 1591496704 2 433 408 1645285376
        incorrect true 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 1 102 90.8 1251237888 2 139   117    1975853056 2 111 86.2 1784545280 1 227 158 3533041664 1 220 153 3611676672 3 939 726 11297107968 1 444   361    5295476736 1 66.3 37.1  2301493248 3 275 174 7970983936 3 333 226 8220864512 1 54.1 45.4 817504256 1 51.5 43.3 794488832 2 122 102 1591496704 2 433 408 1645285376
score (88 tasks, max score: 148) 0 -11 1 -1 -1 -25 -7 10 -17 -8 16 16 6 -6
Run set MathSAT5-heaparray.ArraysReach50 MathSAT5-oldarray.ArraysReach50 MathSAT5-uf.ArraysReach50 PRINCESS-heaparray-quantifiers.ArraysReach50 PRINCESS-heaparray.ArraysReach50 PRINCESS-oldarray.ArraysReach50 PRINCESS-uf.ArraysReach50 SMTInterpol-heaparray.ArraysReach50 SMTInterpol-oldarray.ArraysReach50 SMTInterpol-uf.ArraysReach50 Z3-heaparray-quantifiers.ArraysReach50 Z3-heaparray.ArraysReach50 Z3-oldarray.ArraysReach50 Z3-uf.ArraysReach50