我使用Z3的.NET API。 当我通过调用实例化一个求解：
Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit));
并给它60秒（60000毫秒）时限某些型号的声明
s.Check()
60秒后不返回。 对于某些型号，它返回几秒钟后，它在我的情况就不会是一个问题，但对于一些车型也完全不回（我后3天内取消的过程）。
我怎么能强迫Z3停止给定的时限后检查？
Answer 1:
该TryFor组合子使用“取消”的标志来实现。 新的战术是非常敏感，而当“解除”标志很快终止。 不幸的是，通用战术smt是一个包装在一个通用的解决者。 这种通用求解器是不是很敏感。 在几个关键的地方它可以得到“丢失”：量词实例化，单面等qflia战术是建立在之上smt和许多其他的战术。 因为，你正在试图解决自由量词问题。 我假设的smt策略是在单面模块的内部循环。 在单纯形模块smt战术使用任意精度有理数实现。 因此，它可能是非常耗时的对非平凡的线性实/整数的问题。
没有太多可以做，以解决此问题。 如果你真的需要在运行时间了有力的保障，我看到的唯一解决方案是创建运行Z3一个单独的进程，而当它需要更多的杀死它k秒钟解决问题。
话虽这么说，Z3的未来版本将有一个全新的运算模块。 当取消标志设置这个新的模块（如新的战术）将很快终止。
文章来源: TryFor in Z3 does not stop checking after the given timelimit
