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. |