Z3：關於Z3 int2bv的問題？

Question

我對Z3（smt2格式）操作有點困惑int2bv。我寫了一個這樣的SMT2表達：

(declare-const t1 Int) 
(assert (= ((_ int2bv 2) t1) #b11)) 
(check-sat) 
(get-model) 

當我Z3解決它，它得到：

sat 
(model 
    (define-fun t1() Int 
    0) 
) 

是正確的嗎？不應該是3？我認爲int2bv操作只是將int值轉換爲等效的bitvector值。但似乎不是！

謝謝！

Answer 1

int2bv函數本質上處理爲未解釋（如文檔中所述），所以語義不精確。有先前已經對這些轉換函數的一些問題，它們可能會有所幫助在這裏太：

Z3: an exception with int2bv

Check overflow with Z3

bv-enable-int2bv-propagation option