z3rlimit behaving differently in ide mode v.s. command line mode?

[LukeXuan]

I have a file which adjusts z3rlimit inline with the following macro

#push-options "--z3rlimit 10"

For some reason, this enables Z3 to solve a lemma in emacs (--ide mode). However, the following command line failed,

/.../fstar.exe file.fst --smt /.../z3 --include /.../lib --already_cached \* --cache_checked_modules --ext context_pruning

I made sure the emacs sub-process is invoked with the same arguments (except for --ide). Is there any insight into why this happens? I can easily fix the problem by increasing the limit to 20, but it's bothering me not knowing the culprit.

[mtzguido]

Hi Luke,

there are very minor discrepancies in the SMT interaction between F* and Z3 in batch mode and interactive mode. In the IDE we make more use of (push) and (pop) to allow the editor to backtrack over a definition (to edit it again, etc). In Z3, a (pop) doesn't fully undo the changes incurred from the last push, some heuristics can be affected and then become the difference between a working proof and a failing one.

I've also noticed that sometimes just adding a (push) at the top of a file can have an impact.

Given this, it's quite hard to make F* behave exactly the same in the IDE and batch mode, but you should only observe a difference in proofs that are very close to the edge. Is it possible your proof needs a bit of stabilization?