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

对吗？ t1 不应该是 3 吗？我认为 int2bv 操作只是将 int 值转换为等效的 bitvector 值。但好像不是！

谢谢！

Answer 1

int2bv 函数本质上被处理为未解释的（如文档中所述），因此语义不精确。以前有一些关于这些转换函数的问题，它们在这里也可能有帮助：

Z3: an exception with int2bv

Check overflow with Z3

bv-enable-int2bv-propagation option

Z3 : Questions About Z3 int2bv?