diff options
Diffstat (limited to 'Source/Core/AbsyCmd.cs')
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 25 |
1 files changed, 20 insertions, 5 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 231ae272..746e70c0 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2664,11 +2664,6 @@ namespace Microsoft.Boogie { {
result = LiteralExpr.And(result, c);
result.Type = Type.Bool;
- var nAryExpr = result as NAryExpr;
- if (nAryExpr != null)
- {
- nAryExpr.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
- }
}
else
{
@@ -2757,6 +2752,26 @@ namespace Microsoft.Boogie { public Expr OrigExpr;
public Dictionary<Variable, Expr> IncarnationMap;
+ Expr verifiedUnder;
+ public Expr VerifiedUnder
+ {
+ get
+ {
+ if (verifiedUnder != null)
+ {
+ return verifiedUnder;
+ }
+ verifiedUnder = QKeyValue.FindExprAttribute(Attributes, "verified_under");
+ return verifiedUnder;
+ }
+ }
+
+ public void MarkAsVerifiedUnder(Expr expr)
+ {
+ Attributes = new QKeyValue(tok, "verified_under", new List<object> { expr }, Attributes);
+ verifiedUnder = expr;
+ }
+
// TODO: convert to use generics
private object errorData;
public object ErrorData {
|