fix(solver): fail closed when the portfolio re-check disagrees

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.

include/fold/symbolic/tactics.hpp

@@ -32,6 +32,14 @@ z3::check_result checkWithAssumptionsProfiled(z3::solver& solver,
 z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vector& assumptions,
                                     unsigned timeout_ms, ::fold::SolverStats& stats);
 
+/// Portfolio answers come from a separate solver; detectors re-check on their
+/// own solver to get a model or an unsat core. The answer stands only when the
+/// re-check agrees: a re-check that times out or disagrees yields unknown, so a
+/// finding is never emitted from a SAT verdict the reporting solver did not
+/// reproduce (and has no model for).
+[[nodiscard]] z3::check_result reconcilePortfolioRecheck(z3::check_result portfolio,
+                                                         z3::check_result recheck);
+
 /// Check assumptions with an ESCALATING timeout. A query that returns UNKNOWN
 /// at `base_timeout_ms` is re-checked at 2x, 4x, ... up to a cap, so a query
 /// that is just barely over budget still resolves (SAT/UNSAT) instead of losing

src/detect/div_by_zero.cpp

@@ -208,6 +208,7 @@ class DivByZeroObserver : public SafetyObserver {
                 if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
                     z3::check_result artifact_result = solver_->check(assumptions);
+                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
                     if (artifact_result == z3::unsat) {
@@ -254,6 +255,7 @@ class DivByZeroObserver : public SafetyObserver {
                 if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
                     z3::check_result artifact_result = local_s.check(assumptions);
+                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
                     if (artifact_result == z3::unsat) {

src/detect/int_overflow.cpp

@@ -422,6 +422,7 @@ class IntOverflowObserver : public SafetyObserver {
                 if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
                     z3::check_result artifact_result = solver_->check(assumptions);
+                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
                     if (artifact_result == z3::unsat) {
@@ -469,6 +470,7 @@ class IntOverflowObserver : public SafetyObserver {
                 if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
                     z3::check_result artifact_result = local_s.check(assumptions);
+                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
                     if (artifact_result == z3::unsat) {

src/detect/null_deref.cpp

@@ -287,6 +287,7 @@ class NullDerefObserver : public SafetyObserver {
                 if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
                     z3::check_result artifact_result = solver_->check(assumptions);
+                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
                     if (artifact_result == z3::unsat) {
@@ -334,6 +335,7 @@ class NullDerefObserver : public SafetyObserver {
                 if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
                     z3::check_result artifact_result = local_s.check(assumptions);
+                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
                     if (artifact_result == z3::unsat) {

src/symbolic/tactics.cpp

@@ -359,6 +359,10 @@ z3::check_result checkAdaptive(z3::solver& solver, const z3::expr_vector& assump
     }
 }
 
+z3::check_result reconcilePortfolioRecheck(z3::check_result portfolio, z3::check_result recheck) {
+    return portfolio == recheck ? portfolio : z3::unknown;
+}
+
 z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vector& assumptions,
                                     unsigned timeout_ms, ::fold::SolverStats& stats) {
     z3::expr query = smt_solver.ctx().bool_val(true);

tests/unit/test_model_validation.cpp

@@ -122,3 +122,15 @@ TEST_CASE("portfolio translation accepts Fold theory and rejects unsupported exp
     CHECK(fold::symbolic::checkWithPortfolio(unsupported_solver, assumptions, 100, stats) ==
           z3::unknown);
 }
+
+TEST_CASE("portfolio verdicts stand only when the re-check agrees", "[portfolio][soundness]") {
+    // The re-check used to be consulted only for its model/core; a SAT
+    // portfolio verdict whose re-check timed out was still reported as SAT.
+    using fold::symbolic::reconcilePortfolioRecheck;
+    CHECK(reconcilePortfolioRecheck(z3::sat, z3::sat) == z3::sat);
+    CHECK(reconcilePortfolioRecheck(z3::unsat, z3::unsat) == z3::unsat);
+    CHECK(reconcilePortfolioRecheck(z3::sat, z3::unknown) == z3::unknown);
+    CHECK(reconcilePortfolioRecheck(z3::unsat, z3::unknown) == z3::unknown);
+    CHECK(reconcilePortfolioRecheck(z3::sat, z3::unsat) == z3::unknown);
+    CHECK(reconcilePortfolioRecheck(z3::unsat, z3::sat) == z3::unknown);
+}