Maliciously crafted contracts could trigger pathological Z3 behaviour (exponential blowup, excessive memory usage). The verifier should set a timeout on Z3 solver invocations.

solver = z3.Solver()
solver.set("timeout", 5000)  # 5 second timeout per contract

First, check whether this is already implemented in vera/smt.py or vera/verifier.py. If it is, document the default limits in the spec. If not, add it.

The three-tier fallback means undecidable contracts already degrade to runtime checks — a timeout should do the same.