我们有一个（大）SMT-LIBv2 输入文件，使用QF_UF逻辑片段。Z3 能够unsat在几秒钟内确定该文件。但是，当我们打开验证生产时，z3 会unknown在几秒钟后报告，并且不会使用大量内存资源。当使用不同的求解器 (veriT) 尝试相同的文件时，我们能够在几秒钟内获得证明 (~500 KB)。
由于QF_UF是一个可判定的片段，而且我们的文件似乎并不太难，我们对这个结果相当惊讶。我们最好的猜测是 z3 耗尽了某种内部资源限制。所以我们有两个问题：有没有办法找出 z3 放弃和报告的原因unknown（这么快）？如果这是由于一些内部限制，可以通过一些配置设置来增加吗？