我正在使用 Z3 的 .NET API。当我通过调用实例化求解器时:
Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit));
并为某些模型指定 60 秒(60000 毫秒)的 TimeLimit
s.Check()
60 秒后不返回。对于某些型号,它会在几秒钟后返回,在我的情况下这不是问题,但对于某些型号,它根本不会返回(我在 3 天后取消了该过程)。
如何在给定的时间限制后强制 Z3 停止检查?