相同的輸入，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++庫的實現不同，我們還觀察到了性能的其他波動。