fix(solver): never memoize a core from a portfolio disagreement

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.

include/fold/cli/profile.hpp

@@ -47,6 +47,7 @@ struct DetectorProfile {
     std::uint64_t z3_elapsed_ms = 0;
     std::uint64_t abstract_sat = 0;
     std::uint64_t abstract_unsat = 0;
+    std::uint64_t portfolio_disagreements = 0;
     std::uint64_t z3_decisions = 0;
     std::uint64_t z3_conflicts = 0;
     std::uint64_t findings_emitted = 0;

include/fold/symbolic/tactics.hpp

@@ -42,10 +42,13 @@ z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vecto
 
 /// Re-checks a decided portfolio verdict on `solver`, the reporting solver, so
 /// it holds the model or unsat core, and reconciles the two answers. Unknown
-/// stays unknown without a re-check.
+/// stays unknown without a re-check. A verdict the re-check does not reproduce
+/// counts in `stats.portfolio_disagreements`; callers must then neither read a
+/// model nor memoize an unsat core from `solver`.
 [[nodiscard]] z3::check_result recheckPortfolioVerdict(z3::solver& solver,
                                                        const z3::expr_vector& assumptions,
-                                                       z3::check_result portfolio);
+                                                       z3::check_result portfolio,
+                                                       ::fold::SolverStats& stats);
 
 /// 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

include/fold/symbolic/theory.hpp

