Z3 int2bv 操作

Question

我在位向量操作方面遇到了一些问题。特别是，给定以下模型。我期待var0 是11。

(declare-const var1 Int)
(declare-const var0 Int)
(assert (= var1 10))
(assert (= var0 ((_ bv2int 32) (bvor ((_ int2bv 32) var1) ((_ int2bv 32) 1)))))
(check-sat)
(get-model)
(exit)

不过，Z3为了好玩给出的解决方案是：

sat (model 
(define-fun var1 () Int 10) 
(define-fun var0 () Int (- 1)) 
)

这意味着，-1 而不是 10。我做错了什么吗？

Answer 1

不幸的是，int2bv 和 bv2int 是未解释的函数。语义可能无法按预期工作。

见Z3 : Questions About Z3 int2bv?