optimization - z3 的错误结果

Question

我正在尝试使用 Z3 SMT Solver 证明以下内容:((x*x) + x) = ((~x * ~x) + ~x)。这是正确的，因为 c 编程语言中的溢出语义。

现在我写了下面的smt-lib代码:

(declare-fun a () Int)

(define-fun myadd ((x Int) (y Int)) Int (mod (+ x y) 4294967296) )
(define-fun mynot ((x Int))         Int (- 4294967295 (mod x 4294967296)) )
(define-fun mymul ((x Int) (y Int)) Int (mod (* x y) 4294967296) )

(define-fun myfun1 ((x Int)) Int (myadd (mynot x) (mymul (mynot x) (mynot x))) )
(define-fun myfun2 ((x Int)) Int (myadd x (mymul x x)) )

(simplify (myfun1 0))
(simplify (myfun2 0))

(assert (= (myfun1 a) (myfun2 a)))
(check-sat)
(exit)

z3 的输出是:

0
0
unsat

现在我的问题是:为什么结果“不满意”？我的代码中的 simplify 命令表明可以获得有效分配，因此 myfun1 和 myfun2 具有相同的结果。

我的代码有问题还是 z3 中的错误？

请任何人帮助我。谢谢

Answer 1

不正确的结果是由于 Z3 公式/表达式预处理器中的错误。该错误已得到修复，并且已经是当前版本 (v4.3.1) 的一部分。该错误影响使用以下形式的公式的基准测试:(mod (+ a b)) 或 (mod (* a b))。

我们可以在线重试这个例子here , 得到预期的结果。