1
は、私は、次のSMT-LIB2スクリプトました：Z3 v3.2のは、Mac上で実行している整数/ bv混合ベンチマークの健全性問題？
(set-option :produce-models true)
(declare-fun s0() Int)
(declare-fun table0 (Int) (_ BitVec 8))
(assert (= (table0 0) #x00))
(assert
(let ((s3 (ite (or (< s0 0) (<= 1 s0)) #x01 (table0 s0))))
(let ((s5 (ite (bvuge s3 #x02) #b1 #b0)))
(= s5 #b1))))
(check-sat)
(get-model)
を、私が取得：
sat
(model
;; universe for (_ BitVec 8):
;; bv!val!2 bv!val!3 bv!val!0 bv!val!1
;; -----------
;; definitions for universe elements:
(declare-fun bv!val!2() (_ BitVec 8))
(declare-fun bv!val!3() (_ BitVec 8))
(declare-fun bv!val!0() (_ BitVec 8))
(declare-fun bv!val!1() (_ BitVec 8))
;; cardinality constraint:
(forall ((x (_ BitVec 8)))
(and (= x bv!val!2) (= x bv!val!3) (= x bv!val!0) (= x bv!val!1)))
;; -----------
(define-fun s0() Int
(- 1))
(define-fun table0 ((x!1 Int)) (_ BitVec 8)
(ite (= x!1 0) bv!val!0
(ite (= x!1 (- 1)) bv!val!3
bv!val!0)))
)
S0 = -1モデルであると述べています。しかし、s0 = -1では、s3 = 1とs5 =＃b0となり、アサーションは偽になります。実際、私はベンチマークが不満足であると確信しています。
私がZ3出力に気付いたことの1つは、カーディナリティ制約のために与えられた数式です。それは言う：
;; cardinality constraint:
(forall ((x (_ BitVec 8)))
(and (= x bv!val!2) (= x bv!val!3) (= x bv!val!0) (= x bv!val!1)))
アサーションは、むしろ奇妙な音です。それは違反ではないでしょうか？私はこれが問題の根本的な原因であるかどうかはわかりませんが、確かに怪しいと聞こえます。