use zero fuel in triggers

dafny-lang · Feb 24, 2025 · 388cf6b · 388cf6b
1 parent cca1c96
commit 388cf6b
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
@@ -214,6 +214,11 @@ public ExpressionTranslator WithNoLits() {
         return CloneExpressionTranslator(this, BoogieGenerator, Predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, true);
       }
 
+      public ExpressionTranslator WithZeroFuel() {
+        Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
+        return CloneExpressionTranslator(this, BoogieGenerator, Predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(BoogieGenerator, 0), layerIntraCluster, readsFrame, modifiesFrame, true);
+      }
+
       public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFunction, Boogie.Expr layerArgument) {
         Contract.Requires(applyLimited_CurrentFunction != null);
         Contract.Requires(layerArgument != null);

diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs
@@ -4527,7 +4527,7 @@ List<SplitExprInfo> TrSplitExprForMethodSpec(BodyTranslationContext context, Exp
     Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IOrigin tok, Dictionary<IVariable, Expression> substMap = null) {
       Contract.Requires(etran != null);
       Contract.Requires(tok != null);
-      var argsEtran = etran.WithNoLits();
+      var argsEtran = etran.WithNoLits().WithZeroFuel();
       Bpl.Trigger tr = null;
       foreach (var trigger in attribs.AsEnumerable().Where(aa => aa.Name == "trigger").Select(aa => aa.Args)) {
         List<Bpl.Expr> tt = [];
@@ -4548,7 +4548,7 @@ Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IOrigin to
     Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IOrigin tok, List<Variable> bvars, Dictionary<IVariable, Expression> substMap, Dictionary<TypeParameter, Type> typeMap) {
       Contract.Requires(etran != null);
       Contract.Requires(tok != null);
-      var argsEtran = etran.WithNoLits();
+      var argsEtran = etran.WithNoLits().WithZeroFuel();
       Bpl.Trigger tr = null;
       var fueledTrigger = new Dictionary<List<Expression>, bool>();
       // translate the triggers once to see if fuel or the heap is used as quantifier boundvar