In my usecase I try to use the solver to solve multiple formulas one after the other. Sometimes, the solver hangs on a certain formula, but when I try to run it again on the very same formula it succeeds immediately. Below is a minimal example in which I run the solver on the same formula multiple times, and after a few attempts it hangs indefinitely.
from z3 import *
def test_solve():
s, s1, s2 = Strings('s s1 s2')
i, t = Ints('i t')
sl = Solver()
start = datetime.now()
sl.add(Not(Implies(And(i < t,
Contains(s, s1),
Not(SuffixOf(s1, s)),
Or(0 < i, PrefixOf(s1, s))),
Or(PrefixOf(s2, s), PrefixOf(s1, s)))))
print(f"{attempt}: {sl.check()}. Solved in {datetime.now() - start}")
for attempt in range(20):
test_solve()
This is its output:
0: sat. Solved in 0:00:00.504905
1: sat. Solved in 0:00:01.313257
2: sat. Solved in 0:00:00.543546
3: sat. Solved in 0:00:00.137668
4: sat. Solved in 0:00:00.268307
5: sat. Solved in 0:00:00.189427
It hangs on the 6th attempt. Is this an expected behavior? Is there anything I can do to mitigate this?
No, I'd say this is not expected. It is true that there are "random" seeds etc. that are in play which can affect performance in each run; but the differences you're seeing (and I can replicate) are way too much to chalk it up to random seeds. The string solver that you are using has its problems, and I think this'd be a good test-case to report to the developers so they can take a look and see if they can spot why there's so much discrepancy. Please file it at: https://github.com/Z3prover/z3/issues