merge

12 files changed, 527 insertions, 62 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index d961eb3e..5ed619d6 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1865,14 +1865,14 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public byte[] MD5DependenciesChecksum_;

-    public byte[] MD5DependenciesChecksum

+    public byte[] MD5DependencyChecksum_;

+    public byte[] MD5DependencyChecksum

     {

       get

       {

         Contract.Requires(DependenciesCollected);

 

-        if (MD5DependenciesChecksum_ == null && MD5Checksum != null)

+        if (MD5DependencyChecksum_ == null && MD5Checksum != null)

         {

           var c = MD5Checksum;

           var transFuncDeps = new HashSet<Function>();

@@ -1918,9 +1918,9 @@ namespace Microsoft.Boogie {
               }

             }

           }

-          MD5DependenciesChecksum_ = c;

+          MD5DependencyChecksum_ = c;

         }

-        return MD5DependenciesChecksum_;

+        return MD5DependencyChecksum_;

       }

     }

 

@@ -1932,16 +1932,16 @@ namespace Microsoft.Boogie {
       }

     }

 

-    string dependenciesChecksum;

-    public string DependenciesChecksum

+    string dependencyChecksum;

+    public string DependencyChecksum

     {

       get

       {

-        if (dependenciesChecksum == null && MD5DependenciesChecksum != null)

+        if (dependencyChecksum == null && MD5DependencyChecksum != null)

         {

-          dependenciesChecksum = BitConverter.ToString(MD5DependenciesChecksum);

+          dependencyChecksum = BitConverter.ToString(MD5DependencyChecksum);

         }

-        return dependenciesChecksum;

+        return dependencyChecksum;

       }

     }

 

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index b16fb1ba..26a28e0e 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1999,7 +1999,7 @@ namespace Microsoft.Boogie {
     public string/*!*/ callee { get; set; }

     public Procedure Proc;

     public LocalVariable AssignedAssumptionVariable;

-    public bool EmitDependenciesChecksum;

+    public bool EmitDependencyChecksum;

 

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

     // the call happens with * as these parameters

@@ -2087,12 +2087,12 @@ namespace Microsoft.Boogie {
         stream.Write(" := ");

       }

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

-      if (stream.UseForComputingChecksums && EmitDependenciesChecksum)

+      if (stream.UseForComputingChecksums && EmitDependencyChecksum)

       {

-        var c = Proc.DependenciesChecksum;

+        var c = Proc.DependencyChecksum;

         if (c != null)

         {

-          stream.Write(string.Format("[dependencies_checksum:{0}]", c));

+          stream.Write(string.Format("[dependency_checksum:{0}]", c));

         }

       }

       stream.Write("(");

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 8d372b0c..95a11a65 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1804,10 +1804,10 @@ namespace Microsoft.Boogie {
       this.name.Emit(stream, 0xF0, false);

       if (stream.UseForComputingChecksums)

       {

-        var c = Func.DependenciesChecksum;

+        var c = Func.DependencyChecksum;

         if (c != null)

         {

-          stream.Write(string.Format("[dependencies_checksum:{0}]", c));

+          stream.Write(string.Format("[dependency_checksum:{0}]", c));

         }

       }

       stream.Write("(");

@@ -1893,7 +1893,19 @@ namespace Microsoft.Boogie {
       this.Type = type;

     }

 

-    public string/*!*/ FunctionName {

+    public override bool Equals(object obj) {

+      TypeCoercion other = obj as TypeCoercion;

+      if (other == null) {

+        return false;

+      } else {

+        return object.Equals(Type, other.Type);

+      }

+    }

+

+

+

+    public

+      string/*!*/ FunctionName {

       get {

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

 

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index eefc7102..32985053 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -57,7 +57,6 @@ namespace Microsoft.Boogie {
       Contract.Invariant(Body != null);

     }

 

-

     public BinderExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,

                       List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)

       : base(tok)

@@ -77,24 +76,43 @@ namespace Microsoft.Boogie {
       get;

     }

 

+    protected static bool CompareAttributesAndTriggers = false;

+

+    public static bool EqualWithAttributesAndTriggers(object a, object b) {

+      CompareAttributesAndTriggers = true;

+      var res = object.Equals(a, b);

+      Contract.Assert(CompareAttributesAndTriggers);

+      CompareAttributesAndTriggers = false;

+      return res;

+    }

+

     [Pure]

     [Reads(ReadsAttribute.Reads.Nothing)]

     public override bool Equals(object obj) {

-      if (obj == null)

+      return BinderEquals(obj);

+    }

+

+    public bool BinderEquals(object obj) {

+      if (obj == null) {

         return false;

+      }

       if (!(obj is BinderExpr) ||

-          this.Kind != ((BinderExpr)obj).Kind)

+          this.Kind != ((BinderExpr) obj).Kind) {

         return false;

+      }

+

+      var other = (BinderExpr) obj;

 

-      BinderExpr other = (BinderExpr)obj;

-      // Note, we consider quantifiers equal modulo the Triggers.

       return this.TypeParameters.SequenceEqual(other.TypeParameters)

              && this.Dummies.SequenceEqual(other.Dummies)

+             && (!CompareAttributesAndTriggers || object.Equals(this.Attributes, other.Attributes))

              && object.Equals(this.Body, other.Body);

     }

 

     [Pure]

     public override int GetHashCode() {

+      // Note, we don't hash triggers and attributes

+   

       // DO NOT USE Dummies.GetHashCode() because we want structurally

       // identical Expr to have the same hash code **not** identical references

       // to have the same hash code.

@@ -103,7 +121,6 @@ namespace Microsoft.Boogie {
         h = ( 53 * h ) + dummyVar.GetHashCode();

       }

 

-      // Note, we consider quantifiers equal modulo the Triggers.

       h ^= this.Body.GetHashCode();

 

       // DO NOT USE TypeParameters.GetHashCode() because we want structural

@@ -351,6 +368,22 @@ namespace Microsoft.Boogie {
     public override Absy StdDispatch(StandardVisitor visitor) {

       return visitor.VisitQKeyValue(this);

     }

+

+    public override bool Equals(object obj) {

+      var other = obj as QKeyValue;

+      if (other == null) {

+        return false;

+      } else {

+        return Key == other.Key && object.Equals(Params, other.Params) &&

+               (Next == null

+                 ? other.Next == null

+                 : object.Equals(Next, other.Next));

+      }

+    }

+

+    public override int GetHashCode() {

+      throw new NotImplementedException();

+    }

   }

 

   public class Trigger : Absy {

@@ -448,6 +481,20 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Absy>() != null);

       return visitor.VisitTrigger(this);

     }

+

+    public override bool Equals(object obj) {

+      var other = obj as Trigger;

+      if (other == null) {

+        return false;

+      } else {

+        return this.Tr.SequenceEqual(other.Tr) && 

+          (Next == null ? other.Next == null : object.Equals(Next, other.Next));

+      }

+    }

+

+    public override int GetHashCode() {

+      throw new NotImplementedException();

+    }

   }

 

   public class ForallExpr : QuantifierExpr {

@@ -736,6 +783,15 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public override bool Equals(object obj) {

+      var other = obj as QuantifierExpr;

+      if (other == null) {

+        return false;

+      } else {

+        return this.BinderEquals(obj) && 

+          (!CompareAttributesAndTriggers || object.Equals(Triggers, other.Triggers));

+      }

+    }

   }

 

 

diff --git a/Source/Core/AlphaEquality.cs b/Source/Core/AlphaEquality.cs
new file mode 100644
index 00000000..1d4a1d95
--- /dev/null
+++ b/Source/Core/AlphaEquality.cs
@@ -0,0 +1,162 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+

+using System.ComponentModel;

+

+namespace Microsoft.Boogie

+{

+

+  using System;

+  using System.IO;

+  using System.Collections;

+  using System.Collections.Generic;

+  using System.Diagnostics;

+  using System.Diagnostics.Contracts;

+

+  public class AlphaEquality : IEqualityComparer<Expr>

+  {

+    private readonly DeBruijnRenamer deBruijn = new DeBruijnRenamer();

+

+    bool IEqualityComparer<Expr>.Equals(Expr x, Expr y) {

+      var nx = deBruijn.Rename(x);

+      var ny = deBruijn.Rename(y);

+      return BinderExpr.EqualWithAttributesAndTriggers(nx, ny);

+    }

+

+    int IEqualityComparer<Expr>.GetHashCode(Expr obj) {

+      return 0; 

+      // Best we can do because GetHashCode for Expression don't respect its equality.

+      // When it does, we can instead use: 

+      // return deBruijn.Rename(obj).GetHashCode(); 

+    }

+

+    // Renames expressions into deBruijn indicies, such as

+    //     (lambda x : int :: x + a) 

+    // into

+    //     (lambda bv#0 : int :: bv#0 + fv#0) 

+    // It does not handle type variables yet, but it could be added.

+    //

+    // This class could be made public, but it is not since the Rename method 

+    // could then leak FreeVariables out of here.

+    private class DeBruijnRenamer : Duplicator

+    {

+

+      // Maps from index positions and types to new variables

+      private readonly TypeDict<BoundVariable> boundVars =

+        new TypeDict<BoundVariable>("bv", ti => new BoundVariable(Token.NoToken, ti));

+

+      private readonly TypeDict<FreeVariable> freeVars =

+        new TypeDict<FreeVariable>("fv", ti => new FreeVariable(ti));

+

+      // These three variables are reset at the beginning of every renaming

+      private int boundVarCount, freeVarCount;

+      private Dictionary<Variable, FreeVariable> freeVarMap;

+

+      // Cached, previous results

+      private readonly Dictionary<Expr, Expr> cache = new Dictionary<Expr, Expr>();

+

+      public Expr Rename(Expr e) {

+        Expr ne;

+        if (!cache.TryGetValue(e, out ne)) {

+          boundVarCount = 0;

+          freeVarCount = 0;

+          freeVarMap = new Dictionary<Variable, FreeVariable>();

+

+          ne = VisitExpr(e);

+          cache[e] = ne;

+#if DEBUG_ALPHA_RENAMING

+          var wr = new TokenTextWriter("<console>", Console.Out, true);

+          Console.Write("nm( ");

+          e.Emit(wr);

+          Console.WriteLine(" )");

+          Console.Write("  = ");

+          ne.Emit(wr);

+          Console.WriteLine("");

+          Console.WriteLine("h = " + ne.GetHashCode());

+#endif

+        }

+        return ne;

+      }

+

+      public override BinderExpr VisitBinderExpr(BinderExpr node) {

+        var subst = new Dictionary<Variable, Expr>();

+        var newBound = new List<Variable>();

+        foreach (var bv in node.Dummies) {

+          var bvNew = boundVars[boundVarCount++, bv.TypedIdent.Type];

+          newBound.Add(bvNew);

+          subst[bv] = new IdentifierExpr(Token.NoToken, bvNew);

+        }

+        node.Dummies = this.VisitVariableSeq(newBound);

+        node.Body = this.VisitExpr(Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), node.Body));

+        return node;

+      }

+

+      public override Variable VisitVariable(Variable node) {

+        FreeVariable fv;

+        var bv = node as BoundVariable;

+        if (boundVars.ContainsValue(bv)) {

+          return node;

+        } else if (freeVarMap.TryGetValue(node, out fv)) {

+          return fv;

+        } else {

+          return freeVarMap[node] = freeVars[freeVarCount++, node.TypedIdent.Type];

+        }

+      }

+

+      public override Expr VisitIdentifierExpr(IdentifierExpr node) {

+        var ie = (IdentifierExpr) base.VisitIdentifierExpr(node);

+        // Need to fix up the name, since IdentifierExpr's equality also checks the name

+        ie.Name = ie.Decl.TypedIdent.Name;

+        return ie;

+      }

+

+      private class TypeDict<A>

+      {

+        private readonly Dictionary<Tuple<int, Type>, A> vars = new Dictionary<Tuple<int, Type>, A>();

+

+        private readonly string Prefix;          // either "bv" or "fv"

+        private readonly Func<TypedIdent, A> Mk; // either new BoundVar or new FreeVar

+

+        public TypeDict(string prefix, Func<TypedIdent, A> mk) {

+          Prefix = prefix;

+          Mk = mk;

+        }

+

+        // For debugging purposes, we create unique names when types differ, but the index are the same.

+        private int created = 0;

+

+        // Make sure that this index and this type is always mapped to the same variable

+        public A this[int i, Type t] {

+          get {

+            A v;

+            if (!vars.TryGetValue(Tuple.Create(i, t), out v)) {

+              v = Mk(new TypedIdent(Token.NoToken, Prefix + i + "#" + created++, t));

+              vars[Tuple.Create(i, t)] = v;

+            }

+            return v;

+          }

+        }

+

+        public bool ContainsValue(A a) {

+          return vars.ContainsValue(a);

+        }

+      }

+

+      private class FreeVariable : Variable

+      {

+        public FreeVariable(TypedIdent ti) : base(Token.NoToken, ti) {}

+

+        public override bool IsMutable {

+          get { throw new cce.UnreachableException(); }

+        }

+

+        public override void Register(ResolutionContext rc) {

+          throw new cce.UnreachableException();

+        }

+      }

+    }

+  }

+}

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index 881daa7f..27f4eea7 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -164,6 +164,7 @@
     <Compile Include="AbsyExpr.cs" />

     <Compile Include="AbsyQuant.cs" />

     <Compile Include="AbsyType.cs" />

