In some cases, SMT verification of selectors VCs requires the global selector in the context. For instance: https://github.com/FStarLang/FStar/blob/c751ed5db01a24c13e334bab2c5762389a34791b/examples/steel/Selectors.LList.Derived.fst#L11
The most probable cause is that refinements on the types of selectors prevent SMT triggering.
We need to look in detail at generated SMT queries.
In the meantime, a workaround is to add let h = get ... at different points of the program (usually mostly at the very beginning) when SMT verification fails.
In some cases, SMT verification of selectors VCs requires the global selector in the context. For instance: https://github.com/FStarLang/FStar/blob/c751ed5db01a24c13e334bab2c5762389a34791b/examples/steel/Selectors.LList.Derived.fst#L11
The most probable cause is that refinements on the types of selectors prevent SMT triggering.
We need to look in detail at generated SMT queries.
In the meantime, a workaround is to add
let h = get ...at different points of the program (usually mostly at the very beginning) when SMT verification fails.