The minisat expensive simplification procedure has been fixed recently to correct a bug that could make the solver spend too much time during conflict minimization. The issue was raised by Allen Van Gelder in a paper (SAT'11 ?). The code of minisat available in github contains the fix. We might want to implement our own.

It might be the case that such issue arrises when using cardinality constraints. Need to investigate further.