相同的输入，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真）

对公式，并重新运行它，这次它在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++库的实现不同，我们还观察到了性能的其他波动。