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 MathSAT5-oldarray MathSAT5-uf PRINCESS-heaparray-quantifiers PRINCESS-heaparray PRINCESS-oldarray PRINCESS-uf SMTInterpol-heaparray SMTInterpol-oldarray SMTInterpol-uf Z3-heaparray-quantifiers Z3-heaparray Z3-oldarray Z3-uf
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/ status cputime (s) walltime (s) memUsage host 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) memUsage host 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
benchmarks/array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i 543    538    14999998464 zeus03 902    883    zeus24 2363203584 3.58 2.13 207601664 zeus20 902    863    4938846208 zeus19 901    859    zeus20 4749336576 901    819    zeus21 4560994304 4.92 2.93 zeus01 291037184 912    891    4768194560 zeus23 902    856    zeus17 4701954048 3.76 2.26 zeus13 209952768 9.20 6.00 787546112 zeus19 8.63 5.59 zeus06 784465920 901    885    zeus21 796811264 3.85 2.28 zeus15 204636160
benchmarks/array-examples/sorting_bubblesort_false-unreach-call2_ground.i 901    882    2538803200 zeus03 901    883    zeus10 1355788288 3.78 2.22 206458880 zeus02 901    820    4834357248 zeus07 902    820    zeus10 4810702848 902    825    zeus15 4869525504 5.00 2.94 zeus09 293703680 902    847    4803031040 zeus16 901    857    zeus01 4885319680 3.75 2.22 zeus20 201650176 7.11 4.43 571928576 zeus14 7.27 4.45 zeus16 571891712 901    885    zeus19 836485120 3.75 2.24 zeus08 202244096
benchmarks/array-examples/sorting_bubblesort_false-unreach-call_ground.i 902    881    1639313408 zeus06 901    882    zeus09 1385177088 3.46 2.09 201633792 zeus19 902    822    4852011008 zeus09 901    822    zeus18 4832972800 902    823    zeus07 4839530496 4.84 2.85 zeus04 292495360 901    849    4808658944 zeus01 901    854    zeus12 4838445056 4.03 2.40 zeus13 209330176 7.29 4.58 560488448 zeus15 7.27 4.51 zeus20 563986432 902    886    zeus14 842137600 3.89 2.27 zeus10 205697024
benchmarks/array-examples/sorting_selectionsort_false-unreach-call2_ground.i 902    881    1658474496 zeus21 901    883    zeus20 1560948736 3.77 2.23 204582912 zeus12 902    819    4585041920 zeus19 901    817    zeus19 4601556992 901    817    zeus18 4595290112 5.09 2.94 zeus20 298078208 901    855    4686524416 zeus12 901    855    zeus03 4916973568 3.89 2.32 zeus12 211922944 6.80 4.22 556810240 zeus21 7.53 4.72 zeus11 573534208 902    884    zeus06 828653568 3.81 2.25 zeus17 201199616
benchmarks/array-examples/sorting_selectionsort_false-unreach-call_ground.i 902    882    1412030464 zeus10 902    883    zeus04 1344020480 3.65 2.16 205053952 zeus21 902    816    4596994048 zeus16 902    819    zeus21 4594823168 901    817    zeus08 4572852224 5.57 3.23 zeus16 296329216 902    849    4735946752 zeus12 902    857    zeus22 4741406720 3.85 2.29 zeus08 210747392 6.97 4.36 560439296 zeus22 7.19 4.55 zeus09 565448704 902    883    zeus20 809959424 3.80 2.28 zeus14 202772480
benchmarks/array-examples/standard_allDiff2_false-unreach-call_ground.i 902    877    1399738368 zeus09 902    881    zeus17 2844401664 3.54 2.11 204283904 zeus09 901    819    4589244416 zeus03 902    818    zeus13 4605739008 901    820    zeus06 4582113280 4.57 2.67 zeus08 291389440 902    852    4680814592 zeus08 902    858    zeus11 4656582656 4.03 2.36 zeus19 210284544 6.94 4.32 561168384 zeus10 7.23 4.47 zeus13 561090560 902    880    zeus02 1086390272 3.69 2.19 zeus18 203337728
benchmarks/array-examples/standard_copy1_false-unreach-call_ground.i 902    879    4745707520 zeus05 902    882    zeus22 4513742848 3.83 2.24 205619200 zeus05 902    811    4600160256 zeus24 902    815    zeus03 4625092608 902    815    zeus10 4602466304 4.72 2.81 zeus11 298823680 902    845    4821860352 zeus09 902    858    zeus14 4757823488 3.96 2.35 zeus06 208543744 8.18 5.10 709529600 zeus17 7.45 4.71 zeus16 659750912 901    885    zeus22 833343488 3.69 2.21 zeus05 205488128
benchmarks/array-examples/standard_copy2_false-unreach-call_ground.i 902    880    4617334784 zeus22 901    882    zeus10 4426731520 3.69 2.18 203235328 zeus20 902    815    4958580736 zeus22 902    819    zeus23 4936802304 902    821    zeus05 4923932672 4.98 2.95 zeus23 300683264 902    846    4811321344 zeus18 901    838    zeus21 5002915840 3.77 2.27 zeus03 208281600 8.60 5.45 798121984 zeus22 8.44 5.41 zeus10 790970368 902    885    zeus05 832229376 3.52 2.10 zeus03 205418496
benchmarks/array-examples/standard_copy3_false-unreach-call_ground.i 902    879    4648157184 zeus21 902    877    zeus02 2381791232 3.77 2.25 208523264 zeus17 902    817    4951605248 zeus13 902    813    zeus24 4946333696 901    820    zeus15 4928180224 5.04 2.99 zeus10 299896832 902    843    4844421120 zeus17 901    859    zeus07 4909559808 3.89 2.31 zeus19 205488128 8.97 5.78 809709568 zeus21 8.92 5.72 zeus05 814964736 902    885    zeus17 838426624 3.85 2.34 zeus20 204849152
benchmarks/array-examples/standard_copy4_false-unreach-call_ground.i 902    878    4619153408 zeus24 902    879    zeus01 2791895040 3.68 2.22 202792960 zeus08 902    814    4938014720 zeus13 902    815    zeus10 4947845120 902    819    zeus15 4918730752 4.88 2.91 zeus13 302297088 902    849    4663984128 zeus16 902    855    zeus18 4729753600 3.64 2.17 zeus22 205938688 8.85 5.75 818085888 zeus21 9.33 5.94 zeus21 816971776 902    884    zeus14 823083008 3.69 2.19 zeus23 208232448
benchmarks/array-examples/standard_copy5_false-unreach-call_ground.i 901    875    4638576640 zeus09 902    881    zeus09 4373934080 3.89 2.40 210407424 zeus11 902    813    4894388224 zeus04 903    813    zeus08 4949487616 902    820    zeus21 4958789632 4.91 2.90 zeus14 301846528 902    842    4797243392 zeus04 901    858    zeus15 4821159936 3.79 2.26 zeus14 205676544 9.81 6.57 865992704 zeus16 11.1  7.43 zeus03 869601280 902    885    zeus19 821669888 3.79 2.20 zeus09 202809344
benchmarks/array-examples/standard_copy6_false-unreach-call_ground.i 902    877    4617756672 zeus07 902    879    zeus03 2410983424 3.62 2.17 203784192 zeus01 902    814    4937912320 zeus13 902    817    zeus17 4997193728 902    817    zeus05 4927434752 5.07 2.99 zeus04 301924352 901    844    4823740416 zeus06 901    859    zeus07 4913184768 3.93 2.32 zeus15 206311424 10.1  6.86 864194560 zeus20 9.64 6.60 zeus17 873291776 902    885    zeus12 812920832 3.96 2.33 zeus15 201678848
benchmarks/array-examples/standard_copy7_false-unreach-call_ground.i 902    876    4704833536 zeus16 901    879    zeus05 2751000576 3.60 2.15 203489280 zeus03 902    810    5012267008 zeus03 902    812    zeus17 4975362048 902    817    zeus18 4966342656 5.19 3.06 zeus23 295460864 901    845    4843831296 zeus11 902    859    zeus01 4893061120 3.86 2.28 zeus08 200712192 12.0  7.94 961146880 zeus12 12.4  8.17 zeus14 955088896 901    884    zeus17 836063232 3.63 2.18 zeus12 206241792
benchmarks/array-examples/standard_copy8_false-unreach-call_ground.i 902    875    4736950272 zeus02 901    880    zeus08 2418327552 3.53 2.16 208965632 zeus12 901    813    4984840192 zeus13 901    815    zeus12 4912644096 901    818    zeus04 4957962240 4.98 2.94 zeus12 301465600 901    847    4832014336 zeus02 902    860    zeus18 4905865216 3.71 2.25 zeus09 212119552 12.2  8.20 961507328 zeus04 13.0  8.55 zeus05 960278528 901    885    zeus04 828682240 3.75 2.22 zeus19 208605184
benchmarks/array-examples/standard_copy9_false-unreach-call_ground.i 901    873    4732178432 zeus14 901    880    zeus18 2413539328 3.57 2.13 202018816 zeus20 902    811    4979077120 zeus02 901    813    zeus24 4956721152 901    818    zeus15 4917477376 4.97 2.96 zeus19 298897408 902    843    4858376192 zeus23 902    853    zeus09 4788477952 3.77 2.28 zeus04 208613376 14.2  9.59 985616384 zeus23 13.2  8.82 zeus10 981471232 902    884    zeus07 837148672 4.00 2.33 zeus24 202285056
benchmarks/array-examples/standard_copyInitSum2_false-unreach-call_ground.i 902    880    4535291904 zeus18 902    881    zeus14 4499972096 3.95 2.37 204439552 zeus07 902    815    4963160064 zeus22 902    813    zeus08 4960555008 901    816    zeus15 4972068864 4.84 2.87 zeus14 301768704 902    837    4942368768 zeus21 902    848    zeus15 4815888384 3.89 2.29 zeus07 211492864 7.62 4.84 709312512 zeus08 8.41 5.17 zeus03 724430848 901    885    zeus15 821190656 3.47 2.10 zeus11 206647296
benchmarks/array-examples/standard_init1_false-unreach-call_ground.i 901    880    4657348608 zeus08 902    882    zeus06 4636327936 3.56 2.11 206692352 zeus09 901    818    4594675712 zeus17 901    817    zeus08 4603846656 902    816    zeus10 4614164480 4.75 2.82 zeus18 293707776 902    848    4795379712 zeus16 902    844    zeus17 4831977472 3.71 2.21 zeus06 206651392 7.71 4.81 565506048 zeus22 7.11 4.49 zeus24 558235648 902    885    zeus12 834879488 3.79 2.20 zeus19 204312576
benchmarks/array-examples/standard_init2_false-unreach-call_ground.i 902    877    2441314304 zeus23 902    882    zeus10 4415565824 3.53 2.11 202076160 zeus24 902    815    4965031936 zeus14 902    818    zeus12 4937560064 901    816    zeus11 4954570752 4.78 2.83 zeus10 305926144 901    851    4823920640 zeus23 902    849    zeus24 4844077056 3.86 2.33 zeus12 204304384 7.71 4.70 563167232 zeus11 7.18 4.50 zeus13 565407744 901    885    zeus09 837083136 3.71 2.18 zeus15 196902912
benchmarks/array-examples/standard_init3_false-unreach-call_ground.i 902    878    2468352000 zeus21 902    880    zeus04 2780364800 3.91 2.32 205348864 zeus16 901    812    4919894016 zeus11 902    817    zeus01 4968505344 901    821    zeus02 4985745408 4.78 2.82 zeus13 299651072 902    851    4806672384 zeus14 902    852    zeus03 4800925696 3.87 2.27 zeus06 206934016 7.46 4.65 556707840 zeus18 7.04 4.41 zeus20 564199424 902    886    zeus08 827293696 3.63 2.16 zeus02 204828672
benchmarks/array-examples/standard_init4_false-unreach-call_ground.i 901    878    2807603200 zeus23 902    879    zeus05 2775281664 3.93 2.34 208371712 zeus07 901    816    4971270144 zeus07 902    812    zeus15 4907425792 902    817    zeus03 4974227456 5.00 2.98 zeus14 304017408 901    851    4780122112 zeus15 902    851    zeus07 4795850752 3.89 2.30 zeus17 207396864 7.14 4.48 558428160 zeus19 6.99 4.31 zeus03 568688640 902    885    zeus21 827269120 3.88 2.31 zeus20 202887168
benchmarks/array-examples/standard_init5_false-unreach-call_ground.i 901    879    2476064768 zeus18 902    880    zeus13 2408513536 3.63 2.17 203214848 zeus22 902    809    4958916608 zeus12 902    813    zeus01 4985835520 902    815    zeus16 4910608384 4.81 2.89 zeus10 303673344 901    848    4881551360 zeus07 901    855    zeus03 4936368128 3.97 2.38 zeus15 202452992 7.39 4.66 554610688 zeus20 7.22 4.59 zeus24 556343296 902    884    zeus01 834166784 3.63 2.12 zeus20 208150528
benchmarks/array-examples/standard_init6_false-unreach-call_ground.i 901    877    2799411200 zeus24 902    878    zeus06 2390577152 3.85 2.25 203546624 zeus05 902    818    4966973440 zeus14 902    820    zeus05 4957048832 902    818    zeus07 4929527808 5.53 3.22 zeus08 303218688 901    849    4779081728 zeus14 901    858    zeus15 4824559616 3.73 2.20 zeus09 206925824 8.51 5.18 565874688 zeus12 6.89 4.35 zeus19 558149632 902    884    zeus10 814776320 3.78 2.21 zeus13 210808832
benchmarks/array-examples/standard_init7_false-unreach-call_ground.i 902    877    1672876032 zeus01 902    880    zeus04 2417115136 4.24 2.52 207294464 zeus01 902    820    4969971712 zeus22 902    817    zeus11 4939816960 901    817    zeus15 4975943680 5.13 3.02 zeus06 292552704 902    850    4819415040 zeus07 902    856    zeus06 4907233280 3.76 2.23 zeus24 211181568 7.33 4.59 556273664 zeus14 7.47 4.74 zeus11 559378432 902    885    zeus11 833724416 3.65 2.17 zeus15 199630848
benchmarks/array-examples/standard_init8_false-unreach-call_ground.i 901    879    2469064704 zeus11 902    880    zeus15 1343467520 3.77 2.19 206741504 zeus16 901    818    4966756352 zeus05 902    818    zeus16 4960956416 902    820    zeus12 4930441216 4.79 2.84 zeus18 297099264 901    851    4829196288 zeus07 902    857    zeus11 4961660928 3.77 2.27 zeus15 207310848 7.28 4.51 564322304 zeus22 6.96 4.36 zeus15 556421120 902    885    zeus16 818139136 3.82 2.24 zeus15 204050432
benchmarks/array-examples/standard_init9_false-unreach-call_ground.i 902    878    1669832704 zeus24 901    879    zeus21 2680045568 3.68 2.22 209264640 zeus14 902    818    4967288832 zeus07 902    816    zeus17 4969644032 901    815    zeus20 5012250624 5.06 2.96 zeus05 298868736 901    854    4740202496 zeus22 902    856    zeus01 4845604864 4.22 2.52 zeus03 208429056 7.61 4.72 557694976 zeus01 7.26 4.55 zeus16 559620096 902    884    zeus05 825606144 3.84 2.25 zeus05 202805248
benchmarks/array-examples/standard_minInArray_false-unreach-call_ground.i 902    882    1422102528 zeus11 901    883    zeus12 2479554560 3.70 2.23 206520320 zeus04 902    814    4621164544 zeus11 902    815    zeus17 4598173696 902    818    zeus14 4580487168 5.15 3.02 zeus01 297025536 902    852    4813844480 zeus20 901    854    zeus16 4811481088 4.02 2.39 zeus02 206585856 7.65 4.79 561942528 zeus05 7.04 4.40 zeus07 560226304 902    884    zeus02 839815168 3.79 2.24 zeus07 206970880
benchmarks/array-examples/standard_partition_false-unreach-call_ground.i 901    879    4547870720 zeus07 902    875    zeus17 839815168 3.60 2.15 202960896 zeus01 902    813    4854476800 zeus14 901    815    zeus18 4877189120 902    822    zeus12 4877512704 4.56 2.70 zeus21 296452096 902    847    4828065792 zeus09 902    857    zeus03 4820611072 4.00 2.37 zeus03 203882496 8.58 5.46 791597056 zeus19 8.35 5.36 zeus20 785580032 901    885    zeus10 841146368 3.65 2.15 zeus21 203767808
benchmarks/array-examples/standard_running_false-unreach-call.i 901    876    1593540608 zeus08 902    879    zeus17 1385340928 3.69 2.21 205217792 zeus01 902    813    4928782336 zeus03 902    815    zeus09 4890992640 901    818    zeus21 4878417920 4.71 2.81 zeus03 296366080 902    847    4810108928 zeus16 901    851    zeus08 4891897856 3.98 2.35 zeus05 212353024 8.14 5.14 709177344 zeus01 8.34 5.17 zeus17 716435456 902    884    zeus19 825643008 3.67 2.19 zeus22 200835072
benchmarks/array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i 547    540    14999998464 zeus17 7.57 4.30 zeus21 283222016 3.59 2.16 210026496 zeus19 902    868    4660170752 zeus04 901    862    zeus19 4702658560 902    817    zeus23 4572028928 5.43 3.13 zeus01 293158912 912    888    4627681280 zeus15 902    858    zeus24 4595245056 3.84 2.30 zeus16 207990784 9.58 6.41 787750912 zeus11 9.51 6.13 zeus19 798318592 902    882    zeus05 807014400 3.55 2.07 zeus21 200695808
benchmarks/array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 552    546    14999998464 zeus22 902    881    zeus23 2397298688 3.91 2.30 212680704 zeus23 901    854    5033975808 zeus05 902    863    zeus21 4630437888 902    810    zeus20 4583944192 4.80 2.83 zeus16 290045952 913    888    4915191808 zeus08 902    858    zeus05 4639989760 3.98 2.38 zeus10 208695296 9.27 5.95 792633344 zeus18 8.60 5.47 zeus03 789266432 902    884    zeus13 817504256 3.80 2.25 zeus04 207290368
benchmarks/array-examples/relax_true-unreach-call.i 4.72 2.71 224231424 zeus23 4.46 2.62 zeus18 219185152 4.52 2.62 215150592 zeus03 5.57 3.22 309825536 zeus17 6.27 3.56 zeus06 307093504 10.0  5.50 zeus10 417382400 5.49 3.21 zeus11 314957824 4.33 2.55 218853376 zeus24 4.85 2.82 zeus12 231493632 4.61 2.67 zeus03 222965760 4.91 2.82 217182208 zeus01 4.35 2.51 zeus22 214659072 4.85 2.85 zeus08 219762688 4.39 2.55 zeus13 215023616
benchmarks/array-examples/sanfoundry_02_true-unreach-call_ground.i 901    881    1418477568 zeus09 901    883    zeus05 1579724800 3.91 2.29 205869056 zeus03 901    812    4592431104 zeus01 901    817    zeus01 4599148544 902    815    zeus24 4599762944 4.99 2.91 zeus15 295436288 902    850    4835627008 zeus23 902    860    zeus06 4899536896 4.41 2.59 zeus06 207962112 7.13 4.43 561569792 zeus12 7.43 4.50 zeus18 565170176 901    887    zeus03 825290752 3.81 2.26 zeus07 203370496
benchmarks/array-examples/sanfoundry_10_true-unreach-call_ground.i 901    880    4594393088 zeus03 901    881    zeus24 4606017536 901    878    2185170944 zeus11 902    814    4857323520 zeus15 901    820    zeus22 4909494272 901    820    zeus12 4887625728 902    820    zeus11 4844699648 902    845    4918423552 zeus01 902    856    zeus10 4977152000 901    847    zeus07 4922036224 902    884    940199936 zeus19 902    884    zeus20 953683968 902    884    zeus09 927465472 901    886    zeus03 813453312
benchmarks/array-examples/sanfoundry_24_true-unreach-call.i 5.77 3.47 352309248 zeus22 3.80 2.24 zeus02 207634432 3.52 2.11 204652544 zeus24 14.2  7.81 468058112 zeus17 13.7  7.44 zeus19 454545408 10.9  6.09 zeus01 401858560 5.21 3.06 zeus15 297406464 6.53 3.72 355594240 zeus11 4.14 2.49 zeus10 216125440 3.91 2.34 zeus02 210726912 5.90 3.56 444342272 zeus07 6.05 3.64 zeus16 439009280 3.66 2.20 zeus12 207474688 3.46 2.10 zeus14 204795904
benchmarks/array-examples/sanfoundry_27_true-unreach-call_ground.i 902    882    1430261760 zeus02 901    884    zeus11 2470330368 3.79 2.26 206512128 zeus13 902    813    4589481984 zeus07 901    819    zeus07 4581924864 901    817    zeus03 4584390656 5.10 3.01 zeus22 300273664 902    852    4732436480 zeus15 902    855    zeus10 4887990272 4.21 2.57 zeus11 212152320 7.08 4.40 567230464 zeus23 7.73 4.88 zeus23 560463872 901    886    zeus08 840437760 3.73 2.20 zeus23 204529664
benchmarks/array-examples/sanfoundry_43_true-unreach-call_ground.i 12.2  7.86 827146240 zeus21 3.83 2.28 zeus03 209448960 3.54 2.09 203186176 zeus17 13.9  7.61 789729280 zeus04 11.8  6.77 zeus04 773083136 6.03 3.57 zeus12 326078464 5.30 3.08 zeus16 295366656 842    826    4346318848 zeus11 3.70 2.18 zeus21 213680128 3.89 2.31 zeus13 208080896 11.9  7.58 856334336 zeus13 11.5  7.57 zeus23 849367040 3.83 2.27 zeus07 208269312 3.64 2.14 zeus03 203206656
benchmarks/array-examples/sorting_bubblesort_true-unreach-call_ground.i 901    878    847069184 zeus21 902    882    zeus20 1597992960 3.69 2.17 204931072 zeus15 901    822    4819165184 zeus21 902    822    zeus07 4848975872 901    826    zeus21 4872540160 4.91 2.85 zeus20 295514112 902    852    4728586240 zeus17 902    839    zeus21 5246083072 3.68 2.19 zeus19 206888960 7.13 4.50 561319936 zeus01 7.11 4.39 zeus10 557977600 902    885    zeus20 836685824 3.63 2.15 zeus23 206032896
benchmarks/array-examples/sorting_selectionsort_true-unreach-call_ground.i 901    882    1408737280 zeus21 902    883    zeus05 1343488000 3.78 2.24 204439552 zeus12 901    818    4609110016 zeus22 902    820    zeus24 4591108096 902    814    zeus22 4560859136 5.21 3.05 zeus04 298414080 902    851    4700446720 zeus24 902    846    zeus21 4877246464 4.12 2.41 zeus06 207511552 7.49 4.70 566435840 zeus04 7.14 4.49 zeus04 562536448 902    883    zeus03 817164288 3.78 2.24 zeus06 207110144
benchmarks/array-examples/standard_compareModified_true-unreach-call_ground.i 901    883    4457943040 zeus02 902    884    zeus15 1332252672 3.63 2.16 202870784 zeus04 902    812    4593389568 zeus13 902    815    zeus09 4571185152 902    818    zeus13 4581625856 4.82 2.86 zeus23 296398848 902    847    4768362496 zeus16 902    851    zeus19 4843966464 3.83 2.30 zeus07 212049920 8.86 5.64 790372352 zeus11 8.99 5.58 zeus15 786272256 901    886    zeus10 833613824 3.62 2.12 zeus13 205860864
benchmarks/array-examples/standard_compare_true-unreach-call_ground.i 902    882    2773061632 zeus17 902    884    zeus13 1347493888 3.58 2.14 202194944 zeus17 902    817    4619423744 zeus21 901    813    zeus16 4595097600 901    816    zeus19 4582277120 5.00 2.91 zeus15 288804864 902    849    4800217088 zeus06 901    839    zeus21 5174366208 3.71 2.21 zeus24 207081472 8.23 5.13 713814016 zeus13 8.02 4.97 zeus21 710815744 902    885    zeus16 848613376 3.63 2.16 zeus04 203915264
benchmarks/array-examples/standard_copy1_true-unreach-call_ground.i 901    880    4715905024 zeus01 901    878    zeus10 4605001728 3.60 2.12 208244736 zeus22 902    811    4602097664 zeus17 901    814    zeus14 4625711104 901    818    zeus08 4591144960 4.89 2.88 zeus15 289476608 902    847    4802977792 zeus09 901    854    zeus01 4814786560 3.62 2.17 zeus08 208207872 7.83 4.95 717905920 zeus24 7.92 5.00 zeus04 720609280 901    885    zeus21 844386304 3.72 2.24 zeus18 202948608
benchmarks/array-examples/standard_copy2_true-unreach-call_ground.i 901    879    4602290176 zeus23 902    874    zeus16 2908827648 3.98 2.38 201383936 zeus04 902    814    4919664640 zeus23 901    814    zeus24 4942798848 902    818    zeus06 4935696384 4.66 2.78 zeus17 294141952 902    846    4760895488 zeus13 901    854    zeus16 4783374336 3.82 2.26 zeus16 210108416 9.29 5.86 792014848 zeus20 8.56 5.44 zeus22 796491776 902    884    zeus18 821030912 3.60 2.15 zeus08 201285632
benchmarks/array-examples/standard_copy3_true-unreach-call_ground.i 902    878    4630581248 zeus14 901    880    zeus11 4424785920 3.83 2.33 208826368 zeus11 902    812    4938903552 zeus22 902    817    zeus07 4936429568 902    821    zeus06 4917002240 5.23 2.98 zeus02 301522944 902    846    4808007680 zeus14 902    854    zeus02 4787027968 3.86 2.27 zeus07 211505152 9.33 6.01 805859328 zeus09 9.05 5.79 zeus06 818724864 902    885    zeus15 832352256 3.90 2.30 zeus13 200867840
benchmarks/array-examples/standard_copy4_true-unreach-call_ground.i 902    879    4595937280 zeus07 902    878    zeus14 2798473216 3.62 2.14 204394496 zeus19 902    814    4915322880 zeus16 902    811    zeus03 4925169664 902    815    zeus16 4894650368 5.22 3.06 zeus17 299511808 902    845    4864548864 zeus16 901    849    zeus01 4838666240 3.91 2.30 zeus16 204673024 9.92 6.44 819191808 zeus18 9.28 6.12 zeus24 816668672 902    884    zeus14 821977088 3.55 2.11 zeus06 200613888
benchmarks/array-examples/standard_copy5_true-unreach-call_ground.i 902    877    4611457024 zeus17 902    878    zeus06 2427658240 3.43 2.06 204988416 zeus09 902    810    4915515392 zeus09 902    814    zeus05 4941352960 902    819    zeus23 4944162816 5.31 3.12 zeus16 296316928 901    844    4863291392 zeus11 901    851    zeus03 4811063296 3.59 2.15 zeus15 204886016 9.58 6.48 864677888 zeus18 10.1  6.80 zeus03 867119104 902    885    zeus06 818307072 3.76 2.22 zeus17 198823936
benchmarks/array-examples/standard_copy6_true-unreach-call_ground.i 901    876    4665012224 zeus14 901    879    zeus04 2750414848 3.78 2.23 204496896 zeus06 902    813    4941389824 zeus02 901    811    zeus06 4977688576 901    820    zeus13 4932857856 4.99 2.90 zeus17 290623488 902    845    4821921792 zeus11 902    858    zeus02 4875407360 4.08 2.42 zeus15 205774848 10.8  7.12 870543360 zeus02 9.95 6.90 zeus03 870469632 902    884    zeus17 819765248 3.82 2.26 zeus03 201150464
benchmarks/array-examples/standard_copy7_true-unreach-call_ground.i 902    876    4673867776 zeus07 902    879    zeus16 2413395968 3.78 2.24 208478208 zeus22 902    815    4977840128 zeus20 902    812    zeus06 4943429632 902    814    zeus02 4943601664 5.26 3.13 zeus22 297910272 902    831    5053186048 zeus21 901    860    zeus24 4859744256 3.92 2.32 zeus05 205377536 12.9  8.41 958169088 zeus08 11.9  7.89 zeus04 955789312 902    885    zeus09 846229504 3.83 2.25 zeus17 202563584
benchmarks/array-examples/standard_copy8_true-unreach-call_ground.i 902    877    4721496064 zeus15 902    879    zeus03 2810458112 3.96 2.32 207728640 zeus08 901    813    4991770624 zeus23 902    814    zeus06 4970323968 901    818    zeus19 4949458944 4.86 2.86 zeus22 296046592 902    838    4891385856 zeus09 902    860    zeus02 4833112064 3.84 2.27 zeus08 203530240 13.0  8.48 957116416 zeus15 13.6  9.10 zeus08 962072576 901    885    zeus24 839278592 3.94 2.31 zeus05 208879616
benchmarks/array-examples/standard_copy9_true-unreach-call_ground.i 901    875    4706111488 zeus19 901    879    zeus15 2392072192 3.68 2.18 206356480 zeus22 901    812    4964835328 zeus17 902    808    zeus02 4917923840 902    816    zeus04 4951543808 5.08 2.99 zeus24 298430464 901    844    4809269248 zeus18 901    859    zeus16 4812181504 3.74 2.25 zeus08 206548992 13.5  9.15 985591808 zeus22 13.2  8.78 zeus15 978915328 901    884    zeus18 833814528 3.84 2.26 zeus06 202600448
benchmarks/array-examples/standard_copyInitSum2_true-unreach-call_ground.i 902    880    4540542976 zeus22 902    875    zeus22 2458230784 3.85 2.22 205611008 zeus16 902    815    4980625408 zeus24 902    812    zeus19 4942340096 902    818    zeus19 4944412672 4.70 2.81 zeus01 294486016 902    850    4718100480 zeus17 902    854    zeus04 4823248896 3.94 2.30 zeus24 206635008 8.31 5.22 722649088 zeus12 8.36 5.27 zeus20 707477504 901    885    zeus05 823910400 3.42 2.01 zeus21 202289152
benchmarks/array-examples/standard_copyInitSum3_true-unreach-call_ground.i 902    880    4532961280 zeus24 901    878    zeus04 2423697408 3.62 2.18 204300288 zeus14 902    814    4955312128 zeus07 902    814    zeus20 4963348480 901    814    zeus12 4927557632 4.93 2.84 zeus21 297885696 902    846    4821127168 zeus12 902    853    zeus13 4910714880 3.71 2.25 zeus22 208637952 8.81 5.46 715284480 zeus17 8.00 5.00 zeus18 713752576 902    885    zeus15 817246208 3.43 2.08 zeus11 207818752
benchmarks/array-examples/standard_copyInitSum_true-unreach-call_ground.i 902    879    4436275200 zeus15 902    877    zeus13 2435379200 3.55 2.12 202145792 zeus09 902    814    4945694720 zeus22 902    819    zeus09 4974845952 902    818    zeus18 4938526720 5.17 3.01 zeus09 291663872 902    849    4755423232 zeus19 901    855    zeus23 4898258944 3.86 2.30 zeus13 205045760 8.36 5.23 718749696 zeus11 8.04 5.01 zeus14 724791296 902    885    zeus20 827047936 4.16 2.43 zeus16 203214848
benchmarks/array-examples/standard_copyInit_true-unreach-call_ground.i 902    879    4452814848 zeus13 902    878    zeus15 4458024960 3.86 2.30 210239488 zeus14 902    816    4977954816 zeus21 901    814    zeus02 4945752064 902    818    zeus13 4945125376 4.99 2.90 zeus15 287395840 901    847    4856913920 zeus01 902    855    zeus20 4922572800 4.03 2.41 zeus12 212582400 7.88 5.00 707194880 zeus08 8.01 5.05 zeus18 722583552 902    885    zeus09 821862400 3.70 2.22 zeus01 200171520
benchmarks/array-examples/standard_find_true-unreach-call_ground.i 901    886    2458087424 zeus07 4.02 2.37 zeus19 216649728 3.51 2.09 208805888 zeus20 902    825    4697186304 zeus24 901    825    zeus02 4759764992 901    824    zeus22 4699639808 4.95 2.91 zeus24 290795520 902    827    5495070720 zeus13 901    820    zeus17 6216536064 3.83 2.27 zeus17 208801792 6.68 4.23 561987584 zeus05 7.18 4.44 zeus16 561872896 902    888    zeus10 880779264 3.77 2.26 zeus13 204820480
benchmarks/array-examples/standard_init1_true-unreach-call_ground.i 902    882    4693245952 zeus13 902    881    zeus12 4611121152 3.61 2.15 201596928 zeus08 901    815    4622180352 zeus10 902    821    zeus13 4581388288 902    820    zeus02 4600623104 5.64 3.24 zeus16 299941888 901    854    4753346560 zeus22 902    847    zeus18 4791689216 3.63 2.12 zeus21 210710528 7.18 4.49 560123904 zeus17 7.49 4.64 zeus06 559730688 902    885    zeus03 827793408 3.41 2.04 zeus03 204513280
benchmarks/array-examples/standard_init2_true-unreach-call_ground.i 902    880    4524240896 zeus10 902    879    zeus02 2926698496 3.60 2.14 202334208 zeus22 901    817    4967768064 zeus04 902    814    zeus03 4920532992 902    820    zeus18 4959907840 4.88 2.89 zeus15 296386560 902    854    4714717184 zeus16 902    853    zeus09 4832866304 4.03 2.40 zeus05 208072704 6.76 4.27 552886272 zeus19 7.49 4.69 zeus13 558751744 902    882    zeus01 841748480 3.49 2.08 zeus10 202969088
benchmarks/array-examples/standard_init3_true-unreach-call_ground.i 902    880    4442673152 zeus08 902    880    zeus11 2785275904 3.84 2.29 203325440 zeus08 902    814    4968996864 zeus22 902    815    zeus10 4980809728 902    815    zeus14 4933832704 4.75 2.83 zeus18 286470144 901    847    4842082304 zeus04 901    849    zeus01 4858785792 3.83 2.28 zeus12 211927040 7.06 4.44 564240384 zeus19 7.24 4.57 zeus22 568385536 902    885    zeus24 813002752 3.49 2.11 zeus07 202813440
benchmarks/array-examples/standard_init4_true-unreach-call_ground.i 901    878    2807599104 zeus19 902    881    zeus20 2421596160 3.92 2.32 210784256 zeus14 901    814    4950265856 zeus11 902    818    zeus11 4931219456 902    818    zeus19 4954349568 4.95 2.90 zeus06 297086976 902    847    4845072384 zeus12 902    856    zeus03 4954537984 3.70 2.22 zeus06 212045824 7.26 4.52 567652352 zeus22 6.72 4.26 zeus22 557613056 902    885    zeus13 825888768 3.61 2.13 zeus20 202297344
benchmarks/array-examples/standard_init5_true-unreach-call_ground.i 901    880    2463645696 zeus12 901    880    zeus06 2728935424 3.76 2.23 209887232 zeus12 902    816    4963049472 zeus15 902    814    zeus05 4965113856 902    815    zeus12 4944203776 5.41 3.21 zeus06 295448576 902    846    4848603136 zeus11 902    853    zeus05 4911570944 3.72 2.21 zeus19 206880768 6.86 4.31 555454464 zeus23 7.17 4.54 zeus24 559046656 902    885    zeus20 827322368 3.49 2.06 zeus21 204029952
benchmarks/array-examples/standard_init6_true-unreach-call_ground.i 901    878    1719681024 zeus02 901    879    zeus05 2405191680 3.47 2.06 205520896 zeus23 902    815    4961816576 zeus03 902    816    zeus14 4957786112 901    818    zeus18 4944044032 4.77 2.82 zeus05 293679104 902    851    4846051328 zeus15 902    858    zeus20 4947689472 3.73 2.21 zeus14 209424384 6.91 4.33 567812096 zeus24 7.31 4.60 zeus17 567017472 901    884    zeus21 831115264 3.78 2.21 zeus15 202719232
benchmarks/array-examples/standard_init7_true-unreach-call_ground.i 901    878    2497077248 zeus12 902    879    zeus10 2369687552 3.81 2.25 206958592 zeus09 902    816    4945747968 zeus02 901    817    zeus13 4954255360 902    819    zeus21 4972982272 4.91 2.95 zeus01 298049536 902    849    4822085632 zeus13 902    859    zeus05 4719763456 3.82 2.33 zeus13 206770176 7.45 4.64 566644736 zeus08 7.24 4.49 zeus20 561950720 902    885    zeus24 810295296 3.77 2.26 zeus24 199528448
benchmarks/array-examples/standard_init8_true-unreach-call_ground.i 901    879    2776698880 zeus08 901    879    zeus06 2380521472 3.76 2.25 208904192 zeus18 901    815    4954968064 zeus13 902    817    zeus03 4985008128 901    817    zeus03 4951912448 5.20 3.00 zeus03 295473152 902    849    4715065344 zeus09 901    859    zeus08 4917067776 3.81 2.29 zeus14 208998400 7.23 4.49 567312384 zeus14 6.96 4.43 zeus11 565006336 901    884    zeus19 829992960 3.93 2.32 zeus13 206856192
benchmarks/array-examples/standard_init9_true-unreach-call_ground.i 901    876    1686024192 zeus01 901    879    zeus12 2666926080 3.67 2.15 202330112 zeus24 902    813    4930539520 zeus05 902    815    zeus18 4956061696 902    819    zeus01 4943966208 5.33 3.12 zeus06 292294656 902    852    4786720768 zeus02 902    856    zeus13 4851834880 3.65 2.20 zeus24 206200832 7.04 4.49 571199488 zeus21 7.37 4.63 zeus20 558743552 902    884    zeus07 831696896 3.73 2.20 zeus03 204959744
benchmarks/array-examples/standard_maxInArray_true-unreach-call_ground.i 902    882    1629605888 zeus23 902    884    zeus15 1277550592 3.68 2.21 206008320 zeus07 902    814    4616232960 zeus02 901    816    zeus09 4596215808 901    818    zeus02 4588142592 4.89 2.90 zeus18 298098688 902    854    4775772160 zeus11 902    858    zeus19 4826578944 3.74 2.23 zeus12 213962752 7.25 4.50 558374912 zeus16 7.64 4.71 zeus02 561807360 901    885    zeus24 831381504 3.57 2.10 zeus23 200974336
benchmarks/array-examples/standard_minInArray_true-unreach-call_ground.i 901    882    1627299840 zeus20 902    884    zeus06 2466349056 3.82 2.29 210587648 zeus01 901    817    4614725632 zeus07 901    814    zeus18 4641247232 901    816    zeus24 4603056128 4.38 2.55 zeus21 301776896 901    854    4761210880 zeus11 902    852    zeus20 4806438912 3.83 2.29 zeus20 210034688 6.82 4.24 560418816 zeus23 7.22 4.65 zeus11 564625408 901    885    zeus21 826826752 3.81 2.24 zeus14 206323712
benchmarks/array-examples/standard_palindrome_true-unreach-call_ground.i 902    881    4620042240 zeus22 902    880    zeus14 4631285760 3.62 2.12 206360576 zeus17 901    815    4619542528 zeus05 901    814    zeus22 4622082048 901    819    zeus03 4597960704 5.08 3.01 zeus07 298373120 901    853    4736999424 zeus04 901    852    zeus18 4801581056 3.59 2.14 zeus20 209240064 7.55 4.72 560427008 zeus05 7.00 4.47 zeus11 559763456 902    885    zeus05 1014292480 3.74 2.19 zeus05 202084352
benchmarks/array-examples/standard_partial_init_true-unreach-call_ground.i 901    883    4586520576 zeus22 902    884    zeus08 1518276608 3.52 2.11 202481664 zeus19 902    813    4614590464 zeus01 901    819    zeus21 4616597504 901    818    zeus17 4540219392 5.16 3.04 zeus19 300113920 901    846    4819136512 zeus10 901    858    zeus18 4944551936 3.60 2.16 zeus08 207269888 8.59 5.52 789929984 zeus22 8.72 5.52 zeus11 798765056 901    886    zeus18 834252800 3.70 2.19 zeus24 204197888
benchmarks/array-examples/standard_partition_original_true-unreach-call_ground.i 901    883    4560318464 zeus05 901    884    zeus15 1354555392 3.60 2.14 210407424 zeus22 902    820    4565278720 zeus10 901    817    zeus08 4559564800 901    824    zeus13 4543660032 5.13 3.01 zeus14 305381376 901    842    4794310656 zeus04 901    858    zeus17 4889780224 3.90 2.31 zeus18 210300928 8.77 5.47 792440832 zeus06 8.99 5.62 zeus18 785321984 902    887    zeus10 838582272 3.84 2.26 zeus06 206884864
benchmarks/array-examples/standard_partition_true-unreach-call_ground.i 902    879    1460465664 zeus09 901    880    zeus18 1343287296 3.48 2.08 202485760 zeus19 902    818    4873019392 zeus23 902    817    zeus03 4894097408 902    817    zeus12 4807036928 4.67 2.77 zeus03 299003904 902    846    4809494528 zeus09 902    857    zeus20 4840734720 3.83 2.28 zeus01 206241792 7.82 4.99 660111360 zeus22 8.27 5.20 zeus11 715649024 901    885    zeus21 842813440 3.72 2.22 zeus12 203755520
benchmarks/array-examples/standard_password_true-unreach-call_ground.i 901    883    2533122048 zeus06 902    884    zeus10 1360384000 3.50 2.08 203542528 zeus24 901    815    4607844352 zeus14 902    816    zeus11 4602871808 902    821    zeus13 4597788672 4.78 2.80 zeus02 302006272 901    850    4767514624 zeus14 902    853    zeus22 4766838784 3.76 2.21 zeus20 205983744 8.21 5.19 663588864 zeus07 7.35 4.69 zeus08 658944000 901    885    zeus07 832131072 3.57 2.13 zeus20 203218944
benchmarks/array-examples/standard_reverse_true-unreach-call_ground.i 901    881    4694265856 zeus07 902    882    zeus07 4594925568 3.98 2.34 211050496 zeus04 901    814    4600123392 zeus06 901    814    zeus03 4625539072 901    818    zeus15 4630056960 4.80 2.84 zeus20 299421696 901    847    4725174272 zeus22 902    849    zeus04 4806807552 3.90 2.31 zeus09 206172160 7.82 5.03 712384512 zeus09 7.41 4.71 zeus04 711020544 902    885    zeus03 818012160 3.83 2.20 zeus16 203878400
benchmarks/array-examples/standard_running_true-unreach-call.i 901    874    1627156480 zeus16 902    876    zeus04 841007104 3.78 2.22 204341248 zeus23 902    813    4882468864 zeus23 901    816    zeus07 4895514624 902    818    zeus12 4877762560 5.10 3.00 zeus19 297664512 901    842    4840353792 zeus08 902    850    zeus20 4762214400 3.62 2.19 zeus11 206036992 7.93 4.93 713891840 zeus09 8.61 5.38 zeus22 713101312 902    885    zeus16 832610304 3.65 2.20 zeus01 205561856
benchmarks/array-examples/standard_sentinel_true-unreach-call.i 5.75 3.49 350908416 zeus07 4.03 2.40 zeus02 219267072 3.73 2.23 204509184 zeus07 902    819    4767928320 zeus23 901    821    zeus01 4840005632 902    818    zeus13 5044678656 5.04 3.02 zeus14 289689600 6.27 3.58 350261248 zeus06 4.29 2.54 zeus23 217821184 3.92 2.33 zeus01 205049856 6.92 4.38 560390144 zeus14 7.67 4.66 zeus07 569954304 4.30 2.56 zeus12 215371776 3.64 2.17 zeus16 203448320
benchmarks/array-examples/standard_seq_init_true-unreach-call_ground.i 902    881    4678696960 zeus17 902    883    zeus09 4597256192 3.74 2.23 206299136 zeus02 901    813    4602736640 zeus22 901    814    zeus13 4607582208 901    815    zeus14 4625100800 4.98 2.88 zeus09 296382464 901    851    4769804288 zeus06 901    859    zeus08 4724658176 3.67 2.20 zeus03 206942208 7.79 4.83 568967168 zeus15 6.93 4.34 zeus06 562159616 902    886    zeus04 828096512 3.55 2.09 zeus22 203743232
benchmarks/array-examples/standard_strcmp_true-unreach-call_ground.i 913    905    3565686784 zeus11 902    883    zeus10 1346396160 3.85 2.28 203616256 zeus01 901    869    4772282368 zeus08 901    867    zeus02 4654886912 901    815    zeus11 4607664128 4.62 2.73 zeus20 298770432 911    894    4489969664 zeus06 902    858    zeus13 4920832000 3.97 2.35 zeus05 204480512 112    107    14999998464 zeus21 111    106    zeus12 14999998464 902    886    zeus08 958259200 3.66 2.17 zeus04 202924032
benchmarks/array-examples/standard_strcpy_original_true-unreach-call.i 902    892    1302568960 zeus03 901    893    zeus08 705626112 3.39 2.03 201867264 zeus10 901    824    4732694528 zeus07 901    825    zeus21 4807438336 901    826    zeus03 4865593344 5.27 3.10 zeus05 303259648 8.15 4.54 467533824 zeus10 901    829    zeus18 6267052032 3.94 2.34 zeus18 207433728 8.07 5.02 716075008 zeus14 7.92 4.97 zeus20 716234752 901    892    zeus21 809558016 3.59 2.11 zeus20 201687040
benchmarks/array-examples/standard_strcpy_true-unreach-call_ground.i 6.68 4.09 458063872 zeus15 3.81 2.25 zeus21 215404544 3.54 2.11 205406208 zeus12 901    818    4693757952 zeus02 902    823    zeus14 4687417344 902    827    zeus06 4612214784 4.85 2.83 zeus14 298291200 7.36 4.17 465403904 zeus07 901    842    zeus22 6021603328 3.91 2.31 zeus09 210386944 7.84 4.90 713834496 zeus08 8.30 5.23 zeus01 653783040 902    887    zeus02 928284672 3.64 2.20 zeus07 202883072
benchmarks/array-examples/standard_two_index_01_true-unreach-call.i 902    882    4603179008 zeus21 901    882    zeus01 4664291328 3.55 2.13 207073280 zeus20 902    818    4898181120 zeus22 902    818    zeus08 4901195776 901    817    zeus13 4904460288 4.91 2.87 zeus01 289673216 901    856    4731269120 zeus22 902    853    zeus22 4795535360 4.64 2.85 zeus07 208572416 901    888    823758848 zeus11 901    888    zeus05 821727232 901    885    zeus12 841474048 3.48 2.07 zeus17 201494528
benchmarks/array-examples/standard_two_index_02_true-unreach-call.i 902    880    4718661632 zeus10 902    882    zeus03 4635725824 3.68 2.16 207048704 zeus06 901    816    4600958976 zeus06 901    814    zeus04 4606160896 902    818    zeus04 4589805568 4.94 2.89 zeus24 296087552 902    845    4824289280 zeus07 902    850    zeus17 4751409152 3.83 2.26 zeus07 214011904 8.04 5.07 716410880 zeus11 8.45 5.28 zeus11 724520960 902    884    zeus02 831721472 4.01 2.36 zeus15 201928704
benchmarks/array-examples/standard_two_index_03_true-unreach-call.i 901    881    4615643136 zeus11 902    882    zeus21 4667715584 3.86 2.23 206315520 zeus03 902    811    4591648768 zeus11 901    818    zeus02 4598472704 902    815    zeus05 4622426112 5.34 3.14 zeus05 296288256 901    851    4784119808 zeus08 901    850    zeus05 4763205632 3.64 2.17 zeus07 206852096 901    889    816902144 zeus09 901    888    zeus05 823390208 901    885    zeus16 849227776 3.63 2.18 zeus09 202100736
benchmarks/array-examples/standard_two_index_04_true-unreach-call.i 901    880    4715077632 zeus03 902    883    zeus05 4659601408 3.95 2.34 206233600 zeus04 902    814    4638285824 zeus01 901    815    zeus01 4604907520 902    820    zeus11 4604018688 5.40 3.12 zeus14 302174208 902    849    4763156480 zeus09 901    846    zeus09 4794413056 3.67 2.18 zeus23 208084992 8.18 5.04 711958528 zeus01 8.67 5.37 zeus16 712851456 901    885    zeus21 854515712 3.84 2.27 zeus05 205709312
benchmarks/array-examples/standard_two_index_05_true-unreach-call.i 901    881    4719988736 zeus19 902    881    zeus24 4525281280 3.47 2.08 202866688 zeus06 902    806    4632797184 zeus08 901    817    zeus10 4612333568 901    817    zeus23 4617830400 4.87 2.88 zeus01 289488896 901    845    4833087488 zeus24 902    854    zeus12 4742598656 3.84 2.30 zeus16 201281536 8.41 5.23 707977216 zeus01 8.03 5.06 zeus03 713256960 902    884    zeus14 825790464 3.86 2.28 zeus05 201117696
benchmarks/array-examples/standard_two_index_06_true-unreach-call.i 901    881    4654194688 zeus14 902    882    zeus14 4663566336 4.05 2.40 204328960 zeus22 902    814    4598906880 zeus24 901    819    zeus21 4591480832 901    818    zeus20 4591640576 4.78 2.79 zeus15 296095744 901    850    4824686592 zeus05 902    846    zeus13 4789260288 3.81 2.24 zeus06 208719872 901    888    824233984 zeus18 901    889    zeus03 818089984 901    886    zeus15 838778880 3.72 2.22 zeus19 200327168
benchmarks/array-examples/standard_two_index_07_true-unreach-call.i 901    880    4703735808 zeus15 902    881    zeus02 4647514112 3.50 2.10 204939264 zeus22 902    814    4609277952 zeus23 901    814    zeus23 4624326656 901    818    zeus19 4613607424 5.01 2.92 zeus20 297525248 901    847    4807372800 zeus01 902    849    zeus13 4790403072 3.92 2.30 zeus01 207376384 8.50 5.26 716529664 zeus14 8.09 5.05 zeus05 708186112 902    885    zeus16 826220544 3.63 2.16 zeus15 198488064
benchmarks/array-examples/standard_two_index_08_true-unreach-call.i 901    881    4725358592 zeus14 901    882    zeus13 4628754432 3.91 2.34 208216064 zeus04 901    814    4602081280 zeus03 902    815    zeus02 4602687488 901    820    zeus02 4598820864 5.15 3.00 zeus01 298582016 902    849    4769062912 zeus19 902    856    zeus09 4806451200 3.75 2.23 zeus07 210661376 8.58 5.29 709038080 zeus16 7.42 4.71 zeus20 658104320 901    885    zeus20 848171008 3.75 2.17 zeus24 202702848
benchmarks/array-examples/standard_two_index_09_true-unreach-call.i 901    880    4717142016 zeus01 902    883    zeus13 4656832512 3.64 2.20 205189120 zeus11 902    819    4601376768 zeus21 902    814    zeus15 4611231744 902    813    zeus15 4609191936 4.71 2.78 zeus20 295194624 901    845    4824440832 zeus13 902    849    zeus15 4806492160 3.85 2.28 zeus22 205000704 7.73 4.93 717348864 zeus14 7.94 5.05 zeus15 708665344 902    885    zeus22 838336512 3.93 2.31 zeus06 200589312
benchmarks/array-examples/standard_vararg_true-unreach-call_ground.i 901    887    2527412224 zeus09 4.18 2.45 zeus01 213610496 3.52 2.11 204738560 zeus15 902    827    4660383744 zeus22 902    828    zeus07 4651290624 901    831    zeus04 4553596928 5.11 2.96 zeus16 297590784 902    804    7534891008 zeus24 901    807    zeus19 8148262912 3.91 2.32 zeus12 206585856 7.30 4.50 564359168 zeus02 6.94 4.38 zeus08 560685056 901    888    zeus22 891920384 3.61 2.13 zeus16 204115968
benchmarks/array-examples/standard_vector_difference_true-unreach-call_ground.i 902    880    4808974336 zeus21 901    882    zeus21 4635201536 3.61 2.15 201809920 zeus20 902    816    4614369280 zeus06 902    816    zeus13 4616880128 902    821    zeus19 4601241600 4.92 2.90 zeus14 298983424 902    835    4990771200 zeus21 902    848    zeus22 4826722304 3.96 2.36 zeus08 202731520 9.06 5.73 798928896 zeus11 8.80 5.62 zeus19 798396416 901    885    zeus03 844906496 3.75 2.24 zeus12 205524992
benchmarks/reducercommutativity/rangesum05_false-unreach-call.i 7.87 4.70 270807040 zeus01 6.89 4.23 zeus10 251473920 10.3  5.80 430088192 zeus07 902    795    4919816192 zeus03 901    801    zeus03 5011025920 197    132    zeus15 3799191552 63.1  32.4  zeus01 1012768768 18.5  9.88 582270976 zeus16 901    821    zeus12 6204637184 20.4  10.8  zeus13 558092288 902    894    464191488 zeus15 902    894    zeus23 475553792 902    894    zeus08 854151168 700    693    zeus18 429907968
benchmarks/reducercommutativity/rangesum10_false-unreach-call.i 14.6  9.88 379768832 zeus10 13.4  8.53 zeus16 355049472 16.4  9.60 546213888 zeus15 901    789    5248798720 zeus10 902    791    zeus08 5234950144 901    738    zeus18 7875842048 100    54.4  zeus16 1417048064 41.3  21.2  854040576 zeus07 902    830    zeus11 6239875072 38.8  19.9  zeus07 811601920 913    907    309100544 zeus05 913    906    zeus04 360026112 913    906    zeus22 373415936 913    908    zeus07 299044864
benchmarks/reducercommutativity/rangesum20_false-unreach-call.i 78.3  66.2  1283522560 zeus14 31.0  20.0  zeus12 770199552 39.8  25.0  904937472 zeus21 902    765    5135667200 zeus04 901    773    zeus12 5174210560 905    751    zeus20 6692122624 310    233    zeus22 4042989568 76.9  41.2  1730428928 zeus06 902    847    zeus04 5074644992 71.5  37.1  zeus01 1245384704 913    908    335585280 zeus02 913    908    zeus19 264310784 913    905    zeus05 393515008 901    895    zeus08 318836736
benchmarks/reducercommutativity/rangesum40_false-unreach-call.i 903    885    6811799552 zeus01 107    91.4  zeus01 1414057984 82.5  60.9  1008279552 zeus12 902    831    4789305344 zeus16 901    830    zeus13 4869681152 902    628    zeus04 12014194688 902    808    zeus19 4611346432 177    126    4524924928 zeus14 912    812    zeus11 6627696640 118    75.5  zeus12 2809114624 913    906    359247872 zeus11 913    907    zeus12 360116224 913    899    zeus15 785686528 913    908    zeus24 290459648
benchmarks/reducercommutativity/rangesum60_false-unreach-call.i 903    882    1697124352 zeus22 417    397    zeus20 2667245568 912    891    1561849856 zeus24 901    827    5519753216 zeus21 901    833    zeus04 5286522880 908    767    zeus07 5046902784 902    811    zeus13 4667924480 622    555    4813320192 zeus16 912    805    zeus19 6105841664 255    205    zeus11 4513325056 913    907    390152192 zeus02 913    907    zeus16 382005248 901    885    zeus13 824307712 913    908    zeus13 270737408
benchmarks/reducercommutativity/rangesum_false-unreach-call.i 11.3  8.63 393011200 zeus08 5.68 3.33 zeus17 243642368 9.79 5.54 412143616 zeus08 1000    550    13054349312 zeus08 1000    550    zeus18 13282893824 1000    533    zeus10 13255888896 1000    533    zeus12 13248749568 37.2  19.2  929648640 zeus15 901    762    zeus16 8463990784 26.0  13.6  zeus21 661528576 902    895    292196352 zeus08 901    895    zeus01 295120896 902    895    zeus04 402411520 913    906    zeus05 328060928
benchmarks/reducercommutativity/avg05_true-unreach-call.i 6.51 3.87 255164416 zeus22 913    906    zeus18 4741926912 913    1030    4590002176 zeus22 901    790    5533442048 zeus19 901    798    zeus19 5417447424 901    771    zeus01 6573727744 903    756    zeus02 7654776832 14.9  7.97 542924800 zeus21 903    831    zeus20 6778241024 903    831    zeus22 6481612800 137    133    349265920 zeus17 58.3  55.0  zeus02 317452288 902    896    zeus04 525946880 902    896    zeus06 499617792
benchmarks/reducercommutativity/avg10_true-unreach-call.i 14.6  9.71 399867904 zeus03 13.0  8.92 zeus19 335323136 902    893    1284706304 zeus02 902    762    5684305920 zeus04 901    772    zeus01 5696233472 920    771    zeus20 6604038144 902    752    zeus22 6530502656 35.4  18.3  847179776 zeus21 907    835    zeus04 6704967680 902    815    zeus14 6624550912 901    894    452546560 zeus21 901    895    zeus08 446726144 901    895    zeus14 396894208 904    895    zeus17 495038464
benchmarks/reducercommutativity/avg20_true-unreach-call.i 82.5  69.6  1161273344 zeus03 35.3  25.0  zeus03 738017280 912    896    5210169344 zeus07 901    753    6172872704 zeus09 902    761    zeus19 6177054720 901    757    zeus11 6242603008 902    747    zeus05 5752815616 70.4  38.3  2079203328 zeus13 908    814    zeus21 6189039616 902    802    zeus06 7095037952 908    895    767528960 zeus12 901    889    zeus01 774758400 902    891    zeus10 600588288 901    889    zeus22 778903552
benchmarks/reducercommutativity/avg40_true-unreach-call.i 888    867    5812273152 zeus11 107    93.1  zeus03 1412075520 391    367    2428219392 zeus13 902    827    4844027904 zeus23 901    828    zeus20 4873535488 902    646    zeus14 10821709824 901    814    zeus17 4620185600 201    152    4530720768 zeus15 913    801    zeus16 6524661760 118    78.6  zeus10 3444486144 468    447    1053503488 zeus07 432    415    zeus21 998735872 902    882    zeus01 852041728 429    405    zeus01 893927424
benchmarks/reducercommutativity/avg60_true-unreach-call.i 902    885    1584357376 zeus13 493    476    zeus18 4770779136 909    877    2751086592 zeus20 901    827    5476872192 zeus14 901    829    zeus21 5396807680 905    786    zeus13 4803764224 901    814    zeus24 4650254336 720    656    5053255680 zeus17 906    820    zeus14 5209206784 347    300    zeus06 4528852992 902    885    919584768 zeus11 902    883    zeus10 906948608 901    881    zeus18 823218176 902    880    zeus10 834826240
benchmarks/reducercommutativity/avg_true-unreach-call.i 11.0  8.52 382648320 zeus01 902    894    zeus20 989138944 913    905    5022183424 zeus24 1000    533    13083406336 zeus10 1000    535    zeus03 13049802752 905    483    zeus08 13057277952 1000    532    zeus09 13114580992 10.8  5.99 548380672 zeus21 901    768    zeus07 8042303488 901    838    zeus10 5489127424 901    896    277196800 zeus07 901    896    zeus16 274665472 901    897    zeus20 260145152 6.13 3.69 zeus07 238297088
benchmarks/reducercommutativity/max05_true-unreach-call.i 6.85 4.09 257044480 zeus19 913    905    zeus10 5331476480 901    889    1663856640 zeus04 901    781    6616317952 zeus21 901    773    zeus20 6629920768 902    770    zeus08 6297858048 901    758    zeus23 6791131136 16.0  8.72 556593152 zeus10 902    839    zeus10 6042279936 902    849    zeus13 5263564800 902    894    831725568 zeus13 902    894    zeus08 839172096 902    895    zeus14 825196544 902    895    zeus07 838877184
benchmarks/reducercommutativity/max10_true-unreach-call.i 15.8  10.7  406462464 zeus11 80.5  75.6  zeus04 14999998464 902    891    768532480 zeus01 902    830    4682457088 zeus11 901    833    zeus19 4704940032 901    784    zeus02 6089969664 912    813    zeus14 5201088512 39.4  20.5  888741888 zeus02 902    868    zeus02 4676894720 907    871    zeus22 4090945536 902    894    783065088 zeus05 902    894    zeus24 771362816 902    893    zeus21 1046892544 901    892    zeus02 831361024
benchmarks/reducercommutativity/max20_true-unreach-call.i 906    889    4573245440 zeus11 97.2  85.9  zeus19 14999998464 908    892    5365030912 zeus02 901    800    5306859520 zeus21 902    797    zeus17 5327605760 902    781    zeus02 6546882560 902    769    zeus15 5888647168 90.2  52.1  3025367040 zeus07 904    857    zeus22 4865400832 911    864    zeus01 3104555008 52.0  41.6  767680512 zeus09 55.0  44.2  zeus13 765698048 902    889    zeus22 742658048 901    887    zeus15 813056000
benchmarks/reducercommutativity/max40_true-unreach-call.i 902    882    3416793088 zeus10 160    146    zeus23 14999998464 128    101    2552381440 zeus03 901    821    4808744960 zeus24 902    827    zeus02 5017337856 903    754    zeus19 7552024576 902    799    zeus12 4617613312 249    193    4558905344 zeus22 911    842    zeus11 5285314560 128    87.4  zeus16 3385483264 638    617    1234341888 zeus07 666    644    zeus23 1265225728 902    883    zeus19 1099436032 439    412    zeus01 946696192
benchmarks/reducercommutativity/max60_true-unreach-call.i 904    885    1591996416 zeus24 417    398    zeus10 14999998464 288    256    2681847808 zeus19 902    835    5343576064 zeus09 901    828    zeus06 5450366976 947    798    zeus20 6706671616 901    802    zeus24 4665585664 902    825    4957229056 zeus20 980    803    zeus13 6827667456 283    232    zeus14 4573421568 902    886    890212352 zeus08 902    887    zeus21 943915008 903    881    zeus19 1367023616 902    881    zeus09 856223744
benchmarks/reducercommutativity/max_true-unreach-call.i 9.13 6.75 386977792 zeus10 902    890    zeus21 904208384 901    887    2964217856 zeus02 901    789    5386182656 zeus17 901    791    zeus14 5387616256 902    804    zeus22 5250080768 902    813    zeus23 5016899584 12.7  6.99 613285888 zeus24 901    852    zeus23 5691379712 901    843    zeus18 5255114752 902    892    827981824 zeus10 902    891    zeus18 832663552 902    893    zeus02 810823680 902    890    zeus18 960290816
benchmarks/reducercommutativity/sep05_true-unreach-call.i 6.71 4.04 258396160 zeus21 32.8  30.1  zeus21 251322368 902    890    2108272640 zeus21 902    739    6686113792 zeus13 902    742    zeus07 6773354496 437    343    zeus22 4690968576 301    212    zeus08 4678180864 19.6  10.4  557600768 zeus15 902    864    zeus03 3985125376 901    783    zeus08 7495888896 902    894    811933696 zeus09 902    894    zeus12 861052928 19.0  16.5  zeus13 241467392 902    895    zeus23 810147840
benchmarks/reducercommutativity/sep10_true-unreach-call.i 15.4  10.3  397668352 zeus12 166    161    zeus17 345948160 902    891    1515417600 zeus04 902    795    5717172224 zeus17 902    792    zeus10 5711458304 914    737    zeus11 8778366976 902    734    zeus16 9881288704 46.1  23.6  884137984 zeus24 902    869    zeus07 1767710720 911    870    zeus17 4511793152 902    894    693190656 zeus14 902    894    zeus03 686125056 349    343    zeus08 384757760 466    460    zeus03 425316352
benchmarks/reducercommutativity/sep20_true-unreach-call.i 568    554    13671854080 zeus18 913    898    zeus06 811704320 639    624    14999998464 zeus04 902    787    5354344448 zeus09 902    780    zeus15 5394378752 902    679    zeus23 9350455296 952    729    zeus03 10721169408 83.6  45.7  1907089408 zeus17 1000    645    zeus13 11655192576 972    578    zeus07 12495331328 901    887    827203584 zeus04 901    888    zeus12 787329024 913    900    zeus24 1935151104 913    898    zeus05 2286088192
benchmarks/reducercommutativity/sep40_true-unreach-call.i 902    881    1117134848 zeus12 912    895    zeus23 992669696 913    889    1563426816 zeus03 901    820    4908924928 zeus10 901    828    zeus21 4973686784 901    810    zeus07 4699111424 901    819    zeus08 4632977408 902    729    8511774720 zeus17 903    593    zeus09 11834048512 133    89.2  zeus17 3500830720 614    595    1088634880 zeus20 627    608    zeus08 1087971328 912    896    zeus08 1800015872 504    479    zeus09 897634304
benchmarks/reducercommutativity/sep60_true-unreach-call.i 901    889    1397952512 zeus08 912    891    zeus06 1938591744 913    886    1419911168 zeus19 901    835    5385125888 zeus18 901    829    zeus12 5345869824 902    822    zeus02 4598452224 904    815    zeus16 4691849216 916    769    8047788032 zeus10 903    682    zeus07 12447629312 313    257    zeus12 4544045056 901    886    931463168 zeus20 901    885    zeus16 919965696 902    880    zeus12 1040519168 902    880    zeus15 841576448
benchmarks/reducercommutativity/sep_true-unreach-call.i 9.37 6.93 390197248 zeus23 902    893    zeus23 959631360 913    905    4996149248 zeus10 902    777    5438427136 zeus04 902    777    zeus24 5753786368 901    810    zeus24 4930289664 901    814    zeus01 4741955584 13.6  7.56 622211072 zeus05 902    851    zeus06 5233074176 901    834    zeus21 5073309696 170    164    724824064 zeus18 309    302    zeus22 775786496 902    894    zeus20 774934528 902    892    zeus22 855556096
benchmarks/reducercommutativity/sum05_true-unreach-call.i 6.03 3.56 251961344 zeus21 902    893    zeus20 853344256 67.7  60.0  746414080 zeus17 901    791    5344923648 zeus12 901    792    zeus19 5261336576 122    75.8  zeus02 2674679808 152    95.4  zeus17 2375905280 13.6  7.49 539045888 zeus12 901    817    zeus24 6028234752 130    98.2  zeus08 3608158208 902    895    787329024 zeus06 902    895    zeus22 789753856 902    895    zeus22 779960320 902    894    zeus11 776065024
benchmarks/reducercommutativity/sum10_true-unreach-call.i 13.4  8.54 394403840 zeus11 9.55 5.67 zeus12 331083776 902    892    736968704 zeus15 901    814    4927037440 zeus01 901    813    zeus06 4918218752 902    771    zeus13 7547740160 901    767    zeus15 6336950272 39.5  20.3  884690944 zeus22 902    826    zeus08 6395793408 901    853    zeus15 4666867712 901    894    491634688 zeus08 902    894    zeus12 496562176 902    894    zeus02 809529344 902    891    zeus13 832753664
benchmarks/reducercommutativity/sum20_true-unreach-call.i 57.2  44.9  1168994304 zeus13 25.5  15.7  zeus07 718032896 901    883    904790016 zeus09 901    805    4670763008 zeus22 901    802    zeus10 4658016256 913    759    zeus15 8047804416 902    763    zeus19 5670051840 71.7  39.7  1605939200 zeus06 901    847    zeus20 4599152640 901    810    zeus08 6661226496 901    889    785006592 zeus03 901    890    zeus16 762531840 901    889    zeus10 794144768 901    889    zeus21 735371264
benchmarks/reducercommutativity/sum40_true-unreach-call.i 640    622    5879193600 zeus13 70.5  56.5  zeus04 1403027456 106    84.0  1589956608 zeus17 901    826    4811530240 zeus17 902    828    zeus20 4964917248 901    771    zeus08 6407626752 901    810    zeus21 4587462656 228    178    4777013248 zeus03 903    843    zeus18 4767547392 117    78.7  zeus17 3241287680 901    881    965353472 zeus23 902    880    zeus06 1019658240 901    884    zeus04 787931136 428    404    zeus10 888856576
benchmarks/reducercommutativity/sum60_true-unreach-call.i 904    886    1594904576 zeus05 207    190    zeus05 4434714624 255    223    2650726400 zeus05 902    829    5402062848 zeus02 901    831    zeus17 5297934336 901    776    zeus07 5278568448 901    805    zeus12 4617699328 672    603    4984733696 zeus01 903    830    zeus12 4629532672 302    253    zeus11 4496699392 901    883    958349312 zeus02 902    884    zeus07 953700352 901    881    zeus10 831131648 902    880    zeus06 829661184
benchmarks/reducercommutativity/sum_true-unreach-call.i 9.37 6.97 383610880 zeus18 901    892    zeus01 744480768 902    891    798273536 zeus14 901    812    4707049472 zeus04 902    811    zeus10 4646027264 901    823    zeus12 4590661632 901    810    zeus21 4638420992 14.3  7.85 602136576 zeus10 901    847    zeus09 5708136448 901    855    zeus07 4734881792 902    894    766750720 zeus01 901    893    zeus21 762249216 902    893    zeus16 843972608 902    892    zeus13 867454976
array-simplified-benchmarks/arrays-size-10/10_data_structures_set_multi_proc_false-unreach-call_ground.i 23.4  18.5  483495936 zeus18 10.4  5.74 zeus24 419946496 12.8  7.56 478048256 zeus23 362    281    5387468800 zeus09 378    295    zeus15 5332271104 72.2  36.9  zeus04 1061752832 901    791    zeus05 7067553792 30.6  15.9  908378112 zeus20 20.0  10.5  zeus05 585895936 29.5  15.3  zeus13 707174400 16.5  11.5  429133824 zeus13 16.1  11.2  zeus11 435916800 11.1  6.68 zeus07 419950592 13.3  7.96 zeus22 465575936
array-simplified-benchmarks/arrays-size-10/10_sorting_bubblesort_false-unreach-call2_ground.i 7.84 4.53 364306432 zeus11 7.12 4.19 zeus19 360271872 8.28 4.94 375570432 zeus11 40.2  20.8  858484736 zeus16 38.3  19.8  zeus17 844529664 38.2  19.6  zeus01 873869312 44.8  23.2  zeus20 855732224 14.2  7.69 488828928 zeus05 14.0  7.72 zeus22 510451712 18.2  9.64 zeus09 582406144 7.43 4.33 352735232 zeus24 7.13 4.18 zeus07 349839360 6.38 3.79 zeus02 253980672 7.69 4.56 zeus21 355635200
array-simplified-benchmarks/arrays-size-10/10_sorting_bubblesort_false-unreach-call_ground.i 7.84 4.43 363433984 zeus03 7.54 4.32 zeus17 358912000 8.11 4.77 375484416 zeus07 40.8  21.0  849371136 zeus12 39.1  20.3  zeus06 860004352 36.6  18.8  zeus21 841408512 41.7  21.6  zeus11 861110272 14.7  7.89 498167808 zeus11 12.1  6.62 zeus21 475086848 17.7  9.38 zeus01 549294080 7.73 4.42 357736448 zeus15 7.06 4.20 zeus12 354373632 6.99 4.15 zeus20 251678720 8.20 4.85 zeus20 349839360
array-simplified-benchmarks/arrays-size-10/10_sorting_selectionsort_false-unreach-call2_ground.i 7.41 4.26 369291264 zeus15 7.68 4.33 zeus22 355520512 7.86 4.47 368205824 zeus18 46.1  23.8  881516544 zeus09 47.1  24.3  zeus24 876113920 47.5  24.5  zeus13 909389824 51.8  26.6  zeus08 897089536 14.9  8.02 527876096 zeus17 14.1  7.64 zeus19 476262400 17.1  9.14 zeus15 536494080 10.5  6.11 390868992 zeus01 9.89 5.73 zeus01 381927424 9.79 5.68 zeus04 379875328 10.6  6.23 zeus06 402395136
array-simplified-benchmarks/arrays-size-10/10_sorting_selectionsort_false-unreach-call_ground.i 6.28 3.61 265601024 zeus11 6.15 3.68 zeus14 261943296 901    891    2349506560 zeus07 901    773    5395603456 zeus16 901    781    zeus19 5633650688 901    777    zeus18 5362552832 901    797    zeus05 5093470208 24.0  12.6  757456896 zeus03 18.5  9.74 zeus03 685907968 34.1  19.8  zeus09 964501504 901    896    314179584 zeus18 901    896    zeus02 314564608 902    893    zeus08 905453568 901    895    zeus21 377982976
array-simplified-benchmarks/arrays-size-10/10_standard_allDiff2_false-unreach-call_ground.i 14.7  8.24 548659200 zeus14 14.4  8.28 zeus04 544669696 14.2  7.92 538472448 zeus12 85.1  44.1  1425281024 zeus07 81.6  42.4  zeus09 1327558656 86.4  44.7  zeus23 1324605440 77.4  40.0  zeus02 1400602624 46.9  24.4  889745408 zeus06 41.6  21.6  zeus06 839958528 45.8  24.0  zeus05 871477248 24.1  16.0  736337920 zeus15 23.5  15.6  zeus21 723005440 24.9  16.9  zeus12 722763776 23.8  16.0  zeus10 725884928
array-simplified-benchmarks/arrays-size-10/10_standard_copy1_false-unreach-call_ground.i 6.68 3.82 263512064 zeus01 6.82 4.03 zeus08 264491008 8.16 4.71 378183680 zeus13 45.8  23.5  872665088 zeus15 45.4  23.4  zeus05 887046144 44.0  22.6  zeus23 903004160 64.3  34.4  zeus13 1391038464 11.9  6.45 439533568 zeus10 10.1  5.56 zeus05 419016704 14.4  7.81 zeus11 485015552 6.67 3.95 255782912 zeus13 6.31 3.74 zeus03 254914560 6.48 3.77 zeus05 249659392 7.25 4.33 zeus05 272367616
array-simplified-benchmarks/arrays-size-10/10_standard_copy2_false-unreach-call_ground.i 11.3  7.09 406425600 zeus15 8.90 5.04 zeus12 297299968 12.4  7.56 456691712 zeus08 74.7  38.9  1189978112 zeus07 68.7  35.8  zeus09 1151590400 57.6  29.7  zeus03 1140416512 901    773    zeus21 8342138880 17.6  9.46 581079040 zeus12 15.2  8.21 zeus20 519663616 25.7  13.5  zeus15 762970112 8.64 5.25 374444032 zeus08 9.02 5.45 zeus14 374267904 7.35 4.48 zeus20 268451840 10.5  6.60 zeus22 401575936
array-simplified-benchmarks/arrays-size-10/10_standard_copy3_false-unreach-call_ground.i 18.2  13.4  471011328 zeus07 11.3  6.45 zeus13 432324608 17.2  11.4  591618048 zeus12 615    437    11032576000 zeus14 611    428    zeus13 10919972864 70.1  37.3  zeus19 1341657088 902    775    zeus18 7641153536 27.2  14.2  674377728 zeus11 19.4  10.3  zeus17 612872192 42.7  22.0  zeus01 936366080 12.0  7.14 428138496 zeus22 12.2  7.32 zeus22 424611840 10.8  6.58 zeus22 396754944 14.2  9.17 zeus05 479481856
array-simplified-benchmarks/arrays-size-10/10_standard_copy4_false-unreach-call_ground.i 32.2  26.9  517390336 zeus04 13.0  7.61 zeus12 482639872 27.3  19.6  781148160 zeus05 1000    669    12020342784 zeus11 1000    679    zeus20 11874877440 87.2  48.6  zeus17 1585627136 901    791    zeus11 6165086208 33.8  17.5  686018560 zeus06 25.3  13.3  zeus04 734994432 46.5  23.9  zeus14 889995264 13.8  8.48 457191424 zeus12 15.0  8.99 zeus16 451117056 12.2  7.51 zeus22 408379392 19.9  13.4  zeus04 592064512
array-simplified-benchmarks/arrays-size-10/10_standard_copy5_false-unreach-call_ground.i 67.7  61.3  757989376 zeus15 17.0  10.1  zeus07 559718400 49.6  40.9  845213696 zeus10 902    638    10884358144 zeus08 901    645    zeus12 11308531712 109    65.3  zeus10 2457645056 901    832    zeus16 4523327488 39.5  20.4  854360064 zeus07 33.2  17.2  zeus11 823701504 42.7  22.3  zeus04 1347510272 15.7  9.84 496852992 zeus12 15.8  9.99 zeus10 498180096 14.0  8.81 zeus05 434520064 24.6  17.6  zeus23 729022464
array-simplified-benchmarks/arrays-size-10/10_standard_copy6_false-unreach-call_ground.i 133    125    1208758272 zeus22 18.2  11.0  zeus22 622108672 94.1  83.6  886419456 zeus20 992    646    9081450496 zeus09 901    623    zeus02 9669664768 139    88.5  zeus13 3680825344 901    837    zeus03 4572852224 42.7  22.0  859549696 zeus10 37.4  19.4  zeus07 859942912 55.5  29.7  zeus07 1373470720 17.7  11.6  530857984 zeus01 17.1  11.0  zeus16 530722816 14.9  9.55 zeus17 453787648 31.8  23.9  zeus05 792240128
array-simplified-benchmarks/arrays-size-10/10_standard_copy7_false-unreach-call_ground.i 246    236    1503191040 zeus14 21.8  13.3  zeus07 715501568 152    140    927076352 zeus11 903    626    9376710656 zeus04 902    628    zeus09 9356099584 159    106    zeus10 4454043648 901    825    zeus13 4590641152 47.0  24.1  886419456 zeus03 40.0  20.7  zeus17 871948288 53.8  29.1  zeus23 1735266304 19.5  13.0  565207040 zeus03 20.0  13.3  zeus11 559673344 17.2  11.3  zeus17 474574848 39.7  31.6  zeus09 788471808
array-simplified-benchmarks/arrays-size-10/10_standard_copy8_false-unreach-call_ground.i 389    377    2237628416 zeus12 27.8  17.0  zeus07 781144064 209    194    1013276672 zeus03 901    638    9813319680 zeus05 902    632    zeus12 9251041280 231    165    zeus08 5573890048 901    821    zeus06 4685717504 52.4  27.5  1221857280 zeus04 42.0  21.7  zeus08 862654464 57.5  31.8  zeus06 1518469120 23.6  16.3  605962240 zeus17 21.3  14.5  zeus21 617795584 18.8  12.7  zeus23 501948416 48.3  39.7  zeus18 803139584
array-simplified-benchmarks/arrays-size-10/10_standard_copy9_false-unreach-call_ground.i 609    595    3665969152 zeus23 30.4  19.0  zeus20 796672000 236    219    1040715776 zeus07 902    653    9429958656 zeus07 902    654    zeus22 9487093760 297    220    zeus05 6184513536 901    803    zeus20 4810653696 56.9  30.0  1299668992 zeus12 46.8  24.2  zeus06 877473792 66.5  38.3  zeus02 2184110080 24.5  17.0  671457280 zeus14 23.7  16.5  zeus03 654589952 21.7  14.7  zeus04 529563648 61.4  51.7  zeus11 812437504
array-simplified-benchmarks/arrays-size-10/10_standard_copyInitSum2_false-unreach-call_ground.i 9.48 5.72 322232320 zeus11 12.0  7.01 zeus06 449249280 22.6  14.1  633171968 zeus21 88.6  46.0  1323089920 zeus10 84.8  43.9  zeus07 1293135872 88.8  45.6  zeus15 1352474624 106    60.1  zeus16 1917091840 31.0  16.1  815202304 zeus06 19.2  10.3  zeus06 663552000 35.8  18.4  zeus12 682119168 901    895    321515520 zeus20 901    895    zeus07 328208384 33.3  27.9  zeus04 439975936 33.4  26.6  zeus06 490610688
array-simplified-benchmarks/arrays-size-10/10_standard_init1_false-unreach-call_ground.i 6.51 3.72 274071552 zeus03 6.39 3.68 zeus23 261324800 7.30 4.19 363323392 zeus01 43.2  22.4  827817984 zeus18 38.9  20.2  zeus04 834314240 39.3  20.4  zeus04 832868352 51.3  26.4  zeus09 903729152 9.43 5.31 404963328 zeus08 9.10 5.09 zeus22 394166272 12.7  6.90 zeus13 469053440 7.65 4.48 339009536 zeus22 6.64 4.02 zeus19 260739072 6.05 3.68 zeus18 249409536 7.29 4.39 zeus06 351449088
array-simplified-benchmarks/arrays-size-10/10_standard_init2_false-unreach-call_ground.i 10.0  5.53 416624640 zeus22 8.93 5.00 zeus01 306110464 9.57 5.64 404467712 zeus11 52.7  27.1  897650688 zeus14 54.2  27.8  zeus15 921690112 54.2  27.8  zeus14 943755264 57.9  29.7  zeus21 1015271424 15.5  8.38 533233664 zeus24 15.5  8.30 zeus22 511041536 22.7  12.0  zeus10 634920960 8.51 5.20 367267840 zeus14 8.80 5.33 zeus14 361881600 7.94 4.80 zeus02 267952128 9.23 5.72 zeus14 377401344
array-simplified-benchmarks/arrays-size-10/10_standard_init3_false-unreach-call_ground.i 13.3  7.48 443699200 zeus20 11.4  6.50 zeus11 426975232 12.6  7.69 466587648 zeus19 65.5  33.6  1032712192 zeus18 66.5  34.2  zeus16 1002070016 64.7  33.2  zeus08 1139470336 74.7  39.0  zeus14 1509957632 21.1  11.1  642584576 zeus21 21.1  11.1  zeus08 632242176 28.7  14.9  zeus22 731410432 11.7  6.90 413368320 zeus10 11.1  6.66 zeus08 412094464 11.1  6.59 zeus03 397766656 12.4  7.81 zeus04 416362496
array-simplified-benchmarks/arrays-size-10/10_standard_init4_false-unreach-call_ground.i 13.1  7.74 481976320 zeus13 12.1  7.18 zeus11 466173952 14.5  9.20 543080448 zeus24 71.4  37.5  1242722304 zeus23 72.1  37.7  zeus13 1246900224 74.7  38.6  zeus15 1236582400 75.5  40.5  zeus06 1442398208 23.5  12.4  617914368 zeus15 24.5  12.9  zeus01 707354624 33.9  17.5  zeus18 694288384 13.0  7.92 416657408 zeus12 12.2  7.48 zeus24 412995584 11.3  6.86 zeus21 403697664 14.3  9.25 zeus06 437157888
array-simplified-benchmarks/arrays-size-10/10_standard_init5_false-unreach-call_ground.i 16.2  9.51 542724096 zeus03 14.6  8.78 zeus05 522936320 20.6  13.0  612089856 zeus19 83.8  44.9  1473294336 zeus05 83.9  45.1  zeus03 1403719680 79.3  42.3  zeus21 1420460032 83.5  46.2  zeus06 1687879680 29.7  15.5  719138816 zeus06 33.0  17.1  zeus16 809455616 36.1  18.7  zeus10 806187008 15.7  9.74 442605568 zeus12 13.6  8.52 zeus18 440696832 14.1  8.68 zeus01 440381440 17.4  11.7  zeus20 461262848
array-simplified-benchmarks/arrays-size-10/10_standard_init6_false-unreach-call_ground.i 19.2  12.0  617025536 zeus14 18.2  11.3  zeus19 600666112 23.6  15.6  737464320 zeus19 96.1  53.1  1601736704 zeus01 101    55.3  zeus09 1647382528 95.0  52.2  zeus01 1637056512 94.2  53.6  zeus01 2199429120 35.4  18.4  757919744 zeus14 33.8  17.5  zeus23 867508224 40.7  21.1  zeus13 846626816 16.2  10.3  465383424 zeus01 16.0  10.1  zeus04 460431360 15.0  9.54 zeus21 465526784 20.6  14.3  zeus08 501608448
array-simplified-benchmarks/arrays-size-10/10_standard_init7_false-unreach-call_ground.i 26.0  15.7  775774208 zeus04 21.8  13.5  zeus15 683220992 29.4  19.4  796950528 zeus18 109    64.0  2053767168 zeus06 108    63.2  zeus13 1980608512 102    58.9  zeus13 1875550208 113    66.1  zeus01 2553532416 37.7  19.4  886800384 zeus18 37.8  19.6  zeus07 860139520 41.2  21.3  zeus10 849416192 17.2  11.2  492920832 zeus12 17.6  11.5  zeus17 488546304 17.0  11.1  zeus08 488972288 22.5  16.3  zeus11 520531968
array-simplified-benchmarks/arrays-size-10/10_standard_init8_false-unreach-call_ground.i 28.4  17.9  819597312 zeus06 26.2  16.4  zeus08 800575488 38.1  24.8  853590016 zeus01 122    75.6  2549612544 zeus14 127    78.6  zeus07 2849099776 125    76.4  zeus09 2463420416 126    77.3  zeus14 2877161472 41.2  21.2  874803200 zeus20 42.4  21.8  zeus03 875835392 43.2  22.5  zeus19 872235008 19.4  12.8  521732096 zeus11 19.5  12.9  zeus07 506707968 18.9  12.6  zeus21 506949632 26.1  19.4  zeus03 555630592
array-simplified-benchmarks/arrays-size-10/10_standard_init9_false-unreach-call_ground.i 32.5  20.4  845467648 zeus16 29.0  18.7  zeus10 794542080 40.8  28.2  877043712 zeus20 152    99.3  3091001344 zeus23 148    97.6  zeus01 3178127360 140    90.8  zeus06 2610257920 141    90.3  zeus22 3301072896 44.5  22.9  884490240 zeus21 42.0  21.7  zeus09 887799808 48.9  25.5  zeus10 1009745920 22.5  15.1  544698368 zeus03 21.5  14.4  zeus24 539291648 20.7  14.1  zeus21 544043008 30.3  23.0  zeus09 603635712
array-simplified-benchmarks/arrays-size-10/10_standard_minInArray_false-unreach-call_ground.i 8.02 4.49 358137856 zeus15 6.60 3.79 zeus16 269729792 7.37 4.20 354668544 zeus06 51.6  26.5  874582016 zeus23 53.2  27.4  zeus18 886743040 47.6  24.5  zeus04 863973376 59.6  30.6  zeus20 1064722432 11.1  6.11 436867072 zeus14 9.88 5.44 zeus07 415404032 11.7  6.47 zeus10 467603456 6.91 4.08 341479424 zeus17 7.53 4.40 zeus02 345374720 6.23 3.76 zeus23 263114752 7.23 4.31 zeus22 347246592
array-simplified-benchmarks/arrays-size-10/10_standard_partition_false-unreach-call_ground.i 901    888    733655040 zeus08 902    886    zeus20 724684800 123    115    779694080 zeus02 902    820    4606742528 zeus10 902    819    zeus13 4603625472 634    549    zeus16 4602118144 901    822    zeus07 4620800000 31.6  16.6  885997568 zeus09 255    219    zeus03 4684791808 235    193    zeus13 4486582272 902    893    792543232 zeus14 902    894    zeus09 819044352 902    894    zeus13 835457024 902    893    zeus15 790315008
array-simplified-benchmarks/arrays-size-10/10_standard_running_false-unreach-call.i 12.5  7.28 436080640 zeus04 11.8  6.62 zeus03 420687872 12.7  7.15 459550720 zeus02 77.1  39.3  1130885120 zeus21 71.5  36.6  zeus02 1148321792 73.6  37.6  zeus15 1090859008 72.9  38.4  zeus03 1353752576 32.0  16.6  713068544 zeus15 23.1  12.2  zeus03 696946688 29.2  15.3  zeus24 638926848 9.29 5.69 382074880 zeus22 9.79 5.96 zeus16 386314240 8.71 5.33 zeus08 365752320 10.7  6.50 zeus02 403304448
array-simplified-benchmarks/arrays-size-10/10_data_structures_set_multi_proc_trivial_true-unreach-call_ground.i 9.51 5.94 298967040 zeus09 7.88 4.51 zeus02 286945280 8.55 5.01 302424064 zeus19 167    106    2324893696 zeus14 171    107    zeus07 2197401600 112    60.4  zeus20 1664118784 590    516    zeus15 4558540800 68.9  35.1  1295675392 zeus17 54.2  27.7  zeus10 856997888 62.6  32.0  zeus12 943882240 25.8  18.3  459288576 zeus22 29.0  20.6  zeus04 450625536 18.6  11.4  zeus10 445399040 18.9  11.9  zeus18 475267072
array-simplified-benchmarks/arrays-size-10/10_data_structures_set_multi_proc_true-unreach-call_ground.i 29.4  23.3  531542016 zeus09 11.7  6.58 zeus24 454492160 17.7  10.6  502886400 zeus03 411    329    5652631552 zeus21 426    332    zeus16 5575950336 78.9  40.6  zeus17 1169448960 900    724    zeus02 6959935488 48.0  24.6  899534848 zeus12 39.9  20.5  zeus18 723484672 54.6  27.9  zeus12 881405952 22.8  16.4  486117376 zeus24 24.0  17.5  zeus01 493223936 17.1  10.8  zeus17 473608192 17.8  11.3  zeus21 526856192
array-simplified-benchmarks/arrays-size-10/10_relax_true-unreach-call.i 4.49 2.66 217849856 zeus03 4.65 2.68 zeus08 221044736 4.47 2.57 215179264 zeus16 6.06 3.47 308121600 zeus11 5.55 3.20 zeus08 308105216 10.3  5.73 zeus05 439459840 5.91 3.35 zeus17 309080064 4.64 2.68 223371264 zeus13 4.70 2.78 zeus06 225730560 4.49 2.63 zeus04 220311552 4.36 2.60 217980928 zeus07 4.56 2.67 zeus08 211812352 4.97 2.89 zeus09 232034304 4.45 2.55 zeus12 219938816
array-simplified-benchmarks/arrays-size-10/10_sanfoundry_02_true-unreach-call_ground.i 902    892    735027200 zeus21 902    891    zeus20 743415808 902    892    2310266880 zeus16 902    780    5154414592 zeus11 901    779    zeus07 5143842816 902    774    zeus07 4968169472 902    789    zeus14 4786524160 907    894    795451392 zeus02 901    810    zeus20 7527256064 902    795    zeus02 6811234304 902    892    864038912 zeus23 902    893    zeus13 871587840 18.2  13.2  zeus05 414294016 902    894    zeus15 840818688
array-simplified-benchmarks/arrays-size-10/10_sanfoundry_10_true-unreach-call_ground.i 8.02 4.67 288722944 zeus19 9.67 5.60 zeus04 341184512 86.8  72.8  1335259136 zeus01 497    426    4448403456 zeus21 506    432    zeus14 4640378880 396    329    zeus03 4553232384 521    445    zeus19 4625694720 17.2  9.25 609980416 zeus17 15.2  8.23 zeus01 596267008 116    82.2  zeus04 3624701952 901    884    821870592 zeus04 901    886    zeus01 842366976 303    288    zeus09 858140672 901    887    zeus03 812994560
array-simplified-benchmarks/arrays-size-10/10_sanfoundry_24_true-unreach-call.i 3.79 2.25 209838080 zeus08 4.17 2.46 zeus09 210702336 3.89 2.29 211890176 zeus24 11.5  6.45 402792448 zeus22 10.1  5.54 zeus21 385110016 11.7  6.38 zeus13 402608128 9.89 5.47 zeus24 389115904 4.26 2.52 215846912 zeus10 4.11 2.46 zeus09 217042944 4.45 2.65 zeus10 220164096 3.91 2.29 209186816 zeus17 4.04 2.44 zeus12 213995520 3.93 2.34 zeus01 204709888 3.84 2.27 zeus08 207425536
array-simplified-benchmarks/arrays-size-10/10_sanfoundry_27_true-unreach-call_ground.i 902    893    737169408 zeus06 901    891    zeus20 753377280 901    892    2319495168 zeus23 106    57.0  1548804096 zeus10 112    60.1  zeus05 1575288832 107    57.2  zeus23 1540464640 109    58.9  zeus12 1483096064 902    773    8172748800 zeus12 901    768    zeus23 8620449792 901    742    zeus02 9363902464 902    893    797073408 zeus12 902    893    zeus01 808214528 902    894    zeus22 791572480 902    893    zeus01 828293120
array-simplified-benchmarks/arrays-size-10/10_sanfoundry_43_true-unreach-call_ground.i 3.76 2.30 213573632 zeus04 3.74 2.22 zeus16 200806400 3.75 2.21 213942272 zeus21 5.86 3.37 312504320 zeus14 6.04 3.42 zeus09 321335296 5.28 3.08 zeus23 314535936 5.16 3.04 zeus19 300699648 3.87 2.29 214097920 zeus20 3.68 2.20 zeus19 208457728 4.23 2.55 zeus13 215904256 3.79 2.24 213618688 zeus20 3.69 2.23 zeus14 208719872 3.67 2.23 zeus18 209121280 3.73 2.21 zeus20 206757888
array-simplified-benchmarks/arrays-size-10/10_sorting_bubblesort_true-unreach-call_ground.i 6.34 3.65 242925568 zeus16 12.1  7.51 zeus16 340299776 52.2  39.1  776458240 zeus14 901    819    4668608512 zeus11 901    816    zeus14 4658331648 902    816    zeus15 4689584128 901    821    zeus12 4608983040 901    787    8470372352 zeus12 48.5  27.1  zeus07 1835790336 55.0  28.6  zeus01 1218605056 902    893    805199872 zeus06 901    893    zeus07 799035392 902    893    zeus19 844398592 902    893    zeus24 844599296
array-simplified-benchmarks/arrays-size-10/10_sorting_selectionsort_true-unreach-call_ground.i 7.02 4.09 288067584 zeus22 5.67 3.37 zeus23 249081856 901    890    4478672896 zeus19 901    778    5421883392 zeus14 901    781    zeus17 5252415488 901    779    zeus21 5356580864 902    798    zeus23 5100236800 25.1  13.2  646950912 zeus06 15.6  8.49 zeus17 674709504 902    851    zeus07 4815097856 901    895    315789312 zeus24 901    896    zeus10 320360448 11.8  8.69 zeus04 270045184 902    894    zeus05 754053120
array-simplified-benchmarks/arrays-size-10/10_standard_compareModified_true-unreach-call_ground.i 7.22 4.10 250277888 zeus02 901    883    zeus06 4221452288 901    889    754069504 zeus23 901    828    4144775168 zeus03 901    831    zeus05 4528881664 902    823    zeus03 4695240704 901    835    zeus10 4532609024 13.4  7.32 496582656 zeus07 60.9  33.5  zeus11 1959571456 901    762    zeus06 6882283520 901    892    774623232 zeus24 902    892    zeus18 785965056 902    889    zeus14 881143808 902    893    zeus11 838946816
array-simplified-benchmarks/arrays-size-10/10_standard_compare_true-unreach-call_ground.i 902    883    2356793344 zeus09 901    884    zeus03 4211621888 902    882    2326511616 zeus02 511    450    4490825728 zeus09 481    425    zeus20 4038266880 165    117    zeus23 2685980672 466    408    zeus06 3590950912 62.3  35.1  1736888320 zeus05 51.7  27.7  zeus19 1394270208 901    863    zeus18 5220503552 287    281    686505984 zeus11 296    290    zeus07 695074816 45.3  39.3  zeus18 670183424 902    893    zeus06 832884736
array-simplified-benchmarks/arrays-size-10/10_standard_copy1_true-unreach-call_ground.i 5.70 3.36 246640640 zeus11 6.05 3.49 zeus14 238526464 13.4  8.80 365047808 zeus03 902    824    4671025152 zeus12 902    822    zeus18 4689993728 97.4  54.5  zeus14 1628635136 161    111    zeus13 2708480000 7.95 4.41 300257280 zeus21 7.27 4.06 zeus19 277495808 33.1  17.1  zeus20 759988224 673    664    785379328 zeus20 668    660    zeus12 767782912 275    269    zeus14 679575552 901    894    zeus13 823943168
array-simplified-benchmarks/arrays-size-10/10_standard_copy2_true-unreach-call_ground.i 8.53 5.03 295624704 zeus16 8.04 4.61 zeus20 285200384 25.4  19.8  608546816 zeus01 901    816    4648431616 zeus22 902    819    zeus18 4624543744 150    94.1  zeus02 2208518144 703    635    zeus06 4576456704 17.9  9.62 704786432 zeus18 12.5  6.90 zeus09 431796224 52.1  26.6  zeus24 898314240 902    893    811577344 zeus17 902    893    zeus09 838209536 902    892    zeus13 859557888 902    892    zeus22 820609024
array-simplified-benchmarks/arrays-size-10/10_standard_copy3_true-unreach-call_ground.i 11.6  7.72 339857408 zeus13 9.26 5.59 zeus06 314593280 56.0  48.2  706609152 zeus04 901    817    4594249728 zeus15 902    820    zeus12 4570521600 197    134    zeus02 2446970880 902    820    zeus16 4968505344 29.9  15.6  852074496 zeus07 19.6  10.4  zeus11 656482304 58.2  30.2  zeus01 1423908864 902    894    746438656 zeus18 902    893    zeus10 808869888 902    891    zeus06 824627200 902    892    zeus17 829493248
array-simplified-benchmarks/arrays-size-10/10_standard_copy4_true-unreach-call_ground.i 17.5  13.2  417996800 zeus13 12.5  7.72 zeus15 363253760 90.7  81.0  757956608 zeus18 901    818    4620169216 zeus18 901    817    zeus10 4567953408 239    175    zeus17 3085926400 901    806    zeus20 5375283200 36.0  19.2  980111360 zeus22 23.3  12.1  zeus08 681197568 69.9  37.9  zeus16 1911791616 902    893    786333696 zeus03 902    893    zeus08 772390912 902    892    zeus18 793780224 901    890    zeus21 823279616
array-simplified-benchmarks/arrays-size-10/10_standard_copy5_true-unreach-call_ground.i 28.8  23.8  548847616 zeus05 14.8  9.25 zeus12 435822592 163    152    779722752 zeus20 901    812    4562599936 zeus18 902    811    zeus09 4584275968 276    208    zeus10 3898257408 902    831    zeus02 4528369664 44.9  24.6  1333149696 zeus02 27.3  14.3  zeus14 790839296 83.0  46.3  zeus16 1914433536 902    893    793665536 zeus19 902    892    zeus24 795877376 901    892    zeus05 707321856 901    890    zeus16 783851520
array-simplified-benchmarks/arrays-size-10/10_standard_copy6_true-unreach-call_ground.i 47.9  42.4  758054912 zeus18 17.8  11.2  zeus08 519180288 288    273    892370944 zeus12 901    810    4649820160 zeus11 901    811    zeus17 4710273024 331    256    zeus24 3919908864 901    838    zeus05 4563431424 51.7  29.4  1623277568 zeus02 33.0  17.0  zeus10 860012544 95.7  57.2  zeus13 3028004864 902    890    835149824 zeus21 902    892    zeus12 792895488 901    892    zeus19 662372352 901    890    zeus14 728670208
array-simplified-benchmarks/arrays-size-10/10_standard_copy7_true-unreach-call_ground.i 84.5  76.2  946003968 zeus13 21.7  14.2  zeus03 646057984 433    419    882311168 zeus12 901    802    4731912192 zeus24 901    806    zeus07 4679208960 384    301    zeus13 3798581248 902    827    zeus12 4631932928 63.4  38.2  2290061312 zeus14 33.1  17.2  zeus24 832040960 109    68.4  zeus03 3713830912 902    891    858136576 zeus11 904    892    zeus04 845307904 902    893    zeus24 427597824 902    892    zeus21 695267328
array-simplified-benchmarks/arrays-size-10/10_standard_copy8_true-unreach-call_ground.i 132    122    1281617920 zeus21 24.5  15.6  zeus04 730345472 625    607    953204736 zeus16 902    803    4756496384 zeus23 901    805    zeus09 4761595904 426    347    zeus19 4407574528 901    820    zeus03 4642471936 69.9  45.6  2950307840 zeus11 40.2  20.8  zeus14 858681344 136    95.5  zeus13 3742597120 902    890    805490688 zeus16 902    890    zeus01 809594880 901    892    zeus01 457404416 901    891    zeus20 692555776
array-simplified-benchmarks/arrays-size-10/10_standard_copy9_true-unreach-call_ground.i 189    180    1424257024 zeus03 29.7  19.4  zeus21 752992256 842    824    964206592 zeus05 901    796    4825952256 zeus17 902    802    zeus10 4784201728 479    395    zeus19 4500721664 901    799    zeus14 4842446848 85.9  59.7  3661729792 zeus12 38.7  20.0  zeus21 853012480 156    106    zeus02 4527009792 901    888    867684352 zeus21 901    888    zeus17 835080192 901    894    zeus04 359964672 902    892    zeus19 663896064
array-simplified-benchmarks/arrays-size-10/10_standard_copyInitSum2_true-unreach-call_ground.i 9.63 5.63 319737856 zeus15 11.0  6.58 zeus16 318849024 85.7  77.2  739704832 zeus21 182    117    2454216704 zeus17 180    116    zeus13 2388529152 165    110    zeus10 2107531264 255    194    zeus02 3410665472 20.0  10.7  613625856 zeus05 21.1  11.1  zeus22 603262976 76.5  40.2  zeus14 1321889792 21.1  16.6  357253120 zeus18 21.1  16.7  zeus08 346091520 901    892    zeus09 763953152 491    482    zeus16 720789504
array-simplified-benchmarks/arrays-size-10/10_standard_copyInitSum3_true-unreach-call_ground.i 13.8  9.55 403169280 zeus04 11.6  7.31 zeus09 375169024 902    889    767598592 zeus14 203    134    3135873024 zeus21 203    135    zeus19 3425304576 168    106    zeus02 2407399424 871    793    zeus14 4583063552 36.2  18.8  884621312 zeus22 30.1  15.7  zeus23 883458048 87.8  46.0  zeus08 1341128704 53.8  48.6  493293568 zeus09 58.1  52.8  zeus03 491216896 901    891    zeus20 869609472 901    890    zeus07 743481344
array-simplified-benchmarks/arrays-size-10/10_standard_copyInitSum_true-unreach-call_ground.i 8.98 5.42 308224000 zeus14 10.2  6.07 zeus01 322375680 76.3  67.4  741142528 zeus16 169    109    2739208192 zeus01 160    103    zeus03 2211819520 166    110    zeus22 2296160256 256    194    zeus16 2959052800 31.6  16.5  882688000 zeus23 22.2  11.7  zeus20 747511808 69.6  36.4  zeus19 1180856320 902    891    846909440 zeus13 902    891    zeus07 851230720 902    891    zeus07 769310720 478    468    zeus11 716800000
array-simplified-benchmarks/arrays-size-10/10_standard_copyInit_true-unreach-call_ground.i 9.14 5.15 290177024 zeus16 8.97 5.04 zeus15 293183488 20.5  14.6  580030464 zeus12 166    106    2515296256 zeus11 174    113    zeus20 2253381632 124    74.1  zeus10 1874886656 219    163    zeus04 3111063552 13.5  7.38 540688384 zeus06 11.4  6.30 zeus06 402247680 54.0  27.5  zeus15 903983104 714    705    781807616 zeus14 902    893    zeus18 808591360 351    342    zeus14 765931520 252    245    zeus19 686215168
array-simplified-benchmarks/arrays-size-10/10_standard_find_true-unreach-call_ground.i 901    886    4220043264 zeus01 4.05 2.44 zeus12 218161152 901    886    4215877632 zeus01 257    210    3510079488 zeus18 280    231    zeus21 4101079040 231    186    zeus22 4287946752 260    211    zeus02 4400697344 50.7  27.3  1239461888 zeus03 48.4  26.3  zeus13 926220288 42.8  23.5  zeus08 1237372928 383    371    803143680 zeus17 479    467    zeus16 792895488 129    118    zeus21 773545984 422    409    zeus22 797999104
array-simplified-benchmarks/arrays-size-10/10_standard_init1_true-unreach-call_ground.i 5.65 3.31 234749952 zeus05 5.78 3.33 zeus02 232116224 11.3  6.94 359907328 zeus01 103    61.0  1861480448 zeus12 101    60.1  zeus05 1663827968 96.8  55.0  zeus18 1787469824 92.3  50.4  zeus06 1560039424 7.39 4.16 285970432 zeus11 7.58 4.26 zeus05 272240640 29.1  15.2  zeus15 671985664 460    453    699228160 zeus18 412    406    zeus07 701480960 135    129    zeus10 690597888 121    116    zeus04 483135488
array-simplified-benchmarks/arrays-size-10/10_standard_init2_true-unreach-call_ground.i 8.15 4.54 282656768 zeus24 7.98 4.54 zeus12 285171712 14.6  9.68 448659456 zeus15 115    64.8  1618477056 zeus22 103    58.0  zeus18 1575636992 103    57.2  zeus13 1667891200 103    55.0  zeus02 1451843584 12.7  6.87 511885312 zeus19 10.9  6.08 zeus03 407072768 36.9  19.0  zeus13 712794112 901    893    721010688 zeus16 901    893    zeus05 710311936 178    171    zeus05 684126208 206    199    zeus01 506732544
array-simplified-benchmarks/arrays-size-10/10_standard_init3_true-unreach-call_ground.i 9.47 5.45 313163776 zeus10 9.39 5.52 zeus05 304181248 19.3  13.3  497184768 zeus24 111    62.6  1892442112 zeus09 115    64.3  zeus21 1578422272 109    61.3  zeus04 1548058624 102    56.4  zeus05 1662844928 18.0  9.70 613376000 zeus12 16.7  8.85 zeus01 579948544 43.3  22.2  zeus13 868937728 901    893    734007296 zeus05 901    893    zeus04 718393344 211    201    zeus18 714145792 265    259    zeus15 548233216
array-simplified-benchmarks/arrays-size-10/10_standard_init4_true-unreach-call_ground.i 10.3  6.19 347480064 zeus12 10.3  6.16 zeus07 339013632 29.4  21.2  608870400 zeus04 112    63.3  2214535168 zeus17 111    63.6  zeus15 1810583552 118    66.1  zeus06 1700376576 109    62.7  zeus11 1936629760 19.2  10.3  638357504 zeus15 19.9  10.6  zeus11 684466176 50.3  25.7  zeus13 876380160 901    893    667639808 zeus04 901    892    zeus11 726568960 229    220    zeus19 692203520 375    366    zeus13 630730752
array-simplified-benchmarks/arrays-size-10/10_standard_init5_true-unreach-call_ground.i 14.1  8.37 422682624 zeus20 12.1  7.37 zeus06 393277440 33.0  24.1  679088128 zeus09 123    70.2  1784307712 zeus19 126    72.0  zeus24 1717923840 122    68.4  zeus14 1886703616 128    75.4  zeus16 2311798784 25.2  13.2  649318400 zeus21 26.2  13.8  zeus13 758710272 57.6  29.4  zeus12 889212928 901    893    679968768 zeus14 901    893    zeus02 676139008 236    227    zeus10 701984768 434    425    zeus07 668119040
array-simplified-benchmarks/arrays-size-10/10_standard_init6_true-unreach-call_ground.i 15.0  9.17 489275392 zeus06 17.5  11.3  zeus09 462307328 41.5  30.6  776146944 zeus13 127    72.4  1979023360 zeus22 123    70.6  zeus21 1923776512 125    71.0  zeus08 1676156928 141    87.7  zeus07 2487660544 32.9  17.1  737083392 zeus10 32.2  16.8  zeus06 852725760 54.8  28.1  zeus04 898826240 901    891    705568768 zeus11 901    891    zeus10 710062080 258    248    zeus05 706957312 526    516    zeus08 698933248
array-simplified-benchmarks/arrays-size-10/10_standard_init7_true-unreach-call_ground.i 21.4  12.7  681078784 zeus09 19.1  11.7  zeus13 592343040 59.9  47.4  719884288 zeus08 138    78.7  1806508032 zeus13 134    77.0  zeus18 1977724928 134    77.1  zeus03 1876844544 180    117    zeus09 3187728384 36.8  19.0  875270144 zeus06 35.9  18.5  zeus01 838909952 56.8  29.2  zeus02 958869504 901    891    728686592 zeus21 901    891    zeus18 733425664 265    255    zeus19 752275456 619    609    zeus20 713101312
array-simplified-benchmarks/arrays-size-10/10_standard_init8_true-unreach-call_ground.i 24.5  15.0  689209344 zeus08 23.1  14.2  zeus02 681299968 65.3  52.9  740470784 zeus22 141    82.0  1843728384 zeus08 136    78.6  zeus04 1907601408 129    74.7  zeus23 1915039744 188    125    zeus07 3436711936 38.0  19.8  906272768 zeus02 42.8  22.1  zeus19 905650176 58.3  30.1  zeus22 963219456 901    891    695005184 zeus08 901    891    zeus22 701411328 333    322    zeus01 767029248 706    696    zeus22 735395840
array-simplified-benchmarks/arrays-size-10/10_standard_init9_true-unreach-call_ground.i 25.3  16.1  707440640 zeus05 24.5  15.6  zeus21 737460224 76.2  62.7  821944320 zeus03 143    82.3  2151550976 zeus01 143    83.0  zeus21 1991561216 137    79.3  zeus03 2304311296 200    138    zeus01 4257341440 39.5  20.5  894488576 zeus21 38.6  20.0  zeus09 875425792 59.9  31.3  zeus05 1085935616 901    891    726048768 zeus13 901    891    zeus09 703782912 320    309    zeus03 764690432 792    779    zeus10 803196928
array-simplified-benchmarks/arrays-size-10/10_standard_maxInArray_true-unreach-call_ground.i 902    893    761364480 zeus17 902    893    zeus02 746135552 902    892    2364669952 zeus03 163    102    2662871040 zeus14 175    110    zeus06 2738544640 140    85.0  zeus11 2392203264 112    61.1  zeus20 1997975552 901    789    8147628032 zeus20 901    790    zeus14 7672659968 901    779    zeus22 9164451840