diff --git a/charon-pin b/charon-pin index 1922211c..8dbc03bb 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -5984bd9b25b01afad4762efc250220bb969e59d4 +8a17efc262ef3af377ab172efc865edcf1bb40ea diff --git a/flake.lock b/flake.lock index d8e43085..8a08ed8e 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1735820899, - "narHash": "sha256-EaF0qwltokDO9joM6BNBS5WuDz8eBVwydoWCEhBhhKg=", + "lastModified": 1736180214, + "narHash": "sha256-BtyLLaWlN/b8SC/6eL0f9Imaoq71bHjAWh/ASugXxfk=", "owner": "aeneasverif", "repo": "charon", - "rev": "5984bd9b25b01afad4762efc250220bb969e59d4", + "rev": "8a17efc262ef3af377ab172efc865edcf1bb40ea", "type": "github" }, "original": { @@ -177,11 +177,11 @@ ] }, "locked": { - "lastModified": 1735784864, - "narHash": "sha256-tIl5p3ueaPw7T5T1UXkLc8ISMk6Y8CI/D/rd0msf73I=", + "lastModified": 1736216977, + "narHash": "sha256-EMueGrzBpryM8mgOyoyJ7DdNRRk09ug1ggcLLp0WrCQ=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "04d5f1836721461b256ec452883362c5edc5288e", + "rev": "bbe7e4e7a70d235db4bbdcabbf8a2f6671881dd7", "type": "github" }, "original": { diff --git a/src/interp/InterpreterStatements.ml b/src/interp/InterpreterStatements.ml index bf2a91e8..9ab06402 100644 --- a/src/interp/InterpreterStatements.ml +++ b/src/interp/InterpreterStatements.ml @@ -738,8 +738,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) let fn_ref = Option.get (Substitute.lookup_and_subst_trait_decl_provided_method - trait_decl method_name trait_decl_ref.decl_generics - func.generics) + trait_decl method_name trait_ref func.generics) in let method_id = fn_ref.fun_id in let method_def = ctx_lookup_fun_decl ctx method_id in @@ -772,7 +771,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) let fn_ref = Option.get (Substitute.lookup_and_subst_trait_decl_method trait_decl - method_name trait_decl_ref.decl_generics func.generics) + method_name trait_ref func.generics) in let method_id = fn_ref.fun_id in let generics = fn_ref.fun_generics in