calc_lbd(c.cnf) was called inside the trail loop on every iteration,
but each intermediate result was immediately overwritten by the next.
Only the final LBD matters, so compute it once after the loop.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

auto last_restart = 0 deduced to int, but it stores sat_confl which is
uint64_t. The narrowing assignment silently truncates for large conflict
counts, making the restart interval computation wrong.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

1. Type error: include_solution() takes const FF& but was passed a raw
   uint64_t. Create an FMpz Field value from the BDD count.

2. Logic error: branch_found_unsat() is a const getter (returns bool),
   not a setter. The UNSAT case was silently doing nothing, failing to
   mark either branch as UNSAT. Use mark_branch_unsat() instead.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

StackLevel contains unique_ptr members (branch_mc array) and cannot be
copied. Use a const reference instead.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…ation

Two performance optimizations inspired by CaDiCaL:

1. Prefetch next watch's clause data in the long-clause propagation loop.
   Hides memory latency by issuing the prefetch before processing the
   current clause. This is a standard technique in modern SAT solvers.

2. Poison-based recursive clause minimization (Sörenson/Biere SAT'09,
   used in CaDiCaL/Kissat). When lit_redundant() fails because a
   variable has no antecedent or wrong abstraction level, mark it and
   all intermediate variables as "poison" (seen[v]=4). Future
   lit_redundant() calls that encounter a poisoned variable immediately
   return false, avoiding redundant re-exploration of the same failing
   subtree. Poison marks are cleaned up at the end of minimize_uip_cl()
   along with all other seen[] entries.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

When propagation finds a new watch literal for a clause, the old code
stored plit (the false literal being propagated) as the blocking literal
in the new watch entry. Since plit is always false, the blocking literal
check would never succeed for this watch, forcing a clause dereference
every time.

Use c[0] (the other watched literal) instead. c[0] is unknown or may
become true later, giving the blocking literal check a real chance of
short-circuiting future clause visits. This is the approach used in
CaDiCaL. Applied to both propagate() and v_propagate().

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

The record_comp() loop traverses variables in BFS order. Adjacent
variables in comp_vars can be numerically far apart, causing cache
misses when accessing their holder metadata (timestamp, level, occ
data).

Two prefetch hints added:
1. Prefetch next variable's holder metadata at the start of each
   iteration, so timestamp/level/size lookups are cache-warm.
2. Prefetch next long clause's literal data in the clause traversal
   loop (only for non-ternary clauses where we access long_clauses_data;
   ternary clause data is inline in ClData and needs no extra fetch).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Replace the step-function conflicts/decisions heuristic in reduce_db()
with an EMA of the conflict rate, enabled via --rdbemarate 1. The EMA
smooths phase transitions between SAT-like and UNSAT-like solving,
avoiding cliff discontinuities in the target multiplier. Alpha is
tunable via --rdbemalpha (default 0.15). Original step-function
behaviour is preserved when the flag is off.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Print the actual new lbd_cutoff value instead of hardcoded "3",
which would be wrong if base_lbd_cutoff \!= 2.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

This reverts commit bbfd564.

This reverts commit 98c0f99.