autopilot

Synopsis: autopilot;

Description:

This macro performs the following steps:
  1. Finish symbolic execution
  2. Separate proof obligations
  3. Expand invariant definitions
  4. Try to close all proof obligations

Arguments:

No arguments required