+    <Compile Include="AlphaEquality.cs" />

     <Compile Include="InterProceduralReachabilityGraph.cs" />

     <Compile Include="CommandLineOptions.cs" />

     <Compile Include="DeadVarElim.cs" />

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index c884be3c..45c68fdd 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -52,6 +52,9 @@ namespace Microsoft.Boogie {
     }

 

     private class LambdaVisitor : StandardVisitor {

+      private readonly Dictionary<Expr, FunctionCall> liftedLambdas = 

+        new Dictionary<Expr, FunctionCall>(new AlphaEquality());

+

       internal List<Expr/*!*/>/*!*/ lambdaAxioms = new List<Expr/*!*/>();

       internal List<Function/*!*/>/*!*/ lambdaFunctions = new List<Function/*!*/>();

       [ContractInvariantMethod]

@@ -148,43 +151,61 @@ namespace Microsoft.Boogie {
           }

         }

 

+        var sw = new System.IO.StringWriter();

+        var wr = new TokenTextWriter(sw, true);

+        lambda.Emit(wr);

+        string lam_str = sw.ToString();

+

+        FunctionCall fcall;

         IToken tok = lambda.tok;

         Formal res = new Formal(tok, new TypedIdent(tok, TypedIdent.NoName, cce.NonNull(lambda.Type)), false);

