linux - 相同的输入，Z3 在 Windows 上工作，但在 Linux 上给出分段错误

Question

我使用 Z3 作为有界程序验证的后端求解器。我在不同的操作系统 Windows 7 X64 和 SuSe 10.3 X64 上向 Z3 提供相同的公式，Z3 都是 3.2 版。

他们的输入是： run.z3，它包含嵌套的量词。

在没有启用任何显式选项（默认模式）的情况下，Z3 在 Windows 上运行良好，但是，它在 Linux 上给了我“分段错误”：

../solvers/z3/bin/z3：第 11 行：27951 分段错误

然后我添加唯一的选项

（设置选项：PULL_NESTED_QUANTIFIERS true）

到公式，然后重新运行它，这次它可以在 Linux 上运行，而在 Windows 上它仍然可以运行并且求解速度更快。该选项解决了我在 Linux 上的问题。

Windows 和 Linux 上的 3.2 版 Z3 是否提供不同的功能？这是真的，还有什么区别？提前致谢！

Answer 1

Linux 和 Windows 版本并不完全相同，但它们提供的功能基本相同。主要区别在于使用的任意精度数包（注：在下一个版本中我们将使用我们自己的包，这种差异将不再存在）。我们还必须进行一些调整以应对这两个平台之间的差异。崩溃是由于内存损坏。此错误已修复，下一个版本将包含修复。

由于以下原因，可能会出现性能差异：Linux 和 Windows 版本是使用不同的浮点单元编译的。在 Z3 中实现的一些启发式算法中使用了浮点计算。因此，浮点计算的这种波动可能会产生不同的搜索空间。我们使用的一些标准 C++ 函数（例如std::sort）在 gcc 和 Visual Studio 中有不同的实现。我们还观察到由于 Visual Studio 和 GCC 中标准 C++ 库的实现差异导致的其他性能波动。