--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2010 ---
Le mar. 17 ao?t 2010 17:06:02 CEST, "Kerstin Hartig" <kerstin.hartig at first.fraunhofer.de> a ?crit : > > This problem only ocurs with the Simplify prover right now. > So maybe it is just a prover problem? And Simplify is not safe to use? I have not taken the time to dig much further, but if you enable debug mode in GWhy (in the Proof menu), you can see on the terminal that Simplify rightly answers Invalid... ... but in that case, it outputs a counter-example (i.e. a model of the negation of the formula), which of course contains occurences of the Valid predicate. My guess is that the regexp used by Why to check Simplify's answer needs to be refined. In the mean time, renaming Valid to something else might help ;-) -- E tutto per oggi, a la prossima volta. Virgile