-        Function fn = new Function(tok, "lambda@" + lambdaid++, freshTypeVars, formals, res, "auto-generated lambda function",

-          Substituter.Apply(Substituter.SubstitutionFromHashtable(substFnAttrs), lambdaAttrs));

-        lambdaFunctions.Add(fn);

 

-        FunctionCall fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name));

-        fcall.Func = fn;  // resolve here

+        if (liftedLambdas.TryGetValue(lambda, out fcall)) {

+          if (CommandLineOptions.Clo.TraceVerify) {

+            Console.WriteLine("Old lambda: {0}", lam_str);

+          }

+        } else {

+          if (CommandLineOptions.Clo.TraceVerify) {

+            Console.WriteLine("New lambda: {0}", lam_str);

+          }

+          Function fn = new Function(tok, "lambda#" + lambdaid++, freshTypeVars, formals, res, "auto-generated lambda function",

+            Substituter.Apply(Substituter.SubstitutionFromHashtable(substFnAttrs), lambdaAttrs));

+

+          fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name));

+          fcall.Func = fn;  // resolve here

+          liftedLambdas[lambda] = fcall;

 

-        List<Expr/*!*/> selectArgs = new List<Expr/*!*/>();

-        foreach (Variable/*!*/ v in lambda.Dummies) {

-          Contract.Assert(v != null);

-          selectArgs.Add(new IdentifierExpr(v.tok, v));

-        }

