Worked on more native support for partially-verified assertions.

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 {