The reason is the conjunctions of several problems:
Type invariants are expressed in terms of axioms with a quantifier instead of a definition
Why3 decides to encode these algebraic types with FOL, to support polymorphism. The reason for this is not clear, but may be related to the fact that we are using polymorphic logical functions for record projections, while it seems we could use native projections.
Why3 tries to be smart by replacing the pattern matching in these axioms with other quantifiers.
The end result is that, instead of just unfolding a definition, SMT solvers have to instantiate several quantifiers, and have a hard time with that.
Hence, there are many possible solutions for this problem:
Have monomorphic clone-based translation of algebraic types
Do not generate code for record projections, but instead use native ones
Do not use axioms (this would also fix #879, btw), but rather support mutually inductive definitions
The reason is the conjunctions of several problems:
The end result is that, instead of just unfolding a definition, SMT solvers have to instantiate several quantifiers, and have a hard time with that.
Hence, there are many possible solutions for this problem: