Method test_bv_zero_extend

tests/test_z3_ported.py:1996–2000

ZeroExt preserves concrete values.

(self, kernel)

        assert prove(claim)

    def test_bv_zero_extend(self, kernel):
        """ZeroExt preserves concrete values."""
        v = BitVecVal(10, 8)
        claim = ZeroExt(8, v) == BitVecVal(10, 16)
        assert prove(claim)

    def test_array_functional_update(self, kernel):
        """Two stores at same index: second overwrites first."""