mcsat: fall back to model cache when target cache value is infeasible

[ahmed-irfan]

When deciding a value, the feasibility-aware plugins (na, ff, bv, uf) used a single cached hint (target cache preferred, else model cache). If that value was infeasible they went straight to a fresh pick, discarding the model cache's saved phase.

Try both cached tiers in priority order instead: tier 1 (target cache), then tier 2 (model cache), each checked against the variable's feasible set, before falling back to a fresh pick. The new behavior only fires when the target value is present but infeasible and the model value is present, feasible, and different - every other path is unchanged.

Add trail_get_cached_candidates() to own the priority ordering, NULL-stripping, and dedup (skip tier 2 when identical to tier 1) in one place; each plugin's decide path is now a plain loop over the returned candidates with only its own feasibility predicate. bool_plugin keeps the original combined getter (it has no feasible set).

Also fix a latent copy-paste assert in mcsat_value_eq (VALUE_LIBPOLY vs VALUE_RATIONAL comparison asserted v1->type instead of v2->type).

Full regression suite: 1726/1726 pass.

[coveralls]

coverage: 68.798% (+0.005%) from 68.793% — mcsat-cached-value-tier-fallback into master