fixed type checking errors in QED stuff

1 files changed, 0 insertions, 3 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index d1651ff4..6c333143 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2363,10 +2363,7 @@ namespace Microsoft.Boogie {
           tc.Error(this, "atomic specification allowed only in a yielding procedure");

           return;

       }

-      bool oldYields = tc.Yields;

-      tc.Yields = isAtomicSpecification;

       this.Condition.Typecheck(tc);

-      tc.Yields = oldYields;

       Contract.Assert(this.Condition.Type != null);  // follows from postcondition of Expr.Typecheck

       if (!this.Condition.Type.Unify(Type.Bool)) {

         tc.Error(this, "postconditions must be of type bool");