Synchronize conjecture generation with E-matching.  Minor fix to --full-saturate-quant.