Post-conditions not satisfied after lemma call

[Lilii13]

Hello Fstar community,

I have some issues in the following piece of code. The first assert is exactly the pre-condition of lemma_test and works fine.
Calling the lemma is fine as well, however the assert that comes right after it, which represents the post-condition of the lemma is not verified.

assert(forall e. memP e l' ==> (el_of (e)) = (el_of (ep)) \/ (el_of (e)) ``disjoint`` (el_of (ep)));

lemma_test ep i n r l';

assert(forall e. memP e (fct i n r l') ==> (el_of (e)) = (el_of(ep)) \/ (el_of (e)) ``disjoint`` (el_of (ep)));
fct is a recursive function and lemma_test is also recursive, my guess is that the result of the lemma is not unfolded enough, that's why the post-condition is not valid, or is it something else? any solution on how to solve this?

Thanks a lot!

[nikswamy]

Is it possible to most a minimal repro?

From the perspective of the caller, it doesn't matter that lemma_test is recursive.

Without seeing more of the code, my initial guess is that it has to do with reproving the quantifier in the assertion from the quantified formula in the postcondition of the lemma.

Is it a true SMT failure or is it just a timeout? Have your tried using --query_stats. If it says "canceled" it's worth trying it with a higher rlimit. E.g., #push-options "--z3rlimit_factor 2" just preceding your definition.

[Lilii13]

Hello Nik,

Thank you for answering, the issue was actually an inversion in the disjoint, it was accidently swapped and z3 couldn't see the symmetry.

All solved, great thanks for the tips!