-        NAryExpr axcall = new NAryExpr(tok, fcall, axCallArgs);

-        axcall.Type = res.TypedIdent.Type;

-        axcall.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals);

-        NAryExpr select = Expr.Select(axcall, selectArgs);

-        select.Type = lambdaBody.Type;

-        List<Type/*!*/> selectTypeParamActuals = new List<Type/*!*/>();

-        List<TypeVariable> forallTypeVariables = new List<TypeVariable>();

-        foreach (TypeVariable/*!*/ tp in lambda.TypeParameters) {

-          Contract.Assert(tp != null);

-          selectTypeParamActuals.Add(tp);

-          forallTypeVariables.Add(tp);

+          List<Expr/*!*/> selectArgs = new List<Expr/*!*/>();

+          foreach (Variable/*!*/ v in lambda.Dummies) {

+            Contract.Assert(v != null);

+            selectArgs.Add(new IdentifierExpr(v.tok, v));

+          }

+          NAryExpr axcall = new NAryExpr(tok, fcall, axCallArgs);

+          axcall.Type = res.TypedIdent.Type;

+          axcall.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals);

+          NAryExpr select = Expr.Select(axcall, selectArgs);

+          select.Type = lambdaBody.Type;

+          List<Type/*!*/> selectTypeParamActuals = new List<Type/*!*/>();

