Exploit the accessors for ADTs in SMTLIB
The ADTs in SMTLIB allow the declaration of accessors. WhyML allows it too, with a syntax like
type list 'a = Nil | Cons (hd : 'a) (tl : list 'a)
The above is not accepted by Why3 though, because an accessor must occur in all constructor (i.e. with the same name and type).
Allowing partially defined accessors in WhyML would opne the possibility to exploit SMTLIB accessors as well.
The problem though is how to interpret accessors in solvers where they are not supported. A declaration like
function hd : list 'a -> 'a
axiom hd_spec : forall x y. hd (Cons x y) = x
seems dangerous because hd Nil
may be interpreted differently by provers (clarification needed)