From a6bbbf1ad9ec298ab08e9a50826c755d3a3140c4 Mon Sep 17 00:00:00 2001 From: zafer-esen Date: Mon, 7 Aug 2023 18:55:45 -0400 Subject: [PATCH] Fix: incorrect pruning of axiom with monomorhphization. (#4396) An axiom in DafnyPrelude was incorrectly being pruned away with the `monomorphic` type encoding, because it was losing its (polymorphic) quantifier and trigger. This meant automatic edge inference from triggers was no longer applicable. Moved the axiom in question into a uses clause to prevent it from being pruned. The change has no affect on other type encodings `arguments` (current default) and `predicates`. There is more discussion related to the fix here in [Boogie PR 767](https://github.com/boogie-org/boogie/pull/767). By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyCore/DafnyPrelude.bpl | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/DafnyPrelude.bpl b/Source/DafnyCore/DafnyPrelude.bpl index 579eede1e33..ef3d567612d 100644 --- a/Source/DafnyCore/DafnyPrelude.bpl +++ b/Source/DafnyCore/DafnyPrelude.bpl @@ -967,8 +967,9 @@ type Seq T; function Seq#Length(Seq T): int; axiom (forall s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s)); -function Seq#Empty(): Seq T; -axiom (forall :: { Seq#Empty(): Seq T } Seq#Length(Seq#Empty(): Seq T) == 0); +function Seq#Empty(): Seq T uses { + axiom (forall :: { Seq#Empty(): Seq T } Seq#Length(Seq#Empty(): Seq T) == 0); +} axiom (forall s: Seq T :: { Seq#Length(s) } (Seq#Length(s) == 0 ==> s == Seq#Empty()) // The following would be a nice fact to include, because it would enable verifying the