Method test_length_concat

tests/test_z3_semantic.py:733–736

len(a ++ b) = len(a) + len(b) for ground strings.

(self, kernel)

        assert _try_prove(Length(StringVal("")) == IntVal(0))

    def test_length_concat(self, kernel):
        """len(a ++ b) = len(a) + len(b) for ground strings."""
        a, b = StringVal("foo"), StringVal("bar")
        assert _try_prove(Length(StrConcat(a, b)) == Length(a) + Length(b))

    def test_prefix_of(self, kernel):
        assert _try_prove(PrefixOf(StringVal("ab"), StringVal("abc")))