+          List<TypeVariable> forallTypeVariables = new List<TypeVariable>();

+          foreach (TypeVariable/*!*/ tp in lambda.TypeParameters) {

+            Contract.Assert(tp != null);

+            selectTypeParamActuals.Add(tp);

+            forallTypeVariables.Add(tp);

+          }

+          forallTypeVariables.AddRange(freeTypeVars);

+          select.TypeParameters = SimpleTypeParamInstantiation.From(lambda.TypeParameters, selectTypeParamActuals);

+

+          Expr bb = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaBody);

+          NAryExpr body = Expr.Eq(select, bb);

+          body.Type = Type.Bool;

+          body.TypeParameters = SimpleTypeParamInstantiation.EMPTY;

+          Trigger trig = new Trigger(select.tok, true, new List<Expr> { select });

+

+          lambdaFunctions.Add(fn);

+          lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies,

+            Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaAttrs),

+            trig, body));

         }

-        forallTypeVariables.AddRange(freeTypeVars);

-        select.TypeParameters = SimpleTypeParamInstantiation.From(lambda.TypeParameters, selectTypeParamActuals);

-

-        Expr bb = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaBody);

-        NAryExpr body = Expr.Eq(select, bb);

-        body.Type = Type.Bool;

-        body.TypeParameters = SimpleTypeParamInstantiation.EMPTY;

-        Trigger trig = new Trigger(select.tok, true, new List<Expr> { select });

-        lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies,

-          Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaAttrs),

-          trig, body));

 

         NAryExpr call = new NAryExpr(tok, fcall, callArgs);

         call.Type = res.TypedIdent.Type;

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 05c4b44b..a9220a4c 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1066,7 +1066,7 @@ namespace Microsoft.Boogie
       {

         #region Verify the implementation

 

-        verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum, impl.Name, impl.tok, programId);

+        verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependencyChecksum, impl.Name, impl.tok, programId);

 

         using (var vcgen = CreateVCGen(program, checkers))

         {

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index b5f6d1cd..d44aff7f 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -197,7 +197,7 @@ namespace Microsoft.Boogie
       // TODO(wuestholz): Maybe we should speed up this lookup.

       var oldProc = programInCachedSnapshot.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == node.Proc.Name);

       if (oldProc != null

-          && oldProc.DependenciesChecksum != node.Proc.DependenciesChecksum

+          && oldProc.DependencyChecksum != node.Proc.DependencyChecksum

           && node.AssignedAssumptionVariable == null)

       {

         if (DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))

@@ -236,7 +236,7 @@ namespace Microsoft.Boogie
         }

         else

         {

-          node.EmitDependenciesChecksum = true;

+          node.EmitDependencyChecksum = true;

         }

       }

 

@@ -308,7 +308,7 @@ namespace Microsoft.Boogie
       // TODO(wuestholz): Maybe we should speed up this lookup.

       var funcs = newProg.TopLevelDeclarations.OfType<Function>();

       return oldProc.DependenciesCollected

-             && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependenciesChecksum == dep.DependenciesChecksum)));

+             && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)));

     }

 

     public override Procedure VisitProcedure(Procedure node)

@@ -437,7 +437,7 @@ namespace Microsoft.Boogie
       {

         priority = Priority.MEDIUM;

       }

-      else if (impl.DependenciesChecksum == null || result.DependeciesChecksum != impl.DependenciesChecksum)

+      else if (impl.DependencyChecksum == null || result.DependeciesChecksum != impl.DependencyChecksum)

       {

         priority = Priority.LOW;

       }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index d88d4667..fe40618e 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -112,6 +112,11 @@ namespace VC {
         return ret;

       }

     }

