Abstract
The Proof2Test system, designed for the AutoProof environment, uses the underlying SMT Solving Technology to generate test cases for proof failures. These test cases can be simplified by reducing the magnitude of the values of the variables present in them. The present work describes a simplification strategy to generate test cases that use small values and are easily understandable by programmers.