From 4fc18b2fe45c9a29cb0b8fe93d3102cec9c83194 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 12 Oct 2010 00:13:50 +0000
Subject: Boogie: * enhanced the printing of captured states * addressed some
 warnings issued by VS 2010 * some code formatting

---
 .../Polyhedra/LinearConstraintSystem.cs            |   3 +-
 Source/AIFramework/Polyhedra/SimplexTableau.cs     |   1 -
 Source/Basetypes/BigNum.cs                         |   1 -
 Source/Core/Absy.cs                                |   7 +-
 Source/Provers/Simplify/ProverInterface.cs         |   4 +
 Source/Provers/Z3/Prover.cs                        |   7 -
 Source/Provers/Z3/ProverInterface.cs               |   4 +
 Source/VCExpr/Boogie2VCExpr.cs                     |  22 ++
 Source/VCExpr/TypeErasure.cs                       |  21 +-
 Source/VCExpr/TypeErasurePremisses.cs              | 382 +++++++++++----------
 Source/VCExpr/VCExprAST.cs                         |   9 +-
 Source/VCGeneration/ConditionGeneration.cs         | 118 +++++--
 Source/VCGeneration/Context.cs                     |   7 +-
 Source/VCGeneration/VC.cs                          |  27 +-
 14 files changed, 376 insertions(+), 237 deletions(-)

(limited to 'Source')

diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
index c259febe..b6ce193a 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
+++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
@@ -156,7 +156,6 @@ namespace Microsoft.AbstractInterpretationFramework {
       FrameVertices = null;
       FrameRays = null;
       FrameLines = null;
-      IMutableSet ss;
       FrameDimensions.Clear();  // no implicit lines
     }
 
@@ -672,7 +671,7 @@ namespace Microsoft.AbstractInterpretationFramework {
       CHECK_NEXT_CONSTRAINT: {
         }
 #if DEBUG_PRINT
-        Console.WriteLine("Widen checking: done with that constraint");
+        Console.WriteLine("Widen checking: done with that constraint");
 #endif
       }
 
diff --git a/Source/AIFramework/Polyhedra/SimplexTableau.cs b/Source/AIFramework/Polyhedra/SimplexTableau.cs
index 4b5eaf43..4c37e980 100644
--- a/Source/AIFramework/Polyhedra/SimplexTableau.cs
+++ b/Source/AIFramework/Polyhedra/SimplexTableau.cs
@@ -364,7 +364,6 @@ namespace Microsoft.AbstractInterpretationFramework {
         START_ANEW:
           ;
         }
-        return false; // make compiler shut up
       }
     }
 
diff --git a/Source/Basetypes/BigNum.cs b/Source/Basetypes/BigNum.cs
index f5299f47..2e56fd1a 100644
--- a/Source/Basetypes/BigNum.cs
+++ b/Source/Basetypes/BigNum.cs
@@ -277,7 +277,6 @@ namespace Microsoft.Basetypes {
           }
         }
       }
-      return ZERO; // make compiler shut up
     }
 
     ////////////////////////////////////////////////////////////////////////////
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 398382a8..39f69ccc 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -3611,11 +3611,8 @@ namespace Microsoft.Boogie {
           return new Sequential(new AtomicRE(b), second);
         }
       } else {
-        {
-          Contract.Assume(false);
-          throw new cce.UnreachableException();
-        }
-        return new AtomicRE(b);
+        Contract.Assume(false);
+        throw new cce.UnreachableException();
       }
     }
   }
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 1f563c0f..1d7bdbb3 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -757,6 +757,10 @@ namespace Microsoft.Boogie.Simplify {
       //Contract.Requires(var != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
+      VCExprVar v = AxBuilder.TryTyped2Untyped(var);
+      if (v != null) {
+        var = v;
+      }
       return Namer.Lookup(var);
     }
 
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 4a16e6b6..33e622ba 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -597,13 +597,6 @@ namespace Microsoft.Boogie.Z3
           int k = s.IndexOfAny(new char[] { ' ', '}' }, j);
           Contract.Assume(j <= k);
           string id = s.Substring(j, k - j);
-#if IS_THIS_A_GOOD_IDEA
-          // remove any @@-suffix
-          int doubleAt = id.IndexOf("@@");
-          if (doubleAt != -1) {
-            id = id.Substring(0, doubleAt);
-          }
-#endif
           j = k + 1;
           Contract.Assume(!identifierToPartition.ContainsKey(id));  // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
           identifierToPartition.Add(id, zID);
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 9289b5b7..af9668d4 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -295,6 +295,10 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
       //Contract.Requires(var != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
+      VCExprVar v = AxBuilder.TryTyped2Untyped(var);
+      if (v != null) {
+        var = v;
+      }
       return Namer.Lookup(var);
     }
     
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index b90196e2..64239e42 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -277,6 +277,28 @@ namespace Microsoft.Boogie.VCExprAST {
       return cce.NonNull(res);
     }
 
