z3から間違った結果

Question

私はZ3 SMTソルバーで次のことを証明しようとしています：((x*x) + x) = ((~x * ~x) + ~x)。 これは、Cプログラミング言語のオーバーフローセマンティックのために正しいです。 Z3から

(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) 

出力は次のとおりです：

は、今私は、次のSMT-libのコードを書かれている

0 
0 
unsat 

今、私の質問：なぜ結果が "UNSAT" とは？私のコードのsimplifyコマンドは、myfun1とmyfun2が同じ結果を持つように有効な割り当てを得ることが可能であることを示しています。

私のコードに問題がありますか、これはz3のバグですか？

誰でも助けてください。 Thx

Answer 1

誤った結果は、Z3の式/式プリプロセッサのバグが原因でした。バグは修正され、現在のリリース（v4.3.1）の一部になっています。このバグは、(mod (+ a b))または(mod (* a b))という形式の式を使用するベンチマークに影響しました。

例文hereをオンラインで再試行して、予期した結果を得ることができます。