Description
KeY is weak on nested ∀∃ quantifications and cannot proof simple statements that cvc5 and z3 can do in .01 s.
Reproducible
a.length = i_0,
\forall int u; (u < v_0 & u >= 0 -> \exists int j; (j < i_0 & j >= 0 & u = a[j]))
==>
\forall int u;
(u >= 0 & u < v_0 -> \exists int j; ((j >= 0 & j < a.length & u = a[j])<<SC>>))
is a MVE sequent that cannot be closed by KeY's automation. It can be closed by manual interaction and by SMT solvers.
Steps to reproduce
The above example can be encoded into a KeY file. User interaction is just skolemisation of u and then obvious instantiation.
Additional information
The automation somehow gets stuck and does not instantiate the LHS ∀u with the skolem obtained from the RHS ∀u. The trigger mechanism seems incomplete here.
This is not a soudness issue, but a completeness issue.
Description
KeY is weak on nested
∀∃quantifications and cannot proof simple statements that cvc5 and z3 can do in .01 s.Reproducible
is a MVE sequent that cannot be closed by KeY's automation. It can be closed by manual interaction and by SMT solvers.
Steps to reproduce
The above example can be encoded into a KeY file. User interaction is just skolemisation of u and then obvious instantiation.
Additional information
The automation somehow gets stuck and does not instantiate the LHS ∀u with the skolem obtained from the RHS ∀u. The trigger mechanism seems incomplete here.
This is not a soudness issue, but a completeness issue.