fix: Visit let-expression components consistently

Previously, the Rhss and Body are a let expression where visited in different orders in
different parts of Boogie. They are now visited consistently, always Rhss before Body.

Fixes #192

Author: RustanLeino

Source/Core/AbsyQuant.cs

@@ -1119,11 +1119,16 @@ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bo
     public override void ComputeFreeVariables(Set freeVars) {
       //Contract.Requires(freeVars != null);
 
+      foreach (var e in Rhss) {
+        e.ComputeFreeVariables(freeVars);
+      }
       foreach (var v in Dummies) {
         Contract.Assert(v != null);
         Contract.Assert(!freeVars[v]);
       }
-      Body.ComputeFreeVariables(freeVars);
+      foreach (var v in Dummies) {
+        freeVars.AddRange(v.TypedIdent.Type.FreeVariables);
+      }
       for (var a = Attributes; a != null; a = a.Next) {
         foreach (var o in a.Params) {
           var e = o as Expr;
@@ -1132,13 +1137,8 @@ public override void ComputeFreeVariables(Set freeVars) {
           }
         }
       }
-      foreach (var v in Dummies) {
-        freeVars.AddRange(v.TypedIdent.Type.FreeVariables);
-      }
+      Body.ComputeFreeVariables(freeVars);
       freeVars.RemoveRange(Dummies);
-      foreach (var e in Rhss) {
-        e.ComputeFreeVariables(freeVars);
-      }
     }
   }
 }

Source/Core/MaxHolesLambdaLifter.cs

@@ -131,8 +131,7 @@ public override Expr VisitLetExpr(LetExpr node) {
 
             replacements.AddRange(bodyTemplate.GetReplacements());
             _templates[node] = new TemplateWithBoundVariables(replacements);
-        }
-        else {
+        } else {
             var newRhss = from arg in varBodies select ((TemplateNoBoundVariables) _templates[arg]).GetReplacement();
             LambdaLiftingTemplate template = new TemplateNoBoundVariables(
                 new LetExpr(node.tok, node.Dummies, newRhss.ToList(),

Source/Core/StandardVisitor.cs

@@ -311,9 +311,9 @@ public virtual Expr VisitLambdaExpr(LambdaExpr node) {
     public virtual Expr VisitLetExpr(LetExpr node) {
       Contract.Requires(node != null);
       Contract.Ensures(Contract.Result<Expr>() != null);
-      node.Body = this.VisitExpr(node.Body);
-      node.Dummies = this.VisitVariableSeq(node.Dummies);
       node.Rhss = this.VisitExprSeq(node.Rhss);
+      node.Dummies = this.VisitVariableSeq(node.Dummies);
+      node.Body = this.VisitExpr(node.Body);
       return node;
     }
     public virtual Formal VisitFormal(Formal node) {
@@ -878,9 +878,9 @@ public override Expr VisitLambdaExpr(LambdaExpr node) {
           return this.VisitBinderExpr(node);
       }
       public override Expr VisitLetExpr(LetExpr node) {
-          this.VisitExpr(node.Body);
-          this.VisitVariableSeq(node.Dummies);
           this.VisitExprSeq(node.Rhss);
+          this.VisitVariableSeq(node.Dummies);
+          this.VisitExpr(node.Body);
           return node;
       }
       public override Formal VisitFormal(Formal node)

Test/letexpr/git-issue-192.bpl

@@ -0,0 +1,24 @@
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type AAA;
+type BBB;
+type CCC;
+
+function Apple(AAA, BBB): CCC;
+function Banana(int): BBB;
+
+procedure Proc()
+{
+  var m: [AAA]CCC;
+  m :=
+      // Once upon a time, the lambda lifting for the following body switched
+      // the roles of 15 and Banana(700), by traversing the components of let
+      // expressions in a different order when figuring out holes from when
+      // replacing the holes with new bound variables of the lambda lifting.
+      (lambda aaa: AAA :: 
+          (var g := 15;
+             Apple(aaa, Banana(700))
+          )
+      );
+}

Test/letexpr/git-issue-192.bpl.expect

@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors