> After further thought, it seems like the place to deal with this is > really operator_predicate_proof(), as in the attached draft patch > against HEAD. This passes the smell test for me, in the sense that > it's an arguably correct and general extension of the proof rules, > but it could use more testing.
I am not sure if we are covering the case when clause_const and pred_const are both NULL. In this case, we should be able to return true only by checking op_strict(pred_op) or maybe even without checking that. Am I mistaken?