z3 - z3 は私の制限の一部を無視していますか?

Question

stackoverflow-ers(?)、

私はz3で遊んでいて、次の制限を解決しようとしています:

(declare-const A (_ BitVec 32))
(declare-const B (_ BitVec 32))
(declare-const C (_ BitVec 32))
(declare-const D (_ BitVec 32))
(declare-const E (_ BitVec 32))
(declare-const F (_ BitVec 32))

(assert (<= A #xFFFFFFFF))
(assert (<= B #xFFFFFFFF))
(assert (<= C #xFFFFFFFF))


(assert (> A #x00000000))

;(Commented) Restriction #1 (assert (> B #x00000000))
(assert (> C #x00000000))

(assert (= D (bvand (bvmul (bvmul A B) #x00000008) #xFFFFFFFF) ))
(assert (<= D #xFFFFFFFF))

(assert (= E (bvand (bvmul (bvmul A C) #x00000008) #xFFFFFFFF)))
(assert (<= D E))

(assert (= F (bvand (bvmul A #x00000008) #xFFFFFFFF)))    

;(Uncommented) Restriction #2
(assert (> (bvand (bvmul F B) #xFFFFFFFF) D))

(assert (< (bvand (bvmul A B) #xFFFFFFFF) #x7FFFFFFF))
(assert (< (bvand (bvmul A C) #xFFFFFFFF) #x7FFFFFFF))


(assert (< D #x01000000))

(check-sat)

(get-value(A))
(get-value(B))
(get-value(C))
(get-value(D))
(get-value(F))

これらの制約にはいくつかの問題があります: a) 最初の問題は、z3 が「制限 #2」を無視していることです。

(assert (> (bvand (bvmul F B) #xFFFFFFFF) D))

、私が得る値は次のとおりです。

A: #x000070e0
B: #x0000000a
C: #x00000014
D: #x00234600
F: #x00038700

制限にもかかわらず、F*B = D です。

b）「制限＃1」のコメントを外した場合

(assert (> B #x00000000))

私は次の結果を得ています：

A: #x0000a000
B: #x00000007
C: #x00000000

それは椅子 - キーボード インターフェイスのバグですか? 私は何を間違っていますか？

これを Z3 オンラインで実行します。

前もって感謝します！