Function and its arguments are tracked.
(self)
| 1889 | assert "y" in names |
| 1890 | |
| 1891 | def test_function_vars(self): |
| 1892 | """Function and its arguments are tracked.""" |
| 1893 | f = Function("f", IntSort(), IntSort()) |
| 1894 | x = Int("x") |
| 1895 | app = f(x) |
| 1896 | names = {n for n, _ in app._vars} |
| 1897 | assert "f" in names |
| 1898 | assert "x" in names |
| 1899 | |
| 1900 | def test_uninterpreted_sort_vars(self): |
| 1901 | """DeclareSort introduces a type variable.""" |