diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs index 4e4ae2a6f..b0dfb3f13 100644 --- a/Source/Core/Monomorphization.cs +++ b/Source/Core/Monomorphization.cs @@ -1301,7 +1301,7 @@ class MonomorphizationVisitor : VarDeclOnceStandardVisitor private readonly HashSet originalConstants; // Note that original axioms refer to axioms of the original program which might have been updated in-place during monomorphization. public readonly Dictionary> originalAxiomToSplitAxioms; - private readonly Dictionary originalAxiomToUninstantiatedCopies; + private readonly Dictionary originalAxiomToUninstantiatedCopy; private MonomorphizationVisitor(CoreOptions options, Program program, HashSet polymorphicFunctionAxioms) { @@ -1310,7 +1310,7 @@ private MonomorphizationVisitor(CoreOptions options, Program program, HashSet ax, _ => new HashSet()); - originalAxiomToUninstantiatedCopies = program.Axioms.ToDictionary(ax => ax, ax => (Axiom) ax.Clone() ); + originalAxiomToUninstantiatedCopy = program.Axioms.ToDictionary(ax => ax, ax => (Axiom) ax.Clone() ); implInstantiations = new Dictionary, Implementation>>(); nameToImplementation = new Dictionary(); program.TopLevelDeclarations.OfType().Where(impl => impl.TypeParameters.Count > 0).ForEach( @@ -1410,7 +1410,7 @@ private static void UpdateDependencies(MonomorphizationVisitor monomorphizationV foreach (var (originalAxiom, newAxioms) in monomorphizationVisitor.originalAxiomToSplitAxioms) { var originalAxiomFc = new FunctionAndConstantCollector(); - var uninstantiatedOriginalAxiom = monomorphizationVisitor.originalAxiomToUninstantiatedCopies[originalAxiom]; + var uninstantiatedOriginalAxiom = monomorphizationVisitor.originalAxiomToUninstantiatedCopy[originalAxiom]; originalAxiomFc.Visit(uninstantiatedOriginalAxiom); var originalAxiomFunctions = originalAxiomFc.Functions; @@ -1440,9 +1440,11 @@ private static void UpdateDependencies(MonomorphizationVisitor monomorphizationV { if (function.TypeParameters.Any()) // Polymorphic function { + var functionInstantiations = + monomorphizationVisitor.functionInstantiations[function].Values.ToHashSet(); var instancesToAddDependency = originalAxiomFunctions.Contains(function) - ? newAxiomFunctions[newAxiom] - : monomorphizationVisitor.functionInstantiations[function].Values.ToHashSet(); + ? newAxiomFunctions[newAxiom].Intersect(functionInstantiations) + : functionInstantiations; foreach (var inst in instancesToAddDependency) { inst.OtherDefinitionAxioms.Add(newAxiom);