Add to ORKGA major issue in the activity of deductive program verification is the understanding of the reason for why some proof fails. To help the user understand the problem and decide what needs to be fixed in the code or the specification of her program, it is essential to provide means to investigate such a failure. To that mean, we propose a technique for generatingcounterexamples, exhibiting some values for the variables of the program where a given part of the specification fails to be validated. To produce such a counterexample, we exploit the ability of SMT (Satisfiability Modulo Theories) solvers to propose, when a proof of a formula is not found, a counter-model. Turning such a counter-model into a counterexample for the initial pro...