Z3整流2bv运行 [英] Z3 int2bv operation
本文介绍了Z3整流2bv运行的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
我遇到了一些有关位向量操作的问题。特别是，在给定以下模型的情况下。我原以为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?
这篇关于Z3整流2bv运行的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
查看全文
