--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on April 2013 ---
On 24/04/2013 15:45, Cristiano Sousa wrote: > Hi Lo?c, > > Here is an example: http://pastebin.com/jzq4Qg0r > The axiomatic was indeed inconsistent. diff --git a/src/wp/share/memory.why b/src/wp/share/memory.why index d75c81b..eaddcb2 100644 --- a/src/wp/share/memory.why +++ b/src/wp/share/memory.why @@ -41,7 +41,7 @@ theory Memory p.base = q.base -> (addr_le p q <-> p.offset <= q.offset) axiom addr_lt_def: forall p q :addr [addr_lt p q]. - p.base = q.base -> (addr_le p q <-> p.offset < q.offset) + p.base = q.base -> (addr_lt p q <-> p.offset < q.offset) axiom addr_le_bool_def : forall p q : addr [ addr_le_bool p q]. addr_le p q <-> addr_le_bool p q = True Thanks for finding it! (thanks also z3!) -- Fran?ois