Establishing witnesses for trivial predicates takes RU

[stefan-aws]

Dafny version

4.0.0

Code to produce this issue

predicate P<X>(s: seq<X>) {
  true
}

predicate Q<X,Y>(m: map<X,Y>) {
  true
}

type S<X> = s: seq<X> | P(s) witness []

type M<X,Y> = m: map<X,Y> | Q(m) witness map[]

Command to run and resulting output

No response

What happened?

Establishing that the empty sequence and the empty map satisfy the trivial predicates above still takes 57K RU each. Question: can we reduce that number (for above predicates, and generally, also for slightly more involved ones)?

What type of operating system are you experiencing the problem on?

Mac