bug fixes in Duplicate.cs and parsing of invariant attributes

other bug fixes in QED stuff

9 files changed, 168 insertions, 74 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 38902d57..579c9cf6 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -393,7 +393,9 @@ namespace Microsoft.Boogie
             Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).Compute();

             ensures.Add(new Ensures(false, transitionRelation));

             string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);

-            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, new List<IdentifierExpr>(), ensures);

+            List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

+            program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));

+            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);

             impl.Proc = proc;

             this.decls.Add(impl);

@@ -424,7 +426,9 @@ namespace Microsoft.Boogie
                 ensures.Add(new Ensures(false, assertCmd.Expr));

             }

             string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

-            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, new List<IdentifierExpr>(), ensures);

+            List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

+            program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));

+            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);

             impl.Proc = proc;

             this.decls.Add(impl);

@@ -496,7 +500,9 @@ namespace Microsoft.Boogie
             List<Block> blocks = new List<Block>();

             blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));

             string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

-            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, new List<IdentifierExpr>(), ensures);

+            List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

+            program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));

+            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);

             impl.Proc = proc;

             this.decls.Add(impl);

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index ee1547f2..5aff9bb7 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -76,6 +76,7 @@ namespace Microsoft.Boogie
         {

             CallCmd callCmd = (CallCmd) base.VisitCallCmd(node);

             callCmd.Proc = VisitProcedure(callCmd.Proc);

+            callCmd.callee = callCmd.Proc.Name;

             absyMap[node] = callCmd;

             return callCmd;

         }

@@ -86,6 +87,7 @@ namespace Microsoft.Boogie
             foreach (CallCmd callCmd in parCallCmd.CallCmds)

             {

                 callCmd.Proc = VisitProcedure(callCmd.Proc);

+                callCmd.callee = callCmd.Proc.Name;

             }

             absyMap[node] = parCallCmd;

             return parCallCmd;

@@ -96,46 +98,54 @@ namespace Microsoft.Boogie
             if (!QKeyValue.FindBoolAttribute(node.Attributes, "yields"))

                 return node;

             if (!procMap.ContainsKey(node))

-                procMap[node] = base.VisitProcedure(node);

+            {

+                Procedure proc = (Procedure)node.Clone();

+                proc.Name = string.Format("{0}_{1}", node.Name, phaseNum);

+                proc.InParams = this.VisitVariableSeq(node.InParams);

+                proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies);

+                proc.OutParams = this.VisitVariableSeq(node.OutParams);

+                if (moverTypeChecker.procToActionInfo.ContainsKey(node) && moverTypeChecker.procToActionInfo[node].phaseNum < phaseNum)

+                {

+                    proc.Requires = new List<Requires>();

+                    proc.Ensures = new List<Ensures>();

+                }

+                else

+                {

+                    proc.Requires = this.VisitRequiresSeq(node.Requires);

+                    proc.Ensures = this.VisitEnsuresSeq(node.Ensures);

+                }

+                procMap[node] = proc;