+    /// <summary>
+    /// Unlike LookupVariable, this method does not create a new variable mapping if none is
+    /// found.  Instead, this method returns null in such cases.  Also, this method does not
+    /// look for bound variables.
+    /// </summary>
+    /// <param name="boogieVar"></param>
+    /// <returns></returns>
+    public VCExprVar TryLookupVariable(Variable boogieVar) {
+      Contract.Requires(boogieVar != null);
+
+      VCExprVar res;
+      Formal fml = boogieVar as Formal;
+      if (fml != null && Formals.TryGetValue(fml, out res))
+        return cce.NonNull(res);
+
+      if (UnboundVariables.TryGetValue(boogieVar, out res)) {
+        return cce.NonNull(res);
+      }
+
+      return null;  // not present
+    }
+
     ///////////////////////////////////////////////////////////////////////////////////
 
     internal readonly VCGenerationOptions/*!*/ GenerationOptions;
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index a33ea631..20c946e5 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -424,8 +424,8 @@ namespace Microsoft.Boogie.TypeErasure {
     public VCExprVar Typed2Untyped(VCExprVar var) {
       Contract.Requires(var != null);
       Contract.Ensures(Contract.Result<VCExprVar>() != null);
-      VCExprVar res;
-      if (!Typed2UntypedVariables.TryGetValue(var, out res)) {
+      VCExprVar res = TryTyped2Untyped(var);
+      if (res == null) {
         res = Gen.Variable(var.Name, TypeAfterErasure(var.Type));
         Typed2UntypedVariables.Add(var, res);
         AddVarTypeAxiom(res, var.Type);
@@ -433,6 +433,23 @@ namespace Microsoft.Boogie.TypeErasure {
       return cce.NonNull(res);
     }
 
+    /// <summary>
+    ///  This method is like Typed2Untyped, except in the case where the given variables
+    ///  doesn't exist in the mapping.  For that case, this method returns null whereas
+    ///  Typed2Untyped creates a new variable that it adds to the mapping.
+    /// </summary>
+    /// <param name="var"></param>
+    /// <returns></returns>
+    public VCExprVar TryTyped2Untyped(VCExprVar var) {
+      Contract.Requires(var != null);
+      VCExprVar res;
+      if (Typed2UntypedVariables.TryGetValue(var, out res)) {
+        return res;
+      } else {
+        return null;
+      }
+    }
+
     protected abstract void AddVarTypeAxiom(VCExprVar/*!*/ var, Type/*!*/ originalType);
 
     ///////////////////////////////////////////////////////////////////////////
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index 09794803..25aa8074 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -31,19 +31,19 @@ namespace Microsoft.Boogie.TypeErasure
   // type parameters (in the same order as they occur in the signature
   // of the original function).
 
-  internal struct UntypedFunction {
+  internal struct UntypedFunction
+  {
     public readonly Function/*!*/ Fun;
     // type parameters that can be extracted from the value parameters
     public readonly List<TypeVariable/*!*/>/*!*/ ImplicitTypeParams;
     // type parameters that have to be given explicitly
     public readonly List<TypeVariable/*!*/>/*!*/ ExplicitTypeParams;
     [ContractInvariantMethod]
-void ObjectInvariant() 
-{
-    Contract.Invariant(Fun != null);
+    void ObjectInvariant() {
+      Contract.Invariant(Fun != null);
       Contract.Invariant(cce.NonNullElements(ImplicitTypeParams));
       Contract.Invariant(cce.NonNullElements(ExplicitTypeParams));
-}
+    }
 
 
     public UntypedFunction(Function/*!*/ fun,
@@ -58,7 +58,8 @@ void ObjectInvariant()
     }
   }
 
-  public class TypeAxiomBuilderPremisses : TypeAxiomBuilderIntBoolU {
+  public class TypeAxiomBuilderPremisses : TypeAxiomBuilderIntBoolU
+  {
 
     public TypeAxiomBuilderPremisses(VCExpressionGenerator gen)
       : base(gen) {
@@ -132,17 +133,23 @@ void ObjectInvariant()
 
     private MapTypeAbstractionBuilderPremisses MapTypeAbstracterAttr;
 
-    internal override MapTypeAbstractionBuilder/*!*/ MapTypeAbstracter { get {Contract.Ensures(Contract.Result<MapTypeAbstractionBuilder>() != null);
+    internal override MapTypeAbstractionBuilder/*!*/ MapTypeAbstracter {
+      get {
+        Contract.Ensures(Contract.Result<MapTypeAbstractionBuilder>() != null);
 
-      if (MapTypeAbstracterAttr == null)
-        MapTypeAbstracterAttr = new MapTypeAbstractionBuilderPremisses (this, Gen);
-      return MapTypeAbstracterAttr;
-    } }
+        if (MapTypeAbstracterAttr == null)
+          MapTypeAbstracterAttr = new MapTypeAbstractionBuilderPremisses(this, Gen);
+        return MapTypeAbstracterAttr;
+      }
+    }
 
-    internal MapTypeAbstractionBuilderPremisses/*!*/ MapTypeAbstracterPremisses { get {Contract.Ensures(Contract.Result<MapTypeAbstractionBuilderPremisses>() != null);
+    internal MapTypeAbstractionBuilderPremisses/*!*/ MapTypeAbstracterPremisses {
+      get {
+        Contract.Ensures(Contract.Result<MapTypeAbstractionBuilderPremisses>() != null);
 
-      return (MapTypeAbstractionBuilderPremisses)MapTypeAbstracter;
-    } }
+        return (MapTypeAbstractionBuilderPremisses)MapTypeAbstracter;
+      }
+    }
 
     ////////////////////////////////////////////////////////////////////////////
 
@@ -150,15 +157,14 @@ void ObjectInvariant()
     // the field is overwritten with its actual value in "Setup"
     private Function/*!*/ TypeFunction;
     [ContractInvariantMethod]
-void ObjectInvariant() 
-{
-    Contract.Invariant(TypeFunction != null);
-}
+    void ObjectInvariant() {
+      Contract.Invariant(TypeFunction != null);
+    }
 
 
-    public VCExpr TypeOf(VCExpr expr){
-Contract.Requires(expr != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+    public VCExpr TypeOf(VCExpr expr) {
+      Contract.Requires(expr != null);
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
       return Gen.Function(TypeFunction, expr);
     }
 
@@ -169,26 +175,28 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
     public List<VCExprLetBinding/*!*/>/*!*/
            GenTypeParamBindings(// the original bound variables and (implicit) type parameters
                                 List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ oldBoundVars,
-                                // VariableBindings to which the translation
-                                // TypeVariable -> VCExprVar is added
+      // VariableBindings to which the translation
+      // TypeVariable -> VCExprVar is added
                                 VariableBindings/*!*/ bindings,
                                 bool addTypeVarsToBindings) {
       Contract.Requires(typeParams != null);
       Contract.Requires(cce.NonNullElements(oldBoundVars));
       Contract.Requires(bindings != null);
 
-    Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()));
+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()));
 
       // type variables are replaced with ordinary variables that are bound using a
       // let-expression
       if (addTypeVarsToBindings) {
-        foreach (TypeVariable/*!*/ tvar in typeParams){Contract.Assert(tvar != null);
-          bindings.TypeVariableBindings.Add(tvar, Gen.Variable(tvar.Name, T));}
+        foreach (TypeVariable/*!*/ tvar in typeParams) {
+          Contract.Assert(tvar != null);
+          bindings.TypeVariableBindings.Add(tvar, Gen.Variable(tvar.Name, T));
+        }
       }
 
       // extract the values of type variables from the term variables
-      List<VCExprVar/*!*/>/*!*/ UtypedVars = new List<VCExprVar/*!*/> (oldBoundVars.Count);
-      List<Type/*!*/>/*!*/ originalTypes = new List<Type/*!*/> (oldBoundVars.Count);
+      List<VCExprVar/*!*/>/*!*/ UtypedVars = new List<VCExprVar/*!*/>(oldBoundVars.Count);
+      List<Type/*!*/>/*!*/ originalTypes = new List<Type/*!*/>(oldBoundVars.Count);
       foreach (VCExprVar var in oldBoundVars) {
         VCExprVar/*!*/ newVar = bindings.VCExprVarBindings[var];
         if (newVar.Type.Equals(U)) {
@@ -196,7 +204,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
           originalTypes.Add(var.Type);
         }
       }
-      
+
       UtypedVars.TrimExcess();
       originalTypes.TrimExcess();
 
@@ -206,7 +214,8 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
 
     public VCExpr/*!*/ AddTypePremisses(List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings,
                                     VCExpr/*!*/ typePremisses, bool universal,
-                                    VCExpr/*!*/ body) {Contract.Requires(cce.NonNullElements(typeVarBindings));
+                                    VCExpr/*!*/ body) {
+      Contract.Requires(cce.NonNullElements(typeVarBindings));
       Contract.Requires(typePremisses != null);
       Contract.Requires(body != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -217,7 +226,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
       else
         bodyWithPremisses = Gen.AndSimp(typePremisses, body);
 
-      return Gen.Let(typeVarBindings, bodyWithPremisses);      
+      return Gen.Let(typeVarBindings, bodyWithPremisses);
     }
 
 
@@ -236,7 +245,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
       Contract.Requires(bindings != null);
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()));
 
-      List<VCExprLetBinding/*!*/>/*!*/ typeParamBindings = new List<VCExprLetBinding/*!*/> ();
+      List<VCExprLetBinding/*!*/>/*!*/ typeParamBindings = new List<VCExprLetBinding/*!*/>();
       foreach (TypeVariable/*!*/ var in vars) {
         Contract.Assert(var != null);
         VCExpr extractor = BestTypeVarExtractor(var, types, concreteTypeSources);
@@ -249,7 +258,8 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
     }
 
     private VCExpr BestTypeVarExtractor(TypeVariable/*!*/ var, List<Type/*!*/>/*!*/ types,
-                                        List<VCExprVar/*!*/>/*!*/ concreteTypeSources) {Contract.Requires(var != null);
+                                        List<VCExprVar/*!*/>/*!*/ concreteTypeSources) {
+      Contract.Requires(var != null);
       Contract.Requires(cce.NonNullElements(types));
       Contract.Requires(cce.NonNullElements(concreteTypeSources));
       List<VCExpr/*!*/> allExtractors = TypeVarExtractors(var, types, concreteTypeSources);
@@ -271,13 +281,12 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
     }
 
     private List<VCExpr/*!*/>/*!*/ TypeVarExtractors(TypeVariable/*!*/ var, List<Type/*!*/>/*!*/ types,
-                                             List<VCExprVar/*!*/>/*!*/ concreteTypeSources)
-      {
+                                             List<VCExprVar/*!*/>/*!*/ concreteTypeSources) {
       Contract.Requires(var != null);
       Contract.Requires(cce.NonNullElements(types));
       Contract.Requires(cce.NonNullElements(concreteTypeSources));
       Contract.Requires((types.Count == concreteTypeSources.Count));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
       List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();
       for (int i = 0; i < types.Count; ++i)
         TypeVarExtractors(var, types[i], TypeOf(concreteTypeSources[i]), res);
@@ -285,11 +294,11 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
       return res;
     }
 
-    private void TypeVarExtractors(TypeVariable var, Type completeType, VCExpr innerTerm, List<VCExpr/*!*/>/*!*/ extractors){
-Contract.Requires(innerTerm != null);
-Contract.Requires(completeType != null);
-Contract.Requires(var != null);
-Contract.Requires(cce.NonNullElements(extractors));
+    private void TypeVarExtractors(TypeVariable var, Type completeType, VCExpr innerTerm, List<VCExpr/*!*/>/*!*/ extractors) {
+      Contract.Requires(innerTerm != null);
+      Contract.Requires(completeType != null);
+      Contract.Requires(var != null);
+      Contract.Requires(cce.NonNullElements(extractors));
       if (completeType.IsVariable) {
         if (var.Equals(completeType)) {
           extractors.Add(innerTerm);
@@ -320,37 +329,40 @@ Contract.Requires(cce.NonNullElements(extractors));
     // Symbols for representing functions
 
     // Globally defined functions
-    private readonly IDictionary<Function/*!*/, UntypedFunction/*!*/>/*!*/ Typed2UntypedFunctions; 
+    private readonly IDictionary<Function/*!*/, UntypedFunction/*!*/>/*!*/ Typed2UntypedFunctions;
     [ContractInvariantMethod]
-void Typed2UntypedFunctionsInvariantMethod(){
-Contract.Invariant(cce.NonNullElements(Typed2UntypedFunctions));} 
+    void Typed2UntypedFunctionsInvariantMethod() {
+      Contract.Invariant(cce.NonNullElements(Typed2UntypedFunctions));
+    }
 
     // distinguish between implicit and explicit type parameters
     internal static void SeparateTypeParams(List<Type/*!*/>/*!*/ valueArgumentTypes,
                                             TypeVariableSeq/*!*/ allTypeParams,
                                             out List<TypeVariable/*!*/>/*!*/ implicitParams,
                                             out List<TypeVariable/*!*/>/*!*/ explicitParams) {
-        Contract.Requires(cce.NonNullElements(valueArgumentTypes));
-Contract.Requires(allTypeParams != null);
-Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out implicitParams)));
-Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitParams)));
-        TypeVariableSeq/*!*/ varsInInParamTypes = new TypeVariableSeq ();
-        foreach (Type/*!*/ t in valueArgumentTypes){Contract.Assert(t != null);
-          varsInInParamTypes.AppendWithoutDups(t.FreeVariables);}
-
-        implicitParams = new List<TypeVariable/*!*/> (allTypeParams.Length);
-        explicitParams = new List<TypeVariable/*!*/> (allTypeParams.Length);
-
-        foreach (TypeVariable/*!*/ var in allTypeParams) {
-          Contract.Assert(var != null);
-          if (varsInInParamTypes.Has(var))
-            implicitParams.Add(var);
-          else
-            explicitParams.Add(var);
-        }
-        
-        implicitParams.TrimExcess();
-        explicitParams.TrimExcess();      
+      Contract.Requires(cce.NonNullElements(valueArgumentTypes));
+      Contract.Requires(allTypeParams != null);
+      Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out implicitParams)));
+      Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitParams)));
+      TypeVariableSeq/*!*/ varsInInParamTypes = new TypeVariableSeq();
+      foreach (Type/*!*/ t in valueArgumentTypes) {
+        Contract.Assert(t != null);
+        varsInInParamTypes.AppendWithoutDups(t.FreeVariables);
+      }
+
+      implicitParams = new List<TypeVariable/*!*/>(allTypeParams.Length);
+      explicitParams = new List<TypeVariable/*!*/>(allTypeParams.Length);
+
+      foreach (TypeVariable/*!*/ var in allTypeParams) {
+        Contract.Assert(var != null);
+        if (varsInInParamTypes.Has(var))
+          implicitParams.Add(var);
+        else
+          explicitParams.Add(var);
+      }
+
+      implicitParams.TrimExcess();
+      explicitParams.TrimExcess();
     }
 
     internal UntypedFunction Typed2Untyped(Function fun) {
@@ -361,7 +373,7 @@ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitParams))
 
         // if all of the parameters are int or bool, the function does
         // not have to be changed
