cleaned up the OG code

enabled it to be always on

1 files changed, 2 insertions, 1 deletions

diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 71471413..b86e0a54 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -558,6 +558,7 @@ namespace Microsoft.Boogie {
 

   public class TypecheckingContext : CheckingContext {

     public List<IdentifierExpr> Frame;  // used in checking the assignment targets of implementation bodies

+    public bool Yields;

 

     public TypecheckingContext(IErrorSink errorSink)

       : base(errorSink) {

@@ -566,7 +567,7 @@ namespace Microsoft.Boogie {
     public bool InFrame(Variable v) {

       Contract.Requires(v != null);

       Contract.Requires(Frame != null);

-      return Frame.Any(f => f.Decl == v);

+      return Frame.Any(f => f.Decl == v) || Yields;

     }

   }

 }