kdrag.Undef

kdrag.Undef(sort: SortRef, *args) → ExprRef

Create an “undefined” value possibly dependent on other values. You will not be able to prove anything about this value that is not true of any symbol.

>>> Undef(smt.IntSort())
undef!...
>>> x = smt.Const("x", smt.IntSort())
>>> Undef(smt.IntSort(), x)
f!...(x)

Parameters:

sort (SortRef)

Return type:

ExprRef