Merge

21 files changed, 430 insertions, 148 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index ca707746..adaf7cf3 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -502,8 +502,8 @@ Global
 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|.NET.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.Build.0 = Release|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.Build.0 = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|x86.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|.NET.ActiveCfg = Debug|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

@@ -520,13 +520,13 @@ Global
 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|.NET.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Any CPU.Build.0 = Release|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.ActiveCfg = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|.NET.ActiveCfg = Release|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Checked|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Checked|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Release|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.Build.0 = Release|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|.NET.ActiveCfg = Debug|x86

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index cb0ca968..a9c41efb 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -355,20 +355,20 @@ namespace Microsoft.Boogie {
       }

     }

 

-    void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g, 

-                                  List<Implementation/*!*/>/*!*/ loopImpls, 

+    void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g,

+                                  List<Implementation/*!*/>/*!*/ loopImpls,

                                   Dictionary<string, Dictionary<string, Block>> fullMap) {

       Contract.Requires(impl != null);

       Contract.Requires(cce.NonNullElements(loopImpls));

-      // Enumerate the headers 

+      // Enumerate the headers

       // for each header h:

-      //   create implementation p_h with 

+      //   create implementation p_h with

       //     inputs = inputs, outputs, and locals of impl

       //     outputs = outputs and locals of impl

       //     locals = empty set

       //   add call o := p_h(i) at the beginning of the header block

       //   break the back edges whose target is h

-      // Enumerate the headers again to create the bodies of p_h 

+      // Enumerate the headers again to create the bodies of p_h

       // for each header h:

       //   compute the loop corresponding to h

       //   make copies of all blocks in the loop for h

@@ -697,7 +697,7 @@ namespace Microsoft.Boogie {
       }

       return g;

     }

-    

+

     public class IrreducibleLoopException : Exception {}

 

     public Graph<Block> ProcessLoops(Implementation impl) {

@@ -1397,7 +1397,7 @@ namespace Microsoft.Boogie {
       : base(tok, typedIdent) {

       Contract.Requires(tok != null);

       Contract.Requires(typedIdent != null);

-      Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);

+      Contract.Requires(typedIdent.Name != null && (!typedIdent.HasName || typedIdent.Name.Length > 0));

       Contract.Requires(typedIdent.WhereExpr == null);

       // base(tok, typedIdent);

       this.Unique = true;

@@ -2378,6 +2378,18 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)

+      : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) {

+      Contract.Requires(structuredStmts != null);

+      Contract.Requires(localVariables != null);

+      Contract.Requires(outParams != null);

+      Contract.Requires(inParams != null);

+      Contract.Requires(typeParams != null);

+      Contract.Requires(name != null);

+      Contract.Requires(tok != null);

+      //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors());

+    }

+

     public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts)

       : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()) {

       Contract.Requires(structuredStmts != null);

@@ -3232,11 +3244,11 @@ namespace Microsoft.Boogie {
       Contract.Requires(varSeq != null);

     }

     /*  PR: the following two constructors cause Spec# crashes

-        public TypeVariableSeq(TypeVariable! var) 

+        public TypeVariableSeq(TypeVariable! var)

           : base(new TypeVariable! [] { var })

         {

         }

-        public TypeVariableSeq() 

+        public TypeVariableSeq()

           : base(new TypeVariable![0])

         {

         } */

@@ -3723,4 +3735,4 @@ namespace Microsoft.Boogie {
       }

     }

   }

