Differential testing harness (EnumerationSolver oracle + known-answer cases)

[paultristanwagner]

Type: infrastructure · Milestone: M0

Goal

A differential / known-answer test harness to catch and guard the soundness bugs (#f01, #f02, …) before fixing them.

Scope

• SAT: generate random small CNFs (3–6 vars, incl. all-negative and unit clauses); assert EnumerationSolver (brute-force, re-validating oracle) agrees with DPLLSolver and DPLLCDCLSolver on SAT/UNSAT, and that returned models satisfy the CNF via assignment.evaluate(cnf).
• Theories: a table of hand-written QF_LRA/LIA/EQ/EQUF/BV/NRA instances with known verdicts, including negation and disjunction cases that exercise false-assigned atoms (the #f01 trigger).
• Wire into mvn test.

Why first

Cheap (hours), needs no new parser, and turns #f01/#f02 into failing tests that flip to passing once fixed.