Take the state at a join as the disjunction of the states behind it

[coord-e]

Last of three, on top of #227 (which is on top of #226). Each removes one predicate variable that stood for a fact the constraints already state elsewhere.

A block reached by more than one edge took a template inferred from a clause per incoming edge. The states its predecessors leave say exactly what it is entered in, so their disjunction is its precondition, and only a loop header still has one to infer: the state carried by its back edge is not yet known when it is analyzed. needs_own_precondition becomes is_loop_header accordingly.

A disjunction is no conjunct of a Horn clause body, so this holds only as long as no predicate variable appears in the states. Where one does, the disjunction is named by a predicate variable of its own, bounded from below by each state — which is what the block had all along. Body::into_formula decides which of the two applies.

The states are collected as the predecessors are analyzed and installed once they all have been, so a block that inherits its precondition holds the states until then rather than a flag.

Effect

Over tests/ui/pass (160 files):

	predicate variables	constraints
main	1691	—
after #226	1293	1088 KiB
after #227	734	917 KiB
after this	676	832 KiB

The path explosion this invites did not show up: the constraints came out 9% smaller, since naming a state costs an argument list at every use, which the disjunction rarely exceeds. Worst case loop_invariant_multi.rs at 1.23x (2.4 KiB to 2.9 KiB), best result_mut.rs at 0.35x (59 KiB to 21 KiB).

With all three, a predicate variable is generated only where something is genuinely unknown: the type of a function without an annotation, and a loop header without an invariant!. A fully annotated program with no loop generates constraints with none at all — an annotated fn abs(x: i64) -> i64 { if x >= 0 { x } else { -x } } comes out as a plain SMT problem and verifies.

Notes for review

• Nothing pins the counts above. The generated constraints changing shape is invisible to the ui tests: while writing this I had Refinement::disjunction demand a predicate-variable-free form even for a single state, which quietly put a predicate variable back on every block that inherits, and all 316 tests still passed. A unit test over Refinement::disjunction would cover the case that broke; happy to add one.
• is_loop_header reads a back edge off the dominator tree, which answers the question asked (is some predecessor analyzed after this block?) only for a reducible CFG. An irreducible one does not go unnoticed: the state arrives after the precondition is installed, and push_basic_block_precondition panics.
• Hoisting the existential variables of every disjunct in front of the disjunction is valid as long as every sort is inhabited.

316 tests pass.