Boogie: Removed and completed a task comment

1 files changed, 2 insertions, 1 deletions

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index cf0bcaa4..c36551d6 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -72,7 +72,7 @@ void ObjectInvariant()
     // constructor to allow cloning

     [NotDelayed]

     internal TypeAxiomBuilderPremisses(TypeAxiomBuilderPremisses builder)

-      : base(builder) {//TODO: Possible troublespot

+      : base(builder) {

       Contract.Requires(builder != null);

       TypeFunction = builder.TypeFunction;

       Typed2UntypedFunctions =

@@ -321,6 +321,7 @@ Contract.Requires(cce.NonNullElements(extractors));
 

     // Globally defined functions

     private readonly IDictionary<Function/*!*/, UntypedFunction/*!*/>/*!*/ Typed2UntypedFunctions; 

+    [ContractInvariantMethod]

 void Typed2UntypedFunctionsInvariantMethod(){

 Contract.Invariant(cce.NonNullElements(Typed2UntypedFunctions));}