z3 4.3.2 не удается найти модель для целых 3-х целей (0)

Question

Я пытаюсь использовать Back-end для Z3 Why3, чтобы получить модели, которые затем могут использоваться для получения тестовых примеров с ошибками в программах. Тем не менее, 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. Он все еще существует?

Update Последняя аксиомой Abs_pos было неправильно (я поиграл немного с выходом Why3 перед размещением здесь и в конечном итоге вставив неправильную версию выпуска). Теперь это исправлено.

Answer 1

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

(утверждают (не (FORALL ((х Int)) (< = 0 (Abs1 х)))))

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