+

+    public override string ToString()

+    {

+        return info.impl.Name;

+    }

   }

 

   public class CallSite {

@@ -175,7 +180,13 @@ namespace VC {
         }

         scs.interfaceExprs = newInterfaceExprs;

       }

-      return gen.Implies(callSiteExpr, svc.vcexpr);

+      //return gen.Implies(callSiteExpr, svc.vcexpr);

+      return svc.vcexpr;

+    }

+

+    public override string ToString()

+    {

+        return callSite.calleeName;

     }

   }

 

@@ -404,7 +415,7 @@ namespace VC {
           i++;

           AssumeCmd callSiteAssumeCmd = (AssumeCmd)block.Cmds[i];

           IdentifierExpr iexpr = (IdentifierExpr) callSiteAssumeCmd.Expr;

-          CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, prover.Context.BoogieExprTranslator.LookupVariable(iexpr.Decl), block, instr, callSiteAssumeCmd.Attributes);

+          CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, prover.Context.BoogieExprTranslator.LookupVariable(iexpr.Decl), block, instr, assumeCmd.Attributes);

           if (!callSites.ContainsKey(block))

             callSites[block] = new List<CallSite>();

           callSites[block].Add(cs);

diff --git a/Test/test2/LambdaExt.bpl b/Test/test2/LambdaExt.bpl
new file mode 100644
index 00000000..be0d84ee
--- /dev/null
+++ b/Test/test2/LambdaExt.bpl
@@ -0,0 +1,146 @@
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure Simplest() {
+  var id1, id2 : [int]int;
+  id1 := (lambda x: int :: x);
+  id2 := (lambda x: int :: x);
+  assert id1 == id2;
+  id2 := (lambda x: int :: 0);
+  assert id1 == id2; // fail
+}
+
+procedure Const() {
+  var v, w : [int][int]int;
+  var f, g : [int, int]int;
+
+  v := (lambda x : int :: (lambda y : int :: x));
+
+  w := (lambda x : int :: (lambda i : int :: x));
+  assert v == w;
+
+  w := (lambda i : int :: (lambda y : int :: i));
+  assert v == w;
+
+  w := (lambda a : int :: (lambda b : int :: b));
+  assert v == w; // should fail, now two different functions
+
+  f := (lambda x : int, y : int :: x);
+  assert f == (lambda p : int, q : int :: p);
+  assert f == (lambda p : int, q : int :: q); // should fail, different functions
+}
+
+procedure PolyConst() {
+  assert (lambda<A> x: A :: x) == (lambda<A>x: A :: x); // fails because of type parameters. this could be fixed.
+  /* // more tests, when it is fixed
+  var k1 : <A1>[A1]<B1>[B1]A1;
+  var k2 : <A2>[A2]<B2>[B2]A2;
+  k1 := (lambda<A> x: A :: (lambda<B> y: B :: x));
+  k2 := (lambda<A> x: A :: (lambda<C> z: C :: x));
+  assert k1 == k2;
+  k2 := (lambda<X> u: X :: (lambda<Y> v: Y :: u));
+  assert k1 == k2;  */
+}
+
+procedure FreeVarP() {
+  var k : real;
+  var m : [int]real;
+  m := (lambda x:int :: k);
+  assert m[0] == k;
+}
+
+procedure FreeVarQ() {
+  var k : int;
+  var m : [int]int;
+  m := (lambda x:int :: k); // should be a different lambda from in FreeVarP, because they have different types
+  assert m[0] == k;
+}
+
+procedure Quantifiers() {
+  var k1 : [int]bool;
+  var k2 : [int]bool;
+  k1 := (lambda x: int :: (exists y: int :: x > y));
+  k2 := (lambda x: int :: (exists y: int :: x > y));
+  assert k1 == k2;
+  k2 := (lambda x: int :: (exists z: int :: x > z));
+  assert k1 == k2;
+}
+
+procedure FreeVariables() {
+  var m : [bool,bool,bool]bool;
+  var k : [bool,bool]bool;
+
+  var f : [bool]bool;
+  var g : [bool]bool;
+
+  var a : bool;
+  var b : bool;
+
+  f := (lambda r: bool :: a);
+  g := (lambda s: bool :: b);
+  if (a == b) {
+    assert f == g; // should be OK
+  } else {
+    assert f == g; // should fail
+  }
+
+  f := (lambda r: bool :: k[a,b]);
+  g := (lambda s: bool :: k[b,a]);
+  if (a == b) {
+    assert f == g; // should be OK
+  } else {
+    assert f == g; // should fail
+  }
+
+  f := (lambda r: bool :: m[a,a,b]);
+  g := (lambda s: bool :: m[a,b,b]);
+  if (a == b) {
+    assert f == g; // should fail because they are different lambda
+  } else {
+    assert f == g; // should fail because they are different lambda
+  }
+}
+
+function f(int) : int;
+
+procedure Triggers() {
+  var a,b : [int]bool;
+  a := (lambda x:int :: (forall u:int :: { f(u) } x == f(u)));
+  b := (lambda y:int :: (forall v:int :: { f(v) } y == f(v)));
+  assert a == b;
+  b := (lambda y:int :: (forall v:int :: y == f(v)));
+  assert a == b; // should fail because triggers are different
+}
+
+procedure Attributes() {
+  var a,b : [int]bool;
+  a := (lambda x:int :: (forall u:int :: {:attrib f(u) } x == f(u)));
+  b := (lambda y:int :: (forall v:int :: {:attrib f(v) } y == f(v)));
+  assert a == b;
+  b := (lambda y:int :: (forall v:int :: {:battrib f(v) } y == f(v)));
+  assert a == b; // should fail since attributes are different
+  a := (lambda x:int :: (forall u:int :: {:battrib f(x) } x == f(u)));
+  assert a == b; // should fail since attributes are different
+}
+
+procedure Old() {
+  var u,v : [int]int;
+  var a,b : int;
+  u := (lambda x:int :: old(x+a));
+  v := (lambda y:int :: old(y+b));
+  if (a == b) {
+    assert u == v; // ok
+  } else {
+    assert u == v; // fails
+  }
+}
+
+type Box;
+function $Box<T>(T) : Box;
+function $Unbox<T>(Box) : T;
+
+procedure Coercion() {
+  assert (lambda x: Box :: $Box($Unbox(x): int))
+      == (lambda y: Box :: $Box($Unbox(y): int));
+}
+
diff --git a/Test/test2/LambdaExt.bpl.expect b/Test/test2/LambdaExt.bpl.expect
new file mode 100644
index 00000000..fac42eb2
--- /dev/null
+++ b/Test/test2/LambdaExt.bpl.expect
@@ -0,0 +1,56 @@
+LambdaExt.bpl(10,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(6,7): anon0
+LambdaExt.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(17,5): anon0
+LambdaExt.bpl(30,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(17,5): anon0
+LambdaExt.bpl(34,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(34,3): anon0
+LambdaExt.bpl(84,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(79,5): anon0
+    LambdaExt.bpl(84,5): anon9_Else
+LambdaExt.bpl(92,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(79,5): anon0
+    LambdaExt.bpl(84,5): anon9_Else
+    LambdaExt.bpl(87,5): anon3
+    LambdaExt.bpl(92,5): anon10_Else
+LambdaExt.bpl(98,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(79,5): anon0
+    LambdaExt.bpl(82,5): anon9_Then
+    LambdaExt.bpl(87,5): anon3
+    LambdaExt.bpl(90,5): anon10_Then
+    LambdaExt.bpl(95,5): anon6
+    LambdaExt.bpl(98,5): anon11_Then
+LambdaExt.bpl(100,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(79,5): anon0
+    LambdaExt.bpl(84,5): anon9_Else
+    LambdaExt.bpl(87,5): anon3
+    LambdaExt.bpl(92,5): anon10_Else
+    LambdaExt.bpl(95,5): anon6
+    LambdaExt.bpl(100,5): anon11_Else
+LambdaExt.bpl(112,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(108,5): anon0
+LambdaExt.bpl(119,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(117,5): anon0
+LambdaExt.bpl(121,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(117,5): anon0
+LambdaExt.bpl(123,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(117,5): anon0
+LambdaExt.bpl(134,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(129,5): anon0
+    LambdaExt.bpl(134,5): anon3_Else
+
+Boogie program verifier finished with 4 verified, 13 errors