(self)
| 944 | assert r.size() == 16 |
| 945 | |
| 946 | def test_bv2int(self): |
| 947 | x = BitVec("x", 8) |
| 948 | r = BV2Int(x) # default is_signed=False → unsigned (BV2NAT) |
| 949 | assert isinstance(r._ast, UnOpNode) and r._ast.op == UnOp.BV2NAT |
| 950 | assert r.sort() == IntSort() |
| 951 | # is_signed=True → signed (BV2INT) |
| 952 | r2 = BV2Int(x, is_signed=True) |
| 953 | assert isinstance(r2._ast, UnOpNode) and r2._ast.op == UnOp.BV2INT |
| 954 | |
| 955 | def test_int2bv(self): |
| 956 | x = Int("x") |