Verus choose more triggers than wanted

[ahuoguo]

use vstd::prelude::*;

verus! {

uninterp spec fn f(x: int, y: int) -> bool;
uninterp spec fn g(x: int, y: int) -> bool;
uninterp spec fn h(x: int, y: int) -> bool;

proof fn hi() 
    ensures forall |x: int, y: int, z: int| f(x, y) && g(y, z) && h(x, z)
{
    assume(false);
}

}
fn main(){}

Run verus example.rs --triggers and it reports

> verus hi.rs --triggers
note: automatically chose triggers for this expression:
  --> hi.rs:10:13
   |
10 | ...es forall |x: int, y: int, z: int| f(x, y) && g(y, z) && h(x, z)
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

note:   trigger 1 of 4:
  --> hi.rs:10:45
   |
10 |     ensures forall |x: int, y: int, z: int| f(x, y) && g(y, z) &&...
   |                                             ^^^^^^^    ^^^^^^^

note:   trigger 2 of 4:
  --> hi.rs:10:45
   |
10 |     ensures forall |x: int, y: int, z: int| f(x, y) && g(y, z) &&...
   |                                             ^^^^^^^    ^^^^^^^

note:   trigger 3 of 4:
  --> hi.rs:10:45
   |
10 | ...y: int, z: int| f(x, y) && g(y, z) && h(x, z)
   |                    ^^^^^^^               ^^^^^^^

note:   trigger 4 of 4:
  --> hi.rs:10:56
   |
10 | ...t, z: int| f(x, y) && g(y, z) && h(x, z)
   |                          ^^^^^^^    ^^^^^^^

note:   trigger 2 of 4:
  --> hi.rs:10:45
   |
10 | ...y: int, z: int| f(x, y) && g(y, z) && h(x, z)
   |                    ^^^^^^^               ^^^^^^^

note:   trigger 3 of 4:
  --> hi.rs:10:56
   |
10 | ...t, z: int| f(x, y) && g(y, z) && h(x, z)
   |                          ^^^^^^^    ^^^^^^^

verification results:: 1 verified, 0 errors

There are 2 problems with the output: (1) trigger 1 and trigger 2 are the same; (2) trigger 2 and trigger 3 are printed twice (this behavior is not quite consistent among multiple runs...)

IIRC, Verus’s automatic trigger selection only chooses one valid trigger?

The #![all_triggers] implementation is correct tho...