--- layout: fc_discuss_archives title: Message 113 from Frama-C-discuss on December 2009 ---
>> The conditions is not discharged although axiom select_store_eq seems >> quite sufficient to discharge it. Is integer_of_int32 somehow getting in >> the way? > >Which prover are you using? alt-ergo 0.9 seems indeed to have some >difficulties, but Simplify 1.5.4 and z3 2.0 succeed on all obligations. To complete Virgile's answer, alt-ergo 0.9 has problems with -jessie-int-model bounded and -jessie-int-model modulo, and succeeds with -jessie-int-model exact. I think we can pass this along to alt-ergo developers, it can probably be considered an interesting example. Pascal