diff --git a/test/Main.hs b/test/Main.hs
index d9940c2..d65864f 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -162,6 +162,66 @@ tests =
   , check ("difference logic agrees with bounded brute force on "
            ++ show (length randomDlProblems) ++ " random problems")
           (all dlAgrees randomDlProblems)
+
+  , check "at-most-k (sequential counter) encodes <= k exactly"
+          (all (\n -> all (cardCorrect atMostK (<=) n) [0 .. n]) [1 .. 4])
+  , check "at-least-k (sequential counter) encodes >= k exactly"
+          (all (\n -> all (cardCorrect atLeastK (>=) n) [0 .. n]) [1 .. 4])
+  , check "exactly-k (sequential counter) encodes == k exactly"
+          (all (\n -> all (cardCorrect exactlyK (==) n) [0 .. n]) [1 .. 4])
+
+  , check "vertex cover: triangle K3 has a cover of size 2 but not 1"
+          (vcSatValid 2 triangleK3 && solveCdcl (vertexCover 1 triangleK3) == CdclUnsat)
+  , check "vertex cover: odd cycle C5 needs 3, not 2"
+          (vcSatValid 3 cycleC5 && solveCdcl (vertexCover 2 cycleC5) == CdclUnsat)
+  , check "vertex cover: star K1,3 is covered by its center alone"
+          (vcSatValid 1 star13)
+
+  , check ("BVE is equisatisfiable and reconstructs models on "
+           ++ show (length randomCnfs) ++ " random CNFs")
+          (all bveCorrect randomCnfs)
+  , check ("BVE reconstructs models for " ++ show (length satisfiableCnfs)
+           ++ " constructed-satisfiable CNFs")
+          (all bveReconstructs satisfiableCnfs)
+
+  , check ("XOR Gaussian solve agrees with brute force on " ++ show (length xorSystems)
+           ++ " random GF(2) systems")
+          (all xorGaussSound xorSystems)
+  , check "XOR Gaussian solve is equisatisfiable to the CNF expansion"
+          (all xorEquisat xorSystems)
+  , check "XOR empty parity-1 clause is UNSAT, parity-0 is SAT"
+          (gaussIsUnsat (xorClause [] True) && gaussIsSat (xorClause [] False))
+
+  , check "hamiltonian path agrees with brute-force permutation search"
+          (all hamPathOk hamGraphs)
+  , check "hamiltonian cycle agrees with brute-force permutation search"
+          (all hamCycleOk hamGraphs)
+
+  , check ("model enumeration counts match brute force on " ++ show (length randomCnfs)
+           ++ " random CNFs")
+          (all enumerateOk randomCnfs)
+  , check "N-queens solution counts match the known sequence for N=1..7"
+          queensCountsOk
+
+  , check ("incremental SAT under assumptions agrees with brute force on "
+           ++ show (length incAssumps) ++ " cases")
+          (all incrementalOk incAssumps)
+  , check "incremental final conflict clause is a real unsatisfiable core"
+          (all incrementalCoreReal incAssumps)
+  , check "batched incremental queries reuse the solver without changing verdicts"
+          incrementalBatchConsistent
+
+  , check ("DRAT/RUP proof or model is correct on " ++ show (length randomCnfs)
+           ++ " random CNFs")
+          (all dratVerifies randomCnfs)
+  , check "DRAT proofs for pigeonhole UNSAT instances verify by RUP"
+          phpProofsVerify
+  , check "corrupting a pigeonhole proof makes the RUP checker reject it"
+          dratCorruptRejected
+
+  , check "heap returns variables in non-increasing activity order"
+          (all heapDescends heapActivityCases)
+  , check "heap increase-key promotes a bumped variable to the top" heapBumpOk
   ]
 
 check :: String -> Bool -> IO Bool
@@ -570,3 +630,237 @@ randDlProblem s0 =
 
 randomDlProblems :: [DlProblem]
 randomDlProblems = fst (genN 60 randDlProblem 20240828)
