Proof-checking code; regressions now check proofs for all single-query valid/unsat regressions by default; numerous fixups of segmentation faults and missing functionality in existing proof-checking code.