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?