注意，在z3中进行调用替换时，它总是会简化表达式，但是在我们的项目中，仅替换和保留原始结构是必要的。根据以下帖子，该功能将被修复，想知道它是否已经存在吗？还是有办法关闭简化功能？
substitution in Z3Py
最佳答案
是的，此问题已在不稳定分支中得到解决（请参见here）；现在，它的行为应完全符合预期。
关于java - Z3 Java中的替代，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/22869338/