> 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?

Reply via email to