--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on September 2020 ---
Hi, I found that a counter example plugin for WP is mentioned in the paper "Frama-C A Software Analysis Perspective", but it was also mentioned that it was not yet released at that point. In the mailing list archive there are some posts mentioning `-wp-unsat-model` which has since been removed and one passing arguments directly to alt-ergo. What is currently the best way to get counterexamples? why3 detects CVC4 and Z3 in a "counter example" variant, how can those be used to get a counterexample? Best regards Matthias