--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] proving stack axioms with jessie



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