我遇到了一些有关位向量操作的问题。特别是，在给定以下模型的情况下。我原以为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。我是否做错了什么？

推荐答案

遗憾的是，int2bv和bv2int是未解释的函数。语义可能不会像您预期的那样工作。

参见Z3 : Questions About Z3 int2bv?