I didn't actually hack on it but I remembered I had dumps from the noble time_t upgrades with problems, and I ran solver3 on those and it performed decently, so I am quite happy.
Shows the backtracking is working correctly.
Still need to actually go and record the unsatisfiability cores (i.e. A->B->C->D and X->Y->Z but D conflicts Z) before backtracking so I can show them to the user at the end. And to avoid making the same bad decisions again in different branches...
