fix(oob,uaf): re-check portfolio verdicts on the reporting solver

Problem: with --portfolio the OOB and UAF detectors took the portfolio's
SAT/UNSAT answer as final. The portfolio solves on its own contexts, so the
reporting solver was never checked: OOB read its counterexample from an
unchecked solver (i=0 under `i > 5`), and a SAT the reporting solver would
not reproduce was still emitted. Other detectors already fail closed through
reconcilePortfolioRecheck.

Fix: add symbolic::recheckPortfolioVerdict, which re-checks a decided verdict
on the reporting solver and reconciles the two (disagreement or timeout ->
unknown), and apply it at the four OOB and two UAF portfolio sites. The
now-redundant UNSAT-only artifact re-checks in OOB checkHazard are removed.

Test: test_proved_requires_exact_model "[portfolio]" requires the portfolio
counterexample to satisfy the path (was i=0, now i=6).

include/fold/symbolic/tactics.hpp

@@ -40,6 +40,13 @@ z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vecto
 [[nodiscard]] z3::check_result reconcilePortfolioRecheck(z3::check_result portfolio,
                                                          z3::check_result recheck);
 
+/// 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.
+[[nodiscard]] z3::check_result recheckPortfolioVerdict(z3::solver& solver,
+                                                       const z3::expr_vector& assumptions,
+                                                       z3::check_result portfolio);
+
 /// 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/oob_access.cpp

@@ -286,6 +286,8 @@ class OOBObserver : public SafetyObserver {
                               static_cast<unsigned>(budget_.per_query.count()), stats_)
                         : symbolic::checkAdaptive(*solver_, assumptions,
                                                   static_cast<unsigned>(budget_.per_query.count()));
+                if (budget_.portfolio)
+                    result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result);
                 stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                     std::chrono::steady_clock::now() - t0);
                 if (stats_.profiling_enabled && !budget_.portfolio) {
@@ -324,6 +326,8 @@ class OOBObserver : public SafetyObserver {
                               static_cast<unsigned>(budget_.per_query.count()), stats_)
                         : symbolic::checkAdaptive(local_s, assumptions,
                                                   static_cast<unsigned>(budget_.per_query.count()));
+                if (budget_.portfolio)
+                    result = symbolic::recheckPortfolioVerdict(local_s, assumptions, result);
                 stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                     std::chrono::steady_clock::now() - t0);
                 if (stats_.profiling_enabled && !budget_.portfolio) {
@@ -504,20 +508,14 @@ class OOBObserver : public SafetyObserver {
                                                    stats_)
                     : symbolic::checkAdaptive(*solver_, assumptions,
                                               static_cast<unsigned>(budget_.per_query.count()));
+            if (budget_.portfolio)
+                result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result);
             stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                 std::chrono::steady_clock::now() - t0);
             if (stats_.profiling_enabled && !budget_.portfolio) {
                 stats_.accumulate(solver_->statistics(), result);
             }
-            if (budget_.portfolio && result == z3::unsat) {
-                auto artifact_t0 = std::chrono::steady_clock::now();
-                z3::check_result artifact_result = solver_->check(assumptions);
-                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, detector_name);
-                }
-            } else if (result == z3::unsat) {
+            if (result == z3::unsat) {
                 rememberUnsatCore(*solver_, path, hazard, detector_name);
             }
         } else {
@@ -534,20 +532,14 @@ class OOBObserver : public SafetyObserver {
                           s, assumptions, static_cast<unsigned>(budget_.per_query.count()), stats_)
                     : symbolic::checkAdaptive(s, assumptions,
                                               static_cast<unsigned>(budget_.per_query.count()));
+            if (budget_.portfolio)
+                result = symbolic::recheckPortfolioVerdict(s, assumptions, result);
             stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
                 std::chrono::steady_clock::now() - t0);
             if (stats_.profiling_enabled && !budget_.portfolio) {
                 stats_.accumulate(s.statistics(), result);
             }
-            if (budget_.portfolio && result == z3::unsat) {
-                auto artifact_t0 = std::chrono::steady_clock::now();
-                z3::check_result artifact_result = s.check(assumptions);
-                stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
-                    std::chrono::steady_clock::now() - artifact_t0);
-                if (artifact_result == z3::unsat) {
-                    rememberUnsatCore(s, path, unsafe, detector_name);
-                }
-            } else if (result == z3::unsat) {
+            if (result == z3::unsat) {
                 rememberUnsatCore(s, path, unsafe, detector_name);
             }
         }

src/detect/use_after_free.cpp

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

src/symbolic/tactics.cpp

@@ -363,6 +363,17 @@ z3::check_result reconcilePortfolioRecheck(z3::check_result portfolio, z3::check
     return portfolio == recheck ? portfolio : z3::unknown;
 }
 
+z3::check_result recheckPortfolioVerdict(z3::solver& solver, const z3::expr_vector& assumptions,
+                                         z3::check_result portfolio) {
+    if (portfolio == z3::unknown)
+        return z3::unknown;
+    try {
+        return reconcilePortfolioRecheck(portfolio, solver.check(assumptions));
+    } catch (const z3::exception&) {
+        return 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_proved_requires_exact_model.cpp

@@ -187,3 +187,25 @@ TEST_CASE("constant-index array OOB keeps Proved only on an exact encoding",
         CHECK(*c == fold::Confidence::Heuristic);
     }
 }
+
+TEST_CASE("portfolio OOB verdicts are re-checked on the reporting solver",
+          "[proved-contract][oob][portfolio]") {
+    // The portfolio answers on its own solvers; the model used to be read from
+    // the reporting solver without re-checking it, so the counterexample did
+    // not satisfy the path (i=0 under `i > 5`).
+    auto unit = parse("int f(int i) { int a[4] = {0}; if (i > 5) return a[i]; return 0; }");
+    REQUIRE(unit);
+    fold::SolverBudget b;
+    b.portfolio = true;
+    fold::SolverStats s;
+    bool found = false;
+    for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s)) {
+        if (f.id.rfind("oob-access:", 0) != 0)
+            continue;
+        found = true;
+        REQUIRE(f.evidence.counterexample.size() == 1);
+        CHECK(f.evidence.counterexample[0].first == "i");
+        CHECK(std::stoll(f.evidence.counterexample[0].second) > 5);
+    }
+    CHECK(found);
+}