+            }

             return procMap[node];

         }

 

         public override Implementation VisitImplementation(Implementation node)

         {

-            if (moverTypeChecker.procToActionInfo.ContainsKey(node.Proc) && moverTypeChecker.procToActionInfo[node.Proc].phaseNum < phaseNum)

+            Implementation impl = base.VisitImplementation(node);

+            impl.Name = impl.Proc.Name;

+            foreach (Block block in impl.Blocks)

             {

-                CodeExpr action = (CodeExpr) VisitCodeExpr(moverTypeChecker.procToActionInfo[node.Proc].thisAction);

-                Implementation impl = new Implementation(Token.NoToken, node.Name, node.Proc.TypeParameters, node.Proc.InParams, node.Proc.OutParams, new List<Variable>(), action.Blocks);

-                impl.Proc = VisitProcedure(node.Proc);

-                impl.Proc.AddAttribute("inline", 1);

-                impl.AddAttribute("inline", 1);

-                return impl;

-            }

-            else

-            {

-                Implementation impl = base.VisitImplementation(node);

-                foreach (Block block in impl.Blocks)

+                GotoCmd gotoCmd = block.TransferCmd as GotoCmd;

+                if (gotoCmd == null) continue;

+                List<Block> labelTargets = new List<Block>();

+                List<string> labelNames = new List<string>();

+                foreach (Block x in gotoCmd.labelTargets)

                 {

-                    GotoCmd gotoCmd = block.TransferCmd as GotoCmd;

-                    if (gotoCmd == null) continue;

-                    List<Block> labelTargets = new List<Block>();

-                    List<string> labelNames = new List<string>();

-                    foreach (Block x in gotoCmd.labelTargets)

-                    {

-                        Block y = (Block)absyMap[x];

-                        labelTargets.Add(y);

-                        labelNames.Add(y.Label);

-                    }

-                    gotoCmd.labelTargets = labelTargets;

-                    gotoCmd.labelNames = labelNames;

+                    Block y = (Block)absyMap[x];

+                    labelTargets.Add(y);

+                    labelNames.Add(y.Label);

                 }

-                return impl;

+                gotoCmd.labelTargets = labelTargets;

+                gotoCmd.labelNames = labelNames;

             }

+            return impl;

         }

 

         public override Requires VisitRequires(Requires node)

         {

             Requires requires = base.VisitRequires(node);

+            if (node.Free)

+                return requires;

             if (QKeyValue.FindIntAttribute(requires.Attributes, "phase", int.MaxValue) != phaseNum)

                 requires.Condition = Expr.True;

             return requires;

@@ -144,8 +154,13 @@ namespace Microsoft.Boogie
         public override Ensures VisitEnsures(Ensures node)

         {

             Ensures ensures = base.VisitEnsures(node);

+            if (node.Free)

+                return ensures;

             if (ensures.IsAtomicSpecification || QKeyValue.FindIntAttribute(ensures.Attributes, "phase", int.MaxValue) != phaseNum)

+            {

                 ensures.Condition = Expr.True;

+                ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);

+            }

             return ensures;

         }

 

@@ -162,6 +177,7 @@ namespace Microsoft.Boogie
     {

         LinearTypeChecker linearTypeChecker;

         Dictionary<Absy, Absy> absyMap;

+        int phaseNum;

         List<Declaration> decls;

         List<IdentifierExpr> globalMods;

         Dictionary<string, Procedure> asyncAndParallelCallDesugarings;

@@ -169,10 +185,11 @@ namespace Microsoft.Boogie
         List<Implementation> yieldCheckerImpls;

         Procedure yieldProc;

 

-        public OwickiGries(LinearTypeChecker linearTypeChecker, Dictionary<Absy, Absy> absyMap, List<Declaration> decls)

+        public OwickiGries(LinearTypeChecker linearTypeChecker, Dictionary<Absy, Absy> absyMap, int phaseNum, List<Declaration> decls)

         {

             this.linearTypeChecker = linearTypeChecker;

             this.absyMap = absyMap;

+            this.phaseNum = phaseNum;

             this.decls = decls;

             Program program = linearTypeChecker.program;

             globalMods = new List<IdentifierExpr>();

@@ -216,7 +233,7 @@ namespace Microsoft.Boogie
                     Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);

                     inputs.Add(f);

                 }

-                yieldProc = new Procedure(Token.NoToken, "og_yield", new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

+                yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", phaseNum), new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

                 yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

             }

             CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());

@@ -341,8 +358,7 @@ namespace Microsoft.Boogie
                     }

                     count++;

                 }

-                proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), ensuresSeq);

-                proc.AddAttribute("yields");

+                proc = new Procedure(Token.NoToken, string.Format("{0}_{1}", procName, phaseNum), new List<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), ensuresSeq);

                 asyncAndParallelCallDesugarings[procName] = proc;

             }

             CallCmd dummyCallCmd = new CallCmd(Token.NoToken, proc.Name, ins, outs);

@@ -437,7 +453,7 @@ namespace Microsoft.Boogie
             yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));

 

             // Create the yield checker procedure

-            var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);

+            var yieldCheckerName = string.Format("{0}_YieldChecker_{1}_{2}", decl is Procedure ? "Proc" : "Impl", decl.Name, phaseNum);

             var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

             yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

             yieldCheckerProcs.Add(yieldCheckerProc);

@@ -577,7 +593,7 @@ namespace Microsoft.Boogie
                         {

                             if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))

                             {

-                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());

+                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}_{1}", callCmd.Proc.Name, phaseNum), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());

                             }

                             var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];

                             CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);

@@ -847,13 +863,47 @@ namespace Microsoft.Boogie
             decls.Add(yieldImpl);

         }

 

-        private QKeyValue RemoveYieldsAttribute(QKeyValue iter)

