Z3 timing variability

Question

I have encountered some extreme timing variability in Z3, with identical queries sometimes taking a few seconds, sometimes hours -- much more extreme what is discussed here (and without any changes to variable names). These queries only involve integer and Boolean variables. Is this just a normal result of heuristics that use randomization?

Answer 1

My experience with such cases: It all depends! It could be a simple efficiency issue, or maybe something more fundamental. It could be that your own encoding is rather inefficient, or maybe z3 is missing a heuristic case that sends it down to the wrong path. (I find mixing Int's with Bool's usually is OK, so long as you don't try to code up boolean logic with some funky arithmetic.)

Since you haven't told us anything about your particular problem, it's impossible to guess. But if you distill it to something small enough that exhibits the issue, you should file a ticket at https://github.com/Z3Prover/z3/issues and at least have the developers take a look and opine one way or the other. The smaller your example, the better. You can also post it here, of course.