--- layout: fc_discuss_archives title: Message 71 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] counterexamples through Frama-C WP



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