Problem: null-deref, div-by-zero and int-overflow re-check a portfolio
verdict on the reporting solver and reconcile the two, but then memoized the
re-check's unsat core (and read its model) from the raw re-check result. A
portfolio SAT that the re-check called UNSAT became unknown, yet its core was
still reused as the assumptions for later queries on the same path. The
disagreement itself was silent: no stat, and the trace showed the portfolio's
verdict.
Fix: all six sites use symbolic::recheckPortfolioVerdict and act only on the
reconciled verdict, so an unknown leaves no core or model behind. The helper
counts SolverStats::portfolio_disagreements (merged, printed, and exported in
the detector profile), and the sites trace
"UNKNOWN (portfolio re-check disagreed)".
Test: test_model_validation "[portfolio]" checks the helper's agreement,
unknown and disagreement cases and the merged counter. Full suite: 140/140.
Problem: with --portfolio, null-deref, div-by-zero and int-overflow take
the verdict from a separate portfolio solver, then re-check on their own
solver only to obtain a model or unsat core. The re-check's result was
never compared: if it timed out (unknown) or disagreed, the portfolio's
SAT still produced a finding, with no model from the reporting solver.
Fix: symbolic::reconcilePortfolioRecheck() keeps the verdict only when
the re-check reproduces it and otherwise returns unknown. It is applied
at all six re-check sites.
Test: test_model_validation "portfolio verdicts stand only when the
re-check agrees" covers agreement, re-check unknown, and disagreement in
both directions. null_deref, int_overflow, div_by_zero and
source_structure pass.
