Code review of the synth PR surfaced three bugs.

• Duplicate safe_div in reducedb.cpp: safe_div was moved to constants.h but the old copy in reducedb.cpp (inside namespace CMSat) was not removed. Both definitions coexist since reducedb.cpp includes constants.h.

• Integer truncation in oracle cache sort comparator (oracle.cpp): The sort lambda for selecting the best cache lookup variable assigned a double product to uint64_t, truncating the fractional part. Since occs[a] ranges 0.0–0.5, most values truncate to 0, making the sort effectively random.

// Before: truncates to 0 for small values, defeating the sort
uint64_t fa = (double)cache_lookup_frequencies[a]*occs[a];

// After: preserves fractional ordering
double fa = (double)cache_lookup_frequencies[a]*occs[a];

• lits_rem not accumulated in oracle_vivif (oracle_use.cpp): Used = instead of +=, so only the last shortened clause's removal count was reported.

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.