ICanVerify is more general + Forward-compatibility for {:fuel} on Ass…

…ertStmt
dafny-lang · Oct 18, 2024 · 0e988bc · 0e988bc
1 parent 4958d39
commit 0e988bc
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs
@@ -367,9 +367,9 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
  .WithArg("low", Type.Int, DefaultInt(1))
  .WithArg("high", Type.Int, DefaultInt(2))
  .WithArg("functionName", Type.ResolvedString(), DefaultString(""))
- .Filter(attributeHost => attributeHost is Function),
+ .Filter(attributeHost => attributeHost is Function or AssertStmt),
  BuiltIn("IsolateAssertions")
- .Filter(attributeHost => attributeHost is MemberDecl or DatatypeDecl or RedirectingTypeDecl),
+ .Filter(attributeHost => attributeHost is ICanVerify),
  BuiltIn("Options")
  .WithArg(TupleItem0Name, Type.ResolvedString())
  .Filter(attributeHost => attributeHost is ModuleDecl or ModuleDefinition),