Skip to content
This repository was archived by the owner on May 4, 2024. It is now read-only.

Commit 7b24d06

Browse files
authored
[move-prover] fix field type instantiation in borrow edge (#350)
1 parent f963939 commit 7b24d06

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

language/move-prover/boogie-backend/src/bytecode_translator.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -1611,7 +1611,7 @@ impl<'env> FunctionTranslator<'env> {
16111611
let field_env = &struct_env.get_field_by_offset(*offset);
16121612
let sel_fun = boogie_field_sel(field_env, &memory.inst);
16131613
let new_dest = format!("{}({})", sel_fun, (*mk_dest)());
1614-
let new_dest_ty = &self.inst(&field_env.get_type());
1614+
let new_dest_ty = &field_env.get_type().instantiate(&memory.inst);
16151615
let mut new_dest_needed = false;
16161616
let new_src = self.translate_write_back_update(
16171617
new_dest_ty,

0 commit comments

Comments
 (0)