SMT solvers have a hard time unfolding type invariants

[jhjourdan]

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 Recursive definitions and invariant #879, btw), but rather support mutually inductive definitions