-}
\ No newline at end of file
+}

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index b0c7cdb6..ae051b40 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1625,6 +1625,16 @@ namespace Microsoft.Boogie {
   public abstract class CallCommonality : SugaredCmd {

     public QKeyValue Attributes;

 

+    private bool isFree = false;

+    public bool IsFree {

+      get {

+        return isFree;

+      }

+      set {

+        isFree = value;

+      }

+    }

+

     protected CallCommonality(IToken tok, QKeyValue kv)

       : base(tok) {

       Contract.Requires(tok != null);

@@ -1753,7 +1763,11 @@ namespace Microsoft.Boogie {
 

     public override void Emit(TokenTextWriter stream, int level) {

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

-      stream.Write(this, level, "call ");

+      stream.Write(this, level, "");

+      if (IsFree) {

+        stream.Write("free ");

+      }

+      stream.Write("call ");

       EmitAttributes(stream, Attributes);

       string sep = "";

       if (Outs.Count > 0) {

@@ -2029,7 +2043,7 @@ namespace Microsoft.Boogie {
       Expr preConjunction = null;

       for (int i = 0; i < this.Proc.Requires.Length; i++) {

         Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);

-        if (!req.Free) {

+        if (!req.Free && !IsFree) {

           if (hasWildcard) {

             Expr pre = Substituter.Apply(s, req.Condition);

             if (preConjunction == null) {

@@ -2211,7 +2225,11 @@ namespace Microsoft.Boogie {
     }

     public override void Emit(TokenTextWriter stream, int level) {

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

-      stream.Write(this, level, "call ");

+      stream.Write(this, level, "");

+      if (IsFree) {

+        stream.Write("free ");

+      }

+      stream.Write("call ");

       EmitAttributes(stream, Attributes);

       stream.Write("forall ");

       stream.Write(TokenTextWriter.SanitizeIdentifier(callee));

@@ -2355,7 +2373,7 @@ namespace Microsoft.Boogie {
       Expr preConjunction = null;

       for (int i = 0; i < this.Proc.Requires.Length; i++) {

         Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);

-        if (!req.Free) {

+        if (!req.Free && !IsFree) {

           Expr pre = Substituter.Apply(s, req.Condition);

           if (preConjunction == null) {

             preConjunction = pre;

@@ -2957,4 +2975,4 @@ namespace Microsoft.Boogie {
       return visitor.VisitGotoCmd(this);

     }

   }

-}
\ No newline at end of file
+}

diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs
index 55c1648e..30ca85ba 100644
--- a/Source/Core/BitvectorAnalysis.cs
+++ b/Source/Core/BitvectorAnalysis.cs
@@ -95,7 +95,7 @@ namespace Microsoft.Boogie {
 

     private Dictionary<Expr, DisjointSet> exprToDisjointSet = new Dictionary<Expr, DisjointSet>();

     private Dictionary<Variable, DisjointSet> varToDisjointSet = new Dictionary<Variable, DisjointSet>();

-    private DisjointSet uniqueBv32Set = new DisjointSet();

+    private readonly DisjointSet uniqueBv32Set = new DisjointSet();

 

     public int Bits(Expr expr) {

       DisjointSet disjointSet = MakeDisjointSet(expr);

@@ -185,6 +185,10 @@ namespace Microsoft.Boogie {
       program.TopLevelDeclarations.Add(intToBvRewriter.bv32Id);

     }

 

+    public override Axiom VisitAxiom(Axiom node) {

+      return node;

+    }

+

     public override Implementation VisitImplementation(Implementation node) {

       for (int i = 0; i < node.InParams.Length; i++) {

         DisjointSet a = MakeDisjointSet(node.InParams[i]);

@@ -367,27 +371,19 @@ namespace Microsoft.Boogie {
           }

         }

 

-        /*

-          for (int i = 0; i < node.Args.Length; i++) {

-            DisjointSet actual = MakeDisjointSet(node.Args[i]);

-            DisjointSet formal = MakeDisjointSet(func.InParams[i]);

-            actual.Union(formal);

-          }

-          Debug.Assert(func.OutParams.Length == 1);

-          MakeDisjointSet(node).Union(MakeDisjointSet(func.OutParams[0]));

-        */

-

         if (func.Name == "intToBv32") {

-          Debug.Assert(node.Args.Length == 1);

-          Expr e = node.Args[0];

-          DisjointSet actual = MakeDisjointSet(e);

-          actual.Union(uniqueBv32Set);

+          DisjointSet arg0 = MakeDisjointSet(node.Args[0]);

+          arg0.Union(uniqueBv32Set);

         }

 

         if (func.Name == "bv32ToInt") {

-          Debug.Assert(node.Args.Length == 1);

-          DisjointSet actual = MakeDisjointSet(node);

-          actual.Union(uniqueBv32Set);

+          DisjointSet result = MakeDisjointSet(node);

+          result.Union(uniqueBv32Set);

+        }

+

+        if (func.Name == "INT_AND" || func.Name == "INT_OR" || func.Name == "INT_XOR" || func.Name == "INT_NOT") {

+          DisjointSet result = MakeDisjointSet(node);

+          result.Union(uniqueBv32Set);

         }

       }

 

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index b1fbd609..7519fb4c 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -905,7 +905,10 @@ CallCmd<out Cmd/*!*/ c>
      QKeyValue kv = null;

      Expr en;  List<Expr> args;

      c = dummyCmd;

+     bool isFree = false;

   .)

+  [ "free"          (. isFree = true;  .)

+  ]

   "call"                          (. x = t; .)

   { Attribute<ref kv> }

   ( Ident<out first>

@@ -914,7 +917,7 @@ CallCmd<out Cmd/*!*/ c>
         { "," CallForallArg<out en> (. es.Add(en); .)

         }

       ]

-      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); .)

+      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)

     |

                                   (. ids.Add(new IdentifierExpr(first, first.val)); .)

       [ "," CallOutIdent<out p>  (.

@@ -938,7 +941,7 @@ CallCmd<out Cmd/*!*/ c>
         { "," CallForallArg<out en> (. es.Add(en); .)

         }

       ]

-      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); .)

+      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)

     )

   | "forall"

     Ident<out first> "("              (. args = new List<Expr>(); .)

@@ -946,7 +949,7 @@ CallCmd<out Cmd/*!*/ c>
       { "," CallForallArg<out en> (. args.Add(en); .)

       }

     ]

-    ")"                           (. c = new CallForallCmd(x, first.val, args, kv); .)

+    ")"                           (. c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree; .)

   | "*"

                                   (. ids.Add(null); .)

       [ "," CallOutIdent<out p>  (.

@@ -970,7 +973,7 @@ CallCmd<out Cmd/*!*/ c>
         { "," CallForallArg<out en> (. es.Add(en); .)

         }

       ]

-      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); .)

+      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)

   )

   .

 

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 9c208b86..34f43896 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1013,7 +1013,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 			}

 			c = new HavocCmd(x,ids);

 			

-		} else if (la.kind == 48) {

+		} else if (la.kind == 33 || la.kind == 48) {

 			CallCmd(out cn);

 			Expect(7);

 			c = cn; 

@@ -1194,7 +1194,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		QKeyValue kv = null;

 		Expr en;  List<Expr> args;

 		c = dummyCmd;

+		bool isFree = false;

 		

+		if (la.kind == 33) {

+			Get();

+			isFree = true;  

+		}

 		Expect(48);

 		x = t; 

 		while (la.kind == 25) {

@@ -1214,7 +1219,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 					}

 				}

 				Expect(9);

-				c = new CallCmd(x, first.val, es, ids, kv); 

+				c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; 

 			} else if (la.kind == 11 || la.kind == 47) {

 				ids.Add(new IdentifierExpr(first, first.val)); 

 				if (la.kind == 11) {

@@ -1250,7 +1255,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 					}

 				}

 				Expect(9);

-				c = new CallCmd(x, first.val, es, ids, kv); 

+				c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; 

 			} else SynErr(103);

 		} else if (la.kind == 49) {

 			Get();

@@ -1267,7 +1272,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				}

 			}

 			Expect(9);

-			c = new CallForallCmd(x, first.val, args, kv); 

+			c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree; 

 		} else if (la.kind == 42) {

 			Get();

 			ids.Add(null); 

@@ -1304,7 +1309,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				}

 			}

 			Expect(9);

-			c = new CallCmd(x, first.val, es, ids, kv); 

