No push pop

[giltho]

Z3 is terrible at incremental solving, and I'm not sure what happens but it's the cause of the flakiness of that one query in the gillian-c aws case study.

Also, using Unix.gettimeofday instead of Sys.time for all perf measures because otherwise this was not counting e.g. time waiting for z3 🙃 The measures were entirely all over the place

[giltho]

Booyah! Please merge if you're happy with the code :) Feel free to change to your taste, I'm not extremely happy with the way I fetch the necessary definitions so if you think of a better solution

[PetarMax]

"The measures were entirely all over the place."

From my very extensive experience, this is simply not likely. More evidence is needed to justify claims like these. We may have never had z3 time out on a test before somehow.

[giltho]

I don't know when the use of Sys.time was introduced, but when switching to Unix.gettimeofday I observed that the time went from being consistently much below the wall clock time to matching it more or less exactly (a few miliseconds apart).
It is possible that the change was done by me in like 2020 though, and that it came after your work on improving solver time

[NatKarmios]

It works, I'm cool with it :P

[giltho]

@PetarMax AH but I know what is happening re timing!
Back when you were working on Gillian, it was calling z3 as a library directly! This means z3 was running in the same process so cpu time would measure z3 times as well.
Timings started being entirely bananas when we moved to using z3 through a separate process probably