From d544b045d428dcf5f8a6f2909a5a8c244b96fb80 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 10 Jan 2024 11:53:23 -0800 Subject: [PATCH 01/17] Implement :resource_limit --- Source/DafnyCore/Options/BoogieOptionBag.cs | 4 ++-- .../Verifier/BoogieGenerator.ExpressionTranslator.cs | 5 +++++ .../TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy | 2 +- .../TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy | 2 +- .../LitTests/LitTest/git-issues/git-issue-3855.dfy | 2 +- .../LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy | 2 +- docs/DafnyRef/Attributes.md | 9 ++++++--- 7 files changed, 17 insertions(+), 9 deletions(-) diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index 675cea0ea44..324e81d2083 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -63,7 +63,7 @@ public static class BoogieOptionBag { new("--error-limit", () => 5, "Set the maximum number of errors to report (0 for unlimited)."); public static readonly Option SolverResourceLimit = new("--resource-limit", - @"Specify the maximum resource limit (rlimit) value to pass to Z3. A resource limit is a deterministic alternative to a time limit. The output produced by `--log-format csv` includes the resource use of each proof effort, which you can use to determine an appropriate limit for your program. Multiplied by 1000 before sending to Z3."); + @"Specify the maximum resource limit (rlimit) value to pass to Z3. A resource limit is a deterministic alternative to a time limit. The output produced by `--log-format csv` includes the resource use of each proof effort, which you can use to determine an appropriate limit for your program."); public static readonly Option SolverPlugin = new("--solver-plugin", @"Dafny uses Boogie as part of its verification process. This option allows customising that part using a Boogie plugin. More information about Boogie can be found at https://github.com/boogie-org/boogie. Information on how to construct Boogie plugins can be found by looking at the code in https://github.com/boogie-org/boogie/blob/v2.16.3/Source/Provers/SMTLib/ProverUtil.cs#L316"); @@ -120,7 +120,7 @@ static BoogieOptionBag() { o.TheProverFactory = ProverFactory.Load(o.ProverDllName); } }); - DafnyOptions.RegisterLegacyBinding(SolverResourceLimit, (o, v) => o.ResourceLimit = Boogie.Util.BoundedMultiply(v, 1000)); + DafnyOptions.RegisterLegacyBinding(SolverResourceLimit, (o, v) => o.ResourceLimit = v); DafnyOptions.RegisterLegacyBinding(SolverLog, (o, v) => o.ProverLogFilePath = v); DafnyOptions.RegisterLegacyBinding(SolverOption, (o, v) => { if (v is not null) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index c4b4a0acbb5..388932e2662 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -1959,6 +1959,11 @@ public Boogie.QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) BigNum.FromUInt(Boogie.Util.BoundedMultiply((uint)litExpr.asBigNum.ToIntSafe, 1000)), litExpr.Immutable); } + + // Do this after the above multiplication because :resource_limit should not be multiplied. + if (name == "resource_limit") { + name = "rlimit"; + } kv = new Boogie.QKeyValue(Token.NoToken, name, parms, kv); } return kv; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy index c433efd53b2..043e461374f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy @@ -136,7 +136,7 @@ class Map { } // Removes key from the domain of M (and does nothing if key wasn't in M to begin with) - method {:rlimit 3000} {:vcs_split_on_every_assert} Remove(key: Key) + method {:resource_limit 3000000} {:vcs_split_on_every_assert} Remove(key: Key) requires Valid() modifies Repr ensures Valid() && fresh(Repr - old(Repr)) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy index d161585df1b..3855d710829 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy @@ -3,7 +3,7 @@ ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)} -lemma{:rlimit 10000} L() +lemma{:resource_limit 10000000} L() { assert f(10, 5) == 0; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy index dec9da7cfad..3d9a59a6d5c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy @@ -637,7 +637,7 @@ function partitionOfJustHeapRegions(os : set) : (partition : map // witness. The method could equally well have been written using an // existential quantifier and no ghost out-parameter. method - {:rlimit 8000} + {:resource_limit 8000000} {:vcs_split_on_every_assert} BFS(source: Vertex, dest: Vertex, ghost AllVertices: set) returns (d: int, ghost path: List) diff --git a/docs/DafnyRef/Attributes.md b/docs/DafnyRef/Attributes.md index 47ce6ac457f..0310d2cc6e6 100644 --- a/docs/DafnyRef/Attributes.md +++ b/docs/DafnyRef/Attributes.md @@ -393,12 +393,15 @@ Print effects are enforced only with `--track-print-effects`. `{:priority N}` assigns a positive priority 'N' to a method or function to control the order in which methods or functions are verified (default: N = 1). -### 11.2.14. `{:rlimit}` {#sec-rlimit} +### 11.2.14. `{:resource_limit}` and `{:rlimit}` {#sec-rlimit} -`{:rlimit N}` limits the verifier resource usage to verify the method or function at `N * 1000`. -This is the per-method equivalent of the command-line flag `/rlimit:N`. +`{:resource_limit N}` limits the verifier resource usage to verify the method or function to `N`. + +This is the per-method equivalent of the command-line flag `/rlimit:N` or `--resource-limit N`. If using [`{:vcs_split_on_every_assert}`](#sec-vcs_split_on_every_assert) as well, the limit will be set for each assertion. +The attribute `{:rlimit N}` is also available, and limits the verifier resource usage to verify the method or function to `N * 1000`. This version is deprecated, however. + To give orders of magnitude about resource usage, here is a list of examples indicating how many resources are used to verify each method: * 8K resource usage From d3daf43b707ac1f451baa58802df0620be358c61 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 11 Jan 2024 11:54:28 -0800 Subject: [PATCH 02/17] Use non-multiplied resource limit for Std --- Source/DafnyStandardLibraries/src/Std/dfyconfig.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml b/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml index 2b40b5ef8fb..afc4a115a7a 100644 --- a/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml +++ b/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml @@ -12,7 +12,7 @@ reads-clauses-on-methods = true # Options important for sustainable development # of the libraries themselves. -resource-limit = 1000 +resource-limit = 1000000 warn-as-errors = true # These give too many false positives right now, but should be enabled in the future warn-redundant-assumptions = false From 728d501fe7a9013b70be950f7d72a7a3550794c4 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 11 Jan 2024 11:56:48 -0800 Subject: [PATCH 03/17] Use :resource_limit in DafnyLanguageServer.Test --- .../DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs | 4 ++-- .../SimpleLinearVerificationGutterStatusTester.cs | 2 +- .../DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs index 094695d5afb..3a00d293a66 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs @@ -27,7 +27,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest { public class DafnyLanguageServerTestBase : LanguageProtocolTestBase { protected readonly string SlowToVerify = @" -lemma {:rlimit 100} SquareRoot2NotRational(p: nat, q: nat) +lemma {:resource_limit 100000} SquareRoot2NotRational(p: nat, q: nat) requires p > 0 && q > 0 ensures (p * p) != 2 * (q * q) { @@ -42,7 +42,7 @@ requires p > 0 && q > 0 } }".TrimStart(); - protected string SlowToVerifyNoLimit => SlowToVerify.Replace(" {:rlimit 100}", ""); + protected string SlowToVerifyNoLimit => SlowToVerify.Replace(" {:resource_limit 100000}", ""); protected readonly string NeverVerifies = @" lemma {:neverVerify} HasNeverVerifyAttribute(p: nat, q: nat) diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs index 0adac6007db..5f54eeb8e2e 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs @@ -70,7 +70,7 @@ await VerifyTrace(@" | : if n <= 1 then n else fib(n-1) + fib(n-2) | :} | : -[ ]:method {:rlimit 1} Test(s: seq) +[ ]:method {:resource_limit 1000} Test(s: seq) [=]: requires |s| >= 1 && s[0] >= 0 { assert fib(10) == 1; assert {:split_here} s[0] >= 0; [ ]:}", true, intermediates: false); } diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index 521a0bdf2de..a82833e9df5 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -488,7 +488,7 @@ public async Task IndicateClickableWarningSignsOnMethodHoverWhenResourceLimitRea var documentItem = await GetDocumentItem(@" ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)} -lemma{:rlimit 10000} L() +lemma{:resource_limit 10000000} L() { assert f(10, 5) == 0; } ", "testfileSlow.dfy", true); From a9687db8447f803924d99e889a4bb271938eecc4 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 11 Jan 2024 14:29:23 -0800 Subject: [PATCH 04/17] Update Std to use `:resource_limit` everywhere --- .../binaries/DafnyStandardLibraries-cs.doo | Bin 1340 -> 1340 bytes .../binaries/DafnyStandardLibraries-go.doo | Bin 1360 -> 1360 bytes .../binaries/DafnyStandardLibraries-java.doo | Bin 1321 -> 1321 bytes .../binaries/DafnyStandardLibraries-js.doo | Bin 1867 -> 1867 bytes .../DafnyStandardLibraries-notarget.doo | Bin 1314 -> 1314 bytes .../binaries/DafnyStandardLibraries-py.doo | Bin 1331 -> 1331 bytes .../examples/FileIO/WriteBytesToFile.dfy | 2 +- .../examples/JSON/JSONExamples.dfy | 6 +++--- .../Std/Arithmetic/Internal/ModInternals.dfy | 2 +- .../DafnyStandardLibraries/src/Std/Base64.dfy | 6 +++--- .../src/Std/Collections/Seq.dfy | 2 +- .../JSON/ConcreteSyntax.SpecProperties.dfy | 4 ++-- .../src/Std/JSON/Serializer.dfy | 4 ++-- .../src/Std/JSON/ZeroCopy/Deserializer.dfy | 18 +++++++++--------- .../src/Std/JSON/ZeroCopy/Serializer.dfy | 6 +++--- .../src/Std/TargetSpecific/dfyconfig.toml | 2 +- .../src/Std/Unicode/Utf16EncodingForm.dfy | 2 +- .../src/Std/Unicode/Utf8EncodingForm.dfy | 4 ++-- .../src/Std/Unicode/Utf8EncodingScheme.dfy | 2 +- 19 files changed, 30 insertions(+), 30 deletions(-) diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index 289bb463082c11873669bdb1817f8801e62797da..36be3acd176ea62f377a8b47d6e9389b7fe75278 100644 GIT binary patch delta 49 vcmdnPwTFu@z?+#xgn@y9gW+;eFk|vD7IO%Lk<}UiVTcb& diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo index b0c70f357426f92454ed6b36e3fde76b25e97aae..794dd1aeda72f159d83b5ee9c903dbffc5def9d6 100644 GIT binary patch delta 49 vcmcb>b%Bd7z?+#xgn@y9gW*P=cEm)!^DH2Gb%Bd7z?+#xgn@y9gTb$~KYSwJc@_}8@!?lyFk|v97IO$gl+_vlY{L(^ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index 45727f4816a11b92b0eacf5580e2e1a6c64f4604..707a6bc26968f0e8487028dca1e2501430f2de7f 100644 GIT binary patch delta 49 vcmZ3gUFk|v&7IO&W9g8&pTOtqb diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo index 8510c9484f638ab9e5991aefc55ddae568ac8b9b..023c86b43c1caa65462efb9f87ab293d77cc41e9 100644 GIT binary patch delta 49 vcmX@jcbbncz?+#xgn@y9gW+19cEm)!^DH2G7IO&WIg2#_R^t!C diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo index 4b61fef7812d22895f2b95fc0dc7dd6013b01a0e..7a0599cbec11488c8cdf43ebc6ffb5fb885f1c59 100644 GIT binary patch delta 49 vcmdnYwV8`Az?+#xgn@y9gW+bLcEm)!^DH2G 0 ensures ModAutoMinus(n) { diff --git a/Source/DafnyStandardLibraries/src/Std/Base64.dfy b/Source/DafnyStandardLibraries/src/Std/Base64.dfy index cefb455de69..02bd16eaa06 100644 --- a/Source/DafnyStandardLibraries/src/Std/Base64.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Base64.dfy @@ -98,7 +98,7 @@ module Std.Base64 { else (c - 65 as char) as index } - lemma {:rlimit 2000} {:vcs_split_on_every_assert} CharToIndexToChar(c: char) + lemma {:resource_limit 2000000} {:vcs_split_on_every_assert} CharToIndexToChar(c: char) requires IsBase64Char(c) ensures IndexToChar(CharToIndex(c)) == c { @@ -1213,7 +1213,7 @@ module Std.Base64 { AboutDecodeValid(s, DecodeValid(s)); } - lemma {:rlimit 12000} DecodeValidEncode1Padding(s: seq) + lemma {:resource_limit 12000000} DecodeValidEncode1Padding(s: seq) requires IsBase64String(s) requires |s| >= 4 requires Is1Padding(s[(|s| - 4)..]) @@ -1449,7 +1449,7 @@ module Std.Base64 { seq(|b|, i requires 0 <= i < |b| => b[i] as uint8) } - lemma {:vcs_split_on_every_assert} {:rlimit 1000000} UInt8sToBVsToUInt8s(u: seq) + lemma {:vcs_split_on_every_assert} {:resource_limit 1000000000} UInt8sToBVsToUInt8s(u: seq) ensures BVsToUInt8s(UInt8sToBVs(u)) == u { // TODO: reduce resource use diff --git a/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy b/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy index e4ef670e50d..65358c44dc7 100644 --- a/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy @@ -749,7 +749,7 @@ module Std.Collections.Seq { /* Applying a function to a sequence is distributive over concatenation. That is, concatenating two sequences and then applying Map is the same as applying Map to each sequence separately, and then concatenating the two resulting sequences. */ - lemma {:opaque} {:rlimit 1000000} LemmaMapDistributesOverConcat(f: (T ~> R), xs: seq, ys: seq) + lemma {:opaque} {:resource_limit 1000000000} LemmaMapDistributesOverConcat(f: (T ~> R), xs: seq, ys: seq) requires forall i {:trigger xs[i]}:: 0 <= i < |xs| ==> f.requires(xs[i]) requires forall j {:trigger ys[j]}:: 0 <= j < |ys| ==> f.requires(ys[j]) ensures Map(f, xs + ys) == Map(f, xs) + Map(f, ys) diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/ConcreteSyntax.SpecProperties.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/ConcreteSyntax.SpecProperties.dfy index e5788fa0d01..6aed16f9d0a 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/ConcreteSyntax.SpecProperties.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/ConcreteSyntax.SpecProperties.dfy @@ -36,7 +36,7 @@ module Std.JSON.ConcreteSyntax.SpecProperties { ensures Spec.ConcatBytes(ts, pt0) == Spec.ConcatBytes(ts, pt1) {} - lemma {:induction ts0} {:rlimit 10000} ConcatBytes_Linear(ts0: seq, ts1: seq, pt: T --> bytes) + lemma {:induction ts0} {:resource_limit 10000000} ConcatBytes_Linear(ts0: seq, ts1: seq, pt: T --> bytes) requires forall d | d in ts0 :: pt.requires(d) requires forall d | d in ts1 :: pt.requires(d) ensures Spec.ConcatBytes(ts0 + ts1, pt) == Spec.ConcatBytes(ts0, pt) + Spec.ConcatBytes(ts1, pt) @@ -47,4 +47,4 @@ module Std.JSON.ConcreteSyntax.SpecProperties { assert ts0 + ts1 == [ts0[0]] + (ts0[1..] + ts1); } } -} \ No newline at end of file +} diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/Serializer.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/Serializer.dfy index 852ba6d6d83..cad694e4b58 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/Serializer.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/Serializer.dfy @@ -64,7 +64,7 @@ module Std.JSON.Serializer { Failure(o.error) } - function {:vcs_split_on_every_assert} {:rlimit 1000} Number(dec: Values.Decimal): Result { + function {:vcs_split_on_every_assert} {:resource_limit 1000000} Number(dec: Values.Decimal): Result { var minus: jminus := Sign(dec.n); var num: jnum :- Int(Math.Abs(dec.n)); var frac: Maybe := Empty(); @@ -133,4 +133,4 @@ module Std.JSON.Serializer { var val :- Value(js); Success(MkStructural(val)) } -} \ No newline at end of file +} diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy index bde25681af1..53ed407f6f6 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy @@ -59,7 +59,7 @@ module Std.JSON.ZeroCopy.Deserializer { return Cursor(cs.s, cs.beg, point', cs.end).Split(); } - opaque function {:vcs_split_on_every_assert} {:rlimit 1000000} Structural(cs: FreshCursor, parser: Parser) + opaque function {:vcs_split_on_every_assert} {:resource_limit 1000000000} Structural(cs: FreshCursor, parser: Parser) : (pr: ParseResult>) requires forall cs :: parser.fn.requires(cs) ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, st => Spec.Structural(st, parser.spec)) @@ -72,7 +72,7 @@ module Std.JSON.ZeroCopy.Deserializer { type jopt = v: Vs.View | v.Length() <= 1 witness Vs.View.OfBytes([]) - function {:rlimit 100000} TryStructural(cs: FreshCursor) + function {:resource_limit 100000000} TryStructural(cs: FreshCursor) : (sp: Split>) ensures sp.SplitFrom?(cs, st => Spec.Structural(st, SpecView)) { @@ -244,7 +244,7 @@ module Std.JSON.ZeroCopy.Deserializer { elems' } - opaque function {:rlimit 10000} {:vcs_split_on_every_assert} AppendLast(ghost cs0: FreshCursor, + opaque function {:resource_limit 10000000} {:vcs_split_on_every_assert} AppendLast(ghost cs0: FreshCursor, ghost json: ValueParser, elems: Split>, elem: Split, @@ -280,7 +280,7 @@ module Std.JSON.ZeroCopy.Deserializer { elems' } - lemma {:rlimit 10000} AboutTryStructural(cs: FreshCursor) + lemma {:resource_limit 10000000} AboutTryStructural(cs: FreshCursor) ensures var sp := Core.TryStructural(cs); var s0 := sp.t.t.Peek(); @@ -476,7 +476,7 @@ module Std.JSON.ZeroCopy.Deserializer { case OtherError(err) => err } - opaque function {:vcs_split_on_every_assert} {:rlimit 10000} JSON(cs: Cursors.FreshCursor) : (pr: DeserializationResult>) + opaque function {:vcs_split_on_every_assert} {:resource_limit 10000000} JSON(cs: Cursors.FreshCursor) : (pr: DeserializationResult>) ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, Spec.JSON) { Core.Structural(cs, Parsers.Parser(Values.Value, Spec.Value)).MapFailure(LiftCursorError) @@ -694,7 +694,7 @@ module Std.JSON.ZeroCopy.Deserializer { Success(cs.Split()) } - opaque function {:rlimit 10000} String(cs: FreshCursor): (pr: ParseResult) + opaque function {:resource_limit 10000000} String(cs: FreshCursor): (pr: ParseResult) ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, Spec.String) { var SP(lq, cs) :- Quote(cs); @@ -755,7 +755,7 @@ module Std.JSON.ZeroCopy.Deserializer { else Success(sp) } - opaque function {:vcs_split_on_every_assert} {:rlimit 100000} Exp(cs: FreshCursor) : (pr: ParseResult>) + opaque function {:vcs_split_on_every_assert} {:resource_limit 100000000} Exp(cs: FreshCursor) : (pr: ParseResult>) ensures pr.Success? ==> pr.value.SplitFrom?(cs, exp => Spec.Maybe(exp, Spec.Exp)) { var SP(e, cs) := @@ -974,7 +974,7 @@ module Std.JSON.ZeroCopy.Deserializer { } } - opaque function {:vcs_split_on_every_assert} {:rlimit 10000} Object(cs: FreshCursor, json: ValueParser) + opaque function {:vcs_split_on_every_assert} {:resource_limit 10000000} Object(cs: FreshCursor, json: ValueParser) : (pr: ParseResult) requires cs.SplitFrom?(json.cs) ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, Spec.Object) @@ -985,4 +985,4 @@ module Std.JSON.ZeroCopy.Deserializer { Success(sp) } } -} \ No newline at end of file +} diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy index ef153a9a698..044b8e64a0e 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy @@ -155,7 +155,7 @@ module Std.JSON.ZeroCopy.Serializer { ensures Spec.Number(num) == num.minus.Bytes() + num.num.Bytes() + Spec.Maybe(num.frac, Spec.Frac) + Spec.Maybe(num.exp, Spec.Exp) {} - lemma {:vcs_split_on_every_assert} {:rlimit 10000} NumberHelper2(num: jnumber, writer: Writer) + lemma {:vcs_split_on_every_assert} {:resource_limit 10000000} NumberHelper2(num: jnumber, writer: Writer) ensures if num.exp.NonEmpty? then ( if num.frac.NonEmpty? then writer.Bytes() + Spec.Number(num) == writer.Bytes() + num.minus.Bytes() + num.num.Bytes() + num.frac.t.period.Bytes() + num.frac.t.num.Bytes() + num.exp.t.e.Bytes() + num.exp.t.sign.Bytes() + num.exp.t.num.Bytes() else writer.Bytes() + Spec.Number(num) == writer.Bytes() + num.minus.Bytes() + num.num.Bytes() + num.exp.t.e.Bytes() + num.exp.t.sign.Bytes() + num.exp.t.num.Bytes() @@ -468,7 +468,7 @@ module Std.JSON.ZeroCopy.Serializer { // needs to call ItemsSpec and the termination checker gets confused by // that. Instead, see Items above. // DISCUSS - method {:rlimit 10000} MembersImpl(obj: jobject, writer: Writer) returns (wr: Writer) + method {:resource_limit 10000000} MembersImpl(obj: jobject, writer: Writer) returns (wr: Writer) decreases obj, 1 ensures wr == MembersSpec(obj, obj.data, writer) { @@ -547,4 +547,4 @@ module Std.JSON.ZeroCopy.Serializer { } wr } -} \ No newline at end of file +} diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml index 07ec5a99d80..d48d60ce73e 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml @@ -12,7 +12,7 @@ reads-clauses-on-methods = true # Options important for sustainable development # of the libraries themselves. -resource-limit = 1000 +resource-limit = 1000000 warn-as-errors = true warn-redundant-assumptions = true warn-contradictory-assumptions = true diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy index 9892385703b..e8679c68069 100644 --- a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy @@ -115,7 +115,7 @@ module Std.Unicode.Utf16EncodingForm refines UnicodeEncodingForm { } function - {:rlimit 1200} + {:resource_limit 1200000} DecodeMinimalWellFormedCodeUnitSubsequenceDoubleWord(m: MinimalWellFormedCodeUnitSeq): (v: ScalarValue) requires |m| == 2 ensures 0x10000 <= v <= 0x10FFFF diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy index 795994d89cb..98f73258179 100644 --- a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy @@ -214,7 +214,7 @@ module Std.Unicode.Utf8EncodingForm refines UnicodeEncodingForm { } function - {:rlimit 115000} + {:resource_limit 115000000} DecodeMinimalWellFormedCodeUnitSubsequenceTripleByte(m: MinimalWellFormedCodeUnitSeq): (v: ScalarValue) requires |m| == 3 ensures 0x800 <= v <= 0xFFFF @@ -231,7 +231,7 @@ module Std.Unicode.Utf8EncodingForm refines UnicodeEncodingForm { } function - {:rlimit 4000} + {:resource_limit 4000000} DecodeMinimalWellFormedCodeUnitSubsequenceQuadrupleByte(m: MinimalWellFormedCodeUnitSeq): (v: ScalarValue) requires |m| == 4 ensures 0x10000 <= v <= 0x10FFFF diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingScheme.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingScheme.dfy index eee8c8c433e..5aa4a6a3a1f 100644 --- a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingScheme.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingScheme.dfy @@ -54,7 +54,7 @@ module Std.Unicode.Utf8EncodingScheme { * Deserializing a byte sequence and then serializing the result, yields the original byte sequence. */ lemma - {:rlimit 3000} + {:resource_limit 3000000} LemmaDeserializeSerialize(b: seq) ensures Serialize(Deserialize(b)) == b { From e3637ef20c36d0555c7bcd2668b75deb2a792e49 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 12 Jan 2024 09:15:23 -0800 Subject: [PATCH 05/17] Fix `--resource-limit` flags in tests --- .../TestFiles/LitTests/LitTest/cli/solverLog.dfy | 2 +- .../TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy | 2 +- .../LitTests/LitTest/dafny4/git-issue106.dfy.expect | 2 +- .../LitTests/LitTest/git-issues/github-issue-4804.dfy | 2 +- .../LitTests/LitTest/verification/nonLinearArithmetic.dfy | 6 +++--- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy index 4686b97830f..b4d0e365b4d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy @@ -1,4 +1,4 @@ -// RUN: %verify --solver-log="log.smt2" --resource-limit 10 "%s" > "%t" +// RUN: %verify --solver-log="log.smt2" --resource-limit 10000 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // RUN: %OutputCheck --file-to-check "log.smt2" "%s" // CHECK: rlimit 10000 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy index 98b2f8bf292..66bedb5b517 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy @@ -1,4 +1,4 @@ -// RUN: %verify "%s" --resource-limit 10000 > "%t" +// RUN: %verify "%s" --resource-limit 10000000 > "%t" // RUN: %diff "%s.expect" "%t" ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect index 757646ed6c3..2985385d3ec 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect @@ -1,3 +1,3 @@ -git-issue106.dfy(6,21): Verification out of resource (L (correctness)) +git-issue106.dfy(6,32): Verification out of resource (L (correctness)) Dafny program verifier finished with 1 verified, 0 errors, 1 out of resource diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy index b3b0167d5e3..29b6ac4cc73 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %verify --resource-limit 1000 %s > %t +// RUN: %exits-with 4 %verify --resource-limit 1000000 %s > %t // RUN: %diff "%s.expect" "%t" module Power { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy index eae991a3240..1d7b1c0939b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy @@ -1,5 +1,5 @@ -// RUN: ! %verify "%s" --disable-nonlinear-arithmetic --resource-limit 1000 > "%t" -// RUN: ! %verify "%s" --resource-limit 1000 >> "%t" +// RUN: ! %verify "%s" --disable-nonlinear-arithmetic --resource-limit 1000000 > "%t" +// RUN: ! %verify "%s" --resource-limit 1000000 >> "%t" // RUN: %diff "%s.expect" "%t" module Power0 { @@ -102,4 +102,4 @@ module {:disableNonlinearArithmetic false} Power3 { LemmaPowAdds(b, e1 - e2, e2); } -} \ No newline at end of file +} From c2e5a21739758176d9a4f7c114ac1800d521ffc3 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 12 Jan 2024 09:15:37 -0800 Subject: [PATCH 06/17] Rebuild standard libraries --- .../binaries/DafnyStandardLibraries-cs.doo | Bin 1340 -> 1340 bytes .../binaries/DafnyStandardLibraries-go.doo | Bin 1360 -> 1360 bytes .../binaries/DafnyStandardLibraries-java.doo | Bin 1321 -> 1321 bytes .../binaries/DafnyStandardLibraries-js.doo | Bin 1867 -> 1867 bytes .../DafnyStandardLibraries-notarget.doo | Bin 1314 -> 1314 bytes .../binaries/DafnyStandardLibraries-py.doo | Bin 1331 -> 1331 bytes .../binaries/DafnyStandardLibraries.doo | Bin 56937 -> 56961 bytes 7 files changed, 0 insertions(+), 0 deletions(-) diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index 36be3acd176ea62f377a8b47d6e9389b7fe75278..2404ac2ac0a44c57cc27b50a70276856241afcbe 100644 GIT binary patch delta 44 ucmdnPwTFv0z?+#xgn@y9gJG+i&P3h|%s^`6gGbCDdh$^g3lKet)dm0(4-H5F delta 44 ucmdnPwTFv0z?+#xgn@y9gW+b%BdFz?+#xgn@y9gJGAO&P3h|%s^`6gKx|rdh$&c3otFhY6Ac%@eRQM delta 45 ucmcb>b%BdFz?+#xgn@y9gW*P=_C($b%s^`6gKx|rdh$&c3otFhY6Ad0kPg)V diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index 707a6bc26968f0e8487028dca1e2501430f2de7f..146b93f3b514d068dccba06b1f724499df7194c7 100644 GIT binary patch delta 45 ucmZ3;g diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo index 023c86b43c1caa65462efb9f87ab293d77cc41e9..1605b478099510494d9702920ed5d3ab30114f1f 100644 GIT binary patch delta 45 ucmX@jcbbnkz?+#xgn@y9gJFl8&P3h|%s^`6gO98rdh!)E3oy;kZUX=)l?|={ delta 45 ucmX@jcbbnkz?+#xgn@y9gW+19_C($b%s^`6gO98rdh!)E3oy;kZUX>3G!DW5 diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo index 134899ff0ea9190de0a8342fefd310eb7bbc0826..51a0c93b30be50d4f3b2520904af743330f69b6b 100644 GIT binary patch delta 45 ucmZ3)wTO#1z?+#xgn@y9gJH9q&P3h|%s^`6gA>dkdh%)(3o!kR#RdQsQVqTU delta 45 ucmZ3)wTO#1z?+#xgn@y9gW+PH_C($b%s^`6gA>dkdh%)(3o!kR#RdQ<@ea}e diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo index 7a0599cbec11488c8cdf43ebc6ffb5fb885f1c59..8e700da3ca43b6bd6fe2738103ed981df063be0f 100644 GIT binary patch delta 45 ucmdnYwV8`Iz?+#xgn@y9gJHLu&P3h|%s^`6gPY7Cdh#9?3o!ki#RdQ$q7E|v delta 45 ucmdnYwV8`Iz?+#xgn@y9gW+bL_C($b%s^`6gPY7Cdh#9?3o!ki#RdQ~K@Ud& diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index aba9385db4265d5a2fead18aec14a674db4fec4c..d0a35f0b26c0c5100e216c638aa4a345c1d59131 100644 GIT binary patch delta 47832 zcmV(;K-<6RyaR!~0}fD20|XQR000O8vPLXekq*xevPLXem9lo;1Kj`s4tufd2q1sQ z#+oi?gYuUVztFnqw&DM7sLr(zr;Cz8*r#rFNZsvIOAp8x=(kV_6SnZtR-ai&FcU+5 z%N^{>l!E6h*wC3m?qZamUulod2U)X0)-cFg46@D`WK9gRh9hrkkhLC!Z*j~xxigXJ zb(R{z`H>$%%D?Kx1jR>?dqpw!Jey_Tkd85M=duf*!z#lZeOrR9egKK6}6AlZ&U17yPSWI9L+7~ zwGArg6vN0MumShlf4>2tOLv;UX2WE;8%+|h@e5AID;zqy5_>YA3-*N zzpZ1$SYYUTBaP^M$3Iu*Jc)bTPNEvCQ?D9JgFB_bwG_D8lhAFHXLZu$S<8`Fgq8E0 z3v1jDAOPCp^8@m}m%z44{GgKu!M_F3XhT)VZ@g6E{Op6!wt?#UW;uTtl=Jy?R+B??QidVNcc}*8tjbfVMoKE#e|IBc|B;H@tflLfqMRqER8_;q57`;gA}Y zfTvrwI&rb-UU{lX+@+*e(Z_^9iZh5(DDXo=>cqkBDIW26y3-a zl5C73N4jC$>@3Aa2Y-J8o*5{ zH+r-yv8*v%iyW>+4A%+_*UB8OMN-$IsB8JdwKf{gqpn3!*YcU!BA7|c(2>t{HZHne zDPsqfN~&kwhIfk9+x%FX4>t*QZRAf=ayWag3G89ja4HgP%o2a~Ae;IXGe*pW2_H&a zMCbD`G{caNm`qoAABW3HRQ$2OIveC!G|g3miK(T04ypCvq&~4rSZ-#z%8|cJ9{ih2 zzg{-!-%>L+%?jO0QicNKC1v~zh>4SV_D$^Q&P#RQJj@xP)B;=_d&N^eG00-tfv@_? z$_Mp@-!;C6kTQQQ{3V6x)z8j%9nJNr53CTB9K(&#YmBpJjk71_rSMqZmzBs%!B)ga zwAY~zYb*JF{$@lmkPSgtQ(&^mopXAmA3leLWeMGC2BwM`W@ajR1uAMT z{Xc#Iy-a@{;%d&}oxhVHoGo0|0JFnt%Ky*0KAiubh1dytk>Vn5iveonc`vKg4FMg$ z*NPVgE$7#;9-Cr5e@t5{rj=^r?S|(wYjb4`(;Cq|Ymf|bw?T^JwFQv&9(PGQg+!DM zS~R~6`ch2;19BzR4{ZHC$ucD4t3y*}Bmw=V{QRPv zbjW#Chk7cSun(p9=;0V9!Jh0Xg+{oWhj2F+VII!U&pYq5hNmg8*yl|R1lmt8*}`xL zo92JnQ4GWDy#3C|USm(gD9z!C^XUl?de2Sb1&fe|BF^*w*BOF%F_^VA{G(%{NDAH?e{jF`Wea$8s@ zPTe*x0#fX1Zv-JhjGg%85r*z+6w0LqX4Uk1jq&&AS$R>d9Aj%16;<$}F0v4sA2!JI zhYzcFTuJPw)x(GH+z6@4^^?>@ZQC^Lxp&+Vcu z`V`QD0cO21u%3Alw#Hlr*LoQKn5*qO$^hv2`6fk{0lE!o%9z|3I>VmA@w36bk%9bP zm_le0L^~CMdo&oMw1!de63j=i!=W}C;^q8ToKSSkf1MMlU9Z`{UPZ5Vz^CHR^*k|k zqX+9-3zEXqbU1vXqa*P!@DaV_1f_pu`p$ScN;RoeqC%w?m%o zBG8^}3~+3u=8e`rbB7;r;MC(p$PsE-&0-w}oPx8)a7YAG>kfA|5H`S(Y8H4SHMERM znoPv2+i%$F@je%3UG*0{5`{9{A6K%NdIJA)&)gP^H9^R)AF5Gl-IG>LShuP-S@>6| znO7@p5AY{6@r>cVZw!6@VLyLYAo4~ueH)H=j`a~KovVts`^g;IUR>2pag_xKbWv z6M-CwHb9OqJt;kQm0}i6PLk3ozq8P_u8Xogt5nMR$l+_LqW+Z-EB`;9)x|3y{Ej5T!>Qip zu|^yZic{(-7Tm&cG>yz{EUL>z#|&;mOd-3xT-4Kd zt(g;VH~n194eoZj{#<{EwVBSIey_qe_2QggGa~SR$C;|oDZWLf;T@9_tsn(HK~bvt zekS0__3&Cl+`U!@lyJi*fp#yZ?{#25;o>$IFG>SY9nks+ST^U=oq=}ZFz;)`G_M7K z00Oodl6=;04K_O#I)<%YWQYfsfA3tISzA+as!YIJXET)B2xot+*m4XrzF>w$k%j{# z@k?`}X6(g{28%b@SUd?L!Nz|zo$!r{n3<+G;f$_IRfUBjwX|~9k{mhvW+_WYS@#`!ybg2@dRBqBQulWKwy!Mlh}ytTr- z4fKDSFXbI4tdHJ7+|zrl>`w+!G;Of9zcADhxeQJA(5#B#a$nvKj#+_A<-gd3u1t`v zD*#g-yhwQOBtYB5v&v1<(rp%3&Tl>zwE_(%du^e@abYd=n1|ep2SQhZy<8cHayi$% zNF;8n=!_^V^XjWN(kj$9Pq$EqtDsKtCqRD#)+T2%=C9-xo06$^v+!nR?nYvG<#^@! zGZ-QG7#2txL7a2RNyCyu9iRgolZKHsh4O!U z$A8-?RE+q$Ore&q<9H-z(8jR3xbWvi?eLzQIUY~WlDa|5ya($;bEnR?L>kK(l~1S& zlPzY{w6Je!Mny8tpHW+`iihVfp%K0oT=4zlvY0u z6!qp4@W1wi8yClh6K*Rw;qGlQ;bwn}g<&0>hWWq`ihNigW6|mA_9o|+Gym=VktXLL za`}^U4bK&roV^P_UrvXaH<7X-O5)N`rtHO8@#pDiRKm1Bf5@Kr&0b93_uw!-f3;X& zmSS_2b*;>?d-PpOd3Xb=VrNR_0dYa+Q;0AvH{?r5s ztP743xGtZHw#lRNjO{;9=g;TtKgr#FD3_JU0-nXUFp4)VSL(76k>9vM8_E=+5gPSV zLz6X~TIlSO=~CXrt)GgZ_+~2<+4SY%Xc(pL{fyxsV=_uj`f}Tb=I}96f*I&88WK@{ zXTRbQk8crQczV`h2XCEQ#w&BE208fy{(^bj>&gzFB{$8U?B(%vmj1 zL4~gb6!%Fy=omPF932{^!W;t(nDhX{6vvGsAs2zPcRhnS*dev2;f~P6f_FOM&!%K| zL~bQblwGWoWQVP$Bv*J~rV1VZ+M87K4{6LpSk#dQG6r7|_5cn0bu`W-Ps{71nizLTUPgvd zja*J)-}#AeqK?qI$+grZIOJF4}{Yu!07xdJwp{5mX& zWB7Z940nC!IYC9JV@Hn|pffgNM~|4|#4TP#D84EB>cvA3w$keG_}L~KzD+&@zuJZz zh3Q+fM{v-LpRLVzKkBPtT)nV@5_D&P3v$FCz-NN8@01_A-hD5aRY|C;4^{;=sJtOYBrDD7*Xll_+hoDz} z2+I2}RsUts%{%98Z%cHiQsu8~gb0GtLbPF#;yjIs6ALIupuh1g#-0Q8$B$3d^oi+P zlcZ+8Eywy|M1W`^Mr0V}Nl=o1xx6fAvJ_S#^mq8_VEGU8kTO=$$DIJ#i+>O=#4JcW zqh>`7oc({&z+6MeG>g{8@e{4qiXPQEq&J2;X^ly-&7EJHE?vei$QQ71&^*-TH!J(-*5ae-mfEcJyop-bjjS(9 zWMnesWRFH$s?nCPsLsrY8aOr>1SQF;Ed!dhP;M2_D3lsOPKwXy1X!5Jf}@Z}4RC!e z$lrg}+UY3e7MS>o>S|d|oTL^!f1Xahl(Ts$KfK#4qIrQakpmd3RM?ov1Du@^-(<8k zXDl^`i)pR+wL}Y=CuluW1IQB#$Z0Jgr!*!T0(lZ7Cqpn{OQ0o&ECD3b6mpTD8CD5g zTWAuyGa}0o800z#%k#cxp{$0lg3Tgh^GAOxy6%^`So2nm(N)`NT63?osPVd+vt)^u zPW*X#EuI$lCM!8ivb&@^P3E+$wHyh`6ZUCH*p%2dS($Gn^nlF${L5)wnOh<^X^+#e z$U_9(f#5A+S;*Cuy9>#edqC`A@#Q7l@96tl#72oXQfjlr>9GBV$sTN&n7xrW0h@pC zkA&b-dn7TgFB6 zm0@~)nZbFQd{b*#8r2FcJZi{_jlaD;wH$kjW4XCKh2W-S1Wc|ko7?b#HE76INYt?9 zHEan^??ZonGbexNT7T!RZ=(TP&Hyn@a>6uvLOzK!(q6`G z(2wOwU-lX9*~4H$o@OawUJ%#u7S< zi|BSlLzobO^+q;i!J!u0`9eXrQYFQbv&-4uKrm-gGVP>fygRfumyN&iNT42(PHfAt z9hZ;A^Q46SGU?6Mub};O5}jgNItXet;7>jCw{oS?S{e{b4Ppr(g1gEX!41UH@;0Ib z${?vMnralaCg2e}x;Fch;`)DcZ!#!H^H);9w6pV~)>c4D1aAXUaL2u!azYocP0j(d zBHZ=4m1Hpf+|#z?`HO`_NjX)V4zI*{#dMYWEtlf_W~E#IS@Hb-E1uuJ7WcfPJ5d?8IfRnBYoPSX5_r=# zGcWqK6+}&#B83EYMNz5UOEGloaa#TaZMlW7upeG5~*HBQ8bwR8Z7LDDAjH z!H_!&a?EF>CEy$Z@8n3JQ(podErD#@Gr$FH!5W~TNQ{v8hQ$c8l3yJ1YnQK^N%pf9 zVpj*Ms~{OM*wMAIPcw|DS(rI~kpnWwMsE-`Ou$2$%QNhW-S#Mb&!e>E2kQBxO_gtl z!X7j6o+J#w&NF|NWY$liu%u7S|LlH0Ffb7y!hH`eji9gH5KVe)W=O)nMjQ_F*qs~xm8t1^BRj06Srg83&34lD& z4NOxyda!R4$%GLICon7(#0cu`fFu4DpIRiPuEoJ&aYug@pXbsTT=w{5G$Ml}q#<-l zb#>5+P-1ho9$Oscbi@jDd} zR6WLZtqwOXT#5GsjA_P5{7Y`@m+He<4zwofpBgz&qNx?J7PTGpLahjl*FN3>Pn=DG?~Rca=9z!3)FQsa)svn=5jP;>JcyZZvKh8`AU z>cobCH`9gwcEPCzgHvXq7%=Y+YzP7e#BF?Gd0LI-O`k@aFqL^i)Q|TJgq+xu_i2({ zZajb3$}{)q4uNKpF$rX_;Q>lEhhpepg>pL84U1#CnQ|EEX<^_xMc|^@V)Gq|1VFnY z$Gd8!(6M#W1*I}*fi0R1u?mLU8LrZG?7q6h{kpbe+p&B38jMzt4c}KeHHlJ*qZ2Qh z&R}UEDH-`zoP~-}TzI4`O}>t3KgozD)$4!88$t=FbeFeD!%nTElcm2DN-j1HZ~M!4 zO19jxEE{nuY}&Lgxi+Arr!6x}wGu0txhG&m)mdUNU9SW;zFk>7SLHu?C<}))-$LUS55zemL!^3w2GAp~oA}a$ z@M5e@Z3}d$hn^d=Uz^09{oK#(*z;IsHAYrF2esJtirh2PC|p7N_9MQ$jAT*F4nZ`} zXnQg7jDO4Nf`7}YRCVs9yVN((A)$Y0yYLDr%k%k*lJA^W;Hu3pZgm%pYS(ex>=A?K z+@E6B5e#$`kt()E^c$U?MS}`!6UFX{RlvC|!yc;1)8FCshiS-XE7j^Oj#nqJ*Wm$_ z4@?-80F08P3_>%qP|=M*S_F89{{?D(;y!KIP(owLX5Lyg)|#=hs=*)o3=sh4JP zAsb5wLA6pncHL}Ee@!W=Y#mR#tYpV%IkYY!D7XrqxL zGGM+V&C7(<_PiS;uuso!(f6Ja&iCxM^uGV`q`!kFHA}c{oY+~&i;;foEX#5Iwhqh7 z``0k9TX$KJWIlnG@3d+=E6;z+>Dx{=cV00stEe*mS&$%VHt1bMn<#rHOwG*vt4Ny> zdRI!OH)#Uw0G)H$a5pNJLdDTIJa;B%MWZh@XUDpVMyyYwrh%zBBUFvtuO{dG4K?mJ z(=_ctLj2IGc6Rr=mPCe7wzH77ZK!3-(deh;g7r5c*h>Cur#f;<4XJ=D6JZb=1%2z1JG%(LB`qH+ z?u9$K&@HBANj+?6!A#eceP-)Q9i9qE+OZT`yBvG*cz@%UIc%Ukn{GmFi#uI6TAK*h z=&|hzwTs_11c|yY)tr9?t@f?8K+F~^urBx|=QEirylkf{SG#_d$_mw7bnTUY%Ze~# z6(jH!HVe*^GZ&B>awj{SMB6_|jAp$@0Y7;|w$r)k42I{CQ2u2FCu6_a4yzxRlVNXM zP8Pk9_>3R-wZzz2J8bn3q|o^}TsTM$kb=huGKbA6WV4MZBV2#!Myj<4JFpHHgpJeM zNTGE^*E?EOT+(F4*J-e!%6*qiE8M7(>o$qH&Y{V1ycyI{JCVNU6dRH`6<^GBG_^sm z3Pc18E_a!+^ixNw$Wlt^sWjW$$Hp%SuN2-{ck3I~R(U@HF`yXOBvp;&9I6-^7Id6) zQp2}XoX;@MoHKtVN;sC~W(lRnXxEe`By@o&T;b~0Ol_63Rxf?x8%p1Jy%|9_M?$YP$Ve{8wOGAwC8IziXEbZGD6wV8WajS~!btXJdjeXeOWw>+51P@sz57SEL&dDeK|*Eg zD5z1A+G;{*tWn5_=62ssj}97y7olno;f1Iv^mc!^yA5$P?ZAJr4=*11FAl^QNB)~b zc(YH8as+RVh+&Qev@S8wBZ2cFG16mrb=V<>>PQ~6yToW6$%pm zc}$I|c(VV98dUM+_=p-+^5*bxpBh&3XTQ@vrUsTgI_h=~sF5X~x(D4y#L!*Es)I*| z$Haf&UB#`($DKn;cO=6)j}P|S#PD6ov;9Ypj@s1tifzZo$6ZRHx{`DIhld9TlwNfu z^Nu@hHU@=);@?5H!v>*{P%M0Ouzz?!DO*=^asTMiar-f)bNh;s$NR?zokx`B?Mq&E z4vr5V?H^J4w=db*eSGlv=(tO1;gRInql15gqvL}EK3@Cr;bG?pxEJ(dT=s^;awyvK{m{w##{9ct4u2VTT+gprzgW)) zLRy6wsOUG040F%o`>xMQ^x8J%xQ=PL^4D*t07lD_iPgp|qVq|?h7naqK)K~2mLKg~ zqS1zqn{=%vuFYei512>}lte)IK$qR$_6AP>77{!G05>$Uw;CcX`1&1V<8*&H8GTTT&M_uIA*f@BdPo zm7$J!L_+?~Mp+718Tk52vLzf>lePt?6|2}8Zx3y3tLZl2HtXx^aztYhLi$6}_bQ+<%x61E~78W&udU8TdSY|on!US* z6``hxr_TCqo;zzaR>hMi1z%79spuXa!X(XLm=s&TgW5d`H|s*P74`nS-)=HE?0?;N zA*vWXZ>O9zPL(D^Q3hn%^ZND5A*!)DZ@&}cb`OfvQy}V^KkitMAMvNF^R9mAEOiun z4LW9Y#Z&VdNn=+Z?X-VFo#(+NZ>{GB|7d1SJwAo-8E%l@|?RA0pgTZbk6 zX)Qj8Xz?Rbi#g@+xNAK=63V?FRc;?yU&Ea?uCN2T?)0LRO2dC}wchTF8qR%XaxLJ1 zumIiPK`LYmo8j&%!uRE1IxL@!rh`uo;KL%veu z&KCP_m2OX`PHcarbLbA+Y}i7gYb1f&>vFK1&8sivXzd$OKdLV(;|Fg{5e$2!8N{M` z$zki}{quK%-zI@!vHASr!-IFb#U6#?`N6}7??BOcx#PH8e3%Z=+{SQQjutP<$@|3z z&SXCNw+zn*#r}!Yh`*kczw+4W9Cv%ib9H>16A7%6u*`pxkNgSlM#vo_E`j~}p&GHp z4yuQ!CJbEFn=IHiB z6I26ZAhmfSp8#V%vM2lM31~c*EPrDQx+)$%gp-I&-m1C6;~j4f{n#|^zT}(1s6mHn z&_xZpx`BUO6AEHL)4--NDsyPy&0&1i(y8hSGb5nJP?GaRTF$Vv~LvuT=Ky4z6jK_>2flhCw;J``Fi#v5ZeWBg3LOn$2Y<} za-oY-Ddo6aZy&JjC=;^gA(97;AV=AXU(Y2JDJOr$b^lsa-Eea7B-Lk<+kYn}GodY- z$jES>M;ASuoC`7kiXn`J#$9A^H6ESK#DExF-;Tbb-0xdDV&<-X&fGFppny@k0Iun#pdnwuOLil`t2 zMT!T4&;@FGn@6WN50vzdkwCd0ntlkh zZpx``ZcNT5&po=L>pp&zVF`yd7^L<d%!pkN!lc?Gc*N;L}4Kcj`}KzpskI8Z?NA@7NFwO6|ig( zM)JhkU!R{>@4}k^oFqw$*lM0TB$$8osG!k8Zxf2W3)m14Vc4%1R1;I>w5Akem;SQn7F2~wSAzQl z!v0mYZ^-XAUuHjmVMoKYb$a-l(!;Gwqqt)C?C0TzSUN?2? z8e<%Cip=bnkmC_t;sFE6JJC`u<*#LHMOi$Ykd4FYBPI?_7oB*cBtquhg0Y~afiMhm z6+o@E6ppW^i=TaD6KgGWl>u9Nsyv{*0CTjFSjieTv3K{M&pR9u(8F`CV=a;2=f~C9 z%P#pcxJJXU5ifnDOy}jrMYVt85by{@Hqg~t`v~5EJNrSv*$?b4);l$7=bhciJm9CHE0B1wAEr>$4{ktVz+riW zcyqxf_-DDvKx&0_OqoQ6&6;MT&bH`5eSSE3mJlF#X|2GLkVPLIgPVU4KgxL%);j~_ zdfMc;^u(7Vbr-ipjF63S80A>77tJ<>5sh>s5J=5`W~4ruRm6)qI;3-S-%V=N444{p z9Ojuw!;6&Mlt&0qewYLY)jhR%lZc8eBTFK^sj}b121v)g?zl-X1Ru8d5GsHqfEz73 z$&1l4Q4ZrAN?TB1Tta^c48z^@*x3u!sCx-4sXZL$j(rm+G)?sA7`PZwmA9!wnNIB0 zhCq{g(+R%mnm2Yr1YXEFRJE9&i~UCyz=akMLWndSiM6NcMCNzA%WeI5ko$|FTb6Wg z)5Vz7bV%*^kGlL(TSc+wL)NWX3|Y%y9kb9|jZwW-)0ul&Lb!j3W=@oVm+ofvc^?q& zGlUTt)Jc=_Jn^~{f8EtQ!r7-%u-Sgp@gD)3nKo&z21;E?wq~#~k2wLoDWO>j%{Z#E zF;)gL)l;i}wBAvNTPYW}H5FM=P3EGWuJVW1w5ZKVUHw&yNsh{P>P9R-9rUaP=$#r4 zajMPnzPZT8G%$a5dNFo>F{)HCMZLkqSs=XkE&@!sx)SGp12=EbqTzTeOTZ08&@ zmjq#K@C*@zMI6{fE+yEalWfs-E1@_-I|8GfC`yrOH*1;VVhQ{v!KIKs7U_1+l(o59u=KHSNJ;7oe4&sG0Tsa_FF0}y$6Y|__jUbDX6P6m|2#M;Y_bX#eB@evhs!S-b>G0E zXhdAX2K$4-*d%KzcVM`|LU2_@P4snERqb0?MYXqCLTNP)E}9}t*;ezN0faN&+MfT- zmP>!PwhVDZeFtle8cT`PJ*@Rg2`MwYs3yG;Nb$|0H(RJH6!dvW>ZaF5uugzqb{l+q z{_vqQnkai~ST%7@6R3^5zP6ka)n+$boGmoRI8>{*yl5vy(hSK!ZE?z2N=76lv{t+AjUCgoV-rzRzEDM8t}YM0MDz&u&1`C z{poTMk}rIXD_6Q)5#jSg7BqYMJCOHrK*i(T%cem{hG7}dJH^jab=p&ww{>|R{`(2P z=3khb$LsoFI|i)y)>2(h&4)D5M~Q;Yg*o++YMTM1plK@NXH zA#j5X%;U3}oMaM@;=1*uU!*xxj>enNyI2}UQUPm4LMAc576Y0&Dq{!bQ5ATyf`+_W_sS|wU=}>**4vHR@)N<}5F;YNZ}HGMT@=;xd`@~1KGJo^vdEC+*fKL6j^U4lZoZBgtYJ2dRs zZ`Tb-e(Y5vHgMyAz5P%!Bv@Mps;K70xHr0(&c@~Nf01W)p8Zwz44;C#PZNJ*n6&#) z0x@LSYmvYDC!XGan9dg{q!zH{MdL(3jgL1-ng{+z4E*mcAd0DJhZ?YU-K`C3yLgmH zwp!rbG@5v9?a9)Fgf?W8$cHb}4jt;qK)9PmIF#$y2H`;ZIe>8BM#;aXwkEV?TMiN# zb@VWhS5VwH*6skcK2d?3@{@lv^|i0iSS;}24bgEQSy<9x4y{X_W5PX}-d@eQe1{Jy z&pZ53viU@VkEe=+PaNdC-k}Z`?XJp`XCT})2zOkByMQo4)yq&n`>V0vP0pfqho2=6Y!n-+F$yv2VtSAU*P-p`ih zWbts6JGsfm>lG#B)+2_X+f`Us%^y(E$2)pP050jyI zZ!9t3=;i1D(wSMPEiQism{x@lV%;cW-Hi~VN-_~*G5eIF4(Xdy$_xr{QZy_vqN^s+ z;ZTu7Q4Q~h8}f_T@|8F9JgirQEijMz3tVd*IE|bPLDYQgQF*IgCyr~4$w+~7uF25{ z>aFWgyc527pldeLb!;dKB3|t(&P8EB0SdKXPvUk^YxocxkSTw9(Te)pDi zzw7IMH(U3+Tk3un>wY()``yiTzq`He$0k|O{koGZpF>W)nNm-b;fT%tILyy1T$sP? zeJcOL-#&j)%kH;NnngwB1Fc)y6^=aRUy0kYDs_$cJ(LQ>$uY>b3H*K-UoO_M z+6=iXV2#yC1(m^A)^O0t`#I;dor^q7f-ZbVhaJ)82EIBJK^NgEq)sp@eYrd0BS7p3 zSqF`rB_0XG4X2W)rPFuUB`=0;&;S)AlLN@K=9Ix?oLk2(O5oI<^E;6a=&;W~(_@El@=S&P@zY)W=Bl)8HLJUNic(AWH?J7M{6`h;6clZ}$r9 z#1OSpK6aw1bM=947P*|k5lxND9Ozp#l0`cKYuzN37rkzZp7g@I=zO0{YM0!F-{9UU z{*qqbIrD#NAQ=%|{e@SY(Um1OUMh7;`TQ{T9x&p-A8KiB$-O8!6_$8 zs@+VfcDIyj-YS(iQy!5j;kNlIpz4iy^dUuzK9+xXYZHBRp1+0Yo}9j&sG3X0ej>y~ zm1bb232umz+sscX02sJ=3UTk3gxatC;8wjOWaBV3%bRmnkcH$PgP z+K-!3XzTQg&Rh+WSQGb3 zY(@pCZ{AU8yIuIqwxL4m(VkQn0*f5=?S|F2ldZnpg!(2AS^P_=uY0?|9jSkBVB=t8 z^$lH#eTV8BzK3BO^}R>L<65}46^x5x;$M2BWl6{5x>-gw8U~iL5>pF{4Qj@m!@d@Y zx`i7!sWbcj;ZB#zU|dC9A?OSgB%H1ZrVL!Mfx2S=w-1j+#GgUvUU8Lsy!tQCCyPgO ze!SR_qa+v7QCbTF!q&S^d(k^OpAoRQ$dG^ReBfxFTqFUO{qr$^Y%m3kFq7 z3cl9641KM43190){eqWUF)H3p1xfCC@tH*&Nlib8n!ZgYjqqu)! zGXZrH!v&oJZe$PTd|VhXN+Cp0(cejuzJq&3ZZhz!OuPDf?!wQNNC>cS1&Mo8#CUgo zb4v8If^kcZkOVHd1e{4p_#QxewZ!SqRw6xo1H;HgKho7I&BA2^rax;(|ueMjZT- zg*N5$0#(I0(%Lr8YG^Xa7%OTDIgW_tVlETS7i&W9#2ReAV`^>bK_dE^^1m3G@6{=Y zkPx2l1a_&M*iy^58edLX=jmlRDTl@1X1&YHayIwhKp}29WJrI&%W}nEqL9(ZpC7Vm z7Vvp{>n>jF=G3O6F3rGBP!r{knHU(tKc)Ey~%1alzuq18A~XUzUO$1vky3dyMbn>2NvXmq`sDBG@3e!E`cT z6mS3b(=Tt?|NnpY55Kg(W4+;0gAVn&qhEKa*IoVkfO>skfFDus5B2+f68y30-+e?i zcx2E!BuD7rA&!qoAe|%K=IHQnpM=xJq#Pd~cWHw55x+VI#|Mx0j}FK&_Yvp1j}IOn z9d{p-5D$=m+K(R}b~;C0Ha^`JvEvaR{_*kAai@Jmv*v%$kbT^3A08h*K4|YBKkgns zrde>buiHQFcK7#Lr~RWxhX=>UhmYDMkw=JWj}8uwjt>sn$NR_a$A^cVBbtGoE|U3i zyK~U#Jla1vY9Aau?(TPv_d7?Aj`tawox?|u4mu2LS}&No7`Y#`yN|m2M+`#y@&2QO zBL-0?MDo)$L-@s zhx^^5$B)?*GhPPxtZTgYMzu zV=nt+M#%vK&!okMV5~aevO46y8CH)OQA{!S508I32M0_#j5Ibp8+ZSZagWj2?mRkX z%J!(kSkc};VCL|+-QMp!I(*c5#MJbteb{CM93SpKdc@SH^Z0-f!A3ti*k@YInjWZxMMr027Qy;bzG*A%_1g`$JC2-3ltDYRI#Fj}m`r2G|T zIH6!?#R@2adGJ~+;8$z`k7oq87ys^1x*LD=&S@dxY zMm;IEwD1f{fH-yl_#A3kGbn|{p##I`R?C_eDb{ry7(VA(*7QTMao?rI=VHsAUPzu= zECJom5QW<*Q_~KeZkdYKak^#d*}jWpu9_X|=(4|Fl&p_PsNsifO(60=?C&Rdoauk% z;uqO#V2J|sVBlJ;9kTv;IvSObN0~o-I-B*xf@54RK1|s{p_=q&>o;X@Hu%7Azvz8e z^mrS%|Kd}*{;qi2WGl-#TS+$9UvGDd){~+?osM?(+G(+zP3Dk({OOX9a>}^kt~TGW zu$wIv){O?g26>lf2RTsr>-w6pi!FbL*3F`K?w@?;Ym33+?R3!_{WKevuwLc8?Ir8% z;hX8W{NEyXDb}luFTIDN(2v)L^v>mT$ZImI zXX5n^C3F)#KxuF{Hj?PZ2JARpO)H^A1(#rhwRN)nH}_B*E+w6T%v}$^E=N7E0RPpS z@^jc=7>Z$IdOq%50u4G(`CotK;`Hy$;vY{MV`ir8wfNQK{^9St+CctcGNFunD}Led z*t(q=*l@mj=j9DK@rrhF*RdY^>vtk+dc%kvPrsD^U%8$KkYUDL%{i)&MIG;F;{SFvV6?HLMYmDmE^>v0Ly=V2=oquhljBs zjdvb$QehPFS4%XJ4CX>w71tEDY#@nPCPSmbjWQBwL6T{Vn;?U)s~ei*I}XctB+qvc zXT)>K-<@|h%@w1$(ll56j)|3^xXPh;4o-J#1)}IiV%iPJi3tY;1?ZDvGIxCc@OjB5 zhDlI7HhNNAdfbN42Bd!&;~nu`8>}!!qm@GMNb@97dOm-%?9W5az~`4hMe^nJOzX7# z01sg-hG^jE4kK&##xtfHbg#K22j6Q>0ZFRHUnbmz7k)3iBGur{} z$n8obn3@o<>}_BImJ|97~Kd~)#%`A2eBR~8r53Rtd!sjlE@08C~ zx~z?7eNwFMS-Tc5_`e-#?<#lRU7AYk?3I#!-Pc&vFGXE8~0g2 zzMCP`$`WYx4qJa_#CKUG5NA;t^alwI+ExT z5zH6i#TsaZKUd(N#8b->fUxyFbmw5u&|h-BMY@cp^Jaf>!Dh#z#TI%0;Qo89Ui~A0 zEB2}v57pZSpNtsF))TwGvC0eerZ=2J5B6`$fnTT*RI~tJk>XE*Gxi?k8n$ye8CHP7 z@oT7ZH|P>)+mF>~QO*?SD7O8NTpDA>{k=ZpoLPJ|w5&{fx6Jrk*hdQA;duS$QpS6qn`- zEbU@Iq)V)^sP!7daR#T^eX5;h_hYEa0FBwX~hKue$;F|k)U2^~HuDJg#7u;{k&vuCaV>O$L#kRh~pPA5G+nHUj=I{+v zP56p`&E1<$zMoAmX?Ws~G|-ONqqD)j=xv4}JmV)%NkmDgxp+Q&=mAIWfdCx@iHguA zQmh+4+IFt~21m3azKj54J!KM~4E+(C#X2;4o1Zp+aU)qd8vjPFC@qEuYaPJ3tlrN5*`_280S%VqA#>JaB*K-E^;G(DI;Xxa!X9&#Ub%}iP9b~8?@(cXv%lnCf6$nI zV1F~A@fqOFs2X@0y_)ZsA3c~1K(*lC0CG@&zR=_U5oq>-D+*WLY$ZzV8J@l3;lrYD z2fVy%i$mc(cU&@e&gFYa9sl_*KqAof(*;T1ydy~|)gSY&deYTXpG(^u>S@XjO_ylW zg(h9uu*Legl44L8*=6V5Icv=S>MCO72SNEm_>;Y{LgZP8$H*9jIZQEw>c3gX07dVA z_Dw%`06WT_bwz|d+n0yGi12CFW${y!0fjK?8lCH7z2zjX*GXM@Ob}YbOF@o4vLFkM z-cFy&x*|N6nDQZ1c;w`N*nd7WdX8IDWj$wSzOm598dr01uCXT(X56X__j{ayEYd9A z!d&~VXpjdR0mu{4*95U-zVA&*&B+UYF(<1-lncJde``_+)Qr%Z4Xa6yIgvHfbq}aT z`85p7XWDC|!d7H1TA15ZBwzG(B~EFM)Ef<#Hx)nd9M32Dujt^7+b0>bj) z#^yY~wO0kJf;3w;JdV4jM!j~1jVVJ2g`j4=lpZ8Gfz>ckYAX-9KS+D4{3Ukud{@P8 zS6FxH)>N-xcEV9E-R6EZu{)tdyD4)pHG;Q)(rV_ibFuUCsAj~E`1ZNyD z-l&)PD6>D$tw_?=kl8s#QEVScww9Fv5q?aGlMk8&7sXT_OyJnDAL?WRV$2jBOZWoi z5m{VOux#E4#s6aVsRgHinrCZ)DCAUDu#$l>lWb5ODK=d46->*2l)h}oj>`sO$nIv$ zxDP-+vhKhO?RKo%AKqw}b|FZQcv(lo6npS?0KENf*Q*O@dqp8UjGV$|xXXU2fS0=` zz>^)!6adB^34-?cr>9|TjY~*W+|2(-_RIT!#8Ge1f^`boGi3F~Wi6t$VP~-uW{o=j z;Y{0r2(T?++?u9;O$^-Y{D(9009$?oGuKMxTf2JY89gNoTR$&j;*iBap>(mVEhOWw zK=SxnZL3?R95kWA2@36oKNg{?t1 zHdq}EpJ)z$2FZ64t%h24{T{onYV%Sh`SWYfXriwb?vB@q=N8U;R)eTx_)^a1rI(Wr zx&rJrGo73z1nJ}|aQcBXAa;IMdpkZV#Es|3*wp8ujj^5M>54N&5)9EQ-w-l$S(Hnc zrO4=hkw?GzHjAEmf|++YsgBHPW|v#y%(SPb*M=c~yy6W%UbyMNQ^wd?P8g~Fi5IqQAy7q@dq-eA_;-xW1{9K4-ZV6Sm1RV6ZdiPIH z0#DI@PQo))&?3cRJ8ngaR|sHm0DR)K=3_MEt__&BbBiZ14s~IC z(wq3vW*r@f#0BV^#6KNTHBBaKE%MCg4f9Svrz#m3sGlxk#$r*y2S$o%Y2|LHbm3(= z?lY(Lp}KrN<{M9Qh#acPd+w3&8bpk&{mr4E4fZ3EFvdNL0uP(tMQw zDNn}^;6x>yr9Urwiw_UQSm)fR<)0n(r8_Tg++%^B*cY^TV~kl31%NubJ;(>j7!OcA>u=?00z}5^?cfe}Ux=Z-|YJL*t zpkv_Mb5K~1#la_7oj2ehqv1ON;?_CH8bmoL-Xjj0n(6)V|4^k7P)qgPRLf+bErUUSJO4mJs9T~# z5x1(LQlfnPzsfh&A(vMZaGXoX5<>qSze5dpp@(Px(w)VrU;=(kl-p*nb z3AQb8FUpt85lQJsiqh~l1Cc$EL_%donkzE=EFM7PTssU<YFP-VEHV9#dtMsZ83USB+-nU^$z!-!}!El~UWb zX#Z|lj;gWTxn+Yzd_A;;%}KE)=Fj+KKexBF)Q$>na{kV40}FhA_D9a)65b4eneo{p zcQXxG!v0_!fp+io2UV8O$2+L9pkOXpVixliD!5R31Y4)F$bxGGaJRv*GL=Q3 z4FZ&_NrGiL0{dw)D076?(1){xO*lSAu#QX4VjBD3!#1A-1k2c8{7J`fPBpyW&=8={ zZcQ#q2O&8ro;5Ik4;kVP@2DM(5QpsAni!vCOP5{l4Hb+=bmKAm1(*@M63+>a@t5Y( zW5hrAYGrFEhtG0UkK3&vw?+MoV69-PVyEMd{#K1fl7HXxuHbEb#x>>VDMO|1;_WrJ zQ};+8ZOy6!r&jze_ja^JJ4(y#U4A0-Pk-Vcxt9>26Ev}Z_$duhF$BDi=z+~tqv6@9 z;Is8HM+czHuCEY(^m(KZIEUi{a4{u&0Ud$|qjd`iX|p_y>B3!&IzctCd*VhMF2D0>ey*Q_ zMh+~YdlDLe;F)|pSRg1q2MF$iXV#5&oybJL2t;%Ef=R}**H0Q3e9QKKo)oXG{aP{6 zEk_ISmTrKh-TB>+=y858xajC`#MB_=-@A7ylWGooqu)WwIC$BxG0<2S49k(Bc$k!=`U+y821=L*P2W`*@oVN)4hP;FX)vm)}=>A=qCsulW;OORFSs z*zO}IgKx>=ZD=3u0zLP{h|CvT(4d)HRv?YXBw+QUU1MCt*<$`Cd;qfU28x*m9gKdb z%@c`*+`HfP+>DD{s=dw2C{gE_DpWRr^7ko!v|ZVywr0F*fZrM=_v(?H`7NyNzr738 z^A)x08!FYbCoPrm05IH78hmxbUFjpugAL}e25YJuos1}Dp@@hS#SR>ZgPPuar9wQ^>O8~UdXA=;<#tdVq@I!`%-cl`hX^T@WZ^h=+ z#t2;GcV<4)rOd;t&I?s^aC z`C_bBUA_8DO?}nm3p0ghO5!B<PW)e(7 z?U@9j26in`Q&S0g?U16Ik}4s8n%zkRmx-0}W(iRQ`sV_`T>Cw}bU={x+_bcgfS*<_ z_L=9}xL><9Kh1^OcRch8oDk)ql}m@WVLz?y{#ku$grnBJJKIqUk;FYUKLe*cbq|QV z5a;3uPtDKL^?gt68G&G6mR)Y|s~wfnZud>O;Agx)zqu?2djDe~lNq6ZQ=j@w@7z1$ zi@h)){q-ik*tf5*pP$IdALG@K9|X~QBd-=!ZEU>F)uP*=zk*8u&rvn|h|O~YV^pj#TW$~lH&J~0yj z`c-qzZMaS}T+eYaar9O@`jnFkX{}nV$ySI0nJ#b-*S8F^Fk*x>0>avcu#Q3?aadas zUSTO3J{KhacuilX>UbuALHQ?2K?#=?SGqipfOgeAofi^+Snm;9x8Wjn83+HWb! zl2nBq+HXUg@F|L>hFVjK#}4JX6xR`clMpB0pnkop6v18%Ah4W2{6ph!KlCO)&3^do z@&|7D$V|Zd-;!5Q11#&=EEB*3Y{TH1g=uP5B|S*LTjiWRYCeR_p4hHuEau(#=i2ow z#DMeofWPCPdpE6r-|_Fao1buziZtC`aVF=BJ<;2M69l-zw5fr)OLT$WIenlZ>!e$h zL%vJdFk?0`ux8=PBT-@Jz!iFOu`n|j05?BlN|e-`fRuqRSuF)Owp2$fz+2T!4%lBY z!#G+&p&>l-Tk`%^Lp&s)4J$L~?cSj$?l3KXgP19A&qNS!oQ; z6=8$zaVS>)sl9 zZH-IfnQCfE?^aFCVoBy1BGXxRq-j>z*Pj8Ef$u?kDxj%e_U=Kq6F! zk>KNh8mLdhIY?>WE|Ee|HX_Xc=Vxg>;cEyEm`I=kGB%ol)XLluoyc3Q+|{olEWT|0 zVYQg`2Jro*R}4@20TVy9M(DEq3W?(sB$EW{B;xw>jua9B(S}jb=473jV(idJxJsj! zgmLVw%YrV&7fGG3(W|ejujSwWus=*s&Rw^E`6c=Yhk01)`!$#Vnqgy zzALwL6XUIC@>ck9+@@N0{kYYXZcLB)o#Hpala*i2R* zG*^|3C}0A%VdGd+#D3uOn|AH@=>y zqI*hhc}GdE370^ZXOt>SKr>30&CUfsJ)zyj*|5KR375SJVG?)0!FMnFlyZBwv@@#3H5Z2D}voD3V23}#HY+O}&jLsvOZQp}iW zqBR}uW-+0%On@)nN04iHgRc8Y({w?$xJ?gTtOwrE$S|o4G96*d4HD&?2Dx=2<-%oh zf>&)`;srY0xKCI7pjv5Gux50B(+OUDMav&$RvbHMfxIBjfHcKhvkQYb{a;Kg7v+2* zZ)JViTUF!U$P~qUyH(9%+*_IK9+44wK372bh7oJsbdQ}sSL4_XsKmjGvS*O1CTZlV zNdh^52m@CW3NtZ?-GIVOl3*_DQB-fmyy!+B$yv2r&t|El&>#*R*@~-w39Ma~Ym{?& zEwo^+Y8oP#hA{lOH(OL;9Hq4a7VJMe%o+)_S+HS0-GRsaD`w0{`ECt+6d*wx+HXJw z7eD)tpn_5vAjElLXz4+QhChmH&{m{GRfZIYuPuTO`*{tKNQ=39GAw!cb}GrRp4X7Z zkJUu(!{<0is*XySH<2oTdcvl6_}oa;ylKH08SaQLA=i*pAk(Bv&Q@lvHx{>#uE;VS z4h8gwwV-*$aZ%N0Cf=5R3|PQcylx0w*&+y)Jj!ADs}sBRN)Si2R!GK$m@x&DLhJ?d zeVIZe)zWCN5n`^M))At(gf}8YZast$4K7I`0|wPi$L_O1@3J?j7HjA6>+*8;lNEVPf3;Wi@9tG$5_{i(Qkry=9=IB}t$+hdn0+XhhW!?L(X;0ca?7N~FXRI!MUDp_^9Km+B4Kq?d{ z#hmT1TLU;2n{q6+I4|t}dHv*k+`V>1V}6=5x@DG2b&rx*D^GkB1ne{|1BGkotZ z#^o|j*5lv;yjf@r3}Hge+;!r?*LgLu90EX@k`Wl2IwUMs(z8bv?XPi}GmFZ}7owWofA19HdpQQ6&qu97lND>O?Ce z|4r-hJkyQV37>aKQL+ylf5x>m)HA=U#SXHx>D9-)a^{B3C~o}suDj&y%|rY=Ij#F}osXzKF%WlB1HoaZMq!Q-_@*qb!@9_TY{v$~ znkFZ<>$LvRn#u4fP({8dH)EWR=_0%x$kY)_iC1G5#MNJ*eB55*f4@PX)IYTP!;gAH z$Yq;#8XahW8eY3n1Mmd*Z0}$i`DG=|CM3FV8_>{ z;Hm-pcyjg$B6u1xY?|}imXQTZY(<)GL&C&OSkL?vD$5=ij=F=WEL+RImtz|hD+qsPoKq@XBN4PDLz9RG)27qPe=gTpQ0GbGl3rC*f2_%C z*O!?2`Eu=6BKq|4) z|9N}o#U8?@e=~f3RZ{I_MsS$>uGq{_>lD}mJP18iWGbM8@uf@D+50rhw^_I`tbOka zNGWMSP7#m-+}z3_RseKUn|B!AZq(m)P!;+ZIgfM-G17JOp@vm@Xh()f8bsU)w~y-H zcsB7dZDoKULx!O~%Exis&y{9eU(=^RRyX#FdB{+}f8%s$ECDe`iZ2UKVE3yBr>EVO zguapmAkkIeh%>^YOt;ub_(~{PfurP>^nMd`R^W(dg&YzqHeF|oCu%0l=?UMRPA60D zTmQT{7#7{$D1SZ~kA~yCJKdQMXK$5g4EtZ)ocmev?qCM#T;Sah;4q~29;;D3z~?ZE z_KWVcf2&$ehkaHF_=g_OtpBzIy8LFdD6FrNe)$@gM8_#|Hm#kN>#OfBe9I zJm5cmv_FmoPKT2x!#Bej9b24n8uwfRYD-5-9oc*qxC*1|BQ!7sFx(?;=Ide_8v=M(D#ylOB;x_sj4?DR}&N#0ro4 z$2QgW=UdTJ9Z&FPpU!ebNl7eV8&lPegM`86}XyK?eF}?6#z)O%Nw&^9`MW68!-P`-~#a z51kb=@S;~|=K2oOs7aie+me<-Q?DYGf2(b)goY6Wg><3x%wAz6d*gsu*lKe>_ot zm#Bp^wN6h4QWK2NPeYiymuCiKetA{`F_*xK;hS*{@XycT*?7~#7=M*?aylHJ7a>?o z2(9!6l>q52WQO-a5zqpHqT0@kfymUg`bOI^ zmHDm@6}CgQ8q_qCX1k$?l|mCyf3i7e^JyMsvyfR@COEn@toV1>!QKoW^C0lxDGiyo zDCB)Sj&DqQ?-Xb{n-73n%>vb0S!3XcWZn>^8q{ZS-D!3VnqhYsJkU^^1_c7Q4kewb z@47Q2S$3s9LRZL`SVvqv7}ek{0%GkV5&g+&b*?#-#73IXX2ra=6GTy)74zCwjzncwibY$L?SENz7$UetdB7Wj`&j)^VoPF6!5}{d>Bti>Yk_gk@ z2wq(xB525xG?4TsNzkq3OsJ+nNDu$T@n4JK?;g3Njr?Y&-AE}b9sLoO zHnHbd_Hp)VHXPAPQ>ZNuMO)3WY5zs-tWUesnj5GWQ`Kxb1CLA0e@kmM@9SSD)3dk3 z;`H@PJrdf`?3o(1tj)8*YTDF<&z%xW)UvYSnV%L1<}Fk`aXZvr{jb-y6Kz|sTh#*O zO93JKmkD{u&Tqm+Hl0ca*dc{IB3!u`fdIAL;wua`+kg9f`lIj={5{!?`^lYgdWtdHB>x zG$~;dyf&&D0(vQCtH0%s71mzey8TY4sDpoeGvHle9Dy*FpG}j)m#=nP7QoY; zX9v4FEI>8bnKeknS7z3w8dw0Y)Zm|;VXmv)qTfBsJNFy?$si}mgoBRGeb{Jv=LzU% zw@3y+8gQ=tf9mjQ=l&|`f1;0XUgqyz2T)2X+!^!imsto4*X0+jf*}oHwa`IfMW_aIo zBRZ+9k6Bf-9%ha$AHMTbIECn54kxEyc)p+*QiwI(f76A12vx+F;RY!NU=vnb3(Q+s z?(g5bw|-xZyPZHf`Sgp)#|E1n8Prw+VmVQflCkuurB~yeL;yL@gb4C(cc&E8pwAxo z!@jx}1!RW;$Br{~P1-Q=hqYnM?ouyY=U@R|#K#(u=lBQ@tqpZ*Lsj<(TjH_6%J09g zI2MWbe+Eu8TvdyDx+8OcX4zB4J_zomxv?|b-9NCwC_JbJuMJ@Ioaq~29plrheZ=D2 zN5Xag&~>jr#kwW(up^jwUSDfjyX~M*$2xP3J66GVAoJgOLN9wwDV8R~fu!0@Rs6ao z1gPb(G13CTb#Dj949dA~FfenO4!dBl)Th1BfBFV&fz*E;^RWEKH7HmA^~)bX`2)YW zvx@aQLH$l=6+f(oAF$`ndidc!cI}sYTW1Ck2g8!e?qsZ1^WBXx8{f5KGZb--uW^ps zj>Cs5W zf3&IeCIM^2R<`!u_yXd|UX6!ZDs>lHzV0fa70a9MeIc-JP!(LuP1BjG6fCB;#hm@g z<@L$lFMEdvFj<1rZ?UYJ`oHcye}&ao?pihUz*}^cebfN2J~+tLKdo#`9{c1_LOKUA zj+CDwjuowSV>^hngc&W4QL}HxZ8($tf2pC6)Xxgu9g~=kL)p`=DKW$}n&;Z9GK-0Uzt?6TuBVd_ppk*RgxDzz zBGgHWzjc( zl2A*!!Vhn_sd2Mx8nkE4midx8e-9C;nq!ePraTsDLHueV7Y=m!AalHK$#aQ!h4%fJ z6A3Nu>q^|23*VDgtf@nYBGbuwx{VNMkM|rhe_*HYEO3Gc zfp5~s5UgaO3qi?!_9&A{pFhl#R=U(d@oe&@i(zjWoHm&Fx3(<~TPU@fPi1W^ieOFw za^VMUb?EOfqjiZ6n$o}8rS*~_enGjo<(_oW1RucNlkfo53L%W_$?L}sCZh+*=C{## z_UD@Xxh{Wh$e;J*&-?P{e-HBK1Nrku`Lip3_TGq4O9X?v-5W40-0+4C3-5V@XM6uS*8AgF?@waAfA7Y6e;V|DOm}IF zXI}f);vu5T4-zHcQkepl0iw*c7I6}jN)u^6B8on#XnD_c2L`*2?Fdor&hn|UuDkR` z&v`!X=ZYPn50@Nxv=dhqm>UUxfzeNf0Q|ZPRynpBp(wF zhssfayNX}RaGI$pFvun+nqq+%A4?8J7oDDi4xNl=T{T6zfAFG8R~1agc{YGaAwh9L z5Ez*cnffA{aADys_Qq%D&>7xL8%*G8>139jsHq8PWb12pd&3#s0L!NWA`>_cP!|UX zNRjNV;)9p0p>@j+PqH2+QbM=F?G+f1qaG+GU^JXMK^giQZbK(qG4ge*RoSeCw~KIy z`%&D?4Coa%e}Nx@Sk<|8KQyjXFITN>IJk6sFS>U(fLnL?Im6)S)gx7OY`SPhDF#VV zf`{lpCuQ_{Ggrz3elljGH^=NLpH+VcG3B>^KHER}H9wt9Karj~oJ^i|r*HDckTQv? zQqm6aVFG(5t^;pCv2ctyxvCtvc8Xv82@_x~88yoxf2ZhdGRa0zi&Td(M)yy^y)ul1 z#6?KvaH$f3Rn@dYTJGqDBd2#{cMiAJ@R?PytxFGEkzwApfa06GB&gVexgA@t^=5)y z|JnWZ#o_;k=>t0m#bWYM(i7d<+q(bi=V!bB`D*`gH>|hv`)zlB$F+H}`*LspNu+u^ zRyzhae~(psy#H+fd8G1Yyz;NV?nElLVwIo${Bq}U43E#T+AmYJza(M*$L?XI{!tQo zy#8^lzIAVVmGAP(w=y1THtLSw|77BEU7Q0(xUR3kt5o>skM^(5s{3=@$b1mN24IVy zFq}{aYKyC;z3htKxv`gnSTvWxDS3_d`Q&ige;ulQ>>G-=dU&7&U%wgh;h~Jd+79}L z1>j1o1;rKXy};!_hiRLuF_aN{fSCcWDEG=OaS-wR)w5?h_K^0#V}7&koc|cbf4Dnu z5D_6@&3KDx5^x@Yh4B;u*a>gaO(IsLAjihzd^C!TwHsRq)Kv^hO3P$Y-X7vbC{Bdp ze?tr)2Lkst5jp0U1u^%v`VYIFm%<3aEh@hTm$dwzpGH92K5gXVcNbdzQh?Md80DKj zK3ZLA!dz`oe|RhWLWk6R_lUE`cLvt+$CWspaN&B_r){G~4>7w^{o8XB`+U#G;cT22 zg|D=Fp3)+yAI>MUJOWmetQMiB0Ls=Ze+Pta1*M_1Js`A*x%MRpniy+aF>y-bJQCM~ zpKZ5vLeu~&>|1RTMg5nIj(20Ve{Kfjsu$CeQH7vb?UwW53`mm{&q*i9) zbLe8F8hHE7gJO=P6&!my{oY>31VCzC5K==+g%T!rJ;#zo2kKlzA8PI1e{x;5^m@@U zn%iwK>6kmxUj40);QiL>3u{jo5DPY&?Gy<551O%7rL}d6y0D9~1{`=;&kYDhZKy%T z@DH*LHjR;h;Tt*tNVbBI7S#x%RX}a#6sO{%h7!%j+DR!RZ8r5%#M)8ZjZub(JB6`Ps%=e&yr z3HB&b0&XghiyXuF9_XM69j@?*liBDME#Ez+DmO74bJBj%EecBhU_%jHfB|7=elugb zB?q8aG+hust7hUeO=#z&og+^}KB!6K9(JP1kR0o=Vy<=(3+D#)b>t#6>qQ9`w*m(W zgDUTTk7q0V{V5o>f5=VdvLJhn&D9kJM3Wh5FI@)+lCM)K6s#Dzkq%!CLMHYDZmb1T z^GIXQV)CP+!kx2Y6QSsdir(tl*cDF}f(YBn@h=U?PhC>_!eV@EN-P~&$EFeKG0702 zb@A;h5I_Z|&G}>XAj~=7G`w=&-su&(X48fJNkt71$qqKre~_Nu27rpE00!dxToANj zscy}J#Br6WaFA~4RQ`4$5~M-U<5msAFgVghCdtsuTm)pYYO&B!Y)7%9k!%g`Wd@)N z*fMx2fb5{LtqN|Clrhwzt&%s}ai1JBpMVv-ORLtfMKc~<`Tl~Yc@U7uxW>{g+)@FM;kdXS zbVod}f1dRzgilp-o!Z=# zvKKoac%RnSAZcR36SZAISV^$)v&~5RW4l5`S6pS0{bF>Z93)?)EufA_fJ|EyrPmY} zQiZ$~2Qy5=Zel6^nO}twb;z} zOX{k5mrqke?%X{_hs4HQ>oe3%a{iyse@>#;KVfNiS206RSN!6qz4rOYP=WBxwNURm ztLrVi{8^_*qTOC0^{%T{Lzv6^7UA7+{4)ho+zkeUt=mo(9wcvC!Ibt%w50f6ocP zS|=DxlYNMnJBBiwikC4(v%XLZmA(Ifa}d30@nsC|^pl^>g>!1f9dEE#kkzTaHkADj z=e0pghe88LifHw~Gj}*4Gu=AqWOlL&9{Zx8i@5|9p-gj^Sl|ougxZKKLzNs`AhI#< z)RFeF3MtM}#61{!`K?vqSMeMwf03E@KL3<(r{IZ)`h@nk=TU)H-i+HsTrWf(IA_C8 zhT}$&pKY3SQS2p6f!lTxSx9D~AL#Ov4jZhF!UP29L>x|w8M+1Wp|4fSUBQ5Lq=OLa zGxwmHZ`j-rp|QtoLX0QW4cH!M>c7yaJQt~OT=*V~$Vi=5fRL9f8ADlYK+cS zpdmWjkIe=p0-uB%LlwYuYo=7}XB<-9uQ%LZZdW@eJg>yUG%0{7n&1=AghHx*l+trl zLeFuG9zO+QoRGTC2GJj!AKtFzUvNio0st&Tx0?~AfoX(pS9%~=VTE&n6;}8S{8Xk% zmw-rPI?vAgS{vqIpI*5!e@|_(Z|M4JovXOD_uG+eF753fpHB<_O4+Y;fgxz|G;==+ol( zL;=i$7r&lC-Kvp1D+~^=wJYYV&`*EkZyP>|b=1<`f@`+$e=gL434nm;0RFuHv=%rk zZ1f$c^+O6k`-)c&_mvi>z8e@4@zRKOcuNT05`PJUW;ai@FAe>Dwe7EWwUU-7Cc!ml z$}pR`pZR!Ten_QE$9puxDY6J%CU`j@e`B|)j|d?94R=qIPL>*fuiW*SA%0?C*P*9% zn643XOf%=At@v`$R^73G6m+4R!%j@xhKXef`{9WtV?OQ(E)YsW$_-m+U#1!lj*E-+ zqP2{>(}UMFMK8q>j90r2%o7j2r;;1A*^YW`P8V zv9BJ4?K)#nO5Xg0Rj}Bnb57fCZZuG1TG|)D;TnA>rOXF^8rNJeFh?Y)E*n^0-XFc3 zgX@=Gx8i{HErq7AC#y+mH$aZe@{#}zlr=Dd@oZCXZRnY^T63W|=4JQL9~J+1ot&FR*3X zNJWdr#EfNsnFtxJVGNfV<4t_LYwe4;2rU2@w9nlv(C-%T!XQ0N>CA)ZkFJ~Lg2*ou zN+v?KfDqp2G97|F;IZ~k4Yh=B3VX#+!HmQ^xDwlg4QC)mIkqzsKsU|((=?H?)FI|A zD`*EHE~RD=0wI=E(I`yc`KY80u1l+rrcW^;7}D&2CRCokNA)&kTiaR^HO0_!oZ`XU zRy#OU03tK?-Hw64^I%&(tYU&tg9As_4b8L3P|L}YwuU%!l%D-!Dgi;+s?a|57p@1O`-QoK2y7D ziyo(K z@_p%nYXSHK--CA++&~mK63%-wIXNkE>#;F$EAtOfwO@kOp-$0(BYYBmJwMGu4-@S5 z%9Lz!KvM%5Z>rR@LDIuZ zsQOPxoMDWO6P|`e>)7V3*aD5t~68V4Oel~N3FtOerOUv=y4;)2&-T}UqKPISfv z>d6^1v2_?L&a(ttM2i}tN;X8z<+Q%&gi8Wn%7ywTg_R_K@1&u_H}EWpZjRn0FVuuR zYcPwdc|+W}y2`%uI$8?DetSC{A#e6_JgXY`Rsf;HYW#v#02d* zabB{OmSv-T`6(gKc!vLQr}IyJRCBP#YF|r!O)PbOrtofQ%g#Wc zI2G0F*-X6p8(C3x5>bqE@sH{%tZi)iqC1@pyQ4-S6Ej9tHM11=pE{8h^C~j4a71u) zU_k25vbqxtLo2CCF_W{-CjIz-b51PDmzBsYi*Zg$*dqPMyl*lFH=mraX-wyq@{}5{ z{!YfZ^SVHTyB%4}9ESruJPbF@==59aK)#1@V8lF8ilOhgfb#o!6R(ofV|8C5lg8>C zGkfam9(Il%>nkzqY=^1oR}R%p$dwfjuIA)tRupswGjoeo2x6?^|JnI}va+%zK9s3& zgeKHE9seiex+uPi!n$+~ywmlWlzBRst2}2oiy6QkZ0wmy;iP5YiVYCPwp=mZnw(WS zbb%I)?<|Oh`pZSi+}##E9m3jjOD{^6bd0DI4<%69&y&F?Y<)m?H^NeyJ2?FQGH2_e zW5>K47X#5kvyM4IHwDgr@g^^~eVYnrGJ8WX?o=>*{Lb9&U>25ya$7=CrjKbOA<~$| z3^mgi@<&*=oXa7HC3o>tl)ESlev?|<6=cFl>pi3po#T(_v0SOa0$J6fikX}oll2h+#QI@?K#A5>bQPp_ zGlgXL!+Fk5OYqxo6q`tTj64XN`qOJFl(&%1wE2U^0tq+OZg@8t`5I)eId=3%maNA| z>)^bX!mK#&!MU}6sSw2v>VzoTHjPLOW-Dt15xo$E17eW)7A0;iByK4I%=+$gSqQU^ znzqq*cn}_}g+^iF!9V1_iiF@{bK(_S0)3f4rd~;5V2M*><0s<#3^3P&9-fo2U^c9_ zoR&k{$1uc;=9xvVV?eLMsaF>8mMRCST;HF0g zbZ+!+W~k*b%NgY>vhqol(u-;3?-T}(8jsI=*X_e2Ln9p?)5@knKIzeg4o6hqc#N7V zFLY^PsC3zXiE>CE76H4N@r>2X&%$tl>Qb4DT;e15>kjnp?m<|D8`>=}wc)STT9`5@ zD#ToxP;)8ZB6cSL@T&|^rDM6{VqVvGc+&gx;1 zvW^n9A<9b+0lI+@;5re`QVQ#xBSxjMR|uq#r5O8v>`uT+L!d)s%?^a!NsqF`Xf`^; zvbhE+(_nBUWw{1d2#VBA#R9Jm=o`;?a~nWz*-PBP;ZqQaIU4qJ2%x)I;S9FkycJR! zECf~+>B#0F09KW$uT{~nsDvr}Ymts0#X7FtuZtL*o8Yk9M=^TkJ+hx5NT@2F$%fTB zF+J*k>nRd(v1(_LNX-u$DHkHN6-S7&nVYDk5`@Y_l{mUTHTt#W?EkN5y(LGkxuo*^ zV2pHnjp((~xHT<1k0)oJ4kwL44vrE`1-rCu%jO5$PZ!1%X?uPlmYanqwD8w z998JbTpFGX;aTRq@T1G1h|;vc5@YhR7`PaJEWs~eMjN{N?KWM}7!4Y!@4>bNB^HGsp@E0L+(=`_lqdga>pXgtB@gH$NF5!QV&%;Ji`cDar?%CQj|XlgR%rGCi8^-0 z^#J-<_PGtm;ID`d7}^L0<2~$7MQv0rR=mgpDLpN{5u%#WcqeK=w-hc`1YKsC_M__3 zx|eS%d=1IA3v6`aYPC`^w!uoNQi7_AuScjTf5lwyypi^Bv}J0CZtB0y9`Ivq4@gxSYWsu~&~q+wFQ}p5dwp1$-UD?T!9KJ!QmR=H z+q7xaHXo&Wg@*q2t?w%Q#45ZR7hOm!Im-uFO}|n4-J|T)-t)utwb#Gy{1>;oYG^y^ ze@RSwVY=~cE$i|T9tF$BkahUmFKR~PBw~|D-bqf3_0JM9#M@`E8{gS%#Up$H)v}r zg~{$e3Iax4qc9-zC|)h16VDNO_^A1bb*ds$DY|GRCtV2bLQtK5;v zV{hQ@y#A{Gh(vUrj9KA=s=lU4&Bx3CcI_2_2BB&Zpj!SqU`u0jO=xVYDI>l#w+<(i zp{J>Lumw%=rLf6HEP~4z-Zb#ad&QBaDJHh`-oiNli2CNpaH=uHWT|!q(u6ALe}=q- zMNBz?WbW5J{_=y)^mfa>CP=^G;fPi1{$%f}<5#sN*?I^_t&g2mopF%Y*RQ!?!l*0x zE{pe;O#CSslZVcGN+y|#1LSk&I?u_hpK=es70Z{_}f3`b*lMl3J z(gz>;I5ifBz-(Zz8xeo9xVNKo6f`>xV6MPO#owY9sm&$Y?*f7HdF8~=sI9^wuVyuW zRL0<~ck^L}a7>R4Y1zhoB{liMr}3CI9-!J*hk6zI4T>(DknJWy3#-l|&wD^YWw!iXK-e?i0 zp)HGgcz>;r*L?a#8}Q3T!hMs1%)2u06ZYFd5S1a48t8W`0~%xogAhwmvv2P2gO|S_ z-UI1VhA)$YAd*ZVY@~As@HVWrmoI?lL9?Ou^h|csu!*=7b?###e{#hsYj((x>VEp# zLchkP1^rxizs9|Vz6(h1N5hf(bpoqvLkW0=M;Q?w>W;2+XQ7W#!+kGinD}SMXsb+= z7kU8;AHkBZCWXeo9Y5aXg1p*3cQ?yfZ8&UW?HbB0&0MSYmcUs%x#$j}l=`fc&$`NdTn>Fq;&|{p zCy7U8Lj1GgH}nusG!Sei!hsYoP0meYx=>bPnOUbI{If<-e|x#{;vR7+5|5uG0s(Dp z78vMPHL;=E_qoVfN}+BN|ODbyxi4M{P^Y8LbUGqT2pD#U_Hu zNj|(Z6A^pce@$ePG`+sQzeOvaRhf|-TLumAa0QI# zpar1q>o0zc#PGUc-yI4rplo6@c77G%vf~*%;ng zZMk<=Sw+1lJswR8c=fUm|JvwO+~VpQkw*Jx;3#+ph{v16WXwDS$7N0ReCU;nNG!8% zh&F9Z&W!8CV|Xx78}fNuKS~&`S?-*|JXlAPuH^U77DYS8UfeTxGuXw1bd+`JRWEGM z_$IRVe|0;J1gu(Jora+f8ouodV-_=df(e4o(&}+%2lqFsOy*2;l6vej|St#I3 zqYL}3M;Pkf`6;tP2c5%}nIaORKEa6?vsu*`!ddkQAJ?D?QGrvH`lJFvD8#aDX&So; z6Dn}~yx`<;+8vID<2Pn*0v_#I&;amEvAQ3#f2aF_In7Vsu@|0F62SMv$x`rDz%4&O zZVVfOI~PuTpAaWcsG?AkiZfKG&RBO!2&tOs!G%8v@mbUS#jO2)chqN_ZkN&C9pd}s z81R-RrEE1L!^Zq}tBz>(>XJV{q63XgDDZ~CA^b0Mq1l+XqXZ@J8XrDgM@o0EP}6zR ze;+Dy`66#rA`%xji$<#qi}~nXoUf5_^DEoU7#DStG>L@~y6cW!6*U3pYhiOELtKSz zs|M##WS2ox4lff${YLbdHLjireWe_He_}POwI@oifcQj5t!0eFmaf}0`ce|=f` z(oR}!t&rX#D7J}s{8fYeym>O|pBG>1!`6!l-%=XH6FW=$*}QsRf!h4^QpeXosS=|_ zaY~yI3}(!9NE4%#LM6nQEixAmB;@iHzkD@M5YzJUTw0fDX=qh5qUG^HrlqNE1TDyt z>gf|RbIjABUw7JGR|(a|JLdc{fB03-L!nzEGaKr@m@30?IveH%_Y}Q;HXP^OsR7gy zIyz>-MJHq6f3n~bMqtpOs#`X{gI>Iqr3&jWfpB@I=OV^|w~ozc97NYG+XOEDMhH#V z%{pb(>$mwd|5DS=*oxC%hwd`eagY{(vXp^{s19a7c@Nl?c3<-FU1|xve;(pxB1(|U zwmQiJ?l0xh4YWmi)-7g#j?IyCE&jbZ`pa#O;{M$g=ivS78=(>wBdFR;uDwB`-O=0| zBR%NX-5L4zaZFDyZTC^ynKapPJ#($EVd>RJ=i2=G+lu?2WyOW7>tNGk=!8;hI06Abx>Tfe~S0F&)PHf|MepiS)*a&T_MS~j$@^Vv{sSH=9FKg<-@CD z*lUS9lDgYU2hn0Tjb-+;K%g8UQN;#4S)B(pGCJmB!S(xCgnYIXc@kP?;(?4l8y2$y zVpK0ph=DS~hRF-dIxCIM;Ba+WTzP_gSsd94?Y66YC+pzNiX&FxfA~1We9j#*5t_RUSHF$QnHLUUleWaHh`UhFh z=CFT|RY&)4@s@Kc{-AAr$A)NneXj-=R0h;{EG`I9BDxT`RPdAWt0gEs&t~d;aefb& z8$lpO)il_01|Av)R1I3`%1xV&JY|p1wTROCMj@G#KCCZ)0O1;o+}~^4-)q~SXKnl9 zIqlgQS@pV=JWVZ^(D;;yIx?$8oe1ce%{0&uxi)|cD_c@mJQ8gCn%i}EmBF^utF+cC z-D!6=!OP>;{H9Iv85RbQ-tLS);Y|rrr!5Bp0?AgJ@C@lR^o5~r$9ot$gTL>Am6r<} zSk=G5A=AHqdlPmp08)(88S%x_XbxF(k;O}k&&$j6;Y+k^4}4}p62M3|(KGG^`wfpZ zVi1=>p*-W@QBA3{gGKz2F6w!~%Z?>JLm8>Cq-%~9*Gllp-sWBMX9d1dgy2d2J}M5w zd%Vx(REN3iQMR1R9m2s2Oop!;l8ekhA+K57%12{=9(4#l$6aG)S|raRb2L;QPM^|M z$QYBzG;)ghjOoIt;uU&V2mCj+vSb^d*uE!JcyxdGQrubeef8~;-MQd}y5RfN+u3*( zf|LErHe@JEL`R>Uz!MrLu-H;POkHsjMnIwD+VYsAF_6^D(ac;iRRfNM@uT)j$bYSG zt>X88sr#P7&gum_xfVy2YgQ$~F-TkwBFZz$p~8Wu4IBJtv6uQHpY=uYP4DJ-kRHJu zK*tj$xbLxEYG+Qk=8fq&vMG4Cs!5;{2?4@+lS~Hyl|)JaEsCX(#f(dWradKx?dE&N z3_Q}=EqhU1DG~Hiwlpq04T68bmAO!bhkkp1|A9r5_>bq~9-hotdI);wQ4ds`=Z%P^ zn%HgzY0fCm0iRU#f}et`f7APT`%n3kcQ5m9|E(fv|EZ{CtV%Q~bNrPLT3Js#mzS;; zg=H*MQ}K22Aqg>2m&5hmCFNiY$xF>(^aYb+G~CVMq8+&|9nU>y8jzy^Gte#N7B%I6 zT@-`vt+z32gpzbpewY@^71M0Cf9;-`orNc#rT45cb0m8?>0Oaz1xvrj6YzP&Uj&yH zbRxbfPYB7EI%N~h6c#pl64sZ~NvQ{&ea_i6c4S!dz`>9L!w11aOrQ?X@ot~HSpjH1 z&(SQ#4SLHYm$B0TpTl*bXu@TB?93*Agk3g1(T9buJxF1i#OUZ4Dq{~8S(4S7yRYWq z$!PLXQH=8BEA?Jc_Qd5Pxr~;%;wG9zk`C2boN0=BiwH}uJEu~kR8TcCJn(!|*Hlga zc9M|D64TNdgZMP=>-1du@Lzv{%gSS2S+y3J^xnZNUO_EDS$vDO&gKh$$g#~P z#wpR>>H_*TX#!mCUlW*M5(!)oXgepQwgUyV;DqXB->9bHJrDJP;7JT=$5 zt~Bhqkab$cC0R13M>GaU)nm||PTd$_n&hHQ*^+CHfK9Eu{js7_w+})iU2Ue<6~GFJJ9OWgfG@D+r57JoJA8n#X%88ams5DxDMa_qyPW z@H_gN^TGDL+}VKEHGo|fR0WGY&9oGdAOXvQb+S~3&M6xw7I@_DOR_h7Ql;R<76P?{z`Z^*j2Sdd>FzKTofL1T0^z zErX$R%En(yt<6VK*?hc)TJvCWwdQNC@%gFKT=X$rcgX)PZo&}t>vF6>Erb&~C`A`NrC79yoVPo#t_(AS?QgHP-*-;6u` zV#lC5+@kK7>=dCyD_sP7CXxxJ(x*D^Dv&Ldm=wv63bxlVs~o$`*@Fd9SxIEngV*h523lfbWa zZ}I7F=gohfPiFO=3HSgtzs7rfq`=^=b_0fM{s#g|qJ8X1S~a}|R$b1qxjttJXjW$6 z=!1=JF=L^BP0s#gJcBS;cM@pkfPFU1RB>-$=>q%wm8m(6b`vqH|D{=kcvp|KwelnWK)}8f*`SZ=!GeFk}l=<)(0j^h{KCXFmK7r^C}zRG4!M)J@H~D5Vsr*G>^0?98-npwNiF zf9amSjIutDNZD@baOBakU^alx+{jjXZ%E9|Op{3`Uui<;_V@0Jvp8U0Sqi-Q=xS*% z7@J9f4|?I6;;k?U-j)q9tuFA{6p69KS?GPC zNiEldF`^Q#&)8+v!`-&Ff)Z1-1f;YjV9UD!NOQ>)&wO?%)-eQKUmw+ZtcyFT6AK4_ z-&|;qHL+oa;|KpBVl%{x9uK&TKavp~QfYXw&|ost%gSdlQYT#+C7a$83lTkAcuL1ELUr%$u;%0 zJTxg4hD_!bjM@JPf2_g;mPlr`n|Y`$9aP?`2Cj`HdFKANQpJ$2QJFMaCfK^_FN=UK zLPqf=DZ=6U2G0Cz9qr)BmcDvB%}<77HEtD8H{*-FN3j=s=}tU+K6am_o0I2%rH(!0 z%!i$YSd?GDGATBf^4hcM9kT@6ylbKJalypU;jFPnV!8J7N@UYnsiaAZVh~=fh&R5hGkDBppD(G0bQZ zP1{X`s~Q*PtG?Sc$93b5a5L&#yTI1RBsci{jud@@2t=)1bwz#ouWxw2B zE?v-X#F&QJ{=VWS?fc3!UAAJKtCZftRq>t%(=g+7|F7w^()IySfPpQJgBi1 zOuag+(3=#O@6@yoBVDm7#8*bDg!8_vbJ+xoE#q#vxsdw)#YFjk-gSE{gA&X0QFkc{ z2)#%>m{&q~MR$m2ah7^+Fv5ap`p=6nK)alxU{jD*-I2wmth*FNRa9|R$N#eM%GZVn zmR`%qLX$#}sUk`|M<#m(ruCLFH+m$l?=dPpv>Sn!@AdMe)(B>bzQ3p&gYf)a@9og`~=1vAn{CF$=bHwQM-NYC+mW? zG$Jq_AE!edk&Vf>-We;(WbdNy?N{TX3&x>h_D`*B|9rN8qUOV7YLet&h&7&q=my5e zq`!Ls(>>~chL#JDg@+T%#8x)Q3$?#sjADEp;Y(!^zS4Vbnx$$ahbM651waY5jo{fa z&Ne7Owwad`9zMcW`pQswW2mUuZDBwjHSOQyrw=fnpAiBHI7}GKVhvQfq-6Z_wp0iBHAKmW4@zfZ}m_2gf)|6 zL}~pS7E-f)_%gScNnJeaoTLM+6Xeq#2QKKE;j8=OP#P%viiEL)xA(dch&Hs zm2FsmZc`%Fi(6z<6cD978a2i&=P1o7ruH-koU#9L>YC#<`(BOay=ZfuEh+-SeKx#u z*O8?`=QD3!wJD^!KW&wKLk%Ye(05PzJyjuS;8^QT@SNT9 zjq%)lUMkPct=)DEa5YK1c@@v8Zk*@(TM5s96Fpsz=gg#z@!Wl0D$h;c#C8mDHA%dA z70;<|oag#m3C|NfU61GP;5Ei_`*o=t*NGI{F}T(Au+~-l#;S34)29+{$Ge%E*<77R zmqe$%H#2>%x9la4tsma1hpK(mu6uGZQXku+4^95l-1-uQ(+_sNui@Gu&GFBCbe2zl zI}Hrd)zMl3*@DpF35MlC{F!?#03W!}Uob?<`{XUosuqSwHF*hWF#elD;@T9Y9Q)!o zz#zGH9w~z;^hhxRC>u44s8Zz62p zL{{b-jTg0E4lK`CG}ef+R`NC zn#e~^%oZ?C*1B_8Cwx;xd&WmK+03Ht4Oi0_NVFibhk?RU&>(34N`_f{|7sZc zSJRMU$-FVrzLp*HXBnHDW$JPa4{tYI;hz}`pNZVNW)U3}*(A%y8-v~&^+w}Xnz~2e zv!FmUmWe|&CZnnYv*EY*Z%76O;1n>4iv?CN3`&+VlfK!q7m3I44ZxEjy(j`({*z0+GFJY_V8KY80oU+J zmOJFGc|gpB(mNnV(Q^mH6dBNo#66v-oVi=9;Tkk7^*nXv_H-NnP=|N4&N_-XCKV>v zK7}y-uJL|}G3!($G(s345pj>x2(5>~lheI85^w%S5gXq=WMZKxhETem`%z1i9lkPu zP|JGuwY&e0S@Pi85lf_k55e3(K&F4?zHRc$#3M27EeuyO<3HrJ3kn2~gzb)tdb9~@ z0_IqWygro-)jIcmOK#sqmOU^1d*N;;AB+U7d;4I0`G!vrRj)nrw01ZTW3?PeVpCx* zIt1S%T~1lW`L2qS^}Z!x`zCBMMwL-wi3!wKBFSNCibE*d!(4&U#D+|B?Jb(ruq>rv z*nMRp!$s2=ny&mTfYrLHtbMhf@(4|6sYrT4Z!{`YR519|Y(=@TwX=F@h%KpWR%A7f(12971M<q+;g6q*)pYOlY!qA_j55oL_f1XWDlv^sZO11>54nUN9Dr+a385m7 z{7ZSrBg#eT%aa)^CR1cf7n@m;e|V@Z>ss3<_r}3QP0UgDE(N>FRw1R69KaNz#1}qDXeo16i%-I?D1A;PP&O@F)*VXRHk|(UCCu=so-uSV6W{;*k6%x zAhcyYru|CODU+ALCnoe*P~VtKX%R8y)@)i<-l?Cv(DUTi^@ zljOi73LJkI1PG>OhY0LdY^=oH^` zW@=F{!bu-=V2R-H=U`LlthMq};xO3b{@$dcyRP_nIwR(PlMZ!ah47HFQXdSo2v59z zjY6yv8`6ylp-I535Exrcii>M46Rq#`CQ26!i%y+P$UR`Pi8bP>(PTx7oFNy41EYv4{Dy84K z@{SQ~Sk7F3%l_$tCjuIiVDZLz=HGr`DOXS1v-bPsIjMIN3YGPv43T3~N*oAvF4*^Z z7E_K>BnC^Lbuuj6d8et(kZ6jH^kHAd##50U}(blD5 z^?&;{@!e8H9vZM1Ksua&OI|+9PYXY zxRv!|9UulR{HLd?G@Bu;?&bVA_Iw<>F}QVqaRdxn_)h}IonE0q#c^BZxZMpHNXW^- zdYO;#;SGAz$v>`rnV*dEOEu{p9yY!kt0jHAG1U!}t~+dHhfO?zoJ>Z+8S5oGOf`)f zm#yqFc{sc`oi3@r@9K4U@aa_Tv8KcRBHgvJPYDV?HI-!zkGPn!Pi08#C>!DC5YcCU z_?d?cyI0tZWA6O~XJQCG8NM0L9xL87`jVQl5||g0kI4bSQ7a<`(M5Mh!#(Jg zsAk@@@d*ZYgapGtNP>YtWyjvWds~)Ye@HA2i9y*d`rWhqKhG!NjgqL+9~L$+S@nty zRC$|P66nt>zu#U_J^a3ZvhoG~`90Fpt8t$0YyS)vX8OII?9;%|1V#JVKcQ#tHfbdf z=op?zC&=yD^gJiNGiSqXyqa=50-c0S%~SPn2>qykY}(ZIjVUS3rx`p)WwcToi^7^p z!E~{btZj=~3-=icyFGNduUFU>{)ifgkq@Yg~Cv4ktLFH`N+*_7EDkvH=uq-_m9d>|~+5P^cBd0$zb? z`0oY#>H~YSs+DyEs~>(mVufl1@#L^iUD}cVdFNoa(L{BHAB?jX2*N-0BfoqpXWEH) zArEbRd^i{;armu&Xdol>ib+hd>imGI^Lh)6Sx%x0*%ftlC6HC~hKj>rAtm-EqM1!0 z>u0BCN2?eoNk6u{`166nao|25b>RJ3h3kMf@i>8%FkK#vq3!1QIKjxsf*$9bSki+9 zd|nPS4vqons^r}?zsQxH23@gpHBHp&ag?)ox&RMTE0Ugn<>NJY@YC@}e^736Xbj^D5hKtNJRG`6N;Y#kWHGMU0k@U1EV8(VL+WfBiG2C^ z2CFFLVGj>dPbR*TeJC4&+8Y{!>r-P{dRBb^;SjvPGDn;h@ zYEl4yJs&-P2S>#lJlWbgpG_J%Fs~0P9>$esk_i8kNNhQ}AY8;&Z)V@qT5%_n%9%6H zyfiZ$56+2$xNK`)S>w$Y1Is4tVB1o-0Q;OwIYUreo}QhVV6{8!)_MS%rccB%++OX8 zKC_A9dfsBCyhaw|y&RroM%TH9N5T{tOe^6a!=SK#gbX>Z64I8aX#{j{oWl-rIQyjK zGeKs<8!|+M{$nvT2&VC~y(&I~W!O7sGb7P+wBzqeKnTHmY4E!u!e?(@K>Y z3+3Z*rmXcM``+wE{4Ibp^3CqbIAG+~&>PnCVn*fUa6&X%S+0xpa37dGQJv*Q6|=$6 z6}1K7y7SCU>adl$VR6{v=x|gGe(|Mw0T8}_{PS(8F5mtI?>aFdT0`BzCRV^|04~$0>16R88r=s3} zN>q=n8exOxu#cS|2DeOIWdgqII2ZnzUq-wNQI`YvC;W5wzg|Dt`(^L&fb<_IylpTt zZ?AUN);I3m|KY)pJ3l{uvitNlYo&Mok63f>tMLRt0*vn2(aI{`P+e_hD;@l+qyAdM zzt+@W>-g8Y`fCIK+E9Pp!@usSzwYCIU-#8tKj2?KsJ|ZIUk}t@KjL3Ms=vAf89M3F zpU_L6{)BD@^e6O_)1T1M3H=E@?KlWOI|z>*geMNdu7mJYLpYX`ODALbs%{l4U3yuY zONIhBXMH)UlA);d{5d4&_*?kEoc8)sYv4SOZDe3Pb0Z2*26??25Brk=Xvk=PdHd(C zR-al`?EUi3*9Wg&zTE$1=WzG+uY1px)>rjjOqAh=9KW~r<_tlw+lMr${KK|?E`3GbW?%q=1zEE5pG4J0eyP@x zf-~ij;mUkW(Xpd&rUuOB-GWIhyA8f(ye;Y`{77r8tGj!N(gn^&!1ju2T^XcRTis5P zkC)JNh2zxt8vqLk0UvUd>731MNPxtC;-GG3Wn(A-Dnmzos)bK~6u+H=sF3 zgKe>F5P^vId^=ZviTA1!uSBuYpHrvpfeAhCx#T1OU%UC?0Iz5H`vfGNE zN}GqS^kN-%!HB6Cyf-;-kA=Km6l%9HMNmy;Lsw}}ua1KYh*b(wAcWE;FLmqo?8AJ5 z4wr^cTN;eJ`)xHC#)raRtP#@m_-)>QpAVADo@!UPxDd5}TPt1pyrs{9VCxFp%6dBL z&eVR1_2GDh!cs(5b*332hu`GE(&m7dE5nS=-TAEneUPT8nIWD4q?(yWW+?+-xACq~ z5jc=6w0L?}Mxc>Xx_NJj^uY+w|`=hct^weY~$zpwRbEQtJ3o`c~X}+lusfj2y6t2YUi5EiMvSWupmj|s;9E@W}>DDb@n5cXnjRC46Y1^EUzNnN#Z&6_?0U=l&Ky0ovrdEGM z)=S%dDJGmiy%M!kxA+~M9=qjl84EePwT%bTkKBQOv|eqE;4HFiAC=_zI<=GDi$?%!}W#PC`4b7YY7R%?_eRB zE~W6)6X7}MmeVwRev&{hV|JqTdTkofXuUq2%bMjylxtdJ)&W^GPUqLkr7RLwT+wvQ z!hM^6ad~`>?Ydyee4BR%Xe~o%-4^>W>kdcy13zM$pI`vgq8BlV=pSsEsj7) z%fj}R1{*EPK~RBoN_Jb>?D|q&z`3sHbB4wC060>z+_T&dSpTrR{>-m`fDLq4cQg#D zV>2}9!5}7)4RFxXRryq!O9XW95#xrtSuEmz7kY{?@5{Chnn|+W-^v0(zjn_Wfgh)p zT@(uwVz;#3tc&g*3U1@mogl#Pe0)L;^TC|^1e-4F>O#%y!Q|t3Hi>KvSO+?PX_^y9 zL)aJvAPUpa(8yrQ6MUd(oL|n$7Xv^#;!%T3N_NI`w1H@V3I+lzUsyQ+ETg^c&_JPo zb9jXI1vwk%vbv*^D-=UQ;5|FrPTBez;X;UgeMhOD+zIQ|X7CMn21&b)5U-NFAfp=Z zp}eJSnqsEdl@~P!w!#7PZ|QyEBRtP?T{PYC!@rF;#vBa%n|WV=fhh@;{e4%bLvaA1 z`Y~r7)>fzj;(K_KxCM?M9S{{NNatgJtQ2);l5ZJ=nac`^@m(}f7FFubvM>^7TRVDFQ%bemK z9os%i*STa@HJzNI)9(Y?tIm>l^f&$cAa;-UaPsQ#=>w+if=h>rwdcd}?7{YbwoF%a z@OW>JT8n0`z7`aDX<*2&E$cH>{0*zW4nJ03I%^NCIx=G0cfhbkUsQ(|6|n?6Z_!3k zYI?Z%!>R2R9NqAqWx%J-{Thtw+)r|T`V=j+ zwy|XjU91mAq~P$FPpISC@vs*B6ojZi;z4Zewmo{m;6sl6t=Xe3@yeXV&{ecJ+jY<* z2*8Ruy3aav=sMd8f}-#&%RGlmI5v9)-QKy_B>2fAeK}lv6mV8tXzI3q>~}Ljd&o%) zjsq$nG;M=_(X5lZ&j?^io(Gi*wkhx}UKPUaL{*5W3%An1g`G0l4f$g+Ps_crXMmVU z^AH8pA|asY@NAk0N5Z0HY&9B|sqhbvwp?s=?Zbgo}Mwq_j`He!nLZo^59U(HS) z2mnyP!@k;4JB;-zz+u9FOpZtY9JTy8TN1rajq?I*I1S+XYi11&_3iQ#kZkI=vK}Yz ze0H+FhIb|W2IZSK!7PK430vj^78lbNb!<+Gb=z1bi@9urK+agxn-MhCfhTF5`!^_R zU{Uz}&LeDd*c|hUn@4vIdGlI)OM%lilGz98pZ=VXpCtMzW6H08XAP)VUn3mVolwvL zg}9X^&dn4GqqGM^-~Q52);JV=ngw(8GjLBP=e;O6vlG^9F9pdiEi%?X5Aw@mlv*$; z>M)=@*w=0a41dM6IT=oi*>966`dQt%51Kvh+e5k-a8KAi;`9A`_tx)~VxQvoeAurE z1xjP{T^%MV?stxVn{{Z1PlcN3M29E^wVHiKl)-+|D7 z&Oqpz^ytt&UyE&n7DFg?Ht|8eZ;N)fMkEThLZpTV3zm@7x!+!0x$mch08dX)xcljb`L#YYw$LJEX|BPLI^fh=rA+64u_{9Oad)m(ey$^>1Y`9+2GxGN zzX}TQexx#K%8&R!TKM%st4F2fI;iFv3JLhJ+O%4Xu}H|*=S}j^zs;xl7c~6J#V_Qq z#={7hI7Z7Jp+u+m#t;6aTjS`aHn~Us+MC+H=2o0xy|j*wipthjGxS?T<^5inqFZQXDO zj*_jL!!qc{PAP*@lV&~!tzXXz6!5Wp2Yp>WVhHuy;go$^)1Mj*2M-2*Z3A%Y++U4y z7GFtetgYP(hea77&@eG1)KGS{{zJOOy&rWpSL+WVUHw?vRnwCXM|lnLDA7*yNyx@m zm5`u%O3YRD^&1r^gs5!h*<1H*Jt1rxnDe1STZxmQ*c*THtNw+(fDH7y54v2MqoCL0 zpf`NbB@T(Ug}dUm8@X?J7<1C6>RzvO()LD<6^*F{7~7 z_9?*$yV)^kj?PbxPd`4`;G6t=32t?MTvJWU>C+7O(ZJ+$%dnsRe7aU5VKLh5V=zjNEB@@$hi+A4oXx$_@z zb?&XseZY0BnjP34`1sJmk3frFmMq7*0{)7H{&|k0W>Ow5nl_i?vQ=@zf`Q&ZpDKbTiw9X=2hC?w`;4lhgbq{#32R2FF6+JBAlZJFWQk|I_Yp zw9>#1>`WPSXI-R5``Lf*9BwO`z@w{F65TQfWwZ$oBvY3>n>#>MQreKoNL>7~|02zc z>Ex^ndChghhp)C9?rzB|^Ky_~105s|I||yy94l0PFfOv$fN_ZneK^15v;Apfke_ss z^@kRoX?oh7_20tcXWpsoL!N(Pm70|96~YVt9q?|5&$^2!5{G{iJJt;*5W4WNmF;dX zhSR}$zn>R{aZV?ZGXradC5EFGOAkp`x)_Qey4A>)VWzak!>5n8)%5wO=AIQVCE0hk zv!{<0j!z#8+^8a$1%-j=PY=!dJ1<+=on4qBmXkC+UcwSCxCY#)J!N$1T(hPzwG#0P zBqDe|NC5SELSld0B}`=V>18mVi1r1i)JqGpLN+vq3o-bjie>m5GmE5wshyX#1T~5b zor*Q9Q6eEOpGS?kCr=b7fBwV~qB&G={%9e42|_l<6bgVE@qM0u+y&^rA@p4U2}Mob z6V_RLTx@AQPCzN)qdulofEgQ_|G;KF~%!X0$CnT+kLlNsoFZR!$J=tsj>C%aHyq7luR9r14AEfg zvPDyq%V(Mkc&@WAE!ert*N0|_GDM_|SE0ki<9*@EpO~a(xwcbvMbFih1t;suTuU=w zmi;MPVFDOL7G`>S>i+>yO928D0~7!N00;oGMl4v9^W8TNvPLXem9lo;1Kj`s4ttY0 M-YW+C-2eap0I8b0P5=M^ delta 47823 zcmV($K;yrGy#wjI0}fD20|XQR000O8dvT9fkq*xedvT9f(mBbE>)ZeUCwj5#2q1qq z8}W;*i*CE!zM*>5!j`T?3Zb03${}^3Pc7k-fzNND2PRhGqpd!(IAA7*{FZywm8t*E zS*4+agxs$v=f2WzoDZ^QgREhYwHRcbG02)2WDV!s)F5j;2;bM3adKxOz3Z$mf|DXY zcgknQwcr8=V68yx`6M5jm}nJBRyuz{t!qLFkt~1eDLP%wUR$AAuu@Z@_i8EhhQ7NC z0+0Cae_x&EPpBnxFfbBIxTjQlZyS}y&_uAMFlyCM>D#T+LkF||pD2e4Rn&V`dTtfv z|Jx-`$tpcpF}K{n{*PL2P^I@DmEFEdk2>v6<|k^Oqu-{&uXYU|IhtF;$1i^qyx?C` zm)}&+ydt|@IQJ#HzJQ1Z?5Z7m1fsSNA_aVVr?`A!7#Oh4HGi^ReBjq2k{0A$EDS_A zpGr>>W)kbxx9z?1KE<(|d&XCRu}p?u@-Fk9Yw}Ako7ZP8opM2{K5IF`7c{Jcm03{K zW)}BQJq0P9*fk1kCVMr4SOYIk(ifUp)Y{ z#Wx4!B`<-!l=$f;4}yR7q0xq_kRNub#G%;-p}hjt_04iHDChI(tR{bju*iV?@7nBX ziQk3()WV)DKCS_@28~DulSR*+ip4$iv%6Si{LQD(gs<-2@G+%2H>e|SkrsQz;Toc&1s^L^5*q9~iK{oX(W{iKB2@^h)xP8v&VQ7XS z9Wj}%@V*F_lc@M(e`+?!vuK*D1`|_D`5aQ~!AX5rm$2N-bd@82nLPM6mwvr$(!Zr< zY?>9im81*>#!Jfhw+<7>@$Bo@(M6Z)l6jajLa7C~E%u71d}5Hrv;&{=mE{iVv%YJ5 z`5%uC_1yw53-H-W8)FK4eqU(;6d zaoPPuUR$bvMT98y1Xa3b-K@RxZ_%di%YFb`g|-kF4!u5OdT+2OHpwQvs1}P+`NL#b z^(L=+3p=6o?CF~y8oQ8CvrrMw`8n9Y&6#hf43_+o=KO!VVqShe9aitF#S;xor+%(i z^XqiV2^opHQdw@};<3J;O)r0}W^+C&grpMDy+S{|=jN##q{TPaZV%_5r@uNkl_zNd z6gVj_dWw?0LjBE%VjvrWu%^IdlZ)o`NI!fI3(FF^)eKA(GtA6X^4?R_T>5|f0(zO^ z!_}O_JAZ#CK{#8utN~_+)s+9Ab!RyLKMS!F^diMY+!h1W$n#!Ss~ZA3eyboc<-?{%=%zjBh79PMehGg;Qt{4DY&w|zt+#e>v`-5!IA3k4 zPMNkuyN-M6ziyyIjvBe6-kMeTdg0FI5_&{3>zT&E$ybM_%t!+IP5JpnIq8t|st)y3 zG-01a@zKLEOoBbxQwoi6HxJ=%F2X#VpPzT$X$?2)cl6`8ZM{5@>dui-duCSiIhU_5_{zw zKY=9>jJ`0?kPe0bMFJy6vg&(Umw;e==Ba-}pryf;b3TaISr{>YG3Bv&$IHPS~7*th-KseP8RNw-zLY zr|EF`L`O&BVc^So$q7oy$cqQUi$;GGE}VrvNS^n3yhaC&5*a4=(ZTS{n3@;;XmCwN zgX=^zC@kSs`8lDYSu>VWTDuM9)bF3!NQ%cXJ$8GzmjOy8tnQ(VFU(l*!kM%r93^)a6jp2|8rq&(qY#?laBh@VMMrvpol{A@%SGV7= z)#H6G%)06?cq9sCxIeCBG4%xg<(|1M7Hfi#Uq4i%(z+b2ny_wFZ?f?3O*5}n*dE|d zXyO^eecu@R{A+%$K;$)O`U-y>@f_MOvbW!yPaiPF=rjx zLnJ=zOk0!|Eg}%Ba-L1+=rWX>H$|eFi5^aDS zUwTrE*p6y{(POSAo(G)&`f@t_fzkM-$0qbanUQ0A;wA;3&oPWe!$yCvS)dS91P{iz zQ7XkOnw%u1Q+{WmYuyoLdseBG^^wDOQAPbLAy)o>JgbXWK=>U=gojhT&0~!?9u%k4 zQ!KcJ;bk?^-h_-fsH2 zm>b;fbp4GGYcria{a$~CZ|cQ4zgtA$|Bf?Np;LT|Ov5`SC0aoWe1f7>^U+Melk4HN zhPZpJ4k+P+Me8GPViy{pNNa8o;M9tWX z8x0n3vaxs)M1qa~YC7Q?6)`hSZ^9W}m8uF0MQUl~tR*>e_H|O0jQ{@>+u&2{LO!XdWBk)I*W0YcTrdgg z?%Ip`S6-5a+mYPbu;W|(6$c&ulYxZ0W6UB3Os?33ZK8jBrDFV1(buMY@-Mvs9;y4) z>hkHUjvFTBugnGM%<7(Io4LtFaAVnLn)7Npy%ca%Yq98WdMEsS8&xx)7*JtuuPD)e zF^0!H=<^9-NLU_C2{|SXX~=)879Yq-kqkj=O_Or{G%ACtD;KQpEx>3t5U>&X$VqsF z8>cC{5i@@RYaA?kh%BkeD`M@BQ%G{3m=vY=aeIH(Aa?AjI}6G3S371k8&A0Y(W#cV zds+;kil7qS4*I3^C8Z5Dco|cnwyi=aXJjdY?jhC6U zS>Tm&Fq0v?wrcL+=B_&h1jwuG$6iLt#QR1|6saY>~huCBZ^F2 zaeXDbauDiEExa}Vx8uYMNT)&t{EhQ>`~;I5E=WXn7$(&OBZ7Akn|N!5c^l|8U&=d9 zSRa4AgSe;nTG^irqG;M+ZGT~?BXSvfxl?PlT4%G`~_@XGPZ^Jg$Z@Gya8@XT|tv7Fa?j{W*YYOF;jsLb&s2G3o zcbP&hU&rxC&Y+E9b#dX(i`wBmIdeRooF#RGmU$1>hvrV5Z;3RPGb*1@6((EEsA*x} z(u|5^oIj(sTon(`pZ;V^%%~iR-+e|+X&Es=rj#qFE&}beS~*jz?I^8&94P9|C*XhW z2{$f|4JX`IaKhc&V#3W93&T1%4fB729~AkpK*ple)$L8rEoc7Q`y)-xLFDo$=Ng_X zFgbe{e!iRzGjAegLzKj&p-kC}v*ORw(Wr!JfBuj?@teJvzVE?deEw>&zAVM&D(hOA zWB2G|l=Ar0hF3@G(d=XXCL-Z`!+kc{%hV~8tV)F`T=X=XD8shm;1wUpqDJ1*Wx~ zn8KZ&*-v)dEkEp9T;)>EW=DA&#SJ+T6UM1(VbFk9{AqiyG(0kRjTuOCA6dQD(jZ=Y z!orFn$WmHTR|)v!iNsHqmRJ(kmqdCy76O?G_vo5&3VgFrH40Qon6rOcu!0I-2`KK9 zc+fF$0697|N`*NF7%=GphAEC4MM5qDY43UlbFf2dPs1Idi3RU;!k<5O-Zisz)Tf7{Au)*}65w%6HBg1?Q&DX0hZ~_AZ6^&)`oR z_L9R6$x42!Y(?Is_ds4r@1frIA9qyimDjqX9)FGDkkS+Da|M5FEcr=T636gI3>ohF z&U1o_P{)oQF+gW*#Eu>@#fe+Ih){e;^wo=p9&Dx6;qkLgHhi0W27a{-ISSLaW{=>Y z89!T_?|#%*!?=231tsXt02kzlKY-5!W#1`3cFR{(dfMlV(BvQgx(ZJqsBx|`64x*z zBwfC)_1(-#N;ZGE);$7~nsq{~iO36wkXg|K{L-W5<7qVker2|n8=gJhdgK;HtAc*QG8wX`4iO9A8OvidUi(0?n)_AjzE9oTZ}yi=#L+ts_7HcwI2jpHX;trb10bx3avchVY@Vw*d^HeI@mUyv_g;h=e_%WqctuQi&0BYdih z=ygpj$f=sd$Jbh{e@J!;p&U1KD=Hk);E)0n`WsT;hUA01_^R;_^D|48)fe>A>MUBK z;iB&FZk0PiwRW49hS>_{ejlM0H#bK<0==oiV$*+`=6X}0E&f@B+RHYE4Y;8TjJtBp zA>7bBwLx9i;BUx$4xRTyJb6s*NZ(=D}G>3I{ivKv`nl*q_r%E=y$ zwp61nVNso#5jAjZFbGPLRa*u$YoXjKpiw9_f}9ke(Fw3Hkp)K~j~d|mT9Ci1wbN0` zEiixa71hc>X+{d?{!1Qhs>1Sw!;!V^*#^#S!blop=vF3lR8l$VW)3oMZX;I^KH)qKbEuHxD^jbVE z?oC#5m}GZJcbd#;S!+2Glqc-dkgzGSZL%`oNaz8X`}vpCx-z#!Zqgp7VUdRjx&y&m z!m^O7D|Z)?FZY1h!{W_iPK^G4U;|CFfn^0aRN5q9|^&w_DFwX zT*()ky5=}bd;@Ln@(1C-eR+1`izW={Ujwf=w3UEf9nw44EAn&gCO^n`p8X{5c3+sNCLkH&Jh z_mR}Vz7QTDvO(@P-g2Wn1KaRUcqAW(!Gr=visHl)VYD`7!OCnwpx_Gpc#y*fHm zpb}k4F*#R2Z78RXFDD=OkeoU(IjytggqWVObk7n{)^3DOnB_{SjU{vz7tw$1h=wpB z0_%-z$bv&Hw)2I8Zly|!C1;njy@6oPq-5Gj$#{2YZ7v&so;BAwWlVLL7#i|0uR z{bkadtzSX==_ESEv~&>EYQUd*=5OUnqqQ_3mKwwoKm>P{F@hV2rR8lz36w!nSv1us zYE8f+c64p_C&l&W-egdY=C6OGfN5vvMXjxXlnCAiq~MNwJLQBfUYnc)Xhpc|b1TVU z{JE!X$@3QriIQ@vI2~Sz^NQ&z^;<5*`OQkV{MRXMcHc!_xZF5=8PTmHqX5kuuY>2*2X!aJN`H?YgY?RUi8slk7M@`NDGTdcXX zc`xzdN3o_a;AGhI$)cQ1dThc|hZxCIlDgTZ=O5wlWa!chINB+7pj7u=uwOuwIeuPh zL01<=S-4kU$s^F_PK$ma&$u$Es;b7FzS;Y>9NWKHwGWq7ot^n#h|p(_DR_|!6x=%# z^eCX@nPV0?;K&Hb8^C{we*`xo(GF|SiLt8#koy{S>v*?rb0Qz87xYo?8()lVqN|U% z-L(_w@-qHu=6;+B^<~_#Wb87kwv0Oo8Jhuo8F!*GZgU7Fb=N@Yl_l_|ZDwBdZ7YbH zFw4P~?|a`w5?G+4+#yuMk|-(G0k$BCQpd2_RAd0YMqG;Usi1$TjZoTgg@Pe>6y%uC zNK3#u0^Z4yK&QS0I$8qRxMzS1+JZGeL6I0C?+uF)W+lHky5KdrNDu@x(+W|-XD?YVIN?nVC!{UxAKF_5wxa@!N$7n(0Tpv*bg;-RXYr3vKF#<)x3^0}Nf)9rx51Vi- zCNk~tOkvp#xSJN>jIp!{2)i3nBg?L)B7y%cDMw35M$u{ONd|eF>IoXsm8mVKY}qbm zy}<%z3^9LDT(D;P!m>UM%X*hwqX1VppE?$6y8O;7ud6M2>O;ZQvepF_Ua5MF>slRd zT(}bN2N=_gk@%O~)-TnEu^ebk)IT+Ho zIMBHB2fVfGhX-E#k2k9O9E4uM4(ymP7LyUdmBt_yCHCkjG1X0z9Sl7z#?*-o0dJ-Y z{q2HN4F;#oLNQ?89oP^A4v5?M!t%5l%bPxpHeo9Bgs30y83;MCC-2iFyWDuNm1pkJ z9Rh#NBx4fDV8a8HY!1cH!3yPcsv8!^bTj2J($m7gb&9}6v&H5+5($8IMUHpXN}*%x zqzg)A&;naD8)6j)3sDiTibJ$F^hl@--N(9vi-|a%vK#5=SRqG@ZfHKvFXD ztvCx6qqy)$S(U2<(eNl#m5mTDzdGIfUznqQ`#yCz6zQX+qrf79U4A`jcPQondJFB3q=0w7|@ zjB*Yi&{_am7iVWEoQD?)r1D^Pe3q&>p3(MV;u-&z z(*^&QQ>p6QOLwVnphH5@cHtFLmgj%-7bV|0t-w{AU)<_08r81jxY;8H&$&OvtRooc zC?ZvCjp#QzJ&Ohv)+UPG6RUu8TZTPUlc&GK>kreA&sM6{SsbrUV6VdiC?A+GC;=EH zNg0G@WTB!PfwTzl4*v_({KS3Qu%U#;lFhues8o*&3ygiwxwB;`QZLQoLN0F4rC^M9@YfMP$HyN1B%j ztL=F=NMN6y-JeakQXEU)>)S0`fVMSm-nw>UbpVD zBFTILE#GO?c2=I3)3=>$?!13uURF_M{IeiI)NIhZh&EC7PMDgR`B#xPBlND6OmETz z*a14{vf*x2EQN}rad_@b&Wc7~YR-;z6^&S*L`?%zb4I8dxnE7r`5S87Z>DM5gM|2@ zRqgEVbuEbup=@U%ZQD@GmZQ;6%LVIiLa>$m*G_fhlp0d`pEiBU>}P+OlJCoVN_TOx zLcQ3P=h*zp#lR6;>NUE6g$jVwM?AbD1P?o<)h5CqHVXRIC3kiafJ<6FRNM=9a-myH z%aVH7(1Mw+EBnmWl{!2XkhEhdw01f6;_?2*FLT&Hdp6yK+7@@ZZnQQLuF+%L6>1m1 zYX}l`U#d9^TJ2kFftY_SR$yK5OU`F9S9sY@SFU#bDwP$gx#-#}|CSYD#wteOD{K~= zCuc4oH{?!sIEl7@kQmK+j{<)3hHR&E(-{oUBcc4u3Qop;vmI7HE+@m@xST9{Bk>tO z?rVv$vv%0(AxNR~bGUGj93Tac5o8XVQ^;l;QAW7ZjZ|w9c3^)UE(jZ^wUI*Wh^}|E zs<@=dim%gPLzVk3nO3+_CD&~db)7?#<9IWuqjn;F&nY$}b1J@=>1b+$UKNN47F_N! zW9g@kRFS2W&{Ju)w~viq5?(31v+mY6s;%;V1Y$rjut};K%Q;jrG%V;i<)nshr#PQs zoH=JolyEG|%@Th~jnS?tO-SehQMkg@t(n>?XRTgMrCRF)L83Cq`|M z!wPQ2$H(%Kee(vZJ5ZR=G?Bh18N1vknw;2jb7dBSLC(nmQ|-z zx|Wrv5x7RCRol1-!`CWf#1{BmbLh*=QV+}}1zwAn)Q6sL?Op?sYoaeU=r;6?2JFAC zKVom|7MeG@#!vEQ@RQcPZs^1?3@hcM`iI6hPr8W%!vb*P!0^w})2`G^!;w{GB3mM! z93@l@MvZ^#D|0t`mY6qq*_(f2THK}2*Td$o#g>K|TYjItE0Iuq=Ks0pE-<@fMN3A3 zM$Tx~W>I3xkjc#7GlY@s&GrPeN|(HupB^-$b%FgZwbK<7%Z7?skAsBD)=^NSB(>Fq z&{(685zXzsogN)D2roj_9>NPzQ|Rq*cN^kp+JS%nVjo^S@?RW?F^>E=I@anKb4Aqf5Xm^RxI+73V17f_6>L~)Jla2^ z^lx9Xv-|kq@zHUY(!wLju}237N5=;Te7t}5>|-xUM)uL&OD@Yv4Y4*yP;`1@PubiAa9s7-7M#|mVrRTPw6U$5+ko4wudBcjjYSX@Fxtg6NN>1%Vrh)y`Z!M2mM$l( zmjQ&_xyfN+3SC#4YW~_1j6HwHZ3)bt`?dkLS>NC^Df>oF+rfRul;l$iErtkGB% zPo5Nf5&fs4dw2*lGlOCBYW)ss_bA+~3(Z#4`}2Og$>6a6b>D@kV)VS7a?&_enh-@9 zkZI5B*DHsp#_GKNPK?_Mb@F>!5Uu&-40I4qf-+oYi6&q|Fmh`8!_#mRik4P=%l*8k$ z_4r6A_kL8lePn$NciOnZ4(Phmi&82L!_|7bFKRgVmC3b$1Hyj-bbkk_kS%P6yQ>J_ zmxJlBd^Va6J~@cfUOG+*;k%7#`gDbm`eEWBWx3ZBd-rLi4jiO3dq|{&lm#jTmvY@3 z?rPB$5G!tD%M?RG8%cfc4lo5L1c~ycs)cbqwyWD>C_)VRN{u^P?7LOEJ)JtSmCm6% zY_nktiLQ|ZZm)mK!E!dQzLcZ2Z$$m5zNj=GyfKw8?3HE^i|QqZt?TyB-wA%3tcAtq z^M?-)-t8896pH5u4xX}8#1=cK2%?%Wa8+-zU{5WM z;#Y0GG7{W%J2LWk$B*of1G@7^{vV95*G#-T|H$~uVNtxVB=1d74UB<&=81d)jQPl( z?5iiB@m#X}jVzp3n2=mB=F6yI{<8r-yz_z1I z$eM>p9yEd+Wh;I?mr$gf6xaQ0QEJ17ls`sL7nY z`q{IWk9y|pwV#~5`t?eQ)+UAZIUI)Y@V1|7NonYOs$Q?7MSO zU(J66auUM0(oOdz=lU?o?5C%m5x)4&oBdIFJKd6hm4FqnjqZ#=A)(5HhZ{W%#%kiVF|7; zC(saWhynV(e-Gq|!byKrC~XwcxNUyn*gng=avWYXmM7=)Bq4+-!Y<^Nl(K(j z44xP}w16Xr7S_JSX!RUTWVoRH=g~{pf}1HI&=75i0pAMUn84zGxIVKK9!Pgy0vY6@m0S z(c8|#6R>21KxxB?&jxz{1Bg&fOqJ7`QjA^tbDmpJ6)If`?h^?6S0%n7^CRNXP+c%l z9Yr<_O=JP_Q!}`RYb6>f#f%~Ar3DQ$vNDcVb1#)-d3fE_t!s>N$SE?jUqXM5M{tP; z3?%PFOSzQ4maP?K@o+*m4y%utI5b^!;*F9BnRg4uf|3TpFvwK^wboKNzM3w6_K{7j zwb1rVW2 zSMvyGpGv`I`%%Y#1Z-y7q`4X>btT!F!Nxr11oWnaW+gP^sLIAz8OT&mt@_b=M;&gZ zT-?@FWJNWZi+Z}sA70a5bFQU=pI*$fcSFyE?SaX%9;m$1OseAN& z7v8JlB^YrBhNRqFWICPWxpv2UyAxjNMtGYS$NKtyLl3Z>bI4p0gt5UhL=YBnU=z8N zV2e(&Mc1u_;t1^sjCP_ZMW)@%#cIY01xJ+81b-+ZbYOqDF=yzQ5*aU6p54`q5hJ!z zMO}f>62}z?v)WFHgG=EE*S6JrX8>#lTU+>WCl7)%>BT}X^wtZ%&^vEt!zx9FVIE+A z*3>g2SSDB3(BWs$MzUWg(XSKe*G=^6zVowS=W+C!2{dBw#l&QEmXNT2)_ZQdN~%F8 z)qrr68B2fkZpd@p-V)v8A6p7`j+~WvSFOZrFV1NS5{vV0z!l3#%e%_Z-ILjFao%

