Add some diversity to Dafny's alimentation

1 files changed, 4 insertions, 4 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 8200f254..6f1a5833 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2261,9 +2261,9 @@ namespace Microsoft.Dafny {
 

       Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new List<Bpl.Expr> { funcAppl });

       var typeParams = TrTypeParamDecls(f.TypeArgs);

-      Bpl.Expr meat;

+      Bpl.Expr tastyVegetarianOption;

       if (visibility == FunctionAxiomVisibility.ForeignModuleOnly && f.IsProtected) {

-        meat = Bpl.Expr.True;

+        tastyVegetarianOption = Bpl.Expr.True;

       } else {

         var bodyWithSubst = Substitute(body, null, substMap);

         if (f is PrefixPredicate) {

@@ -2271,14 +2271,14 @@ namespace Microsoft.Dafny {
           bodyWithSubst = PrefixSubstitution(pp, bodyWithSubst);

         }

         var etranBody = layer == null ? etran : etran.LimitedFunctions(f, new Bpl.IdentifierExpr(f.tok, layer));

-        meat = BplAnd(CanCallAssumption(bodyWithSubst, etranBody),

+        tastyVegetarianOption = BplAnd(CanCallAssumption(bodyWithSubst, etranBody),

           Bpl.Expr.Eq(funcAppl, etranBody.TrExpr(bodyWithSubst)));

       }

       QKeyValue kv = null;

       if (lits != null) {

         kv = new QKeyValue(f.tok, "weight", new List<object>() { Bpl.Expr.Literal(3) }, null);

       }

-      Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, kv, tr, Bpl.Expr.Imp(ante, meat));

+      Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, kv, tr, Bpl.Expr.Imp(ante, tastyVegetarianOption));

       var activate = AxiomActivation(f, visibility == FunctionAxiomVisibility.ForeignModuleOnly, visibility == FunctionAxiomVisibility.IntraModuleOnly, etran);

       string comment;

       if (overridingClass == null) {