--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on January 2016 ---
On Wed, Jan 27, 2016 at 09:40:33AM +0100, Claude Marché wrote: > > By default, to prove a goal from a set of hypotheses, Alt-Ergo negates > the goal and attempts to establish unsatisfiability. > > With the experimental and undocument options related to "models", the > goal is not negated anymore, hence the wrong results you get. Thank you! So it is not due to the experimental nature, but due to the design... Given the fact that Frama-C exposes access to Alt-Ergo's options essentially via a simple double click on the goal, it might be useful to document from the Frama-C side which options of Alt-Ergo could be useful for Frama-C users, and which are unsafe/forbidden. (Since currently, Frama-C still picks up a green bullet for that falsum...) Wolfram