Trying to do BVA on redundant clauses after 100K conflicts

Also, making the 2-lit DIFF hack work only after 100K conflicts.