+        private static QKeyValue RemoveYieldsAttribute(QKeyValue iter)

         {

             if (iter == null) return null;

             iter.Next = RemoveYieldsAttribute(iter.Next);

             return (QKeyValue.FindBoolAttribute(iter, "yields")) ? iter.Next : iter;

         }

 

+        public static QKeyValue RemoveStableAttribute(QKeyValue iter)

+        {

+            if (iter == null) return null;

+            iter.Next = RemoveStableAttribute(iter.Next);

+            return (QKeyValue.FindBoolAttribute(iter, "stable")) ? iter.Next : iter;

+        }

+

+        public static QKeyValue RemovePhaseAttribute(QKeyValue iter)

+        {

+            if (iter == null) return null;

+            iter.Next = RemovePhaseAttribute(iter.Next);

+            return (QKeyValue.FindIntAttribute(iter, "phase", int.MaxValue) != int.MaxValue) ? iter.Next : iter;

+        }

+

+        public static QKeyValue RemoveQedAttribute(QKeyValue iter)

+        {

+            if (iter == null) return null;

+            iter.Next = RemoveQedAttribute(iter.Next);

+            return QKeyValue.FindBoolAttribute(iter, "qed") ? iter.Next : iter;

+        }

+

+        public static QKeyValue RemoveMoverAttribute(QKeyValue iter)

+        {

+            if (iter == null) return null;

+            iter.Next = RemoveMoverAttribute(iter.Next);

+            if (QKeyValue.FindIntAttribute(iter, "atomic", int.MaxValue) != int.MaxValue ||

+                QKeyValue.FindIntAttribute(iter, "right", int.MaxValue) != int.MaxValue ||

+                QKeyValue.FindIntAttribute(iter, "left", int.MaxValue) != int.MaxValue ||

+                QKeyValue.FindIntAttribute(iter, "both", int.MaxValue) != int.MaxValue) 

+                return iter.Next;

+            else 

+                return iter;

+        }

+

         public void Transform(List<Implementation> impls, List<Procedure> procs)

         {

             foreach (var impl in impls)

@@ -889,12 +939,14 @@ namespace Microsoft.Boogie
                         proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g));

                     }

                     proc.Attributes = RemoveYieldsAttribute(proc.Attributes);

+                    proc.Attributes = RemoveStableAttribute(proc.Attributes);

                 }

                 decls.Add(proc);

             }

             foreach (var impl in impls)

             {

                 impl.Attributes = RemoveYieldsAttribute(impl.Attributes);

+                impl.Attributes = RemoveStableAttribute(impl.Attributes);

                 decls.Add(impl);

             }

         }

@@ -904,29 +956,41 @@ namespace Microsoft.Boogie
             Program program = linearTypeChecker.program;

             foreach (int phaseNum in moverTypeChecker.assertionPhaseNums)

             {

-                MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, int.MaxValue);

+                MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, phaseNum);

                 List<Implementation> impls = new List<Implementation>();

                 List<Procedure> procs = new List<Procedure>();

                 foreach (var decl in program.TopLevelDeclarations)

                 {

-                    Implementation impl = decl as Implementation;

-                    if (impl == null || !QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) continue;

-                    Implementation duplicateImpl = duplicator.VisitImplementation(impl);

-                    impls.Add(duplicateImpl);

-                    procs.Add(duplicateImpl.Proc);

+                    Procedure proc = decl as Procedure;

+                    if (proc == null || !QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;

+                    Procedure duplicateProc = duplicator.VisitProcedure(proc);

+                    procs.Add(duplicateProc);

+                    if (moverTypeChecker.procToActionInfo.ContainsKey(proc) && moverTypeChecker.procToActionInfo[proc].phaseNum < phaseNum)

+                    {

+                        CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(moverTypeChecker.procToActionInfo[proc].thisAction);

+                        Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, new List<Variable>(), action.Blocks);

+                        impl.Proc = duplicateProc;

+                        impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

+                        impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

+                        impls.Add(impl);

+                    }

                 }

                 foreach (var decl in program.TopLevelDeclarations)

                 {

-                    Procedure proc = decl as Procedure;

-                    if (proc == null || !QKeyValue.FindBoolAttribute(proc.Attributes, "yields") || duplicator.procMap.ContainsKey(proc)) continue;

-                    procs.Add(duplicator.VisitProcedure(proc));

+                    Implementation impl = decl as Implementation;

+                    if (impl == null || 

+                        !QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields") ||

+                        (moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) && moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum)) 

