Method test_empty_concat_left

tests/test_z3_semantic.py:809–813

(self, kernel)

        assert len(Tactic("simp [String.append_assoc]").apply(g)) == 0

    def test_empty_concat_left(self, kernel):
        x = String("x")
        g = Goal()
        g.add(StrConcat(StringVal(""), x) == x)
        assert len(Tactic("simp").apply(g)) == 0

    def test_empty_concat_right(self, kernel):
        x = String("x")