Severity: Medium · Category: testing · Confidence: high
Problem
Tested: DPLL/CDCL/Enumeration SAT, CNF round-trip, Tseitin (1 case), Simplex feasibility/optimization, Rational, polynomial arithmetic, two parsers. Untested at the verdict level: the lazy SMT loop, QF_NRA solving/CAD, QF_BV solving, QF_EQUF (no test references EqualityFunctionParser/EqualityFunctionSolver), and CDCL conflict-analysis correctness beyond the SAT/UNSAT boolean. These are exactly the highest-risk paths (findings #f01–#f06). Parser tests assert only happy paths — none assert rejection of malformed/empty/over-wide input.
Location
src/test/java/ (11 files, ~751 LOC)
Fix
Add verdict-level tests asserting SAT/UNSAT against known answers per theory (incl. negation/disjunction). Builds on the differential harness (M0) and SMT-LIB benchmark runner (M2). Add malformed-input rejection tests.
Severity: Medium · Category: testing · Confidence: high
Problem
Tested: DPLL/CDCL/Enumeration SAT, CNF round-trip, Tseitin (1 case), Simplex feasibility/optimization, Rational, polynomial arithmetic, two parsers. Untested at the verdict level: the lazy SMT loop, QF_NRA solving/CAD, QF_BV solving, QF_EQUF (no test references
EqualityFunctionParser/EqualityFunctionSolver), and CDCL conflict-analysis correctness beyond the SAT/UNSAT boolean. These are exactly the highest-risk paths (findings #f01–#f06). Parser tests assert only happy paths — none assert rejection of malformed/empty/over-wide input.Location
src/test/java/(11 files, ~751 LOC)Fix
Add verdict-level tests asserting SAT/UNSAT against known answers per theory (incl. negation/disjunction). Builds on the differential harness (M0) and SMT-LIB benchmark runner (M2). Add malformed-input rejection tests.