diff --git a/flake.lock b/flake.lock index 866c7728..0700d9da 100644 --- a/flake.lock +++ b/flake.lock @@ -26,11 +26,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1770303219, - "narHash": "sha256-pUsxUS5TyhYAiVu1VFwKDtPFVNZy9+izjz8LWM8DvBs=", + "lastModified": 1770745295, + "narHash": "sha256-OsHuLEcZnhWIJu4S6lbQlZ4iygwFx7mkFtPUC9E6tME=", "owner": "aeneasverif", "repo": "charon", - "rev": "b684df3a5ec342695a45a9b62a4079235b5e478e", + "rev": "2419dcb26b8d44895bf8c18e7eed2ede9249f6e6", "type": "github" }, "original": { diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 57e0276e..dbaa6dc1 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -2193,7 +2193,7 @@ and expression_of_statement_kind (env : env) (ret_var : C.local_id) (s : C.state (* [ p ]))) *) | _ -> Krml.Helpers.eunit end - | Assert a -> expression_of_assertion env a + | Assert (a, _on_failure) -> expression_of_assertion env a | Call { func =