From daf9d219d3d224e2da3f3e02e674f02899dfb9f9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Oct 2019 14:25:45 -0700 Subject: [PATCH] fix: must reset assignments before each iteration Reason: the join points cached values are incorrect since they were computed using the previous values for `funVals`. --- library/Init/Lean/Compiler/IR/UnreachBranches.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/library/Init/Lean/Compiler/IR/UnreachBranches.lean b/library/Init/Lean/Compiler/IR/UnreachBranches.lean index d13a005891..c3b7251f07 100644 --- a/library/Init/Lean/Compiler/IR/UnreachBranches.lean +++ b/library/Init/Lean/Compiler/IR/UnreachBranches.lean @@ -221,6 +221,7 @@ partial def interpFnBody : FnBody → M Unit def inferStep : M Bool := do ctx ← read; + modify $ fun s => { assignments := ctx.decls.map $ fun _ => {}, .. s }; ctx.decls.size.mfold (fun idx modified => do match ctx.decls.get! idx with | Decl.fdecl fid ys _ b => do