Diagnosing a hard proof
"The proof doesn't converge" is a symptom, not a diagnosis. Before changing anything, collect facts:
| Measurement | What it tells you |
|---|---|
| Flops in the property's cone of influence | Size of the problem. Hundreds: usually fine. Tens of thousands: expect to reduce. |
| Bounded depth reached | How far the engines got. Compare it with how deep the behaviour is (from covers). |
| Which engine made progress | BMC good but no proof → the property is probably true but not inductive: think helper invariants. |
| Large counters, memories, wide arithmetic in the cone | Classic sources of difficulty — candidates for abstraction. |
| Does the same property prove on a smaller configuration? | If yes, the logic is right and the problem is scale. |