---
layout: fc_discuss_archives
title: Message 86 from Frama-C-discuss on November 2009
---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Lemma from ACSL doc doesn't verify
- Subject: [Frama-c-discuss] Lemma from ACSL doc doesn't verify
- From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
- Date: Wed, 25 Nov 2009 16:50:36 +0100
- In-reply-to: <20091125162200.0a3ccb44@is010235>
- References: <FC0686BB6178BC43B9DC035287A11A720DBE657C91@SI-MBX12.de.bosch.com> <20091125162200.0a3ccb44@is010235>
Oops, sorry I meant
//@ lemma mean_property: \forall int l, h; l <= h ==> l <= l + (h-l)/2 <= h;
still doesn't verify. I haven't tried the latest version of why however. I have AltErgo 0.7.3 and Z3 1.3.
-Boris