Performance Tips

Reduce solver work without weakening the proof. Use triggers, snapshots, and modular boundaries to keep verification responsive.

Trigger Management

Triggers guide when the SMT solver instantiates quantified variables. Poor trigger choices cause verification to time out or fail to prove valid properties. This page covers how to diagnose and fix trigger-related performance issues.

Minimizing old()

The old()

Modular Verification

Modular verification means verifying components independently rather than as a