hmm so Z3 has a timeout option you can set. In our experience we haven't really seen it hang or do anything out of the ordinary - unsat problems on average see

hmm so Z3 has a timeout option you can set. In our experience we haven't really seen it hang or do anything out of the ordinary - unsat problems on average seem to take longer than sat problems (it probably needs to scan a lot more). We've pushed it to about a million variables or so and it has handled it well thought we might only be a the lower end of workloads.