z3 4.3.2 не удается найти модель для генерируемых Why3 (выполнимых) целей

Question

Я пытаюсь использовать внутреннюю часть Why3 Z3 для извлечения моделей, которые затем могут быть использованы для получения тестовых случаев с ошибками в программах. Тем не менее, Z3 версии 4.3.2, кажется, не может ответить sat для любой цели Why3. Похоже, некоторые аксиоматические определения, используемые Why3, каким-то образом путают Z3. Например, следующий пример (который является крошечной частью того, что генерирует Why3)

(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (ite (<= 0 x) (= (abs1 x) x) (= (abs1 x) (- x)))))

(check-sat)

результаты в timeout со следующей командной строкой:

z3 -smt2 model.partial=true file.smt2 -T:10

С другой стороны, изменив определение на

(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (=> (<= 0 x) (= (abs1 x) x))))

  (assert
  (forall ((x Int)) (=> (> 0 x) (= (abs1 x) (- x)))))

достанет мне модель (выглядит довольно разумно)

(model 
  (define-fun abs1 ((x!1 Int)) Int
    (ite (>= x!1 0) x!1 (* (- 1) x!1)))
)

но если я попытаюсь добавить следующую аксиому, присутствующую в оригинальном файле Why3, а именно

;; Abs_pos
(assert (forall ((x Int)) (<= 0 (abs1 x))))

опять Z3 ответы timeout,

Что-то мне не хватает в конфигурации Z3? Более того, в предыдущих версиях Why3 была опция MODEL_ON_TIMEOUT, что позволило восстановить модель в таких условиях. Несмотря на то, что не было никакой гарантии, что это была настоящая модель, поскольку Z3 не смог завершить ее проверку, на практике такие модели обычно содержали всю необходимую мне информацию. Тем не менее, я не нашел подобной опции в 4.3.2. Это все еще существует?

Обновление Последняя аксиома Abs_pos был не прав (я немного поиграл с выводом Why3, прежде чем публиковать здесь, и в итоге вставил неверную версию проблемы). Это сейчас исправлено.

Answer 1

Дополнительная аксиома

(подтвердить (не (forall ((x Int)) (<= 0 (abs1 x)))))

делает проблему неудовлетворительной, так как abs1 всегда возвращает неотрицательное целое число, а с дополнительной аксиомой требуется наличие отрицательного результата для abs1 для некоторого x. Веб-версия Z3 возвращает ненадлежащее состояние, как и ожидалось, см. Здесь.