Can call merge [Ignore]

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -156,15 +156,41 @@ public virtual IEnumerable<Type> ComponentTypes {
 
   public virtual bool IsImplicit => false;
 
+  public static IEnumerable<Expression> ConjunctsWithLetsOnOutside(Expression expr) {
+    foreach (var conjunct in Conjuncts(expr)) {
+      if (conjunct is LetExpr { Exact: true } letExpr) {
+        foreach (var letBodyConjunct in ConjunctsWithLetsOnOutside(letExpr.Body)) {
+          yield return new LetExpr(letExpr.tok, letExpr.LHSs, letExpr.RHSs, letBodyConjunct, letExpr.Exact, letExpr.Attributes) {
+            Type = letExpr.Type
+          };
+        }
+      } else {
+        yield return conjunct;
+      }
+    }
+  }
+
+  /// <summary>
+  /// Return the negation of each of the expressions in "expressions".
+  /// If there is just one expression in "expressions", then use the given token "tok" for the negation.
+  /// Otherwise, use the token from each expression.
+  /// </summary>
+  static IEnumerable<Expression> NegateEach(IOrigin tok, IEnumerable<Expression> expressions) {
+    var exprs = expressions.ToList();
+    foreach (Expression e in exprs) {
+      yield return Expression.CreateNot(exprs.Count == 1 ? tok : e.tok, e);
+    }
+  }
+
   public static IEnumerable<Expression> Conjuncts(Expression expr) {
     Contract.Requires(expr != null);
     Contract.Requires(expr.Type.IsBoolType);
     Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));
 
     expr = StripParens(expr);
-    if (expr is UnaryOpExpr unary && unary.Op == UnaryOpExpr.Opcode.Not) {
-      foreach (Expression e in Disjuncts(unary.E)) {
-        yield return Expression.CreateNot(e.Tok, e);
+    if (expr is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Not } unary) {
+      foreach (Expression e in NegateEach(expr.Tok, Disjuncts(unary.E))) {
+        yield return e;
       }
       yield break;
 
@@ -189,26 +215,26 @@ public static IEnumerable<Expression> Disjuncts(Expression expr) {
     Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));
 
     expr = StripParens(expr);
-    if (expr is UnaryOpExpr unary && unary.Op == UnaryOpExpr.Opcode.Not) {
-      foreach (Expression e in Conjuncts(unary.E)) {
-        yield return Expression.CreateNot(e.Tok, e);
+    if (expr is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Not } unary) {
+      foreach (Expression e in NegateEach(expr.Tok, Conjuncts(unary.E))) {
+        yield return e;
       }
       yield break;
 
     } else if (expr is BinaryExpr bin) {
       if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {
-        foreach (Expression e in Conjuncts(bin.E0)) {
+        foreach (Expression e in Disjuncts(bin.E0)) {
           yield return e;
         }
-        foreach (Expression e in Conjuncts(bin.E1)) {
+        foreach (Expression e in Disjuncts(bin.E1)) {
           yield return e;
         }
         yield break;
       } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
         foreach (Expression e in Conjuncts(bin.E0)) {
           yield return Expression.CreateNot(e.Tok, e);
         }
-        foreach (Expression e in Conjuncts(bin.E1)) {
+        foreach (Expression e in Disjuncts(bin.E1)) {
           yield return e;
         }
         yield break;

Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs

@@ -73,7 +73,7 @@ public DafnyModel(Model model, DafnyOptions options) {
       fMapEmpty = new ModelFuncWrapper(this, "Map#Empty", 0, 0);
       fIs = new ModelFuncWrapper(this, "$Is", 2, tyArgMultiplier);
       fIsBox = new ModelFuncWrapper(this, "$IsBox", 2, 0);
-      fBox = new ModelFuncWrapper(this, "$Box", 1, tyArgMultiplier);
+      fBox = new ModelFuncWrapper(this, BoogieGenerator.BoxFunctionName, 1, tyArgMultiplier);
       fDim = new ModelFuncWrapper(this, "FDim", 1, 0);
       fIndexField = new ModelFuncWrapper(this, "IndexField", 1, 0);
       fMultiIndexField = new ModelFuncWrapper(this, "MultiIndexField", 2, 0);
@@ -85,7 +85,7 @@ public DafnyModel(Model model, DafnyOptions options) {
       fU2Int = new ModelFuncWrapper(this, "U_2_int", 1, 0);
       fTag = new ModelFuncWrapper(this, "Tag", 1, 0);
       fBv = new ModelFuncWrapper(this, "TBitvector", 1, 0);
-      fUnbox = new ModelFuncWrapper(this, "$Unbox", 2, 0);
+      fUnbox = new ModelFuncWrapper(this, BoogieGenerator.UnboxFunctionName, 2, 0);
       fLs = new ModelFuncWrapper(this, "$LS", 1, 0);
       fLz = new ModelFuncWrapper(this, "$LZ", 0, 0);
       InitDataTypes();

Source/DafnyCore/Rewriters/InductionHeuristic.cs

@@ -178,4 +178,4 @@ expr is BoxingCastExpr ||
       return false;
     }
   }
-}
+}

Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs

@@ -171,7 +171,8 @@ string InfoFirstLineEnd(int count) {
       messages.Add($"Part #{splitPartIndex} is '{Comprehension.Term}'");
     }
     if (Candidates.Any()) {
-      messages.Add($"Selected triggers:{InfoFirstLineEnd(Candidates.Count)}{string.Join(", ", Candidates)}");
+      var subst = Util.Comma("", NamedExpressions, pair => $" where {pair.Item2} := {pair.Item1}");
+      messages.Add($"Selected triggers:{InfoFirstLineEnd(Candidates.Count)}{string.Join(", ", Candidates)}{subst}");
     }
     if (RejectedCandidates.Any()) {
       messages.Add($"Rejected triggers:{InfoFirstLineEnd(RejectedCandidates.Count)}{string.Join("\n  ", RejectedCandidates)}");

Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs

@@ -155,6 +155,9 @@ enum BuiltinFunction {
       AtLayer
     }
 
+    public const string BoxFunctionName = "$Box";
+    public const string UnboxFunctionName = "$Unbox";
+
     Bpl.Expr Lit(Bpl.Expr expr, Bpl.Type typ) {
       Contract.Requires(expr != null);
       Contract.Requires(typ != null);
@@ -506,11 +509,11 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan
         case BuiltinFunction.Box:
           Contract.Assert(args.Length == 1);
           Contract.Assert(typeInstantiation == null);
-          return FunctionCall(tok, "$Box", Predef.BoxType, args);
+          return FunctionCall(tok, BoxFunctionName, Predef.BoxType, args);
         case BuiltinFunction.Unbox:
           Contract.Assert(args.Length == 1);
           Contract.Assert(typeInstantiation != null);
-          return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "$Unbox", typeInstantiation, args), typeInstantiation);
+          return Bpl.Expr.CoerceType(tok, FunctionCall(tok, UnboxFunctionName, typeInstantiation, args), typeInstantiation);
 
         case BuiltinFunction.RealToInt:
           Contract.Assume(args.Length == 1);