Method test_lambda_constant

tests/test_z3_semantic.py:1327–1331

Select(Lambda(x, 42), anything) = 42

(self, kernel)

        assert _try_prove(Select(f, IntVal(5)) == IntVal(6))

    def test_lambda_constant(self, kernel):
        """Select(Lambda(x, 42), anything) = 42"""
        x = Int("x")
        f = Lambda([x], IntVal(42))
        assert _try_prove(Select(f, IntVal(999)) == IntVal(42))

    def test_lambda_square(self, kernel):
        """Select(Lambda(x, x*x), 7) = 49"""