On 08/06/2014 11:18 PM, Matthias Bentrup wrote: > > Ah, I had a different understanding of assume, i.e. placing an > assume(A) at some point in code adds not the axiom A, but rather > the axiom "control flow reaches this spot => A". (Your understanding is the conventional one.)