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.ArraysReach MathSAT5-oldarray.ArraysReach MathSAT5-uf.ArraysReach PRINCESS-heaparray-quantifiers.ArraysReach PRINCESS-heaparray.ArraysReach PRINCESS-oldarray.ArraysReach PRINCESS-uf.ArraysReach SMTInterpol-heaparray.ArraysReach SMTInterpol-oldarray.ArraysReach SMTInterpol-uf.ArraysReach Z3-heaparray-quantifiers.ArraysReach Z3-heaparray.ArraysReach Z3-oldarray.ArraysReach Z3-uf.ArraysReach
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/benchmarks/ 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
test/programs/benchmarks/ 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
total tasks 118 84400   82300   384732033024 118 83700   81700    328579366912 118 19600   19100   96259244032 118 104000   93000   584804958208 118 104000   93200   584922939392 118 102000 90200 614682218496 118 25100 20900 201770909696 118 81200 75700 478694166528 118 103000   95900    605543464960 118 17300 15200   157984497664 118 28200 27500 96071409664 118 28200 27600 96033193984 118 101000   99700    95430283264 118 25000 24500 40508424192
    correct results 2 18.0 11.3 1179455488 3 15.2 8.81 700305408 5 217   161   3635933184 2 28.1 15.4 1257787392 2 25.5 14.2 1227628544 4 576 429 8093585408 2 453 308 7054086144 3 855 834 5052174336 3 12.1 7.21 647626752 7 660 460   14207205376 4 325 309 2374766592 4 384 369 2381615104 3 11.8 7.02 631115776 1 700 693 429907968
        correct true 2 18.0 11.3 1179455488 3 15.2 8.81 700305408 1 67.7 60.0 746414080 2 28.1 15.4 1257787392 2 25.5 14.2 1227628544 4 576 429 8093585408 2 453 308 7054086144 3 855 834 5052174336 3 12.1 7.21 647626752 1 130 98.2 3608158208 4 325 309 2374766592 4 384 369 2381615104 3 11.8 7.02 631115776 0
        correct false 0 0 4 149   101   2889519104 0 0 0 0 0 0 6 529 362   10599047168 0 0 0 1 700 693 429907968
    incorrect results 0 0 5 1170   1030   11903131648 0 0 1 197 132 3799191552 0 0 0 8 1740 1380   31715106816 0 0 0 4 1800 1700 3627114496
        incorrect true 0 0 0 0 0 1 197 132 3799191552 0 0 0 0 0 0 0 0
        incorrect false 0 0 5 1170   1030   11903131648 0 0 0 0 0 0 8 1740 1380   31715106816 0 0 0 4 1800 1700 3627114496
score (118 tasks, max score: 202) 4 6 -74 4 4 -24 4 6 6 -120 8 8 6 -63
Run set MathSAT5-heaparray.ArraysReach MathSAT5-oldarray.ArraysReach MathSAT5-uf.ArraysReach PRINCESS-heaparray-quantifiers.ArraysReach PRINCESS-heaparray.ArraysReach PRINCESS-oldarray.ArraysReach PRINCESS-uf.ArraysReach SMTInterpol-heaparray.ArraysReach SMTInterpol-oldarray.ArraysReach SMTInterpol-uf.ArraysReach Z3-heaparray-quantifiers.ArraysReach Z3-heaparray.ArraysReach Z3-oldarray.ArraysReach Z3-uf.ArraysReach