| Class | Description |
|---|---|
| AbstractCounterExampleGenerator |
Implementations of this class are used find a counter example for a given
Sequent using the SMT solver SolverType.Z3_CE_SOLVER. |
| AbstractSideProofCounterExampleGenerator |
Implementation of
AbstractCounterExampleGenerator which instantiates
the new Proof as side proof. |