+                        continue;

+                    Implementation duplicateImpl = duplicator.VisitImplementation(impl);

+                    impls.Add(duplicateImpl);

                 }

                 Dictionary<Absy, Absy> reverseAbsyMap = new Dictionary<Absy, Absy>();

                 foreach (Absy key in duplicator.absyMap.Keys)

                 {

                     reverseAbsyMap[duplicator.absyMap[key]] = key;

                 }

-                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, reverseAbsyMap, decls);

+                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, reverseAbsyMap, phaseNum, decls);

                 ogTransform.Transform(impls, procs);

             }

         }

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 91680403..254f058d 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -121,6 +121,7 @@ namespace Microsoft.Boogie
             {

                 if (block.TransferCmd is ReturnExprCmd)

                 {

+                    block.TransferCmd = new ReturnCmd(block.TransferCmd.tok);

                     blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);

                     continue;

                 }

@@ -194,7 +195,10 @@ namespace Microsoft.Boogie
             foreach (var g in program.GlobalVariables())

             {

                 if (QKeyValue.FindBoolAttribute(g.Attributes, "qed"))

+                {

                     this.qedGlobalVariables.Add(g);

+                    g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);

+                }

             }

             this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();

             this.assertionPhaseNums = new HashSet<int>();

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 65e91db5..66e9d4a6 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1821,7 +1821,7 @@ namespace Microsoft.Boogie {
   }

 

   public class CallCmd : CallCommonality, IPotentialErrorNode {

-    public string/*!*/ callee { get; private set; }

+    public string/*!*/ callee { get; set; }

     public Procedure Proc;

 

     // Element of the following lists can be null, which means that

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 42bb7b34..e954944f 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -809,6 +809,7 @@ WhileCmd<out WhileCmd/*!*/ wcmd>
                          } else {

                            invariants.Add(new AssertCmd(z, e, kv));

                          }

+						 kv = null;

                       .)

     ";"

   }

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 0c49867c..07ccba77 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -25,6 +25,18 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Cmd>() != null);

       return base.VisitAssertCmd((AssertCmd)node.Clone());

     }

+    public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node)

+    {

+        //Contract.Requires(node != null);

+        Contract.Ensures(Contract.Result<Cmd>() != null);

+        return base.VisitAssertEnsuresCmd((AssertEnsuresCmd)node.Clone());

+    }

+    public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node)

+    {

+        //Contract.Requires(node != null);

+        Contract.Ensures(Contract.Result<Cmd>() != null);

+        return base.VisitAssertRequiresCmd((AssertRequiresCmd)node.Clone());

+    }

     public override Cmd VisitAssignCmd(AssignCmd node) {

       //Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Cmd>() != null);

@@ -149,6 +161,18 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<DeclWithFormals>() != null);

       return base.VisitDeclWithFormals((DeclWithFormals)node.Clone());

     }

+    public override Ensures VisitEnsures(Ensures node)

+    {

+        //Contract.Requires(node != null);

+        Contract.Ensures(Contract.Result<Ensures>() != null);

+        return base.VisitEnsures((Ensures)node.Clone());

+    }

+    public override List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq)

+    {

+        //Contract.Requires(ensuresSeq != null);

+        Contract.Ensures(Contract.Result<List<Ensures>>() != null);

+        return base.VisitEnsuresSeq(new List<Ensures>(ensuresSeq));

+    }

     public override ExistsExpr VisitExistsExpr(ExistsExpr node) {

       //Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<ExistsExpr>() != null);

@@ -266,6 +290,18 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<BinderExpr>() != null);

       return base.VisitBinderExpr((BinderExpr)node.Clone());

     }

+    public override Requires VisitRequires(Requires node)

+    {

+        //Contract.Requires(node != null);

+        Contract.Ensures(Contract.Result<Requires>() != null);

+        return base.VisitRequires((Requires)node.Clone());

+    }

+    public override List<Requires> VisitRequiresSeq(List<Requires> requiresSeq)

+    {

+        //Contract.Requires(requiresSeq != null);

+        Contract.Ensures(Contract.Result<List<Requires>>() != null);

+        return base.VisitRequiresSeq(new List<Requires>(requiresSeq));

+    }

     public override Cmd VisitRE(RE node) {

       //Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Cmd>() != null);

@@ -332,26 +368,6 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<List<Variable>>() != null);

       return base.VisitVariableSeq(new List<Variable>(variableSeq));

     }

