Method test_function_decl

tests/test_z3_compat.py:331–339

(self)

        assert isinstance(radd._ast.lhs, IntLit) and radd._ast.lhs.val == 1

    def test_function_decl(self):
        S = DeclareSort("S")
        f = Function("f", IntSort(), S)
        x = Int("x")
        app = f(x)
        # f and S should be free vars
        assert any(n == "f" for n, _ in app._vars)
        var_names = {n for n, _ in app._vars}
        assert "S" in var_names

    def test_nat_var(self):
        n = Nat("n")