Same input, Z3 works on Windows, but gives Segmentation Faults on Linux

Question

I use Z3 as a back-end solver on bounded program verification. I feed same formulas to Z3 on different operating systems, Windows 7 X64 and SuSe 10.3 X64, both Z3 are version 3.2.

Their input is: run.z3, it contains nested quantifiers.

Without any explicit options enabled(the default mode), Z3 works very well on Windows, however, it gives me "Segmentation fault" on Linux:

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

Then I add the only option

(set-option :PULL_NESTED_QUANTIFIERS true)

to the formulas, and re-run it, this time it works on Linux, and on Windows it still works and solves faster. That option solves my problem on Linux.

Does Z3 of version 3.2 on Windows and Linux provide different features? It that's true, what else differences are? Thanks in advance!

Answer 1

The Linux and Windows versions are not identical but they provide essentially the same features. The main difference is the arbitrary precision number package used (remark: in the next version we will be using our own package, and this difference will not exist anymore). We also had to make several adjustments to cope with differences between these two platforms. The crash was due to a memory corruption. This bug has been fixed, and the next release will contain the fix.

Performance differences are possible due to the following reasons: the Linux and Windows versions were compiled using different floating point units. Floating point computations are used in some heuristics implemented in Z3. So, this fluctuations in floating point computations may produce a different search space. Some standard C++ functions we use (e.g. std::sort) have a different implementation in gcc and Visual Studio. We also observed other fluctuations in performance due to differences in the implementation of the standard C++ library in Visual Studio and GCC.