diff options
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 2 | ||||
| -rw-r--r-- | Source/Core/BoogiePL.atg | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 7e5651f2..86fda429 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -18,7 +18,7 @@ namespace Microsoft.Boogie { using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
- using Set = GSet<object>;
+ using Set = GSet<object>; // not that the set used is not a set of Variable only, as it also contains TypeVariables
//---------------------------------------------------------------------
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index c7950c9a..33172e7f 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -97,7 +97,7 @@ private class BvBounds : Expr { Contract.Requires(stream != null);
{Contract.Assert(false);throw new cce.UnreachableException();}
}
- public override void ComputeFreeVariables(Set/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }
+ public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }
public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } }
}
|