+
+buildDoubleArray :: [Double] -> ST s (STUArray s Int Double)
+buildDoubleArray xs = newListArray (0, length xs - 1) xs
+
+zeroDoubleArray :: Int -> ST s (STUArray s Int Double)
+zeroDoubleArray n = newArray (0, n - 1) 0
+
+popAll :: VarHeap s -> ST s [Int]
+popAll h = do
+  done <- heapIsEmpty h
+  if done
+    then return []
+    else do
+      v <- heapRemoveMax h
+      rest <- popAll h
+      return (v : rest)
+
+nonIncreasing :: [Double] -> Bool
+nonIncreasing xs = and (zipWith (>=) xs (drop 1 xs))
+
+heapDescends :: [Double] -> Bool
+heapDescends acts = runST $ do
+  let n = length acts
+  arr <- buildDoubleArray acts
+  h <- newHeap n arr
+  mapM_ (heapInsert h) [0 .. n - 1]
+  popped <- popAll h
+  let poppedActs = map (acts !!) popped
+  return (nonIncreasing poppedActs
+          && sort poppedActs == sort acts
+          && length popped == n)
+
+heapActivityCases :: [[Double]]
+heapActivityCases =
+  [ [3, 1, 4, 1, 5, 9, 2, 6]
+  , [1, 2, 3, 4, 5]
+  , [5, 4, 3, 2, 1]
+  , [2, 2, 2, 2]
+  , [7]
+  , [0.5, 10.5, 3.3, 3.3, 8.1, 0.0]
+  ]
+
+heapBumpOk :: Bool
+heapBumpOk = runST $ do
+  arr <- zeroDoubleArray 5
+  h <- newHeap 5 arr
+  mapM_ (heapInsert h) [0 .. 4]
+  writeArray arr 3 100
+  heapIncrease h 3
+  top <- heapRemoveMax h
+  return (top == 3)
+
+bitVectors :: Int -> [[Bool]]
+bitVectors 0 = [[]]
+bitVectors m = [ b : rest | b <- [False, True], rest <- bitVectors (m - 1) ]
+
+cardCorrect :: (Int -> [Lit] -> Int -> ([Clause], Int)) -> (Int -> Int -> Bool) -> Int -> Int -> Bool
+cardCorrect enc predicate n k = all check (bitVectors n)
+  where
+    lits = [ posLit (Var i) | i <- [1 .. n] ]
+    check bits =
+      let units = zipWith (\i b -> [ if b then posLit (Var i) else negLit (Var i) ]) [1 ..] bits
+          (cardClauses, _) = enc k lits (n + 1)
+      in isCdclSat (solveCdcl (CNF (cardClauses ++ units)))
+           == predicate (length (filter id bits)) k
+
+vcSatValid :: Int -> Graph -> Bool
+vcSatValid k g = case solveCdcl (vertexCover k g) of
+  CdclSat model -> validVertexCover k g model
+  CdclUnsat     -> False
+
+triangleK3 :: Graph
+triangleK3 = Graph 3 [(1, 2), (2, 3), (1, 3)]
+
+star13 :: Graph
+star13 = Graph 4 [(1, 2), (1, 3), (1, 4)]
+
+bveCorrect :: CNF -> Bool
+bveCorrect cnf =
+  bruteForceSat cnf == bruteForceSat (bveCnf r)
+    && case solveCdcl (bveCnf r) of
+         CdclSat m -> satisfies (completeModel cnf (reconstructBve r m)) cnf
+         CdclUnsat -> True
+  where r = bve cnf
+
+bveReconstructs :: CNF -> Bool
+bveReconstructs cnf = case solveCdcl (bveCnf r) of
+  CdclSat m -> satisfies (completeModel cnf (reconstructBve r m)) cnf
+  CdclUnsat -> not (bruteForceSat cnf)
+  where r = bve cnf
+
+randXorClause :: Int -> Seed -> (XorClause, Seed)
+randXorClause numVars s0 =
+  let (parity, s1) = randBool s0
+      pick v st = let (b, st') = randBool st in (if b then [Var v] else [], st')
+      go []       st acc = (acc, st)
+      go (v : vs) st acc = let (xs, st') = pick v st in go vs st' (acc ++ xs)
+      (vs, s2) = go [1 .. numVars] s1 []
+  in (xorClause vs parity, s2)
+
+randXorSystem :: Seed -> ([XorClause], Seed)
+randXorSystem s0 = let (nc, s1) = randInt 1 6 s0 in genN nc (randXorClause 5) s1
+
+xorSystems :: [[XorClause]]
+xorSystems = fst (genN 200 randXorSystem 777)
+
+xorBruteSat :: [XorClause] -> Bool
+xorBruteSat sys = any (`systemSatisfies` sys) (allAssignments vs)
+  where vs = nub [ Var v | c <- sys, v <- IntSet.toList (xorVars c) ]
+
+gaussIsSat :: XorClause -> Bool
+gaussIsSat c = case gaussSolve [c] of Just _ -> True; Nothing -> False
+
+gaussIsUnsat :: XorClause -> Bool
+gaussIsUnsat = not . gaussIsSat
+
+xorGaussSound :: [XorClause] -> Bool
+xorGaussSound sys = case gaussSolve sys of
+  Just m  -> systemSatisfies m sys && xorBruteSat sys
+  Nothing -> not (xorBruteSat sys)
+
+xorEquisat :: [XorClause] -> Bool
+xorEquisat sys =
+  isGaussSat == isCdclSat (solveCdcl (systemToCnf sys))
+  where isGaussSat = case gaussSolve sys of Just _ -> True; Nothing -> False
+
+hamGraphs :: [Graph]
+hamGraphs =
+  [ Graph 4 [(1, 2), (2, 3), (3, 4)]
+  , Graph 4 [(1, 2), (2, 3), (3, 4), (4, 1)]
+  , Graph 5 [(1, 2), (2, 3), (3, 4), (4, 5), (5, 1)]
+  , Graph 4 [(1, 2), (1, 3), (1, 4)]
+  , Graph 5 [(1, 2), (2, 3), (3, 1), (3, 4), (4, 5)]
+  , Graph 6 [(1, 2), (2, 3), (3, 4), (4, 5), (5, 6), (6, 1), (1, 4)]
+  ]
+
+adjPairs :: Graph -> [(Int, Int)]
+adjPairs (Graph _ edges) = concat [ [(u, w), (w, u)] | (u, w) <- edges ]
+
+brutePathExists :: Graph -> Bool
+brutePathExists g@(Graph n _) = any ok (permutations [1 .. n])
+  where
+    adj = adjPairs g
+    ok p = all (`elem` adj) (zip p (drop 1 p))
+
+bruteCycleExists :: Graph -> Bool
+bruteCycleExists g@(Graph n _) = any ok (permutations [1 .. n])
+  where
+    adj = adjPairs g
+    ok p = all (`elem` adj) (zip p (drop 1 p))
+             && (n < 2 || (last p, head p) `elem` adj)
+
+hamPathOk :: Graph -> Bool
+hamPathOk g = case solveCdcl (hamiltonianPath g) of
+  CdclSat m -> validHamiltonianPath g m && brutePathExists g
+  CdclUnsat -> not (brutePathExists g)
+
+hamCycleOk :: Graph -> Bool
+hamCycleOk g = case solveCdcl (hamiltonianCycle g) of
+  CdclSat m -> validHamiltonianCycle g m && bruteCycleExists g
+  CdclUnsat -> not (bruteCycleExists g)
+
+countBrute :: CNF -> Int
+countBrute cnf = length (filter (`satisfies` cnf) (allAssignments (allVars cnf)))
+
+enumerateOk :: CNF -> Bool
+enumerateOk cnf = countModels (allVars cnf) cnf == countBrute cnf
+
+queensCountsOk :: Bool
+queensCountsOk = [ countQueensSolutions n | n <- [1 .. 7] ] == [1, 0, 0, 2, 10, 4, 40]
+
+randAssumpSet :: Int -> Seed -> ([Lit], Seed)
+randAssumpSet numVars s0 = let (k, s1) = randInt 0 3 s0 in genN k (randLit numVars) s1
+
+incAssumps :: [(CNF, [Lit])]
+incAssumps =
+  concat
+    [ let (sets, _) = genN 3 (randAssumpSet 5) (9000 + i)
+      in [ (cnf, a) | a <- sets ]
+    | (i, cnf) <- zip [0 ..] randomCnfs ]
+
+bruteIncSat :: CNF -> [Lit] -> Bool
+bruteIncSat cnf assumps = any ok (allAssignments vs)
+  where
+    vs = nub (allVars cnf ++ map litVar assumps)
+    ok m = satisfies m cnf && all (\l -> litValue m l == Just True) assumps
+
+incrementalOk :: (CNF, [Lit]) -> Bool
+incrementalOk (cnf, assumps) = case solveAssuming cnf assumps of
+  IncSat m       -> satisfies m cnf
+                      && all (\l -> litValue m l == Just True) assumps
+                      && bruteIncSat cnf assumps
+  IncUnsat _core -> not (bruteIncSat cnf assumps)
+
+incrementalCoreReal :: (CNF, [Lit]) -> Bool
+incrementalCoreReal (cnf, assumps) = case solveAssuming cnf assumps of
+  IncSat _       -> True
+  IncUnsat core  -> all (`elem` assumps) core && not (bruteIncSat cnf core)
+
+incrementalBatchConsistent :: Bool
+incrementalBatchConsistent =
+  all consistent (take 40 (groupQueries incAssumps))
+  where
+    groupQueries pairs = [ (cnf, [ a | (c, a) <- pairs, c == cnf ]) | cnf <- nub (map fst pairs) ]
+    consistent (cnf, queries) =
+      let batched = solveManyAssuming cnf queries
+      in length batched == length queries
+           && map isIncSat batched == map (isIncSat . solveAssuming cnf) queries
+           && and (zipWith (validResult cnf) batched queries)
+    isIncSat (IncSat _)   = True
+    isIncSat (IncUnsat _) = False
+    validResult cnf (IncSat m) as =
+      satisfies m cnf && all (\l -> litValue m l == Just True) as
+    validResult cnf (IncUnsat core) as =
+      all (`elem` as) core && not (bruteIncSat cnf core)
+
+dratVerifies :: CNF -> Bool
+dratVerifies cnf = case solveProof cnf of
+  ProofSat m   -> satisfies m cnf
+  ProofUnsat p -> not (bruteForceSat cnf) && verifyProof cnf p
+
+phpProofsVerify :: Bool
+phpProofsVerify = all ok [(3, 2), (4, 3), (5, 4)]
+  where
+    ok (h, p) = case solveProof (pigeonhole h p) of
+      ProofUnsat proof -> verifyProof (pigeonhole h p) proof
+      ProofSat _       -> False
+
+dratCorruptRejected :: Bool
+dratCorruptRejected = all rejected [pigeonhole 4 3, pigeonhole 5 4]
+  where
+    rejected cnf = case solveProof cnf of
+      ProofUnsat proof -> length proof >= 2 && not (verifyProof cnf (drop 1 proof))
+      ProofSat _       -> False