User queries
Create a fresh variable
Checking satisfiability
Querying the solver
Extracting values
Extracting the unsat core
Extracting a proof
Extracting interpolants
Extracting assertions
Getting solver information
Entering and exiting assertion stack
Tactics
Resetting the solver state
Constructing assignments
Terminating the query
Controlling the solver behavior
Miscellaneous
Solver options
Logics supported