--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on April 2009 ---
Hello, On Wed, Apr 1, 2009 at 16:09, David MENTRE <dmentre at linux-france.org> wrote: > I have open a bug: > ?[#7560] Inability to prove assigns clauses on simple array code > ?https://gforge.inria.fr/tracker/index.php?func=detail&aid=7560&group_id=1123&atid=5488 Virgile closed the bug. After further investigation, it appears that even on original Boris' code, Alt-Ergo is unable to prove "assigns" clause. Boris, are you using another automated theorem prover than Alt-Ergo? If this is the case, the issue is more related to Alt-Ergo than Jessie itself. Is it possible to circumvent this issue, still using Alt-Ergo? Yours, d.