Method test_ite_true_branch

tests/test_z3_semantic.py:278–281

If(True, a, b) = a

(self, kernel)

        assert _try_prove(Implies(Implies(Implies(p, q), p), p))

    def test_ite_true_branch(self, kernel):
        """If(True, a, b) = a"""
        a, b = Bool("a"), Bool("b")
        assert _try_prove(If(BoolVal(True), a, b) == a)

    def test_ite_false_branch(self, kernel):
        """If(False, a, b) = b"""