--- layout: fc_discuss_archives title: Message 71 from Frama-C-discuss on November 2013 ---
I've been successfully using Frama-C WP with alt-ergo, but I do not see a mechanism for retrieving concrete counterexample information from the back-end SMT solvers (either alt-ergo, or others through Why). Just in case I'm missing something, can someone more familiar with WP point me to the appropriate options or confirm that reporting counterexample information is a feature yet to be implemented? If the latter, would such a contribution be welcome? - David