Bugfix: form_read track Fglob like Fpvar

[Gustavo2622]

Logic for dealing with Fglob in form_read was missing, causing the resulting set to miss reads.
Adds logic for this similar to logic for dealing with Fpvars + a regression test exercised via proc change + sim

[fdupress]

From the description only, this feels like it should be flagged as a potentially breaking change. However, it doesn't break any of our external CI proofs.

Is this change only affecting new tactics not yet exercised by external proofs? Or is it not actually breaking? (This is only for purpose of release notes, not a review.)

[alleystoughton]

From the description only, this feels like it should be flagged as a potentially breaking change. However, it doesn't break any of our external CI proofs.

Is this change only affecting new tactics not yet exercised by external proofs? Or is it not actually breaking? (This is only for purpose of release notes, not a review.)

FWIW it didn't break any of my developments, either. (The description made me worry.)

[strub]

@Gustavo2622 Why this PR is a draft?

[Gustavo2622]

I made this a draft because it was extracted from a separate development and I wanted to make sure nothing broke when porting it (the development was not up to date with main when I extracted it, I've rebased and tested on main since).
It is possibly a breaking change but only for cases where it might otherwise be unsound-ish (under-approximating reads).