kdrag.utils.occurs

kdrag.utils.occurs(x: ExprRef, t: ExprRef) → bool

Does x occur in t?

>>> x,y,z = smt.Ints("x y z")
>>> assert occurs(x + y, x + y + z)
>>> assert not occurs(x + y, x + z)
>>> assert occurs(x, x + y + z)
>>> v0 = smt.Var(0, smt.IntSort())
>>> assert occurs(v0, v0 + x + y)

Parameters:

• x (ExprRef)

• t (ExprRef)

Return type:

bool