This allows theories to produce different explanations in analyze, and analyze_final. For example, if a theory knows (a && b) => c and c => d and is asked to explain d, it may prefer to explain using [c] in analyze to generate a better clause, but may as well explain using [a, b] in analyze_final since otherwise it would just be asked to explain c anyway.
This allows theories to produce different explanations in
analyze, andanalyze_final. For example, if a theory knows(a && b) => candc => dand is asked to explaind, it may prefer to explain using[c]inanalyzeto generate a better clause, but may as well explain using[a, b]inanalyze_finalsince otherwise it would just be asked to explaincanyway.