-    public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {

-      //Contract.Requires(node != null);

-      Contract.Ensures(Contract.Result<Cmd>() != null);

-      return base.VisitAssertRequiresCmd((AssertRequiresCmd)node.Clone());

-    }

-    public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) {

-      //Contract.Requires(node != null);

-      Contract.Ensures(Contract.Result<Cmd>() != null);

-      return base.VisitAssertEnsuresCmd((AssertEnsuresCmd)node.Clone());

-    }

-    public override Ensures VisitEnsures(Ensures node) {

-      //Contract.Requires(node != null);

-      Contract.Ensures(Contract.Result<Ensures>() != null);

-      return base.VisitEnsures((Ensures)node.Clone());

-    }

-    public override Requires VisitRequires(Requires node) {

-      //Contract.Requires(node != null);

-      Contract.Ensures(Contract.Result<Requires>() != null);

-      return base.VisitRequires((Requires)node.Clone());

-    }

     public override YieldCmd VisitYieldCmd(YieldCmd node)

     {

         //Contract.Requires(node != null);

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index f1cae496..8049c220 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1147,6 +1147,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 			} else {

 			 invariants.Add(new AssertCmd(z, e, kv));

 			}

+			kv = null;

 			

 			Expect(8);

 		}

diff --git a/Test/og/Answer b/Test/og/Answer
index 8397d051..54ceb547 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -3,7 +3,7 @@
 foo.bpl(14,3): Error BP5001: This assertion might not hold.

 Execution trace:

     foo.bpl(6,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC$0$L0

+    (0,0): inline$Impl_YieldChecker_PC_2147483647_2147483647$0$L0

 

 Boogie program verifier finished with 4 verified, 1 error

 

@@ -11,11 +11,11 @@ Boogie program verifier finished with 4 verified, 1 error
 bar.bpl(13,3): Error BP5001: This assertion might not hold.

 Execution trace:

     bar.bpl(6,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC$0$L0

+    (0,0): inline$Impl_YieldChecker_PC_2147483647_2147483647$0$L0

 bar.bpl(13,3): Error BP5001: This assertion might not hold.

 Execution trace:

     bar.bpl(23,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC$0$L0

+    (0,0): inline$Impl_YieldChecker_PC_2147483647_2147483647$0$L0

 

 Boogie program verifier finished with 3 verified, 2 errors

 

@@ -27,11 +27,11 @@ Boogie program verifier finished with 2 verified, 0 errors
 parallel1.bpl(10,1): Error BP5001: This assertion might not hold.

 Execution trace:

     parallel1.bpl(6,5): anon0

-    (0,0): inline$Proc_YieldChecker_PC$0$L0

+    (0,0): inline$Proc_YieldChecker_PC_2147483647_2147483647$0$L0

 parallel1.bpl(14,3): Error BP5001: This assertion might not hold.

 Execution trace:

     parallel1.bpl(6,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC$0$L0

+    (0,0): inline$Impl_YieldChecker_PC_2147483647_2147483647$0$L0

 

 Boogie program verifier finished with 3 verified, 2 errors

 

@@ -75,7 +75,7 @@ Boogie program verifier finished with 3 verified, 0 errors
 t1.bpl(35,5): Error BP5001: This assertion might not hold.

 Execution trace:

     (0,0): og_init

-    (0,0): inline$Impl_YieldChecker_A$0$L1

+    (0,0): inline$Impl_YieldChecker_A_2147483647_2147483647$0$L1

 

 Boogie program verifier finished with 2 verified, 1 error

 

@@ -92,6 +92,6 @@ async.bpl(14,1): Error BP5001: This assertion might not hold.
 Execution trace:

     async.bpl(7,3): anon0

     async.bpl(7,3): anon0$1

-    (0,0): inline$Proc_YieldChecker_P$1$L0

+    (0,0): inline$Proc_YieldChecker_P_2147483647_2147483647$1$L0

 

 Boogie program verifier finished with 1 verified, 1 error

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 9f467229..b628df30 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -1,5 +1,7 @@
 function RightOpen(n: int) : [int]bool;

 function RightClosed(n: int) : [int]bool;

+axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);

+axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);

 

 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;