+			c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; 

 		} else SynErr(104);

 	}

 

@@ -2028,8 +2033,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		{x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, T,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, T,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},

 		{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

diff --git a/Source/Dafny.sln b/Source/Dafny.sln
index 9e99e4bc..034dfd7b 100644
--- a/Source/Dafny.sln
+++ b/Source/Dafny.sln
@@ -7,6 +7,9 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyPipeline", "Dafny\Dafn
 EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

+		Checked|.NET = Checked|.NET

+		Checked|Any CPU = Checked|Any CPU

+		Checked|Mixed Platforms = Checked|Mixed Platforms

 		Debug|.NET = Debug|.NET

 		Debug|Any CPU = Debug|Any CPU

 		Debug|Mixed Platforms = Debug|Mixed Platforms

@@ -15,6 +18,12 @@ Global
 		Release|Mixed Platforms = Release|Mixed Platforms

 	EndGlobalSection

 	GlobalSection(ProjectConfigurationPlatforms) = postSolution

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|.NET.ActiveCfg = Checked|Any CPU

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|.NET.Build.0 = Checked|Any CPU

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|Any CPU.ActiveCfg = Debug|Any CPU

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|Any CPU.Build.0 = Debug|Any CPU

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|.NET.ActiveCfg = Debug|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|.NET.Build.0 = Debug|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

@@ -26,6 +35,12 @@ Global
 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Any CPU.Build.0 = Release|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|.NET.ActiveCfg = Checked|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|.NET.Build.0 = Checked|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|Any CPU.ActiveCfg = Debug|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|Any CPU.Build.0 = Debug|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

 		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|.NET.ActiveCfg = Debug|Any CPU

 		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|.NET.Build.0 = Debug|Any CPU

 		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 6a448172..902c1f1c 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -27,7 +27,10 @@ namespace Microsoft.Dafny {
     TextWriter wr;

 

     public int ErrorCount;

-    void Error(string msg, params object[] args) {Contract.Requires(msg != null);

+    void Error(string msg, params object[] args) {

+      Contract.Requires(msg != null);

+      Contract.Requires(args != null);

+

       string s = string.Format("Compilation error: " + msg, args);

       Console.WriteLine(s);

       wr.WriteLine("/* {0} */", s);

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 218f95e5..1a0c97de 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -315,7 +315,7 @@ namespace Microsoft.Dafny {
     public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

-      Contract.Requires(typeArgs != null);

+      Contract.Requires(cce.NonNullElements(typeArgs));

       this.tok = tok;

       this.Name = name;

       this.TypeArgs = typeArgs;

@@ -752,7 +752,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(module != null);

       Contract.Requires(cce.NonNullElements(typeArgs));

       Contract.Requires(cce.NonNullElements(ctors));

-      Contract.Invariant(1 <= ctors.Count);

+      Contract.Requires(1 <= ctors.Count);

       Ctors = ctors;

     }

   }

@@ -871,8 +871,8 @@ namespace Microsoft.Dafny {
     void ObjectInvariant() {

       Contract.Invariant(Expr != null);

       Contract.Invariant(cce.NonNullElements(Toks));

-      Contract.Invariant(cce.NonNullElements(Formals));

-      Contract.Invariant(cce.NonNullElements(Refined));

+      Contract.Invariant(Formals == null || cce.NonNullElements(Formals));

+      Contract.Invariant(Refined == null || cce.NonNullElements(Refined));

     }

 

 

@@ -1298,12 +1298,13 @@ namespace Microsoft.Dafny {
     public Statement TargetStmt;  // filled in during resolution

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(TargetLabel == null || 1 <= BreakCount);

+      Contract.Invariant(TargetLabel != null || 1 <= BreakCount);

     }

 

     public BreakStmt(IToken tok, string targetLabel)

       : base(tok) {

       Contract.Requires(tok != null);

+      Contract.Requires(targetLabel != null);

       this.TargetLabel = targetLabel;

     }

     public BreakStmt(IToken tok, int breakCount)

@@ -1639,13 +1640,11 @@ namespace Microsoft.Dafny {
     public IfStmt(IToken tok, Expression guard, Statement thn, Statement els)

       : base(tok) {

       Contract.Requires(tok != null);

-      Contract.Requires(guard != null);

       Contract.Requires(thn != null);

       Contract.Requires(els == null || els is BlockStmt || els is IfStmt);

       this.Guard = guard;

       this.Thn = thn;

       this.Els = els;

-

     }

   }

 

@@ -1875,9 +1874,15 @@ namespace Microsoft.Dafny {
       Contract.Invariant(tok != null);

     }

 

+    [Pure]

+    public bool WasResolved()

+    {

+      return Type != null;

+    }

+

     public Expression Resolved {

       get {

-        Contract.Requires(type != null);  // should be called only on resolved expressions; this approximates that precondition

+        Contract.Requires(WasResolved());  // should be called only on resolved expressions; this approximates that precondition

         Expression r = this;

         while (true) {

           var rr = r as ConcreteSyntaxExpression;

@@ -1899,7 +1904,7 @@ namespace Microsoft.Dafny {
       [NoDefaultContract]  // no particular validity of 'this' is required, except that it not be committed

       set {

         Contract.Requires(cce.IsValid(this));

-        Contract.Requires(Type == null);  // set it only once

+        Contract.Requires(!WasResolved());  // set it only once

         Contract.Requires(value != null);

         //modifies type;

         type = value.Normalize();

@@ -2907,7 +2912,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(operands != null);

       Contract.Requires(operators != null);

       Contract.Requires(desugaring != null);

-      Contract.Requires(operators.Count == operators.Count + 1);

+      Contract.Requires(operands.Count == operators.Count + 1);

 

       Operands = operands;

       Operators = operators;

diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 6a15b1f7..40a8cacc 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

@@ -75,6 +75,10 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

     <DebugType>pdbonly</DebugType>

@@ -85,6 +89,43 @@
     <WarningLevel>4</WarningLevel>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

   </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>bin\Checked\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>

+    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly />

+    <CodeContractsCustomRewriterClass />

+    <CodeContractsLibPaths />

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsExtraAnalysisOptions />

+    <CodeContractsBaseLineFile />

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

       <SpecificVersion>False</SpecificVersion>

@@ -154,4 +195,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 34fcb740..97324ef9 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -723,7 +723,7 @@ namespace Microsoft.Dafny {
             }

             wr.Write(")");

           }

-          bool parensNeeded = !isLastCase && mc.Body.Resolved is MatchExpr;

+          bool parensNeeded = !isLastCase && mc.Body.WasResolved() && mc.Body.Resolved is MatchExpr;

           if (parensNeeded) {

             wr.WriteLine(" => (");

           } else {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 5e2bc911..b9f5e7e6 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -935,9 +935,9 @@ namespace Microsoft.Dafny {
       Contract.Requires(proxy != null);

       Contract.Requires(t != null);

       Contract.Requires(proxy.T == null);

-      Contract.Requires((t is TypeProxy)|| ((TypeProxy)t).T == null);

+      Contract.Requires(!(t is TypeProxy) || ((TypeProxy)t).T == null);

       //modifies proxy.T, ((TypeProxy)t).T;  // might also change t.T if t is a proxy

-      Contract.Ensures(Contract.Result<bool>() || proxy == t || proxy.T != null || (t is TypeProxy && ((TypeProxy)t).T != null));

+      Contract.Ensures(Contract.Result<bool>() == (proxy == t || proxy.T != null || (t is TypeProxy && ((TypeProxy)t).T != null)));

       if (proxy == t) {

         // they are already in the same equivalence class

         return true;

@@ -1845,7 +1845,7 @@ namespace Microsoft.Dafny {
         Contract.Assume(lhs.Type != null);  // a sanity check that LHSs have already been resolved

       }

       // resolve arguments

-      if (!s.IsGhost) {

+      if (!s.IsGhost && s.Receiver.WasResolved()) {

         CheckIsNonGhost(s.Receiver);

       }

       int j = 0;

@@ -2791,7 +2791,7 @@ namespace Microsoft.Dafny {
     void CheckIsNonGhost(Expression expr) {

       Contract.Requires(expr != null);

       Contract.Requires(currentClass != null);

-      Contract.Requires(expr.Type != null);  // this check approximates the requirement that "expr" be resolved

+      Contract.Requires(expr.WasResolved());  // this check approximates the requirement that "expr" be resolved

 

       if (expr is IdentifierExpr) {

         var e = (IdentifierExpr)expr;

@@ -3505,7 +3505,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(currentClass != null);

       Contract.Ensures(expr.Type != null);

 

-      if (expr is ThisExpr) {

+      if (expr is ThisExpr && !expr.WasResolved()) {

         // Allow 'this' here, regardless of scope.AllowInstance.  The caller is responsible for

         // making sure 'this' does not really get used when it's not available.

         expr.Type = GetThisType(expr.tok, currentClass);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 0c5be389..3ec3c291 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -89,7 +89,7 @@ namespace Microsoft.Dafny {
 

         return new Bpl.TypeSynonymAnnotation(Token.NoToken, multiSetTypeCtor, new Bpl.TypeSeq(ty));

       }

-      

+

       public Bpl.Type SeqType(IToken tok, Bpl.Type ty) {

         Contract.Requires(tok != null);

         Contract.Requires(ty != null);

@@ -1069,9 +1069,11 @@ namespace Microsoft.Dafny {
         stmts = builder.Collect(m.tok);

       }

 

+      QKeyValue kv = etran.TrAttributes(m.Attributes);

+

       Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,

         typeParams, inParams, outParams,

-        localVariables, stmts);

+        localVariables, stmts, kv);

       sink.TopLevelDeclarations.Add(impl);

 

       currentMethod = null;

@@ -2749,10 +2751,9 @@ namespace Microsoft.Dafny {
 

       public override Expr VisitIdentifierExpr(Bpl.IdentifierExpr node)

       {

-        Contract.Requires(node != null);

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

 

-        if (subst.ContainsKey(node.Name))

+        if (node != null && subst.ContainsKey(node.Name))

           return subst[node.Name];

         else

           return base.VisitIdentifierExpr(node);

@@ -3580,7 +3581,7 @@ namespace Microsoft.Dafny {
     void TrAlternatives(List<GuardedAlternative> alternatives, Bpl.Cmd elseCase0, Bpl.StructuredCmd elseCase1,

                         Bpl.StmtListBuilder builder, VariableSeq locals, ExpressionTranslator etran) {

       Contract.Requires(alternatives != null);

-      Contract.Requires((elseCase0 == null) == (elseCase1 == null));  // ugly way of doing a type union

+      Contract.Requires((elseCase0 != null) == (elseCase1 == null));  // ugly way of doing a type union

       Contract.Requires(builder != null);

       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

@@ -3663,7 +3664,7 @@ namespace Microsoft.Dafny {
       Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {

 

       Contract.Requires(tok != null);

-      Contract.Requires((dafnyReceiver == null) != (bReceiver == null));

+      Contract.Requires((dafnyReceiver != null) || (bReceiver != null));

       Contract.Requires(method != null);

       Contract.Requires(cce.NonNullElements(Args));

       Contract.Requires(cce.NonNullElements(Lhss));

@@ -4513,7 +4514,7 @@ namespace Microsoft.Dafny {
       public readonly string This;

       public readonly string modifiesFrame = "$_Frame"; // the name of the context's frame variable.

       readonly Function applyLimited_CurrentFunction;

-      readonly int layerOffset = 0;

+      public readonly int layerOffset = 0;

       public int Statistics_FunctionCount = 0;

       [ContractInvariantMethod]

       void ObjectInvariant()

@@ -4562,7 +4563,6 @@ namespace Microsoft.Dafny {
           Contract.Requires(translator != null);

           Contract.Requires(predef != null);

           Contract.Requires(heap != null);

-          Contract.Requires(applyLimited_CurrentFunction != null);

           this.translator = translator;

           this.predef = predef;

           this.HeapExpr = heap;

@@ -4973,7 +4973,7 @@ namespace Microsoft.Dafny {
               return translator.FunctionCall(expr.tok, BuiltinFunction.SetIntersection, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);

             case BinaryExpr.ResolvedOpcode.SetDifference:

               return translator.FunctionCall(expr.tok, BuiltinFunction.SetDifference, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);

- 

+

             case BinaryExpr.ResolvedOpcode.MultiSetEq:

               return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1);

             case BinaryExpr.ResolvedOpcode.MultiSetNeq:

@@ -5359,7 +5359,7 @@ namespace Microsoft.Dafny {
         return Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType)), Bpl.Expr.Literal(0));

       }

 

-      Bpl.QKeyValue TrAttributes(Attributes attrs) {

+      public Bpl.QKeyValue TrAttributes(Attributes attrs) {

         Bpl.QKeyValue kv = null;

         while (attrs != null) {

           List<object> parms = new List<object>();

@@ -6269,7 +6269,6 @@ namespace Microsoft.Dafny {
 

     static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(expr != null);

-      Contract.Requires(receiverReplacement != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

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

 

@@ -6434,8 +6433,7 @@ namespace Microsoft.Dafny {
     static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,

                                                  Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(cce.NonNullElements(elist));

-      Contract.Requires((receiverReplacement == null) == (substMap == null));

-      Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));

+      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));

 

       List<Expression> newElist = null;  // initialized lazily

diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index cf88eed4..5dac8f59 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

@@ -19,6 +19,8 @@
     </FileUpgradeFlags>

     <OldToolsVersion>3.5</OldToolsVersion>

     <UpgradeBackupLocation />

+    <IsWebBootstrapper>false</IsWebBootstrapper>

+    <TargetFrameworkProfile />

     <PublishUrl>publish\</PublishUrl>

     <Install>true</Install>

     <InstallFrom>Disk</InstallFrom>

@@ -31,10 +33,8 @@
     <MapFileExtensions>true</MapFileExtensions>

     <ApplicationRevision>0</ApplicationRevision>

     <ApplicationVersion>1.0.0.%2a</ApplicationVersion>

-    <IsWebBootstrapper>false</IsWebBootstrapper>

     <UseApplicationTrust>false</UseApplicationTrust>

     <BootstrapperEnabled>true</BootstrapperEnabled>

-    <TargetFrameworkProfile />

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

     <DebugSymbols>true</DebugSymbols>

@@ -72,8 +72,12 @@
     <CodeContractsBaseLineFile>

     </CodeContractsBaseLineFile>

     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

     <DebugType>pdbonly</DebugType>

@@ -84,29 +88,60 @@
     <WarningLevel>4</WarningLevel>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

   </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>..\..\Binaries\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly />

+    <CodeContractsCustomRewriterClass />

+    <CodeContractsLibPaths />

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsExtraAnalysisOptions />

+    <CodeContractsBaseLineFile />

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+  </PropertyGroup>

   <ItemGroup>

-    <Reference Include="AbsInt, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\AbsInt\bin\Debug\AbsInt.dll</HintPath>

+    <Reference Include="AbsInt">

+      <HintPath>..\..\Binaries\AbsInt.dll</HintPath>

     </Reference>

-    <Reference Include="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\AIFramework\bin\debug\AIFramework.dll</HintPath>

+    <Reference Include="AIFramework">

+      <HintPath>..\..\Binaries\AIFramework.dll</HintPath>

     </Reference>

-    <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\Core\bin\Debug\Core.dll</HintPath>

+    <Reference Include="Core">

+      <HintPath>..\..\Binaries\Core.dll</HintPath>

     </Reference>

-    <Reference Include="ParserHelper, Version=0.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+    <Reference Include="ParserHelper, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\Binaries\ParserHelper.dll</HintPath>

     </Reference>

     <Reference Include="System" />

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

-    <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\VCGeneration\bin\debug\VCGeneration.dll</HintPath>

+    <Reference Include="VCGeneration">

+      <HintPath>..\..\Binaries\VCGeneration.dll</HintPath>

     </Reference>

   </ItemGroup>

   <ItemGroup>

@@ -147,4 +182,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 714ecd3b..9646ef85 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -333,7 +333,7 @@ namespace Microsoft.Boogie.Houdini {
       Queue<Implementation> queue = new Queue<Implementation>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Implementation impl = decl as Implementation;

-        if (impl != null) {

+        if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {

           queue.Enqueue(impl);

         }

       }

diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
index b87f68d7..bc7bb8c8 100644
--- a/Source/Houdini/Houdini.csproj
+++ b/Source/Houdini/Houdini.csproj
@@ -12,6 +12,7 @@
     <AssemblyName>Houdini</AssemblyName>

     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

     <DebugSymbols>true</DebugSymbols>

@@ -36,6 +37,34 @@
   <PropertyGroup>

     <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

   </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">

+    <OutputPath>bin\Checked\</OutputPath>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly />

+    <CodeContractsCustomRewriterClass />

+    <CodeContractsLibPaths />

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsExtraAnalysisOptions />

+    <CodeContractsBaseLineFile />

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index 859aade9..91d526d2 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -103,6 +103,7 @@
       this.currentStateView.DrawColumnHeader += new System.Windows.Forms.DrawListViewColumnHeaderEventHandler(this.listView1_DrawColumnHeader);

       this.currentStateView.DrawItem += new System.Windows.Forms.DrawListViewItemEventHandler(this.listView1_DrawItem);

       this.currentStateView.SelectedIndexChanged += new System.EventHandler(this.currentStateView_SelectedIndexChanged);

+      this.currentStateView.KeyDown += new System.Windows.Forms.KeyEventHandler(this.currentStateView_KeyDown);

       this.currentStateView.MouseUp += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseUp);

       this.currentStateView.Resize += new System.EventHandler(this.listView1_Resize);

       // 

@@ -175,9 +176,9 @@
       // 

       // matchesList

       // 

-      this.matchesList.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)

-                  | System.Windows.Forms.AnchorStyles.Left)

-                  | System.Windows.Forms.AnchorStyles.Right)));

+      this.matchesList.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom) 

+            | System.Windows.Forms.AnchorStyles.Left) 

+            | System.Windows.Forms.AnchorStyles.Right)));

       this.matchesList.Columns.AddRange(new System.Windows.Forms.ColumnHeader[] {

             this.columnHeader4,

             this.columnHeader5});

@@ -233,9 +234,9 @@
       // 

       // textBox1

       // 

-      this.textBox1.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)

-                  | System.Windows.Forms.AnchorStyles.Left)

-                  | System.Windows.Forms.AnchorStyles.Right)));

+      this.textBox1.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom) 

+            | System.Windows.Forms.AnchorStyles.Left) 

+            | System.Windows.Forms.AnchorStyles.Right)));

       this.textBox1.Location = new System.Drawing.Point(53, 3);

       this.textBox1.Name = "textBox1";

       this.textBox1.Size = new System.Drawing.Size(477, 20);

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index afe0593c..1d55fc13 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -45,8 +45,7 @@ namespace Microsoft.Boogie.ModelViewer
 

       smallFont = stateList.Font;

 

-      if (runAsHostedWindow)

-      {

+      if (runAsHostedWindow) {

         this.fileToolStripMenuItem.Enabled = false;

         this.fileToolStripMenuItem.Visible = false;

       }

@@ -73,11 +72,9 @@ namespace Microsoft.Boogie.ModelViewer
         System.Diagnostics.Debugger.Launch();

       }

 

-      if (filename != null)

-      {

+      if (filename != null) {

         var idx = filename.IndexOf(':');

-        if (idx > 0)

-        {

+        if (idx > 0) {

           modelId = int.Parse(filename.Substring(idx + 1));

           filename = filename.Substring(0, idx);

         }

@@ -88,12 +85,9 @@ namespace Microsoft.Boogie.ModelViewer
 

     private void SetWindowTitle(string fileName)

     {

-      if (fileName == null)

-      {

+      if (fileName == null) {

         this.Text = "Boogie Verification Debugger";

-      }

-      else

-      {

+      } else {

         this.Text = Path.GetFileName(fileName) + " - Boogie Verification Debugger";

       }

     }

@@ -103,10 +97,8 @@ namespace Microsoft.Boogie.ModelViewer
       this.lastModelFileName = modelFileName;

       this.langProvider = Base.Provider.Instance;

 

-      if (!string.IsNullOrWhiteSpace(modelFileName) && File.Exists(modelFileName))

-      {

-        using (var rd = File.OpenText(modelFileName))

-        {

+      if (!string.IsNullOrWhiteSpace(modelFileName) && File.Exists(modelFileName)) {

+        using (var rd = File.OpenText(modelFileName)) {

           allModels = Model.ParseModels(rd).ToArray();

         }

 

@@ -118,19 +110,15 @@ namespace Microsoft.Boogie.ModelViewer
         currentModel = allModels[modelId];

         AddModelMenu();

 

-        foreach (var p in Providers())

-        {

-          if (p.IsMyModel(currentModel))

-          {

+        foreach (var p in Providers()) {

+          if (p.IsMyModel(currentModel)) {

             this.langProvider = p;

             break;

           }

         }

 

         LoadModel(modelId);

-      }

-      else

-      {

+      } else {

         currentModel = new Model();

       }

 

@@ -141,7 +129,7 @@ namespace Microsoft.Boogie.ModelViewer
     private void LoadModel(int idx)

     {

       var i = 0;

-      

+

       //var stateIdx = stateList.SelectedIndices.Count == 0 ? 0 : stateList.SelectedIndices[0];

 

       modelId = idx;

@@ -165,8 +153,7 @@ namespace Microsoft.Boogie.ModelViewer
       foreach (var m in allModels) {

         var currIdx = idx++; // this local needs to be in this block

         var menuItem = modelsToolStripMenuItem.DropDownItems.Add(string.Format("Model #&{0}", currIdx), null, (s, a) => LoadModel(currIdx)) as ToolStripMenuItem;

-        if (currIdx <= 9)

-        {

+        if (currIdx <= 9) {

           menuItem.ShortcutKeys = Keys.Control | (Keys)(currIdx + Keys.D0);

         }

       }

@@ -202,10 +189,10 @@ namespace Microsoft.Boogie.ModelViewer
         stateList.Items[0].Selected = true;

         SetColumnSizes();

       } else {

-        var mapping = new Dictionary<SkeletonItem, SkeletonItem>();        

+        var mapping = new Dictionary<SkeletonItem, SkeletonItem>();

         unfoldingRoot.SyncWith(mapping, oldRoot);

         SkeletonItem newIt = null;

-        while (selectedSkel != null) {          

+        while (selectedSkel != null) {

           if (mapping.TryGetValue(selectedSkel, out newIt)) break;

           selectedSkel = selectedSkel.parent;

         }

@@ -303,7 +290,7 @@ namespace Microsoft.Boogie.ModelViewer
         plusBorder.Height = lineHeight / 2;

         plusBorder.Width = lineHeight / 2;

         plusBorder.X += lineHeight / 4;

-        plusBorder.Y += lineHeight / 4;   

+        plusBorder.Y += lineHeight / 4;

         e.Graphics.DrawRectangle(plusPen, plusBorder);

         if (skel.Expandable) {

           float midX = plusBorder.X + plusBorder.Width / 2;

@@ -493,7 +480,7 @@ namespace Microsoft.Boogie.ModelViewer
       }

 

       textBox1.ForeColor = bad ? Color.Red : Color.Black;

-      

+

       var wordsA = words.ToArray();

       var refsA = eltRef.ToArray();

 

@@ -515,7 +502,7 @@ namespace Microsoft.Boogie.ModelViewer
           s.isMatch = newMatch;

         }

       }

-      

+

       if (previousState >= 0)

         stateList.Items[previousState].ForeColor = previousStateBrush.Color;

       stateList.Items[currentState].ForeColor = currentStateBrush.Color;

@@ -534,7 +521,7 @@ namespace Microsoft.Boogie.ModelViewer
     private void matchesList_DoubleClick(object sender, EventArgs e)

     {

       if (matchesList.SelectedItems.Count == 0) return;

-      var sel = (DisplayItem) matchesList.SelectedItems[0];

+      var sel = (DisplayItem)matchesList.SelectedItems[0];

       GotoNode(sel.skel);

     }

 

@@ -687,8 +674,7 @@ namespace Microsoft.Boogie.ModelViewer
 

     private void openModelMenuItem_Click(object sender, EventArgs e)

     {

-      if (this.openModelFileDialog.ShowDialog() == System.Windows.Forms.DialogResult.OK)

-      {

+      if (this.openModelFileDialog.ShowDialog() == System.Windows.Forms.DialogResult.OK) {

         this.ReadModels(this.openModelFileDialog.FileName, 0);

       }

     }

@@ -710,8 +696,42 @@ namespace Microsoft.Boogie.ModelViewer
       //label1.Font = font;

     }

 

-    private void Main_Load(object sender, EventArgs e) {

+    private void Main_Load(object sender, EventArgs e)

+    {

+

+    }

+

+    private void currentStateView_KeyDown(object sender, KeyEventArgs e)

+    {

+      var node = SelectedNode();

+      if (node == null) return;

+

+      if (e.KeyCode == Keys.Right && !node.skel.Expanded && node.skel.Expandable) {

+        node.skel.Expanded = true;

+        SyncCurrentStateView();

+        return;

+      }

 

+      if (e.KeyCode == Keys.Left) {

+        if (node.skel.Expanded) {

+          node.skel.Expanded = false;

+          SyncCurrentStateView();

+          return;

+        } else {

+          var par = node.skel.parent;

+          if (par != null && par.parent != null) {

+            // par.Expanded = false;

+            foreach (DisplayItem it in currentStateView.Items) {

+              it.Selected = it.skel == par;

+              it.Focused = it.skel == par;

+              if (it.Selected) {

+                it.EnsureVisible();

+              }

+            }

+            SyncCurrentStateView();

+          }

+        }

+      }

     }

   }

 

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index a11199f6..165c8ac9 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -38,7 +38,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
                                f_select_value, f_field, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t, f_select_ptr,

                                f_owners, f_closed, f_roots, f_timestamps, f_select_bool, f_select_int, f_is_null, f_good_state,

                                f_int_to_version, f_int_to_ptrset, f_set_in0, f_is_ghost_field, f_is_phys_field, f_idx, f_field_plus,

-                               f_is_sequential_field, f_is_volatile_field, f_type_project_0, f_array;

+                               f_is_sequential_field, f_is_volatile_field, f_type_project_0, f_array, f_active_option, f_int_to_field;

     public readonly Model.Element tp_object, tp_mathint, tp_bool, tp_state, tp_ptrset, tp_heaptp;

     public readonly Model.Element elt_me, elt_null;

     Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();

@@ -69,6 +69,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_closed = m.MkFunc("$f_closed", 1);

       f_roots = m.MkFunc("$roots", 1);

       f_timestamps = m.MkFunc("$f_timestamp", 1);

+      f_active_option = m.MkFunc("$f_active_option", 1);

       f_field = m.MkFunc("$field", 1);

       f_field_type = m.MkFunc("$field_type", 1);

       f_int_to_ptr = m.MkFunc("$int_to_ptr", 1);

@@ -79,6 +80,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_good_state = m.MkFunc("$good_state", 1);

       f_int_to_version = m.MkFunc("$int_to_version", 1);

       f_int_to_ptrset = m.MkFunc("$int_to_ptrset", 1);

+      f_int_to_field = m.MkFunc("$int_to_field", 1);

       f_set_in0 = m.MkFunc("$set_in0", 2);

       f_is_ghost_field = m.MkFunc("$is_ghost_field", 1);

       f_is_phys_field = m.MkFunc("$is_phys_field", 1);

@@ -518,7 +520,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return res;

     }

 

-    public static readonly string[] synthethic_fields = new string[] { "$f_owns", "$f_ref_cnt", "$f_vol_version", "$f_root", "$f_group_root" };

+    public static readonly string[] synthethic_fields = new string[] { "$f_owns", "$f_ref_cnt", "$f_vol_version", "$f_root", "$f_group_root", "$f_active_option" };

 

     public string ConstantFieldName(Model.Element elt)

     {

@@ -613,18 +615,47 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           else if (tpl.Args[1] == element)

             return tp_object;

 

-        if (tpl.Args.Length == 2 && tpl.Args[0] == element && tpl.Func.Name.StartsWith("$select.$map_t")) {

+        var fname = tpl.Func.Name;

+

+        if (tpl.Args.Length == 2 && tpl.Args[0] == element && fname.StartsWith("$select.$map_t")) {

+          var mt = model.TryGetFunc("MT#" + fname);

+          if (mt != null && mt.Arity == 0)

+            return mt.GetConstant();

           var t1 = GuessType(tpl.Args[1]);

           var t2 = GuessType(tpl.Result);

           var t = f_map_t.TryEval(t1, t2);

           if (t != null)

             return t;

         }

+

+        var tpName = DataTypeName(element, tpl);

+        if (tpName != null) {

+          var tp = model.TryGetFunc("^$#" + tpName);

+          if (tp != null)

+            return tp.GetConstant();

+        }

       }

 

       return tp_mathint;

     }

 

+    string DataTypeName(Model.Element elt, Model.FuncTuple tpl)

+    {

+      var fname = tpl.Func.Name;

+      if (tpl.Args.Length == 1 && tpl.Args[0] == elt && fname.StartsWith("RF#")) {

+        var fldName = tpl.Func.Name.Substring(3);

+        var idx = fldName.LastIndexOf('.');

+        if (idx > 0) {

+          return fldName.Substring(0, idx);

+        }

+      }

+

+      if (tpl.Args.Length == 1 && tpl.Args[0] == elt && (fname.StartsWith("DSZ#") || fname.StartsWith("RSZ#") || fname.StartsWith("DGH#"))) {

+        return fname.Substring(4);

+      }

+      return null;

+    }

+

     public DataKind GetKind(Model.Element tp, out Model.FuncTuple tpl)

     {

       tpl = null;

@@ -656,7 +687,18 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       Model.FuncTuple tpl;

       var kind = GetKind(tp, out tpl);

 

-      if (kind == DataKind.Flat) return elt;

+      if (kind == DataKind.Flat) {

+        if (elt.Kind == Model.ElementKind.Integer) {

+          var tpname = TypeName(tp);

+          if(tpname.StartsWith("$")) tpname = tpname.Substring(1);

+          foreach (var tupl in elt.References) {

+            if (tupl.Args.Length == 1 && tupl.Args[0] == elt && tupl.Func.Name.StartsWith("$int_to_") && tupl.Func.Name.EndsWith(tpname)) {

+              return tupl.Result;

+            }

+          }

+        }

+        return elt;

+      }

 

       if (kind == DataKind.Map) {

         if (elt.Kind == Model.ElementKind.Integer) {

@@ -847,7 +889,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
                 continue;              

               var addr = f_ptr.TryEval(field, elt);

               if (addr != null) addresses.Add(addr);

-              BuildFieldNode(result, state, addr, field, val, addr);

+              var node = ComputeUnionActiveOption(state, elt, val, field);

+              if (node != null)

+                result.Add(node);

+              else

+                BuildFieldNode(result, state, addr, field, val, addr);

             }

           }

           //result.Sort(CompareFields);

@@ -913,6 +959,26 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           var edgname = new EdgeName(this, "[%0]", sel.Args[1]);

           result.Add(new MapletNode(state, edgname, sel.Result, tp_bool) { Category = NodeCategory.Maplet });

         }

+      } else if (kind == DataKind.Flat) {

+        foreach (var tupl in elt.References) {

+          if (tupl.Args.Length == 1 && tupl.Args[0] == elt) {

+            var fname = tupl.Func.Name;

+            var idx = fname.LastIndexOf('.');

+            if (fname.StartsWith("RF#") && idx > 0) {

+              fname = fname.Substring(idx + 1);

+            } else if (fname.StartsWith("DP#p")) {

+              fname = fname.Substring(4);

+              idx = fname.IndexOf('#');

+              if (idx > 0)

+                fname = fname.Substring(idx + 1) + "#" + fname.Substring(0, idx);

+            } else {

+              fname = null;

+            }

+

+            if (fname != null)

+              result.Add(new FieldNode(state, new EdgeName(fname), tupl.Result, GuessType(tupl.Result)) { Category = NodeCategory.SpecField });

+          }

+        }

       }

 

       if (elt != null && !(elt is Model.Boolean)) {

@@ -938,6 +1004,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
             cat = NodeCategory.UserFunction;

           }

 

+          if (name.StartsWith("DF#")) {

+            name = name.Substring(3);

+            cat = NodeCategory.UserFunction;

+          }

+

           if (name.StartsWith("$eq.$"))

             name = "EQ";

 

@@ -974,6 +1045,19 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return result;

     }

 

+    private FieldNode ComputeUnionActiveOption(StateNode state, Model.Element elt, Model.Element val, Model.Element field)

+    {

+      if (f_active_option.AppsWithResult(field).FirstOrDefault() != null) {

+        var activeOpt = f_ptr.OptEval(f_int_to_field.OptEval(val), elt);

+        if (activeOpt != null) {

+          var nm = ConstantFieldName(field);

+          var fieldNode = new FieldNode(state, new EdgeName(nm), activeOpt, GuessType(activeOpt)) { Category = NodeCategory.MethodologyProperty };

+          return fieldNode;

+        }

+      }

+      return null;

+    }

+

     private void AddCasts(StateNode state, Model.Element elt, List<ElementNode> result)

     {

       foreach (var app in f_phys_ptr_cast.AppsWithArg(0, elt)) {

@@ -1050,8 +1134,24 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
           if (fn == f_int_to_version)

             return "version";

 

-        if (fn == f_is_null && tpl.Result == model.True) 

+        if (fn == f_is_null && tpl.Result == model.True)

           isNull = true;

+

+        var dtpName = DataTypeName(elt, tpl);

+        if (dtpName != null) {

+          var dgh = model.TryGetFunc("DGH#" + dtpName);

+          if (dgh != null) {

+            var hd = dgh.TryEval(elt);

+            if (hd != null) {

+              foreach (var nm in hd.References) {

+                if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))

+                  return nm.Func.Name.Substring(3);

+              }

+

+            }

+          }

+          return dtpName;

+        }

       }

 

       var fld = vm.f_field.TryEval(elt);

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index c907bd9f..58c6ad7a 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -206,6 +206,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

     public static string MakeIdPrintable(string s) {

       Contract.Requires(s != null);

+      Contract.Requires(s != "");

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

       // make sure that no keywords are used as identifiers

       switch (s) {

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 000126de..a52a7087 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1533,7 +1533,7 @@ namespace VC {
       new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true),

                       new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true)),

       new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false));

-    public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int));

+    public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "@MV_state_const", Bpl.Type.Int));

 

     public ModelViewInfo(Program program, Implementation impl) {

       Contract.Requires(program != null);