14 Timeout🔗ℹ

Each obligation goes to Z3 with a ten-second limit. If Z3 times out or answers unknown, the obligation fails, and the message says the claim may still be true. The usual cause is a claim that needs induction. The checker unfolds measures a step at a time on constructors, and does not reason about every value of a recursive datatype. A precondition should therefore try to use the callee’s claim with the arguments substituted in, rather than a stronger-seeming fact that implies it only by induction. Nonlinear arithmetic can also time out.