TryFor in Z3 does not stop checking after the given timelimit

Viewed 225

I am using the .NET API of Z3. When I instantiate a solver by calling:

Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit));

and give it a TimeLimit of 60 seconds (60000 milliseconds) for some models the statement

s.Check()

does not return after 60 seconds. For some models it returns a few seconds later, which in my case would not be a problem, but for some models it doesn't return at all (I cancelled the process after 3 days).

How can I force Z3 to stop checking after a given timelimit?

1 Answers
Related