制限付きプログラム検証のバックエンドソルバーとしてZ3を使用します。異なるオペレーティングシステム、Windows7X64とSuSe10.3X64のZ3に同じ数式をフィードします。どちらのZ3も、バージョン3.2です。
それらの入力は次の とおりです。run.z3、ネストされた数量詞が含まれています。
明示的なオプションが有効になっていない場合（デフォルトモード）、Z3はWindowsで非常にうまく機能しますが、Linuxでは「セグメンテーション違反」が発生します。
../solvers/z3/bin/z3：行11：27951セグメンテーション違反
次に、唯一のオプションを追加します
（set-option：PULL_NESTED_QUANTIFIERS true）
数式に追加して再実行すると、今回はLinuxで動作し、Windowsでも動作し、より高速に解決されます。このオプションは、Linuxでの私の問題を解決します。
WindowsとLinuxのバージョン3.2のZ3は異なる機能を提供しますか？それは本当です、他に何の違いがありますか？前もって感謝します！
Linux と Windows のバージョンは同じではありませんが、本質的に同じ機能を提供します。主な違いは、使用される任意精度の数値パッケージです (注意: 次のバージョンでは、独自のパッケージを使用する予定であり、この違いはもう存在しません)。また、これら 2 つのプラットフォームの違いに対処するために、いくつかの調整を行う必要がありました。クラッシュの原因はメモリの破損でした。このバグは修正されており、次のリリースには修正が含まれる予定です。
次の理由により、パフォーマンスの違いが生じる可能性があります。Linux と Windows のバージョンは、異なる浮動小数点単位を使用してコンパイルされています。浮動小数点計算は、Z3 に実装されている一部のヒューリスティックで使用されます。したがって、浮動小数点計算のこの変動により、異なる検索空間が生成される可能性があります。私たちが使用する一部の標準 C++ 関数 (例: std::sort) は、gcc と Visual Studio で異なる実装を持っています。また、Visual Studio と GCC での標準 C++ ライブラリの実装の違いによるパフォーマンスの変動も観測されました。