Check out the Issue Explorer
Looking to fund some work? You can submit a new Funded Issue here.
Whenever we ask the CVC4 or Z3 solvers to check input for satisfiability, we should somehow limit how much time they can spend looking for a solution. The same might apply when we ask for a model, if that is not already done as part of checking for satisfiability. At best, this is just a setting for Z3 and CVC4. In the worst case, we have to set up the solver in a separate thread and somehow kill the thread or do whatever is necessary. If more drastic measures are taken, it of course has to be fully portable.