--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on September 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] counter example plugin



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