@@ -130,6 +130,9 @@ struct SolverStats {
     std::uint64_t timeouts = 0;
     std::uint64_t abstract_sat = 0;
     std::uint64_t abstract_unsat = 0;
+    // Portfolio verdicts the reporting solver did not reproduce (it timed out
+    // or answered the other way); each became unknown.
+    std::uint64_t portfolio_disagreements = 0;
     std::uint64_t bailed_functions = 0;
     std::uint64_t states_merged = 0;
     std::uint64_t states_kept_separate = 0;
@@ -254,6 +257,7 @@ struct SolverStats {
         timeouts += other.timeouts;
         abstract_sat += other.abstract_sat;
         abstract_unsat += other.abstract_unsat;
+        portfolio_disagreements += other.portfolio_disagreements;
         bailed_functions += other.bailed_functions;
         states_merged += other.states_merged;
         states_kept_separate += other.states_kept_separate;
@@ -360,6 +364,9 @@ struct SolverStats {
         if (abstract_sat != 0 || abstract_unsat != 0) {
             os << " abstract_sat=" << abstract_sat << " abstract_unsat=" << abstract_unsat;
         }
+        if (portfolio_disagreements != 0) {
+            os << " portfolio_disagreements=" << portfolio_disagreements;
+        }
         if (bailed_functions != 0) {
             os << " bailed_functions=" << bailed_functions;
         }

src/cli/detector_profile_accum.cpp

@@ -37,6 +37,7 @@ void applySolverStats(DetectorProfile& profile, const ::fold::SolverStats& stats
     profile.z3_elapsed_ms = static_cast<std::uint64_t>(stats.elapsed.count());
     profile.abstract_sat = stats.abstract_sat;
     profile.abstract_unsat = stats.abstract_unsat;
+    profile.portfolio_disagreements = stats.portfolio_disagreements;
     profile.z3_decisions = stats.decisions;
     profile.z3_conflicts = stats.conflicts;
     profile.states_merged = stats.states_merged;

src/cli/profile.cpp

@@ -53,6 +53,7 @@ std::string ScanProfile::to_json() const {
             {"z3_elapsed_ms", detector.z3_elapsed_ms},
             {"abstract_sat", detector.abstract_sat},
             {"abstract_unsat", detector.abstract_unsat},
+            {"portfolio_disagreements", detector.portfolio_disagreements},
             {"z3_decisions", detector.z3_decisions},
             {"z3_conflicts", detector.z3_conflicts},
             {"findings_emitted", detector.findings_emitted},

src/detect/div_by_zero.cpp

@@ -205,24 +205,22 @@ class DivByZeroObserver : public SafetyObserver {
                            result == z3::sat     ? "SAT (flagged)"
                            : result == z3::unsat ? "UNSAT (guarded)"
                                                  : "TIMEOUT");
-                if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
+                if (budget_.portfolio) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
-                    z3::check_result artifact_result = solver_->check(assumptions);
-                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
+                    const auto disagreements = stats_.portfolio_disagreements;
+                    result =
+                        symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_);
+                    if (stats_.portfolio_disagreements != disagreements)
+                        traceQuery("div-by-zero", loc, result,
+                                   "UNKNOWN (portfolio re-check disagreed)");
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
-                    if (artifact_result == z3::unsat) {
-                        rememberUnsatCore(*solver_, path, hazard);
-                    }
-                    if (artifact_result == z3::sat) {
-                        m = solver_->get_model();
-                    }
-                } else {
-                    if (result == z3::unsat)
-                        rememberUnsatCore(*solver_, path, hazard);
-                    if (result == z3::sat)
-                        m = solver_->get_model();
                 }
+                // Only a reconciled verdict leaves `solver_` holding a matching model or core.
+                if (result == z3::unsat)
+                    rememberUnsatCore(*solver_, path, hazard);
+                if (result == z3::sat)
+                    m = solver_->get_model();
             } else {
                 local_s.set(":timeout", static_cast<unsigned>(budget_.per_query.count()));
                 if (supportsParam(local_s.get_param_descrs(), "smt.threads")) {
@@ -252,24 +250,22 @@ class DivByZeroObserver : public SafetyObserver {
                            result == z3::sat     ? "SAT (flagged)"
                            : result == z3::unsat ? "UNSAT (guarded)"
                                                  : "TIMEOUT");
-                if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
+                if (budget_.portfolio) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
-                    z3::check_result artifact_result = local_s.check(assumptions);
-                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
+                    const auto disagreements = stats_.portfolio_disagreements;
+                    result =
+                        symbolic::recheckPortfolioVerdict(local_s, assumptions, result, stats_);
+                    if (stats_.portfolio_disagreements != disagreements)
+                        traceQuery("div-by-zero", loc, result,
+                                   "UNKNOWN (portfolio re-check disagreed)");
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
-                    if (artifact_result == z3::unsat) {
-                        rememberUnsatCore(local_s, path, hazard);
-                    }
-                    if (artifact_result == z3::sat) {
-                        m = local_s.get_model();
-                    }
-                } else {
-                    if (result == z3::unsat)
-                        rememberUnsatCore(local_s, path, hazard);
-                    if (result == z3::sat)
-                        m = local_s.get_model();
                 }
+                // Only a reconciled verdict leaves `local_s` holding a matching model or core.
+                if (result == z3::unsat)
+                    rememberUnsatCore(local_s, path, hazard);
+                if (result == z3::sat)
+                    m = local_s.get_model();
             }
             symbolic::ExprCache::instance().store(canonical_hash, result);
             CachedDivResult cached_result;

src/detect/int_overflow.cpp

@@ -419,24 +419,22 @@ class IntOverflowObserver : public SafetyObserver {
                            : result == z3::unsat    ? "UNSAT (guarded)"
                            : unknown_reason.empty() ? "UNKNOWN"
                                                     : "UNKNOWN (" + unknown_reason + ")");
-                if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
+                if (budget_.portfolio) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
-                    z3::check_result artifact_result = solver_->check(assumptions);
-                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
+                    const auto disagreements = stats_.portfolio_disagreements;
+                    result =
+                        symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_);
+                    if (stats_.portfolio_disagreements != disagreements)
+                        traceQuery("int-overflow", loc, result,
+                                   "UNKNOWN (portfolio re-check disagreed)");
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
-                    if (artifact_result == z3::unsat) {
-                        rememberUnsatCore(*solver_, path, unsafe);
-                    }
-                    if (artifact_result == z3::sat) {
-                        m = solver_->get_model();
-                    }
-                } else {
-                    if (result == z3::unsat)
-                        rememberUnsatCore(*solver_, path, unsafe);
-                    if (result == z3::sat)
-                        m = solver_->get_model();
                 }
+                // Only a reconciled verdict leaves `solver_` holding a matching model or core.
+                if (result == z3::unsat)
+                    rememberUnsatCore(*solver_, path, unsafe);
+                if (result == z3::sat)
+                    m = solver_->get_model();
             } else {
                 local_s.set(":timeout", static_cast<unsigned>(budget_.per_query.count()));
                 if (supportsParam(local_s.get_param_descrs(), "smt.threads")) {
@@ -467,24 +465,22 @@ class IntOverflowObserver : public SafetyObserver {
                            : result == z3::unsat    ? "UNSAT (guarded)"
                            : unknown_reason.empty() ? "UNKNOWN"
                                                     : "UNKNOWN (" + unknown_reason + ")");
-                if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
+                if (budget_.portfolio) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
-                    z3::check_result artifact_result = local_s.check(assumptions);
-                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
+                    const auto disagreements = stats_.portfolio_disagreements;
+                    result =
+                        symbolic::recheckPortfolioVerdict(local_s, assumptions, result, stats_);
+                    if (stats_.portfolio_disagreements != disagreements)
+                        traceQuery("int-overflow", loc, result,
+                                   "UNKNOWN (portfolio re-check disagreed)");
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
-                    if (artifact_result == z3::unsat) {
-                        rememberUnsatCore(local_s, path, unsafe);
-                    }
-                    if (artifact_result == z3::sat) {
-                        m = local_s.get_model();
-                    }
-                } else {
-                    if (result == z3::unsat)
-                        rememberUnsatCore(local_s, path, unsafe);
-                    if (result == z3::sat)
-                        m = local_s.get_model();
                 }
+                // Only a reconciled verdict leaves `local_s` holding a matching model or core.
+                if (result == z3::unsat)
+                    rememberUnsatCore(local_s, path, unsafe);
+                if (result == z3::sat)
+                    m = local_s.get_model();
             }
             symbolic::ExprCache::instance().store(canonical_hash, result);
             CachedOverflowResult cached_result;

