From 9a8c6aa15ee4838606db0810b1ea0cc9fa6d515b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Mon, 2 Sep 2024 23:20:53 +0200 Subject: [PATCH] chore: update F* --- flake.lock | 6 +++--- hacl-star-snapshot/lib/Lib.Sequence.fsti | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/flake.lock b/flake.lock index a9d58fe..43d0a9f 100644 --- a/flake.lock +++ b/flake.lock @@ -72,11 +72,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1724778396, - "narHash": "sha256-qCB4uPRJyxtjYQ9eJob0mWSxjz2A+Eg0ujsCuTBKx8k=", + "lastModified": 1725149949, + "narHash": "sha256-b72qTbJJN51zAOyR9R8LKi0G+J3OPiaYCIHZx3V8yBE=", "owner": "FStarLang", "repo": "FStar", - "rev": "8b8de3fffccfa756e4ce3632aa00932ccb9999d7", + "rev": "5db2e80d643942aa5cb7a1f7fafe2c3a60d3a60b", "type": "github" }, "original": { diff --git a/hacl-star-snapshot/lib/Lib.Sequence.fsti b/hacl-star-snapshot/lib/Lib.Sequence.fsti index 9bced54..3382ac1 100644 --- a/hacl-star-snapshot/lib/Lib.Sequence.fsti +++ b/hacl-star-snapshot/lib/Lib.Sequence.fsti @@ -463,7 +463,7 @@ val lemma_map_blocks: (* Computes the block of the i-th element of (map_blocks blocksize input f g) *) -#push-options "--z3rlimit 50" +#push-options "--z3rlimit 100" let get_block (#a:Type) (#len:nat)