
Hi,
I am using Z3 to determine shortest paths in a graph. Somehow, Z3 takes around 1 min 38 secs to find the shortest path, but around 2 min 58 seconds to find "any path irrespective of cost". Could somebody through some light on why a seemingly easier
problem is taking almost twice the time?


Coordinator
Sep 20, 2013 at 11:01 AM

Without looking at the actual problem you are feeding into Z3, this question is nigh impossible to answer. It could a multitude of things; in the extreme case it could be that the heuristics get lucky on one problem and unlucky on the other. It may also
depend heavily on your encoding of the graph and the properties. Could you perhaps share your input files so we can take a closer look?

