kdrag.kernel.free_vars

kdrag.kernel.free_vars(e: ExprRef) → set[ExprRef]

Get an overapproximation of free variables in a term. This is used for skolemization.

>>> x,y = smt.Ints("x y")
>>> z = FreshVar("z", smt.IntSort())
>>> assert z in free_vars(x + y + z)