Тот же ввод, 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: строка 11: 27951 Ошибка сегментации

Затем я добавляю единственную опцию

(set-option: PULL_NESTED_QUANTIFIERS true)

к формулам и перезапустите его, на этот раз он работает в Linux, а в Windows он все еще работает и решает быстрее. Этот вариант решает мою проблему в Linux.

Обеспечивает ли Z3 версии 3.2 в Windows и Linux разные функции? Это правда, какие еще различия? Заранее спасибо!

Answer 1

Версии для Linux и Windows не идентичны, но они обеспечивают практически одинаковые функции.Основным отличием является используемый пакет с произвольной точностью (примечание: в следующей версии мы будем использовать наш собственный пакет, и эта разница больше не будет существовать).Нам также пришлось внести несколько корректировок, чтобы справиться с различиями между этими двумя платформами.Сбой произошел из-за повреждения памяти.Эта ошибка была исправлена, и следующий выпуск будет содержать исправление.

Различия в производительности возможны по следующим причинам: версии для Linux и Windows были скомпилированы с использованием различных модулей с плавающей запятой.Вычисления с плавающей точкой используются в некоторых эвристиках, реализованных в Z3.Таким образом, эти колебания в вычислениях с плавающей запятой могут создавать другое пространство поиска.Некоторые стандартные функции C ++, которые мы используем (например, std::sort), имеют различную реализацию в gcc и Visual Studio.Мы также наблюдали другие колебания производительности из-за различий в реализации стандартной библиотеки C ++ в Visual Studio и GCC.