Z3如何处理非线性整数算法？

Question

我知道带乘法的整数理论通常是不确定的。但是，在某些情况下，Z3确实会返回模型。我很好奇这是怎么做的。它与实数非线性算术的新决策程序有关吗？Z3为乘法查询返回模型的哪些特定实例（例如：有限模下的整数等）已被识别？任何帮助深表感谢。