Printer for SMTv2 is broken when using projections of sum types in a non-polymorphic context
Why3 script:
type t =
| A (x : unit)
| B (x : unit)
goal g: forall x:t. x = x
When using CVC4, CVC4 complains:
(error "Parse Error: x already declared in this datatype")
And indeed, the generated SMTLIB type declaration is:
(declare-datatypes ((t 0))
(((A (x tuple0)) (B (x tuple0)))))
The problem is that the printer for SMTLIB considers that Why3 projections (well-defined, projection has to be repeated in every constructor) have the same semantics than in SMTLIB (defined only if passed the right constructor, projection needs to be unique in the whole SMTLIB type declaration).
This issue does not occur when
- the goal is polymorphic, because algebraic types are eliminated
- using records, because there is only one constructor.
Also, the FIXME comment here is related.