-        if (Contract.ForAll(0,fun.InParams.Length, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&
+        if (Contract.ForAll(0, fun.InParams.Length, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&
             UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type) &&
             fun.TypeParameters.Length == 0) {
           res = new UntypedFunction(fun, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>());
@@ -398,10 +410,10 @@ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitParams))
       return res;
     }
 
-    private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun){
-Contract.Requires(originalFun != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
-      List<Type/*!*/>/*!*/ originalInTypes = new List<Type/*!*/> (originalFun.InParams.Length);
+    private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun) {
+      Contract.Requires(originalFun != null);
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      List<Type/*!*/>/*!*/ originalInTypes = new List<Type/*!*/>(originalFun.InParams.Length);
       foreach (Formal/*!*/ f in originalFun.InParams)
         originalInTypes.Add(f.TypedIdent.Type);
 
@@ -414,8 +426,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
                                       List<TypeVariable/*!*/>/*!*/ implicitTypeParams,
                                       List<TypeVariable/*!*/>/*!*/ explicitTypeParams,
                                       List<Type/*!*/>/*!*/ originalInTypes,
-                                      Type/*!*/ originalResultType)
-    {
+                                      Type/*!*/ originalResultType) {
       Contract.Requires(cce.NonNullElements(implicitTypeParams));
       Contract.Requires(fun != null);
       Contract.Requires(cce.NonNullElements(explicitTypeParams));
@@ -426,21 +437,23 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
 
       if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) {
         return VCExpressionGenerator.True;
-      }                
+      }
 
       List<VCExprVar/*!*/>/*!*/ typedInputVars = new List<VCExprVar/*!*/>(originalInTypes.Count);
       int i = 0;
