quantifier instance and datatype theory

[clairedross]

Hi Z3 experts,

when trying to prove a SPARK program, we came across a seemingly simple VC that both CVC4 and Z3 could not prove (but Alt-Ergo can). It involves a single instance of a universally quantified formula. Unfortunately, Z3 does not seem to be able to come up with the correct instance, as it returns unknown almost at once. I suspect this is caused by a bad interaction between quantifier instantiation heuristics and datatype theory reasoning. Do you have any advice of how we could manage to prove this kind of code?

unproved.txt

Thanks in advance,
Claire