Hard per-query timeouts

Oct 28, 2014 at 1:53 PM
As far as I understand, Z3 supports two kinds of timeouts:
  • Hard global timeouts that terminate the whole Z3 process on timeout (option -T)
  • Soft per-query timeouts that affect each individual query and keep the Z3 process running, but that are a lot are less reliable (option -t). I did a small experiment and for the proof obligations of F* a 5 second soft timeout takes 180 seconds on average.
Is there any way of getting something that gives us the best of both options? That is, is there any way to get
  • Hard per-query timeouts that are both reliable and only affect each individual query
Nov 24, 2014 at 4:33 PM
This is a tricky issue. Hard timeouts could in theory be implemented by just aborting execution, but that would leave all objects in a possibly illegal state, such that the next query will be affected (and in the worst it might crash). To make sure that all objects are left in a legal state, we can only abort the execution at "safe" points in time, and sometimes it may take quite a while to get from one safe point to another. So the short answer is: No, but we might be able to improve upon the 180 seconds if you can tell us what procedure/tactic is using all that time.
Dec 12, 2014 at 4:26 PM
It seems that this problem is gone for us, since Nik implemented a better logical encoding for F* in which he controls how many recursive unrolling the solver will reason about. If someone is interested in fixing the problem we were obtaining initially we would need to do some git archaeology, but it is possible. Let me know.