-      foreach (Type/*!*/ t in originalInTypes) {Contract.Assert(t != null);
+      foreach (Type/*!*/ t in originalInTypes) {
+        Contract.Assert(t != null);
         typedInputVars.Add(Gen.Variable("arg" + i, t));
         i = i + 1;
       }
 
-      VariableBindings/*!*/ bindings = new VariableBindings ();
+      VariableBindings/*!*/ bindings = new VariableBindings();
 
       // type parameters that have to be given explicitly are replaced
       // with universally quantified type variables
-      List<VCExprVar/*!*/>/*!*/ boundVars = new List<VCExprVar/*!*/> (explicitTypeParams.Count + typedInputVars.Count);
-      foreach (TypeVariable/*!*/ var in explicitTypeParams) {Contract.Assert(var != null);
+      List<VCExprVar/*!*/>/*!*/ boundVars = new List<VCExprVar/*!*/>(explicitTypeParams.Count + typedInputVars.Count);
+      foreach (TypeVariable/*!*/ var in explicitTypeParams) {
+        Contract.Assert(var != null);
         VCExprVar/*!*/ newVar = Gen.Variable(var.Name, T);
         boundVars.Add(newVar);
         bindings.TypeVariableBindings.Add(var, newVar);
@@ -448,9 +461,9 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
 
       // bound term variables are replaced with bound term variables typed in
       // a simpler way
-      foreach(VCExprVar/*!*/ var in typedInputVars){
+      foreach (VCExprVar/*!*/ var in typedInputVars) {
         Contract.Assert(var != null);
-        Type/*!*/ newType = TypeAfterErasure(var.Type); 
+        Type/*!*/ newType = TypeAfterErasure(var.Type);
         Contract.Assert(newType != null);
         VCExprVar/*!*/ newVar = Gen.Variable(var.Name, newType);
         Contract.Assert(newVar != null);
@@ -470,7 +483,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
       VCExpr conclusionWithPremisses =
         // leave out antecedents of function type axioms ... they don't appear necessary,
         // because a function can always be extended to all U-values (right?)
-//        AddTypePremisses(typeVarBindings, typePremisses, true, conclusion);
+        //        AddTypePremisses(typeVarBindings, typePremisses, true, conclusion);
         Gen.Let(typeVarBindings, conclusion);
 
       if (boundVars.Count > 0) {
@@ -481,16 +494,16 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
         return conclusionWithPremisses;
       }
     }
-    
+
     ////////////////////////////////////////////////////////////////////////////
 
-    protected override void AddVarTypeAxiom(VCExprVar var, Type originalType){
-//Contract.Requires(originalType != null);
-//Contract.Requires(var != null);
+    protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) {
+      //Contract.Requires(originalType != null);
+      //Contract.Requires(var != null);
       if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) return;
       AddTypeAxiom(GenVarTypeAxiom(var, originalType,
-                                   // we don't have any bindings available
-                                   new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>()));      
+        // we don't have any bindings available
+                                   new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>()));
     }
 
     public VCExpr GenVarTypeAxiom(VCExprVar var, Type originalType, IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ varMapping) {
@@ -509,7 +522,8 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
 
   /////////////////////////////////////////////////////////////////////////////
 
-  internal class MapTypeAbstractionBuilderPremisses : MapTypeAbstractionBuilder {
+  internal class MapTypeAbstractionBuilderPremisses : MapTypeAbstractionBuilder
+  {
 
     private readonly TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
     [ContractInvariantMethod]
@@ -518,19 +532,21 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
     }
 
 
-    internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen) :base(axBuilder, gen){
+    internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen)
+      : base(axBuilder, gen) {
       Contract.Requires(gen != null);
       Contract.Requires(axBuilder != null);
-      
+
       this.AxBuilderPremisses = axBuilder;
     }
 
     // constructor for cloning
-    internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen, MapTypeAbstractionBuilderPremisses builder):base(axBuilder, gen, builder) {
+    internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen, MapTypeAbstractionBuilderPremisses builder)
+      : base(axBuilder, gen, builder) {
       Contract.Requires(builder != null);
       Contract.Requires(gen != null);
       Contract.Requires(axBuilder != null);
-      
+
       this.AxBuilderPremisses = axBuilder;
     }
 
@@ -935,54 +951,59 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
 
   /////////////////////////////////////////////////////////////////////////////
 
-  public class TypeEraserPremisses : TypeEraser {
+  public class TypeEraserPremisses : TypeEraser
+  {
 
     private readonly TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
     [ContractInvariantMethod]
-void ObjectInvariant() 
-{
-    Contract.Invariant(AxBuilderPremisses != null);
-}
+    void ObjectInvariant() {
+      Contract.Invariant(AxBuilderPremisses != null);
+    }
 
 
     private OpTypeEraser OpEraserAttr = null;
-    protected override OpTypeEraser/*!*/ OpEraser { get {Contract.Ensures(Contract.Result<OpTypeEraser>() != null);
+    protected override OpTypeEraser/*!*/ OpEraser {
+      get {
+        Contract.Ensures(Contract.Result<OpTypeEraser>() != null);
 
-      if (OpEraserAttr == null)
-        OpEraserAttr = new OpTypeEraserPremisses(this, AxBuilderPremisses, Gen);
-      return OpEraserAttr;
-    } }
+        if (OpEraserAttr == null)
+          OpEraserAttr = new OpTypeEraserPremisses(this, AxBuilderPremisses, Gen);
+        return OpEraserAttr;
+      }
+    }
+
+    public TypeEraserPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen)
+      : base(axBuilder, gen) {
+      Contract.Requires(gen != null);
+      Contract.Requires(axBuilder != null);
 
-    public TypeEraserPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen):base(axBuilder, gen){
-Contract.Requires(gen != null);
-Contract.Requires(axBuilder != null);
-      
       this.AxBuilderPremisses = axBuilder;
     }
 
     ////////////////////////////////////////////////////////////////////////////
 
-    public override VCExpr Visit(VCExprQuantifier node, VariableBindings oldBindings){
-Contract.Requires(oldBindings != null);
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+    public override VCExpr Visit(VCExprQuantifier node, VariableBindings oldBindings) {
+      Contract.Requires(oldBindings != null);
+      Contract.Requires(node != null);
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
       VariableBindings bindings = oldBindings.Clone();
 
       // determine the bound vars that actually occur in the body or
       // in any of the triggers (if some variables do not occur, we
       // need to take special care of type parameters that only occur
       // in the types of such variables)
-      FreeVariableCollector coll = new FreeVariableCollector ();
+      FreeVariableCollector coll = new FreeVariableCollector();
       coll.Collect(node.Body);
       foreach (VCTrigger trigger in node.Triggers) {
         if (trigger.Pos)
-          foreach(VCExpr/*!*/ e in trigger.Exprs){
-Contract.Assert(e != null);
+          foreach (VCExpr/*!*/ e in trigger.Exprs) {
+            Contract.Assert(e != null);
 
-            coll.Collect(e);}
+            coll.Collect(e);
+          }
       }
 
-      List<VCExprVar/*!*/> occurringVars = new List<VCExprVar/*!*/> (node.BoundVars.Count);
+      List<VCExprVar/*!*/> occurringVars = new List<VCExprVar/*!*/>(node.BoundVars.Count);
       foreach (VCExprVar var in node.BoundVars)
         if (coll.FreeTermVars.ContainsKey(var))
           occurringVars.Add(var);
@@ -1025,15 +1046,16 @@ Contract.Assert(e != null);
 
       // build a substitution of the type variables that it can be checked
       // whether type premisses are trivial
-      VCExprSubstitution/*!*/ typeParamSubstitution = new VCExprSubstitution ();
-      foreach(VCExprLetBinding/*!*/ binding in typeVarBindings){
-Contract.Assert(binding != null);
-        typeParamSubstitution[binding.V] = binding.E;}
-      SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor (Gen);
+      VCExprSubstitution/*!*/ typeParamSubstitution = new VCExprSubstitution();
+      foreach (VCExprLetBinding/*!*/ binding in typeVarBindings) {
+        Contract.Assert(binding != null);
+        typeParamSubstitution[binding.V] = binding.E;
+      }
+      SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);
       Contract.Assert(substituter != null);
 
-      List<VCExpr/*!*/>/*!*/ typePremisses = new List<VCExpr/*!*/> (newBoundVars.Count);
-      triggers = new List<VCTrigger/*!*/> (newBoundVars.Count);
+      List<VCExpr/*!*/>/*!*/ typePremisses = new List<VCExpr/*!*/>(newBoundVars.Count);
+      triggers = new List<VCTrigger/*!*/>(newBoundVars.Count);
 
       for (int i = 0; i < newBoundVars.Count; ++i) {
         VCExprVar/*!*/ oldVar = oldBoundVars[i];
@@ -1057,14 +1079,14 @@ Contract.Assert(binding != null);
 
       typePremisses.TrimExcess();
       triggers.TrimExcess();
-      
+
       return Gen.NAry(VCExpressionGenerator.AndOp, typePremisses);
     }
 
     // these optimisations should maybe be moved into a separate
     // visitor (peep-hole optimisations)
-    private bool IsTriviallyTrue(VCExpr expr){
-Contract.Requires(expr != null);
+    private bool IsTriviallyTrue(VCExpr expr) {
+      Contract.Requires(expr != null);
       if (expr.Equals(VCExpressionGenerator.True))
         return true;
 
@@ -1155,40 +1177,40 @@ Contract.Requires(expr != null);
       return Gen.Quantify(node.Quan, new List<TypeVariable/*!*/>(), newBoundVars,
                           newTriggers, node.Infos, bodyWithPremisses);
     }
-    
+
     // check whether we need to add let-binders for any of the type
     // parameters to the triggers (otherwise, the triggers will
     // contain unbound/dangling variables for such parameters)
-    private List<VCTrigger/*!*/>/*!*/ AddLets2Triggers( List<VCTrigger/*!*/>/*!*/ triggers/*!*/, List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings){
-Contract.Requires(cce.NonNullElements(triggers/*!*/));
-Contract.Requires(cce.NonNullElements(typeVarBindings));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
-      List<VCTrigger/*!*/>/*!*/ triggersWithLets = new List<VCTrigger/*!*/> (triggers.Count);
+    private List<VCTrigger/*!*/>/*!*/ AddLets2Triggers(List<VCTrigger/*!*/>/*!*/ triggers/*!*/, List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings) {
+      Contract.Requires(cce.NonNullElements(triggers/*!*/));
+      Contract.Requires(cce.NonNullElements(typeVarBindings));
+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
+      List<VCTrigger/*!*/>/*!*/ triggersWithLets = new List<VCTrigger/*!*/>(triggers.Count);
 
-      foreach(VCTrigger/*!*/ t in triggers){
-Contract.Assert(t != null);
-        List<VCExpr/*!*/>/*!*/ exprsWithLets = new List<VCExpr/*!*/> (t.Exprs.Count);
+      foreach (VCTrigger/*!*/ t in triggers) {
+        Contract.Assert(t != null);
+        List<VCExpr/*!*/>/*!*/ exprsWithLets = new List<VCExpr/*!*/>(t.Exprs.Count);
 
         bool changed = false;
-        foreach(VCExpr/*!*/ e in t.Exprs){
-Contract.Assert(e != null);
-Dictionary<VCExprVar/*!*/, object>/*!*/ freeVars =
-            FreeVariableCollector.FreeTermVariables(e);
-Contract.Assert(freeVars!=null&&cce.NonNullElements(freeVars.Keys));
-          if (Contract.Exists(typeVarBindings, b=>                     freeVars.ContainsKey(b.V))) {
+        foreach (VCExpr/*!*/ e in t.Exprs) {
+          Contract.Assert(e != null);
+          Dictionary<VCExprVar/*!*/, object>/*!*/ freeVars =
+                      FreeVariableCollector.FreeTermVariables(e);
+          Contract.Assert(freeVars != null && cce.NonNullElements(freeVars.Keys));
+          if (Contract.Exists(typeVarBindings, b => freeVars.ContainsKey(b.V))) {
             exprsWithLets.Add(Gen.Let(typeVarBindings, e));
             changed = true;
           } else {
             exprsWithLets.Add(e);
           }
         }
-          
+
         if (changed)
           triggersWithLets.Add(Gen.Trigger(t.Pos, exprsWithLets));
         else
           triggersWithLets.Add(t);
       }
-      
+
       return triggersWithLets;
     }
 
@@ -1196,7 +1218,8 @@ Contract.Assert(freeVars!=null&&cce.NonNullElements(freeVars.Keys));
 
   //////////////////////////////////////////////////////////////////////////////
 
-  public class OpTypeEraserPremisses : OpTypeEraser {
+  public class OpTypeEraserPremisses : OpTypeEraser
+  {
 
     private TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
     [ContractInvariantMethod]
@@ -1205,34 +1228,36 @@ Contract.Assert(freeVars!=null&&cce.NonNullElements(freeVars.Keys));
     }
 
 
-    public OpTypeEraserPremisses(TypeEraserPremisses eraser, TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen):base(eraser, axBuilder, gen){
-Contract.Requires(gen != null);
-Contract.Requires(axBuilder != null);
-Contract.Requires(eraser != null);
+    public OpTypeEraserPremisses(TypeEraserPremisses eraser, TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen)
+      : base(eraser, axBuilder, gen) {
+      Contract.Requires(gen != null);
+      Contract.Requires(axBuilder != null);
+      Contract.Requires(eraser != null);
       this.AxBuilderPremisses = axBuilder;
     }
 
-    private VCExpr HandleFunctionOp(Function newFun,  List<Type/*!*/>/*!*/ typeArgs/*!*/, IEnumerable<VCExpr/*!*/>/*!*/ oldArgs, VariableBindings bindings){
-Contract.Requires(bindings != null);
-Contract.Requires(newFun != null);
-Contract.Requires(cce.NonNullElements(typeArgs/*!*/));
-Contract.Requires(cce.NonNullElements(oldArgs));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+    private VCExpr HandleFunctionOp(Function newFun, List<Type/*!*/>/*!*/ typeArgs/*!*/, IEnumerable<VCExpr/*!*/>/*!*/ oldArgs, VariableBindings bindings) {
+      Contract.Requires(bindings != null);
+      Contract.Requires(newFun != null);
+      Contract.Requires(cce.NonNullElements(typeArgs/*!*/));
+      Contract.Requires(cce.NonNullElements(oldArgs));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
       // UGLY: the code for tracking polarities should be factored out
       int oldPolarity = Eraser.Polarity;
       Eraser.Polarity = 0;
 
-      List<VCExpr/*!*/>/*!*/ newArgs = new List<VCExpr/*!*/> (typeArgs.Count);
+      List<VCExpr/*!*/>/*!*/ newArgs = new List<VCExpr/*!*/>(typeArgs.Count);
 
       // translate the explicit type arguments
-      foreach(Type/*!*/ t in typeArgs){
-Contract.Assert(t != null);
-        newArgs.Add(AxBuilder.Type2Term(t, bindings.TypeVariableBindings));}
+      foreach (Type/*!*/ t in typeArgs) {
+        Contract.Assert(t != null);
+        newArgs.Add(AxBuilder.Type2Term(t, bindings.TypeVariableBindings));
+      }
 
       // recursively translate the value arguments
-      foreach(VCExpr/*!*/ arg in oldArgs){
-Contract.Assert(arg != null);
-Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type;
+      foreach (VCExpr/*!*/ arg in oldArgs) {
+        Contract.Assert(arg != null);
+        Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type;
         newArgs.Add(AxBuilder.Cast(Eraser.Mutate(arg, bindings), newType));
       }
 
@@ -1240,8 +1265,9 @@ Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type;
       return Gen.Function(newFun, newArgs);
     }
 
-    public override VCExpr/*!*/ VisitSelectOp   (VCExprNAry/*!*/ node,
-                                             VariableBindings/*!*/ bindings) {Contract.Requires(node != null);Contract.Requires(bindings != null);
+    public override VCExpr/*!*/ VisitSelectOp(VCExprNAry/*!*/ node,
+                                             VariableBindings/*!*/ bindings) {
+      Contract.Requires(node != null); Contract.Requires(bindings != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
 
       MapType/*!*/ mapType = node[0].Type.AsMap;
@@ -1262,29 +1288,29 @@ Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type;
       return HandleFunctionOp(select, typeArgs, node, bindings);
     }
 
-    public override VCExpr VisitStoreOp    (VCExprNAry node, VariableBindings bindings){
-Contract.Requires(bindings != null);
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+    public override VCExpr VisitStoreOp(VCExprNAry node, VariableBindings bindings) {
+      Contract.Requires(bindings != null);
+      Contract.Requires(node != null);
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
       TypeSeq/*!*/ instantiations; // not used
       Function/*!*/ store =
         AxBuilder.MapTypeAbstracter.Store(node[0].Type.AsMap, out instantiations);
       Contract.Assert(store != null);
       return HandleFunctionOp(store,
-                              // the store function never has explicit
-                              // type parameters
+        // the store function never has explicit
+        // type parameters
                               new List<Type/*!*/>(),
                               node, bindings);
     }
 
-    public override VCExpr VisitBoogieFunctionOp (VCExprNAry node, VariableBindings bindings){
-Contract.Requires(bindings != null);
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+    public override VCExpr VisitBoogieFunctionOp(VCExprNAry node, VariableBindings bindings) {
+      Contract.Requires(bindings != null);
+      Contract.Requires(node != null);
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
       Function/*!*/ oriFun = ((VCExprBoogieFunctionOp)node.Op).Func;
       Contract.Assert(oriFun != null);
       UntypedFunction untypedFun = AxBuilderPremisses.Typed2Untyped(oriFun);
-      Contract.Assert( untypedFun.Fun.InParams.Length ==
+      Contract.Assert(untypedFun.Fun.InParams.Length ==
              untypedFun.ExplicitTypeParams.Count + node.Arity);
 
       List<Type/*!*/>/*!*/ typeArgs =
@@ -1293,12 +1319,12 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
       return HandleFunctionOp(untypedFun.Fun, typeArgs, node, bindings);
     }
 
-    private List<Type/*!*/>/*!*/ ExtractTypeArgs(VCExprNAry node, TypeVariableSeq allTypeParams, List<TypeVariable/*!*/>/*!*/ explicitTypeParams){
-Contract.Requires(allTypeParams != null);
-Contract.Requires(node != null);
-Contract.Requires(cce.NonNullElements(explicitTypeParams));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
-      List<Type/*!*/>/*!*/ res = new List<Type/*!*/> (explicitTypeParams.Count);
+    private List<Type/*!*/>/*!*/ ExtractTypeArgs(VCExprNAry node, TypeVariableSeq allTypeParams, List<TypeVariable/*!*/>/*!*/ explicitTypeParams) {
+      Contract.Requires(allTypeParams != null);
+      Contract.Requires(node != null);
+      Contract.Requires(cce.NonNullElements(explicitTypeParams));
+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
+      List<Type/*!*/>/*!*/ res = new List<Type/*!*/>(explicitTypeParams.Count);
       foreach (TypeVariable/*!*/ var in explicitTypeParams) {
         Contract.Assert(var != null);
         // this lookup could be optimised
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 89c615ad..74505150 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -664,7 +664,6 @@ namespace Microsoft.Boogie.VCExprAST {
           return !ib.MoveNext();
         }
       }
-      return true;
     }
 
     public static int PolyHash(int init, int factor, IEnumerable a) {
@@ -1505,6 +1504,14 @@ namespace Microsoft.Boogie.VCExprAST {
         return false;
       return this.Name == t.Name && this.arity == t.arity && this.Type == t.Type;
     }
+    [Pure]
+    [Reads(ReadsAttribute.Reads.Nothing)]
+    public override int GetHashCode() {
+      int h = Name.GetHashCode();
+      h = 7823 * h + arity;
+      h = 7823 * h + Type.GetHashCode();
+      return h;
+    }
     public override int Arity {
       get {
         return arity;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 9e68dc58..55cfa650 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -69,6 +69,7 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(Trace != null);
+      Contract.Invariant(Context != null);
       Contract.Invariant(cce.NonNullElements(relatedInformation));
       Contract.Invariant(cce.NonNullElements(calleeCounterexamples));
     }
@@ -77,16 +78,19 @@ namespace Microsoft.Boogie {
     public BlockSeq Trace;
     public ErrorModel Model;
     public VC.ModelViewInfo MvInfo;
+    public ProverContext Context;
     [Peer]
     public List<string>/*!>!*/ relatedInformation;
 
     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
 
-    internal Counterexample(BlockSeq trace, ErrorModel model, VC.ModelViewInfo mvInfo) {
+    internal Counterexample(BlockSeq trace, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context) {
       Contract.Requires(trace != null);
+      Contract.Requires(context != null);
       this.Trace = trace;
       this.Model = model;
       this.MvInfo = mvInfo;
+      this.Context = context;
       this.relatedInformation = new List<string>();
       this.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
     }
@@ -195,11 +199,70 @@ namespace Microsoft.Boogie {
       }
       // we now have the list of states in 'states'
       states.Sort();
+#if DEBUG_PRINT
+      Console.WriteLine("DEBUG: ---------- start ----------");
+      foreach (Variable v in MvInfo.AllVariables) {
+        List<string> names = new List<string>();
+
+        {
+          string ss = v.Name;
+          VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(v);
+          if (vvar != null) {
+            string uniqueName = Context.Lookup(vvar);
+            ss += " -> " + uniqueName;
+          }
+          names.Add(ss);
+        }
+
+        foreach (int s in states) {
+          if (0 <= s && s < MvInfo.CapturePoints.Count) {
+            VC.ModelViewInfo.Mapping m = MvInfo.CapturePoints[s];
+            var map = m.IncarnationMap;
+            if (map.ContainsKey(v)) {
+              Expr e = (Expr)map[v];
+              var ss = string.Format("[{0}: {1}", m.Description, e.ToString());
+              IdentifierExpr ide = e as IdentifierExpr;
+              if (ide != null) {
+                VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(ide.Decl);
+                if (vvar != null) {
+                  string uniqueName = Context.Lookup(vvar);
+                  ss += " -> " + uniqueName;
+                }
+              }
+              ss += "]";
+              names.Add(ss);
+            }
+          }
+        }
+
+        foreach (var nm in names) {
+          Console.Write("{0} ", nm);
+        }
+        Console.WriteLine();
+      }
+      Console.WriteLine("DEBUG: ---------- end ----------");
+#endif
+      List<Variable> changedVariables;
+      if (states.Count <= 1) {
+        changedVariables = MvInfo.AllVariables;
+      } else {
+        VC.ModelViewInfo.Mapping last = MvInfo.CapturePoints[MvInfo.CapturePoints.Count-1];
+        changedVariables = new List<Variable>();
+        List<Variable> unchangedVariables = new List<Variable>();
+        foreach (Variable v in MvInfo.AllVariables) {
+          if (last.IncarnationMap.ContainsKey(v)) {
+            changedVariables.Add(v);
+          } else {
+            unchangedVariables.Add(v);
+          }
+        }
+        PrintCapturedState(8, unchangedVariables, new Hashtable());
+      }
       foreach (int s in states) {
         if (0 <= s && s < MvInfo.CapturePoints.Count) {
           VC.ModelViewInfo.Mapping m = MvInfo.CapturePoints[s];
           Console.WriteLine("    {0}", m.Description);
-          PrintCapturedState(8, m.IncarnationMap);
+          PrintCapturedState(8, changedVariables, m.IncarnationMap);
         } else {
           Console.WriteLine("    undefined captured-state ID {0}", s);
         }
@@ -263,20 +326,21 @@ namespace Microsoft.Boogie {
       return m;
     }
 
-    void PrintCapturedState(int indent, Hashtable/*Variable -> Expr*/ incarnations) {
+    void PrintCapturedState(int indent, List<Variable> varSet, Hashtable/*Variable -> Expr*/ incarnations) {
       Contract.Requires(0 <= indent);
+      Contract.Requires(varSet != null);
       Contract.Requires(Model != null && MvInfo != null);
       string ind = new string(' ', indent);
 
-      foreach (Variable v in MvInfo.AllVariables) {
+      foreach (Variable v in varSet) {
         string varName = v.Name;
-        string incarnationName = varName;
+        Variable incarnation = v;
         string val = null;
         if (incarnations.ContainsKey(v)) {
           Expr e = (Expr)incarnations[v];
           if (e is IdentifierExpr) {
             IdentifierExpr ide = (IdentifierExpr)e;
-            incarnationName = ide.Decl.Name;
+            incarnation = ide.Decl;
           } else if (e is LiteralExpr) {
             LiteralExpr lit = (LiteralExpr)e;
             val = lit.Val.ToString();
@@ -285,17 +349,25 @@ namespace Microsoft.Boogie {
           }
         }
         if (val == null) {
+          // first, get the unique name
+          string uniqueName;
+          VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(incarnation);
+          if (vvar == null) {
+            uniqueName = incarnation.Name;
+          } else {
+            uniqueName = Context.Lookup(vvar);
+          }
           // look up the value in the model
-          int partition;
-          if (Model.identifierToPartition.TryGetValue(incarnationName, out partition)) {
-            object pvalue = Model.partitionToValue[partition];
+          int zid;
+          if (Model.identifierToPartition.TryGetValue(uniqueName, out zid)) {
+            object pvalue = Model.partitionToValue[zid];
             if (pvalue != null) {
               val = pvalue.ToString();
             } else {
-              val = "*" + partition;  // temporary hack to have something to do in this case
+              val = "*" + zid;  // temporary hack to have something to do in this case
             }
           } else {
-            val = incarnationName;  // temporary hack to have something to do in this case
+            val = uniqueName;  // temporary hack to have something to do in this case
           }
         }
         Console.WriteLine("{0}{1} = {2}", ind, varName, val);
@@ -326,12 +398,12 @@ namespace Microsoft.Boogie {
     }
 
 
-    public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, ErrorModel model, VC.ModelViewInfo mvInfo)
-      : base(trace, model, mvInfo) {
+    public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)
+      : base(trace, model, mvInfo, context) {
       Contract.Requires(trace != null);
       Contract.Requires(failingAssert != null);
+      Contract.Requires(context != null);
       this.FailingAssert = failingAssert;
-      // base(trace);
     }
 
     public override int GetLocation() {
@@ -340,7 +412,7 @@ namespace Microsoft.Boogie {
 
     public override Counterexample Clone()
     {
-        var ret = new AssertCounterexample(Trace, FailingAssert, Model, MvInfo);
+        var ret = new AssertCounterexample(Trace, FailingAssert, Model, MvInfo, Context);
         ret.calleeCounterexamples = calleeCounterexamples;
         return ret;
     }
@@ -356,15 +428,15 @@ namespace Microsoft.Boogie {
     }
 
 
-    public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, ErrorModel model, VC.ModelViewInfo mvInfo)
-      : base(trace, model, mvInfo) {
+    public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)
+      : base(trace, model, mvInfo, context) {
       Contract.Requires(!failingRequires.Free);
       Contract.Requires(trace != null);
+      Contract.Requires(context != null);
       Contract.Requires(failingCall != null);
       Contract.Requires(failingRequires != null);
       this.FailingCall = failingCall;
       this.FailingRequires = failingRequires;
-      // base(trace);
     }
 
     public override int GetLocation() {
@@ -373,7 +445,7 @@ namespace Microsoft.Boogie {
 
     public override Counterexample Clone()
     {
-        var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo);
+        var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context);
         ret.calleeCounterexamples = calleeCounterexamples;
         return ret;
     }
@@ -389,15 +461,15 @@ namespace Microsoft.Boogie {
     }
 
 
-    public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, ErrorModel model, VC.ModelViewInfo mvInfo)
-      : base(trace, model, mvInfo) {
+    public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)
+      : base(trace, model, mvInfo, context) {
       Contract.Requires(trace != null);
+      Contract.Requires(context != null);
       Contract.Requires(failingReturn != null);
       Contract.Requires(failingEnsures != null);
       Contract.Requires(!failingEnsures.Free);
       this.FailingReturn = failingReturn;
       this.FailingEnsures = failingEnsures;
-      // base(trace);
     }
 
     public override int GetLocation() {
@@ -406,7 +478,7 @@ namespace Microsoft.Boogie {
 
     public override Counterexample Clone()
     {
-        var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo);
+        var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo, Context);
         ret.calleeCounterexamples = calleeCounterexamples;
         return ret;
     }
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 40e454fb..ac52111e 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -87,9 +87,8 @@ public abstract class ProverContextContracts:ProverContext{
     protected List<VCExpr> axiomConjuncts;
 
     [ContractInvariantMethod]
-void ObjectInvariant() 
-{
-    Contract.Invariant(gen!=null);
+    void ObjectInvariant() {
+      Contract.Invariant(gen != null);
       Contract.Invariant(genOptions != null);
       Contract.Invariant(translator != null);
       Contract.Invariant(orderingAxiomBuilder != null);
@@ -97,7 +96,7 @@ void ObjectInvariant()
       Contract.Invariant(incrementalProverCommands != null);
       Contract.Invariant(cce.NonNullElements(distincts));
       Contract.Invariant(cce.NonNullElements(axiomConjuncts));
-}
+    }
 
     public VCExprTranslator/*?*/ exprTranslator;
 
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 13206c75..304130ef 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1362,7 +1362,8 @@ namespace VC {
         impl.Blocks = tmp;
       }
 
-      public Counterexample ToCounterexample() {
+      public Counterexample ToCounterexample(ProverContext context) {
+        Contract.Requires(context != null);
         Contract.Ensures(Contract.Result<Counterexample>() != null);
 
         BlockSeq trace = new BlockSeq();
@@ -1375,7 +1376,7 @@ namespace VC {
           foreach (Cmd c in b.Cmds) {
             Contract.Assert(c != null);
             if (c is AssertCmd) {
-              return AssertCmdToCounterexample((AssertCmd)c, cce.NonNull(b.TransferCmd), trace, null, null, new Dictionary<Incarnation, Absy>());
+              return AssertCmdToCounterexample((AssertCmd)c, cce.NonNull(b.TransferCmd), trace, null, null, context, new Dictionary<Incarnation, Absy>());
             }
           }
         }
@@ -1836,7 +1837,7 @@ namespace VC {
             if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
               msg = s.reporter.resourceExceededMessage;
             }
-            callback.OnCounterexample(s.ToCounterexample(), msg);
+            callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);
             outcome = Outcome.Errors;
             break;
           }
@@ -2977,7 +2978,7 @@ namespace VC {
       }
 
       Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo;
-      ProverContext/*!*/ context;
+      protected ProverContext/*!*/ context;
       Program/*!*/ program;
 
       public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,
@@ -3097,7 +3098,6 @@ namespace VC {
         Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));
         Contract.Requires(context != null);
         Contract.Requires(program != null);
-
       }
 
       public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel) {
@@ -3132,7 +3132,7 @@ namespace VC {
             if (b.Cmds.Has(a)) {
               BlockSeq trace = new BlockSeq();
               trace.Add(b);
-              Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel, MvInfo, incarnationOriginMap);
+              Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel, MvInfo, context, incarnationOriginMap);
               callback.OnCounterexample(newCounterexample, null);
               goto NEXT_ASSERT;
             }
@@ -3321,7 +3321,7 @@ namespace VC {
                 // Skip if 'cmd' not contained in the trace or not an assert
                 if (cmd is AssertCmd && traceNodes.Contains(cmd))
                 {
-                    Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, new Dictionary<Incarnation, Absy/*!*/>());
+                    Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, context, new Dictionary<Incarnation, Absy/*!*/>());
                     newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
                     return newCounterexample;
                 }
@@ -3979,7 +3979,7 @@ namespace VC {
           if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, assertCmd.UniqueId) == 0)
           {
             Counterexample newCounterexample;
-            newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, mvInfo, cce.NonNull(info.incarnationOriginMap));
+            newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, mvInfo, context, cce.NonNull(info.incarnationOriginMap));
             newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
             return newCounterexample;
           }
@@ -4110,7 +4110,7 @@ namespace VC {
         // Skip if 'cmd' not contained in the trace or not an assert
         if (cmd is AssertCmd && traceNodes.Contains(cmd))
         {
-          Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, incarnationOriginMap);
+          Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, context, incarnationOriginMap);
           Contract.Assert(newCounterexample != null);
           newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
           return newCounterexample;
@@ -4878,12 +4878,13 @@ namespace VC {
       }
     }
 
-    static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, ErrorModel errModel, ModelViewInfo mvInfo,
+    static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, ErrorModel errModel, ModelViewInfo mvInfo, ProverContext context,
       Dictionary<Incarnation, Absy> incarnationOriginMap) 
     {
       Contract.Requires(cmd != null);
       Contract.Requires(transferCmd != null);
       Contract.Requires(trace != null);
+      Contract.Requires(context != null);
       Contract.Requires(cce.NonNullElements(incarnationOriginMap));
       Contract.Ensures(Contract.Result<Counterexample>() != null);
 
@@ -4904,7 +4905,7 @@ namespace VC {
       {
         AssertRequiresCmd assertCmd = (AssertRequiresCmd)cmd;
         Contract.Assert(assertCmd != null);
-        CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo);
+        CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo, context);
         cc.relatedInformation = relatedInformation;
         return cc;
       }
@@ -4912,13 +4913,13 @@ namespace VC {
       {
         AssertEnsuresCmd assertCmd = (AssertEnsuresCmd)cmd;
         Contract.Assert(assertCmd != null);
-        ReturnCounterexample rc = new ReturnCounterexample(trace, transferCmd, assertCmd.Ensures, errModel, mvInfo);
+        ReturnCounterexample rc = new ReturnCounterexample(trace, transferCmd, assertCmd.Ensures, errModel, mvInfo, context);
         rc.relatedInformation = relatedInformation;
         return rc;
       }
       else 
       {
-        AssertCounterexample ac = new AssertCounterexample(trace, (AssertCmd)cmd, errModel, mvInfo);
+        AssertCounterexample ac = new AssertCounterexample(trace, (AssertCmd)cmd, errModel, mvInfo, context);
         ac.relatedInformation = relatedInformation;
         return ac;
       }
-- 
cgit v1.2.3