Ltac floyd.client_lemmas.check_mpreds2 fails at level 10, which has the result that try entailer! fails when it should simply do nothing.
It might be better to fail at level 4, which is just enough to make entailer! fail at level 0.
A similar issue might apply to floyd.go_lower.check_mpreds, which also fails at level 10, but I don't have a particular suggestion about what's the right failure level for that one.
This issue arises when using dependent funspecs, where indeed we get something that's convertible with mpred but not constr_eq-identical to mpred. See also, VST.lib.verif_SC_atomics (which is currently only in the lib branch of VST).
Ltac floyd.client_lemmas.check_mpreds2 fails at level 10, which has the result that
try entailer!fails when it should simply do nothing.It might be better to fail at level 4, which is just enough to make
entailer!fail at level 0.A similar issue might apply to floyd.go_lower.check_mpreds, which also fails at level 10, but I don't have a particular suggestion about what's the right failure level for that one.
This issue arises when using dependent funspecs, where indeed we get something that's convertible with mpred but not constr_eq-identical to mpred. See also, VST.lib.verif_SC_atomics (which is currently only in the lib branch of VST).