新手第一次用z3，百度不了。。。

70000 · 发表于 2021-11-2 13:15:10

马上注册，结交更多好友，享用更多功能^_^

您需要登录才可以下载或查看，没有账号？立即注册

x

本帖最后由 70000 于 2021-11-2 13:31 编辑

s.add('S' == chr((x >> 2) * 2)
TypeError: 'BitVecRef' object cannot be interpreted as an integer

换成整数型无法进行位运算，该怎么办

70000 · 发表于 2021-11-2 13:40:41

已经解决了
是用s.add(ord('S') == (x >> 2) * 2)

必须用整形才行，不能用char型

账号		自动登录	找回密码
密码			立即注册