Tentative fix for invalid rewrite of negated BDD in map_update_put_domains

[lukaszsamson]

Opening as draft

First cond case handles pure positive disjunction where bdd_map is exact. Second handles noop put when force? = false and put domain is not in any of the leaves). Third one handles everything else by over approximating (applying put to positive DNF and dropping the negations). This is a compromise that widens the result set. A precise version would require a bigger change (computing the image of difference)

Branch 3 converts to DNF and rebuilds via map_union. Branches 1 and 2 add two traversals

Assisted-by: Claude Opus 4.8 & GPT 5.5

Fixes #15509