diff --git a/src/JSON/ZeroCopy/Deserializer.dfy b/src/JSON/ZeroCopy/Deserializer.dfy index 45c0c66e..75e7e1f6 100644 --- a/src/JSON/ZeroCopy/Deserializer.dfy +++ b/src/JSON/ZeroCopy/Deserializer.dfy @@ -238,7 +238,7 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer { elems' } - function {:rlimit 1000} {:vcs_split_on_every_assert} {:opaque} AppendLast(ghost cs0: FreshCursor, + function {:rlimit 100} {:vcs_split_on_every_assert} {:opaque} AppendLast(ghost cs0: FreshCursor, ghost json: ValueParser, elems: Split>, elem: Split,