Method test_sdiv_by_one

tests/test_z3_ported.py:722–726

Signed division by 1: SDiv(x, 1) == x.

(self, kernel)

        assert prove(claim)

    def test_sdiv_by_one(self, kernel):
        """Signed division by 1: SDiv(x, 1) == x."""
        x = BitVec("x", 8)
        claim = ForAll([x], SDiv(x, 1) == x)
        assert prove(claim)

    def test_concat_extract_roundtrip(self, kernel):
        """Extract(7,4, Concat(a,b)) == a for 4-bit a, b."""