FwdChecker: Avoid re-checking locals because of global dependencies

[michael-schwarz]

Summary

Avoid evaluating the same local RHS multiple times during post-solution checking.

The worklist set previously tracked only queued locals. Once processed, a local was removed and could later be scheduled again through a global's influence set, causing redundant transfer-function evaluations.

Neither output map prevents this:

• tau_out deduplicates globals, but a global's first encounter can still schedule already-processed locals.
• sigma_out only deduplicates locals discovered through local side effects. Start unknowns and global influences call add_work directly, while checking it inside add_work would suppress first-time evaluations because check_local updates sigma_out before scheduling.

This change keeps scheduled locals in the worklist set after dequeuing, making it a record of all locals seen during the current checker run. The set is reset between checker invocations.

On an example originating from our witness-validation work, this reduced postsolver runtime from several minutes to about 45 seconds.

[michael-schwarz]

After discussion with Helmut, it seems that perhaps checking for a global should not enqueue any locals at all?