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

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

本帖最后由 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型
页: [1]
查看完整版本: 新手第一次用z3，百度不了。。。