[dataflow] improve determinism of generated SAT system

Fixes two places where we relied on map iteration order when processing
values, which leaked nondeterminism into the generated SAT formulas.
Adds a couple of tests that directly assert that the SAT system is
equivalent on each run.

It's desirable that the formulas are deterministic based on the input:

 - our SAT solver is naive and perfermance is sensitive to even simple
   semantics-preserving transformations like A|B to B|A.
   (e.g. it's likely to choose a different variable to split on).
   Timeout failures are bad, but *flaky* ones are terrible to debug.
 - similarly when debugging, it's important to have a consistent
   understanding of what e.g. "V23" means across runs.

---

Both changes in this patch were isolated from a nullability analysis of
real-world code which was extremely slow, spending ages in the SAT
solver at "random" points that varied on each run.
I've included a reduced version of the code as a regression test.

One of the changes shows up directly as flow-condition nondeterminism
with a no-op analysis, the other relied on bits of the nullability
analysis but I found a synthetic example to show the problem.

Differential Revision: https://reviews.llvm.org/D154948