mkJTHmf`jdhPSf}Z{OM)JabN9DiB^)cXh~0aw&r=sHe;BdN)bADiU6XSUx_` zExhi&^VM}^6Ek*}byERkC|gEOqm2_9|H`Qh$E|H5YxNy2zi8Bb1B;>&aS0pj4+dkCtf}0A z;RXxARTVYS*I8AyZ($YH-ew7<)i}6liZEqc&36V6&UkBk{x@4L-P$t55%nFcHEJv+ zQkQ?P)+;5X%g)>T*%7npR<-&uI3Z z;Mxht1alu?>;h75S%VnIoN@9xsayT9q-uY_^Ev@MuNuRi+Mf2O%SA}O@CmM5>2gJc zZw^_|?CI}7-p2tIk9RMd1|b=SWkBx~KTp+ZPg&m9<$d_?C;V=IVQwC;>x1nWu;K#? zjr%mZ_iGI|_eW}D0$d}+(yCK8lrm2(>aTgGh+1tWbO{GJ2!+56GBA(NW^$5AJc@to z)+Yj^MYT=?Kj#{qR`47rSi(QvX<|0l1vCR5#mh{BeXf|tSbMMJU2ps!QEj^qTC=`( zO~B;>S%M}JqsVzV9qu>eFik!{lS4Lhd&~`f-GC`BkXvI4HsIfeDV~xde~Uc4PX_G^ zvXG`u@R6rOfduvG#!vF!3H9NfPsM+!VB~~j#M#QZ|H+yuCJNzC(qYB!v->L*mAr-< z2~O4Y)s&&1bK=OK#<=tBKYX(s49fZZe`|LM3hA~*v4`x?uxGzrHz4`3SB==fjsNxb zL&=a}Z5gPdniu2V=wdn>m&5->p4oZ!SJg9o3hq8ljA7F5LkYx?Wv@m4>YsmjdjDZM zU!ag$z?K({69F|o-XLin_+KvYKeB)*rluWgz}j`UHmL35Q6kxDfp^nr;<2?SOA`{> zkWC^VzDzrGs3Qa6ZW`fGu45a71L@}g!hstl|C-vG(3WjENMzK}!$4j^ao1HRtjjKBPSF@I%Swy9_>_DiS_% zknehjI$X57Do>t)aMvK*aS`qU!U$C_L;dWp#(pl!CIz6UF_8rF8s0FKHJK8VA`})>T-meq2J}Oo-q7EHq3&cl=UkL#vR*1IHepvMe z3+s{%OE9O!fnUuSo2yA?2L)xHA4>=dE*a6QS1cjyp8G#chT^@k#DJrhqXS51W}&vY z7+_izLWp&vh;=tYj4FT0M2N-gQ;IsIZ%!#QD8Nb4u*8V2nnZ^~MGi$ZydQ4JFJjAA z-puo`UJyxJ4LGXmb%}ybe|rop6&-=Y@qwyThjfmulwC>-S2Lx`(3R2 z-H7gYH`o2{_PQUNWI^}qPO^LsIrU~rJyC`uHv8i+KeKRQ{<8O}{M(1=s62i9L@m4D zK4}&el@GLTX;*(Z@|1riZp*6FHRAVBDi9~fAloMJ`(b>!SjTEJQDq-gr|@?!Kn1*?ud^7u_I(1G;)@BBn&s4N}iTZ z-(8oyP~Dd~bW!6CdNa_ZFn1^9nu%o-DjvB$KYzY9|k(3+U7 z=3KQv6%jZ$F+5QpBhgQTcLaIO=-YxU6^L4R<}xC-$r`@hE3gwo)K2->iKfog2fA70 zat22xx+!|n3-6-yeKM(CauAxdsLdl3Z9 ze#z@UAot@uq&R4ORf`@eUCkC@6N4t!vQWA5yD-Ni8#y{>;h5ot(8OuC{uv67bSx(3 zVZZXTSr9>_b@F^Rs>ao#=ycod_KhFV=bbpeD`w^e>MGw8;ymVJLSrm;ZW5K7*g3ci zj9!0%mU2PFT$g8esUSbc)e}b(0-24>+(v>K0WW*|EXYJQv>?LRd21u|@=j$JpC>lL zE8wBCmW$yiBZ7s0{Vp+zmyqOcPWH=Onj*GIe$6?Nu@h;Ykjbghj&8VAcs~-i? zp;fRtGGEAvTcRyy)>=DcUI6XpP3}5A&hT-eD9v1j@kfe}y?8k9tnghi?^fdBP9Pqp zG~^E+50lxsbWGLBjj2MxLH#&488L4a2;Um*$*}&G0^r|8SamQ8gf>~BZ#dA1VDW!D zguVjX`kri~ZM5W}UqvPT`P6`)Nqo%9uOdLIY^pNck93&|J1c7(*e+v=_!WB7N)foi0@S`QE{kSQG#!hfBRCPhJuOC!Ls$BLq z5hQm!ZRC9T{&z$2*+32!TeVQgB)@-Sl7&x#?i``G6~xq*s|Ie4bjK>@&0+8CntA6u z?d|ACF!IdQ4Rb4l>(#{Zk>+=AD1G+l3Em8!Dt8?MZbZ zu*gy0ZdiRg+3MR(sBiLQ#lM95x>pL^k@^NU4mMWb&^_39sJ`LL7q(H~dqjUcu7!JB z!MHdZ{-rlsmUKL>n`M-sVPH8cF}1MRpis;?;cJnoTeyLfI;iiT=ya(J##O|RIrBD$!wB~}2}rYG^qVXLQeIYjg_c(Y&MhX1?4Le%6h!}Q{2mi&b! zEj1Z>gTQVjR0DBMca&5F)7P z?<7gz!M!4P7I>zm{rf$4wdYDC1X$RA;)WD4-d*335 zBci#O%S7{SnvgrO2Al7gs#HxZ9C9~fneayDUHusHGn znk?3rrC>+FP4nm;(c&e5ae zeTHV|@X@1#4#S$(3#Kkc?g#Deqwf9@gV27w|LEX|!DHAnpvMOc$&lJUAMi$A<^q{X<5~qr-Ol5ku>7`}on}e)s6{V>Slk`9YiiZ~yTDW9_4Z zcKi5oXTQUwy#F}B;KPnliVnm2_z~;Vef;>Kd-(X6%l?>Aa=^edX|W*~s}8uV4*73} z)ni5!Q_TItqt3wrlMW+|4bR5iKV;lvbhbN>j+uY5J?b!4wD%8~IXrH+_dAacA9Wrv zH9cw{wiyA(hx?BnG4<&@K43(!(T@)HnHICAM{Pz1($c>?fA#j!FE5||{X4Nv5@vX4 zz3&{E2Av~iVs@MTu4%L1wM@cpcywSI9vuYK%5)LvJ%0sE1?*bbjTr3JYsOLhmg6pa z3)FvGwhKYz=_b5|1%wkPfe6}KgkwNV(Cu_H3mj*G1SdGqirFIKneO1XHv_zSs#r4V z`7B{?6}{{=MK5ci=wK~^bg*U$E!HfI7V9u6e}x%NDA-xC0!m;WycVnW6W&u)JfeO!Z4Pl_!qJcAM-jvW9#hg#MQN?~#6 z!0@@%vZh6fbsYzW&$*U0{ZMS&cWLpt*s`Y=lBX6+K=(65;daW@v_q#`rlNJ6Zkc+v z?;@G2X2&|Z?5`Ik>m#yg_#s;pi2M)x`w1Rrdb#*T_8M5C06iGE7HfyBf1Zv;CFFlm z<`19FW<9as7?+C=Q?^j3CcWAEP1&0bKJa@kdfyd2-Ue>E_*AaHE8aHQ%5u(Dk`4CP z+ufq|r07qlqg}mrS}bRiIpiFFy5ysrGOoC*%{MIUW=n;2qropc-sLGl4pjcSzGm!V z%b|6%=$-p#-1*vKuy{LN^hQ6;h9!TjS9x!H$vS)ZW;!naw@6ru^(x~_@1dyf<3%C8 zbNL*SnT$B6|EuXl_Gj;k`_)8XW36{b(`NBO+yKJ8Y`dvP5G%D`KU9qEqbVEuLnT>M zO<2#W#{v=14F2+rz2*N^oxPSAgVFRIN8dd9Pzki`E`ThjY&se?5Fgd@lB0h=uHfdh z2E$>Gp}=o&(YM1?7eXd%94-ge^c}vf`U8Bcg+0~jcfBnM-9!&i8r+SIB)YKyJ5E>A zN@!8RCD>qXofQAgJ=BIvNoOE)*Tb*NQ4cJ@fAyyP95xt+V%V6Tk9(IugU(a_SGhR- zd$ah*lg5~tDSIt`HMxKI`>uaBkbjs=DC6FWUoAYg?qLQtoUh(_c|%UTqFvl-tjGTP zoyeNrFk;8kFXjJNuIB+{m@!v#jw)nP$2<77ZB%kwV8x&_BYgk9WGb}75WC^~1QKzk znk!Ju72J<3AM@`Gind%OIWZ}~vL6DygW%y|EJ)*>hn!RxMf}wgO(cJVxsX=HHH9r3 zNFtWW(5P^uj09ScWE$fp$l&YhhUWN=!}1-;^Bu$)@m%tE=bcS+#b~ZH%@w~*VkIc9 zawwjI)7@HuD7ulDb^~%^!T~`6`lOi5ZQeh8Ub2Z{5)_Y(o)niJw;{9vDaLq5e8C1Q zjL~SN&^yvRNtB+?-zzWv)xld8<>D4#RC|IL~a=L zeDaac5MN4)N!}&%ECRA^oekL(_H0X!+pqqJYhf@~zju83g0g?!H{KyG*yock<&0F> zUHRi5&EoG*Y>Qnpi(SLW5C6(TD{!jtVT zTTeA@h|Y~M^<`1j#yL_XdYBV1VUa@YdHVOpeHM`KW(c*i1X{hrmRWh0DW0UUcsZR+ z7t={K(4(`J0MCEjFSbxCT8ogHor2zZYIRDgRTOPrB;}*dH*9;e1uSdsj0_k;F3a-h z2}G8WXps4PKpttdoCVmrY9(h(zN}j7znz7SB)UWd^F?^E23q0I75FFd)UpI1Y<&;i zE*LcQmt1d=E~DwZSzNH$v1qYH-aokiUaMFC2;hpn>cxLU^|rw$BZji|#O`mb@8<{hM;&7it6*Ex`Ap_*3AFy+^r*?OaZV6<~1u8mh((y2RP`V>McoGsQWIZT};e z#+Y$`ug^GV7GKRRN`X*2|89kK~ z7^*TrV|KX8>=^d#pmpd|lY>J-JG-&gaGQx;nTTi#Sxw4Wi&LPso;1NZNfEVu^1LNdGBZR~+_ zxaXCn;>J#utn^Q3#y<%t;_r-A8nJHtS6p{v4fR*uzu}_$54h$4Ec|GF#g zf6E2;oAR@N9pe93&E{gUt#9jRCiK>JX4k7ZeC<>dzT)3)_okEYXVXg>p7#|(KnFphB6Nuq>&DNsovXjW5v_=CAi!8pnZzeU zf5c|74vpUCM@-yER*uHMhAT>o;lWx5aPGK&o=%v50X?5TozJI(ss~Omh(NQra*)xH zF(0u3p~96ISKQl7f>G=tMjY&ji}~F>Fa3l=O>sq0O19?2hP={fHE&8m zJ`vh~##b;rI^b~;@O7=U_#IMg$cN3t*t~(`i*alOEN4&!UknTnThIm>Jk9~~gH2C8 zmA;(Lsqcue$6TdX?&6G7$lmdbQ`q0^FS*wrG^QWe-%MzH26!{72A)Q*<~!y`4<-Xp zE%-Np9F#Bg_u;|+XFYnsoPBnzBRFC7N`hNmn*(u|BS(7!*c!*?D))8uP!p ziWvFnPyP`8WN)kxdDh`EG6rD|Q_P_HZ`LtD(Yt-q&mF*yvS(cpVbAvE;V&Y5nsr%! z{M2MXA&k04hxu4vH)2Fho2+t*^d`8f+|*S;$ng42tFY@1-R01_4^k&0q(qm44WX*Kl18Pxz4a4%8_8O_M6`6|`<_ZW;9mrO@VHM zwcB9KF`7$NsH5X15IvORpf_S&%>ImUSujb%DNiPKN zV9kUmIw3)Rv_VQ$P(caE`^rFn{b)m7hoCyDb|qBJz?WLXVk}qNfleDp(ZE>!s97(i2T4v~HB6M+%0uoC(%ve6i5)%PRk7O@)&;sX)hn2taFk28xnE7}PUz5X z${fr!B@(LJ&NlmvAjbq2jkm~b^srq0baDE&adx(A&+A`UsLFRu$PZwCDg1p=JZXrK zgK_^0r4mlm^ASy(e3q$y#4aq%ZubQUvq=xZ83&9v>SaF4?9X#6lC(8sc8*aL+eebE zWo1BwA5-GwgJ!`+F_i}sICkuZI+=hNGeyS|zCd|I7FQH3n>Rx7znFb$!6~5T*;*h9 zIh7TxWMIrB8&pS%4VQcc(=w$m+p*)aff%y888hw!kdLf8@It$P9jo?-H`=9L2+|{7 z*3mG<9=sg@Z@=61>O$IHQ3wwsr?46BvR^9T5RiYzr8-rfCxc_d5UKj6A@W z-@weZQu)@dUU^1;PYJ`;&&!xNWHC@ET`X%0$@nXfJib=j>Xs?F$ud;yr_&Bj{*S}w z^?!3Gg_efK!2ot>CCM=HpmA@9llX4do4=>_)m-+$ws_32L%R-NtTHm0>6<@#HY`2=zY(iF{ zCJ%f1tMu##j+#5?6FVGV>CdEdlJ~S8@ViIROY}Gzt#HV$_4MEvE3zSKb5!c5Z$1Jh zAm0NhX3fkIN*RFP9h(=<4si^)ILRK_24?`f78imIR!74pnu9^|okXjlR$afxuB+O- zR7w8)+B2Ge=xc?$<8|V>h4Y@(AnF*tl(Tv1<>Z5|0K3ghCua#kI=Kp*ejp8qouAd- zj*kj)%{ekQ^E8}i)ThP8vN%j z=m-D#ly51rf1kN@Ltn1b58Fan%!5w0_8=gR8X;)mTyn$i-*kHI`nz4BFsO0PdY}8n z?c9+!m^JrzMGYSZZ|4=*Yn)1X*k*wG)|0s2{nL}cQ?!%tOck_9vDl7Vk>VACT>lf; z0ObRJ*}_15e3m-^pE#}g7!A2=1E%fV;t7mHT^OJACVsS8M+YKt0s1EKPe)WulgV0( zJo9@?!pCUlY)3F0MQ3+@1&&%H8!$UFFIX7zg zXGeYB&dVG3SfD5N1ufnfV^-CZ1e4@;lW)mlR9Vr*SRsi|wsE%w344c9&~w~bB`<`3 z5TIhqNW#Fc+z^^K@HadCCnn%upf!Wg^Uk{msi zFMbm}g|UR5R+G4%R+GEXQy5k12xEmLKG`N$Pi4P=f;xbG1!WEHQb8@21{KsjAN$#L zqs`)CHXTE}*en)PDqG1LF#a#5urs8gN(jLz%Kv91a zZpZGqr81gCg{PC|6=J1&=xXSHI-sF`H<3>{2`cicrXsr(MD;m%Jb}<@Bofme{>G~~ zO1CM@+?Ai-KZotN10`$@zM4Iq4DH@eXXOuU9{bW8l@m(uLOw5`S}{LYUj@R92pJfy zF8LgwE6oUP$iN`fQav}-G8t&gV9?G#kPzyY=upJ1YN(VbAOElNO*MIcKPu&63GtBh zV^#3XKt*o3`C0)VC%uNeg5|5N{V=PzFpa9WvsgufZ42Cs^5t?wQu>jiG`!6~WKSfK zP??eDiVQ!C2hcdz4g(Z<4Eg9*4Ei|W4gw#ux682#t*`&jw1T*ian9x8yu9qqdW-3d zI*(^aD1oNkV#4=bu=BGdu4(xA^D&Q#>W%?a8xAVq-s}>(*(Yz17K!+_Q>5#1D3Eq7)PLg-8=n36)TvV+vn!- z4yr6Dm`j$J#e9VdE|ea@)~PJA;2HtkZ7{4%Wf5qD0Oe|uU|Ej9ewqx*9HBMz;VfYj zj*k(nvmDjqb}PtjQ9mPC zE10U->A0i6RilyQ-}k&Lcw3)wP5DjAP^r6kd(G|CJ<>;8v+BU96@SaU9c|H$(sFy3 z-^KjXpZJ&UB?RaMO)P#&LsSd_?<0C(Gu3E#b}IO6eZkRx0V%Xse@`)K0ImzE>paA4 z#axCnun7#UkzY)q$b`o-8i}UnI|>Wc=fY^Tv89@T5Kz|=$lz!YXO%?4@VKzV-`=>{ zA|zupuI#U-3+T$H-=CI?n9`HZ^S!+ZR154DlCkXdlg0(#vi+YY#cON7R!nru(Ly|V9oWI8i<pEI zB3ArHL<7pc4iP%|%NXz4L}=$z>$*wLC&BL^R==U7pg}n`3C$)EeAvVI`1QnA< z;)ZhFRC7kjh zcqCKTXG)Soh{{n6G}Z;fa%3nTCMBu9f*2^m`M~Jop_P*E2|VQ?Cx2>54@>;Sz~vCQ zPVhc|-sXc+1OKbLatHeI`--pr`b*|2e_{)0mH7=Dd*nFqEt$Cu?W0|l=N=Q0Nn#5c zG;?bSq{W!5tA4a=EQ&Z#%-@7hJ=WbdF>{}T(eJclBC(Jg_Pd^Magj^4w|N;Q>Ks#r zY6VczK83a`yVQP+clYmGqvT!@k~67=wf(n$_j`JhqPBWN^_lierLr6VhC4@tuWq<2 z9iw@$!Nk>IO_g_(VWg}M5#gcOb^~!xbDHnTk{hZ3E8y4EUC$w@|7&_T%s#Z`hMw9? zCfuBSc^96}$1ds@zJ4d9`=OjMdEcGuGiV`i<|(3!Fxji&>#xi2Iy8Hp(cZ{T_{OMz z*lT#m>1g<(yjbwkP~j$dRjBx0*i(M-V8tBcQ^#XIO*#nP&vg-MD30SrgSTi3Iq#XEfVGI?1$k5PRs^u8d3YsxVXJb@H;cNH zWc!e0BauQ{xDmh(+#3?XK;PdrCJQTnTflm~yYMDojP^4m_)gZzmqwraNuhPS_%hK;{$|DdK#-wn zhdw)?R<^~fyKS*sdRCtp_^<;!g-6d6?uHs?o<>9R!2m8jl{12RoO(%Ik1H2{|JU6X zk!*3RNcm$d`M$KR^LII(Lmw$3H&<1}?fC#y8dG>I*7Pz;Br&e-hPG1eX#}pEL~i)4 zV!z{krAyv;9=TAp!g^3NBMb2Ejs!80K*!Wff=Q@7lOWWF_q}r?uTbt51z^)Y^AvJ8B`4xTod^-;}5B0g)HtFdX5j`2o7V@2Nc_5Dd(+%k6!& zqf*-Kz9|>{VE5-Ym*qfjdMsozBXrbLALN~T=X$Xh2Bg2<#25Sao%Qp76FK=~yc+T= zAX;zaeWI$3jkmc^bQ|WCV zkqPK)f;^e#1uXmLq*sB2qmh*>yUHt8b-sGp*51(EBz||g^33&el@(OBzWj&i^0(gLJ z7+kY3P0gyL2kCdKhOUyPky@a2_A z+bhoGe6c5b8*qYu09TkcH86LHF3>xt4>V+*bc=GxwWBq+tD4CH`zvM`M=K~aghzf$-rs77hXk}?Wd^<7 zi}S?ArRA@1HL0v^f3x6qe+GZqpHd|`od9S@hn%0zYzEAKTlGC=k!RDKz>=rRAjlsDB4Tbksv3uaNM&29qQB(7ZpJ|VN z04e^#Vf4L!;osnM!yXp!t+^;B2w1Te)i|O|ckOWKf0JYyLS(XLh;hG0BiC9P0~2if}uJp>b-It7^WOi_fL1 zHNGg%cR#t=gl__hm%Kboz|>AAy|y+Pn_{e@$I}G2QxlI!vs8$iUIZgx9ig)UiSPnlqgC@@GFI3A14b z&*wWbNob`G#n;;5mH6y3kZd_UDK;jm9WEpGpNpKUhxi9Ok)Vx0-48PxvERL@c~zY( znzLBEsqCX761;`1G5_9^eLXP;baIbive@TREM8Mzh7y%J!j@W;`;=(uh z*kzwmZtrR~q02p0*xMKCT=@r@Wt`RLU%7PrmwJZQB+wEi%;Y8`N-gmf${r$rj~}a( zo6sp<{Ii@*pG}vOVPlfPj0soUb`56eD(6Xx852#krlZ{~CRCOQ@a6jmat&|Lb-!bp zF31*F=%L&6z#AGFCY3>^BW$@rqMXwpw@##7xJ*v)s?AHhK&Kn`>589DE6obljBYx? zi?3+;qs)q92Q82n#2JvLcx!flVGyVPi)rPeoG;{6tS@`3YTO%{qIhq&s#%PCE0f(L zG9u6C3Mk(&Vy&C*S@Y*=9J>LPICxR^406>Zja)TJAO{d(;A%o)CI+z^P?$*)%ndz? z>aCa;-RL7ZtCs88ER_@*#DODQaW#Rp%W{o!F0X|a%vDW81k(_PKlf&TizBxpnX4XEJaXa5mYP$~n2I4=w>J;>1TM{y0> zij=6zkmB&QMbKeCuOSj?F?UafB@f?DB^lQ98q)Z&n#g_l90y6&Q3>-VQbkYL^bX$` ziJCVp7$d_S@%iH#k_u#hnsmw8%B=Oq;>yt#S*F9Gfc~%+G_N==s`|{t+wzYA3)qU+ z4S_3L1fh~gIV^v5Vz*ui;;7aN$+!?RreIQty+FP%Q;4Km8Vxo=%+=F6LKHXeMuf<% zhY+H{B`HL})e)jKtR+F#nrh0QJ3_R#_#it&Zb|gA(J?Q+O(QItQO_ieKzP__6F5r?L2;6Ue26H zf9;K`;s16X&RHDlJbJot9{l{17I{p6^?6uQyp0q+?G{1J$yuay7lj)*(;q2YS$urB zv#kY;-20gM1PC{w#NIcclqTJz2d>6#E8svI-mA4GhFP+7(4DEROILS(i@|s2MZ`S) zNSSfa%-#+mkV+xIb^sX`;5?%50RD>$)`p+$XZB4MgOb`az^;h}bt~*)|6nVB$S=A& zxI2+M{K;|n4PT%uh*DDZkM-2RfBH()XVddOq^Gka*)s=#{>W@KSs=B6ssoAHVygc0 zwgFW8uq^Hoc!Hy!1?rnTKP=*-N>-gN&_H=1kO~D#F=spM)&P#hrW}hc&I`Lg-+@4M zn_)(2_M8GK;EszObsKAriDnRgH~(85Nnx8v>I4(S0PRNz`dBaphmns zR<<0pl@=VHsGVI#isZi$xv~+AiGx!7lhJ@ABPC`~0si*CTXBO5_@hZYfYH=6CfUU5 zZ26MK*vvs~MOaH}3Ie?H=|w)!3?Aes-Sg25AGwQhxr~$bIJf|B78(P8LzqxAcb$0f zbzV)Z$86%6>V~}(i*EsLi~4uD#PI-qUTNC_)is?9)9d^RjlgqP+F&(;3{=Xl5gj>N zT@NqSqCA@P8+>qESsJQ02WgdSRLO!Z#}VGPI?>9=f75zA&vc`8!slI5ln=HaGf{$wO+#Z^lxgHrMhDzkU`{Tm)v`NFWH%;b zPU}8g=Oe0548)z(KycWpQJ7-{zA20Aur4wn+pz($rpbxzI;}snW-@#VRFN;r%^0U+ zx(IIvGIhlA;MJG~arGA{AGeqIZxAT;53T<2quvm5*=C(a2O6M%hS#pt06f9I)gN5v z6GHy7BTJnD$of9c8n3he^?mmGVm15ze`S~@*zvU~xN5*Yo}7Jx2%bg^o96tsWn{q; zTal*QkT7u*)-yka%CZNBqwXLo%hs~*<=95W%82NqX3P?##2^2(ZY*J3Q_4Ih~nIeuM!kMNT){x1Y>&H!9Iawtp;rxnxhP1A#Dakl#rdGnDmE&5D$Of@5y>> zWq;Ho;Say;63Xh4rD}qI)FbYMz-kgTy&9-5fd4w!f8O4Cv4^nf44+?>R6Cgw9Ok|& zHZ#;Z1-1Zx4?<5BnF{D&eCe`t_CC$>Z5D0}Yu~#9@<>{cQv{>{H@7l~6#(7T<{gH& z8}+vxRE0i9&Lf>djC9?6s9}{J+L0lW1`&6{?W4Lko=tpATNxn8kYT8g@^KvZbEO&A z*Yqin)s4Mk9x@d0I2{^GK+KWi%fb`b{p!K#X?G=mp|4~CNOToA;*9Vp(=9ddct?7)5(p@%c;zwJ)R zo4B%nx&n(Qj7BS4>F^(G{Kq=~vB7`b<3H~6A3yLP5BQHC?T=%D)8XXF@Xc^W#};QC zIrM1?456eW(1emTfh&}(3xuI$LtqUh_XO%ta$n#NB|iuvpyYv|1WJB9c4uUdfyavb z#ju#cV@T0+*1ob4`f$>uM`Y9eGQ3a<9zPy`vBIPNvCXgj`BwB)#}mBSr?VVUQW6W; z##A|^2U6-JKln7BbuZg+9~zgUt$ zh@Peysijbqsg>u@yrT>-0@&C$G;H^B#XQ{Io*YsMrm%1ox+k-IT84wIDv;1rZ3kU{ zN9thf7WNr-^lSH1FL!jBpAiyK8`2LU9Y_Y=)1Yk7J$}9*Dw+Enyq;r=B?0#63}$Ke z6VY5!MhT>Fkb%A#yDh0{6T}JHd_!lTM1KInKBI{9LubVdyy(@LxxRxmY7%GWwxp%d z)T>D4YTGKIVFW=TT_`;{3@QJ4+U>u8S94?V@JTB>FhlD~wP2`?mHON=GX(geZ2I$4 zC1~d-C&NqAUNFi?TZ%^yaqN&u2+U)YFQjfFjC>NYl=h|s3M#}}MyAhyZ)KL4m-nLrG`qyY380mR+fj&=oQ!))7|^Mm2bg zfLOaoM1OKxoofyyv5_V;xmXi6+st(Inh>{H6U~17sJIttf*fNlh=XK*TTG`;=bmZt_|`PbQ;AFRaxQwG2-bJ9tf2EPF)OaIa1;$C!$k}2pX~^4J7?Z z5_D@h6RIf?(!+mo{MTamyO%9#BfptxH&V((lPE<_7A;R5hEgWaglna@6P5t~V7DB@Xms)C&Ea@( zPIG=%e2F69Z$Hm}W~*ZV2_+r5BdxOwRbYZ`Xl0Ym{7tM7&pQ5Y7a1n^rAVF|@9?7? z>LeFe{nwKuTc4q`k(j#bxH>C3oW=9;bCpP)hdG@@lM>#*yP~QgpqJv%Dt){Y`$i3K zNiV``JmK`wG4%x>)j!e5Z(Y^mg?=0L%RGSrf9izH>Z>n*|Hc!o@ceqK7I$$=e;-Ute6`!M0G{qVJJ{8+0II>xtU+?UGP8cvVA+4A z2LJ2~6I|^U{q9-bx!>qd202M4oNjdP!|u{ML_p`dMKS==fWz!phfh2AAHU6&N*W-{ zX8V_Xwm)ru+-FKz&(C&WckY7&_!VL! zeDiJQw-t09PM&vFWw7BlqYV$trk!Y%ljlk`!%LnU(Me?;%c`1nD|2l5@SUH+(L?ug zI63{olLW<(Laga>E^I!iBEA7PNHGALu-aN+-ohGxfB)XS_4{hv?F7;pr(aAyHrVXQ zptcea%ZZ9SjHT}@y&C5v0?2tLM38K|JEcelec-^K@YS^_3Of`yc7~~I(k_WVp$%hp zmwMqk2Mh4_J=TakyhnIwZK(4Zs=7zm63+rwe*b;Nu}C~JaH8R=TGZ1Wnea2qo+|c1 zL@&*Mjh)%<{(+4^;gK|WR{%riOy2UTP;_+d5tfIWBC!w>hd zYrovvFEfBR7?xCa5o5KQ?{19Q_^utBp@?&QjdR>~96nJQZ{6Xo-CT-1M5>)FVkNX5 z)r1zn&)c{7sdcw_H9J{fgQIJ`_&hLck6H_j$JMN&O{F&pSR=NwwfDvs5JdKBJk(Nu zsk_kfbyo?kSl)E+3xRcms^D5~n$A?EU@^5V=Il={uTS=V**iRd$r2oSi)Gc+|8?*A zE3Ce9*Q%ih-lD7QqXxM0!7Hx*X=P(_(*|Ud#3Z-!qPx3z8G?cjiOT)us2Sxk&X)B}C1vm=< zn%)&|O&^mS0n1ziEfcxYCF(0_G1Zu~10FDfUN9uDY7dV&sBHWT&R>|ns+H+sP>|6# z~b(dORXH&t(T1J z3(CdS_N0p@_yF#nga@cr++bu+UO!+k88S#VzYWQ=KiA~Xb@_8c{=6rD-j_drkUt;D zpFhfe=T&cbu(0C|5*Ds`LxqLw-hg4@ zhBs_jc+VR=+xyS4-XF($e-i6`H`e>pp!Z|CKx5qT+P@Z$3tfJHWGMNT$`r7S3T3Xf zh?AI9n#lDLQS?bg%X_AaFW7Z#M~G^7mQR&+-KB?l&hv3USL_IVxa7d2ow%yN+(_^X zjD9i%;Me6DEL-C@yZcWeDa?2VFJhjICLh(WmwC7URzby2wkE8JjU0c0=Z0dJdz*@; z*=zXGeXU^33L0Za-BiVK3k$b86u)ECi&3kz?tH$FRu&hR?g zU;_6^C$sECO-(=}TVK1|8_ww3S3VUGnZR*?x;Q{UiezsUU%6xrty^|@lJziq61o*` zufTvD^*}KJqv6yE%Fx$v8#>vFk*`~=%4RLRQiMa?kK$%#K(Dw7{1C*dPN@5#aiw~> zYGuR0rQ3Ud(Pg^Z(?v5%F-VFMJVXaNDWlh$xl$hRlQA2;Ic87! ztol2MDZl;m+5X9|`RQc(iS*RrWb&*#eUmqals;6Il6HU(6WB9x9e4wZg=56YRpr37 zQ~csjm;h_Zs96q)L}!ypHiBBDI*c*8e**56VI&TJELB$r#?bv#)Hxum6&+e};4*xeyAJ{=C7L$jP-sRTb z*8NvMKimD!SNn&%VZD{#Z@Wu7uFZ?xmwWq9BGucm+A+9!tm5PSXZz11l{e#+fBkhQ zQn?j>tNiTemphMRczll4ewnKMB?i^^arqt$W+6e3w_gmGStpQFr|Q zCliG0;v6unb$tz`09*WoF@!ogTih@0WmojLjlB`XLbwc0 z$-A@9Cx_GSQ0-&iP>|Kb110$Sp^y&`W#H9+cF;F009RryD6UxV1uh3VHrw2Xp)}9~ zOb2*H30H23gNWy^o;}k6hqMPC^XqKq{KqK%!(DWPhzJ2|##>C2fb$3}jHeL5PI!}U z60sr$IW`{Wqfun6-Pl5Ou3}J9S|*e7_7E>ZaUv8SVgNZ1xVMSOF~1>*39r?E*qyw8 z6h;VcQTa8vq~-VgGy>Z8X~P}AyU_BN0;E>KDBtw)(dtSQ=4ylb!>iyII;7^iN1Qdj zGq8?7uEgnt3)j0oZ5uUuh}o6u-=3S;H+wz~XXCsme5KX%lomn#a6Xyk5wMzMwFor@ zP_||{AaoTd4W;b?p+(HKFF_zDp4;DlyB;Wp1zvGVL)!FO;*!T(gV!M0x)romYoKdA zf;h_(GCq6FX;pOXrxoqLcj4dAXBO*;=A zFkEaMBsh<(0Z9M8Qvw(bF$cJZYiR)5F0qotz<3k;33r!@EJzj;Pq$__O@FO_jNZG% zyRx=af};ys1c{DZuiRnk3^VtN-p#^%N5Q>wfc@*DhJIWVe@585Y`dkipaxiB-)fU6>c3=kyc?@^ zGZ#C*Ki!R`Z+!%R@3&T8SbMs4 zSg_e_r$Equ(2TVzt*!IYgLr`nvAH=Of4NxKH4~p{LOUnz9C;e@ zK}{O>niEZiRcVLu&!FS_ZV@r@kV-{L zbf3`}=!NWm$+p`@i49b6ccq!yvmi0-Qp%vHxRU}E;u&>Zy+@A>AaS$g$nF3Kg^sV+ z^3x3R@y9r(U@n#jk!m4@h?`33XjUdj?(q#L zMmoXt-AF9y1-pt5%ZbkKVddvSEyOZN(d}IY4dl{)QMDu7((k1Zc`ZphxpJE2iA4P9 zSVk`ziVKsgbBs7zWe{Zr)7ys^&ViSt!e+Y++5G zBd+&uPJV!3VACIW|(l@1W^1lzZ6>xxRcZe zgA!77>nlm1ipjO}c6g?rE8Tbcu z-rThDlT>)UX~1wqE}`qo$xtuy#B-KG_px1B6JP@-@fCBd}3lLcSByhP~a*&mNSVMXK55iTV-s=yO`qf})u z+*sjas@NC9uiR7SI>-fo7e~Wmp|#~&5e1H)6M(f&FqkI$5N~u0WeOE9O^RlJeW4aA zd+7n^AiB`v%NShbC+C`r;na#d-e9jFt5bb#DEl7{X@iyyg$9rm(dvOa?r=h8y7kJ* zJY*F-_C-M#a|tR!ndUCBz!&BTwGml{Dmk`5WMkf`BkfofQkUaOR_f&uGD2O-vH?m;!*u(=^ZV~;6>7*D7huszPy zf1y!%)=}ZO@I4lhkvbg?2BX{}BADO0t@hLylC3~PNVXr44N3$)2{(p+DuC(MOsUw< zIHbB?Z@9nQu69m%UWtWiQUFsl!6%>zg;f10rRS)Gp5qujezLero+G5|( zoz*(`Z)@+jBimfs+dn>kpBDZ-vU%T(_81HM`LeWV&n`1~g!>W#>9Gb6S%UK@L&^&s zrPNoG?kPOPMaVYAqsuI+6=os=07LkvMjsOAQ4^&*&S0fxx&DQDq^k1RS*YB=1aYfPm-#{=EOR7C0+x^c|=5Ly9{4iuVool@_PI8yE-i z(uj3z5`f-@d!b)&%6F-1)J1n0q@!MnIV2+-_fB* zbeOIYb4)YmqOJIH(N^8De-w0~o5M~_u!ad>3H#yMBx64A2rdvmLdp$WXkVrp4~~lq zfAFHUjJwl=cQi#W#Sx5GyA8|}Pr9d;o}Ix(cihhhv^-2el#Qk~j}Jg_SxMKvI6OMtv7b~+s z0>s!?55jhxF(@T(e!?nP?9(}?Z8tX>s4*?=3*c~#zLQes1C4907nm3lRF{n=FYk}u z$iekXuUm1z`f5T`*ptPBtW_d|~2Fe;3ws^Lww>I>kS*^KHobmkuz1(aUe<@6n zXOkNG>QABeom=^~5mdz7U*{icwvwprgY{(^hejtazW%b z2qhCCML-DebD0jo9`IQEr-oWWe>a7_VyIw7;vHOx?ZJjK5ThL1nF*kq=F(}JNLlI- z^OhB~gAkWeGYEkYOR8uTrtf@IQU}+i)ko8(m=FwUb`vVk-=lh)vaM|`iJD?OIZp9l zZmS&}DgcoV`)xSmpWbz(1kuwP3z@1uMd(^##f9^(T?cV*s z<|LK1ON*>P?vW1Lu-F-5iG}uii~=|6?}uk_#%0I5;k+O<3GifY9Nl?&bdBkV1!z0N z6`c7PT%B!Or5!gPou-$|sJ5`pYIP?Y$F=vXapBWnxnQ%>l5OW*%ZF<8?xxWDC7-EX zwQ=RZ*qmAONN>bn)?D{hf6KP^_tT0C1$dTLo3+t7WUd5w{)J|IX3=>A%3LS0pzh#_ zEiCdtx=959v@cA$NBMVFJEZGqMTL8_UPaxx8Hur!mnZ-QJZXf4~tw3BR77+o6Y9 z^?GGWHaVcFfs8j*>e(Ra;W(d|R7xedPAoJgr^ONV-)HP2M{+LQS$xYcHy(X4~$ z-qU>cb}|r4Fk-v{%NJT@_;ZVW2jkUzRDYXK9|5*$OuH%+eq zoH#GpO3Sj*KKGQ6XFS7yxYNp%k}qZu(8Wq1UUoCvS*kf$W3{g(zb2MCKT~+Ov}I=? zP@IbD^=u~IfA@{7s5)~f#<}=Mbrse&Hhs~Z&W7DlqmbDcqpF%&iu+HU$clLtnOQg@ zI65#Ob!S=K35KDS)TEfnS!XkS{5dC<3bs*ovI51+Ke<;P!cU(aE{k)0y$LWQ-FOf-O zb&i=m^>q(BN00TDn02L%pMiU(J7@-r(6I)jtD9 zbTm=XjHs+rCYOGnqXc7!;-uBDau_G2ER!yZu06be``y)#Pj7A@o4xzD^7EdOTg+8;TUZ3Um-Cn0Al?xK%hkHD!K|% zf4iANvispYXQw6j?Kg@|Bt1qRgiZbFH5JNRNN3voL1Tf0n`$?_n~Z!7vez6t`XkHG zp>6C$yhKO zR$ETXA?@VolrxAPPQ+mg9F0CU37U!(*`dqgtLlu^;IA~ro{uRF^I1CfL@@G7G#HsB z#O#HfaI&gn7Yi3KZAlBb1S+AG1?;;q{xwnzyn>d<7>}3k&35?6Vz^5{siHVze_j=_42yu>%y^n==4WBJKy|6iMFR1W`*jC;clRJH!VT>fnA-5yYAsA@ z6BS}EH>kN3a1px`fN@-A`S6l2e?nWWsZ$Zl*AG#y7m}>QeRb$DBuFCKOeQf#0#s-9 zFi2TPiP{k5rH26BKnQT12xlpU_0AEa(%35mQpi$_eRd~cr6JHEvStUu?xaUqVl*2a zV%Y?PlwL46lCoTbD+ERArec9t2lS0+ytxe^x9lbE;P5Gk#2gL#IRwyMf2?o@TW{V9 zDGe3^tBQ1Fa}WTl%GB4Y=vP$26#lhH$B$wi*Y4Lv49-n(*zKbjz49K}PY@(j70+bD zYMq!K_4O2qxLCEbNaW*(jg$)!+KMAYDa=jOQVBxkp-LRxpBnvIa`yjMwBC{<*IXuf zelSKly+-s}Y22EYoyU{2e@};##vlhr2_|wg*U5A?5+2x5k8|XQu;b-Ds}0HkdehPM z^EQqubY(6LPloUob6)t-Wl%(ET40GWd07lx43^**Fry7!{dSwKXp9Dp)c0Upf)a~M z|7?QINCM1$-oX1+l&)PJp0H* zI#I_<+=I%1)Q!>xA2;>iW)Ju=wg;pt4Yhqj3g`_Nxfj$>@R2^OOn;Anx{Y8TS{f;riO^Uw8hC+g&xZ z9rYw8y)fPQww87I2#3-_a6lTBd$>xka-lZ7ImMs1iHn0Z|a%Uwv;ArE)c@T!TrfrT%vJ8l zAWeg7)c;&s~NYfM(TY6++oPR`pb7VNx7-F(iy8>xK6?8*h z!Xl=eKr;919)IpZXL`G3pAe+q@LI&Gb$_zQ)bXoYlWaW%q}IpIs?Ipb>+2_6Fk#e{ ze2m3=KqmfvjDN{P=e-{j%Pl6~l5zRDVqEz@`E&v-Z123-i=J%S=VUNF7Ei)#mV;PU zBAXh;J5lVRBgbByfOl7P>a8X}VAP-OOE&Gp{Bj1B_zhNy5+O0RRd+_CNk2qYN_Pxn zCh-BzGEmWobK9oCOV>5EjGzmOEx{z}j9kuilf82F)|9ulZJAc|ibEj!q?v#y0e{;azsUz$ zGwFkme4HAKLtr+r*NuojS=@usISQJc1~6A(q~Z@yi`3>4?RSAd`Mh#sXw+8WkXN&s zza(Su)_=SCFhe+|$A+|Q zJd>iroZ8^g1^GuX1_2pLiDH^@grKs6A_xHie z-w*GB^eMxa$w3fFCJ;8#xdV6`R@=)L!1JKlP`YyI_oLy+{W^iwwV?#O!lR4`4|PY^xwFv6sNudBGfe!mW3*K! z%768ry~3BTJ5EfDzitHgW=Q~KXA`k+u>ZrbTg}V-atY>QAo3=g>XT!bVZ=A^Iaa$QeM*vNP z5Z`TjBljgcoPJ`!O0^e%erR$w+peL;(tjMa3T_GPw9|-g8%p`kN|~#x%*Wc$ngBIM83 zW+8xnRTBkjs_Ngds?5BypIn~VAen6{Auf9Z6kEeN3qomo)+Cm)7N$0jOtet8S${>Y z&~$oM8RwR61z}h&f}jw+(j)KYiF&v?`Z#GJ<35F@JXKSOL{ zm7L_mn=%oxx7|c0Nz?1=`&+cON$x9|Yulme_S9y*+n?F%4f@$E1-N@EZ#nG0*nQ4U z&GoBl&-M>?H|;oA4EfJc)V$+5N101ubF zc(z#p+P?mZ$4Cq>2KL?Y-vY`eHe=^k5l+jXAQ(28%~whUygM$tFLqw;9PYo=*NWj8 z)s}lkl~vS>(&N#jfcGu?@UM+S#m%g)5oxr41}=ejfOxz~OvcQUZ(PxO94#x%^hPCSOE0kz4VxApUb;hN=6B+S!vBEuj zWp=#gpjJ49$ff?5T7;8U(DL?cYjBHw!L<_>)mm^ zPmTd^X;R8oGcs(<@3HFGRj)32?jt(T$bLwTI5(Dufni@EjRSzil2K_d^GW--)M7%K72tOMjBxugup!+f{WdUr?X*Ra8J?eXTx#cof<$b zp`&9KTy!!9{wE7AVFU&Zs=8(KJLtt*S*o!95(t-PdVelr9C+*4e8xd^-Lg&Kif@F_ zgx#!@Q@wthPxCJ|?ToEB{dMRrLmdZc0Vqouh=}T7_LKKiU1|3vPu!)J(CZ;yCZYtn zY^x(rwZD`HFVMc|S+|(|Id(+OpZNEV=r6Y;iaT{zoLBd&?|w>HjG$^Wx%RGzwnTI9 zhV-CccYizN8^tl@ytFMxX=l<-$3@JwzJ_^MADwIS>u=NTf0pSMF0CVc0?A)ccY2fa zS$U|Kr-s~d4F+xaZFS6Bv5I%H&)PHf|MkNWS)*ZNSRrw?j!mVX9PPr6yNclxb4XWV(e+_Ji1( zLor>0lKZT*R+zyc4)Vi_TizE+=)*$45;ZKg(eEaMk*#&?*D8+8Uo7JfP&KVo*5F|6_heWaHh`UhFh=CFTcRY&)4@s@Kc{-AAr zZ-!`keOCq-R0h;{Aub3}BDxT`RG5p*+~&@k^-#gGKz2 zF1~reYmFs7Lm88>qzjD|7fA4O-sWBMX9d1dgy2d2J}M5wd%U^jREN3MQMR1R9m2s2 zOmMFol8ekhac|s*Rz4bk^Qc4ciR~IQ(;|5mnWLfdaQc)kJ;s zfyI{UVP=YxFxCkr*Otc|je(?Ij%MaEsTy!3jGwPxLQZRaKNY`!Pu=$vc2+Og$+bAD zT(c?>jzQvj5K*2{UK9>IZP?&Hi@m-V`K+&mZ+dscgG31K)H$9K!F`YQQaeY&HSb2x zkvGA+KTQIaxcVQ?o8-lRs3b1`Yf&tPEM{C1H0>!lY&YLCX5f*|ZrLm0N{OJCvZZn1 z2@m`OuFS4nu@QB4@roLx*V?e z)+h&KNWOknqA!^HqTwzE7wyPx=y(!2(}27Km`ZLbm!v6wfua~`Z;_3eAe3#B(!aD= zDwt-o{cHEkY$rUSEWJjJDInPsNbiayD_9;qo=MLm{vx=Opfl=Cd1gnxz9~a!rm(OH zk+8m;LrN#;G;+?Eu_MEp2VR8~7(NIVVghx5j#u~G#R)+3d5*R)?#f#xcZ`*NeAm_m zoe4kbv9pzb5O&%4L|+KH_8^7%4x^)EsEoZlWJy*F?Y^3PC!@(nMKQ{gugQBw*;|#1 zq$*nGGMi`;$thH4MW!k0tsE>%?wp#8GCkEu;K0*KT~jsv+etzq2~0~T1me@Uud{FI z6My{$QmEr|sGmz-SJhfz(t8K9cm=fprQ_voaN8s-d^J9qj0X5gcXT1WrJRUT@YGyywbHQXLe^;&mqW=M8POOV zRgXb;I(1`!`HqV=r9G}W0yanTk_W(X*rHh49`Vql<1?6WywL1lE{{u}MAl3$W{k;{ zq?$Z`2je#s5b20zx#)B%>t+q&eddW{y=y`>GrQ#BOZ#+KX;8R?yt za+}oun%ywKi^Jt2k!A~Z#S;~}MrFh1wet_a;yESdSj9zsRxRoMV&)|MF(k?As%5@y z{z4=VU%uLn$~>lXR}dDFc`Y@Gjz6pRXQi;?{&c$;dk^k=Y#Egxw8SSYXG|} zs0tQ)V`(WMK?0Tq>tv}6ol`bWEbz!Jmt=4FHcH>W;F!LlzXEUX^ow+KKm^wHDJq+f zsWvqfn+Ged)=rkA)}HP>JGgnhW}d6Z-u_l>|C1FPiooBR?QhMN)NJGBXtw9Co;{0y zDmHkAXIYAEO)EC&tX!|n-|K>+>v!}u^_uPbf1X|g30S^bTLwetl#RcZTAPoeviW!o zwdTR%YR%VNgI#iQy|ks*q<&h-7ZTwPT!sV55vwC-50z zl5&M#21bxGADMXuk3O7?L&vy0$NfVKtTuUn*0srF zpw-HsUD)IG>Kxi%MH=RO3`9zUo=6ESD@~iOM15z!9Al5m67w0P8~B4>&dO1n9CJ0qoWYn&QQsL(a(hX? zl4WL0o!7GX6&bs;a-II}I^`X)VKj&Ya1!;!u!n}6CV}7O-s02U&YS-{pUmpL0`LK9 zevOCqNP)ox?FJ0j{Q3X=5FdMdR!wAqRhM&Ct`AoNLY3_|`d~v^%m8SAJF`C-&miE{ z9se1@x9@+MD(+n?U0|QIGBu~sZX&kyzch;wFAIM9A@WGr(xNSwV>Uc{Y-^!5NymAZ z^~0+kv(M&#c`9PPXd^GNUOgGU8Ddy-*+Y;6tTgvSkgm*vbuNDz*~9bl)US5aMY1ogYCia zP4vAUhHRm#+!U^mh>6PX%!mKsba;A-3Uh9Ox~VxAC3Q6uqu7E}6-aHSF zeu1##IvoAA`>B^de5W=|^91rrhN{N)Rw=@RJ(xBK6dLh|EZrNHQGVwU(b_E?gFHF_ zY~k107}@gfjf1&(X%gk+D^2L!{@z`2W(G_qOMy2DT`leJA|G6!g@jpRGwA;dMow{u zdH`=+#3J!!;)S5=>!UiaZgF>XVzuCZI|}WaCN|7){NNu%Y=(Hz zD*%`A*DiwNC=Cx*7feukS^2(2>P$t82-)3dk3;`H@PlMO1>t%2_}a3#>%uxxaPe9^QnL$*p=#L(t9eFP4R?B>lCqeW&O z3FcSID#Gp-MeXCeB2kJ>!aMJ?j^P|cn>ZQJ5zTS%i0frfOHd@j0xJ7+xyt^MQrV9u zqe;C7w);@?Yo9@FE^q|(ANeN~&9Z&&d*_XRq*Et2dl^llS-FXDRpY{Z)t5Tuj@EP= zO8ooUM^${9K(Dce?-zWBg|9+D~DmKp{r3TB$!@W%xj@)z}Xq85hP zi(V|S6V(T9?-Q@g8pJFst?7?FUsQEmzw7tqJGu9K@3r3rbbtK7_IqX*zBT2Nher4$gD>QMP_cFGEsaJ;;dXwVPnVQyNOeMlhAp%Wxb(f;3iYl(^_+J)Y`PvY{(rX!6Xi^9=RYZB^$Yig; zwB9o2MvuhxJ;tAhb|dieyEuJ0b+Aa$}0MRC@S;&V$v*c?!G4|QK{0d$S&7Ota z7~ENbic3|u0pkNqVbzAHlgE>Pvrp{UNt0t1?Cotv!i6_!Z*0%MI+U;XM7Z=d=A2H3=qDlLH4MsPX7SH!zMR{oRX)?ol^?v_^O=Je*i2 zwz5H9s7(c96yxg%UmuI`mEK^}EL9^pJb@c607|fJ1W$=^wm|{1&Af*2@DaAsH-gF= zLq)}I3nR++s`j?E9=FM8&534Z`f9{>fHT99v zq`JGUaqP;R2x|=q1oUdVm!H7C&=xVn@*SOZtADyDteG4mO4Z-6kecnoxA|E0U@-v)z@XM?u8nfr% zXYK_6e6&J;!MG^zleajlS{N7A66`wH&IyiLiYWS($H;uZf~nLD6Y$lzW`{ zfk*W3S$`9Mv)TfjJ3>&{`F@J$iz z86VYTGYhddTut8^(Spdr@U`NsOQ3(cAPD|S)>wSgYPj}SQ;TAqyfMT;|NZwp-Elo<<0iQKSe5ycbP8Ov7~gWekTM&p`Q3P<3xpg=U1i9r^B(LKqbh z@rlz2t%nhl>b*D;Wd25B8s9!nVxiE5P`aM`p-Pi9zA}IK%6j&-yXlVk@ZhcyOPPX? zyWBt&rhmDwqEtP+n?Fr=Jk@8v04qtD&D_wH!!bP+@KYRcR*xwQTLA z(JR$XP={$J9Mm#+OVdqJQJZi2v5P%eakUf^$g+z?Y(=@TwX=F@h%KpWR%A7f(1297 z1M<q+;SZXL)pYOlY!uuVlkLA92Ag=uBg#6H5Wp4TGS6&e6_w<5jM6SA0B05p#b;hl;R5ct}I34+dI{&c}(0F6noV&gpXuRO5is;BK)`+f3o)I0u!%KFWP$XO|+2!uKp?E5?` zD90%hc%=_G85Zu4)6`~2G{tUuv7=gtPU^TdicKqm43~7a*FMQk+XW`-Ppv z;rR_50jb3=1g26md4uLLk#FiEJP5r|^T~64Zr2voT6`(#r`{1eDr?eeVsSmyfjV=m zv_&>1h(vq~5>sfF0ZDE4_2ybbPX8Mn`)dunc^^l$%N}LWr?QvwgHPjG_p%M8UM06B zh*y7i-&w=>L(J)Cc)Z7c^AFh9Xq2OH7Hw4$R@(a3L zzx|r{th0PrIO>J9k#N=CLTLZCZphB^^%>SnnsPw zR(6>@5#F0lm(<^P^*TKGbgK4P(_w#+?poQW1cjfP%Cd&%T1?reG9-4Cjc{{_=!1Xz z%tHn;V_PHP614ZHB!0z>A;*#UF3v5z$+0-7r9kql92vLPIuN!2A|UzizVQuDh=dT; zYooxR#S!qwM6EevwGQNi>kr9g_MIAhF%;e?U0v0bWMw%_#&1TSmWbV=s2ona<6<~l zP?M;>TG=0SPO3keNhbc0#&a_3j`n}2gB+CNd7b)bXxU1>T(n0p0XXjc582fTk)?yfXTalo!@ zJ&DNS1Tf^?D{RIw_kMyiF$A9s-wbDu6>l1SNzGUZ%!|p#FnpzId??pgky=M(ToNmS_%3mcfMdc_8+ zyiF|$^yih|Z?C8xeqVoC`2zp^9_i`TI8XPre})S){oYRYX<%rAqW$cj(1UiHw2}vO z3{RvJ!lpw#BT4`wWHMol6`$#tLcQ~7k^4)*&VAvh2NnoM?Cu6l5 zpt{0?{k9&nRuDm9P6P(bSYK=L22#s6W01CEmX)_0QvQS#mA zmw|otfjwE(%DREo4?iBULN$VTa@eOX?a2SUbFkZJqPoHl#@P!5;h*|BU%r$x?L@qg zhqgXG91N2<{8oQ7kP&*tB&Jw(e!$duy#>ZBC((uMin_WI$f|im#bJby5_=QI%%+g_ zvs1I9RSb@#A6s6~`9R?~aG#Gl@Y1Zpb-A?a% zFNYZi#{hIy@@|@6G-2RsKRDSGQ}!l z*nqb7c@Yy;y+R!w3oijQhH-_65oie>4qYTAn>ih_7}xB8+e%p$S=_@Rb+(N}zI=Rx zRg{u135o+Pv&DyTI~Yc0fCa;KgzzDxk!sx?$LT4Jm0|YNLDYV#wxA*`Wx@%SB6E8+ zDS*G8kDh;nqv8#oZ0(%SCJh~p*9R33<4QA0#QaGlwj5m$E@G=Uv+rrGxRXic%o%6i zlo^f(=fpu=wl%M;@#c$xWfOL=Z7E!UeNLvFA*d}+&(2J++8uUlJpfJ9C*l}mul7Wr z*+g+YZ?RHdBa87~4o@s-SlVT!b+m2i+@P*{ILh8$N3X-m{J0=hTOVTU-JebVxo zAhY2O86raeu^1Wz)A-q56`#Q}?47fjk?1+v@%J@4iwTU62Am_G&$@GC(Ue{LS!1Qz zVjG>^c;LtOPjj`c5c#YhCgUk z0}X#}KrzK7lzH0h&$8L4vmANSc=V{riim5HJ(9)vglZePxVkrOJ$j z@^Ls*)_ReBZ+0X87Qh+#W_M*AFmh|?4eNO^qjGXMAsVeL*F}1`56qsZ&hny)*W-1>V4X9g|YH>M;a|V@gDQO{19zD?K&!)^fE1ut9U!$IcIfTc)lu0pE3;3;)b7BVL85%Ypk7{<-^Kub=GwvUhku`VSP|HW-<= zS37I#8~5)2@ZiUtpC3QjeR`X<(mVf0thx8qcmg2nMfdDzWfiZbuC}t34*u0qf34wP zYwE9c{A*qPwSj+asK4&vU-#5s_wj$P`|7VB@UI`#Uk~uF2kNgM@vk4%UtNL>o%HBW z=%r78LN^2Y6Z*;NPw41`{)C=(9E6`8gvSoT69-|}L3pYm9Lve2Gq8MBw~Cc6y{ye8 zLxG#Kz8qD_P*i&U9FlYVEqq{3dwr=jaGu9DGBBRG5rrp%yk3om{mB3{WVC<0{c~5V zPpvBUe);F?gI6zK?*FoLxcmCoz2{2nt9mac%J4&u-&_0fezN+`fBDt#uXld5)t~ME zRu26B`r2x$b_n~2^^J8~d*|R_@0aJhPhP)xw)1@VfYz_x#RC-5&#QQAPYIKfBACvg z2|D+A=r4Eh?2UH{NL!o_UW|XbjfZuBnJHn6cf!2=!D*--zpZT>lY^Y-9;I-R^x7;^w;3{?#!98-XJ2LB1i z58D_6IBaPVcsBW1xBp<&ZTG#Qj#{vIZ&zuDlkRsXv?R{vFM;OS&~Di2<5z`<|%Xat`L zDb;RvaNaBQB?Z`0+T#2JY%P9dl;g2g`1;Q;E*|BCfUTpO>eh9KDOLmE{6VcS2Kz9MfkFo3~=)Y$n?qG}_*RO?8= znexbRWj?0p*ikrB17`DX!6cU5246GY7IhPTq&3#n-MvKV0%s#&dquUb4AQEtZl}n{ zOK7^naccYxfCYqr4>`(o&So}bJz_s`P&c!(F_Zw6p`$+4!l!=e zwpccZK*W2#ovVMuBUOo~q1fopsnhnr1fLbE0Vaj75K)X`3dY-|DV|TAp2B|FZN*Qe z%|lmuv5vc7#8eF4o1C}DLS8QlwOg1MsHU=^tF)(A$H4`}Dg`MJLTQtix^;W@VLm~J zOT(uv4aVL5wi*oML*Xyh2x)r!Ht)aB2gzkmwJTg)h}wUxm9Bi=(&s?1bp>u^Jsovt zYQMz#aJ)icDI%*n(+rWrZ}MPibHGcGVMgcf{MLXzNK@3z5KjP7&CDaSl!33?c-N>1 z97q;gJSQt7(8wv>ythR9;->(fk7l%;E*&6{Q1gtPp$pFlsp#X|p)wP%p!A9z$hk}L z)ucD|P@{kSQCS^&YBG~#vA(#uQm54gnfs44-_(fIL=+neSK{@=3!!e=F-BxI8CphW zSQS%Y#$}AlgVrbx#<8Px>y|G}R6dW!09BE+ZO%wvRLY^Zs4$g)5UdU$HrE+bt3M*^ zrER|y6HcIBiQ1`K{EkkK-SW4Lg`C~m#sld`?m&N9ueL^T7Fo8BN)mgWTERM%9_iyFJ(`oe4!qA$p`goNRDu#ilb zQh4f#@SJnYX&OF1NuZZ8JJEW*HjQYsUZ2io&GI73HLWr0fGirP^K0c&76~h^XgX%$ zzRiEQJU+*EU9e=n&AS7%mLarmi+z}Nha>%gAF<6(FaTWaBg=uJLWH99kK2S8yFK6Y80U#amsKF&AJL5UpKr}!F1A&zR=0>_UIhzb>?^D%!`in=q&w+zC}Wrf7}E*dBdyo07A))-w0f6t?; zdBlAc7t9W>yw&woPdi?AP%r%v1Tu&tb+er4U@Kj+ZR^ArpGTe}9qGBMl6b6TPH~Tp zZ6BrUT(Ya0PEOJ3_W|uyXURMIoBn+eyT^Mtd3E^o0n>KDr9;Kq^Wk{*V0(XCrYkyl zythZKMKf1l3yQonFyz;k^%*MuhSgt(AFD5&wFg!m8L{m3siSc09mXrm}K zJzV_Z)b6M@!Z^yV`6hJw(kIWO z7LRI@GX2|d_Ewi*u#~-ynVx?ECcLlYN)dqCD@2SPOm%LR28}AU1Z}9=%}jA;XB|3po$UlcQFxYRp2H;^o4tZ=?_6vW{N$0o9IibII4dqRbz6V-yBVN8*2h6E}gGvS46!;de3gLF5Dn!(UTWR3JPMPe6{IQs)<=)scKun~0 zhyrSn5Kwe@Hcf;hVNo)+8V$=-_=iVZF1EUH>F^pl*DoJivknUzF~xYd;iSf|W+x8> z04U&LU+t(J#(EXtFkyct$D@CaTK=3ZiC(A1c>y+@25|i~vj&IycKHcNHuYOskCS&k zJ6T`DyApnb^39uImO;scE%O13i)o8GHYdfpZ7h?;T(&_VXRPVX2%74^leEtL8x%FL zDExls5wi`DHOmEtnK_ z7*HPUYqtW1zhc^)45!8Hx5*U!tnS-S2rPw{&`?AL?> zrLp<04wDr3JI8;`I<&*5LQVAXz-k zj;(Qj<6dVCFL$l#iuaixBFS+BOjUU z;loUUy#jyCf&mLxBwA#yfYOrTZLwD2P~Y?g3Kn`28g}(NXH)VtnD5#~Gjg*v2V5rD zr=ez848O(hnK&CKHvbpUBjq}iuC62%#;Guba9MTVX(HVh&Z)BAE};b{m_;Z0--0o4 zPwK6~i+YO1GtE3rPD4$uB2CS{E8}7jQ zvGr|O2L0G6Wl(C;%*UYh>$!dcK9+Bruggb_n|?c-vQKOJQ={SF!N9L=0B)W8t5MG4 z(PC?f%C6RbNVmB6qward{XwLwA4|Jxdh+2YuOS{K+G#!s+4!mw z5>!u#xvIW?qXLBxC+E}ITlZ}}A#59%=%GXVhm^2wbV3Q(Sf5weHa5~NHr6X;#{0|& zOvuzXa;E-;U4IPpx(~WsnxmlC4Sq1~S>c+AT`M=cbw6bmnjDt zRH*GAP4Fd_w864L>oqGMk`pnbu-5h|!3n$BXWq?Ej!!>6*x;M|dkJoJeq2*qf=^{G zN?TQtcU8{b7Hd+2)m+5qW3^(h<8>ay?;bNSYwh|LV)n-B`Wk08tMrEhp_XX$yL8qP z4wIhQ9z%){vj*#Khi`d-lzMvp_(SJjXX_gb^*KAs`0@Vz)d%7PVvSXFM;e_6>-Sc5 z%?G;XdP;gW;2hz+^wdELMdMr?I+Op|6+9n%-~>7Ktg6${!#1yPyaew0VsM#qt~#dK znCF;A>WU?t)DWDTJ*n~SnsRe7aU5VKLh3*UzjNEB@<5YN+A4qNxAjl8I!Z~;b*{zd z*m6cinmiR|Qu&@^Y2zXmj8oy{_#+sy&b`QxeX22JZfIS9k!lskQH?+FKx++8w-ynC zjX6cYQ-{lu0%<8NaJuPlC%=X)NNeHLI=q-I#0BMt*zx6BC@33fHf=;|{}EO$k-k!? za>B=`SU~#D={$e+K~tM$?xb}-xeO0SAJjM-J?Ov9Pjh(!dXP_t-O=z5^sXf%{GBrw z;=6l_dge(BL$`Zm>&4do!uBVC(I%p_|DeAf^w+DpnGj25Wr^na)aakTFX|dH7B)pL z0M@P5AM2<;5DNz5AkG!hrK=;jNL}_UckuS|XKlwN+mL@eK6+&9#fNZCR;R$$Xzu## zl|zYC=+SSR1)}oaBEPVBtM)y}Sm-`Z#2z}(In*{@xbdc>K}1f#=XpMOxVzl|Ej6U~ zyXisUd^(*>H?v)s8zwd3{`sswIn7_9W=d;3eEN7>O`nfy?pg6tl6`kOd-_=6`1G;B zjVgjIP#B2*^w6xo^RkuQ*@Y=$IZ4ywC9KOh zB({HD!bCQoUIz1tXkTzjy|f@JWJ7bf5Q8tOSccCrvq&14+Id+^P@~Aup;xmSB@*KD zdDNJD@SIa;n6aVx4{X*`e!=-(Z?Z?E!kd5MavE9&r6ga;J8F(OCjipxi~cm=?>usE zM%&`U1#J4Cz1A!fnCZ3DC-f+2L0Ex|1Qr5Dm62TQoJfe0sTn zCpi1kf}P8JeQ1^_Lqy7W6*^2j$QQ2siAidfYdcj}^juw8aI&t Date: Fri, 12 Jan 2024 09:33:08 -0800 Subject: [PATCH 07/17] Fix LSP tests --- Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs | 2 +- .../Synchronization/VerificationStatusTest.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index cb33dfe5a0e..cda13980ad8 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -127,7 +127,7 @@ public async Task DiagnosticsForVerificationTimeoutHasNameAsRange() { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var diagnostics = await GetLastDiagnostics(documentItem); Assert.Contains("Verification out of resource", diagnostics[0].Message); - Assert.Equal(new Range(0, 20, 0, 42), diagnostics[0].Range); + Assert.Equal(new Range(0, 31, 0, 53), diagnostics[0].Range); } [Fact] diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 124304b40d9..21fe1e30c24 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -430,7 +430,7 @@ await SetUp(options => { var successfulRun = await client.RunSymbolVerification(new TextDocumentIdentifier(documentItem.Uri), methodHeader, CancellationToken); Assert.True(successfulRun); - var range = new Range(0, 20, 0, 42); + var range = new Range(0, 31, 0, 53); await WaitForStatus(range, PublishedVerificationStatus.Running, CancellationToken); await WaitForStatus(range, PublishedVerificationStatus.Error, CancellationToken); From cf98d8063b8863fe5341d173a676f10b96cb9372 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 12 Jan 2024 10:25:56 -0800 Subject: [PATCH 08/17] Parse resource limits with K, M, and G suffixes Update several tests to use this form on the command line and in attributes. --- Source/DafnyCore/DafnyOptions.cs | 21 +++++++++++++++++++ Source/DafnyCore/Options/BoogieOptionBag.cs | 11 ++++++++++ .../BoogieGenerator.ExpressionTranslator.cs | 8 +++++++ .../LitTests/LitTest/VSI-Benchmarks/b4.dfy | 2 +- .../LitTests/LitTest/cli/solverLog.dfy | 2 +- .../LitTest/dafny0/RlimitMultiplier.dfy | 2 +- .../verification/nonLinearArithmetic.dfy | 4 ++-- .../LitTest/vstte2012/BreadthFirstSearch.dfy | 2 +- 8 files changed, 46 insertions(+), 6 deletions(-) diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 9307b533c69..61d69df90fd 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -358,6 +358,27 @@ private static string[] ParsePluginArguments(string argumentsString) { ).ToArray(); } + public static bool TryParseResourceCount(string value, out uint number) { + uint multiplier = 1; + if (value.EndsWith("G")) { + multiplier = 1_000_000_000; + value = value.TrimEnd('G'); + } else if (value.EndsWith("M")) { + multiplier = 1_000_000; + value = value.TrimEnd('M'); + } else if (value.EndsWith("K")) { + multiplier = 1_000; + value = value.TrimEnd('K'); + } + + var parseSucceeded = uint.TryParse(value, out number); + if (parseSucceeded) { + number = number * multiplier; + } + + return parseSucceeded; + } + ///

/// Automatic shallow-copy constructor /// diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index 324e81d2083..cdadf4a8496 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -63,6 +63,17 @@ public static class BoogieOptionBag { new("--error-limit", () => 5, "Set the maximum number of errors to report (0 for unlimited)."); public static readonly Option SolverResourceLimit = new("--resource-limit", + result => { + var value = result.Tokens[^1].Value; + + if (DafnyOptions.TryParseResourceCount(value, out var number)) { + return number; + } + + result.ErrorMessage = $"Cannot parse resource limit: {value}"; + return 0; + }, + false, @"Specify the maximum resource limit (rlimit) value to pass to Z3. A resource limit is a deterministic alternative to a time limit. The output produced by `--log-format csv` includes the resource use of each proof effort, which you can use to determine an appropriate limit for your program."); public static readonly Option SolverPlugin = new("--solver-plugin", @"Dafny uses Boogie as part of its verification process. This option allows customising that part using a Boogie plugin. More information about Boogie can be found at https://github.com/boogie-org/boogie. Information on how to construct Boogie plugins can be found by looking at the code in https://github.com/boogie-org/boogie/blob/v2.16.3/Source/Provers/SMTLib/ProverUtil.cs#L316"); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index 388932e2662..25675da91a8 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -1963,6 +1963,14 @@ public Boogie.QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) // Do this after the above multiplication because :resource_limit should not be multiplied. if (name == "resource_limit") { name = "rlimit"; + if (parms[0] is Boogie.LiteralExpr litString && litString.isString) { + if (DafnyOptions.TryParseResourceCount(litString.asString, out var resourceLimit)) { + parms[0] = new Boogie.LiteralExpr(litString.tok, BigNum.FromUInt(resourceLimit), litString.Immutable); + } else { + BoogieGenerator.reporter.Error(MessageSource.Verifier, attr.tok, + $"failed to parse resource count: {parms[0]}"); + } + } } kv = new Boogie.QKeyValue(Token.NoToken, name, parms, kv); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy index 043e461374f..36ca3b7c804 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy @@ -136,7 +136,7 @@ class Map { } // Removes key from the domain of M (and does nothing if key wasn't in M to begin with) - method {:resource_limit 3000000} {:vcs_split_on_every_assert} Remove(key: Key) + method {:resource_limit "3M"} {:vcs_split_on_every_assert} Remove(key: Key) requires Valid() modifies Repr ensures Valid() && fresh(Repr - old(Repr)) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy index b4d0e365b4d..80428d08c12 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy @@ -1,4 +1,4 @@ -// RUN: %verify --solver-log="log.smt2" --resource-limit 10000 "%s" > "%t" +// RUN: %verify --solver-log="log.smt2" --resource-limit 10K "%s" > "%t" // RUN: %diff "%s.expect" "%t" // RUN: %OutputCheck --file-to-check "log.smt2" "%s" // CHECK: rlimit 10000 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy index 66bedb5b517..149fcf019e6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy @@ -1,4 +1,4 @@ -// RUN: %verify "%s" --resource-limit 10000000 > "%t" +// RUN: %verify "%s" --resource-limit 10M > "%t" // RUN: %diff "%s.expect" "%t" ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy index 1d7b1c0939b..47aac2d1f72 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy @@ -1,5 +1,5 @@ -// RUN: ! %verify "%s" --disable-nonlinear-arithmetic --resource-limit 1000000 > "%t" -// RUN: ! %verify "%s" --resource-limit 1000000 >> "%t" +// RUN: ! %verify "%s" --disable-nonlinear-arithmetic --resource-limit 1M > "%t" +// RUN: ! %verify "%s" --resource-limit 1M >> "%t" // RUN: %diff "%s.expect" "%t" module Power0 { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy index 657845b89aa..2148dc0d2c2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy @@ -27,7 +27,7 @@ class BreadthFirstSearch // witness. The method could equally well have been written using an // existential quantifier and no ghost out-parameter. method - {:resource_limit 8000000} + {:resource_limit "8M"} {:vcs_split_on_every_assert} BFS(source: Vertex, dest: Vertex, ghost AllVertices: set) returns (d: int, ghost path: List) From 2fd2e0ad96d58b31d404bb225d87196563389a81 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 12 Jan 2024 10:28:49 -0800 Subject: [PATCH 09/17] Add changelog entry --- docs/dev/news/4975.fix | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/4975.fix diff --git a/docs/dev/news/4975.fix b/docs/dev/news/4975.fix new file mode 100644 index 00000000000..4108fb61b5e --- /dev/null +++ b/docs/dev/news/4975.fix @@ -0,0 +1 @@ +The `{:rlimit N}` attribute, which multiplied `N` by 1000 before sending it to Z3, is deprecated in favor of the `{:resource_limit N}` attribute, which can accept string arguments with `K`, `M` and `G` suffixes for brevity. From 25eb261c501722b6613b8aaf9a04ff895362ca9e Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 12 Jan 2024 10:41:16 -0800 Subject: [PATCH 10/17] Update resource limit in Std examples --- Source/DafnyStandardLibraries/examples/dfyconfig.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyStandardLibraries/examples/dfyconfig.toml b/Source/DafnyStandardLibraries/examples/dfyconfig.toml index 4b85bac48f0..463996a5f82 100644 --- a/Source/DafnyStandardLibraries/examples/dfyconfig.toml +++ b/Source/DafnyStandardLibraries/examples/dfyconfig.toml @@ -5,7 +5,7 @@ standard-libraries = true # but consumers don't have to have this option set # to use the standard libraries in general. reads-clauses-on-methods = true -resource-limit = 1000 +resource-limit = 1000000 warn-as-errors = true warn-redundant-assumptions = true warn-contradictory-assumptions = true From cc7f9e9610c46d23fc9a377eef06f8bd934077a5 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 12 Jan 2024 12:30:10 -0800 Subject: [PATCH 11/17] Use bounded multiplication --- Source/DafnyCore/DafnyOptions.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index b3dd2da730c..4c049e1c817 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -373,7 +373,7 @@ public static bool TryParseResourceCount(string value, out uint number) { var parseSucceeded = uint.TryParse(value, out number); if (parseSucceeded) { - number = number * multiplier; + number = Boogie.Util.BoundedMultiply(number, multiplier); } return parseSucceeded; From ddb546bde20ea6a0a86ae7226e95335bf820ab15 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 12 Jan 2024 12:30:35 -0800 Subject: [PATCH 12/17] Format standard library --- .../binaries/DafnyStandardLibraries-cs.doo | Bin 1340 -> 1340 bytes .../binaries/DafnyStandardLibraries-go.doo | Bin 1360 -> 1360 bytes .../binaries/DafnyStandardLibraries-java.doo | Bin 1321 -> 1321 bytes .../binaries/DafnyStandardLibraries-js.doo | Bin 1867 -> 1867 bytes .../DafnyStandardLibraries-notarget.doo | Bin 1314 -> 1314 bytes .../binaries/DafnyStandardLibraries-py.doo | Bin 1331 -> 1331 bytes .../src/Std/JSON/ZeroCopy/Deserializer.dfy | 8 ++++---- 7 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index 2404ac2ac0a44c57cc27b50a70276856241afcbe..56eca2c2dbc166777a13cd0da606c4b65d4c84d0 100644 GIT binary patch delta 41 tcmdnPwTFu*z?+#xgn@y9gW-76M4pRG$CEbRf6NS|CLdw31X2H4Yyksv4om<5 delta 41 tcmdnPwTFu*z?+#xgn@y9gJG-NM4pRGTirI^f6NS|CLdw31X2H4YytQt4U_-? diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo index ec30b3312d557313f947ad64b618b046c3b2dadc..93d2527fdff21b96a8e3717603901833f73b0348 100644 GIT binary patch delta 41 tcmcb>b%Bc~z?+#xgn@y9gW*ilM4pRGXOcGF|IQ4gCf{JO1X04Qwg3t~4aEQe delta 41 tcmcb>b%Bc~z?+#xgn@y9gJGB3M4pRGyWBS3|IQ4gCf{JO1X04QwgCR|4GjPQ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index 146b93f3b514d068dccba06b1f724499df7194c7..e6b61fa07aab1abec8a7d1d04fe8e1b2d6bb18b6 100644 GIT binary patch delta 41 tcmZ3>, - elem: Split, - sep: Split>) + ghost json: ValueParser, + elems: Split>, + elem: Split, + sep: Split>) : (elems': Split>) requires elems.cs.StrictlySplitFrom?(json.cs) requires elems.SplitFrom?(cs0, SuffixedElementsSpec) From 8978f6951100c0f5205c71b4e4e73d9893c9bb85 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 12 Jan 2024 16:42:27 -0800 Subject: [PATCH 13/17] Fix parsing of :resource_limit with suffixes --- .../Verifier/BoogieGenerator.ExpressionTranslator.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index 25675da91a8..5494a3a705c 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -1963,9 +1963,9 @@ public Boogie.QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) // Do this after the above multiplication because :resource_limit should not be multiplied. if (name == "resource_limit") { name = "rlimit"; - if (parms[0] is Boogie.LiteralExpr litString && litString.isString) { - if (DafnyOptions.TryParseResourceCount(litString.asString, out var resourceLimit)) { - parms[0] = new Boogie.LiteralExpr(litString.tok, BigNum.FromUInt(resourceLimit), litString.Immutable); + if (parms[0] is string str) { + if (DafnyOptions.TryParseResourceCount(str, out var resourceLimit)) { + parms[0] = new Boogie.LiteralExpr(attr.tok, BigNum.FromUInt(resourceLimit), true); } else { BoogieGenerator.reporter.Error(MessageSource.Verifier, attr.tok, $"failed to parse resource count: {parms[0]}"); From b8b258367ffb86cf1b3b6aa3ab9a27c305f26410 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 16 Jan 2024 11:34:47 -0800 Subject: [PATCH 14/17] Use exponential notation for resource limits --- Source/DafnyCore/DafnyOptions.cs | 22 +++---------------- .../LitTests/LitTest/VSI-Benchmarks/b4.dfy | 2 +- .../LitTests/LitTest/cli/solverLog.dfy | 4 ++-- .../LitTest/dafny0/RlimitMultiplier.dfy | 2 +- .../verification/nonLinearArithmetic.dfy | 4 ++-- .../LitTest/vstte2012/BreadthFirstSearch.dfy | 2 +- docs/dev/news/4975.fix | 2 +- 7 files changed, 11 insertions(+), 27 deletions(-) diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 4c049e1c817..e482fd02c74 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -7,6 +7,7 @@ using System.Collections.ObjectModel; using System.CommandLine; using System.Diagnostics; +using System.Globalization; using System.Linq; using System.IO; using System.Reflection; @@ -358,25 +359,8 @@ private static string[] ParsePluginArguments(string argumentsString) { ).ToArray(); } - public static bool TryParseResourceCount(string value, out uint number) { - uint multiplier = 1; - if (value.EndsWith("G")) { - multiplier = 1_000_000_000; - value = value.TrimEnd('G'); - } else if (value.EndsWith("M")) { - multiplier = 1_000_000; - value = value.TrimEnd('M'); - } else if (value.EndsWith("K")) { - multiplier = 1_000; - value = value.TrimEnd('K'); - } - - var parseSucceeded = uint.TryParse(value, out number); - if (parseSucceeded) { - number = Boogie.Util.BoundedMultiply(number, multiplier); - } - - return parseSucceeded; + public static bool TryParseResourceCount(string value, out uint result) { + return uint.TryParse(value, NumberStyles.AllowExponent, null, out result); } /// diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy index 36ca3b7c804..6142067e8a1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy @@ -136,7 +136,7 @@ class Map { } // Removes key from the domain of M (and does nothing if key wasn't in M to begin with) - method {:resource_limit "3M"} {:vcs_split_on_every_assert} Remove(key: Key) + method {:resource_limit "3e6"} {:vcs_split_on_every_assert} Remove(key: Key) requires Valid() modifies Repr ensures Valid() && fresh(Repr - old(Repr)) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy index 80428d08c12..1a4ac35e924 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy @@ -1,7 +1,7 @@ -// RUN: %verify --solver-log="log.smt2" --resource-limit 10K "%s" > "%t" +// RUN: %verify --solver-log="log.smt2" --resource-limit 10e3 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // RUN: %OutputCheck --file-to-check "log.smt2" "%s" -// CHECK: rlimit 10000 +// CHECK: rlimit 10000\) method m() { assert 1 + 1 == 2; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy index 149fcf019e6..693d0ffd17c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy @@ -1,4 +1,4 @@ -// RUN: %verify "%s" --resource-limit 10M > "%t" +// RUN: %verify "%s" --resource-limit 10e6 > "%t" // RUN: %diff "%s.expect" "%t" ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy index 47aac2d1f72..c8fa2bea365 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy @@ -1,5 +1,5 @@ -// RUN: ! %verify "%s" --disable-nonlinear-arithmetic --resource-limit 1M > "%t" -// RUN: ! %verify "%s" --resource-limit 1M >> "%t" +// RUN: ! %verify "%s" --disable-nonlinear-arithmetic --resource-limit 1e6 > "%t" +// RUN: ! %verify "%s" --resource-limit 1e6 >> "%t" // RUN: %diff "%s.expect" "%t" module Power0 { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy index 2148dc0d2c2..2b85d89b705 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy @@ -27,7 +27,7 @@ class BreadthFirstSearch // witness. The method could equally well have been written using an // existential quantifier and no ghost out-parameter. method - {:resource_limit "8M"} + {:resource_limit "8e6"} {:vcs_split_on_every_assert} BFS(source: Vertex, dest: Vertex, ghost AllVertices: set) returns (d: int, ghost path: List) diff --git a/docs/dev/news/4975.fix b/docs/dev/news/4975.fix index 4108fb61b5e..5d1e6ebbac4 100644 --- a/docs/dev/news/4975.fix +++ b/docs/dev/news/4975.fix @@ -1 +1 @@ -The `{:rlimit N}` attribute, which multiplied `N` by 1000 before sending it to Z3, is deprecated in favor of the `{:resource_limit N}` attribute, which can accept string arguments with `K`, `M` and `G` suffixes for brevity. +The `{:rlimit N}` attribute, which multiplied `N` by 1000 before sending it to Z3, is deprecated in favor of the `{:resource_limit N}` attribute, which can accept string arguments with exponential notation for brevity. From 3899f12d8ef2d49e822338ed3385ebb7a142c305 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 17 Jan 2024 10:21:05 -0800 Subject: [PATCH 15/17] Update changelog to mention --resource-limit --- docs/dev/news/4975.fix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/dev/news/4975.fix b/docs/dev/news/4975.fix index 5d1e6ebbac4..fe67d2072d0 100644 --- a/docs/dev/news/4975.fix +++ b/docs/dev/news/4975.fix @@ -1 +1 @@ -The `{:rlimit N}` attribute, which multiplied `N` by 1000 before sending it to Z3, is deprecated in favor of the `{:resource_limit N}` attribute, which can accept string arguments with exponential notation for brevity. +The `{:rlimit N}` attribute, which multiplied `N` by 1000 before sending it to Z3, is deprecated in favor of the `{:resource_limit N}` attribute, which can accept string arguments with exponential notation for brevity. The `--resource-limit` flag also now omits the multiplication and allows exponential notation. From 872e54a8a8f6ff5d30c3713fcedb7ef776a358af Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 17 Jan 2024 11:26:01 -0800 Subject: [PATCH 16/17] Use named parameter --- Source/DafnyCore/Options/BoogieOptionBag.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index cdadf4a8496..5bbf99a944e 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -73,7 +73,7 @@ public static class BoogieOptionBag { result.ErrorMessage = $"Cannot parse resource limit: {value}"; return 0; }, - false, + isDefault: false, @"Specify the maximum resource limit (rlimit) value to pass to Z3. A resource limit is a deterministic alternative to a time limit. The output produced by `--log-format csv` includes the resource use of each proof effort, which you can use to determine an appropriate limit for your program."); public static readonly Option SolverPlugin = new("--solver-plugin", @"Dafny uses Boogie as part of its verification process. This option allows customising that part using a Boogie plugin. More information about Boogie can be found at https://github.com/boogie-org/boogie. Information on how to construct Boogie plugins can be found by looking at the code in https://github.com/boogie-org/boogie/blob/v2.16.3/Source/Provers/SMTLib/ProverUtil.cs#L316"); From a9ee82c43de903ecb4ca33349642f0c29a5b33d8 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 17 Jan 2024 11:26:42 -0800 Subject: [PATCH 17/17] Add check for incompatible attributes to resolver --- .../DafnyCore/AST/Modules/ModuleDefinition.cs | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 933c86c1f6c..56228a4cf01 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -689,6 +689,22 @@ private static PrefixNameModule ShortenPrefix(PrefixNameModule prefixNameModule) return prefixNameModule with { Parts = rest }; } + private static readonly List<(string, string)> incompatibleAttributePairs = + new() { + ("rlimit", "resource_limit") + }; + + private void CheckIncompatibleAttributes(ModuleResolver resolver, Attributes attrs) { + foreach (var pair in incompatibleAttributePairs) { + var attr1 = Attributes.Find(attrs, pair.Item1); + var attr2 = Attributes.Find(attrs, pair.Item2); + if (attr1 is not null && attr2 is not null) { + resolver.reporter.Error(MessageSource.Resolver, attr1.tok, + $"the {pair.Item1} and {pair.Item2} attributes cannot be used together"); + } + } + } + public ModuleSignature RegisterTopLevelDecls(ModuleResolver resolver, bool useImports) { Contract.Requires(this != null); var sig = new ModuleSignature(); @@ -767,6 +783,9 @@ public ModuleSignature RegisterTopLevelDecls(ModuleResolver resolver, bool useIm foreach (MemberDecl m in members.Values) { Contract.Assert(!m.HasStaticKeyword || Attributes.Contains(m.Attributes, "opaque_reveal")); + + CheckIncompatibleAttributes(resolver, m.Attributes); + if (m is Function or Method or ConstantField) { sig.StaticMembers[m.Name] = m; }