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

Question

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

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

没有启用任何显式选项(默认模式)，Z3 在 Windows 上工作得很好，但是，它在 Linux 上给我“段错误”:

../solvers/z3/bin/z3: line 11: 27951 Segmentation fault

然后我添加唯一的选项

(set-option :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++ 库的实现不同，我们还观察到其他性能波动。