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中没有找到类似的选项。它还存在吗？

Update (上一个公理Abs_pos )是错误的(在这里发布之前，我对Why3的输出进行了一些操作，最后粘贴了一个错误的问题版本)。现在已经修好了。

Answer 1

附加公理

(<= 0 (abs1 X)

这使得问题无法满足，因为abs1总是返回一个非负整数，并且使用附加的公理，您需要对某些x的abs1存在一个负结果。Z3的web版本返回unsat，如预期的那样，请参见这里。