src/detect/null_deref.cpp

@@ -284,24 +284,22 @@ class NullDerefObserver : public SafetyObserver {
                            result == z3::sat     ? "SAT (flagged)"
                            : result == z3::unsat ? "UNSAT (guarded)"
                                                  : "TIMEOUT");
-                if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
+                if (budget_.portfolio) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
-                    z3::check_result artifact_result = solver_->check(assumptions);
-                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
+                    const auto disagreements = stats_.portfolio_disagreements;
+                    result =
+                        symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_);
+                    if (stats_.portfolio_disagreements != disagreements)
+                        traceQuery("null-deref", loc, result,
+                                   "UNKNOWN (portfolio re-check disagreed)");
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
-                    if (artifact_result == z3::unsat) {
-                        rememberUnsatCore(*solver_, path, hazard);
-                    }
-                    if (artifact_result == z3::sat) {
-                        m = solver_->get_model();
-                    }
-                } else {
-                    if (result == z3::unsat)
-                        rememberUnsatCore(*solver_, path, hazard);
-                    if (result == z3::sat)
-                        m = solver_->get_model();
                 }
+                // Only a reconciled verdict leaves `solver_` holding a matching model or core.
+                if (result == z3::unsat)
+                    rememberUnsatCore(*solver_, path, hazard);
+                if (result == z3::sat)
+                    m = solver_->get_model();
             } else {
                 local_s.set(":timeout", static_cast<unsigned>(budget_.per_query.count()));
                 if (supportsParam(local_s.get_param_descrs(), "smt.threads")) {
@@ -332,24 +330,22 @@ class NullDerefObserver : public SafetyObserver {
                            result == z3::sat     ? "SAT (flagged)"
                            : result == z3::unsat ? "UNSAT (guarded)"
                                                  : "TIMEOUT");
-                if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) {
+                if (budget_.portfolio) {
                     auto artifact_t0 = std::chrono::steady_clock::now();
-                    z3::check_result artifact_result = local_s.check(assumptions);
-                    result = symbolic::reconcilePortfolioRecheck(result, artifact_result);
+                    const auto disagreements = stats_.portfolio_disagreements;
+                    result =
+                        symbolic::recheckPortfolioVerdict(local_s, assumptions, result, stats_);
+                    if (stats_.portfolio_disagreements != disagreements)
+                        traceQuery("null-deref", loc, result,
+                                   "UNKNOWN (portfolio re-check disagreed)");
                     stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                         std::chrono::steady_clock::now() - artifact_t0);
-                    if (artifact_result == z3::unsat) {
-                        rememberUnsatCore(local_s, path, hazard);
-                    }
-                    if (artifact_result == z3::sat) {
-                        m = local_s.get_model();
-                    }
-                } else {
-                    if (result == z3::unsat)
-                        rememberUnsatCore(local_s, path, hazard);
-                    if (result == z3::sat)
-                        m = local_s.get_model();
                 }
+                // Only a reconciled verdict leaves `local_s` holding a matching model or core.
+                if (result == z3::unsat)
+                    rememberUnsatCore(local_s, path, hazard);
+                if (result == z3::sat)
+                    m = local_s.get_model();
             }
             symbolic::ExprCache::instance().store(canonical_hash, result);
             CachedNullResult cached_result;

src/detect/oob_access.cpp

