TryFor в Z3 не прекращает проверку по истечении заданного срока

Я использую.NET API Z3. Когда я создаю решатель, вызывая:

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

и задайте для него TimeLimit 60 секунд (60000 миллисекунд )для некоторых моделей утверждение

s.Check()

не возвращается через 60 секунд. Для некоторых моделей он возвращается через несколько секунд, что в моем случае не было бы проблемой, но для некоторых моделей он вообще не возвращается (Я отменил процесс через 3 дня ).

Как я могу заставить Z3 прекратить проверку по истечении заданного срока?

5
задан Eric Leschinski 11 June 2013 в 17:57
поделиться