Currently, the method that does conflict analysis is also the method that checks it. Ideally, the output for conflict analysis would be the learned constraint, and proof that the derivation is correct, and then we would have a separate component that verifies the derivation outside the conflict analysis procedure? This is also relevant for any conflict analyser. This ties into the architecture discussion we had/have.