@@ -287,7 +287,8 @@ class OOBObserver : public SafetyObserver {
                         : symbolic::checkAdaptive(*solver_, assumptions,
                                                   static_cast<unsigned>(budget_.per_query.count()));
                 if (budget_.portfolio)
-                    result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result);
+                    result =
+                        symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_);
                 stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                     std::chrono::steady_clock::now() - t0);
                 if (stats_.profiling_enabled && !budget_.portfolio) {
@@ -327,7 +328,8 @@ class OOBObserver : public SafetyObserver {
                         : symbolic::checkAdaptive(local_s, assumptions,
                                                   static_cast<unsigned>(budget_.per_query.count()));
                 if (budget_.portfolio)
-                    result = symbolic::recheckPortfolioVerdict(local_s, assumptions, result);
+                    result =
+                        symbolic::recheckPortfolioVerdict(local_s, assumptions, result, stats_);
                 stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                     std::chrono::steady_clock::now() - t0);
                 if (stats_.profiling_enabled && !budget_.portfolio) {
@@ -509,7 +511,7 @@ class OOBObserver : public SafetyObserver {
                     : symbolic::checkAdaptive(*solver_, assumptions,
                                               static_cast<unsigned>(budget_.per_query.count()));
             if (budget_.portfolio)
-                result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result);
+                result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_);
             stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                 std::chrono::steady_clock::now() - t0);
             if (stats_.profiling_enabled && !budget_.portfolio) {
@@ -533,7 +535,7 @@ class OOBObserver : public SafetyObserver {
                     : symbolic::checkAdaptive(s, assumptions,
                                               static_cast<unsigned>(budget_.per_query.count()));
             if (budget_.portfolio)
-                result = symbolic::recheckPortfolioVerdict(s, assumptions, result);
+                result = symbolic::recheckPortfolioVerdict(s, assumptions, result, stats_);
             stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                 std::chrono::steady_clock::now() - t0);
             if (stats_.profiling_enabled && !budget_.portfolio) {

src/detect/use_after_free.cpp

@@ -481,7 +481,8 @@ class UseAfterFreeObserver : public SafetyObserver {
                                    static_cast<unsigned>(budget_.per_query.count()), stats_)
                              : solver_->check(assumptions);
                 if (budget_.portfolio)
-                    result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result);
+                    result =
+                        symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_);
             } else {
                 z3::solver s(c, "QF_BV");
                 s.set(":timeout", static_cast<unsigned>(budget_.per_query.count()));
@@ -494,7 +495,7 @@ class UseAfterFreeObserver : public SafetyObserver {
                                    stats_)
                              : s.check(assumptions);
                 if (budget_.portfolio)
-                    result = symbolic::recheckPortfolioVerdict(s, assumptions, result);
+                    result = symbolic::recheckPortfolioVerdict(s, assumptions, result, stats_);
             }
         } catch (const z3::exception&) {
             ++stats_.unknown;

src/symbolic/tactics.cpp

@@ -364,14 +364,18 @@ z3::check_result reconcilePortfolioRecheck(z3::check_result portfolio, z3::check
 }
 
 z3::check_result recheckPortfolioVerdict(z3::solver& solver, const z3::expr_vector& assumptions,
-                                         z3::check_result portfolio) {
+                                         z3::check_result portfolio, ::fold::SolverStats& stats) {
     if (portfolio == z3::unknown)
         return z3::unknown;
+    z3::check_result recheck = z3::unknown;
     try {
-        return reconcilePortfolioRecheck(portfolio, solver.check(assumptions));
+        recheck = solver.check(assumptions);
     } catch (const z3::exception&) {
-        return z3::unknown;
     }
+    const z3::check_result reconciled = reconcilePortfolioRecheck(portfolio, recheck);
+    if (reconciled == z3::unknown)
+        ++stats.portfolio_disagreements;
+    return reconciled;
 }
 
 z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vector& assumptions,

tests/unit/test_model_validation.cpp

@@ -134,3 +134,27 @@ TEST_CASE("portfolio verdicts stand only when the re-check agrees", "[portfolio]
     CHECK(reconcilePortfolioRecheck(z3::sat, z3::unsat) == z3::unknown);
     CHECK(reconcilePortfolioRecheck(z3::unsat, z3::sat) == z3::unknown);
 }
+
+TEST_CASE("portfolio re-check on the reporting solver records disagreements",
+          "[portfolio][soundness]") {
+    // A disagreement used to be silent, and the detectors memoized the
+    // re-check's unsat core even when the verdict became unknown.
+    z3::context ctx;
+    z3::solver solver(ctx, "QF_BV");
+    const z3::expr value = ctx.bv_const("value", 64);
+    solver.add(value == ctx.bv_val(7, 64));
+    z3::expr_vector assumptions(ctx);
+    using fold::symbolic::recheckPortfolioVerdict;
+
+    fold::SolverStats stats;
+    CHECK(recheckPortfolioVerdict(solver, assumptions, z3::sat, stats) == z3::sat);
+    CHECK(stats.portfolio_disagreements == 0);
+    CHECK(recheckPortfolioVerdict(solver, assumptions, z3::unknown, stats) == z3::unknown);
+    CHECK(stats.portfolio_disagreements == 0);
+    CHECK(recheckPortfolioVerdict(solver, assumptions, z3::unsat, stats) == z3::unknown);
+    CHECK(stats.portfolio_disagreements == 1);
+
+    fold::SolverStats merged;
+    merged.merge(stats);
+    CHECK(merged.portfolio_disagreements == 1);
+}