Method test_string_length_ground

tests/test_z3_compat.py:1683–1686

len('hello') == len('world').

(self, kernel)

        assert _try_prove(claim)

    def test_string_length_ground(self, kernel):
        """len('hello') == len('world')."""
        claim = Length(StringVal("hello")) == Length(StringVal("world"))
        assert _try_prove(claim)

    def test_string_concat_ground(self, kernel):
        """'ab' ++ 'cd' == 'abcd'."""