Method test_extract

tests/test_z3_ported.py:2224–2229

(self)

        assert isinstance(URem(x, y)._ast, BinOpNode)

    def test_extract(self):
        x = BitVec("x", 16)
        r = Extract(7, 0, x)
        assert r.size() == 8
        r2 = Extract(15, 8, x)
        assert r2.size() == 8

    def test_concat(self):
        a, b = BitVecs("a b", 4)