Я использую.NET API Z3. Когда я создаю решатель, вызывая:
Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit));
и задайте для него TimeLimit 60 секунд (60000 миллисекунд )для некоторых моделей утверждение
s.Check()
не возвращается через 60 секунд. Для некоторых моделей он возвращается через несколько секунд, что в моем случае не было бы проблемой, но для некоторых моделей он вообще не возвращается (Я отменил процесс через 3 дня ).
Как я могу заставить Z3 прекратить проверку по истечении заданного срока?