Z3 может быть несовместимым при решении этой проблемы строки?

Question

Я только что столкнулся с проблемой SMTLIB в теории струн, на которую Z3 мог ответить непоследовательно.При вызове Z3 для решения проблемы : с аргументом smt.string_solver=z3str3 возвращается unsat;без аргументов возвращает sat.

Я также использовал CVC4 для решения проблемы.Он вернул решение , которое, по-моему, является допустимой моделью, поскольку я проверил ее, вручную заменив в задаче переменные.

Поскольку я пытаюсь провести исследование с использованием Z3,Я хотел бы знать, является ли это известным поведением Z3.Спасибо всем, кто мог помочь!:)

Редактировать : Я использовал Z3 4.7.1 в WSL Ubuntu 16.04.

Answer 1

Я бы сказал, что получение без присадок или сат, в зависимости от конфигурации Z3, звучит для меня как ошибка.Проверьте средство отслеживания проблем Z3 на наличие проблем, которые описывают подобное поведение, и, если ничего не появляется, сообщите о проблеме там.В идеале, с минимальным примером для воспроизведения проблемы, ваш текущий довольно длинный.